通过抽象机将λ演算完全抽象编码于HOcore中
计算机科学中的逻辑
2024-08-07 v5
摘要
我们给出传名（call-by-name）与传值（call-by-value）-演算到HOcore（一种无名称限制的最小高阶进程演算）的完全抽象编码。我们考虑-演算侧的若干等价关系——范式互模拟、应用互模拟与上下文等价——并将其内化为抽象机，以证明编码的完全抽象性。我们还展示该技巧可扩展至-演算，即带有控制算子的-演算标准扩展。
引用
@article{arxiv.2205.06665,
title = {Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines},
author = {Małgorzata Biernacka and Dariusz Biernacki and Sergueï Lenglet and Piotr Polesiuk and Damien Pous and Alan Schmitt},
journal= {arXiv preprint arXiv:2205.06665},
year = {2024}
}