一句话：为按值调用 λ 演算引入置换规则，建立 Böhm 树与程序近似理论，并用 Taylor 展开刻画观测等价。
论文研究按值调用（call-by-value）λ 演算中因规约阻塞而难以刻画程序近似的问题。作者从线性逻辑证明网引入置换规则来扩展该演算，使原本卡住的 redex 可被解锁，并在此框架下定义合适的 Böhm(-like) 树与程序近似理论。主要结果包括：具有相同 Böhm 树的 λ 项观测等价；刻画可作为 λ 项实际 Böhm 树出现的 Böhm-like 树；与 Ehrhard 基于 Taylor 展开的近似理论进行比较，给出资源项集合成为某 λ 项 Taylor 展开的充要条件；并证明 λ 项 Taylor 展开的正规形可由其 Böhm 树的正规化 Taylor 展开计算，从而推出两 λ 项具有相同 Böhm 树当且仅当其 Taylor 展开正规形一致。
The call-by-value lambda calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get stuck during the reduction. We show that such an extension allows to define a satisfying notion of B\"ohm(-like) tree and a theory of program approximation in the call-by-value setting. We prove that all lambda terms having the same B\"ohm tree are observationally equivalent, and characterize those B\"ohm-like trees arising as actual B\"ohm trees of lambda terms. We also compare this approach with Ehrhard's theory of program approximation based on the Taylor expansion of lambda terms, translating each lambda term into a possibly infinite set of so-called resource terms. We provide sufficient and necessary conditions for a set of resource terms in order to be the Taylor expansion of a lambda term. Finally, we show that the normal form of the Taylor expansion of a lambda term can be computed by performing a normalized Taylor expansion of its B\"ohm tree. From this it follows that two lambda terms have the same B\"ohm tree if and only if the normal forms of their Taylor expansions coincide.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1809-02659,
title = {Revisiting Call-by-value B\"ohm trees in light of their Taylor expansion},
author = {Emma Kerinec and Giulio Manzonetto and Michele Pagani},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:6)2020}
}