Re: [Caml-list] Equality of functional values

[Jeff Polakow <jeff.polakow@db.com>]

[-- Attachment #1: Type: text/plain, Size: 2295 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 3182 bytes --]