locus: Blueprint

8.1. The signature and its rules🔗

Definition8.1.1
uses 0
Used by 3
Reverse dependency previews
Preview
Definition 8.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsfrom sourcenew

The controls of the trainer: on the server the language catalogue with a node \mathsf{lang}\,c for each language code, the user table with a node \mathsf{user}\,i for each user id, the vocabulary table and the attempt store; in a session the owner, the settings, the five views (each either \mathsf{shown}\,v, active, or \mathsf{hidden}\,v, passive), the practice queue, the recorder and the result; and one request control for each user action. Data are parameters of controls, so the signature is infinite and a rule that touches data is a family indexed by it.

Class: Ctl FROM SOURCE; sig NEW.

Lean code for Definition8.1.1●2 definitions
  • inductive(91 constructors)defined in Miolingo/Sig.lean
    complete
    inductive Ctl : Type
    inductive Ctl : Type
    **The controls.**

    Constructors

    catalogue : Ctl
    The language catalogue; a language by code (port: the language). 
    lang (code : String) : Ctl
    users : Ctl
    The user table; a registered user, by id (port: the user); a guest. 
    user (id : String) : Ctl
    guest : Ctl
    vocabTable : Ctl
    The vocabulary table and its rows (`owner`, `lang`, `self`, `next`):
the rows form a list, from `head` to the table's `schema`. 
    entry : Ctl
    vocabT (rows : List Row) : Ctl
    Spike D1: the vocabulary table as ONE control whose parameter is its
rows (data structure, not navigational structure). 
    progressTable : Ctl
    The attempt store (`user_progress`) and its rows (`owner`, `lang`). 
    attempt : Ctl
    schema : Ctl
    A table's column definitions: the permanent component of a table.
Its port is the end of the table's row list (the sentinel). 
    head : Ctl
    The start of a table's row list (port: the first row, or the
`schema` when there is none). 
    scan (w c i : String) : Ctl
    A scan of the vocabulary list for the word `w` in the language with
code `c` for the user with id `i` (ports: the user, the language, the
position reached).  `c` and `i` are keys copied from `lang c` and
`user i` when the scan starts. 
    word (w : String) : Ctl
    gloss (t : String) : Ctl
    ipa (p : String) : Ctl
    seen (n : Nat) : Ctl
    said (w : String) : Ctl
    heard (a : String) : Ctl
    score (s : Nat) : Ctl
    owner : Ctl
    Whose session this is (port: the user). 
    sidebar : Ctl
    The sidebar, holding the helm: the language pair and the voice. 
    helm : Ctl
    source : Ctl
    The source and target languages (port: the language). 
    target : Ctl
    tts (engine : String) : Ctl
    The TTS engine and the espeak speed. 
    speed (wpm : Nat) : Ctl
    main : Ctl
    The main area, holding the five views. 
    shown (v : View) : Ctl
    A view, showing (active) or hidden (passive). 
    hidden (v : View) : Ctl
    queue : Ctl
    The practice queue; a phrase (`self`, `next`); the end of the queue
(port: the last phrase's `next`). 
    item : Ctl
    tail : Ctl
    cursor : Ctl
    The current phrase (port: the phrase). 
    queueD (ws : List String) (i : Nat) : Ctl
    **The practice queue as data** (app model): the phrases in order and
the index of the current one.  The `cursor` beside it keeps the link
that the recording and the verdict share. 
    langSel (srcs tgts : List String) (s c : String) : Ctl
    **The language settings of a session as data** (app model): the
ordered lists of the languages on offer as source and as target, and
the source code `s` and target code `c` in force.  The two lists are
the app's (`src/config.py:165` `SOURCE_LANGUAGE_OPTIONS`, and the
codes of `LANGUAGE_CONFIG`, `src/config.py:25`), which hold the same
languages in different orders. 
    sess (srcs tgts : List String) (s c v : String) : Ctl
    **A session, with its settings as data** (prototype of the flat
model, `Miolingo/Flat.lean`; not used by the family `App.famA`): the
language options and settings of `langSel`, and the voice `v`.  A
container: the views are its children.  Port: the user. 
    sessN (p : Prefs) : Ctl
    **A session, normalised** (second prototype, `Miolingo/Flat.lean`):
the settings `p`, among them the user's id as a key; no port. 
    progressE (rows : List Att) : Ctl
    **The progress table as data** (second prototype): one row per
attempt, `(user id, language code, target, heard, exact, num, den)`,
as `user_progress` holds them: the user by key, the language as a
plain column. 
    reqTargetD (c : String) : Ctl
    Second prototype: choose the target, or the source, language `c`. 
    reqSourceD (c : String) : Ctl
    reqEngineD (e : String) : Ctl
    Normalised model: choose the speech engine, the voice, the speed, slow speech. 
    reqVoiceD (v : String) : Ctl
    reqSpeedD (wpm : Nat) : Ctl
    reqSlowD (on : Bool) : Ctl
    recorder : Ctl
    The recorder of the practice view: its permanent component (atomic;
recordings sit beside it, each linked to its phrase). 
    audioIn : Ctl
    The main model's recorder (`Miolingo.Main`): a container that always
