The Library
The minimal continuous semantics of the lambdacalculus
Tools
Welch, Peter Hugh (1974) The minimal continuous semantics of the lambdacalculus. PhD thesis, University of Warwick.

PDF
WRAP_Thesis_Welch_1974.pdf  Requires a PDF viewer. Download (17Mb)  Preview 
Official URL: http://webcat.warwick.ac.uk/record=b1747840~S1
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 flowdiagrams, 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 nondeterministic evaluation mechanism called "insideout 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 insideout reductions is established.
The E∞semantics is a 'pure' amodel in that the only nreductions modelled are when there are equivalent ßreductions  otherwise they are not even comparable. Further, ƛexpressions with a normal form are maximal and isolated in E∞, unsolvable expressions are i,the fixedpoint combinators {Yii > 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∞
Item Type:  Thesis (PhD)  

Subjects:  Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software  
Library of Congress Subject Headings (LCSH):  Lambda calculus, Combinatory logic  
Official Date:  December 1974  
Dates: 


Institution:  University of Warwick  
Theses Department:  Department of Computer Science  
Thesis Type:  PhD  
Publication Status:  Unpublished  
Supervisor(s)/Advisor:  Park, David  
Sponsors:  Science Research Council (Great Britain)  
Extent:  330 leaves : illustrations  
Language:  eng 
Request changes or add full text files to a record
Repository staff actions (login required)
View Item 
Downloads
Downloads per month over past year