This page documents the KIV formalization of
Gerhard Schellhorn, Jörg Pfähler, Gidon Ernst, Wolfgang Reif:
A Relational Encoding for a Clash-Free Subset of ASMs.
Submitted to ABZ 2016.
Quick start (detailed explanations follow).
Lemma 1. Given that R
yields update set U
, i.e., ⟦R⟧(A,ξ) ▷ U
:
mod
:f ∉ mod(R)
then (f,a,b) ∉ U
for all a
, b
.dep
:g^A = g^A⊕U
for all g ∈ dep(R,f)
then A, ξ ⊧ asg(R,f)
iff A⊕U, ξ ⊧ asg(R,f)
.asg
(f,a,b) ∈ U
for some a
, b
then A,ξ{farg ↦ a} ⊧ asg(R,f)
.con
A,ξ ⊧ con(R)
then U
is consistent.Theorem 1. Given a rule R
with mod(R) = f
and assuming a clash-free rule with A,ξ ⊧ con(R)
,
then ⟦R⟧(A,ξ) ▷ U
implies that A ∪ (A⊕U)' ⊧ rel(R)(f,f')
.
You are invited to skip directly to syntactic consistency or to the relational semantics.
x,y: variable
f,g,h: function
a,b: value
with a constant _true
u: update
, where a concrete update _(f,a,b)
is written with a leading underscore.A term t: term
is either a variable (embedded as ⌜x⌝
) or application of a function to an argument (written f[t]
).
ASM rules R: rule
comprise
f[t1] := t2
, written _asg(f,t1,t2)
_par(R1,R2)
and sequential _seq(R1,R2)
composition_if(t,R1,R2
We have not (yet) included calls in the KIV development as they behave just like assignments in the consistency check. To support recursive calls, a Kleene fixpoint could be specified as it is done for example in this formalization of RGITL (see the section on procedure declarations).
The semantics is given in terms of
ξ: variable → value
A: function × value → value
, where the carrier set is implicitly given by the type value
(including the booleans with a constant _true
)U: update → bool
that are modeled as higher-order function variables for convenience.
Modification of a valuation at variable x
to a new value a
is just function override, written ξ(x;a)
in KIV, similarly for algebras.
The semantics ⟦t⟧(A,ξ)
of terms t
is standard.
The update semantics ⟦R⟧>(A,ξ)(U)
of rules R
denotes whether R
yields the set of updates U
. It is defined recursively over the structure of rules (axioms sem-*
). The cases are straight forward transcription of the inductive system given e.g. by Börger 1 or Stärk and Nanchen 2, except that true nondeterminism is used here instead of choice functions, i.e., several U
may satisfy ⟦R⟧>(A,ξ)(U)
. We point out some specific aspects of the encoding:
_asg(f,t1,t2)
is a predicate λ u. u = _(f, ⟦t0⟧(A,ξ), ⟦t1⟧(A,ξ))
characterizing this one update u
.R1
and R2
takes apart two cases, depending on whether the first update set U1
is consistent (predicate con(U1)
). The second rule then starts in a modified algebra A ⊕ U1
.(φ ⊃ a ; b)
as in the paper.a
such that the test t
evaluates to the (semantic) constant _true
. The body is then executed with the modified valuation ξ(x;a)
.aU: value → (update → bool)
a
that is either computed by the body or forced to be empty when the test does not hold.U
is then the union of all these aU(a)
(operator U_ .
). Admittedly, the notation is a bit overloaded here.Several helper lemmas about the relation of algebras and update sets are proved here.
The function symbols and variables occuring in terms and formulas are defined here.
The set of functions f
modified by R
is is characterized by mod(R,f)
.
The set of dependencies g
that possibly affect arguments of f
in R
is given by predicate dep(R,f,g)
.
For asg
and con
, we have taken a shallow approach to the embedding (in contrast to the embedding for rules): In the paper, these generate syntactic formulas that can be checked by an external tool. Here, we refrain from a deep encoding of formula syntax as a data type. Since we only ever need the evaluated forms, i.e., A,ξ ⊧ asg(R,f)
and A,ξ ⊧ con(R)
in the notation of the paper, we directly give the result of evaluating the respective formula over A
and ξ
.
Whether function f
is possibly assigned for an argument x
in the algebra A
and valuation ξ
is characterized by asg(R,f,x)(A,ξ)
. The only complex case is that for sequential composition.
Syntactic consistency is given by con(R)(A,ξ)
. Sequential composition quantifies the algebra A
instead of renaming the modified function symbols in the second rule R2
. The values of functions g ∉ mod(R1)
are kept, others are discarded, reflecting the freshness condition on such functions.
The proofs for Lemma 1 are all by induction over the structure of the rule.
Correctness of mod
. is straight forward. Unfolding all definitions recursively once is sufficient.
Correctness of dep
proves a coincidence for asg
. It depends on a similar coincidence for terms to show that the conditions of conditionals and choose/forall match up.
Correctness of asg
encodes the assumption that the designated farg
from the paper do not occur otherwise as an assumption ¬ x ∈ R
(as defined here). The interesting case is sequential composition, which depends on the correctness of mod
and dep
to establish that f
has not been affected by the first part of the sequential composition (proof step 21).
Correctness of con
needs some manual interaction (hollow proof nodes) for instantiating the hypotheses, in particular, the proof for the forall construct is somewhat tedious, because updates of different runs of the body have to be compared.
The relational encoding rel(R)(A,A0,ξ)
relates two algebras A
and A0
, where A
stores the unprimed function symbols f
and A0
stores their primed counterparts. Similarly to the formalization of asg
and dep
, the semantics is thus intertwined with the definitions to spare us to reason about syntactic renaming (the additional overhead seems not justified as the main results reflected faithfully anyway).
The merge operation for parallel composition is thus done on the level of algebras A1
and A2
resulting from the respective subrule.
The forall construct is encoded in terms of a mapping Af
that gives the resulting algebra for the run of the body R
for index a
like it has been done for the update semantics.
Theorem 1 is proved here, as well as the converse statement. These two theorems together show that the relational semantics is in fact identical to the update semantics for consistent rules.