# AudioVMAF: Audio Quality Prediction with VMAF

Arijit Biswas  Sound Tech Research
Dolby Germany GmbH
<EMAIL_ADDRESS>Harald Mundt  Sound Tech Research
Dolby Germany GmbH
<EMAIL_ADDRESS>
###### Abstract

Video Multimethod Assessment Fusion (VMAF) [1],[2],[3] is a popular tool in
the industry for measuring coded video quality. In this study, we propose an
auditory-inspired frontend in existing VMAF for creating videos of reference
and coded spectrograms, and extended VMAF for measuring coded audio quality.
We name our system AudioVMAF. We demonstrate that image replication is capable
of further enhancing prediction accuracy, especially when band-limited anchors
are present. The proposed method significantly outperforms all existing visual
quality features repurposed for audio, and even demonstrates a significant
overall improvement of 7.8% and 2.0% of Pearson and Spearman rank correlation
coefficient, respectively, over a dedicated audio quality metric (ViSQOL-v3
[4]) also inspired from the image domain.

###### Index Terms:

Objective audio quality metrics, video quality metrics, VMAF, ViSQOL, audio
coding, audio signal processing

##  I Introduction

Vision and audition are the richest sources of sensory data that drive the
quality of multimedia experiences. While video storage and transmission
command more resources, audio is also a resource hog and is important to
consumers. Especially since bandwidth-hungry spatial audio [5] is becoming
more pervasive, perceptual audio rate control should be a significant factor
in the quality of experience (QoE) optimization. Therefore, sound-quality
evaluation tests are critical since they provide the necessary user feedback
that drives audio quality improvements. However, subjective listening tests
demand a large amount of time and effort. Thus, there is an impetus to develop
accurate audio quality assessment models.

In the broader context, perceived multimedia QoE is affected by both
perceptual video and audio quality. Quality assessments of audio and video
have both been widely researched for decades yet the two areas have been
largely mutually independent [6]. However, the neurosensory systems of the two
modalities bear similarities. There are both low-level analogous processing
(e.g., masking and multi-scale decomposition) as well as high-level cognitive
modeling leading to a useful fusion of the senses [7]. Furthermore, the
modalities themselves bear similarities that make them inter-convertible,
e.g., using time-frequency representations of audio (spectrograms) to create a
visual format for analysis. So, it is reasonable to consider whether suitable
video quality metrics might be adapted for audio quality prediction.

It has been found in subjective joint audio-visual studies [8] that: (1) video
modality is relatively more important to QoE than the audio modality; (2)
unlike video quality, subjects found it harder to differentiate audio quality
(even with audio bitrates chosen to create large degradation), and (3)
subjects usually judge the quality of each modality sequentially, before
giving an overall rating; suggesting that for a joint audio-visual quality
(AVQ) estimation it makes sense to fuse audio and video quality scores using
posterior fusion strategy [9],[8],[10]. Thus, for an AVQ prediction task,
observation (1) would indicate that it is reasonable to make use of a video
quality metric that is well accepted by the community; observation (2) would
hint that one may not need an incoherent (and consequently a complex) system
architecture. Therefore, for a coherent system design, it becomes valid to ask
the research question, why not derive audio quality from a state-of-the-art
video quality metric?

With the above research question, we propose AudioVMAF to measure audio
quality with the industry-popular VMAF. We are unaware of techniques that
utilize an “out-of-the-box” video quality metric as an audio quality metric.
We are only aware of: (a) adaptation of a set of classical 2D visual quality
indicators for 1D audio signals for measuring audio quality [8]; and (b)
adaptation of a 2D image distortion metric (Structural Similarity Index or
SSIM [11]) to a 2D distortion metric (Neurogram Similarity Index Measure or
NSIM [12]) for measuring speech intelligibility and coded speech [13] and
audio quality [14],[15],[4] with ViSQOL, where the support vector machine
(SVM) [16] is trained for the task. In [8], the 1D variant of 2D visual
quality features was evaluated with stereo audio waveform coded with Advanced
Audio Coding (AAC) at 8, 32, and 128 kb/s. It is expected that the lowest two
bitrates provide an unacceptable audio quality, and differences in decoded
audio bandwidth would already serve as a cue for ranking the quality. We
believe automatic audio quality assessment becomes a challenge when modern
parametric bandwidth extension [17] and parametric stereo coding [17] tools
are utilized at lower bitrates. Thus, we evaluated AudioVMAF with modern audio
codecs for a wide range of bitrates (i.e., quality). Furthermore, unlike the
measures used in [8] and ViSQOL, due to the usage of VMAF, we can predict the
coded audio quality directly on a 0-100 MUSHRA (Multiple Stimuli with Hidden
Reference and Anchor [18]) quality scale; a well-established scale for
assessing audio codecs.

The paper is organized as follows. Section II describes the AudioVMAF
technology. The data used for AudioVMAF evaluation along with the experimental
results are given in Section III, and finally, the conclusion is drawn in
Section IV.

##  II AudioVMAF

VMAF predicts the perceptual video quality of a coded video with respect to an
uncoded reference video. In VMAF, pixel-level data are pooled to create frame-
level image quality measures (Visual Information Fidelity or VIF [19], Detail
Loss Metric or DLM [20]) modified to cover multiple scales of resolution.
Thereafter, different spatial and temporal features are fused using SVM
regression to create frame-level quality scores; and finally, consecutive
frame scores are pooled to produce the final VMAF score.

For audio quality prediction, reference and coded audio signals are extracted
from the corresponding video files (e.g., mp4), and a new set of reference and
coded video files are created containing perceptually motivated spectrograms.
These video files are then fed into VMAF for computing the audio quality score
(Figure 1). Our MATLAB-based framework is built around the FFmpeg [21] tool
which is used for extracting audio from video, creating videos from images,
and for running VMAF. Note that even though the VMAF repository [22] allows
retraining the SVM, in this study, we focused on the proposed auditory-
inspired frontend to VMAF.

Next, we describe how the spectrogram video files are created. Three trivial
steps need to be computed before that: (1) audio is extracted from the video
files, (2) coded audio is resampled to the sample rate of reference audio, and
(3) coded audio is time-aligned with reference audio.

###  II-A Audio to perceptually motivated spectrogram images

First, perceptually motivated power spectrograms of the reference and coded
audio are computed. For stereo audio, left (L), right (R), and mid-signal (M =
0.5(L+R)) are considered. Note that mid-signal has been considered previously
[15],[23] for the coded stereo audio quality prediction task. Next, the
following perceptually inspired setups are employed: (i) analysis with 80
Equivalent Rectangular Bandwidth (ERB) bands [24] in the 30 Hz-18 kHz audible
frequency range, using FFT with a window length of 42.7 ms and Gammatone
filter shape [24] weighting, (ii) the time stride is aligned with the
reference video frame rate (30 fps or 33.3 ms), (iii) the ERB center
frequencies were adjusted to the nearest FFT bin center frequencies to avoid
sampling issues with the relatively low FFT frequency resolution compared to
the narrow Gammatone filter shapes at low frequencies, and (iv) the input
audio is calibrated such that $-25$ dB full-scale sine tone corresponds to 85
dB sound pressure level and signals below the threshold-in-quiet [25] are set
to zero.

###  II-B Framing and timing of spectrogram images

Next, we constructed data frames from the reference and coded spectrograms
individually as follows. At the video frame rate, 32 spectrogram frames
($\approx$1s) are assembled resulting in 2D arrays of size [80$\times$32] for
every audio signal. Then we stacked the 2D arrays for each audio signal on top
of each other which, in the case of stereo audio, results in an array of size
[240$\times$32] due to the three signals L, R, and M. The stacking was done
for a joint analysis of both individual channels as well as their inter-
channel relationships. Finally, for feeding into VMAF, we copy this array as
many times as needed to fit into an image of size 480$\times$640
(height$\times$width). The copying (replication) was done to improve the
quality prediction accuracy of bandlimited audio (see, results in Section
III-B).

###  II-C Color and intensity scaling of spectrogram images

The reference and coded image frames are converted to the dB domain with a
maximum dynamic range of 70 dB. The dB-domain audio data is then quantized
linearly into the [0,255] range. For every frame, the quantized data is used
as an index to the HSV (Hue, Saturation, Value) colormap [26] to create color
images in the Portable Network Graphics (PNG) format. This mapping induces a
non-monotonic conversion from dB to luma, which is then analyzed by VMAF.
Without this mapping from the spectrogram dB-domain to color images using the
HSV colormap, we observed significantly worse audio quality prediction
performance with monotonic grayscale images (see, results in Section III-B).

Figure 1: Utilizing VMAF for both video and audio quality prediction. For
AudioVMAF, reference-coded pairs of perceptually motivated spectrogram videos
are fed to VMAF.

The design choices of AudioVMAF presented in this section were not informed by
the test sets used for its benchmarking. The perceptual front end is similar
in spirit to the perceptual frontend used in ViSQOL-v3. The replication method
was introduced when we observed that the predicted quality of the bandlimited
signals is as high as that of the full-bandwidth signals. The method was found
through experiments. Similarly, the HSV color mapping was also found through
experiments conducted on a typical MUSHRA listening test (different from the
test sets) with 12 excerpts (not present in the test set), involving two
variants of a codec (not present in the test set).

##  III Experiments and Results

###  III-A Test sets

We benchmarked the prediction accuracy of AudioVMAF against subjective
listening scores from the Unified Speech and Audio Coding (USAC) [27]
verification listening tests [28] [29]. These comprehensive tests contain 24
excerpts coded with USAC, High-Efficiency Advanced Audio Coding (HE-AAC), and
Extended Adaptive Multi-Rate – Wideband (AMR-WB+) with bitrates ranging from 8
kb/s mono to 96 kb/s stereo. According to our experience, automatic audio
quality assessment becomes a challenge when parametric coding tools are
activated. Hence, we evaluated AudioVMAF with modern audio codecs which
utilize parametric bandwidth extension and parametric stereo coding tools at
lower bitrates. USAC verification listening tests consist of three separate
listening tests: mono at low bitrates and stereo at both low and high
bitrates. All tests were MUSHRA tests, with a 0-100 quality scale, where a
higher score implies better quality. For the details of these MUSHRA listening
tests, interested readers are referred to [28],[29]. For each of the three
listening tests, we included all the 24 test excerpts, which consist of 8
speech, 8 music, and 8 mixed excerpts (see, Table 4 in [29]).

###  III-B AudioVMAF Benchmarking

We compared the accuracy of AudioVMAF against a dedicated audio quality metric
which is also inherited from the image domain. We decided to use ViSQOL-v3
(operating in audio mode) [30] because the NSIM distortion metric used in
ViSQOL for comparing reference and coded Gammatone spectrograms is inspired by
the 2D image distortion metric. Furthermore, it has been reported in [31],
that out of all objective measures designed to evaluate codecs, ViSQOL shows
the best correlation with subjective scores and achieves high and stable
performance for all content types. Similarly, it was reported in [32] that
overall VISQOL performed very well across five different datasets (see, Table
II in [32], overall correlation with ViSQOL as the teacher).

TABLE I: Performance of AudioVMAF on USAC verification listening tests. The
table shows the correlation coefficients ($R_{p}$ and $R_{s}$) between
predicted objective scores and subjective (MUSHRA) scores for (a) mono
listening test, (b) stereo low-bitrate, and (c) stereo high-bitrate. Note that
AudioVMAF (w/ replication) is enabled with the best settings, i.e., both
replication and HSV colormap.

