Re: [isabelle] Recursive datatypes



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



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