| Summary: | 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 application 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.
|
|---|
