The recent thread on functional idioms for comparing finite arrays got
me thinking about the infinite case. To keep it simple, consider
comparing two infinite lists (in Haskell):

(cycle [3,4]) == (cycle [3,4])

Although the result should be true, the expression above never
terminates.  Is there any way at all to do such a test without resorting
to non-functional features (eg. pointer-equality)?

Thanks,

--
Louis.

--

 \__/
  ^^                      SYGNATURA ZASTPCZA
QRCZAK

Cheers,

Nick.

--

Nick Williams
Software Engineer
Praxis Critical Systems Limited, Bath, UK

-kzm
--
If I haven't seen further, it is by standing in the footprints of giants

--

 \__/
  ^^                      SYGNATURA ZASTPCZA
QRCZAK

Nick.

--

Nick Williams
Software Engineer
Praxis Critical Systems Limited, Bath, UK

Actually it's undecidable if you allow arbitrary functions on at least
one of the sides of the equality operator, because then the equality
operator could be used to solve the halting problem.

Proof sketch:
Assume this scenario,
  (cycle [0]) == number_of_steps (lazy a)
where 'number_of_steps' is the number of steps that 'a' needs to
evaluate, encoded with as many zeroes as there are evaluation steps and
a final 1.
The result of the expression will be False if 'a' can be evaluated in a
finite number of steps, True otherwise.

Of course, it might be possible to built a lot of heuristics into == to
solve the majority of questions. But even with nonrecursive function you
can get into {*filter*} exponential behaviour. For example, you could use
this equality to write down a function to test for equivalence of
boolean terms; that's a "hard" problem: there's no known algorithm that
does better than O(exp(number of free variables)). In fact finding such
an algorithm would be a major breakthrough (it would also immediately
give a non-exponential algorithm for all "hard" problems, such as the
Travelling Salesman or Breaking RSA).

Regards,
Joachim
--
This is not an official statement from my employer or from NICE.

same_items xs ys =
 let xs' = ... get items from xs up to the list back edge
     ys' = ... ditto for ys
     in
   xs' == ys'

To determine where the back edge is, compare the original list (via
pointer equality) with every remaining list as items are popped of.  I'm
not saying this is the most elegant way to do it, just one example of a
non-pure solution. [It does assume the list is circular ofcourse].

--
Louis.

    cycle [1,2,3]          -- cycle of (:) pointers of length 3
    map id (cycle [1,2,3]) -- no cycle, only elements are shared

Moreover, pointer equality speculations are true for a straightforward
implementation, but are not mandated by the language and actually
compilers may do it in different ways. For example in GHC two values
may be not pointer-equal until garbage collection, where they suddenly
become pointer-equal.

--

 \__/
  ^^                      SYGNATURA ZASTPCZA
QRCZAK

--
Louis.

  if x == y then e1
  else e2

you have to compare the *values* of x and y, which means, you have to
*evaluate* them. The operational semantics does not tell you anything about
handling semantically equivalent terms.

Your transformation would transform

  if bottom == bottom then unreachable1
  else unreachable2

into "unreachable1" - which is clearly against the operational semantics.
The program must not terminate.

Currently, the "if"-statement allows you to evaluate terms in a strict way
by writing, e.g.

  if x == x then e1
  else unreachable

This wouldn't be possible with your trick anymore. (Actually, the
if-statement has a funny dual in strict languages: there they introduce
laziness, because only one alternative will be evaluated).

Note, btw., that in strict languages you *can* get rid of the if-statement
and (if the language is pure) of the inefficiency of evaluating the term
twice without changing the semantics, whereas you can't in lazy ones
(unless you introduce a primitive "strict"-function as in Haskell). E.g.:

  if maybe_bottom () = maybe_bottom () then maybe_reachable
  else unreachable

-->

  let _ = maybe_bottom () in maybe_reachable

Of course, in strict languages it is always safe to eliminate the choice
induced by if-statements if the condition is known to be a value and if the
"mathematical equivalence" is known.

Best regards,
Markus Mottl

--

    Thus, if one were willing to interlace the data of the list
with something like "period markers", then "==" would be easily
implementable for 'rational' infinite lists. (Though, handed
two copies of the *same* 'transcendent' (i.e. non-'rational')
infinite list, the algorithm would loop, of course.)

    To have "==" restricted to the class of 'rational' infinite
lists need not be completely worthless either. Rational lists
are closed under quite a few interesting transformations
and combinations. And if you push a rational infinite list
through a finite transducer, the infinite output list is,
again, rational (establishing the proper period marks
for the tail of the output sequence may require a bit of
fancy footwork, though).

Christian Stapfer

Regards,
Joachim
--
This is not an official statement from my employer or from NICE.

Some of these languages, e.g. BinProlog, also provide some support for
functional syntax.  I don't know if any of these support lazy
evaluation, though.  One language that might support functional
syntax, lazy evaluation, and rational term unification is Curry,
a combined logic/functional language.

--

WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"

--
Louis.