Model Metric | w/ anchors | w/o anchors
---|---|---
$\mathbf{R_{p}}\uparrow$ | $\mathbf{R_{s}}\uparrow$ | $\mathbf{R_{p}}\uparrow$ | $\mathbf{R_{s}}\uparrow$
ViSQOL-v3 | 0.809 | 0.836 | 0.796 | 0.836
SSIM1D | 0.240 | 0.232 | 0.697 | 0.623
MS-SSIM1D | 0.371 | 0.328 | 0.760 | 0.704
VIFP1D | 0.447 | 0.412 | 0.778 | 0.738
GMSM1D | 0.130 | 0.175 | 0.677 | 0.584
GMSD1D | 0.173 | 0.184 | 0.711 | 0.592
AudioVMAF w/o replication | 0.415 | 0.404 | 0.871 | 0.853
AudioVMAF (w/ replication) | 0.870 | 0.856 | 0.891 | 0.885
AudioVMAF w/o HSV colormap | 0.734 | 0.805 | 0.681 | 0.788

(a)

Model Metric | w/ anchors | w/o anchors
---|---|---
$\mathbf{R_{p}}\uparrow$ | $\mathbf{R_{s}}\uparrow$ | $\mathbf{R_{p}}\uparrow$ | $\mathbf{R_{s}}\uparrow$
ViSQOL-v3 | 0.771 | 0.778 | 0.689 | 0.694
SSIM1D | 0.060 | -0.063 | 0.557 | 0.251
MS-SSIM1D | 0.221 | 0.100 | 0.656 | 0.445
VIFP1D | 0.213 | 0.158 | 0.339 | 0.313
GMSM1D | -0.077 | -0.148 | 0.485 | 0.149
GMSD1D | 0.075 | -0.119 | 0.661 | 0.194
AudioVMAF w/o replication | 0.470 | 0.294 | 0.803 | 0.664
AudioVMAF (w/ replication) | 0.824 | 0.736 | 0.815 | 0.709
AudioVMAF w/o HSV colormap | 0.669 | 0.714 | 0.551 | 0.656

(b)

Model Metric | w/ anchors | w/o anchors
---|---|---
$\mathbf{R_{p}}\uparrow$ | $\mathbf{R_{s}}\uparrow$ | $\mathbf{R_{p}}\uparrow$ | $\mathbf{R_{s}}\uparrow$
ViSQOL-v3 | 0.823 | 0.904 | 0.769 | 0.852
SSIM1D | 0.263 | 0.417 | 0.702 | 0.803
MS-SSIM1D | 0.460 | 0.559 | 0.752 | 0.814
VIFP1D | 0.389 | 0.517 | 0.332 | 0.581
GMSM1D | 0.115 | 0.239 | 0.678 | 0.807
GMSD1D | 0.116 | 0.248 | 0.738 | 0.797
AudioVMAF w/o replication | 0.751 | 0.831 | 0.834 | 0.894
AudioVMAF (w/ replication) | 0.909 | 0.938 | 0.818 | 0.898
AudioVMAF w/o HSV colormap | 0.797 | 0.896 | 0.550 | 0.825

(c)

In addition, we benchmark against a related prior research [8], where 1D
variants of the popular video frame/picture quality predictors, e.g., SSIM
[11], Multi-scale Structural Similarity Index (MS-SSIM) [33], Visual
Information Fidelity in the pixel domain (VIFP) [19], Gradient Magnitude
Similarity Mean (GMSM) [34], and Gradient Magnitude Similarity Deviation
(GMSD) [34] were used to predict audio quality. These measures were defined
using 1D data windows and are denoted with a subscript 1D in Table I. We
utilize the implementation [35] provided by the authors [8]. Note that in the
implementation, SSIM1D, MS-SSIM1D, VIFP1D, GMSM1D are bounded between [0, 1],
whereas GMSD1D is bounded between [0.687, 1]. ViSQOL-v3 on the other hand is
trained to predict the Mean Opinion Score (MOS) (between 1 and 5), but it is
observed to be bounded between [1, 4.732] [36],[30]. Furthermore, none of the
benchmarks are designed for stereo. Internally, ViSQOL-v3 downmixes stereo to
a mono mid-signal and then predicts the MOS. Whereas, the 1D visual quality
measures (as implemented [35]) consider only the left channel. However, to
make them at least comparable with ViSQOL-v3, we report the results by
considering the mono mid signal. For stereo audio, AudioVMAF considers left
(L), right (R), and mid-signal (M) by stacking spectrograms of L, R, and M
channels in the image. We used the Spearman rank-order correlation coefficient
($R_{s}$) to measure the prediction monotonicity of the models and the Pearson
linear correlation coefficient ($R_{p}$) to measure the prediction linearity.
For both $R_{p}$ and $R_{s}$, larger values denote better performance. The
prediction accuracy on three listening tests is presented in Table I.

It can be observed that none of the 1D visual quality features are competitive
in predicting the audio quality if the (3.5 kHz and 7 kHz) bandlimited anchors
are included. We observed that the quality of the anchors was significantly
overestimated (almost as high as the reference quality). Excluding the anchors
improves the accuracy, but none of them outperform ViSQOL-v3. Considering all
three tests, the top two 1D visual quality features are MS-SSIM and VIFP,
indicating the importance of multi-scale modeling and natural statistics-based
features also for audio quality prediction. On the contrary, AudioVMAF
significantly outperforms 1D visual quality features both with and without the
anchors; and performs as well or better than ViSQOL-v3 if anchors are
excluded. We further enhanced the performance with anchors by replicating the
data (see, Section II-B). Overall, across all three listening tests, we
demonstrate a significant improvement ($7.8\%$ and $2\%$ improvement of
Pearson’s and Spearman’s Rank correlation coefficient, respectively) over
ViSQOL-v3. We can also observe that if we do not perform the mapping from the
spectrogram dB-domain to color images using the HSV colormap (see, Section
II-C), the prediction performance of AudioVMAF is significantly degraded.
Furthermore, since the predicted AudioVMAF scores are between 0-100, we can
also easily compute (without any audio quality scale conversion or mapping)
and report the outlier ratios [37] for the AudioVMAF with its best settings
(i.e., with replication and HSV colormap) enabled: 0.740 (mono test), 0.742
(stereo low bitrate test), and 0.773 (stereo high bitrate test).

Finally, we coded the 24 stereo excerpts for a wide range of bitrates using
the (HE)-AAC family of codecs typically used in practice, and demonstrate
(Figure 2) that the mean AudioVMAF score scales with the bitrates. This
observation, along with the strong performance in predicting the subjective
quality (presented in Table I) makes AudioVMAF also suitable for bitrate
laddering (similar to the popular application of VMAF [38]).

Figure 2: Scaling of AudioVMAF scores with bitrates: 24 stereo excerpts coded
with HE-AAC (v1 or v2) and AAC.

##  IV Conclusion and Discussion

In this paper, we present AudioVMAF: a novel “out-of-the-box” VMAF-based coded
audio quality prediction model for 48 kHz sample rate. Our contribution can be
viewed as a perceptual preprocessing to VMAF. We expanded to predict coded
stereo audio quality by stacking spectrograms of left, right, and mid channels
in the image. Furthermore, we found that replicating images leads to improved
prediction accuracy when bandlimited anchors are included. Interestingly, we
also found that the mapping from the spectrogram dB-domain to color images
using the HSV colormap is needed for a reasonable prediction performance. In
the future, we would like to extend the AudioVMAF for multi-channel coded
audio quality prediction, improve the sensitivity of the method at high
bitrates, and investigate re-training the SVM with subjective listening test
data. Finally, for explaining our findings with AudioVMAF, it is worth
understanding the implementation details of VMAF and the dataset that was used
for its training. Such insights informed by our observations might trigger
ideas for improving also VMAF for image and video quality assessment.

With this research, we provide a new angle for developing an audio quality
metric. The proposed method is a step towards merging coded audio and video
quality prediction tasks which may pave a new way for AVQ modeling using a
coherent architecture.

