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 (23:06) From: Andrej Bauer Subject: Re: [Caml-list] Equality of functional values
```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;
> }
>
> 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

```