Dear Alex and all,
once again I started to transform a rather adhoc parser datatype (in
IsaFoR) into some (I think) nicer variant using abstract datatypes with
invariants. After tinkering around for several days (where everything
worked out nicely) I hit a wall, and also remembered that I already did
so some years ago, when I wanted to do the same thing. Only this time,
instead of giving up, I started to think about destructing the wall (not
with my head though ... well ... in a way ;)).
Let me first state my "problem" (parsers are only a special instance).
Suppose you have an abstract datatype with invariant like
typedef T = "{x. Inv x}"
with an "Abs"/"Rep" pair and the invariant "Inv".
---------------------------------------------------------
*Example:* Parsers:
('a, 'b) raw_parser = 'a list => string + ('b * 'a list)
leq p <-> (ALL ts x ts'.
p ts = Inr (x, ts') --> length ts' <= length ts)
typedef ('a, 'b) parser = "{p::('a, 'b) raw_parser. leq p}"
morphisms run Parser
---------------------------------------------------------
When defining a function "f", whose result type is "T", it might be
necessary to "peek under the hood" in order to show termination. When
doing this manually, we destroy the abstraction and always have to
reason about the raw-level and even worse, also all the existing
constants with result type T have to be deconstructed in the definition.
---------------------------------------------------------
*Example:* Suppose we already have do-notation for parsers
(i.e., bind), monadic return, op <|> (for alternatives),
and a parser "just" that parses just the given string. One
simple parser that could be constructed is:
par =
(do { just "(", par; just ")"; return () }) <|>
return ()
However, without lifting the abstraction, we have no handle
on termination. Resulting in something like
par_aux ts = run
((do { just "(", Parser par_aux; just ")"; return () }) <|>
return ())
ts
par = Parser par_aux
where I have to unfold all the abstract definitions in the
body of "par_aux" in order to prove termination and the
termination proof gets really messy (in fact I did not
succeed at all.)
---------------------------------------------------------
Here comes my suggestion (until now I only did a manual --
i.e., all proofs and auxiliary definitions by hand --
case-study for the "par" parser, to check feasibility).
(This only makes sense when "Rep" returns something
of function type.)
Function specifications may be given parameters "Abs", "Rep",
"Inv" (most likely corresponding to some abstract datatype
with invariant) with lemmas:
Abs_inverse: "Inv x ==> Rep (Abs x) = x"
Rep_eqI: "(!!x. Rep f x = Rep g x) ==> f = g"
Then when the user writes something like
function (abstract Abs Rep Inv)
f :: "T"
where
"f = F f"
this is internally replaced by
"Rep f x = Rep (F f) x"
for the inductive definition of the function graph G_f, we replace the
existing (see Alex' thesis, page 17) introduction rules (for simplicity
just using a single recursive call):
(Gamma ==> (r[h/f], h(r[h/f]) : G_f) ==> (x, F h x) : G_f
by
(Gamma ==> (r[h/f], Rep h (r[h/f])) : G_f ==> (x, Rep (F h) x) : G_f
(So we more or less consider "Rep f" instead of just "f" to be the newly
defined function for the purpose of internal constructions.)
The introduction rules for the domain are modified similarly. The
internal definition of the function is now two-fold:
"f' = (%x. THE y. par_graph x y)"
"f = Abs f'"
Furthermore, an additional lemma (besides the usual "x : dom_f ==> EX!y.
(x, y) : G_f") is needed:
"Inv f' ==> x : dom_f ==> (x, Rep (F f) x) : G_f"
(which is proved similarly to the existence part of the standard lemma
and where "Inv f'" is needed to obtain, together with "Abs_inverse",
"Rep f = f'".) Furthermore the usual psimps get an additional assumption:
psimps: "Inv f' ==> x : dom_f ==> Rep f x = Rep (F f) x"
Then the termination proof involves two steps:
- show "!!x. x : dom_f", and
- show "(!!x. x : dom_f) ==> inv f'"
(which is both trivial for the "par" parser). Then we can derive "Rep f
x = Rep (F f) x", which together with "Rep_eqI" yields the desired "f =
F f".
Remark: ideally this should also handle additional parameters of "f"
(which are outside of the abstraction). Maybe something like:
"f x = F f x"
turned into
"Rep (f x) y = Rep (F f x) y"
with
"f' = (%x y. THE z. ((x, y), z) : G_f"
"f = (%x. Abs (f' x))
Any comments? Would anybody else find this useful?
cheers
chris
PS: I started to dive into the function package. My first hurdle is that
for "f" not of function type (as in "par"), no recursive calls are
generated, since "Function_Ctx_Tree.mk_tree" says that "No cong rules
could be found".
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
