[plt-scheme] a few questions (was: Scheme questions?)

From: Hendrik Boom (hendrik at pooq.com)
Date: Sun Dec 4 22:06:17 EST 2005

On Sun, Dec 04, 2005 at 08:51:35PM -0500, Matthias Felleisen wrote:
> 
> On Dec 4, 2005, at 8:19 PM, Gregory Woodhouse wrote:
> 
> >
> >On Dec 4, 2005, at 5:08 PM, Matthias Felleisen wrote:
> >
> >>
> >>>I don't know if the Y combinator had been devised when McCarthy was
> >>>trying to computerize recursion theory,
> >>
> >>1930s.
> >
> >Are you sure?
> 
> Yes.
> 
> >I know lambda calculus was developed in the 1930's, but didn't Dana 
> >Scott develop domain theory (where you get fixed points for continuous 
> >functions) in the 1970's.
> 
> The Y combinator is a syntactic idea, not a semantic one. Yes, it took 
> people some 35 years to develop the semantics of the LC but that 
> doesn't prevent anybody from doing and using Y, the S/K stuff, and many 
> more purely syntactic things.

Actually, the lambda calculus, from early on, had a so-called syntactic
model where the "value" of a lambda expression was the equivalence class
of expressions that were reduction-equicalent to it.

However,  the idea of functions that could take functions as arguments
ad infinitum seems as reasonable a starting point for mathematics as
the conventional set theories where sets can contain sets as elements
ad infinitum.  Its just that if you try to interpret labda calculus
into the set L of functions from L into L, as a set in the set theory,
you run into an awful lot of trouble with the cardinality of sets.

The trouble, as I see it, is not with labmda calculus not having
a model, but with set theory being excessively rich in a way incompatible
with the richness of lambda-calculus.

What Dana Scott did was formulate a topological space D so that instead
of having lambda calculus be interpreted as the set L of all functions
L to L, instead you get D beind isomorphic to the set of continuous
functions from D to D.  I'm told he did this becaise the evident
consistency of lambda calculus and its apparent inconsistency with
regulat set theory made his bain hurt. 

-- hendrik


Posted on the users mailing list.