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