GENERALIZED ALGEBRAIC THEORIES AND CONTEXTUAL CATEGORIES
GENERALIZED ALGEBRAIC THEORIES AND CONTEXTUAL CATEGORIES
复制标题
DOI：
10.1016/0168-0072(86)90053-9
复制
发表时间：
1986-11-01
影响因子：
0.8
通讯作者：
CARTMELL, J
中科院分区：
文献类型：
--
作者：
CARTMELL, J
本文介绍的广义代数理论的概念是从Martin-L6f型理论[11，12]的版本中抽象出来的，是通常的多分类代数或方程理论的概念的推广(例如，如Goguen和Mesguer[6]所描述的)。这些理论在描述能力上等同于Freyd的基本代数理论[5]。人们希望，这一新概念将变得清晰，它是数学实践中特定部分的自然形式化，并且这种形式化没有不必要的编纂。通过引入比通常所考虑的分类结构更一般的分类结构，实现了在方程式理论的先前概念中的这种新概念的额外一般性，因为分类可以表示通常的集合，或者它们可以表示集合族、集合族等。在语法中，通过变量类型(也称为依赖类型)来处理排序结构的一般性，其方式与Martin-L0f的方式非常相似。De Bruijn[2]也有不同类型的概念。可变类型的可能性适合于描述范畴论中出现的那种结构。基本的例子是范畴理论本身，其中Ob看起来是一个类别，被解释为一个集合，而Horn看起来是一个类别，被解释为以Ob x Ob为索引的集合族。表达式Hom(x，y)在该理论的语法中显示为变量类型。在结构上与句法上定义的理论完全对应的代数结构是被称为语境范畴的特殊结构化范畴。之所以这样叫，是因为我们看到，这样一个范畴的对象可以被认为是语境。语境范畴理论被视为通过用正确输入的术语替换变量的操作强加于某些类别的术语和类型表达式的结构的代数描述。
The notion of generalised algebraic theory introduced in this paper has been abstracted from versions of Martin-L6f type theory [11, 12] and is a generalisation of the usual notion of a many-sorted algebraic or equational theory (as described, for example, by Goguen and Meseguer [6]). The theories are equal in descriptive power to the essentially algebraic theories of Freyd [5]. It is hoped that it will become clear that the new notion is a natural formalisation of a definite part of mathematical practice and that this formalisation is free from unnecessary codification. The extra generality of this new notion among previous notions of equational theory is achieved by the introduction of sort structures more general than those usually considered, in that sorts may denote sets as is usual or they may denote families of sets, families of families of sets, or the like. The generality of the sort structures is dealt with in the syntax by variable types (also known as dependent types) in a manner which follows closely to that of Martin-L0f. De Bruijn [2] also has the idea of types which vary. The possibility of variable types suits the theories to the description of the kind of structure that occurs in category theory. The basic example is of the theory of categories itself, in which Ob appears as a sort to be interpreted as a set, whereas Horn appears as a sort to be interpreted as a family of sets indexed by Ob x Ob. The expression Hom (x, y) appears in the syntax of this theory as a variable type. The algebraic structures that structurally correspond exactly to the syntactically defined theories are particularly structured categories to be called contextual categories. These are so called because we see that the objects of such a category can be thought of as contexts. The theory of contextual categories is seen as an algebraic description of the structure imposed on certain classes of term and type expressions by the operation of substitution of correctly typed terms for variables.