Documentation

Linglib.Syntax.Minimalist.Probe.Transmission

Transmission: the Agree state-update on a found goal #

[Cho00] [Dea24]

Probe (Probe/Basic.lean) models the search half of Agree. This file adds the transmission half — what a successful Agree does once a goal is found — realizing the Probe.agreeWith TODO. An Agree operation is a Probe plus a state-update xmit:

Probe.transmit p xmit init goals searches goals; if the probe Agrees with an active goal g, it updates the state via xmit g; otherwise it leaves the state unchanged — Agree fails gracefully, no crash ([Pre14]).

The direction of transmission is the choice of xmit/state, not a separate axis: goal→probe copy (φ-valuation; Agree.applyAgree is recognized as this instance in Agree.lean), probe→goal assignment (dependent case), or sharing. Multiple-goal assignment (a clause's worth of case) is a fold of transmits — the composition axis (cascade/ordered stack), not a single transmit.

source
def Minimalist.Probe.transmit {α : Type u_1} {σ : Type u_2} (p : Probe α) (xmit : α → σ → σ) (init : σ) (goals : List α) :
σ

An Agree operation: search (Probe) + a transmission xmit applied to the active goal it finds. No active goal ⇒ state unchanged (graceful failure).

Equations
  • p.transmit xmit init goals = (p.agree goals).elim init fun (g : α) => xmit g init
Instances For
    source
    @[simp]
    theorem Minimalist.Probe.transmit_nil {α : Type u_1} {σ : Type u_2} {p : Probe α} {xmit : α → σ → σ} {init : σ} :
    p.transmit xmit init [] = init
    source
    theorem Minimalist.Probe.transmit_eq_init_of_agree_none {α : Type u_1} {σ : Type u_2} {p : Probe α} {xmit : α → σ → σ} {init : σ} {goals : List α} (h : p.agree goals = none) :
    p.transmit xmit init goals = init

    Agree fails gracefully: with no goal to value the probe, the state is left unchanged ([Pre14] — failure to Agree does not crash).

    source
    theorem Minimalist.Probe.transmit_eq_init_of_inactive {α : Type u_1} {σ : Type u_2} {p : Probe α} {xmit : α → σ → σ} {init : σ} {goals : List α} {a : α} (hs : p.search goals = some a) (ha : p.act a = false) :
    p.transmit xmit init goals = init

    An inactive closest goal absorbs the probe without transmission ([Dea24]: satisfaction without interaction).

    source
    theorem Minimalist.Probe.transmit_eq_of_agree {α : Type u_1} {σ : Type u_2} {p : Probe α} {xmit : α → σ → σ} {init : σ} {goals : List α} {a : α} (h : p.agree goals = some a) :
    p.transmit xmit init goals = xmit a init

    When the probe Agrees with a, transmission applies xmit a to the state.