From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA11897; Tue, 27 Mar 2001 19:05:53 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA11893 for ; Tue, 27 Mar 2001 19:05:52 +0200 (MET DST) Received: from mail4.microsoft.com (mail4.microsoft.com [131.107.3.122]) by concorde.inria.fr (8.11.1/8.10.0) with SMTP id f2RH5pn06781 for ; Tue, 27 Mar 2001 19:05:51 +0200 (MET DST) Received: from 157.54.1.52 by mail4.microsoft.com (InterScan E-Mail VirusWall NT); Tue, 27 Mar 2001 09:05:42 -0800 (Pacific Standard Time) Received: from red-msg-04.redmond.corp.microsoft.com ([157.54.12.74]) by inet-imc-06.redmond.corp.microsoft.com with Microsoft SMTPSVC(5.0.2195.2883); Tue, 27 Mar 2001 09:05:13 -0800 X-MimeOLE: Produced By Microsoft Exchange V6.0.4418.65 Content-Class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="US-ASCII" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] recursive modules redux, & interface files Date: Tue, 27 Mar 2001 09:05:13 -0800 Message-ID: Thread-Topic: [Caml-list] recursive modules redux, & interface files Thread-Index: AcC2nLl8E1EVrZvnRhS0iPr8dMCcPwAQMLNg From: "Manuel Fahndrich" To: X-OriginalArrivalTime: 27 Mar 2001 17:05:13.0856 (UTC) FILETIME=[16D80800:01C0B6E0] Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk To add more fuel to this interesting conversation, I've recently come across a nice analogy between recursive modules and the assume-guarantee rules known from model checking. The assume-guarantee rule in model checking allows models to be checked relatively independently. In general, the AG rule takes on the form AI | B <=3D BI A | BI <=3D AI ------------------- [some side conditions] A | B <=3D AI | BI where A and B are two processes, and we want to check that the parallel composition A | B conforms to some interface AI | BI. In general, it is not the case that A <=3D AI and B <=3D BI, which would lead to the = result. Instead, some amount of information about the interactions between A and B are needed. This is expressed in the preconditions AI | B <=3D BI, = i.e., we check that B composed with the interface specification of A (AI) conforms to BI, and similarly for A.=20 The side conditions depend on the particular domain being modeled. If the models are synchronous and asynchronous logic circuits, then the side conditions express that there cannot be any logical circularities between module A and B, ie. mutually recursive definitions of wires that do not involve at least one latch. Now what does this have to do with recursive modules? May be by now this is obvious, but let me say it anyway. In the context of recursive modules, composition is linking, and conformance is interface checking. If we have two modules A and B that are mutually recursive and we want to ascribe interfaces AI and BI to these, it may be the case that we cannot do that independently, that is we can only ascribe these interfaces, given that we know we will link A with something conforming to BI and link B with something conforming to AI, ie., we can use the assume guarantee rule. The notation AI | B <=3D BI then simply states that in order to verify that B has interface BI, we also need to know the interfaces AI of module A that will be linked with B. What about the side conditions? It turns out that the side conditions of an assume guarantee rule for modules is very similar to that of logical circuits, namely, we cannot have any circular definitions of values that do not involve a function abstraction (a delay). module A =3D struct let (x:int) =3D B.y end module B =3D struct let (y:int) =3D A.x end contains such a circular definition, whereas=20 module A =3D struct let fx () =3D B.fy () end module B =3D struct let fy () =3D A.fx () end Thus the side conditions are concerned with correct initialization. This is of course not new, Crary and Harper have given sufficient conditions on recursive module definitions for these properties to be true, and I suppose Claudio Russo has similar conditions, although I haven't read his thesis yet. Regards, -Manuel Fahndrich =20 -----Original Message----- From: Xavier Leroy [mailto:Xavier.Leroy@inria.fr]=20 Sent: Tuesday, March 27, 2001 1:01 AM To: Don Syme Cc: caml-list@inria.fr Subject: Re: [Caml-list] recursive modules redux, & interface files > Isn't it feasible to annotate elements of signatures with something that > indicates that an identifier really is bound to a value, rather than a > module?? i.e. You probably meant "rather than a result of an arbitrary computation". Yes, it can be done this way, and I believe such annotations in signatures are necessary for a full treatment of recursion between modules (the Holy Grail :-). However, they also pollute signatures with "implementation details". For more modest forms of recursion, e.g. cross-recursion between compilation units, I was hoping this information could be propagated behind the scene, without cluttering signatures, or just re-inferred and checked at link-time. This is just a vague idea. Cheers, - Xavier Leroy ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr