Show simple item record

dc.contributor.authorEspírito Santo, José Carlos Soaresen
dc.date.accessioned2018-01-31T11:43:16Z
dc.date.available2018-01-31T11:43:16Z
dc.date.issued2002en
dc.identifier.urihttp://hdl.handle.net/1842/27984
dc.description.abstractThis 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 θ, to proofs in the canonical fragment, of terms from certain conservative extensions of the λ-calculus. This assignment, in a sense, is an optimal improvement over the traditional assignment φ, in that it is an isomorphism both in the sense of sound bijection of proofs and isomorphism of normalisation procedures.en
dc.description.abstractFirst, 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.en
dc.description.abstractThis study suggests the definition of conservative extensions of natural deduc­tion (and λ-calculus) based on the idea of a built-in distinction between applica­tive 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 θ . Conceptual rearrangements in proof- theory deriving from these extensions of natural deduction are discussed.en
dc.description.abstractFinally, we argue that, computationally, both the canonical fragment and natural deduction (in the extended sense introduced here) correspond to extensions of the λ-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.en
dc.publisherThe University of Edinburghen
dc.relation.ispartofAnnexe Thesis Digitisation Project 2017 Block 16en
dc.relation.isreferencedbyAlready catalogueden
dc.titleConservative extensions of the λ-calculus for the computational interpretation of sequent calculusen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record