In many cases, equality of functions has been decided by humans,
as has
termination of programs. Of course this doesn't prove that humans
can, in
principle, decide equality for any pair of functions. But neither
has the
opposite been proved.
It hasn't been proved that we can't build a device that can decide
equality for arbitrary functions, either.
I'm sure it can be proved that any mathematical problem can be
reduced to equality of two functions, so our ability to decide it
contradicts Goedel theorem.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe