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=none 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 433E5BC0B for ; Wed, 31 Jan 2007 00:06:20 +0100 (CET) Received: from postar.fmf.uni-lj.si (vega.fmf.uni-lj.si [193.2.67.45]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0UN6JfI009846 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Wed, 31 Jan 2007 00:06:19 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 0DB37FFC9E; Wed, 31 Jan 2007 00:06:15 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id hGJh22KQ37UA; Wed, 31 Jan 2007 00:18:33 +0100 (CET) Received: from [192.168.1.100] (BSN-77-186-71.dsl.siol.net [193.77.186.71]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id C25C2F9C8C; Wed, 31 Jan 2007 00:06:13 +0100 (CET) Message-ID: <45BFCF7D.5010302@fmf.uni-lj.si> Date: Wed, 31 Jan 2007 00:06:37 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Icedove 1.5.0.9 (X11/20061220) MIME-Version: 1.0 To: caml-list@yquem.inria.fr Cc: skaller , 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: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 45BFCF6B.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; andrej:01 andrej:01 theorems:01 decidable:01 fine-grained:01 non-trivial:01 substituted:01 unit-:01 ocaml:01 unit-:01 decidable:01 bool:01 summarize:01 semantics:01 typeclass:01 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