Equality of functional values
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20070130 (15:25) 
From:  Jeff Polakow <jeff.polakow@d...> 
Subject:  Re: [Camllist] Equality of functional values 
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 ProofCarrying 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 email may contain confidential and/or privileged information. If you are not the intended recipient (or have received this email in error) please notify the sender immediately and destroy this email. Any unauthorized copying, disclosure or distribution of the material in this email is strictly forbidden.