paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Extensional and Non-extensional Functions as Processes

扩展与非扩展的函数作为进程
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 1/10 · 该论文属于纯进程演算与λ演算形式语义研究,讨论Milner编码、扩展性与Böhm树等经典理论问题,与用户关注的LLM/Agent静态分析、AI辅助形式化验证、浮点程序分析或贝叶斯程序分析均无直接交叉。引用 3 inbox
Ken Sakayori, Davide Sangiorgi
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:通过参数化 wires 细化 Milner 编码,统一刻画扩展与非扩展的函数作为进程 λ-理论。

本文研究函数作为进程表示时如何获得扩展 λ-理论,以及如何在扩展与非扩展表示间转换。Milner 对纯 λ-演算的编码最多只给出非扩展 λ-理论(β 成立而 η 不成立)。作者在 Internal π(Iπ,所有输出均受绑定的 π-演算子集)中细化该编码,引入参数化组件 wires,并证明当 wires 满足若干代数性质时编码产生 λ-理论。利用 Iπ 的对称性与对偶性,作者划分出三类 wires:两类顺序且互为对偶,另一类并行且自对偶。关键结果是,并行 wires 产生扩展 λ-理论,其等式与带无限 η 的 Böhm trees 相同;另外两类产生非扩展 λ-理论,分别对应 Lévy-Longo trees 与 Böhm trees。

问题
在 π-演算中,函数作为进程的编码通常只能得到非扩展 λ-理论;本文追问能否以及如何获得扩展的 λ-理论,并统一理解扩展与非扩展表示之间的关系。
方法
在 Internal π 中细化 Milner 编码,引入参数化于 wires 的表示;要求 wires 满足若干代数性质,并利用 Iπ 的对称性/对偶性将 wires 分类为三类。
评估
通过数学证明与 λ-理论等式刻画进行评估:证明并行 wires 诱导扩展 λ-理论并与带无限 η 的 Böhm trees 一致,顺序两类分别对应 Lévy-Longo trees 和 Böhm trees。
原文摘要(Abstract)

Following Milner’s seminal paper, the representation of functions as processes has received considerable attention. For pure λ-calculus, the process representations yield (at best) non-extensional λ-theories (i.e., β rule holds, whereas η does not).In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal π, Iπ (a subset of the π-calculus in which all outputs are bound), we develop a refinement of Milner’s original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a λ-theory. Exploiting the symmetries and dualities of Iπ, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional λ-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite η. In contrast, the other two classes of wires yield non-extensional λ-theories whose equalities are those of the Lévy-Longo and Böhm trees.

链接与引用

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

BibTeX
@inproceedings{SakayoriS23,
  title = {Extensional and Non-extensional Functions as Processes},
  author = {Ken Sakayori and Davide Sangiorgi},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175686}
}