*To*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Subject*: Re: [isabelle] A large mutually recursive data type*From*: Victor Gomes <vb358 at cam.ac.uk>*Date*: Fri, 11 Mar 2016 13:30:58 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk, Peter Sewell <Peter.Sewell at cl.cam.ac.uk>, Dmitriy Traytel <traytel at inf.ethz.ch>*In-reply-to*: <A3CA0D55-C9A7-47E6-A0C3-36D765BCEDA4@inria.fr>*References*: <9EA07F44-212D-4E74-9085-D2C90E4BFD0C@cam.ac.uk> <7B624798-A387-44B8-817E-ABC7ABA8CC67@inf.ethz.ch> <204CD2AE-DA00-4512-AB7F-AA3D8F70C284@cam.ac.uk> <A3CA0D55-C9A7-47E6-A0C3-36D765BCEDA4@inria.fr>

Dear Jasmin, Thanks for the prompt reply. Cerberus is an ongoing project written in Lem [1], which can automatically export to executable code (OCaml), and to interactive theorem provers (HOL4 and Isabelle). Currently, we are able to export the model to OCaml and execute C programs [2]. We would like to export the model to a theorem prover and prove some properties about it, but we have not decided each theorem prover yet. We would prefer to use Isabelle, because I have more experience with it. The option 1 is clearly not viable, since it would imply change all the current Cerberus code. It would be great if we could try the second option. Since I am still deciding how to proceed, I donât have firm deadlines yet. Cheers, Victor [1] http://www.cl.cam.ac.uk/~pes20/lem/ [2] http://conf.researchr.org/event/pldi-2016/pldi-2016-papers-into-the-depths-of-c-elaborating-the-de-facto-standards > On 11 Mar 2016, at 12:45, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote: > > Dear Victor, > >> Thanks for the answer. I have also tried Isabelle2013-2 (which I believe uses the old Isabelleâs package) with no success, although I didnât wait much longer. > > In principle, we know how to handle such large datatypes. Mutually recursive definitions can be rephrased as nested definitions. For example, instead of > > datatype > 'a tree_list = Nil | Cons "'a tree" "'a tree_list" and > 'a tree = Node 'a "'a tree_list" > > one can define > > datatype 'a list = Nil | Cons 'a "'a list" > datatype 'a tree = Node 'a "'a tree list" > > (We call this "nesting" because "'a tree" occurs recursively nested under "list", but this is not standard terminology.) The nested version scales much better than mutual one with modern versions of Isabelle (but much worse in old versions) -- nesting basically comes for free, whereas an n-ary mutual construction is O(n^3) or O(n^4) (Dmitriy might know). > > Given your specification, I see two options: > > 1. You could introduce nesting manually, in a more or less ad hoc fashion, inspired by the "tree_list" example above. Although this sometimes leads to satisfactory results (as in the "tree list" example above), in your case the result surely wouldn't be pretty. > > 2. We could internally reduce large mutual specifications to nested ones. We already have much of the machinery in place to do this (see the "Nested-to-Mutual Reduction" paragraph, starting on p. 5, in our ITP 2014 paper [*]), but some more engineering would be necessary to (1) heuristically generalize some of the types in some groups (i.e. automatizing part 1) and (2) lifting all the results across isomorphisms, so that this is completely invisible to the user (except that it scales much better). > > I would expect that point 2 would take us up to one week of work to get it right. It is unfortunately rather technical work. How important is this to you? What are your deadlines? And how acceptable is Option 1? > > Cheers, > > Jasmin > > [*] http://www.loria.fr/~jablanch/co-data-impl.pdf >

**Follow-Ups**:**Re: [isabelle] A large mutually recursive data type***From:*Jasmin Blanchette

**References**:**[isabelle] A large mutually recursive data type***From:*Victor Gomes

**Re: [isabelle] A large mutually recursive data type***From:*Dmitriy Traytel

**Re: [isabelle] A large mutually recursive data type***From:*Victor Gomes

**Re: [isabelle] A large mutually recursive data type***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] A large mutually recursive data type
- Next by Date: [isabelle] New in the AFP: Propositional Resolution
- Previous by Thread: Re: [isabelle] A large mutually recursive data type
- Next by Thread: Re: [isabelle] A large mutually recursive data type
- Cl-isabelle-users March 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list