论文标题
简单类型理论的代数模型：多项式方法
Algebraic models of simple type theories: a polynomial approach
论文作者
论文摘要
我们开发了简单类型理论的代数模型，制定了一个框架，该框架扩展了通用代数以结合代数分类和可变结合。简单类型理论的示例包括Unity和简单的$λ$ -Calculi，计算$λ$ -Calculus和谓词逻辑。 简单类型的理论是在预局部类别中给出的模型，其结构由多项式内膜的代数指定，与自然扣除规则相对应。我们构建的初始模型抽象地描述了简单类型理论的语法。考虑到替代结构，我们进一步提供了结构化的笛卡尔多兼而言之的声音和完整的语义。这一发展将兰贝克（Lambek）简单类型的$λ$ calculus和cartesian关闭的类别（任意简单类型的理论）之间的对应关系进行了概括。
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.
