locus: Blueprint

8.5. Two models: the present one and the normalised one🔗

There are two models of the app. Everything above this section is about the PRESENT model. The NORMALISED model (Miolingo/Flat.lean, namespace Flat.N; ActN.lean, ShapeN.lean) stands beside it and does not replace it: each session is one node carrying its settings as data, and the data follow the app's database schema (the user by key, a language as a value, the tables as rows). The two were run in lockstep on the one-user graph (6,500 pairs of states) and the two-user graph (1,800 pairs), both cut at that bound, with no difference in the screen, the enabled flags, the number of rules fired or the data (TESTED by compiled evaluation). Since the normalised model was given the engine, voice and speed settings and the voice reset on a change of target, which the present model does not have, the comparison is made on the widgets both models have, and still passes. The nodes that follow are about the NORMALISED model only; nothing in them is claimed of the present model.

Definition8.5.1
Statement uses 3
Statement dependency previews
Preview
Definition 6.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Definition 8.5.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsnew

NORMALISED model. A session's settings p are a record: the user id, the source and target options, the chosen source, target and voice, the engine, the speed and the slow-speech choice. For an outside world E and a configuration g (rows of the vocabulary sorted or in order; one option order or the app's two), F^N_{E,g} is the family of rules, and a \to^N b holds when some occurrence of F^N_{E,g} passes its check on a and has result b. A user action a \leadsto^N b adds to a one request node of this model, under any parent and with any links, the result passing its check. Reachability \Rightarrow^{\mathsf u}_N is the reflexive and transitive closure of the two together. The start agents are a_N (one user) and a_{2N} (two users). As for the present model (Definition 8.1.3), a user action is not related to a transition of the library.

