Algebraic models of simple type theories: A polynomial approach
Algebraic models of simple type theories: A polynomial approach
复制标题
简单类型理论的代数模型：多项式方法
DOI：
10.1145/3373718.3394771
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
M. Fiore
中科院分区：
文献类型：
--
作者：
Nathanael Arkor;M. Fiore
我们开发了简单类型理论的代数模型，构建了一个扩展通用代数以纳入代数排序和变量绑定的框架。简单类型理论的例子包括统一和简单类型的 λ 演算、计算 λ 演算和谓词逻辑。简单类型理论给出了 presheaf 类别中的模型，其结构由对应于自然演绎规则的多项式内函子的代数指定。我们构建的初始模型抽象地描述了简单类型理论的语法。考虑到替换结构，我们进一步在结构化笛卡尔多类别中提供合理且完整的语义。这一发展将 Lambek 在简单类型 λ 演算和笛卡尔闭范畴之间的对应关系推广到任意简单类型理论。
We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include the unityped and simply-typed λ-calculi, the computational λ-calculus, and predicate logic. Simple type theories are given models in presheaf categories, with structure specified by algebras of polynomial endofunctors that correspond to natural deduction rules. Initial models, which we construct, abstractly describe the syntax of simple type theories. Taking substitution structure into consideration, we further provide sound and complete semantics in structured cartesian multicategories. This development generalises Lambek's correspondence between the simply-typed λ-calculus and cartesian-closed categories, to arbitrary simple type theories.
通过评估类型化 lambda 演算进行标准化的语义分析
影响因子：
0.5
作者：
Fiore M
通讯作者：
Fiore M