Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!turpin
From: turpin@cs.utexas.edu (Russell Turpin)
Newsgroups: comp.theory
Subject: Re: Lambda Calculus with Pointers: Tomorrow's Challenge.
Summary: Tomorrow?  I plan to defend this semester!
	 But I did it in logic rather than lambda calculus.
Message-ID: <12689@cs.utexas.edu>
Date: 20 Sep 90 03:34:22 GMT
References: <6413@uwm.edu> <6414@uwm.edu> <26256@cs.yale.edu> <6436@uwm.edu>
Organization: U. Texas CS Dept., Austin, Texas
Lines: 27

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