From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 1BCFCBB9A for ; Wed, 5 Oct 2005 13:14:52 +0200 (CEST) Received: from haka.fmf.uni-lj.si (haka.fmf.uni-lj.si [193.2.67.18]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j95BEnCg002276 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Wed, 5 Oct 2005 13:14:51 +0200 Received: from bsn-77-186-71.dsl.siol.net ([193.77.186.71] helo=[192.168.1.100]) by haka.fmf.uni-lj.si with esmtpa (Exim 4.50) id 1EN7EO-0003Xp-Ao for caml-list@yquem.inria.fr; Wed, 05 Oct 2005 13:14:48 +0200 Message-ID: <4343B57B.3070702@andrej.com> Date: Wed, 05 Oct 2005 13:14:03 +0200 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Debian Thunderbird 1.0.2 (X11/20050331) X-Accept-Language: en-us, en MIME-Version: 1.0 Cc: caml-list@yquem.inria.fr References: <20051001210520.64728.qmail@web26809.mail.ukl.yahoo.com> <1128300118.10449.136.camel@rosella> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: 7bit X-SA-Exim-Connect-IP: 193.77.186.71 X-SA-Exim-Mail-From: Andrej.Bauer@andrej.com Subject: Re: [Caml-list] Avoiding shared data X-SA-Exim-Version: 4.2 (built Thu, 03 Mar 2005 10:44:12 +0100) X-SA-Exim-Scanned: Yes (on haka.fmf.uni-lj.si) X-Miltered: at nez-perce with ID 4343B5A9.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; andrej:01 andrej:01 caml-list:01 avoiding:01 transforming:01 rec:01 rec:01 abstraction:01 recursion:01 recursion:01 wrote:01 wrote:01 abstract:01 data:02 transform:03 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Thomas Fischbacher wrote: > He presumably wanted to see a different thing, e.g. > automatically transforming > let rec fac1 x = > if x = 0 > then 1 > else x*(fac1 (x-1)) > ;; > > into > > let fac2 x = > let rec walk so_far todo = > if todo = 0 > then so_far > else walk (todo*so_far) (todo-1) > in walk 1 x > ;; > > My impression is that it may indeed be possible to do something like this > for simple applications, but that the cases that can be covered > automatically presumably are so limited that an experienced programmer > will usually want to attack them by going to a higher form of abstraction > and not waste time on such things anyway. Incidentally, I recently wrote a little piece on how to transform one kind of recursion into another kind of recursion via propositions-as-types http://math.andrej.com/2005/09/16/proof-hacking/ which may be of interest to some of you. I only considered a very simple kind of recursion on natural numbers. My impression is that quite a general form of recursion could be treated (replace natural numbers by a well-founded type, for example). This sort of thing is probably not immediately useful in programming practice. But even "real" programmers should be aware of abstract mathematical ideas because they they indirectly make them write better programs. Best regards, Andrej