Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
复制标题
多元多态代数理论：句法、语义、翻译和方程逻辑
DOI：
10.1109/lics.2013.59
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
M. Fiore and M. Hamana
中科院分区：
文献类型：
--
作者：
Shin-ya Katsumata;Tetsuya Sato;伊関 友伸;Shin-ya Katsumata;M. Fiore and M. Hamana
我们形式化并研究了多态代数理论的概念，正如数学术语所理解的那样，多态代数理论是由具有类型和项变量绑定的多态类型项之间的方程提出的理论。多态代数理论的典型例子是系统F，但我们的框架应用更广泛。额外的普遍性源于一个数学分析，它导致了一个统一的多态代数理论，具有以下成分：；指定任意多态算子的多态签名（例如在扩展的λ-微积分和代数效应中）；;元变量，包括类型和术语，能够对元理论进行一般性描述；;多类型宇宙允许在不同类型宇宙的参数化理论之间进行转换；;提供代数模型一般概念的多态结构（包括系统F的PL-category语义）；;一种多态方程逻辑，它构成了方程推理的健全和完整的逻辑框架。我们的工作是语义驱动的，基于具有变量绑定的抽象语法的分层两级代数建模。
We formalise and study the notion of polymorphic algebraic theory, as understood in the mathematical vernacular as a theory presented by equations between polymorphically-typed terms with both type and term variable binding. The prototypical example of a polymorphic algebraic theory is System F, but our framework applies more widely. The extra generality stems from a mathematical analysis that has led to a unified theory of polymorphic algebraic theories with the following ingredients: ; polymorphic signatures that specify arbitrary polymorphic operators (e.g. as in extended λ-calculi and algebraic effects); ; metavariables, both for types and terms, that enable the generic description of meta-theories; ; multiple type universes that allow a notion of translation between theories that is parametric over different type universes; ; polymorphic structures that provide a general notion of algebraic model (including the PL-category semantics of System F); ; a Polymorphic Equational Logic that constitutes a sound and complete logical framework for equational reasoning. Our work is semantically driven, being based on a hierarchical two-levelled algebraic modelling of abstract syntax with variable binding.