Re: [isabelle] A large mutually recursive data type



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
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.