Equality of functional values

Equality of functional values

[Simon Frost]

Dear Caml List,

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 apparently worked fine in ocaml 3.04, but not in
later versions. I'm using ocaml 3.08.3, and I get this error message
both on Linux (SUSE 9.1 Profession, x86_64) and Windows XP (x86). Any
help would be greatly appreciated! I'd rather not have multiple versions
of ocaml floating around...

Best wishes
Simon
-- 
Simon D.W. Frost, D.Phil.
Assistant Adjunct Professor of Pathology
University of California, San Diego
Mailcode 8208
UCSD Antiviral Research Center
150 W. Washington St.
San Diego, CA 92103
Tel: +1 619 543 8898
Fax: +1 619 543 5094
Email: sdfrost@ucsd.edu

Re: [Caml-list] Equality of functional values

[Tom]

[-- Attachment #1: Type: text/plain, Size: 565 bytes --]

It's hard to perform equality on functional values, as it is hard to confirm
two functions being the same... (even if you know the mathematical
definition of the function, thus even harder if you only know the machine
representation of it...). The best way around is to use == equality (= is
structural equality, while == is referential equality - whether two names
point to the same address in the memory), which might return false often,
but will never fail on functional values. So I guess it's best you edit the
source code (if you can) and change it...

- Tom

[-- Attachment #2: Type: text/html, Size: 584 bytes --]

Re: [Caml-list] Equality of functional values

[Brian Hurt]

Tom wrote:

> It's hard to perform equality on functional values, as it is hard to 
> confirm two functions being the same... (even if you know the 
> mathematical definition of the function, thus even harder if you only 
> know the machine representation of it...). The best way around is to 
> use == equality (= is structural equality, while == is referential 
> equality - whether two names point to the same address in the memory), 
> which might return false often, but will never fail on functional 
> values. So I guess it's best you edit the source code (if you can) and 
> change it...
>

The problem with this is that it fails on partially applied functions.  
For example:

# let f x y = x + y;;
val f : int -> int -> int = <fun>
# f == f;;
- : bool = true
# (f 1) == (f 1);;
- : bool = false
#

This happens for the same reasons that:
# 1. == 1.;;
- : bool = false
#

does.  Basically, both the expressions 1. and (f 1) allocate blocks on 
the heap.  Evaluating them twice allocates different blocks, and thus 
referential comparisons return false.

My general advice is don't depend upon equality of functions.

Brian

Re: [Caml-list] Equality of functional values

[Gerd Stolpmann]

Am Montag, den 29.01.2007, 13:04 -0800 schrieb Simon Frost:
> Dear Caml List,
> 
> 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 apparently worked fine in ocaml 3.04, but not in
> later versions. I'm using ocaml 3.08.3, and I get this error message
> both on Linux (SUSE 9.1 Profession, x86_64) and Windows XP (x86). Any
> help would be greatly appreciated! I'd rather not have multiple versions
> of ocaml floating around...

As far as I remember there was a slight change for the equality around
3.07 or 3.08. Previous versions of O'Caml always tested for physical
equality first, and only if the two values are not the same they are
compared component by component. So if the two compared functions are
always the same, this equality test never failed. In current O'Caml,
such a physical test is not done. E.g. look at

# let f() = 42;;
val f : unit -> int = <fun>
# f = f;;
Exception: Invalid_argument "equal: functional value".
# f == f;;
- : bool = true

In old O'Caml versions "f = f" worked because the "f == f" test was
implicitly performed first. (This was changed because of an
incompatibility with conventional floating point semantics.)

If it is not possible to remove the functional parts from the compared
values entirely, there is an easy workaround: Wrap the functions into
objects. The equality for objects is well-defined: Objects are only
equal if they are the same.

The code looks now like:

# let obj_f = object method f() = 42 end;;
val obj_f : < f : unit -> int > = <obj>
# obj_f = obj_f;;
- : bool = true

In order to call the wrapped function:

# obj_f # f();;
- : int = 42

Gerd
-- 
------------------------------------------------------------
Gerd Stolpmann * Viktoriastr. 45 * 64293 Darmstadt * Germany 
gerd@gerd-stolpmann.de          http://www.gerd-stolpmann.de
Phone: +49-6151-153855                  Fax: +49-6151-997714
------------------------------------------------------------

Re: [Caml-list] Equality of functional values

[Christophe Raffalli]

Gerd Stolpmann a écrit :
> Am Montag, den 29.01.2007, 13:04 -0800 schrieb Simon Frost:
>> Dear Caml List,
>>
>> 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 apparently worked fine in ocaml 3.04, but not in
>> later versions. I'm using ocaml 3.08.3, and I get this error message
>> both on Linux (SUSE 9.1 Profession, x86_64) and Windows XP (x86). Any
>> help would be greatly appreciated! I'd rather not have multiple versions
>> of ocaml floating around...
> 

You could test equality after Marshalling ? On closures, it should compare code address
and the values in the closure. This does not give extentionnal equality (which is impossible), but an
intentional equality which is sometimes meaningful. I am wondering why this is not the default
for = or at least why the is not a way to choose like in the marshall module.

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------

Re: [Caml-list] Equality of functional values

[David MENTRE]

Hello Gerd,

2007/1/29, Gerd Stolpmann <info@gerd-stolpmann.de>:
> As far as I remember there was a slight change for the equality around
> 3.07 or 3.08.

I think that was in OCam 3.08:
http://caml.inria.fr/pub/distrib/ocaml-3.09/notes/Changes
"""
Objective Caml 3.08.0:
----------------------
(Changes that can break existing programs are marked with a "*"  )
[...]
Standard library:
* Revised handling of NaN floats in polymorphic comparisons.
  The polymorphic boolean-valued comparisons (=, <, >, etc) now treat
  NaN as uncomparable, as specified by the IEEE standard.
  The 3-valued comparison (compare) treats NaN as equal to itself
  and smaller than all other floats.  As a consequence, x == y
  no longer implies x = y but still implies compare x y = 0.
"""

Best wishes,
d.

Re: [Caml-list] Equality of functional values

[Andrej Bauer]

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.

Andrej

Re: [Caml-list] Equality of functional values

[skaller]

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

Re: [Caml-list] Equality of functional values

[Brian Hurt]

[-- Attachment #1: Type: text/plain, Size: 2124 bytes --]

skaller wrote:

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

The problem is that "programmer written functions" are a subset of all 
possible functions.  Consider the three following expressions:

let f x = x + 3 in f

let f x y = x + y in (f 3)

let o = object method f x = x + 3 end in o#f

All of these expressions have type int -> int and thus are functions (in 
the general sense).   At which point the naive question becomes why they 
aren't comparable?

Worse yet, all three are "equal" in the sense that for all ints, when 
called with the same argument they will return the same value.

This problem is trickier than it looks at first glance.

Brian


[-- Attachment #2: Type: text/html, Size: 2668 bytes --]

Re: [Caml-list] Equality of functional values

[Jeff Polakow]

[-- Attachment #1: Type: text/plain, Size: 2295 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 3182 bytes --]

Re: [Caml-list] Equality of functional values

[Jacques Carette]

Serious suggestion:  I personally would be quite happy with extensional 
equality on ground values and intensional equality on function values.

Jacques

Re: [Caml-list] Equality of functional values

[Chris King]

Agreed.  Such a comparison is useful for libraries which must work
with arbitrary datatypes but want to compare as finely as possible.  I
once wrote a small pure-O'Caml module to do just that, you
can download it at
http://users.wpi.edu/~squirrel/repos/ocamlrt/fr/fr/genEq.ml.  Caveat
emptor: it does not work on cyclic structures, and uses Obj
extensively so I cannot guarantee it won't crash.  It tries first
physical equality, then structural equality, so it is semantically
different from Caml's = operator in the case of floats.

- Chris

On 1/30/07, Jacques Carette <carette@mcmaster.ca> wrote:
> Serious suggestion:  I personally would be quite happy with extensional
> equality on ground values and intensional equality on function values.
>
> Jacques
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Equality of functional values

[Tom]

[-- Attachment #1: Type: text/plain, Size: 933 bytes --]

I guess the "correct" way to do = equality would be to check for tag (
Obj.tag (Obj.repr x)), and if it isn't float (or float array) then ==
equality would be performed first. The problem is that this would have to be
implemented by the OCaml developers, as the naive implementation:

let equal x y =
         if Obj.tag (Obj.repr x) = Obj.double_tag then x = y
         else
                 if x == y then true else x = y

doesn't work, as it should be called recursively (comparing two lists of
functions will fail, because the functions would be compared by =, not by
equal).

Actually, the implementation could be improved further, as it could actually
return true on examples such as

# let f x y = x + y;;
val f : int -> int -> int = <fun>
# f == f;;
- : bool = true
# (f 1) = (f 1);;
- : bool = true

because the parameters, passed to a closure, could be compared, too...

Anyhow, this can be added to the wishlist :)

- Tom

[-- Attachment #2: Type: text/html, Size: 1198 bytes --]

Re: [Caml-list] Equality of functional values

[Gerd Stolpmann]

Am Dienstag, den 30.01.2007, 21:18 +0100 schrieb Tom:
> I guess the "correct" way to do = equality would be to check for tag
> (Obj.tag (Obj.repr x)), and if it isn't float (or float array) then ==
> equality would be performed first. The problem is that this would have
> to be implemented by the OCaml developers, as the naive
> implementation: 
> 
> let equal x y =
>          if Obj.tag (Obj.repr x) = Obj.double_tag then x = y
>          else 
>                  if x == y then true else x = y
> 
> doesn't work, 

But

let equal x y = 
  Pervasives.compare x y = 0

works!

> as it should be called recursively (comparing two lists of functions
> will fail, because the functions would be compared by =, not by
> equal). 
> 
> Actually, the implementation could be improved further, as it could
> actually return true on examples such as 
> 
> # let f x y = x + y;;
> val f : int -> int -> int = <fun>
> # f == f;;
> - : bool = true 
> # (f 1) = (f 1);;
> - : bool = true
> 
> because the parameters, passed to a closure, could be compared, too...
> 
> Anyhow, this can be added to the wishlist :)

I can fully understand that ( = ) fails on functional values. The
additional test for floats would take a lot of time, given that equality
is the most frequent test.

A better improvement would be that the compiler emits a warning when
there is the possibility that the equality test compares functional
values. In my opinion this is a serious programming error, and the
compiler should help to track it down.

Gerd
-- 
------------------------------------------------------------
Gerd Stolpmann * Viktoriastr. 45 * 64293 Darmstadt * Germany 
gerd@gerd-stolpmann.de          http://www.gerd-stolpmann.de
Phone: +49-6151-153855                  Fax: +49-6151-997714
------------------------------------------------------------

Re: [Caml-list] Equality of functional values

[Fernando Alegre]

Maybe what should be in the wait list is the following:

Keep == as it is now

Revert = to its previous behavior: first check physical then structural

Add a new operator =. for floating-point-aware equality that works on
everything the way = works now.

Would not this make everyone happy?

Fernando

On Tue, Jan 30, 2007 at 09:30:01PM +0100, Gerd Stolpmann wrote:

> But
> 
> let equal x y = 
>   Pervasives.compare x y = 0
> 
> works!

Re: [Caml-list] Equality of functional values

[Christophe TROESTLER]

On Tue, 30 Jan 2007, Fernando Alegre <fernando@cc.gatech.edu> wrote:
> 
> Add a new operator =. for floating-point-aware equality that works on
> everything the way = works now.
> 
> Would not this make everyone happy?

No.  Why not take the suggestion of Gerd Stolpmann and declare

  let ( = ) x y = Pervasives.compare x y = 0

at the beginning of your files ?

ChriS

Re: [Caml-list] Equality of functional values

[Tom]

[-- Attachment #1: Type: text/plain, Size: 427 bytes --]

>
>  Why not take the suggestion of Gerd Stolpmann and declare
>
>   let ( = ) x y = Pervasives.compare x y = 0
>
> at the beginning of your files ?



Because it fails on functions (if functions are the same, it returns true,
otherwise it raises an exception...

# let f x y = x + y;;
val f : int -> int -> int = <fun>
# compare f f;;
- : int = 0
# compare (f 0) (f 0);;
Exception: Invalid_argument "equal: functional value".

[-- Attachment #2: Type: text/html, Size: 665 bytes --]

Re: [Caml-list] Equality of functional values

[Christophe TROESTLER]

On Tue, 30 Jan 2007, Fernando Alegre <fernando@cc.gatech.edu> wrote:
> 
> On Tue, Jan 30, 2007 at 10:01:41PM +0100, Christophe TROESTLER wrote:
> > On Tue, 30 Jan 2007, Fernando Alegre <fernando@cc.gatech.edu> wrote:
> > > 
> > > Add a new operator =. for floating-point-aware equality that works on
> > > everything the way = works now.
> > > 
> > > Would not this make everyone happy?
> > 
> > No. 
> 
> Why not?

Because, like several other people on this list, I am mostly writing
numerical code and, while the behaviour w.r.t. NaN is only
occasionally useful, it is good to have it as the standard (mandated
by IEEE 754).

See also http://caml.inria.fr/pub/ml-archives/caml-list/2001/02/bfbab5317267480356248b6e004c0eee.en.html

> Because that is no good for libraries.

Well, IMHO, for libraries you want to be able to declare the
equality/comparison explicitely in the functions that need it (or else
use a functor).

On Tue, 30 Jan 2007, Fernando Alegre <fernando@cc.gatech.edu> wrote:
> 
> Revert = to its previous behavior: first check physical then structural
>
> On Tue, 30 Jan 2007, Tom <tom.primozic@gmail.com> wrote:
> > 
> > >   let ( = ) x y = Pervasives.compare x y = 0
> > 
> > Because it fails on functions

Ok.  I got mislead by Fernando's comment letting us think that it was
the solution to the OP problem -- but did not check the OP post.

Still, I don't think Andrej Bauer concern was properly addressed: what
concrete problem do you want equality of functions for?

Cheers,
ChriS

Re: [Caml-list] Equality of functional values

[Fernando Alegre]

On Tue, Jan 30, 2007 at 10:46:57PM +0100, Christophe TROESTLER wrote:
> On Tue, 30 Jan 2007, Fernando Alegre <fernando@cc.gatech.edu> wrote:
> > 
> > On Tue, Jan 30, 2007 at 10:01:41PM +0100, Christophe TROESTLER wrote:
> > > On Tue, 30 Jan 2007, Fernando Alegre <fernando@cc.gatech.edu> wrote:
> > > > 
> > > > Add a new operator =. for floating-point-aware equality that works on
> > > > everything the way = works now.
> > > > 
> > > > Would not this make everyone happy?
> > > 
> > > No. 
> > 
> > Why not?
> 
> Because, like several other people on this list, I am mostly writing
> numerical code and, while the behaviour w.r.t. NaN is only
> occasionally useful, it is good to have it as the standard (mandated
> by IEEE 754).

So you are happily using +. and *. for floats now. Why not use
a similar operator =. for float comparison?

The point is that floats in OCaml _are_ treated especially anyway.

> 
> See also http://caml.inria.fr/pub/ml-archives/caml-list/2001/02/bfbab5317267480356248b6e004c0eee.en.html

There are two separate notions of equality mixed together.
My point is, should "OCaml polymorphic equality" be the
same concept at "IEEE equality"?

Why not wish for three separate operators (=,== and =.)?

> 
> > Because that is no good for libraries.
> 
> Well, IMHO, for libraries you want to be able to declare the
> equality/comparison explicitely in the functions that need it (or else
> use a functor).


I mean external libraries which I would not like having to change
at every source file.

Fernando

Re: [Caml-list] Equality of functional values

[skaller]

On Tue, 2007-01-30 at 17:05 -0500, Fernando Alegre wrote:

> There are two separate notions of equality mixed together.
> My point is, should "OCaml polymorphic equality" be the
> same concept at "IEEE equality"?

No, this is not possible. x <> x is the IEEE test for a NaN,
and cannot possibly be used in a structural equality
test which is primarily required for inserting data into
containers: you'd have a Set in which after inserting
a value the value wasn't in the Set!


> Why not wish for three separate operators (=,== and =.)?

What about abstract types?

The bottom line is: you can always write your own comparison
functions and use them with modular functors (extensionally
polymorphic), you can't get a single coherent intensionally
polymorphic equality concept because programs are always using
representations of value rather than the mathematical values.

It is a pity we don't have G'Caml around: it may provide
a convenient way to mix user defined equality with
Ocaml's run time driven polymorphic structural equality.


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

Re: [Caml-list] Equality of functional values

[Andrej Bauer]

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

Re: [Caml-list] Equality of functional values

[Jacques Carette]

Andrej Bauer wrote:
> 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

I really meant 'Intensional equality', in other words, if they are the 
same as far as the system is concerned (in a logic this usually this 
means the same syntactically, but in the case of ocaml that would be 
pointer equality).

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

I was under the impression that ocaml's == did funny things with respect 
to floats?  I want an equality that is "powerful" on ground values and 
== on functional values (ie no exceptions when == is not true).

Jacques

Re: Equality of functional values

[Stefan Monnier]

> I really meant 'Intensional equality', in other words, if they are the same
> as far as the system is concerned (in a logic this usually this means the
> same syntactically, but in the case of ocaml that would be pointer
> equality).

I don't know what the OCaml optimizer may do, but I do know that in SML/NJ
such an intentional equality would often not give the expected result,
because it's pretty common for it to use various forms of eta-like
expansions in the hope of doing uncurrying or argument flattening, so you
may end up with

   f == f

turned into

   (λx1.λx2.f(x1,x2)) == (λy1.λy2.f(y1,y2))

and the system may not try to recognize that the two lambda-expressions are
identical (too costly an analysis for no performance benefit), so it will
compile them to two different pieces of machine language.


        Stefan

Re: [Caml-list] Re: Equality of functional values

[Jacques Carette]

The only times where I have used intensional equality (which was in a 
dynamically typed system for doing mathematics), it would have 
considered the bottom two lambda-expressions to be _different_, as in 
SML/NJ.

This intensional equality is only used for optimizations.  A function 
can optimize some cases based on intensional equality with some known 
cases, and fall-through to a slower general case otherwise.  Not 
recognizing two terms as equivalent only results in slower computation 
time, not an incorrect result.  You might see it as a sort of 
overloading based on function-level matching.

Maple, Mathematica and MuPAD (internally) use this kind of 
dispatch-on-function feature a lot.  This is related to the issue that 
in all these languages, 'constructors' and 'functions' are one and the 
same.  My experience is that in practice, this works.  Perhaps it would 
not be as useful in languages where constructors and functions are 
different.

Jacques

Stefan Monnier wrote:
> I don't know what the OCaml optimizer may do, but I do know that in SML/NJ
> such an intentional equality would often not give the expected result,
> because it's pretty common for it to use various forms of eta-like
> expansions in the hope of doing uncurrying or argument flattening, so you
> may end up with
>
>    f == f
>
> turned into
>
>    (λx1.λx2.f(x1,x2)) == (λy1.λy2.f(y1,y2))
>
> and the system may not try to recognize that the two lambda-expressions are
> identical (too costly an analysis for no performance benefit), so it will
> compile them to two different pieces of machine language.
>
>
>         Stefan
>
>   

Re: [Caml-list] Equality of functional values

[skaller]

On Wed, 2007-01-31 at 00:06 +0100, Andrej Bauer wrote:
> 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.

You're right. Canonical example for me: my own Felix compiler :)
[Encodes functions as data .. Felix language is Turing complete .. :]

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

:) I love this list because there are theoreticians who are
ready to educate us 'real' programmers. 

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

You're right: that was a very nice explanation!

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

The 'axiom_check' facility clearly only checks particular
instances and would only provide a proof if you could
exhaustively elaborate all such instances.

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

Yes. My experience is that it catches quite a lot of errors.
Proof would be better .. but I don't know how to do that.

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

I don't think you're going further .. I'm actually asking that
question! I have looked at Coq, HOPL (light) etc, in the hope
there is some way of using them to complete programmer proof
sketches, but all still seem to need very heavy assistance
beyond the understanding of a non-expert.

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

I believe that this isn't so: there is plenty of incentive
to write correct software. Industry does monitor maintenance
cost of software compared to cost of creating it. We don't need
a plane crash to demonstrate the need for correctness,
in fact that wouldn't help much because the costs aren't
so easy to measure. Wages of people working on maintenance
are measured regularly by all large organisations.

Yet people still use PHP, Python, Java .. why?
Industry may be stupid but it isn't *entirely* stupid :)


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