Email Gateway (Aug 18 2022 at 14:40): Email Gateway (Aug 18 2022 at 14:40):From: Lutz Schroeder <Lutz.Schroeder@dfki.de>
Hi,
I am presently using the function package in a course; specifically, I
am letting the students prove the rules of a Hoare calculus for partial
correctness over a simple imperative language. The recursive definition
of the semantics is, of course, a partial function, with clauses such as
"Sem (c1 ;;; c2) s = Sem c2 (Sem c1 s)"
where ;;; is sequential composition. Now from a clause such as the above
one would wish to conclude a strictness lemma, in the case of sequential
composition:
lemma seq_dom: "Sem_dom (c1;;;c2, s) ==> Sem_dom (c1, s) &
Sem_dom (c2, Sem c1 s)"
Indeed this can be proved, but the only way I found is somewhat
involved: as indicated in the tutorial for the function package, one can
use the fact that Sem_dom is accp Sem_rel, and apply accp_downward in
connection with Sem_rel.intros. However, one then runs across a somewhat
hidden feature: Sem_rel.intros mentions Sem_sumC, not Sem, and one needs
to unfold the definition of Sem in terms of Sem_sumC to make things work
as expected.
Am I overlooking something? One sort of suspects that strictness
assertions such as the above might be available neatly packaged, say as
"Sem.strictness" or so...
Thanks,
Lutz
Email Gateway (Aug 18 2022 at 14:41):From: Alexander Krauss <krauss@in.tum.de>
Hi Lutz,
[...]
However, one then runs across a somewhat
hidden feature: Sem_rel.intros mentions Sem_sumC, not Sem, and one needs
to unfold the definition of Sem in terms of Sem_sumC to make things work
as expected.
This is the construction the function package does internally to get rid
of mutual recursion and currying. It is a bit ugly...
Am I overlooking something? One sort of suspects that strictness
assertions such as the above might be available neatly packaged, say as
"Sem.strictness" or so...
No, this is not packaged, mainly because at the time I implemented it,
it was not clear what kind of rules are "the canonical thing that one
wants to have". Maybe such a packaging will be added at some point...
Alex
Last updated: Apr 24 2024 at 04:17 UTC