A Finitary Subsystem of the Polymorphic lambda-Calculus.
Thorsten Altenkirch, Thierry Coquand · 2001
We give a finitary normalisation proof for the restriction of system F where we quantify only over first-order type. As an application, the functions representable in this fragment are exactly the ones provably total in Peano Arithmetic. This is inspired by the reduction of 1 1 -comprehension to inductive definitions presented in [Buch2] and this complements a result of [Leiv]. The argument uses a finitary model of a fragment of the system AF2 considered in [Kriv, Leiv].