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 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 3C8F4BC0B for ; Tue, 30 Jan 2007 14:55:16 +0100 (CET) Received: from ipmail01.adl2.internode.on.net (ipmail01.adl2.internode.on.net [203.16.214.140]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0UDtCcR023653 for ; Tue, 30 Jan 2007 14:55:15 +0100 Received: from ppp27-234.lns1.syd6.internode.on.net (HELO rosella) ([59.167.27.234]) by ipmail01.adl2.internode.on.net with ESMTP; 31 Jan 2007 00:25:08 +1030 X-IronPort-AV: i="4.13,257,1167571800"; d="scan'208"; a="81311448:sNHT32719848" Subject: Re: [Caml-list] Equality of functional values From: skaller To: Andrej.Bauer@andrej.com Cc: Simon Frost , caml-list@yquem.inria.fr In-Reply-To: <45BF471A.6060603@fmf.uni-lj.si> References: <1170104645.4564.304.camel@penguin.local> <45BF471A.6060603@fmf.uni-lj.si> Content-Type: text/plain Date: Wed, 31 Jan 2007 00:55:03 +1100 Message-Id: <1170165303.6391.20.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.6.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 45BF4E40.001 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 decidable:01 semantics:01 typeclass:01 axioms:01 theorems:01 semantics:01 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 Felix, successor to C++: http://felix.sf.net