Email Gateway (Aug 22 2022 at 10:15): Email Gateway (Aug 22 2022 at 10:15):From: Diego Machado Dias <diegodias.m@gmail.com>
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
Email Gateway (Aug 22 2022 at 10:15):From: Lars Hupel <hupel@in.tum.de>
See also the answer by Manuel on Stack Overflow: http://stackoverflow.com/a/30932175
Email Gateway (Aug 22 2022 at 10:15):From: Manuel Eberl <eberlm@in.tum.de>
Dear Diego,
I already gave you a very detailed answer to your question on
StackOverflow yesterday:
http://stackoverflow.com/questions/30921002
If you find that answer unsatisfactory, may I suggest you explain why
instead of asking the exact same question again here?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 10:15):From: Diego Machado Dias <diegodias.m@gmail.com>
Dear Manuel,
Thank you very much for your quick and the detailed answer in Stack
Overflow,
the theoretical explanation there clarified the issue with the grammar, and
I am
experimenting the suggestions provided there. I'll soon comment on your
answer
there, so the discussion stays in the same place.
This email was sent to the isabelle user's list before the question on Stack
Overflow to be answered. Sorry for the duplication. Next time I will post
either
here or there instead of both places.
Cheers,
Diego Dias
Last updated: Nov 21 2024 at 12:39 UTC