The Completeness Theorem for Typing lambda-Terms
The Completeness Theorem for Typing lambda-Terms
复制标题
输入 lambda 项的完备性定理
DOI：
10.1016/0304-3975(83)90136-6
复制
发表时间：
1983
影响因子：
1.1
通讯作者：
R. Hindley
中科院分区：
文献类型：
--
作者：
R. Hindley
给出了无类型λ-项的类型模式赋给规则，描述了三种不同的语义，并证明了这些规则关于其中两种语义是完备的.类型模式是由类型变量，而不是常量，通过"“建立的。在无类型λ演算的任意模型中定义了语义;这样的模型并没有将类型结构作为其定义的一部分。两种不同的语义完全被一组规则捕获的事实表明，通常的类型语言，以“→”作为其唯一的连接词，不足以表达它们之间的差异。我猜想规则也是完整的关于第三种语义。
Rules for assigning type-schemes to untyped λ-terms are given, three different semantics are described, and the rules are proved complete with respect to two of these semantics. The type-schemes are built up from type-variables, not constants, by ‘→’. The semantics are defined in arbitrary models of the untyped λ-calculus; such models do not come with a type- structures as part of their definition.The fact that two distinct semantics are completely captured by one set of rules says that the usual type-language, with ‘→’ as its only connective, is not expressive enough to describe the differences between them.I conjecture that the rules are also complete with respect to the third semantics.