×

zbMATH — the first resource for mathematics

Partially typed terms between Church-style and Curry-style. (English) Zbl 0998.03009
van Leeuwen, Jan (ed.) et al., Theoretical computer science. Exploring new frontiers of theoretical informatics. International conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1872, 505-520 (2000).
Summary: We introduce several structures between Church-style and Curry-style based on partially typed terms formalism. In the uniform framework, we study the static properties of the \(\lambda\)-terms between the two styles. It is proved that type checking, typability, and type inference for domain-free \(\lambda 2\) are in general undecidable. A simple instance of the second-order unification problem is reduced to the problem of type inference for domain-free \(\lambda 2\). The typability problem is undecidable even for a predicative fragment of domain-free \(\lambda 2\), called the rank 2 fragment. It is also found that making polymorphic domains free and the use of type-holes are independently responsible for the undecidability of the partial polymorphic type reconstruction problem.
For the entire collection see [Zbl 0944.00071].

MSC:
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
Software:
Automath
PDF BibTeX XML Cite