VI Modelling Miolingo

§1 · A reaction that changes activity

Activity belongs to a control, and the signature fixes it (Chapter II, §1), so no node ever changes its activity. What a reaction can do is replace a node by a node of another control, in the same place, keeping what it contains. Chapter II, §4, showed this on two toy panels; here it is in the model. Miolingo's five views come in pairs of controls: shown v is active and hidden v passive.

def active : (c : Ctl) → atomic c = false → Bool
  | hidden _, _ => false
  | _, _ => true

The model writes its bigraphs as trees (Tm, in BigraphSim/Term.lean), compiled to finite data that a certified builder turns into the library's bigraphs. Showing view k in place of view j is one rule, a family over the two views:

def showView (j k : View) : RuleD Ctl where
  redex := Tm.compile [] [[at_ (.reqShow k), nd (.shown j) [] [st 0], nd (.hidden k) [] [st 1], st 2]]
  reactum := Tm.compile [] [[nd (.hidden j) [] [st 0], nd (.shown k) [] [st 1], st 2]]
  eta := [0, 1, 2]

reqShow k ∣ shown j.□₀ ∣ hidden k.□₁ ∣ □₂  ⟶  hidden j.□₀ ∣ shown k.□₁ ∣ □₂,    η = [0, 1, 2]

The redex has one region, and its occurrences lie inside main, which holds the views and where the tab places its request. The instantiation is the identity: what each view contains is carried across unchanged, and so are the other views, in site 2. Only the two controls change. The rule freezes the contents of view j, which can no longer react, and thaws those of view k. It is also linear, since η names each site once. Every rule the simulator accepts is (rulesOf_linear), so the linearity condition of the adequacy theorem of Chapter V holds throughout the model.

Here is the rule at work, on a main area cut down to three of the five views. A click is the environment placing a request where the button lives: the vocabulary tab places reqShow .vocab inside main. The model's rules then run in a simulator, BigraphSim, each of whose steps is a reaction of the concrete theory of Chapter IV.

def Certified (a b : BD Ctrl) : Prop :=
  ∃ (I : Face) (ha : a.check S = true) (hb : b.check S = true)
    (hfa : a.Fits Face.origin I) (hfb : b.Fits Face.origin I),
    (BRS (rulesOf (S := S) (fun r => (fun r => rules.contains r) r = true))).React
      (BD.toBigAt Face.origin I a ha hfa) (BD.toBigAt Face.origin I b hb hfb)

def mainArea : BD Miolingo.Ctl := Tm.compile [] [[nd .main []
  [ nd (.shown .practice) []
      [ nd .queue [] [nd .item ["i1", "i2"] [at_ (.word "bonjour")],
          nd .item ["i2", "i3"] [at_ (.word "merci")], at_ .tail ["i3"]],
        at_ .cursor ["i1"], at_ .recorder ],
    nd (.hidden .vocab) [] [at_ (.sort "word"), at_ (.filter "")],
    nd (.hidden .stats) [] [at_ (.query "stats")] ]]]

def clicked : BD Miolingo.Ctl := Miolingo.click mainArea (· == .main) (.reqShow .vocab)

def switchRun : Run.Trace Miolingo.Ctl := Miolingo.go clicked
def switched : BD Miolingo.Ctl := Miolingo.final switchRun

The kernel checks that one reaction fires, that the vocabulary view then shows, and that the run is a chain of certified reactions (Theorem 1):

/-- The click fires one reaction, and the vocabulary view shows. -/
theorem switch_fires : switchRun.fired.length = 1 ∧ Miolingo.showing switched = [.vocab] := by
  decide +kernel
/-- The run is a chain of certified reactions (`Run.run_sound`). -/
theorem switch_certified : Run.Chain (Run.Certified Miolingo.sig Miolingo.rules) switchRun.states :=
  Run.run_sound _ _ 4 _ ⟨by decide +kernel, rfl, rfl⟩

A request inside a passive node is stuck

