Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!yale!quasi-eli!cs.yale.edu!newsbase!choo
From: choo@cs.yale.edu (young-il choo)
Newsgroups: comp.theory
Subject: Re: Lambda Calculus with Pointers: Tomorrow's Challenge.
Message-ID: <26256@cs.yale.edu>
Date: 19 Sep 90 21:32:02 GMT
References: <6413@uwm.edu> <6414@uwm.edu>
Sender: news@cs.yale.edu
Organization: Computer Science Yale University New Haven CT 06520-2158
Lines: 47
Nntp-Posting-Host: aqua.systemsx.cs.yale.edu
In-reply-to: markh@csd4.csd.uwm.edu's message of 19 Sep 90 03:52:15 GMT

In article <6414@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes:
>    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

> 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.

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. 

> [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.

Having higher-order functions and lexical scoping is sufficient to model
quotation and unquotation (or reference and dereference).

--  Young-il Choo

    Yale University  Computer Science  New Haven  CT 06520-2158
    choo@cs.yale.edu  (203) 432-4099