The minimal continuous semantics of the lambda-calculus

Preview

PDF WRAP_Thesis_Welch_1974.pdf - Requires a PDF viewer. Download (18MB) | Preview

Request Changes to record.

Abstract

A semantics of the ƛ-calculus is presented which is different from any of the lattice models, so far analysed, of Scott and the term models of Morris and Barendregt. The original motivation was to do for ƛ-expressions what Scott had done for flow-diagrams, namely construct a 'syntactic' inverse limit lattice, E∞ in which to represent them. .A further motivation was to abstract out the essential notion J("continuous semantics") behind the theorem that Wadsworth proved concerning some of Scott's models, namely that meaning of a ƛ-expression can be found as the (continuous) limit its approximate reductions. That this idea is relevant to E∞ can be seen since the coordinates , of the image of a ƛ-expression in E∞ .form a subset of its approximate reductions.

To establish the basic fact of ß-modelship about E∞ be shown that Wadsworth's theorem does indeed apply - i.e. that the , it has to 3 E∞-coordinates provide a sufficiently complete subset of all the possible approximate reductions. Translating this back to the ƛ-calculus gives an algorithm ("i'th reductions") for producing ß-reductions which must be proven 'correct' - i.e. that it goes sufficiently far in all cases, : this notion is christened "weak completeness". l'th reductions are generalised to a non-deterministic evaluation mechanism called "inside-out reductions" which behaves in almost the opposite manner to Church's "standard reductions". This generalisation is not too drastic since it is easy to show that a weak completeness result for one implies the same for the other. The weak completeness of inside-out reductions is established.

The E∞-semantics is a 'pure' a-model in that the only n-reductions modelled are when there are equivalent ß-reductions - other-wise they are not even comparable. Further, ƛ-expressions with a normal form are maximal and isolated in E∞, unsolvable expressions are i,the fixed-point combinators {Yi|i > O} are equivalenced and the model itself is substitutive, normal, solvable and implies Morris' "extensional equivalence". Finally, it is the minimal continuous semantics in the sense that Wadsworth's theorem is true in another semantics if and only if it is continuously derivable from E∞

Request changes or add full text files to a record

Repository staff actions (login required)

View Item