Re: [Caml-list] Equality of functional values

[skaller <skaller@users.sourceforge.net>]

On Tue, 2007-01-30 at 14:24 +0100, Andrej Bauer wrote:
> Simon Frost wrote:
> > I'm trying to use a software package written in ocaml (IBAL), however,
> > it fails a test due to 'Fatal error: exception Invalid_argument("equal:
> > functional value"). It seems that equality isn't defined for functional
> > values in OCAML (although I'm not an expert), so I'm wondering what the
> > workaround is.
> 
> This may not sound very helpful, but: you are doing something wrong if 
> you need to rely on equality of functions. Equality of functions is not 
> computable.
> 
> A suitable workaround would be to tell us what it is that you are doing, 
> and we will tell you what to use instead of functions (if possible). To 
> give you an idea of what you I am talking about:
> 
> Suppose you came to us and complained that you cannot compare 
> polynomials with integer coefficients, and it turned out that you 
> represent polynomials as functions. We would then tell you not to do 
> that, and represent polynomials as arrays (or lists) of coefficients, or 
> objects, or some other data structure that is equipped with decidable 
> equality.

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.

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

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.

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);

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

An extension to Ocaml which allowed for semantics
might be interesting: the usual technique is to just
put comments: that's pretty weak in this day an age 
isn't it?


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net