Hello,
> Actually the idea 'equality of functions is not
computable'
> is misleading .. IMHO. Equality of programmer written
> 'functions' should always be computable: more precisely one hopes
> every function could have a mechanically verifiable proof
> of correctness and wished programming languages provided an
> easy way to prove one.
>
What is usually meant by equality of functions (i.e.
either two functions have the same result for equal arguments, or two functions
have the same normal form) is undecidable in the presence of general recursion.
You are substituting the notion of correctness for
equality. However, correctness is an even harder concept to formalize and
automate than equality. The idea of attaching correctness proofs to programs
is an active area of research. Many of the approaches to it (which I am
aware of) come down to some form of dependent typing. Some relevant projects/systems
include Proof-Carrying Code (http://raw.cs.berkeley.edu/pcc.html), Applied
Type System (http://www.cs.bu.edu/~hwxi/ATS/ATS.html) and the earlier Dependent
ML (http://www.cs.bu.edu/~hwxi/DML/DML.html), and Agda (http://agda.sourceforge.net/)
which is actually a proof assistant but feels a lot like a programming
language.
> Andrej's suggestion amounts to a proof technique: use some
> fixed function (which is equal to itself) plus a comparable
> data structure. This may not be so easy to do though.
>
I think Andrej's suggestion amounts to identifying
the data structure on which you really want to check equality.
We can really only check equality on data, and functions
are not data (at last not without some sort of reflection) but rather instructions
for transforming data. If you really want to know if two variables hold
the same function, you should carry identifiers around with your functions
(of course you might eventually want to optimize away the explicit identifiers
and just use a physical equality test).
-Jeff
---
This e-mail may contain confidential and/or privileged information. If you
are not the intended recipient (or have received this e-mail in error)
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in this
e-mail is strictly forbidden.