一句话:给出λ演算到π演算编码相对于Levy-Longo树和Böhm树可靠完备的一般条件,并应用于call-by-name编码。
本文研究λ演算的Levy-Longo树与Böhm树能否通过λ演算到π演算的编码来刻画。作者提出一组一般条件,保证编码相对于这些树结构是可靠且完备的,即编码后的进程行为等价关系能准确对应源项所对应的树。随后将这些条件应用于call-by-name λ演算的多种编码,展示如何通过选择π演算中的行为等价以及调整编码方式,分别得到Levy-Longo树和Böhm树。该工作为λ演算与π演算之间的语义对应提供了统一框架。
Levy-Longo Trees and Bohm Trees are the best known tree structures on the {\lambda}-calculus. We give general conditions under which an encoding of the {\lambda}-calculus into the {\pi}-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name {\lambda}-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the {\pi}-calculus and/or the encoding.