Path: utzoo!attcan!uunet!wuarchive!uwm.edu!csd4.csd.uwm.edu!markh
From: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Newsgroups: comp.theory
Subject: Lambda Calculus with Pointers: Tomorrow's Challenge.
Message-ID: <6414@uwm.edu>
Date: 19 Sep 90 03:52:15 GMT
References: <6413@uwm.edu>
Sender: news@uwm.edu
Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Organization: University of Wisconsin-Milwaukee
Lines: 48


   What if the Lambda Calculus had pointers?  WHat would it look like?  Well,
you're going to answer that question, with a considerable head-start from me,
if you accept this challenge...

   If the Lambda Calculus had pointers, the 'addressing' operator ('&') would
be very similar to LISP's 'QUOTE' operator, and the 'dereferencing' operator
('*') would be like LISP's 'EVAL' operator.  Of course.

   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

to simulate the effect of the programming language sequence:

                  Y = &X; X = 2; return X + *Y;

(which, of course, returns 4).

   The addressing operator would not really be an operator.  In reality,
&X would be a syntatically disguised short-hand for a list expression.
For instance;

	&(lambda X.X)   <==>   [  [lambda, X], X ]

The "*" operator would be an operator defined on lists that generates
results consistent with the equality:

			    X = *&X.

This is your challenge:

[1] Prove that the lambda calculus with pointers is equivalent to the
    lambda calculue without pointers (but with an equality predicate
    for basic symbols) by coming up with an appropriate lambda definition
    of the dereferencing-operator, and an appropriate definition for
    the &X pseudo-expression.

[2] Use this result to show how pointers may be embedded in PURELY
    functional programming languages in such a way that the semantics
    of the '&' makes no reference at all to machine addresses.

A solution may be posted in the future, time permitting its development :)k