From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL,HTML_MESSAGE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 4DC7DBC0B for ; Tue, 30 Jan 2007 15:21:34 +0100 (CET) Received: from smtp.janestcapital.com (www.janestcapital.com [66.155.124.107]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0UELWsK029204 for ; Tue, 30 Jan 2007 15:21:33 +0100 Received: from [192.168.250.117] [209.213.205.130] by janestcapital.com with ESMTP (SMTPD-9.10) id A46A0260; Tue, 30 Jan 2007 09:21:30 -0500 Message-ID: <45BF546A.1040407@janestcapital.com> Date: Tue, 30 Jan 2007 09:21:30 -0500 From: Brian Hurt User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.7.2) Gecko/20040804 Netscape/7.2 (ax) X-Accept-Language: en-us, en MIME-Version: 1.0 To: skaller Cc: Andrej.Bauer@andrej.com, Simon Frost , caml-list@yquem.inria.fr Subject: Re: [Caml-list] Equality of functional values References: <1170104645.4564.304.camel@penguin.local> <45BF471A.6060603@fmf.uni-lj.si> <1170165303.6391.20.camel@rosella.wigram> In-Reply-To: <1170165303.6391.20.camel@rosella.wigram> Content-Type: multipart/alternative; boundary="------------050703010400070003070106" X-Miltered: at discorde with ID 45BF546C.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0100,:01 andrej:01 ocaml:01 ocaml:01 complained:01 coefficients:01 arrays:01 coefficients:01 decidable:01 subset:01 0100,:01 andrej:01 complained:01 arrays:01 decidable:01 This is a multi-part message in MIME format. --------------050703010400070003070106 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit 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 --------------050703010400070003070106 Content-Type: text/html; charset=us-ascii Content-Transfer-Encoding: 7bit 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

--------------050703010400070003070106--