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).conA,ξ ⊧ 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: variablef,g,h: functiona,b: value with a constant _trueu: 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,R2We 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 → valueA: function × value → value, where the carrier set is implicitly given by the type value (including the booleans with a constant _true)U: update → boolthat 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 R2takes 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.