Miser Project Readings
Notes on Lambda Calculus and Combinatory Logic
|
|
Miser Project Readings |
These are notes based on consideration of Barendregt, Hendrik Pieter. The Lambda Calculus: Its Syntax and Semantics. North-Holland (Amsterdam, 1981). ISBN 0-444-85490-8.
Over the intervening time, I have recreated these considerations several times in various forms. My intention is to consolidate them in line with my later thinking and leave this page simply for reference and a form of check-list.
-- Dennis E. Hamilton
Seattle, Washington
2014-05-01
2000-07-18 (orcmid): This was the only serious lambda-calculus book that I kept in preparing to move to Italy in September, 1999. So I am mining it here for combinatory logic (CL).
I will demonstrate that programs for the Miser Engine represent combinatory logic, so combinatory algebra is useable for discussion of an exploration of computational completeness. The CL is equivalent to the closed-form lambda calculus (no free variables) which is equivalent to the set of recursive functions which is equivalent to what is computable. What's cool about Miser is it provides a pretty direct access to CL without presuming CL as primitive. That is, CL is represented, and this raises some interesting things about that and about representing mathematical structures by computer, generally.
My concern is as follows. If the Miser Engine evaluation mechanism provides a valid interpretation of CL, then all of the results of CL apply and can be used to simplify formulae, etc., to reduce and find equivalences, etc. Likewise, the lambda calculus can also be used, since by having CL as a model, the Miser Engine also has the computable part of the lambda calculus as a model. So all theorems and results about CL and the computable lambda calculus are results about the Miser Engine.
If I find that there are exceptions, I need to figure out how to repair the interpretation or else I may have to build a derivative of CL that accounts for them. I would much rather find that the interpretation is sound and valid. So I need to do some theory work to satisfy myself about that.
My readings have involved mining in here enough to put sticky notes on pages where there is relevant material.
The idea is not that people should have to master this stuff. I need to master enough of it so that I can rely on the results of this theoretical work in an informal development that is still supported by the heavier theory. I want to just appeal to it, discuss it informally, and point people to the main bodies of work.
Something I have to work out is the problem of undefined (or non-reducible forms) that come up. These are equivalent to programs that don't terminate. It is fine to have them, of course -- you can't have a universal computer without termination problems -- but I need to make sure that the representation of CL squares with the theory of CL in this area. In particular, I am going to be very rigorous around not allowing program simplifications that will eliminate undefined parts. (This is like avoiding the classic mistakes that come up if you simplify formulae involving divisions and neglect the problem of there being a potentially-0-valued denominator in the original form that was inadvertently simplified out.)
 |
You are navigating Orcmid on GitHub |
created 2000-08-09-07:48 -0700 (pdt) by orcmid |