holds exactly one thing, the current recording or `noAudio`, so that
Record REPLACES the recording without testing for absence. 
    noAudio : Ctl
    recording (audio : String) : Ctl
    A recording and a score, each linked to the phrase it is FOR. 
    result (s : Nat) : Ctl
    voice (v : String) : Ctl
    **The app model** (`Miolingo.App`, increment M1, 2026-10-09).  The
espeak voice of the helm (`settings['voice']`, `sidebar.py:365`); the
result area, a container holding exactly one thing, the verdict or
`noVerdict` (as `audioIn` does for the recording); a verdict, linked
to the phrase it is FOR: exact or not, the similarity `num/den`, and
the edit distance (`compare_phonemes_edit_distance`); and two fields
of an attempt row (`user_progress.perfect_match`, `similarity_score`). 
    resultIn : Ctl
    noVerdict : Ctl
    verdict (exact : Bool) (num den dist : Nat) : Ctl
    exact (b : Bool) : Ctl
    sim (num den : Nat) : Ctl
    vocabE (t : Table) : Ctl
    **M2**: the vocabulary table as the app stores it; an entry being
edited (by key); the vocabulary view's requests (sort, search,
delete, notes, edit, cancel, save, auto-fill). 
    editing (w : String) : Ctl
    reqSort (k : String) : Ctl
    reqSearch (q : String) : Ctl
    reqDelete (w : String) : Ctl
    reqNotes (w n : String) : Ctl
    reqEdit (w : String) : Ctl
    reqCancelEdit (w : String) : Ctl
    reqSave (w : String) (f : EditForm) : Ctl
    reqAutofill (w : String) : Ctl
    reqPaste (passage w label url : String) : Ctl
    **M2b**: "Add from passage" (`vocabulary_tab.py:105`) with the
passage, the word, the source label and the URL as typed; "Import
file" (`vocabulary_tab.py:165`) with the file's contents and the
auto-fetch checkbox. 
    reqImport (contents : String) (enrich : Bool) : Ctl
    pastePanel : Ctl
    The vocabulary view's "Paste a passage" panel
(`vocabulary_tab.py:86`): its permanent component, so the rest of
the view is never empty. 
    materials : Ctl
    The practice view's "Load Practice Materials" panel
(`quick_practice_tab.py:49`): its permanent component (Matthew,
2026-10-09), so "the rest of the view" is never empty and a stray
request cannot block a rule that matches the view. 
    reqAddWord (w : String) : Ctl
    "Add a word" under a result for a target of several words
(`practice_tab.py:226-233`), carrying the typed word. 
    sort (key : String) : Ctl
    The vocabulary view's settings. 
    filter (q : String) : Ctl
    reader : Ctl
    The story view's reader: scene and mode. 
    scene (n : Nat) : Ctl
    mode (m : String) : Ctl
    query (name : String) : Ctl
    What the statistics and history views present (a query on the
attempt store). 
    reqShow (v : View) : Ctl
    reqSource : Ctl
    reqTarget : Ctl
    reqTts (engine : String) : Ctl
    reqSpeed (wpm : Nat) : Ctl
    reqNext : Ctl
    reqPrev : Ctl
    reqRecord (audio : String) : Ctl
    reqClearRec : Ctl
    reqScore : Ctl
    reqCapture : Ctl
    reqAppend (w t p : String) : Ctl
    reqClearQueue : Ctl
    reqGoPractice : Ctl
    "Practise these" in the vocabulary view (`vocabulary_tab.py:555-581`).
  • defdefined in Miolingo/Sig.lean
    complete
    def sig : Sig Ctl
    def sig : Sig Ctl
    **The Miolingo signature.**
Definition8.1.2
uses 1
Used by 2
Reverse dependency previews
Preview
Definition 8.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbridgedunbridgednew

For a rule family F, write a \Rightarrow_F b when b is reachable from a by checked steps: each step is the result of an occurrence of a rule of F that passes the simulator's occurrence checker. The families are F_0 (the first model, in which the vocabulary is a linked list of rows scanned for a duplicate), F_D (the vocabulary table as one control \mathsf{vocabT}\,\mathit{rows}), F_M (the main model) and F_A(E) (the app model).

A user action is NOT a step of \Rightarrow_F. Every rule's redex holds a request or a scan control and no start agent holds one, so nothing is reachable by \Rightarrow_F from a start agent but the start agent itself. The invariants below are therefore stated over reachability with user actions, Definition 8.1.3.

Class: Keys.Reach, Main.Reach, ReachA UNBRIDGED and NEW; D1.Reach BRIDGED and NEW.