Activity governs reaction inside a node. Click Next now. Its button is in the practice view, so the request reqNext is placed inside hidden .practice. The rule next has an occurrence there, but the context above it is passive, so it is no reaction (reaction asks for an active context, Chapter II, §2), and no other rule reacts either. The request is not dropped. It stays where it was placed, and it is stuck.

def stuckNext : BD Miolingo.Ctl := Miolingo.click switched (· == .hidden .practice) .reqNext

/-- Next in the hidden view is stuck: no rule reacts, and the matcher says
    why `next` does not. -/
theorem next_stuck : (Match.step Miolingo.sig Miolingo.rules stuckNext).isEmpty = true := by
  decide +kernel
theorem next_blocked : (Match.whyNot Miolingo.sig (fun r => Miolingo.rules.contains r)
    Miolingo.next stuckNext).head? =
    some "a passive control above the match blocks it (the context is not active)" := by
  decide +kernel

The model makes the same check on its full agent, among its scenario checks: Next clicked in the hidden practice view does not fire, the cursor stays on "bonjour", and the matcher gives the same reason, a passive control above the match.

A disabled button is not a passive control

It is tempting to model a greyed-out button as a passive node. That reads activity the wrong way round. A passive control stops reaction among its contents; a disabled button is one whose click nothing would consume. So the model holds no button state at all. A button is enabled exactly when the request it would place has a matching rule, and the matcher computes that from the state. In the explorer (Explore.lean):

/-- **A button is shown enabled when the simulator finds a step** from the
    state with its request placed.  If it is shown enabled, a checked
    reaction consumes the click.  The converse (shown disabled, so no
    reaction of the library consumes it) needs completeness of `stepA`,
    which is not proved (pruned search, family generator).  Presentation
    derived from the rules, not stored in the model. -/
def enabled (clicked : BD Ctl) : Bool := !(stepA envT clicked).isEmpty

Enabledness is presentation, derived from the rules, so it cannot drift from them. The explorer offers only enabled clicks and shows the disabled ones greyed out. It also counts the states it reaches that hold a stuck request, and it reports none. Whether the app's own conditions for disabling a button agree with the model's, button by button, is OPEN; for Previous they agree (docs/miolingo-bigraph.md).

§2 · Data

Miolingo's states carry data: words, recordings, scores and settings. Three facts about bigraphs decide where the data goes.

Values are parameters of controls

A word is not a node holding a string. It is a control with the string as its parameter, so word "merci" and word "bonjour" are two controls, as are score 82 and score 50. The signature is then infinite, and nothing forbids that: a signature, in Chapter I, is given over any type of controls. A redex node matches only a node of the same control, so a redex that holds word w matches only that word.

Families of rules play the part of sums

