This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Equality of functional values
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-01-30 (15:25) From: Jeff Polakow Subject: Re: [Caml-list] 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 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.
```