## References

  * [1] Netflix Technology Blog. (2016, June) Toward a practical perceptual video quality metric. [Online]. Available: https://netflixtechblog.com/toward-a-practical-perceptual-video-quality-metric-653f208b9652
  * [2] ——. (2020, December) Toward a better quality metric for the video community. [Online]. Available: https://netflixtechblog.com/toward-a-better-quality-metric-for-the-video-community-7ed94e752a30
  * [3] ——. (2018, October) Vmaf: The journey continues. [Online]. Available: https://medium.com/netflix-techblog/vmaf-the-journey-continues-44b51ee9ed12
  * [4] M. Chinen, F. S. C. Lim, J. Skoglund, N. Gureev, F. O’Gorman, and A. Hines, “ViSQOL v3: An open source production ready objective speech and audio metric,” _2020 Twelfth International Conference on Quality of Multimedia Experience (QoMEX)_ , May 2020.
  * [5] Netflix Technology Blog. (2019, September) Engineering a studio quality experience with high-quality audio at netflix. [Online]. Available: https://netflixtechblog.com/engineering-a-studio-quality-experience-with-high-quality-audio-at-netflix-eaa0b6145f32
  * [6] Z. Akhtar and T. H. Falk, “Audio-visual multimedia quality assessment: A comprehensive survey,” _IEEE Access_ , vol. 5, pp. 21 090–21 117, 2017\.
  * [7] M. O. Ernst and H. H. Bülthoff, “Merging the senses into a robust percept,” _Trends in Cognitive Sciences_ , vol. 8, no. 4, pp. 162–169, 2004.
  * [8] X. Min, G. Zhai, J. Zhou, M. C. Q. Farias, and A. C. Bovik, “Study of subjective and objective quality assessment of audio-visual signals,” _IEEE Transactions on Image Processing_ , vol. 29, pp. 6054–6068, 2020.
  * [9] J. G. Beerends and F. E. de Caluwe, “The influence of video quality on perceived audio quality and vice versa,” _Journal of the Audio Engineering Society_ , vol. 47, no. 5, pp. 355–362, May 1999.
  * [10] H. B. Martinez, A. Hines, and M. C. Farias, “See hear now: is audio-visual qoe now just a fusion of audio and video metrics?” in _2022 14th International Conference on Quality of Multimedia Experience (QoMEX)_ , 2022, pp. 1–4.
  * [11] Z. Wang, A. Bovik, H. Sheikh, and E. Simoncelli, “Image quality assessment: from error visibility to structural similarity,” _IEEE Transactions on Image Processing_ , vol. 13, no. 4, pp. 600–612, 2004.
  * [12] “Speech intelligibility prediction using a neurogram similarity index measure,” _Speech Communication_ , vol. 54, no. 2, pp. 306–320, 2012.
  * [13] A. Hines, J. Skoglund, A. C. Kokaram, and N. Harte, “ViSQOL: an objective speech quality model,” _EURASIP Journal on Audio, Speech, and Music Processing_ , vol. 2015, no. 1, p. 13, May 2015.
  * [14] A. Hines, E. Gillen, D. Kelly, J. Skoglund, A. Kokaram, and N. Harte, “ViSQOLAudio: an objective audio quality metric for low bitrate codecs,” _The Journal of the Acoustical Society of America_ , vol. 137, no. 6, pp. 449–455, June 2015.
  * [15] C. Sloan, N. Harte, D. Kelly, A. C. Kokaram, and A. Hines, “Objective assessment of perceptual audio quality using visqolaudio,” _IEEE Transactions on Broadcasting_ , vol. 63, no. 4, pp. 693–705, 2017.
  * [16] C. Cortes and V. Vapnik, “Support-vector networks,” _Machine learning_ , vol. 20, pp. 273–297, 1995.
  * [17] A. C. den Brinker, J. Breebaart, P. Ekstrand, J. Engdegard, F. Henn, K. Kjoerling, W. Oomen, and H. Purnhagen, “An overview of the coding standard MPEG-4 audio amendments 1 and 2: HE-AAC, SSC, and HE-AAC v2,” _EURASIP Journal on Audio, Speech, and Music Processing_ , vol. 2009, no. 1, 2009.
  * [18] “Method for the subjective assessment of intermediate quality level of audio systems,” International Telecommunication Union, Standard Recommendation ITU-R BS.1534-3, 2015.
  * [19] H. Sheikh and A. Bovik, “Image information and visual quality,” _IEEE Transactions on Image Processing_ , vol. 15, no. 2, pp. 430–444, 2006.
  * [20] S. Li, F. Zhang, L. Ma, and K. N. Ngan, “Image quality assessment by separately evaluating detail losses and additive impairments,” _IEEE Transactions on Multimedia_ , vol. 13, no. 5, pp. 935–949, 2011.
  * [21] FFmpeg. (2023) FFmpeg. https://www.ffmpeg.org/.
  * [22] Netflix. (2023) VMAF - Video Multi-Method Assessment Fusion. https://github.com/Netflix/vmaf/.
  * [23] A. Biswas and G. Jiang, “Stereo inse-net: Stereo audio quality predictor transfer learned from mono inse-net,” in _153rd AES Convention_ , October 2022.
  * [24] B. C. Moore, _An introduction to the psychology of hearing_. Brill, 2012.
  * [25] A. Spanias, T. Painter, and V. Atti, _Audio signal processing and coding_. John Wiley & Sons, 2006.
  * [26] MATLAB. (2023) HSV Colormap Array. https://www.mathworks.com/help/matlab/ref/hsv.html/.
  * [27] S. Quackenbush, “Mpeg unified speech and audio coding,” _IEEE MultiMedia_ , vol. 20, no. 2, pp. 72–78, 2013.
  * [28] “Usac verification test report,” International Organisation for Standardisation, Torino, Italy, Tech. Rep. ISO/IEC JTC1/SC29/WG1 MPEG2011/N12232, 2011.
  * [29] S. Quackenbush and R. Lefevbre, “Performance of MPEG unified speech and audio coding,” in _131st AES Convention_ , October 2011.
  * [30] Google. (2022) ViSQOL. https://github.com/google/visqol/.
  * [31] P. M. Delgado and J. Herre, “Can we still use PEAQ? a performance analysis of the ITU standard for the objective assessment of perceived audio quality,” in _2020 Twelfth International Conference on Quality of Multimedia Experience (QoMEX)_ , 2020, pp. 1–6.
  * [32] C.-W. Wu, P. A. Williams, and W. Wolcott, “A multitask teacher-student framework for perceptual audio quality assessment,” in _2021 29th European Signal Processing Conference (EUSIPCO)_ , 2021, pp. 396–400.
  * [33] Z. Wang, E. Simoncelli, and A. Bovik, “Multiscale structural similarity for image quality assessment,” in _The Thrity-Seventh Asilomar Conference on Signals, Systems and Computers, 2003_ , vol. 2, 2003, pp. 1398–1402 Vol.2.
  * [34] W. Xue, L. Zhang, X. Mou, and A. C. Bovik, “Gradient magnitude similarity deviation: A highly efficient perceptual image quality index,” _IEEE Transactions on Image Processing_ , vol. 23, no. 2, pp. 684–695, 2014.
  * [35] LIVE. (2020) AVQA. https://github.com/utlive/avqa/.
  * [36] G. Jiang, A. Biswas, C. Bergler, and A. Maier, “Inse-net: A perceptually coded audio quality model based on cnn,” in _151st AES Convention_ , October 2021.
  * [37] G. Yi, W. Xiao, Y. Xiao, B. Naderi, S. Möller, W. Wardah, G. Mittag, R. Culter, Z. Zhang, D. S. Williamson, F. Chen, F. Yang, and S. Shang, “ConferencingSpeech 2022 Challenge: Non-intrusive Objective Speech Quality Assessment (NISQA) Challenge for Online Conferencing Applications,” in _Proc. Interspeech 2022_ , 2022, pp. 3308–3312.
  * [38] A. V. Katsenou, F. Zhang, K. Swanson, M. Afonso, J. Sole, and D. R. Bull, “Vmaf-based bitrate ladder estimation for adaptive streaming,” in _2021 Picture Coding Symposium (PCS)_ , 2021, pp. 1–5.


11institutetext:  RChain Cooperative
11email<EMAIL_ADDRESS>22institutetext: Pyrofex Corp.
22email<EMAIL_ADDRESS>

# Name-free combinators for concurrency

L.G. Meredith
11 Michael Stay
22

###### Abstract

Yoshida demonstrated how to eliminate the bound names coming from the input
prefix in the asynchronous $\pi$-calculus, but her combinators still depend on
the $\mathsf{new}$ operator to bind names. We modify Yoshida’s combinators by
replacing $\mathsf{new}$ and replication with reflective operators to provide
the first combinator calculus with no bound names into which the asynchronous
$\pi$-calculus has a faithful embedding.

##  1 Introduction

Many term calculi, like $\lambda$-calculus or $\pi$-calculus, involve binders
for names, and the mathematics of bound variable names is subtle. Schönfinkel
introduced the SKI combinator calculus in 1924 to clarify the role of
quantified variables in intuitionistic logic by eliminating them [8]; Curry
developed Schönfinkel’s ideas much further. The difficulties are not merely
theoretical, but represent a real practical challenge in the design of
programming languages. In fact binding is one of the key features of the
PoPLMark Challenge [1]. Certainly, the recent work by Jamie Gabbay and Andrew
Pitts [3] and others [2] on nominal set theory has put the study of bound
names and substitution on a much nicer foundation that can be shown to extend
to practical implementations. However, it introduces an intriguing conundrum.

Specifically, the work of Gabbay and Pitts relies on a version of set theory
(Fraenkel-Mostowski set theory, which we abbreivate to FM set theory) that
admits an infinite supply of “atoms”. This raises the question of where these
atoms come from, which has both theoretical and practical implications. On the
practical side, infinite sets of “atomic” entities, i.e. entities with no
internal structure, are not realizable on modern computers. Modern computers
fundamentally rely on sets of elements with effective internal structure to
provide the kind of compression necessary to produce or compute with infinite
sets. The natural numbers is a prime example. Because of their very regular
internal structure the entire set can be represented by a single recursive
equation. Potentially then, the natural numbers or some other effectively
representable set could provide the source of atoms used in an FM-set
theoretic account of binding in practical implementations. However, this
raises a new question.

In order to represent and compute these effectively representable sets a
notion of computation must already be in place. If that notion of computation
relies on a notion of binding, then not a lot progress has been made! As in
[5] we argue that this circularity, instead of being an obstacle to overcome,
might be a clue to an alternative approach to binding phenomena; and one that
ties together two important computational phenomena that have not normally
been considered as related. More explicitly, we extend the argument made by
Meredith and Radestock that reflection suffices to provide the “atoms” used in
the $\pi$-calculus as channels to produce the first name-free set of
combinators that enjoys a full and faithful interpretation of the calculus.

While the focus of the paper is largely on the technical results it is useful
to consider the larger context motivating them. Reflection and meta-
programming features more generally are part of a growing number of mainstream
languages. Java, C#, even the Haskell and OCaml communities have seen growing
interest in these features with efforts like template Haskell and MetaOCaml,
respectively. In large measure this has to do the fact that programming at
industrial scale requires the leverage of computer programs to write computer
programs. Thus, meta-programming features are simply a practical necessity. On
the other hand, reflection and meta-programming have not received a
theoretical account that fits well with strong typing. This is one of the
reasons why language designs based on typed $\lambda$-calculi have been so
slow to adopt reflection as a feature by comparison to other language designs.

In this setting, the idea that a single feature already enjoying widespread
adoption could account for such a subtle phenomenon as the kind of binding
found in the $\pi$-calculus is both intriguing and worth exploring, even if FM
set theory provides a satisfying account of computation with nominal phenomena
in other respects. However, it is precisely the foundational theoretical
questions raised by the FM set theoretic approach that motivates the
investigation in the first place: what better place to look for the source of
“atoms” than in the reification of theory of computation requiring them?

To be clear, we are not focusing on ordinary abstraction, as that is well
solved by abstraction elimination from the $\lambda$-calculus to
$\mathcal{SKI}$. Instead we are focused on binders for fresh names. For
example, the $\pi$-calculus ([6]) has two binders for names: the
$\mathsf{new}$ operator, which introduces a new name into scope, and the input
prefix, which introduces a name for labeling locations for substitution.
Yoshida [10] describes an elimination algorithm that gets rid of input
prefixes which corresponds in many respects to the elimination of lambda
abstraction; but her combinators still fundamentally depend on the
$\mathsf{new}$ operator. In complementary work, Meredith and Radestock [5]
introduce reflective operators into a higher-order $\pi$-calculus and implment
$\mathsf{new}$ and replication in terms of reflection. Here, we present a
fusion of those ideas: a name-free concurrent combinator calculus into which
Yoshida’s combinators have a faithful embedding.

####  1.0.1 Outline of the paper

To be fully self-contained this paper would need to present four different
calculi and two different encodings: the original $\pi$-calculus, Yoshida’s
combinator calculus, and the encoding from the term calculus to the
combinator; the $\rho$-calculus, and the encoding from the $\pi$-calculus to
the $\rho$-calculus and the new reflective combinator calculus, and the
encoding from the term calculus to the reflective combinator calculus. Such a
manifest provides all the technical inventory to illustrate how the two
encoding techniques, prefix elimination and $\mathsf{new}$ elimination,
combine and how the encoding from the $\pi$-calculus can be constructed by
composing the encoding into the $\rho$-calculus with the encoding into the
reflective combinator calculus. We have provided the complete manifest, but
have pushed the presentation of the $\rho$-calculus and the $\pi$-calculus and
the encoding of the latter into the former in an appendix at the end as the
$\pi$-calculus is quite well known at this point, and the $\rho$-calculus has
been part of the concurrency literature for over a decade. This organization
allows us to focus on the newer results of a name-free combinator calculus for
mobile concurrency.

##  2 A reflective higher-order concurrent combinator calculus

###  2.1 Yoshida’s original combinator calculus

This is the briefest account of Yoshida’s original calculus while her paper,
which is nearly 20 years old, is still an outstanding piece of research and
well worth the effort to read in conjunction with these results.

atom
$\displaystyle\displaystyle{P\mathbin{\mathbf{::=}}0\;|\;\mathsf{m}(a,b)\;|\;\mathsf{d}(a,b,c)\;|\;\mathsf{k}(a)\;|\;\mathsf{fw}(a,b)\;|\;\mathsf{b}_{\mathsf{r}}(a,b)\;|\;\mathsf{b}_{\mathsf{l}}(a,b)\;|\;\mathsf{s}(a,b,c)}$
process
$\displaystyle\displaystyle{\mathbin{\mathbf{\mid}}\;(\mathsf{new}\;a)P\;|\;P|P\;|\;\mathsf{*}P}$