A rule that reads data is a family indexed by it. Checking a pronunciation is score w a c, one rule for each word w, recording a and language code c. Its reactum holds score s, where s = evalScore w a c is computed by an ordinary Lean function (in the model, a stub standing for the app's evaluator). A set of rules is any predicate on rules, so a family may be infinite. The simulator's rules are the checked members of a family:

def rulesOf {Ctrl : Type} {S : Sig Ctrl} (fam : RuleD Ctrl → Prop) : PRule S → Prop :=
  fun ρ => ∃ (r : RuleD Ctrl) (h : r.check S = true), fam r ∧ ρ = RuleD.toPRule h

This is how value passing reduces to pure CCS. An input a(x).P(x), which may receive any value, stands for the sum Σv av.P(v), with one channel av and one continuation for each value [Mil89]. A family of rules indexed by data is that sum, written as rules. The model's scenarios instantiate each family only at the values they use (captureRules, in §3); spike D1, at the end of that section, generates the instances an agent needs instead.

A redex cannot test absence

A rule applies where its redex occurs (Chapter II, §2). Reaction asks for an occurrence and says nothing about what does not occur: there are no negative application conditions. So “add the word to the vocabulary if it is absent, otherwise count it again” is not one rule. A first attempt used two, one to add and one to bump, and a duplicate row was reachable. That was REFUTED for that rule set, by a kernel-checked run (commit 8e457da). The repair is a rule set that turns absence into something positive, which §3 builds, as Chapter II, §5, did for a toy.

§3 · A table as a list

The rows of the vocabulary table form a list. The table holds a head, its rows, and its schema, the table's permanent component, which ends the list as a sentinel. Each row, an entry, has four ports: its user, its language, self and next. The head's port shares a link with the first row's self, each row's next with the self of the row after it, and the last row's next with the schema. In an empty table the head and the schema share one link.

def table : BD Miolingo.Ctl := Tm.compile [("u", 0), ("fr", 1), ("pt", 2)]
  [[nd .vocabTable [] [at_ .head ["p0"],
      nd .entry ["u", "fr", "p0", "p1"] [at_ (.word "bonjour"), at_ (.seen 1)],
      nd .entry ["u", "pt", "p1", "p2"] [at_ (.word "bonjour"), at_ (.seen 1)],
      at_ .schema ["p2"]]]]

Adding a word to the vocabulary places a scan token at the head. scan w c i carries three keys: the word, the target language's code and the user's id, copied from lang c and user i when the scan starts. Its ports are the user, the language and the position reached. At each row exactly one of three rules applies:

The rules make two kinds of comparison, in two different ways. Equality of links is positive. In scanHit the scan and the row share the names u and l, so the redex occurs only where both are linked to the same user and the same language. Inequality of links cannot be tested at all, since a context may join two outer names of a redex: a redex with distinct names u and u′ also occurs where they are one link. Inequality of keys can be tested, because keys are data. scanSkip is a family whose index carries the keys of both the scan and the row, and the model instantiates it only where they differ:

def scanSkip (w c i w' c' i' : String) : RuleD Ctl where
  redex := Tm.compile [("u", 0), ("l", 1), ("p", 2), ("q", 3), ("u'", 4), ("l'", 5)]
    [ [at_ (.scan w c i) ["u", "l", "p"], nd .entry ["u'", "l'", "p", "q"] [at_ (.word w'), st 0]],
      [at_ (.lang c') ["l'"]],
      [at_ (.user i') ["u'"]] ]
  reactum := Tm.compile [("u", 0), ("l", 1), ("p", 2), ("q", 3), ("u'", 4), ("l'", 5)]
    [ [nd .entry ["u'", "l'", "p", "q"] [at_ (.word w'), st 0], at_ (.scan w c i) ["u", "l", "q"]],
      [at_ (.lang c') ["l'"]],
      [at_ (.user i') ["u'"]] ]
  eta := [0]

def captureRules : List (String × RuleD Ctl) :=
  keys.flatMap fun (w, c, i) =>
    [(s!"add to vocabulary: start the scan ({w}, {c})", captureStart w c i s1),
     (s!"scan: end reached, append ({w}, {c})", scanEnd w c i)] ++
    (List.range seenMax).map (fun k => (s!"scan: found, seen {k + 1} → {k + 2} ({w}, {c})", scanHit w c i (k + 1))) ++
    (keys.filter (· != (w, c, i))).map fun (w', c', i') =>
      (s!"scan: pass {w'} ({c'}) looking for {w} ({c})", scanSkip w c i w' c' i')

That exactly one rule applies at each row rests on one invariant: language codes and user ids are keys. It is a theorem of the model. In every state reachable from the initial agent by checked occurrences of the rules, no two lang nodes share a code and no two user nodes share an id:

theorem keys_invariant {a : BD Ctl} (h : Reach agent0 a) : KeysDistinct a

Its proof counts controls. A checked occurrence never increases the number of controls passing a test beyond what the rule's reactum adds (Occ.countP_result_le, in BigraphSim/Count.lean), and no rule adds a lang or a user. Linearity is used once there: the instance of a parameter keeps each node at most once because η is injective, the condition of Chapter V.

The scenarios are theorems of the model, decided by the kernel. They live in the model's scenario checks, Miolingo/ModelChecks.lean, a module built on demand and not by the generator of this page, so they are stated here in words rather than quoted.

Capturing a word that is already there bumps it, with no choice at any step (capture_again_bumps, PROVED). Capture is clicked again after "bonjour" was captured in French: two reactions fire, then nothing reacts, and the table holds one row, "bonjour" in French, seen twice.

Capturing it again in another language passes the first row, whose code differs, and appends a second (capture_other_language_appends, PROVED). With the target set to Portuguese, three reactions fire, and the table holds two rows, "bonjour" in French and in Portuguese, each seen once.

Two captures at once, two clicks before any reaction, put two scans on the list. Whichever appends first, the other then meets the new row and bumps it. Insertion into a linked list is safe under concurrency, because a scan still behind the sentinel meets whatever another scan appended. Every interleaving ends with one row (concurrent_captures_one_row, PROVED).

The check is bounded. terminals 5 follows every interleaving for at most five reactions. In each state where it stops, the table holds one row, seen twice, and there is more than one such state.

The rows as one value

The other way keeps the rows out of the place graph altogether. One control takes the whole table as its parameter, vocabT rows (spike D1, in Miolingo/D1.lean; the proposal is docs/data-design.md). Capture is then one family over the rows, and its reactum holds vocabT (insertOrBump (w, c, i) rows), for an ordinary function on lists:

def insertOrBump (k : String × String × String) : List Row → List Row
  | [] => [⟨k.1, k.2.1, k.2.2, 1⟩]
  | r :: rs => if r.key = k then { r with seen := r.seen + 1 } :: rs else r :: insertOrBump k rs

No scan is needed, and deduplication becomes a lemma about lists. A general theorem carries any invariant of controls to every step:

theorem preserves (P : Ctrl → Prop)
    (hfam : ∀ r, fam r = true → (∀ c ∈ r.redex.ctrls, P c) → ∀ c ∈ r.reactum.ctrls, P c)
    (hc : o.check S fam a = true) (ha : ∀ c ∈ a.ctrls, P c) : ∀ c ∈ o.result.ctrls, P c

theorem insertOrBump_nodup (k : String × String × String) (rs : List Row)
    (h : (rs.map Row.key).Nodup) : ((insertOrBump k rs).map Row.key).Nodup

theorem dedup_invariant {a : BD Ctl} (h : Reach agentD a) : a.ctrls.all tableKeysDistinct = true

Theorem 3 is stated over reachability by checked occurrences of the family. The same statement over the library's reaction relation needs the converse of the simulator's soundness, that every reaction has a checked certificate, and that is OPEN. The data form has a price: links inside the data become values, so a row's user becomes a user id instead of a link to the user. The proposal chooses between the forms by asking whether a user moves along the structure. The queue and the cursor stay places and links; rows that are only queried or updated as a whole can be data.

The model's main form now keeps its table this way (Miolingo/Main.lean). The table is vocabT rows, capture is the family captureD, and Practise these reads the table. Its own deduplication invariant is PROVED (Main.dedup_invariant), and the explorer runs it. The scan model of this section stays, as the target of D2 below and as the model this chapter quotes.

The two forms are joined by spike D2 (Miolingo/D2.lean). A step of the data form is compiled to a chain of the list form's reactions, a scan, and each compiled run is validated: when validation succeeds, the chain is a chain of certified reactions from the encoding of the first state to the encoding of the second, up to a renumbering of nodes (validate_sound, PROVED). The general simulation, that every step of the data form is matched by reactions of the list form, is OPEN.

§4 · What has been proved

PROVED means sorry-free in Lean, with the axioms checked: every result below rests on propext and Quot.sound only.

§5 · References

1. [Mil89]Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Cited for the reduction of value passing to pure CCS; not among this repository's sources.