zbMATH — the first resource for mathematics

Un algorithme non typable dans le système F. (An algorithm not typable in the system F). (French) Zbl 0665.03008
A term of \(\lambda\)-calculus which computes the relation \(m\leq n\) is shown to be not typable in the second order typed lambda calculus, introduced by J. Y. Girard, if m and n are declared to be of type integer, i.e. \[ \forall X((X\to X)\to (X\to X)). \] An extension of the system F is proposed to type the above mentioned term.
Reviewer: A.Pettorossi

03B40 Combinatory logic and lambda calculus
03B15 Higher-order logic; type theory (MSC2010)
68Q65 Abstract data types; algebraic specification