*To*: Diego Machado Dias <diegodias.m at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Recursive datatypes*From*: Lars Hupel <hupel at in.tum.de>*Date*: Sat, 20 Jun 2015 12:29:53 +0200*In-reply-to*: <CAJA562v+LXaHC9ScYtpXVvuvKGOWQ_N6OZQk=Pne8-P=kVBTdA@mail.gmail.com>*References*: <CAJA562v+LXaHC9ScYtpXVvuvKGOWQ_N6OZQk=Pne8-P=kVBTdA@mail.gmail.com>*User-agent*: K-9 Mail for Android

See also the answer by Manuel on Stack Overflow: http://stackoverflow.com/a/30932175 Le 19 juin 2015 11:57:07 GMT+02:00, Diego Machado Dias <diegodias.m at gmail.com> a Ãcrit : >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

**References**:**[isabelle] Recursive datatypes***From:*Diego Machado Dias

- Previous by Date: [isabelle] a simplifier question 3
- Next by Date: Re: [isabelle] Recursive datatypes
- Previous by Thread: [isabelle] Recursive datatypes
- 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