markh@csd4.csd.uwm.edu (Mark William Hopkins) (09/19/90)
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 :)kchoo@cs.yale.edu (young-il choo) (09/20/90)
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
markh@csd4.csd.uwm.edu (Mark William Hopkins) (09/20/90)
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.
turpin@cs.utexas.edu (Russell Turpin) (09/20/90)
----- In article <6436@uwm.edu>, markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: > It comes close, but won't let you slip in an X under the lambda X, > like the sequence I posted ... > > That feature of 'aliasing' is a crucial aspect of one's intuition > of pointers. I agree. Without true aliasing that arises from pointers having a common destination, it is impossible to develop an interface to the real data structures that are produced by word processors, paint and draw programs, database systems, hypertext systems, etc. > 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. This problem is very close to my research topic, but it seemed to me that logic rather than the lambda calculus was the better context. (Lambda calculus always gave me the willies.) In a few weeks, you can read how to express pointers in a logic language that has a clean least fixed-point semantics. Essentially, pointers are relativized paths through hierarchical structures. I would think someone who likes reductions, etc, can figure out how to translate this into the context of lambda calculus. Russell