Equivalence of expressions

mann@cs.uni-frankfurt.de mann@cs.uni-frankfurt.de
Fri, 27 Nov 1998 20:19:22 +0100


Has anybody implemented a tool for proving equivalence of expressions
in a lazy functional language?

What kinds of equational theories are reasonable for a non-strict
semantics?

O.k., I know about Abramsky's "lazy lambda calculus", but as far as I
know, it is not a theory for dealing with a functional programming
language or, at least, a core language with algebraic data types.
I think, e.g. for the case that xs is an infinite list

append xs ys = xs

should be provable in such a theory.

Is there any theorem prover capable of doing this?

Regards,

Matthias Mann