We write $\mathsf{c};\mathsf{c′};\ldots;$ to denote these agents.
$\mathsf{m}(a,b)$ (message) carries $a$ name $b$ to name $a$, $\mathsf{d}$
(duplicator) distributes a message to two locations, $\mathsf{fw}$ (forwarder)
forwards a message (thus linking two locations), $\mathsf{k}$ (killer) kills a
message, while $\mathsf{b}_{\mathsf{r}}$ (right binder),
$\mathsf{b}_{\mathsf{l}}$ (left binder) and $\mathsf{s}$ (synchroniser)
generate new links. In particular $\mathsf{b}_{\mathsf{r}}$ and
$\mathsf{b}_{\mathsf{l}}$ represent two different ways of binding names – in
$\mathsf{b}_{\mathsf{r}}$ one uses the received name for output, while in
$\mathsf{b}_{\mathsf{l}}$ one uses it for input. In contrast, $\mathsf{s}$ is
used for pure synchronisation without value passing, which is indeed necessary
in interaction scenarios.

As in the $\pi$-calculus, the $\mathsf{new}$ operator is a binding operator
for names, so Yoshida’s calculus also has a notion of free and bound names.

$\displaystyle\mathbin{\mathsf{FN}(\mathbin{0})}:=\emptyset\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(\mathsf{k}(a))}:=\\{a\\}\penalty 50\hskip 20.00003pt
plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(\mathsf{m}(a,b))}=\mathbin{\mathsf{FN}(f(a,b))}=\mathbin{\mathsf{FN}(\mathsf{b}_{\mathsf{r}}(a,b))}=\mathbin{\mathsf{FN}(\mathsf{b}_{\mathsf{l}}(a,b))}:=\\{a,b\\}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(\mathsf{d}(a,b,c))}=\mathbin{\mathsf{FN}(\mathsf{s}(a,b,c))}:=\\{a,b,c\\}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}((\mathsf{new}\;a)P)}:=\mathbin{\mathsf{FN}(P)}\setminus\\{a\\}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(P|Q)}:=\mathbin{\mathsf{FN}(P)}\cup\mathbin{\mathsf{FN}(Q)}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(!P)}:=\mathbin{\mathsf{FN}(P)}$

The bound names of a process, $\mathbin{\mathsf{BN}(P)}$, are those names
occurring in $P$ that are not free. For example, in
$(\mathsf{new}\;b)\mathsf{m}(a,b)$, the name $a$ is free, while $b$ is bound.

In the following definition, $\stackrel{{\scriptstyle\rightharpoonup}}{{x}}$
indicates a list of names, $u:\stackrel{{\scriptstyle\rightharpoonup}}{{x}}$
indicates the concatenation of $u$ onto the vector, and abuse set notation
$u\in\stackrel{{\scriptstyle\rightharpoonup}}{{x}}$ to assert or require that
$u$ occurs in $\stackrel{{\scriptstyle\rightharpoonup}}{{x}}$.

###### Definition 1

Two processes, $P,Q$, are alpha-equivalent if
$P=Q\\{\stackrel{{\scriptstyle\rightharpoonup}}{{y}}/\stackrel{{\scriptstyle\rightharpoonup}}{{x}}\\}$
for some
$\stackrel{{\scriptstyle\rightharpoonup}}{{x}}\in\mathbin{\mathsf{BN}(Q)},\stackrel{{\scriptstyle\rightharpoonup}}{{y}}\in\mathbin{\mathsf{BN}(P)}$,
where
$Q\\{\stackrel{{\scriptstyle\rightharpoonup}}{{y}}/\stackrel{{\scriptstyle\rightharpoonup}}{{x}}\\}$
denotes the capture-avoiding substitution of
$\stackrel{{\scriptstyle\rightharpoonup}}{{y}}$ for
$\stackrel{{\scriptstyle\rightharpoonup}}{{x}}$ in $Q$.

###### Definition 2

The structural congruence $\equiv$ between processes [7] is the least
congruence containing alpha-equivalence and satisfying the commutative monoid
laws (associativity, commutativity and as identity) for parallel composition
$|$.

Rewrite rules