Lean code for Definition8.1.2●4 definitions
  • inductive(2 constructors, Prop, 2 parameters)defined in Miolingo/Keys.lean
    complete
    inductive Reach : BD Ctl → BD Ctl → Prop
    inductive Reach : BD Ctl → BD Ctl → Prop
    Reachability by checked steps.

    Constructors

    refl (a : BD Ctl) : Keys.Reach a a
    tail {a b c : BD Ctl} :
  Keys.Reach a b → MStep b c → Keys.Reach a c
  • inductive(2 constructors, Prop, 2 parameters)defined in Miolingo/D1.lean
    complete
    inductive Reach : BD Ctl → BD Ctl → Prop
    inductive Reach : BD Ctl → BD Ctl → Prop
    Reachability by checked steps.

    Constructors

    refl (a : BD Ctl) : D1.Reach a a
    tail {a b c : BD Ctl} :
  D1.Reach a b → CStep b c → D1.Reach a c
  • inductive(2 constructors, Prop, 2 parameters)defined in Miolingo/Main.lean
    complete
    inductive Reach : BD Ctl → BD Ctl → Prop
    inductive Reach : BD Ctl → BD Ctl → Prop
    Reachability by checked steps of the family.

    Constructors

    refl (a : BD Ctl) : Main.Reach a a
    tail {a b c : BD Ctl} :
  Main.Reach a b → CStepM b c → Main.Reach a c
  • inductive(2 constructors, Prop, 3 parameters)defined in Miolingo/AppInv.lean
    complete
    inductive ReachA (E : App.Env) : BD Ctl → BD Ctl → Prop
    inductive ReachA (E : App.Env) :
  BD Ctl → BD Ctl → Prop
    Reachability by checked steps of the family.

    Constructors

    refl {E : App.Env} (a : BD Ctl) : ReachA E a a
    tail {E : App.Env} {a b c : BD Ctl} :
  ReachA E a b → CStepA E b c → ReachA E a c
Definition8.1.3
uses 1
Used by 6
Reverse dependency previews
Preview
Theorem 8.2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsunbridgednew

NEW (no counterpart in the sources). A user action a \rightsquigarrow b holds when b is a with exactly one new node, whose control is a request control, under any parent and with any port links, and b passes the check of well-formedness. This is any well-formed request, anywhere: a request inside a hidden view is a user action, and several requests may be pending at once, so it over-approximates what a user can do. Write a \Rightarrow^{\mathsf u}_F b for the least relation closed under checked steps of F and user actions.

UNBRIDGED: a user action is an edit of the data. No theorem relates it to a labelled transition of the library or to composition with a context; that is OPEN. A click of the explorer is a user action when it finds its place and its result is well formed (click_act, clickR_act), and not conversely. The results below are about data and checked occurrences, not about the library's reachability.

Class: Miolingo.isRequest, Miolingo.ReachU NEW; Miolingo.Act UNBRIDGED and NEW.

Lean code for Definition8.1.3●3 definitions
  • defdefined in Miolingo/Act.lean
    complete
    def isRequest : Ctl → Bool
    def isRequest : Ctl → Bool
    **The request controls** (NEW): what the environment may place.  `scan`
is not one: only rules create it.
  • defdefined in Miolingo/Act.lean
    complete
    def Act (a b : BD Ctl) : Prop
    def Act (a b : BD Ctl) : Prop
    **A user action** (NEW; UNBRIDGED to the library): `b` is `a` with
exactly one new request node, under any parent `p` and with any port
links `ls`, and `b` passes the check.  Any well-formed request,
anywhere; an over-approximation of what a user can do.
  • inductive(3 constructors, Prop, 3 parameters)defined in Miolingo/Act.lean
    complete
    inductive ReachU (step : BD Ctl → BD Ctl → Prop) : BD Ctl → BD Ctl → Prop
    inductive ReachU (step : BD Ctl → BD Ctl → Prop) :
  BD Ctl → BD Ctl → Prop
    **Reachability with user actions** (NEW), for a step relation `step`:
closed under `step` and under `Act`.

    Constructors

    refl {step : BD Ctl → BD Ctl → Prop} (a : BD Ctl) :
  ReachU step a a
    react {step : BD Ctl → BD Ctl → Prop} {a b c : BD Ctl} :
  ReachU step a b → step b c → ReachU step a c
    act {step : BD Ctl → BD Ctl → Prop} {a b c : BD Ctl} :
  ReachU step a b → Act b c → ReachU step a c
Theorem8.1.4
uses 0used by 0✓L∃∀N

Every parametric rule that the simulator derives from a rule family F is linear, so every rule of every model in this chapter is: its map \eta from reactum sites to redex sites is injective,

\rho \in \mathrm{rulesOf}(F) \;\Longrightarrow\; \forall i\, j.\;\; \eta_\rho(i) = \eta_\rho(j) \Rightarrow i = j .

Rests on NEW: rulesOf; not audited: PRule.Linear.

Lean code for Theorem8.1.4●1 theorem
  • theoremdefined in BigraphSim/Rule.lean
    complete
    theorem rulesOf_linear {Ctrl : Type} {S : Sig Ctrl} {fam : RuleD Ctrl → Prop}
  {ρ : PRule S} (h : rulesOf fam ρ) : ρ.Linear
    theorem rulesOf_linear {Ctrl : Type}
  {S : Sig Ctrl} {fam : RuleD Ctrl → Prop}
  {ρ : PRule S} (h : rulesOf fam ρ) :
  ρ.Linear
    **The standing rule, discharged: every rule of a BigraphSim family is
linear.**