paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Trees from Functions as Processes

作为进程的函数所生成的树
LMCS vol.Volume 14, Issue 32018匹配度 1/10 · 该论文属于纯 λ 演算与 π 演算编码的形式语义理论研究,关注 Levy-Longo 树/Böhm 树,与静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关联。仅在广义 PL 理论上相关,但与用户当前具体研究方向差距很大。引用 3 inbox
Davide Sangiorgi, Xian Xu
crossref: 2026-09-10

AI 速览

一句话:给出λ演算到π演算编码相对于Levy-Longo树和Böhm树可靠完备的一般条件,并应用于call-by-name编码。

本文研究λ演算的Levy-Longo树与Böhm树能否通过λ演算到π演算的编码来刻画。作者提出一组一般条件,保证编码相对于这些树结构是可靠且完备的,即编码后的进程行为等价关系能准确对应源项所对应的树。随后将这些条件应用于call-by-name λ演算的多种编码,展示如何通过选择π演算中的行为等价以及调整编码方式,分别得到Levy-Longo树和Böhm树。该工作为λ演算与π演算之间的语义对应提供了统一框架。

问题
如何用π演算编码刻画λ演算的Levy-Longo树和Böhm树,并保证编码在树语义上可靠且完备。
方法
提出一般性条件,并通过在π演算中选择不同行为等价和不同编码进行实例化。
评估
理论证明与多个call-by-name λ演算编码的案例分析,说明两类树可从不同等价与编码组合得到。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

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