Re: [Caml-list] Equality of functional values

[Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>]

skaller wrote:
> 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.

There are two major reasons why equality of functions might not be 
computable in a specific situation:

1) Sufficiently general functions are allowed so that various 
diagonalization theorems kick in and we get a proof that equality is not 
decidable.

2) The functions are "simple", but they are represented in such a way 
that they cannot be tested for equality.

The first reason is more "theoretical" (but still underappreciated by 
"real" programmers), while the second shows up in practice.

Since there are several possible notions of equality, I should specify 
which one I mean. Let us take a very fine-grained one, namely 
observational equality: expressons e1 and e2 are observationally equal, 
if for every program context C[-] of ground type, C[e1] equals C[e2]. 
"Ground type" is usually taken to be int, or some other non-trivial type 
for which equality is not a problematic concept. Observational equality 
is of interest because an expression e1 may always be substituted for an 
observationally equal e2. (Think of e1 being more efficient than e2.)

Now, to explain how 2) appears, consider observational equality of 
values of type unit->unit in ocaml. Also, to keep thing manageable, let 
us ignore exceptions, store, timing, and other computational effects. Up 
to observational equality there are only two values of type unit->unit, 
namely

  fun _ -> ()

and

  let rec f x = f x in (f : unit -> unit)

If we decide to represent these two values in some form other than 
unit->unit, e.g.

   type fake_unit = Identity | TheDivergingFunction

then equality is decidable. But as far as the type unit->unit is 
concerned, there is no equality test

   eq : (unit->unit) -> (unit->unit) -> bool

(Can you prove it? When you do, you will see that the reason for it is 
that we have allowed sufficiently general functions, i.e., reason 2) 
above is really reason 1) in disguise.) Even if eq gets the source code, 
it still cannot decide equality.

So I hope that clears up some points about equality of functions, 
especially:

> Of course for an arbitrary function, equality isn't decidable,
> but programmers don't write arbitrary functions (except in
> error).

To summarize what I wrote above: it may be a matter of how functions are 
represented, not _which_ functions we are trying to compare.

> 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.

No, my suggestion amounts to this: very likely Simon is representing a 
data structure by embedding it into a function space in such a way that 
he loses valuable information, which could help him decide equality.

> BTW: Felix is one of the few general languages around that
> actually allows a statement of semantics:
> 
> typeclass SemiGroup[t with Eq[t]] {
>   virtual fun add: t * t -> t;
>   axiom assoc(x:t, y:t, z:t): add(x, add(y,z)) == add(add(x,y),z);
> }
> 
> These axioms are checkable:
> 
> instance SemiGroup[int] {
>   fun add:int * int -> int = "$1+$2";
> }
> 
> axiom_check(1,2,3);

You are confusing checking of particular instances and checking the 
general statement in which x, y and z, are universally quantified.

Checking of particular instances may still be valuable to a programmer, 
though, as it is a form of run-time correctness checking.

> however there's currently no way to state and prove
> theorems. It would be interesting if someone had some
> idea how to use one of the existing theorem provers
> to act as a proof assistant (verify user given proof,
> filling in enough 'gaps' in the formal steps to make
> it practical).

I would go further: it would be interesting to augment real programming 
languages with ways of writing specifications that can then be tackled 
by theorem provers and proof asistants. In the long run this might 
educate programmers about the value of correct programs. Naturally, as 
long as only Mars space probes and the occasional airplane crash because 
of software errors, there won't be sufficient economic incentive to 
wrote correct software.

Jacques Carette said he would be happy with an intensional notion of 
equality of functions. Surely Jacques, you would want some guarantees 
about such an equality to make it useful, otherwise one could just define

   let reallySillyIntensionalEquality f g = false

So are you suggesting something other than ocaml's == ? What guarantees 
would you expect?

Speaking of ==, here is a question that has been bugging me: if e1 == 
e2, are e1 and e2 observationally equal (ignoring store, exceptions, etc.)?

Andrej