Lean code for Definition8.5.1●8 definitions
  • abbrevdefined in Miolingo/Flat.lean
    complete
    abbrev Prefs : Type
    abbrev Prefs : Type
    The settings of a session (`Miolingo.Prefs`, in the signature).
  • structure(2 fields)defined in Miolingo/Flat.lean
    complete
    structure Cfg : Type
    structure Cfg : Type
    **The choices still open** (questions 3 and 5 of
`docs/miolingo-normalised.md`), so that either answer costs no rework.
* `sortedRows`: the progress table is kept sorted (a multiset, as the
  present model's attempt nodes are); otherwise a new row is appended
  (the order of the attempts is kept, as the app keeps it).
* `appOrders`: the screen lists the source options in the order of
  `srcs` and the target options in the order of `tgts`, as the app
  does; otherwise both in one fixed order.
Question 4 (dropping the cursor's link) is NOT built: `recording` and
`verdict` have a port in the signature, shared with the older models.

    Fields

    sortedRows : Bool
    appOrders : Bool
  • defdefined in Miolingo/Flat.lean
    complete
    def famN (E : App.Env) (g : Flat.N.Cfg) (r : RuleD Ctl) : Bool
    def famN (E : App.Env) (g : Flat.N.Cfg)
  (r : RuleD Ctl) : Bool
  • defdefined in Miolingo/Flat.lean
    complete
    def agentN : BD Ctl
    def agentN : BD Ctl
  • defdefined in Miolingo/Flat.lean
    complete
    def agent2N : BD Ctl
    def agent2N : BD Ctl
  • defdefined in Miolingo/ActN.lean
    complete
    def CStepN (E : App.Env) (g : Flat.N.Cfg) (a b : BD Ctl) : Prop
    def CStepN (E : App.Env) (g : Flat.N.Cfg)
  (a b : BD Ctl) : Prop
    **A checked step of the normalised family.**
  • defdefined in Miolingo/ActN.lean
    complete
    def ActN (a b : BD Ctl) : Prop
    def ActN (a b : BD Ctl) : Prop
    **A user action** (UNBRIDGED to the library, as `Miolingo.Act`): `b` is
`a` with exactly one new request node of this model, under any parent
and with any port links, and `b` passes the check.
  • inductive(3 constructors, Prop, 3 parameters)defined in Miolingo/ActN.lean
    complete
    inductive ReachUN (step : BD Ctl → BD Ctl → Prop) : BD Ctl → BD Ctl → Prop
    inductive ReachUN (step : BD Ctl → BD Ctl → Prop) :
  BD Ctl → BD Ctl → Prop
    **Reachability with user actions**, for a step relation `step`.

    Constructors

    refl {step : BD Ctl → BD Ctl → Prop} (a : BD Ctl) :
  Flat.N.ReachUN step a a
    react {step : BD Ctl → BD Ctl → Prop} {a b c : BD Ctl} :
  Flat.N.ReachUN step a b →
    step b c → Flat.N.ReachUN step a c
    act {step : BD Ctl → BD Ctl → Prop} {a b c : BD Ctl} :
  Flat.N.ReachUN step a b →
    Flat.N.ActN b c → Flat.N.ReachUN step a c
Definition8.5.2
uses 1used by 1✓L∃∀N
Tagsnew

NORMALISED model. The state invariant \mathrm{stateOk}(d) is the conjunction of four decidable conditions on a description d:

  • W1: every node that is not a request sits in one of the places its control allows;

  • W2: the server has one of each of its parts, and every session is one session node with one of each of its parts, one audio content, one result content, each view once, and exactly one view shown;

  • P1: every session's settings are well formed (source and target are options and differ, the engine is an engine, the voice is on offer for the target and the engine, and every target option has a voice for every engine);

  • U1: every session's user id is the id of a user node.

Lean code for Definition8.5.2●6 definitions
  • defdefined in Miolingo/ShapeN.lean
    complete
    def W1 (d : BD Ctl) : Bool
    def W1 (d : BD Ctl) : Bool
    W1: every node that is not a request sits in one of its homes.
  • defdefined in Miolingo/ShapeN.lean
    complete
    def W2 (d : BD Ctl) : Bool
    def W2 (d : BD Ctl) : Bool
    W2: the server has one of each of its parts; every session is one
session node with one of each of its parts, one audio content, one
result content, each view once, and exactly one view shown.
  • defdefined in Miolingo/ShapeN.lean
    complete
    def P1 (d : BD Ctl) : Bool
    def P1 (d : BD Ctl) : Bool
    P1: every session's settings are well formed.
  • defdefined in Miolingo/ShapeN.lean
    complete
    def U1 (d : BD Ctl) : Bool
    def U1 (d : BD Ctl) : Bool
    U1: every session's user id is the id of a user node.
  • defdefined in Miolingo/ShapeN.lean
    complete
    def stateOk (d : BD Ctl) : Bool
    def stateOk (d : BD Ctl) : Bool
    All the state invariants in force.
  • defdefined in Miolingo/ShapeN.lean
    complete
    def prefsOk (p : Flat.N.Prefs) : Bool
    def prefsOk (p : Flat.N.Prefs) : Bool
    Well-formed settings: source and target are options and differ, and
each has another option to reset to; the engine is one of the engines;
the voice is on offer for the target and the engine (P2); and every
target option has a voice for every engine, so that a reset always
finds one.
Theorem8.5.3
uses 1used by 0✓L∃∀N

NORMALISED model. The state invariant holds along reachability by checked reactions and user actions, from both start agents, for every outside world E and configuration g, with no hypothesis on the rules; the user actions allowed are any request placed anywhere, which is wider than what the screen offers:

a_N \Rightarrow^{\mathsf u}_N a \;\Longrightarrow\; \mathrm{stateOk}(a) , \qquad a_{2N} \Rightarrow^{\mathsf u}_N a \;\Longrightarrow\; \mathrm{stateOk}(a) .

In particular every reachable session shows exactly one view. The corresponding statements for the present model are CONDITIONAL (Theorem 8.4.5).

Rests on NEW: Env, Flat.N.CStepN, Flat.N.Cfg, Flat.N.ReachUN, Flat.N.agent2N, Flat.N.agentN, ShapeN.stateOk.

Lean code for Theorem8.5.3●2 theorems
  • theoremdefined in Logic/MiolingoCountN3.lean
    complete
    theorem stateOk_agentN (E : App.Env) (g : Flat.N.Cfg) {a : BD Ctl}
  (h : Flat.N.ReachUN (Flat.N.CStepN E g) Flat.N.agentN a) :
  ShapeN.stateOk a = true
    theorem stateOk_agentN (E : App.Env)
  (g : Flat.N.Cfg) {a : BD Ctl}
  (h :
    Flat.N.ReachUN (Flat.N.CStepN E g)
      Flat.N.agentN a) :
  ShapeN.stateOk a = true
    **`stateOk` along reachability from the one-user start agent.**
  • theoremdefined in Logic/MiolingoCountN3.lean
    complete
    theorem stateOk_agent2N (E : App.Env) (g : Flat.N.Cfg) {a : BD Ctl}
  (h : Flat.N.ReachUN (Flat.N.CStepN E g) Flat.N.agent2N a) :
  ShapeN.stateOk a = true
    theorem stateOk_agent2N (E : App.Env)
  (g : Flat.N.Cfg) {a : BD Ctl}
  (h :
    Flat.N.ReachUN (Flat.N.CStepN E g)
      Flat.N.agent2N a) :
  ShapeN.stateOk a = true
    **`stateOk` along reachability from the two-user start agent.**
Theorem8.5.4
uses 1used by 0✓L∃∀N

NORMALISED model (S1N). The ids and kinds of the widgets of a screen, the rows of the vocabulary listing apart, depend only on whether the engine is espeak and on which views are shown. For every description d and region r whose session node has settings p,

\mathrm{kinds}(\mathrm{render}^N_{E,g}(d, r)) \;=\; \mathrm{top}^N(p.\mathrm{engine} = \mathtt{espeak},\; \mathrm{shown}(d, r)) .

This holds of every description, reachable or not.

Rests on NEW: Env, Flat.N.Cfg, Flat.N.Prefs, Flat.N.prefsOf, Flat.N.readSessN, Flat.N.renderN, Flat.N.topKindsN, Prefs and 5 more; not audited: UI.flatL, View.

Lean code for Theorem8.5.4●4 declarations
  • theoremdefined in Logic/MiolingoS1N.lean
    complete
    theorem s1N (E : App.Env) (g : Flat.N.Cfg) (d : BD Ctl) (r : Nat)
  (p : Flat.N.Prefs) (h : Flat.N.prefsOf d r = some p) :
  UI.flatL (Flat.N.renderN E g d r) =
    Flat.N.topKindsN (p.engine == "espeak") (Flat.N.readSessN d r).shown
    theorem s1N (E : App.Env) (g : Flat.N.Cfg)
  (d : BD Ctl) (r : Nat)
  (p : Flat.N.Prefs)
  (h : Flat.N.prefsOf d r = some p) :
  UI.flatL (Flat.N.renderN E g d r) =
    Flat.N.topKindsN
      (p.engine == "espeak")
      (Flat.N.readSessN d r).shown
    **S1 for N.** The ids and kinds of the widgets of the screen of a
session with settings `p`, rows apart: the settings (with the speed
when the engine is espeak, the slow-speech choice otherwise), then the
shown views.
  • defdefined in Miolingo/Flat.lean
    complete
    def renderN (E : App.Env) (g : Flat.N.Cfg) (d : BD Ctl) (r : Nat) :
  UI.Screen
    def renderN (E : App.Env) (g : Flat.N.Cfg)
  (d : BD Ctl) (r : Nat) : UI.Screen
    The screen of session `r`.  The engine and the voice are choices; the
speed is an input shown only with espeak, slow speech a switch shown
only otherwise (`src/ui/sidebar.py:343-360`).  Pitch, the Whisper
model size and the scoring algorithm are not modelled: nothing modelled
reads them.  With `g.appOrders` the two choices list
the settings' own option lists; otherwise both list `langsShown`.
  • defdefined in Miolingo/Flat.lean
    complete
    def topKindsN (espeak : Bool) (shown : List View) : List (String × UI.Kind)
    def topKindsN (espeak : Bool)
  (shown : List View) :
  List (String × UI.Kind)
    **The widgets of a screen** (S1 for this model, two cases): the
settings, with the speed when the engine is espeak and the slow-speech
choice otherwise; then the shown view as in `UI.topKinds`.
  • defdefined in Miolingo/Flat.lean
    complete
    def prefsOf (d : BD Ctl) (r : Nat) : Option Flat.N.Prefs
    def prefsOf (d : BD Ctl) (r : Nat) :
  Option Flat.N.Prefs