A Strong Normalisation Condition for Pure Type Systems
Abstract
A proof theoretical analysis suggests that the process of
cut elimination in a sequent calculus corresponds to the normalisation of the
proofs in natural deduction. If one moves to proofs decorated with lambda terms
according to the Curry-Howard’s
isomorphism, the same observation leads to realising that the process of normalisation
of the lambda-terms decorating the proofs in natural deduction is deeply connected
with the property of closure under substitution of the lambda terms decorating
the proofs in a sequent calculus. In this paper we show that this observation
becomes a criterion to recognise the strongly normalising Pure Type Systems.
Full text