## Conservative extensions of the lambda-calculus for the
computational interpretation of sequent calculus

**José Carlos Soares do Espírito Santo**
*Abstract:*

This thesis offers a study of the Curry-Howard
correspondence for a certain fragment (the *canonical*
fragment) of sequent calculus based on an investigation of the
relationship between cut elimination in that fragment and
normalisation. The output of this study may be summarised in a new
assignment Theta, to proofs in the canonical fragment, of terms
from certain conservative extensions of the lambda-calculus. This
assignment, in a sense, is an optimal improvement over the
traditional assignment phi, in that it is an isomorphism both in
the sense of sound bijection of proofs and isomorphism of
normalisation procedures.

First, a systematic definition of calculi of
cut-elimination for the canonical fragment is carried out. We study
various *right* protocols, *i.e.* cut-elimination
procedures which give priority to right permutation. We pay
particular attention to the issue of what parts of the procedure
are to be implicit, that is, performed by meta-operators in the
style of natural deduction. Next, a comprehensive study of the
relationship between normalisation and these calculi of
cut-elimination is done, producing several new insight of
independent interest, particularly concerning a generalisation of
Prawitz's mapping of normal natural deduction proofs into sequent
calculus.

This study suggests the definition of
conservative extensions of natural deduction (and lambda-calculus)
based on the idea of a built-in distinction between *applicative
term* and application, and also between *head* and
*tail* application. These extensions offer perfect
counterparts to the calculi in the canonical fragment, as
established by the mentioned mapping Theta. Conceptual
rearrangements in proof-theory deriving from these extensions of
natural deduction are discussed.

Finally, we argue that, computationally, both
the canonical fragment and natural deduction (in the extended sense
introduced here) correspond to extensions of the lambda-calculus
with applicative terms; and that what distinguishes them is the way
applicative terms are structured. In the canonical fragment, the
head appli cation of an applicative term is ``focused''. This, in
turn, explains the following observation: some reduction rules of
calculi in the canonical fragment may be interpreted as transition
rules for abstract call-by-name machines.

This report is available in the following formats:

Previous |

Index |

Next