Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uwm.edu!csd4.csd.uwm.edu!markh
From: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Newsgroups: comp.theory
Subject: Re: Lambda Calculus with Pointers: Tomorrow's Challenge.
Message-ID: <6436@uwm.edu>
Date: 19 Sep 90 23:54:49 GMT
References: <6413@uwm.edu> <6414@uwm.edu> <26256@cs.yale.edu>
Sender: news@uwm.edu
Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Organization: University of Wisconsin-Milwaukee
Lines: 36

On the challenge of embedding pointers directly into the pure Lambda Calculus:

In article <26256@cs.yale.edu> choo@cs.yale.edu (young-il choo) writes:
>
>Let * = lambda x.xy
>    & = lambda x.lambda y.x
>
>Fact:  For all terms M, M = *(&M).
>
>The intuition is that & encodes an object x by making it into a function
>lambda y.x, and * decodes it by giving the object x some random object y as
>argument. 

It comes close, but won't let you slip in an X under the lambda X, like the
sequence I posted:

>    Then you could do the following beta-reduction sequence:
...
>       *( lambda Y. &((lambda X. X + *Y) 2)   &X )
>    -> *(       &((lambda X. X + *&X) 2)  )
>    -> *(       &((lambda X. X + X) 2 )               )
>    -> *(       &(2 + 2) )                            ^
>    -> *(       &4 )                                  |
>    -> 4                                              |
                                             Missing bracket added

That feature of 'aliasing' is a crucial aspect of one's intuition of pointers.

There's two levels of beta-reduction going on here: one's operating on an
expression (the third reduction step above), and the other is operating on the
syntax of an expression inside the &() (in the very first reduction step
above).

That means that the substitution rule for this kind of reduction is not going
to be trivial to formulate, and that is what makes the prospect of embedding
this extended Lambda Calculus into the pure Lambda Calculus a challenge.