[racket] Lambda, object identity & streams

On Thu, Apr 17, 2014 at 12:46:08PM -0400, Bradley Lucier wrote:
> > In the process of toying with streams & memoization (more below), I've 
> > tripped over the question: when does Racket consider two lambdas to be 
> > identical?
> 
> I came across the same question when working with my constructive 
> reals package.  (A constructive real number is basically a function 
> that returns a stream of integers of various kinds, depending on the 
> representation.)
> 
> For example, could I tell that "one" "plus" "one" equals (returns the same stream of integers) "two" "times" "one" (where all the quoted terms are in the constructive reals).

This is an inherent issue with the constructive reals.  In fact, this 
touches the very essence of constructivity.

> 
> Using Gambit, I couldn't figure out how.

There is no general algorithm to tell whether two constructive reals 
are equal.  (Or real numbers for that matter; there isn't even a way 
of *writing* all the classical real numbers so you can compute with 
them).

It's an unsolvable problem in general.

Classically, the trichotomy law is:

for some x, y, either x < y or x = y or x > y.

Constructively, what we have is

for any x and y, there is an epsilon > 0 such that
              x < y + epsilon or x > y - epsilon

Classically, there are two truth values, and every proposition is 
either true or false.

Constructively, there are still only two truth values, but all we
can say is soe propositions are true, some are false, and some we just 
don't know.  "Just don't know" isn't a truth value, just an admission 
of ignorance.  But constructively, we can't assert that p or q without 
being able to find out which it is, so that's as far as we go.

I've placed a rudimentary explanation ot this on my web page; see
http://topoi.pooq.com/hendrik/howconstr.html and 
http://topoi.pooq.com/hendrik/constructivism.html.
 
> 
> But there was a way to see that "one" "plus" "one" equals (another instance of) "one" "plus" "one", and that was to serialize both lambdas computing the two constructive reals and then to compare the serialized values.  The serialized lambdas "remembered" how they were composed from simpler lambdas, so if two of them were constructed using the same sequence of operations, then the serialized representations could tell that they were the same, while they were stored as two different closures in memory.  I still couldn't tell that "one" "plus" "two" equals "two" "plus" "one".

Only for some specific presentations of the numbers "one" and "two".
Which is one of the conceptual reasone why computers usually use 
floating point or rational arithmetic instead of the fully general 
constructive reals.  Of course there are performance reasons as well.

-- hendrik

> 
> I didn't go much further with the question of how different representations of lambdas might facilitate checking "equality" of more general terms.

It won't solve the general problem; it can solve some substs of the 
problem.

-- hendrik

> 
> Brad
> 

> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users