The completeness theorem for typing λ-terms

AbstractRules 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