关于简单类型的函数机算：范畴语义与强规范化
摘要：函数机器演算（FMC）是最近引入的一种λ演算的泛化形式，它包括高阶全局状态，概率和非确定性选择，以及输入和输出，同时保留了可汇聚性。该演算可以编码这些影响的名值调用语义。这是通过两个独立的泛化实现的，从FMC的操作语义的角度来看都是自然的，它由一个简单的多堆栈机器给出。 第一个泛化将λ演算的语法分解为允许项的顺序组合和编码规约策略的方式。具体而言，存在着保持操作语义的名值调用语义和值调用语义的λ演算的翻译。第二个泛化根据“位置”（对应于机器的多个堆栈）对应用和抽象进行参数化，从而将给定效果的操作语义、语法和规约规则与λ演算的相应组件统一起来。FMC还配备了一个简单的类型系统，用于限制和捕捉效果的行为。 此论文提出了两个主要贡献，证明λ演算的两个基本特性被FMC保留。第一个贡献是表明FMC的范畴语义，在适当的等式理论下，可以通过自由笛卡尔闭范畴给出。等式理论通过观察等价性的概念进行验证。第二个贡献是证明有类型的FMC项是强规约的。这是对Gandy关于λ演算的证明的扩展（和简化），还强调了其潜在的操作直觉。
作者：Chris Barrett
论文ID：2305.16073
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-26