Show simple item record

dc.contributor.advisorJay, Barry
dc.contributor.advisorSannella, Donald
dc.contributor.advisorKahrs, Stefan
dc.contributor.authorGhani, Neil
dc.date.accessioned2004-03-03T13:59:31Z
dc.date.available2004-03-03T13:59:31Z
dc.date.issued1995-12
dc.identifier.urihttp://hdl.handle.net/1842/404
dc.descriptionhttp://www.youtube.com/watch?v=SJaMtBKnN-I
dc.description.abstractThis thesis is about rewriting in the typed lambda-calculus. Traditional categorical models of typed lambda-calculus use concepts such as functor, adjunction and algebra to model type constructors and their associated introduction and elimination rules, with the natural categorical equations inherent in these structures providing an equational theory for lambda-terms. One then seeks a rewrite relation which, by transforming terms into canonical forms, provides a decision procedure for this equational theory. Unfortunately the rewrite relations which have been proposed, apart from for the most simple of calculi, either generate the full equational theory but contain no decision procedure, or contain a decision procedure but only for a sub-theory of that required. Our proposal is to unify the semantics and reduction theory of the typed lambda-calculus by generalising the notion of model from categorical structures based on term equality to categorical structures based on term reduction. This is accomplished via the addition of a pre-order to each of the hom-sets of the category which will be used to reflect the reduction of one term to another. Canonical rewrite relations, whose associated theory matches that suggested by the traditional semantics, may then be derived from the natural categorical constructions on these ordered categories. Rewrite relations derived in this fashion typically consist of a contractive beta-rewrite rule and an expansionary eta-rewrite rule for each type constructor. Although confluent, the presence of expansionary eta-rewrite rules means the rewrite relation is not strongly normalising and so cannot in itself be used as the basis of a decision procedure. Instead, decidability of the equational theory is proved by a variety of term rewriting techniques which will necessarily vary from calculus to calculus. These techniques are developed in three case studies; the simply typed lambda-calculus with unit, product and exponential types; the linear lambda-calculus containing the tensor from linear logic; and the bicartesian closed calculus obtained by adding coproducts to the simply typed lambda-calculus.en
dc.format.extent462776 bytes
dc.format.extent8017212 bytes
dc.format.extent863958 bytes
dc.format.mimetypeapplication/x-dvi
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleAdjoint Rewritingen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record