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=HTML_MESSAGE, UNPARSEABLE_RELAY 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 1813ABC0C; Tue, 30 Jan 2007 16:25:11 +0100 (CET) Received: from imr5.us.db.com (imr4.us.db.com [160.83.65.196]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0UFP9wi013310 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL); Tue, 30 Jan 2007 16:25:10 +0100 Received: from sdbo1006.db.com by imr5.us.db.com id l0UFL6ME008976; Tue, 30 Jan 2007 10:25:05 -0500 (EST) In-Reply-To: <1170165303.6391.20.camel@rosella.wigram> To: caml-list@yquem.inria.fr Cc: caml-list-bounces@yquem.inria.fr Subject: Re: [Caml-list] Equality of functional values MIME-Version: 1.0 X-Mailer: Lotus Notes Release 6.5.5 CCH1 March 07, 2006 From: Jeff Polakow Message-ID: Date: Tue, 30 Jan 2007 10:21:51 -0500 X-MIMETrack: Serialize by Router on sdbo1006/DBNA/DeuBaInt/DeuBa(Release 6.5.4 HF129|May 12, 2005) at 01/30/2007 10:25:05 AM, Serialize complete at 01/30/2007 10:25:05 AM Content-Type: multipart/alternative; boundary="=_alternative 005465EA85257273_=" X-Miltered: at discorde with ID 45BF6355.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; polakow:01 polakow:01 undecidable:01 recursion:01 formalize:01 transforming:01 undecidable:01 recursion:01 formalize:01 transforming:01 verifiable:98 verifiable:98 sourceforge:01 sourceforge:01 sans-serif:98 This is a multipart message in MIME format. --=_alternative 005465EA85257273_= Content-Type: text/plain; charset="US-ASCII" 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. --=_alternative 005465EA85257273_= Content-Type: text/html; charset="US-ASCII"
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.
--=_alternative 005465EA85257273_=--