F-semantics for type assignment systems

Abstract

Yokouchi, H., F-semantics for type assignment systems, Theoretical Computer Science 129 (1994) 39-77. This paper develops F-semantics for type systems that assign types to untyped λ-terms. Curry's system is complete for F-semantics, but a polymorphic type assignment system is not so. We introduce two additional rules (FI) and (FE), and show that a polymorphic type assignment system becomes complete for F-semantics if we add these two rules. Furthermore, we apply the same method to a polymorphic type assignment system without the β-equality rule and obtain a similar completeness result. We also show that an intersection type assignment system is complete for F-models if we add two rules defined on the basis of (FI) and (FE). © 1994.