*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Recursive datatypes*From*: Diego Machado Dias <diegodias.m at gmail.com>*Date*: Fri, 19 Jun 2015 10:57:07 +0100

Hi all, I am wondering if is there a natural way of encoding in Isabelle a grammar like this: Value = VInt int | ... Cmd = Skip | NonDeterministicChoice "Cmd set" | ... The motivation would be to give definition a few specification commands in terms of Non deterministic choice, e.g.: Magic == NonDeterministicChoice {} Rely c r z = Defined using set compreehension and NonDeterministicChoice Isabelle complains about the recursive occurrence of type "Cmd" in "Cmd set" when I try to represent the grammar through a datatype, i.e.: Unsupported recursive occurrence of type "Cmd" via type constructor "Set.set" in type expression "Cmd set". Use the "bnf" command to register "Set.set" as a bounded natural functor to allow nested (co)recursion through it Looking the Isabelle error message when I use set, I couldn't figure out how to register the bounded natural functor for the type 'set' in this context, so I decided to try two speculative solutions. *Speculative solution* *Option 1* Instead of use set, if I use an inductively defined datatype such as list, Isabelle does not complain e.g. datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ... Lists are not the right abstraction here, but I give it a go to see if it would work or not. The immediate effect of using lists is that, instead of use set comprehension I need to use sequence filtering, and the problem then become to come up with two lists: one containing all elements of *Cmd*, and other containing all elements of *Value*. I declared two uninterpreted constants: consts Values :: "Value list" consts Programs :: "Cmd list" Because lists are finite, it makes more sense to explain the constants as "all elements (of interest) of Cmd" and "all values (of interest)". Say, all elements of interest are those that can be represented in the memory of a computer. *Option 2* If I need to use consts, then I could just declare NonDeterministicChoiceSet as consts NonDeterministicChoiceSet :: "Cmd set â Cmd" and explain it (informally) as a function that receives a set of Cmd, and returns the correspondent NonDeterministicChoice fed with the list containing all the elements of the set given as argument, ordered by some criteria, say lexicographic order. Then, rather than use "NonDeterministicChoice" when giving a semantics, I would give a semantics for "NonDeterministicChoiceSet" and only use "NonDeterministicChoiceSet" in the theory. *Questions* 1. Do these modelling make sense if my intention is to capture the grammar of Cmd and give an operational semantics to the constructors of Cmd? 2. Is there a better way of represent that grammar? 3. Is Isabelle the appropriated theorem-prover if I want to represent that grammar? I experimented define this grammar in Z/Eves using free types, and it raised no complains. Thanks in advance for any suggestions, Diego Dias

**Follow-Ups**:**Re: [isabelle] Recursive datatypes***From:*Lars Hupel

**Re: [isabelle] Recursive datatypes***From:*Manuel Eberl

- Previous by Date: [isabelle] Isabelle2015: install problem on Win 7
- Next by Date: Re: [isabelle] Isabelle2015: install problem on Win 7
- Previous by Thread: Re: [isabelle] Isabelle2015: install problem on Win 7
- Next by Thread: Re: [isabelle] Recursive datatypes
- Cl-isabelle-users June 2015 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