From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id D011DBDDA for ; Fri, 26 Aug 2005 18:49:08 +0200 (CEST) Received: from smtp.cegetel.net (mf01.sitadelle.com [212.94.174.68]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j7QGn80h003252 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Fri, 26 Aug 2005 18:49:08 +0200 Received: from [192.168.144.2] (84-4-33-159.adslgp.cegetel.net [84.4.33.159]) by smtp.cegetel.net (Postfix) with ESMTP id 8B6493184EA; Fri, 26 Aug 2005 18:48:50 +0200 (CEST) Message-ID: <430F47F1.5020302@univ-savoie.fr> Date: Fri, 26 Aug 2005 18:48:49 +0200 From: Christophe Raffalli User-Agent: Mozilla Thunderbird 1.0.6 (X11/20050716) X-Accept-Language: fr, en MIME-Version: 1.0 To: Diego Olivier Fernandez Pons Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Re: Parameter evaluation order References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at nez-perce with ID 430F4804.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 caml-list:01 pons:01 compiler:01 denotes:01 denotes:01 reasonnable:01 monadic:01 ...:98 ...:98 define:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=FORGED_RCVD_HELO autolearn=disabled version=3.0.3 Diego Olivier Fernandez Pons a écrit : > Bonjour, > > >>why should the evaluation order be specified: this is needed if you >>want to formally reason about programs ... as far as I know. > > > Could you elaborate more on this ? > > I see the evaluation order in Caml more as a compiler optimization > problem that a semantic one. If I need a specific evaluation order, I > just sequencialize my program explicitelly. > Let us say you want to prove a program using references ... one possible way is to translate is automatically in a purely functional program using a state monad ... then you need to specify the evaluation order to define the translation of let x = f a_1 ... a_n in which could approximately be (x' denotes the translation of x) ans s denotes the states holding the map table assigning values to addresses let s,a_n = a'_n s in let s,a_(n-1) = a'_(n-1) s in .. let s,a_1 = a'_1 s in let s,x = f' s a_1 ... a_n in to define this translation, you need to know the evaluation order and it is not reasonnable to assume that the program you want to prove if fully sequentialized (and if you want to force sequentialized program then you should only allow variables as function arguments in the language definition ;-). Remark: clearly, a good proof system should not show the monadic translation and hide it behind the scene ... but such a system for full ML does not exist yes (as far as I know).