Call-by-name Milner encoding

The call-by-name Milner encoding is a translation of the pure untyped \lambda-calculus into the pure untyped \pi-calculus.

The encoding

Please expand

Soundness

The encoding is sound for the \lambda\beta theory.

Induced theory

The encoding itself induces an equational theory between \lambda-terms, where two \lambda-terms M, N are considered equal when their translations \llbracket M \rrbracket and \llbracket N \rrbracket are behaviourally equivalent.

The theory induced in this manner by the CBN encoding has been shown to be the Lévy-Longo tree (LT) equality Sangiorgi 1993, 2000. Remarkably, the result is robust under various notions of behavioural equivalence Sanrgiorgi and Xu 2018.

References

Sangiorgi, Davide. 1994. ‘An Investigation into Functions as Processes’. In Mathematical Foundations of Programming Semantics, edited by Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, 802:143–59. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-58027-1_7.

@inproceedings{sangiorgi_1994,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {An investigation into functions as processes},
	volume = {802},
	doi = {10.1007/3-540-58027-1_7},
	booktitle = {Mathematical {Foundations} of {Programming} {Semantics}},
	publisher = {Springer Berlin Heidelberg},
	author = {Sangiorgi, Davide},
	editor = {Brookes, Stephen and Main, Michael and Melton, Austin and Mislove, Michael and Schmidt, David},
	year = {1994},
	pages = {143--159},
}

Sangiorgi, Davide, and Xian Xu. 2018. ‘Trees from Functions as Processes’. Logical Methods in Computer Science 14 (3). https://doi.org/10.23638/LMCS-14(3:11)2018.

@article{sangiorgi_2018,
	title = {Trees from {Functions} as {Processes}},
	volume = {14},
	doi = {10.23638/LMCS-14(3:11)2018},
	number = {3},
	journal = {Logical Methods in Computer Science},
	author = {Sangiorgi, Davide and Xu, Xian},
	year = {2018}
}