$\begin{array}[]{rl}\mathsf{d}(a,b,c)|\mathsf{m}(a,x)&\rightarrow\mathsf{m}(b,x)|\mathsf{m}(c,x)\\\
\mathsf{k}(a)|\mathsf{m}(a,x)&\rightarrow 0\\\
\mathsf{fw}(a,b)|\mathsf{m}(a,x)&\rightarrow\mathsf{m}(b,x)\\\
\end{array}\quad\quad\begin{array}[]{rl}\mathsf{b}_{\mathsf{r}}(a,b)|\mathsf{m}(a,x)&\rightarrow\mathsf{fw}(b,x)\\\
\mathsf{b}_{\mathsf{l}}(a,b)|\mathsf{m}(a,x)&\rightarrow\mathsf{fw}(x,b)\\\
\mathsf{s}(a,b,c)|\mathsf{m}(a,x)&\rightarrow\mathsf{fw}(b,c)\end{array}$
$\begin{array}[]{rl}\mathsf{*}P&\rightarrow P|\mathsf{*}P\\\ \end{array}$
$\displaystyle\displaystyle{\hbox{\hskip
13.85675pt\vbox{\hbox{\hskip-13.85675pt\hbox{\hbox{$\displaystyle\displaystyle{{P}\rightarrow{P}^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
21.76237pt\vbox{\vbox{}\hbox{\hskip-21.76237pt\hbox{\hbox{$\displaystyle\displaystyle{{{P}|{Q}}\rightarrow{{P}^{\prime}|{Q}}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
56.9297pt\vbox{\hbox{\hskip-56.9297pt\hbox{\hbox{$\displaystyle\displaystyle{{{P}\mathbin{\equiv}{P}^{\prime}}\quad\quad{{P}^{\prime}\rightarrow{Q}^{\prime}}\quad\quad{{Q}^{\prime}\mathbin{\equiv}{Q}}}$}}}\vbox{}}}\over\hbox{\hskip
13.13501pt\vbox{\vbox{}\hbox{\hskip-13.13501pt\hbox{\hbox{$\displaystyle\displaystyle{{P}\rightarrow{Q}}$}}}}}}$

####  2.1.1 Translating the $\pi$-calculus into Yoshida’s combinators

We assume the following annotations ($+$ stands for the output and $-$ stands
for the input), which denote how each name is used in the rules of
interaction:

$\mathsf{m}(a^{+},v^{\pm});\mathsf{d}(a^{−},b^{+},c^{+});\mathsf{k}(a^{−});\mathsf{fw}(a^{−},b^{+});\mathsf{b}_{\mathsf{l}}(a^{−}b^{+});\mathsf{b}_{\mathsf{r}}(a^{−}b^{−});\mathsf{s}(a^{−}b^{−}c^{+})$

Note the annotated polarities are preserved by reduction, e.g.

$\mathsf{d}(a^{−},b^{+},c^{+})|\mathsf{m}(a^{+},v)\to\mathsf{m}(b^{+},v)|\mathsf{m}(b^{+},v)$

$\displaystyle[\\![a!(b)]\\!]=\mathsf{m}(a,b)\penalty 50\hskip 20.00003pt plus
0.5fil minus 5.0pt[\\![\mathsf{for}(x\leftarrow
a)P]\\!]=\mathsf{for}^{*}(x\leftarrow a)[\\![P]\\!]\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt[\\![P|Q]\\!]=[\\![P]\\!]|[\\![Q]\\!]\penalty 50\hskip 20.00003pt plus
0.5fil minus
5.0pt[\\![(\mathsf{new}\;x)P]\\!]=(\mathsf{new}\;x)[\\![P]\\!]\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt[\\![\mathsf{*}P]\\!]=\mathsf{*}[\\![P]\\!]\penalty 50\hskip 20.00003pt
plus 0.5fil minus 5.0pt[\\![0]\\!]=0$

where

$\begin{array}[]{llrl}(I)&\mathsf{for}^{*}(x\leftarrow
a)(P|Q)&=&(\mathsf{new}\;c_{1}c_{2})(\mathsf{d}(a,c_{1},c_{2})|\mathsf{for}^{*}(x\leftarrow
c_{1})P|\mathsf{for}^{*}(x\leftarrow c_{2})Q)\\\
(II)&\mathsf{for}^{*}(x\leftarrow
a)(\mathsf{new}\;c^{\prime})P&=&(\mathsf{new}\;c)\mathsf{for}^{*}(x\leftarrow
a)P\\{c/c^{\prime}\\}\\\ (III)&\mathsf{for}^{*}(x\leftarrow
a)\mathbin{0}&=&\mathsf{k}(a)\\\ (IV)&\mathsf{for}^{*}(x\leftarrow
a)\mathsf{*}P&=&(\mathsf{new}\;c)(\mathsf{fw}(a,c)|\mathsf{*}\mathsf{for}^{*}(x\leftarrow
c)(P|\mathsf{m}(c,x)))\\\ (V)&\mathsf{for}^{*}(x\leftarrow
a)c(v^{+},\vec{w})&=&(\mathsf{new}\;c)(\mathsf{s}(a,c,v)|c(c^{+},\vec{w}))\mbox{\quad$x\notin\\{v\vec{w}\\}$}\\\
(VI)&\mathsf{for}^{*}(x\leftarrow
a)c(v^{-},\vec{w})&=&(\mathsf{new}\;c)(\mathsf{s}(a,v,c)|c(c^{-},\vec{w}))\mbox{\quad$x\notin\\{v\vec{w}\\}$}\\\
(VII)&\mathsf{for}^{*}(x\leftarrow
a)\mathsf{m}(v,x)&=&\mathsf{fw}(a,v)\mbox{\quad$x\neq v$}\\\
(VIII)&\mathsf{for}^{*}(x\leftarrow
a)\mathsf{fw}(x,v)&=&\mathsf{b}_{\mathsf{l}}(a,v)\mbox{\quad$x\neq v$}\\\
(IX)&\mathsf{for}^{*}(x\leftarrow
a)\mathsf{fw}(v,x)&=&\mathsf{b}_{\mathsf{r}}(a,v)\mbox{\quad$x\neq v$}\\\
(X)&\mathsf{for}^{*}(x\leftarrow
a)c(\vec{v}_{1}x^{+}\vec{v}_{2})&=&(\mathsf{new}\;c)\mathsf{for}^{*}(x\leftarrow
a)(\mathsf{fw}(c,x)|c(\vec{v}_{1}c\vec{v}_{2}))\mbox{\quad$x\notin\vec{v}_{1}$}\\\
(XI)&\mathsf{for}^{*}(x\leftarrow
a)c(x^{-}\vec{v})&=&(\mathsf{new}\;c)\mathsf{for}^{*}(x\leftarrow
a)(\mathsf{fw}(x,c)|c(c\vec{v}))\\\ (XII)&\mathsf{for}^{*}(x\leftarrow
a)\mathsf{b}_{\mathsf{r}}(v,x^{-})&=&(\mathsf{new}\;c_{1}c_{2}c_{3})\mathsf{for}^{*}(x\leftarrow
a)(\mathsf{d}(v,c_{1},c_{2})|\mathsf{s}(c_{1},x,c_{3})|\mathsf{b}_{\mathsf{r}}(c_{2},c_{3}))\mbox{\quad$x\notin\\{v\\}$}\\\
(XIII)&\mathsf{for}^{*}(x\leftarrow
a)\mathsf{s}(v,x^{-},w)&=&(\mathsf{new}\;c_{1}c_{2})\mathsf{for}^{*}(x\leftarrow
a)(\mathsf{s}(v,c_{1},c_{2})|\mathsf{m}(c_{1},x)|\mathsf{b}_{\mathsf{l}}(c_{2},w))\mbox{\quad$x\notin\\{v\\}$}\end{array}$

###  2.2 Reflective higher-order (RHO) combinator calculus

The $\pi$-calculus is not a closed theory, but rather a theory dependent upon
some theory of names. Taking an operational view, one may think of the
$\pi$-calculus as a procedure that when handed a theory of names provides a
theory of processes that communicate over those names. This openness of the
theory has been exploited in $\pi$-calculus implementations like the execution
engine in Microsoft’s Biztalk [4], where an ancillary binding language
provides a means of specifying a ‘theory’ of names: e.g., names may be TCP/IP
ports, or URLs, or object references, etc. But foundationally, one might ask
if there is a closed theory of processes, i.e. one in which the theory of
names arises from and is wholly determined by the theory of processes.
Meredith and Radestock have shown that this is not only possible, but results
in a calculus that enjoys both the features of concurrency and meta-
programming [5]. The key idea is to provide the ability to quote processes,
effectively reifying them as names, and to unquote them, effectively
reflecting names back as processes.

The same technique can be applied to Yoshida’s combinators. We remove new
names and replication, introduce quoting/unquoting operators, allow processes
in the second argument of a send, and introduce an extra rewrite governing the
interaction between sending and unquoting.

atom
$\displaystyle\displaystyle{P\mathbin{\mathbf{::=}}0\;|\;\mathsf{m}(a,P)\;|\;\mathsf{d}(a,b,c)\;|\;\mathsf{k}(a)\;|\;\mathsf{fw}(a,b)\;|\;\mathsf{b}_{\mathsf{r}}(a,b)\;|\;\mathsf{b}_{\mathsf{l}}(a,b)\;|\;\mathsf{s}(a,b,c)}$
process $\displaystyle\displaystyle{\mathbin{\mathbf{\mid}}\;*a\;|\;P|P}$
nominal $\displaystyle\displaystyle{a\mathbin{\mathbf{::=}}\mathsf{@}P}$

Rewrite rules

$\begin{array}[]{rl}\mathsf{d}(a,b,c)|\mathsf{m}(a,P)&\rightarrow\mathsf{m}(b,P)|\mathsf{m}(c,P)\\\
\mathsf{k}(a)|\mathsf{m}(a,P)&\rightarrow 0\\\
\mathsf{fw}(a,b)|\mathsf{m}(a,P)&\rightarrow\mathsf{m}(b,P)\\\
\mathsf{b}_{\mathsf{r}}(a,b)|\mathsf{m}(a,P)&\rightarrow\mathsf{fw}(b,@(P))\\\
\end{array}\quad\quad\begin{array}[]{rl}\mathsf{b}_{\mathsf{l}}(a,b)|\mathsf{m}(a,P)&\rightarrow\mathsf{fw}(@(P),b)\\\
\mathsf{s}(a,b,c)|\mathsf{m}(a,P)&\rightarrow\mathsf{fw}(b,c)\\\
(a)|\mathsf{m}(a,P)&\rightarrow P\end{array}$
$\displaystyle\displaystyle{\hbox{\hskip
13.85675pt\vbox{\hbox{\hskip-13.85675pt\hbox{\hbox{$\displaystyle\displaystyle{{P}\rightarrow{P}^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
21.76237pt\vbox{\vbox{}\hbox{\hskip-21.76237pt\hbox{\hbox{$\displaystyle\displaystyle{{{P}|{Q}}\rightarrow{{P}^{\prime}|{Q}}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
56.9297pt\vbox{\hbox{\hskip-56.9297pt\hbox{\hbox{$\displaystyle\displaystyle{{{P}\mathbin{\equiv}{P}^{\prime}}\quad\quad{{P}^{\prime}\rightarrow{Q}^{\prime}}\quad\quad{{Q}^{\prime}\mathbin{\equiv}{Q}}}$}}}\vbox{}}}\over\hbox{\hskip
13.13501pt\vbox{\vbox{}\hbox{\hskip-13.13501pt\hbox{\hbox{$\displaystyle\displaystyle{{P}\rightarrow{Q}}$}}}}}}$

###### Definition 3

The structural congruence $\equiv$ between processes [7] is the least
congruence satisfying the commutative monoid laws (associativity,
commutativity and as identity) for parallel composition $|$ and $*(@(P))\equiv
P$.

Note that alpha equivalence is no longer part of structural congruence. While
there is a faithful embedding of Yoshida’s combinators into RHO combinators
(see below), RHO combinators can see the internal structure of names and
distinguish them.

####  2.2.1 Implementing replication with reflection

As mentioned before, it is known that replication (and hence recursion) can be
implemented in a higher-order process algebra [7]. As our first example of
calculation with the machinery thus far presented we give the construction
explicitly in the RHO combinator calculus.

######  Definition 4 (Replication)

$D(x,v,w):=(\mathsf{d}(x,v,w)|\mathsf{fw}(v,x)|{*}(w))$

$\begin{array}[]{rl}\mathsf{*}_{(x,v,w)}P&=\mathsf{m}(x,D(x,v,w)\;|\;P)\;|\;D(x,v,w)\\\
&=\mathsf{d}(x,v,w)\;|\;\mathsf{fw}(v,x)\;|\;{*}(w)\;|\;\mathsf{m}(x,D(x,v,w)\;|\;P)\\\
&\rightarrow\mathsf{m}(v,D(x,v,w)\;|\;P)\;|\;\mathsf{m}(w,D(x,v,w)\;|\;P)\;|\;\mathsf{fw}(v,x)\;|\;{*}(w)\;|\;\mathsf{m}(x,D(x,v,w)\;|\;P)\\\
&\rightarrow\mathsf{m}(x,D(x,v,w)\;|\;P)\;|\;\mathsf{m}(w,D(x,v,w)\;|\;P)\;|\;{*}(w)\\\
&\rightarrow\mathsf{m}(x,D(x,v,w)\;|\;P)\;|\;D(x,v,w)\;|\;P\\\
&=\;\mathsf{*}_{(x,v,w)}P\;|\;P\end{array}$

Of course, this encoding, as an implementation, runs away, unfolding
$\mathsf{*}P$ eagerly. It is possible to obtain a lazier replication operator
restricted to the embedding of input-guarded $\pi$ processes. The reader
familiar with the $\lambda$-calculus will have noticed the similarity between
$D$ and the “paradoxical” or “fixed point” combinator $Y$.

####  2.2.2 Implementing new names with reflection

Here we provide an encoding of Yoshida’s combinator calculus into the RHO
combinator calculus. Since all names are global in the RHO combinator
calculus, we encounter a small complication in the treatment of free names at
the outset. There are several ways to handle this. One is to insist that the
translation be handed a closed program, one in which all names are bound
either by input or by restriction, but this feels inelegant. Another is to
provide an environment, $r:\mathcal{N}_{\mbox{\tiny
Yoshida}}\rightarrow\mathsf{@}\mathsf{Proc}$, for mapping the free names in a
Yoshida process into names in the RHO combinator calculus. Maintaining the
updates to the environment, however, obscures the simplicity of the
translation. We adopt a third alternative.

To hammer home the point that Yoshida’s combinator calculus is parameterized
in a theory of names, we instantiate her calculus with the names of the RHO
combinator calculus. This is no different than instantiating her calculus
using the natural numbers, or the set of URLs as the set of names. Just as
there is no connection between the structure of these kinds of names and the
structure of processes in the $\pi$-calculus, there is no connection between
the processes quoted in the names used by the theory and the processes
generated by the theory, and we exploit this fact.

Let $\mathsf{@}\mathsf{Proc}$ be set of names in the RHO combinator calculus,
$\mathsf{Proc}$ be the set of terms of the RHO combinator calculus, and
$\mathsf{Proc}_{\mbox{\tiny Yoshida}}$ be the set of terms of her combinator
calculus built using $\mathsf{@}\mathsf{Proc}$ _as the names_. The translation
will be given in terms of a function

$[\\![-]\\!]_{2}(-,-):\mathsf{Proc}_{\mbox{\tiny
Yoshida}}\times\mathsf{<EMAIL_ADDRESS>
The guiding intuition is that we construct alongside the process a distributed
memory allocator, the process’ access to which is mediated through the second
argument to the function, called $p$ below. The first argument, called $n$
below, determines the shape of the memory for the given allocator.

Since Yoshida’s calculus is parametric in a set of names, we can choose
$\mathsf{@}\mathsf{Proc}$ for that set. Given a process $P$ in Yoshida’s
calculus, we pick names $n$ and $p$ in the RHO calculus such that $n\neq p$
and both are distinct from the free names of $P$. Then we define

$[\\![P]\\!]=[\\![P]\\!]_{2}(n,p),$

Name allocation will make heavy use of the following two name constructors

$\displaystyle x^{l}$ $\displaystyle:=$
$\displaystyle\mathsf{@}\mathsf{b}_{\mathsf{l}}(x,\mathsf{m}(x,*x))$
$\displaystyle x^{r}$ $\displaystyle:=$
$\displaystyle\mathsf{@}\mathsf{b}_{\mathsf{r}}(x,\mathsf{m}(x,*x))$

Note that by construction, $\mathsf{@}P$ cannot occur as a name in $P$ and
hence any name derived from a process that is built using $\mathsf{@}P$ cannot
occur in $P$. Thus, the effect of the superscripts $l$ and $r$ on a name $x$
is to construct a name that is guaranteed to be fresh with respect to the free
names of the process being interpreted. More generally, mentioning a name, say
$n$, in the constructor of a another name, say $n^{\prime}$, guarantees
distinction between $n$ and $n^{\prime}$; likewise, mentioning a process, say
$P$, in the constructor of a name $n$ guarantees that $n$ is fresh in $P$. The
particular choices of combinators used in the name constructors are irrelevant
for the purposes of freshness. We make heavy use of this fact in our
interpretation of prefix elimination.

The interpretation function $[\\![-]\\!]_{2}(n,p)$ is straightforward for all
but replication and $\mathsf{new}$.

$\displaystyle[\\![\mathbin{0}]\\!]_{2}(n,p)$ $\displaystyle=$
$\displaystyle[\\![\emph{c}(\stackrel{{\scriptstyle\rightharpoonup}}{{a}})]\\!]_{2}(n,p)$
$\displaystyle=$
$\displaystyle\emph{c}(\stackrel{{\scriptstyle\rightharpoonup}}{{a}})\mbox{,
where $\emph{c}$ is any combinator but $m$}$
$\displaystyle[\\![\mathsf{m}(a,P)]\\!]_{2}(n,p)$ $\displaystyle=$
$\displaystyle\mathsf{m}(a,[\\![P]\\!]_{2}(n,p))$
$\displaystyle[\\![P\mathbin{\texttt{|}}Q]\\!]_{2}(n,p)$ $\displaystyle=$
$\displaystyle[\\![P]\\!]_{2}(n^{l},p^{l})\mathbin{\texttt{|}}[\\![Q]\\!]_{2}(n^{r},p^{r})$

These latter two forms require extra care. We define them in terms of a prefix
form and then use a version of Yoshida’s prefix elimination to remove the
prefix.

$\displaystyle[\\![\mathsf{*}P]\\!]_{2}(n,p)$ $\displaystyle=$
$\displaystyle\mathsf{m}(x,[\\![P]\\!]_{3}(n^{r},p^{r}))|D(x,v,w)|\mathsf{m}(n^{r},*n^{l})|\mathsf{m}(n^{r},*n^{l})$
$\displaystyle\mbox{where
}x=@([\\![P]\\!]_{2}(n,p))^{ll},v=@([\\![P]\\!]_{2}(n,p))^{lr},\mbox{ and
}w=@([\\![P]\\!]_{2}(n,p))^{rr}$
$\displaystyle[\\![(\mathsf{new}\;x)P]\\!]_{2}(n,p)$ $\displaystyle=$
$\displaystyle[\\![\mathsf{for}(x\leftarrow
p?)[\\![P]\\!]_{2}(n^{l},p^{l})|\mathsf{m}(p,*n)]\\!]_{4}(n,p)$

As expected, the interpretation of replication makes use of the $D$ operator
defined above. Note that name allocation is intertwined with prefix and new
elimination.

$\displaystyle[\\![P]\\!]_{3}(n,p)$ $\displaystyle:=$
$\displaystyle[\\![\mathsf{for}(n^{\prime}\leftarrow
n?)\mathsf{for}(p^{\prime}\leftarrow
p?)([\\![P]\\!]_{2}(n^{\prime},p^{\prime})|(D(x)|n!(n^{\prime l})|p!(p^{\prime
l})))]\\!]_{4}.$

To handle prefix elimination we must import most of Yoshida’s algorithm. The
key difference is that we must allocate names that guarantee freshness
relative to the free names of the processes being translated. In those rules
below with a “where” clause, the specific choice of combinators in the names
is not so important as mentioning those names and processes with respect to
which the name mush be fresh. For example, in rule $I$, for prefix to a
parallel composition, we must ensure that $v$ and $w$ are fresh with respect
to the names in $P$ and $Q$, and distinct from each other, and then we must
update both the name allocator for each parallel component and the channels on
which fresh names are communicate (so that there is no interference between
the two components) in the recursive call.

Because the input to $[\\![-]\\!]_{4}$ is already in combinator form, we do
not have to import rules 2 – 4 of her algorithm. Like her, we assume the
following annotations ($+$ stands for the output and $−$ stands for the
input), which denote how each name is used in the rules of interaction:

$\mathsf{m}(a^{+},v^{\pm});\mathsf{d}(a^{−},b^{+},c^{+});\mathsf{k}(a^{−});\mathsf{fw}(a^{−},b^{+});\mathsf{b}_{\mathsf{l}}(a^{−}b^{+});\mathsf{b}_{\mathsf{r}}(a^{−}b^{−});\mathsf{s}(a^{−}b^{−}c^{+})$

As above the annotated polarities are preserved by reduction, e.g.

$\mathsf{d}(a^{−},b^{+},c^{+})|\mathsf{m}(a^{+},v)\to\mathsf{m}(b^{+},v)|\mathsf{m}(b^{+},v)$

Similarly, for economy of expression, we emulate Yoshida’s use of c to
represent any combinator matching the arity specification.

$\begin{array}[]{llrl}(I)&[\\![\mathsf{for}(x\leftarrow
p?)P|Q]\\!]_{4}(n,q)&:=&(\mathsf{d}(p,v,w)|[\\![\mathsf{for}(x\leftarrow
v?)P]\\!]_{4}(n_{1},q_{1})|[\\![\mathsf{for}(x\leftarrow
w?)Q]\\!]_{4}(n_{2},q_{2})\\\ &&&\mbox{where
$v=\mathsf{@}(\mathsf{m}(q,\mathsf{b}_{\mathsf{l}}(q,n)|P|Q))$,
$w=\mathsf{@}(\mathsf{m}(q,\mathsf{b}_{\mathsf{r}}(q,n)|P|Q))$,}\\\
&&&\mbox{$n_{1}=\mathsf{@}(\mathsf{b}_{\mathsf{l}}(v,w)|\mathsf{m}(q,\mathsf{m}(v,*w)))$,
$n_{2}=\mathsf{@}(\mathsf{b}_{\mathsf{r}}(v,w)|\mathsf{m}(q,\mathsf{m}(v,*w)))$}\\\
&&&\mbox{$q_{1}=\mathsf{@}(\mathsf{b}_{\mathsf{l}}(n_{1},n_{2})|\mathsf{m}(q,\mathsf{m}(v,*w)))$,
$q_{2}=\mathsf{@}(\mathsf{b}_{\mathsf{r}}(n_{1},n_{2})|\mathsf{m}(q,\mathsf{m}(v,*w)))$}\\\
(V)&[\\![\mathsf{for}(x\leftarrow
p?)\emph{c}(v^{+},w)]\\!]_{4}(n,q)&:=&\mathsf{s}(p,a,v)|\emph{c}(a^{+},\stackrel{{\scriptstyle\rightharpoonup}}{{w}})\mbox{,
where
$a=@(\mathsf{m}(q,*n)|\emph{c}(v^{+},\stackrel{{\scriptstyle\rightharpoonup}}{{w}}))$
and $x\not\in v:\stackrel{{\scriptstyle\rightharpoonup}}{{w}}$}\\\
(VI)&[\\![\mathsf{for}(x\leftarrow
p?)\emph{c}(v^{-},\stackrel{{\scriptstyle\rightharpoonup}}{{w}})]\\!]_{4}(n,q)&:=&\mathsf{s}(p,v,a)|\emph{c}(a^{-},\stackrel{{\scriptstyle\rightharpoonup}}{{w}})\mbox{,
where $a=@(\mathsf{m}(q,*n)|\emph{c}(v^{-},w))$ and $x\not\in
v:\stackrel{{\scriptstyle\rightharpoonup}}{{w}}$}\\\
(VII)&[\\![\mathsf{for}(x\leftarrow
p?)\mathsf{m}(v,x)]\\!]_{4}(n,q)&:=&\mathsf{fw}(p,v)\\\
(VIII)&[\\![\mathsf{for}(x\leftarrow
p?)\mathsf{fw}(x,v)]\\!]_{4}(n,q)&:=&\mathsf{b}_{\mathsf{l}}(p,v)\\\
(IX)&[\\![\mathsf{for}(x\leftarrow
p?)\mathsf{fw}(v,x)]\\!]_{4}(n,q)&:=&\mathsf{b}_{\mathsf{r}}(p,v)\\\
(X)&[\\![\mathsf{for}(x\leftarrow
p?)\emph{c}(\stackrel{{\scriptstyle\rightharpoonup}}{{v}},x^{+},\stackrel{{\scriptstyle\rightharpoonup}}{{w}})]\\!]_{4}(n,q)&:=&[\\![\mathsf{for}(x\leftarrow
p?)\mathsf{fw}(a,x)|\emph{c}(\stackrel{{\scriptstyle\rightharpoonup}}{{v}},a^{+},\stackrel{{\scriptstyle\rightharpoonup}}{{w}})]\\!]_{4}(n^{\prime},q)\\\
&&&\mbox{where
$a=@(\mathsf{m}(q,*n)|\emph{c}(\stackrel{{\scriptstyle\rightharpoonup}}{{v}},x^{+},\stackrel{{\scriptstyle\rightharpoonup}}{{w}}))$}\mbox{
and $n^{\prime}=\mathsf{@}(\mathsf{m}(a,\mathsf{m}(q,*n)))$}\\\
(XI)&[\\![\mathsf{for}(x\leftarrow
p?)\emph{c}(x^{-},\stackrel{{\scriptstyle\rightharpoonup}}{{v}})]\\!]_{4}(n,q)&:=&[\\![\mathsf{for}(x\leftarrow
p?)\mathsf{fw}(x,a)|\emph{c}(a^{-},\stackrel{{\scriptstyle\rightharpoonup}}{{v}})]\\!]_{4}(n^{\prime},q)\\\
&&&\mbox{where $a=@(\mathsf{m}(q,*n)|\emph{c}(x^{-},v))$}\mbox{ and
$n^{\prime}=\mathsf{@}(\mathsf{m}(a,\mathsf{m}(q,*n)))$}\\\
(XII)&[\\![\mathsf{for}(x\leftarrow
p?)\mathsf{b}_{\mathsf{r}}(v,x^{-})]\\!]_{4}(n,q)&:=&[\\![\mathsf{for}(x\leftarrow
p?)(\mathsf{d}(v,w_{1},w_{2})|\mathsf{s}(w_{1},x,w_{3})|\mathsf{b}_{\mathsf{r}}(w_{2},w_{3}))]\\!]_{4}(n^{\prime},q)\\\
&&&\mbox{where
$w_{1}=\mathsf{@}(\mathsf{b}_{\mathsf{l}}(q,n)|\mathsf{m}(q,\mathsf{b}_{\mathsf{r}}(v,x^{-})))$,
$w_{2}=\mathsf{@}(\mathsf{b}_{\mathsf{r}}(q,n)|\mathsf{m}(q,\mathsf{b}_{\mathsf{r}}(v,x^{-})))$,}\\\
&&&\mbox{$w_{3}=\mathsf{@}(\mathsf{b}_{\mathsf{l}}(p,v)|\mathsf{m}(w_{1},*w_{2})$,
and $n^{\prime}=\mathsf{@}(\mathsf{s}(w_{1},w_{2},w_{3}))$}\\\
(XIII)&[\\![\mathsf{for}(x\leftarrow
p?)\mathsf{s}(v,x^{-},w)]\\!]_{4}(n,q)&:=&[\\![\mathsf{for}(x\leftarrow
p?)(\mathsf{s}(v,w_{1},w_{2})|\mathsf{m}(w_{1},*x)|\mathsf{b}_{\mathsf{l}}(w_{2},w))]\\!]_{4}(n^{\prime},q)\\\
&&&\mbox{where $w_{1}=@(\mathsf{b}_{\mathsf{l}}(q,n)|\mathsf{s}(v,x^{-},w))$,
$w_{2}=@(\mathsf{b}_{\mathsf{r}}(q,n)|\mathsf{s}(v,x^{-},w))$,}\\\
&&&\mbox{and $n^{\prime}=\mathsf{@}(\mathsf{m}(w_{1},*w_{2}))$}\end{array}$

Note that all $\mathsf{new}$-binding is now interpreted, as in Wischik’s
global $\pi$-calculus, as an input [9].

It is also noteworthy that the translation is dependent on how the parallel
compositions in a process are associated. Different associations will result
in different bindings for $\mathsf{new}$ names. This will not result in
different behavior, however: while the RHO combinators can encode different
behaviors depending on the choice of name, Yoshida’s combinators cannot and
the embedding is insensitive to the choice.

####  2.2.3 Faithfulness of the translation

###### Definition 5

An _observation relation_ , $\downarrow_{\mathcal{N}}$, over a set of names,
$\mathcal{N}$, is the smallest relation satisfying the rules below.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}y\in{\mathcal{N}},\;x\mathbin{\equiv_{N}}y\end{array}}{\begin{array}[]{@{}c@{}}\mathsf{m}(x-)\downarrow_{\mathcal{N}}x\end{array}}$
(Out-barb)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mbox{$P\downarrow_{\mathcal{N}}x$
or
$Q\downarrow_{\mathcal{N}}x$}\end{array}}{\begin{array}[]{@{}c@{}}P|Q\downarrow_{\mathcal{N}}x\end{array}}$
(Par-barb)

We write $P\Downarrow_{\mathcal{N}}x$ if there is $Q$ such that $P\Rightarrow
Q$ and $Q\downarrow_{\mathcal{N}}x$.

This definition is parametric in the the argument accepted in the second
position in the message combinator, $\mathsf{m}(x-)$, i.e. the payload of the
message: in the RHO combinators the payload is a process, while in Yoshida’s
the payload is a name. Likewise, because the definition of barbed bisimulation
given below is dependent on the definition of the observation relation, the
definition is really a template for the notion of bisimulation that must be
instantiated to the kind of payload accepted by the message combinator.

###### Definition 6

An ${\mathcal{N}}$-_barbed bisimulation_ over a set of names, ${\mathcal{N}}$,
is a symmetric binary relation ${\mathcal{S}}_{\mathcal{N}}$ between agents
such that $P\;{\mathcal{S}}\;_{\mathcal{N}}Q$ implies:

  1. 1.

If $P\rightarrow P^{\prime}$ then $Q\Rightarrow Q^{\prime}$ and
$P^{\prime}\;{\mathcal{S}}\;_{\mathcal{N}}Q^{\prime}$.

  2. 2.

If $P\downarrow_{\mathcal{N}}x$, then $Q\Downarrow_{\mathcal{N}}x$.

$P$ is ${\mathcal{N}}$-barbed bisimilar to $Q$, written
$P\stackrel{{\scriptstyle\centerdot}}{{\approx}}_{\mathcal{N}}Q$, if
$P\;{\mathcal{S}}\;_{\mathcal{N}}Q$ for some ${\mathcal{N}}$-barbed
bisimulation ${\mathcal{S}}_{\mathcal{N}}$.

###### Theorem 2.1

$P\stackrel{{\scriptstyle\centerdot}}{{\approx}}_{\pi}Q\iff[\\![P]\\!]\stackrel{{\scriptstyle\centerdot}}{{\approx}}_{\texttt{FN}(P)}[\\![Q]\\!]$.

######  Proof (Proof sketch)

The forward direction $\Rightarrow$ is immediate from the definition of the
translation. The reverse direction is only interesting in the case of $!$ and
$\mathsf{new}$. The replication case follows immediately from the calculation
following definition 4. In the $\mathsf{new}$ case, transitions on
$\mathsf{new}$-bound names will be in one-to-one correspondence with names
provided by the name parameters of the translation function. By construction,
these are not observable by the observation relation.

###### Remark 1

In light of this theorem, it is worth pointing out that this version of the
RHO combinators has no rule for _introducing_ terms of the form $\mathsf{*}x$.
The $b_{r}$ and $b_{l}$ combinators introduce new names from processes, but
the do not introduce new reflection terms. Yet, this calculus suffices to
faithfully represent the Yoshida combinators. This is because the translation
function is carefully introducing just those terms, via the $D(x,v,w)$
operator, guided by the use of replication in the source to the translation.

##  3 Conclusion and future work

We have shown how to construct a concurrent higher-order combinator calculus
that uses reflection to avoid the necessity for new and bound names. Yoshida’s
combinators, and therefore the asynchronous $\pi$-calculus, have a faithful
embedding into the calculus. While the results are interesting in their own
right we developed them to serve a larger purpose. In a forthcoming paper we
demonstrate an algorithm taking a graph-enriched Lawvere theory (representing
a formal specification of a term calculus) and a more vanilla Lawvere theory
(representing a specification of a notion of collection, such as set, or bag,
or list, etc) and produce a type system for the term calculus enjoying
soundness and completeness. Nominal phenomena do not neatly fit inside the
expressive power of graph-enriched Lawvere theories, thus potentially limiting
the scope of the applicability of this algorithm. However, with the reflective
techniques we can extend this algorithm to cover many languages and term
calculi with binding.

At a more foundational level it turns out that the reflective techniques can
be applied to set theory itself deriving a form of FM set theory in which the
“atoms” of one set theory are the sets of another copy of set theory. Roughly
speaking, we may imagine that there are “red” sets and “black” sets. The “term
constructors” of red set theory (the curly braces of set notation) can use
either red sets or black sets, which the element-of predicate ($\in$) red set
theory can only inspect red sets and treats black sets as “atomic”. The
symmetric situation holds for black set theory: the element-of predicate
cannot see inside red sets. This framework all the building blocks necessary
to realize a version of FM set theory from a more traditional set theory with
reflection and provides a bridge between Gabbay and Pitts’ account of nominal
phenomena and the reflection-based approach.

## References

  * [1] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic, _Mechanized metatheory for the masses: The poplmark challenge_ , pp. 50–65, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005.
  * [2] Ranald Clouston, _Nominal lawvere theories: A category theoretic account of equational theories with names_ , J. Comput. Syst. Sci. 80 (2014), no. 6, 1067–1086.
  * [3] Murdoch Gabbay and Andrew M. Pitts, _A new approach to abstract syntax with variable binding_ , Formal Asp. Comput. 13 (2002), no. 3-5, 341–363.
  * [4] Microsoft Corporation, _Microsoft biztalk server_ , microsoft.com/biztalk/default.asp.
  * [5] L. Gregory Meredith and Matthias Radestock, _A reflective higher-order calculus._ , Electr. Notes Theor. Comput. Sci. 141 (2005), no. 5, 49–67.
  * [6] Robin Milner, _The polyadic $\pi$-calculus: A tutorial_, Logic and Algebra of Specification Springer-Verlag (1993).
  * [7] David Sangiorgi and David Walker, _The $\pi$-calculus: A theory of mobile processes_, Cambridge University Press, 2001.
  * [8] Moses Schönfinkel, _On the Building Blocks of Mathematical Logic_ , From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (Jean van Heijenoort, ed.), iuniverse.com, 1924, pp. 355–366.
  * [9] Lucian Wischik, _Old names for nu_ , Submitted for publication, 2004.
  * [10] Nobuko Yoshida, _Minimality and separation results on asynchronous mobile processes - representability theorems by concurrent combinators_ , Theor. Comput. Sci. 274 (2002), no. 1-2, 231–276.

##  4 Appendix: Translating the $\pi$-calculus into the $\rho$-calculus

###  4.1 $\rho$-calculus

It is striking to compare the $\rho$-calculus with the $\pi$-calculus as the
former is a vastly simpler theory and yet has enjoys more features.
Specifically, the specification of the $\rho$-calculus’s structural
equivalence and reduction rules are notably simpler, with one small technical
caveat: name equivalence depends on structural equivalence which depends upon
$\alpha$-equivalence which depends on name equivalence. Meredith and Radestock
show that this cycle terminates innocently due to the design of the grammar.
This technical complexity seems a small price to pay for a much simpler
calculus that enjoys both higher order communication as well reflection and
meta-programming features.

process
$\displaystyle\displaystyle{P,Q\mathbin{\mathbf{::=}}\mathbin{0}\;\mathbin{\mathbf{\mid}}\;\mathsf{for}(y\leftarrow
x)P\;\mathbin{\mathbf{\mid}}\;x!(Q)\;\mathbin{\mathbf{\mid}}\;\mathsf{*}x\;\mathbin{\mathbf{\mid}}\;P|Q}$
name $\displaystyle\displaystyle{x,y\mathbin{\mathbf{::=}}\mathsf{@}P}$

###### Definition 7

_Free and bound names_ The calculation of the free names of a process, $P$,
denoted $\mathbin{\mathsf{FN}(P)}$ is given recursively by

$\displaystyle\mathbin{\mathsf{FN}(\mathbin{0})}=\emptyset\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(\mathsf{for}(y\leftarrow
x)(P))}=\\{x\\}\cup\mathbin{\mathsf{FN}(P)}\setminus\\{y\\}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(x!(P))}=\\{x\\}\cup\mathbin{\mathsf{FN}(P)}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(P|Q)}=\mathbin{\mathsf{FN}(P)}\cup\mathbin{\mathsf{FN}(Q)}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathbin{\mathsf{FN}(\mathsf{}{x})}=\\{x\\}\penalty-10000\hskip
20.00003pt plus 0.5fil minus 5.0pt$

An occurrence of $x$ in a process $P$ is bound if it is not free. The set of
names occurring in a process (bound or free) is denoted by
$\mathbin{\mathcal{N}(P)}$.

###### Definition 8

The structural congruence $\equiv$ between processes [7] is the least
congruence containing alpha-equivalence and satisfying the commutative monoid
laws (associativity, commutativity and as identity) for parallel composition
$|$.

###### Definition 9

The name equivalence $\mathbin{\equiv_{N}}$ is the least congruence satisfying
these equations

Quote-drop
$\displaystyle\displaystyle{\mathsf{@}\mathsf{*}x\mathbin{\equiv_{N}}x}$
Struct-equiv $\displaystyle\displaystyle{\hbox{\hskip
11.7462pt\vbox{\hbox{\hskip-11.74619pt\hbox{\hbox{$\displaystyle\displaystyle{P\mathbin{\equiv}Q}$}}}\vbox{}}}\over\hbox{\hskip
22.079pt\vbox{\vbox{}\hbox{\hskip-22.07898pt\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{@}P\mathbin{\equiv_{N}}\mathsf{@}Q}$}}}}}}$

###  4.2 Operational semantics

COMM $\displaystyle\displaystyle{\hbox{\hskip
20.82362pt\vbox{\hbox{\hskip-20.82361pt\hbox{\hbox{$\displaystyle\displaystyle{x_{trgt}\mathbin{\equiv_{N}}x_{src}}$}}}\vbox{}}}\over\hbox{\hskip
80.78632pt\vbox{\vbox{}\hbox{\hskip-80.78632pt\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{for}(y\leftarrow
x_{trgt})P|x_{src}!(Q)\rightarrow P\\{\mathsf{@}Q/y\\}}$}}}}}}$ PAR
$\displaystyle\displaystyle{\hbox{\hskip
13.85675pt\vbox{\hbox{\hskip-13.85675pt\hbox{\hbox{$\displaystyle\displaystyle{P\rightarrow
P^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
27.87334pt\vbox{\vbox{}\hbox{\hskip-27.87334pt\hbox{\hbox{$\displaystyle\displaystyle{P|Q\rightarrow
P^{\prime}|Q}$}}}}}}$ EQUIV $\displaystyle\displaystyle{\hbox{\hskip
58.31856pt\vbox{\hbox{\hskip-58.31856pt\hbox{\hbox{$\displaystyle\displaystyle{{P\mathbin{\equiv}P^{\prime}}\quad\quad{P^{\prime}\rightarrow
Q^{\prime}}\quad\quad{Q^{\prime}\mathbin{\equiv}Q}}$}}}\vbox{}}}\over\hbox{\hskip
13.13501pt\vbox{\vbox{}\hbox{\hskip-13.13501pt\hbox{\hbox{$\displaystyle\displaystyle{P\rightarrow
Q}$}}}}}}$

###  4.3 $\pi$-calculus

In this presentation of the $\pi$-calculus we update the syntax for input-
guarded processes to reflect the widespread adoption of comprehension notation
in languages ranging from Scala to Python for use in reactive programming.
Here we go with the Scala notation writing $\mathsf{for}(y\leftarrow x)P$
where Milner might have written $x?(y)P$. Admittedly, it’s somewhat more
verbose, but conveys to a younger generation of programmers more familiar with
reactive programming the intended semantics of the expression. Similarly,
since we keep the output expression $x!(y)$ we avoid collision with the
traditional notation for reflection ($!P$) by writing $\mathsf{*}P$ instead,
which is at least somewhat reminiscent of the Kleene star and the familiar
from regular expressions.

process
$\displaystyle\displaystyle{P,Q\mathbin{\mathbf{::=}}\mathbin{0}\;\mathbin{\mathbf{\mid}}\;\mathsf{for}(y\leftarrow
x)P\;\mathbin{\mathbf{\mid}}\;x!(y)\;\mathbin{\mathbf{\mid}}\;(\mathsf{new}\;x)P\;\mathbin{\mathbf{\mid}}\;P|Q\;\mathbin{\mathbf{\mid}}\;\mathsf{*}P}$

Note that there is no production for $x$’s and $y$’s in the grammar. This
reflects the fact that the $\pi$-calculus is _parametric_ in the collection
channel names. That collection merely has to be countably infinite and have an
effective equality. As such it is perfectly reasonable to choose a collection
names, namely the names of the $\rho$-calculus. We can make this choice
without loss of generality because we can always choose some other countably
infinite set with an effective equality, say $\mathcal{N}$ and then require an
invertible map, $\mathsf{code}:\mathcal{N}\to@\mathsf{Proc}$.

###  4.4 Structural congruence

###### Definition 10

The structural congruence, $\equiv$, between processes is the least congruence
closed with respect to alpha-renaming, satisfying the abelian monoid laws for
parallel (associativity, commutativity and as identity), and the following
axioms:

  1. 1.

the scope laws:

$\displaystyle(\mathsf{new}\;x)\mathbin{0}$ $\displaystyle\equiv$ ,
$\displaystyle(\mathsf{new}\;x)(\mathsf{new}\;x)P$ $\displaystyle\equiv$
$\displaystyle(\mathsf{new}\;x)P,$
$\displaystyle(\mathsf{new}\;x)(\mathsf{new}\;y)P$ $\displaystyle\equiv$
$\displaystyle(\mathsf{new}\;y)(\mathsf{new}\;x)P,$ $\displaystyle
P|(\mathsf{new}\;x)Q$ $\displaystyle\equiv$
$\displaystyle(\mathsf{new}\;x)P|Q,\;\mbox{{if}
}x\not\in\mathbin{\mathsf{FN}(P)}$

  2. 2.

the recursion law:

$\displaystyle\mathsf{*}P\equiv P|\mathsf{*}P$

  3. 3.

the name equivalence law:

$\displaystyle P\equiv P\\{x/y\\},\;\mbox{{if} }x\mathbin{\equiv_{N}}y$

###  4.5 Operational semantics

COMM $\displaystyle\displaystyle{\mathsf{for}(y\leftarrow x)P|x!(v)\rightarrow
P\\{v/y\\}}$ PAR $\displaystyle\displaystyle{\hbox{\hskip
13.85675pt\vbox{\hbox{\hskip-13.85675pt\hbox{\hbox{$\displaystyle\displaystyle{P\rightarrow
P^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
27.87334pt\vbox{\vbox{}\hbox{\hskip-27.87334pt\hbox{\hbox{$\displaystyle\displaystyle{P|Q\rightarrow
P^{\prime}|Q}$}}}}}}$ NEW $\displaystyle\displaystyle{\hbox{\hskip
13.85675pt\vbox{\hbox{\hskip-13.85675pt\hbox{\hbox{$\displaystyle\displaystyle{P\rightarrow
P^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
47.34978pt\vbox{\vbox{}\hbox{\hskip-47.34978pt\hbox{\hbox{$\displaystyle\displaystyle{(\mathsf{new}\;x)P\rightarrow(\mathsf{new}\;x)P^{\prime}}$}}}}}}$
EQUIV $\displaystyle\displaystyle{\hbox{\hskip
58.31856pt\vbox{\hbox{\hskip-58.31856pt\hbox{\hbox{$\displaystyle\displaystyle{{P\mathbin{\equiv}P^{\prime}}\quad\quad{P^{\prime}\rightarrow
Q^{\prime}}\quad\quad{Q^{\prime}\mathbin{\equiv}Q}}$}}}\vbox{}}}\over\hbox{\hskip
13.13501pt\vbox{\vbox{}\hbox{\hskip-13.13501pt\hbox{\hbox{$\displaystyle\displaystyle{P\rightarrow
Q}$}}}}}}$

Here we stick with tradition and write $\Rightarrow$ for $\rightarrow^{*}$,
and rely on context to distinguish when $\rightarrow$ means reduction in the
$\pi$-calculus and when it means reduction in the $\rho$-calculus. The set of
$\pi$-calculus processes will be denoted by $\mathsf{Proc}_{\pi}$.

###  4.6 The translation

The translation will be given by a function,
$[\\![-]\\!](-,-):\mathsf{Proc}_{\pi}\times\mathsf{@}\mathsf{Proc}\times\mathsf{@}\mathsf{Proc}\rightarrow\mathsf{Proc}$.
The guiding intuition is that we construct alongside the process a distributed
memory allocator, the process’ access to which is mediated through the second
argument to the function. The first argument determines the shape of the
memory for the given allocator.

Given a process, $P$, we pick $n$ and $p$ such that $n\neq p$ and distinct
from the free names of $P$. For example,
$n=\mathsf{@}\Pi_{m\in\mathbin{\mathsf{FN}(P)}}m!(\mathsf{@}\mathbin{0})$ and
$p=\mathsf{@}\Pi_{m\in\mathbin{\mathsf{FN}(P)}}\mathsf{for}({\mathsf{@}\mathbin{0}}\leftarrow{m}){\mathbin{0}}$.
Then

$[\\![P]\\!]=[\\![P]\\!]_{2nd}(n,p)$

where

$\displaystyle[\\![\mathbin{0}]\\!]_{2nd}(n,p)$ $\displaystyle=$
$\displaystyle[\\![x!(@Q)]\\!]_{2nd}(n,p)$ $\displaystyle=$ $\displaystyle
x!(Q)$ $\displaystyle[\\![\mathsf{for}(y\leftarrow x)P]\\!]_{2nd}(n,p)$
$\displaystyle=$ $\displaystyle\mathsf{for}(y\leftarrow
x)[\\![P]\\!]_{2nd}(n,p)$ $\displaystyle[\\![P|Q]\\!]_{2nd}(n,p)$
$\displaystyle=$
$\displaystyle[\\![P]\\!]_{2nd}(n^{l},p^{l})|[\\![Q]\\!]_{2nd}(n^{r},p^{r})$
$\displaystyle[\\![\mathsf{*}P]\\!]_{2nd}(n,p)$ $\displaystyle=$
$\displaystyle
x!([\\![P]\\!]_{3rd}(n^{r},p^{r}))|D(x)|n^{r}!n^{l}|p^{r}!p^{l}$
$\displaystyle[\\![(\mathsf{new}\;x)P]\\!]_{2nd}(n,p)$ $\displaystyle=$
$\displaystyle\mathsf{for}(x\leftarrow p)[\\![P]\\!]_{2nd}(n^{l},p^{l})|p!(n)$

and

$\displaystyle x^{l}$ $\displaystyle\triangleq$ $\displaystyle\mathsf{@}x!(x)$
$\displaystyle x^{r}$ $\displaystyle\triangleq$
$\displaystyle\mathsf{@}\mathsf{for}(x\leftarrow x?)\mathbin{0}$
$\displaystyle[\\![P]\\!]_{3rd}(n^{\prime\prime},p^{\prime\prime})$
$\displaystyle\triangleq$ $\displaystyle\mathsf{for}(n\leftarrow
n^{\prime\prime}?)\mathsf{for}(p\leftarrow
p^{\prime\prime}?)([\\![P]\\!]_{2nd}(n,p)|(D(x)|n^{\prime\prime}!(n^{l})|p^{\prime\prime}!(p^{l})))$

###### Remark 2

Note that all $\mathsf{new}$-binding is now interpreted, as in Wischik’s
global $\pi$-calculus, as an input guard [9].

###### Remark 3

It is also noteworthy that the translation is dependent on how the parallel
compositions in a process are associated. Different associations will result
in different bindings for $\mathsf{new}$-ed names. This will not result in
different behavior, however, as the bindings will be consistent throughout the
translation of the process.

######  Theorem 4.1 (Correctness)

$P\stackrel{{\scriptstyle\centerdot}}{{\approx}}_{\pi}Q\iff[\\![P]\\!]\stackrel{{\scriptstyle\centerdot}}{{\approx}}_{r(\texttt{FN}(P))}[\\![Q]\\!]$.

_Proof sketch_ : An easy structural induction.

One key point in the proof is that there are contexts in the $\rho$-calculus
that will distinguish the translations. But, these are contexts that can see
the fresh names, $n$, and the communication channel, $p$, for the ‘memory
allocator’. These contexts do not correspond to any observation that can be
made in the $\pi$-calculus and so we exclude them in the $\rho$-calculus side
of our translation by our choice of ${\mathsf{N}}$ for the bisimulation. This
is one of the technical motivations behind our introduction of a less standard
bisimulation.

###### Example 1

In a similar vein consider, for an appropriately chosen $p$ and $n$ we have

$[\\![(\mathsf{new}\;v)(\mathsf{new}\;v)u!(v)]\\!]=\mathsf{for}(v\leftarrow
p)(\mathsf{for}({v}\leftarrow{\mathsf{@}p!(p)})(u!(v)|\mathsf{@}p!(p))!(\mathsf{@}n!(n)))|p!(n)$

and

$[\\![(\mathsf{new}\;v)u!(v)]\\!]=\mathsf{for}(v\leftarrow p)(u!(v))|p!(n)$

Both programs will ultimately result in an output of a single fresh name on
the channel $u$. But, the former program will consume more resources. Two
names will be allocated; two memory requests will be fulfilled. The
$\rho$-calculus can see this, while the $\pi$-calculus cannot. In particular,
the $\pi$-calculus requires that
$(\mathsf{new}\;x)(\mathsf{new}\;x)P\equiv(\mathsf{new}x)P$.

Implementations of the $\pi$-calculus, however, having the property that
$(\mathsf{new}\;x)P$ involves the allocation of memory for the structure
representing the channel $x$ come to grips with the implications this
requirement has regarding memory management. If memory is allocated upon
encountering the $\mathsf{new}$-scope, there are situations where the left-
hand side of the equation above will fail while the right-hand will succeed.
Remaining faithful to the equation above requires that such implementations
are lazy in their interpretation of $(\mathsf{new}\;x)P$, only allocating the
memory for the fresh channel at the first moment when that channel is used.

Having a detailed account of the structure of names elucidates this issue at
the theoretical level and may make way to offer guidance to implementations.