diff --git a/AGENTS.md b/AGENTS.md index fd4b2b3..5b2a195 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -76,6 +76,16 @@ and depend on this library. (interfaces, par, wire, plug), corruption models, environment actions, leakage. *Generic only* — security-flavored UC layers (computational equivalence, asymptotic security) live in VCVio. +- `PolyFun/Realizability/`: step classes (`StepClass` — a wide subcategory of + `Type u` presented by a representation structure on types and an + admissibility predicate on functions; with products, sums and distributivity + it is exactly a distributive category) and realizability of `FreeM` program + families by `DynComputation` machines whose first-order step maps are + admissible. Closed under `ofFn`, input precomposition, result + postcomposition, `bind`, interface transport, and class refinement. + Instances: unconstrained, finite-state, Mathlib-`Computable`, and a bridge + from any class of word functions. *Generic only* — cost measures and + concrete complexity classes live downstream. - `PolyFun/Control/`: monad and comonad infrastructure transitively required by the above (coalgebra, comonad, free / freecont monad algebra, monad iter / hom, lawful re-exports). @@ -228,6 +238,8 @@ too specific or too changeable to keep at the repo root. - [`docs/wiki/itree.md`](docs/wiki/itree.md): interaction trees layer. - [`docs/wiki/interaction.md`](docs/wiki/interaction.md): generic interaction framework (`TypeTree`, two-party, multiparty, concurrent, UC). +- [`docs/wiki/realizability.md`](docs/wiki/realizability.md): step classes and + realizability of free programs by admissible state machines. - [`docs/wiki/notation.md`](docs/wiki/notation.md): notation reference (UC composition operators). - [`docs/wiki/gotchas.md`](docs/wiki/gotchas.md): recurring traps and diff --git a/PolyFun.lean b/PolyFun.lean index 55153ac..21000fc 100644 --- a/PolyFun.lean +++ b/PolyFun.lean @@ -223,3 +223,8 @@ public import PolyFun.PFunctor.SubstMonoid.Extension public import PolyFun.PFunctor.Trace public import PolyFun.PFunctor.Wiring public import PolyFun.PFunctor.Wiring.Parallel +public import PolyFun.Realizability.Basic +public import PolyFun.Realizability.Closure +public import PolyFun.Realizability.Instances +public import PolyFun.Realizability.Machine +public import PolyFun.Realizability.StepClass diff --git a/PolyFun/PFunctor/Bound.lean b/PolyFun/PFunctor/Bound.lean index 2c5db7f..0fd5c12 100644 --- a/PolyFun/PFunctor/Bound.lean +++ b/PolyFun/PFunctor/Bound.lean @@ -31,7 +31,7 @@ witnesses the equivalence by `Iff.rfl`. @[expose] public section -universe v w uA uB +universe v w uA uB uA₂ uB₂ namespace PFunctor.FreeM @@ -240,4 +240,18 @@ lemma isTotalRollBound_seq {og : FreeM P (α → β)} {oa : FreeM P α} IsTotalRollBound (og <*> oa) (n₁ + n₂) := by refine isRollBound_seq (fun a b => a + b) ?_ ?_ h₁ h₂ <;> grind +/-- Interface transport along a lens preserves total roll bounds. A lens relabels +positions and reindexes directions, leaving the branching structure — and hence the +number of rolls along each branch — untouched. -/ +lemma isTotalRollBound_mapLens {Q : PFunctor.{uA₂, uB₂}} (l : Lens P Q) + (oa : FreeM P α) {n : ℕ} (h : oa.IsTotalRollBound n) : + (oa.mapLens l).IsTotalRollBound n := by + induction oa generalizing n with + | pure x => simp + | lift_bind a cont ih => + rw [isTotalRollBound_lift_bind_iff] at h + rw [FreeM.mapLens_lift_bind, FreeM.liftBind_eq, + isTotalRollBound_lift_bind_iff] + exact ⟨h.1, fun d => ih _ (h.2 _)⟩ + end PFunctor.FreeM diff --git a/PolyFun/PFunctor/Dynamical/DynComputation.lean b/PolyFun/PFunctor/Dynamical/DynComputation.lean index 1b9b515..d558c10 100644 --- a/PolyFun/PFunctor/Dynamical/DynComputation.lean +++ b/PolyFun/PFunctor/Dynamical/DynComputation.lean @@ -170,6 +170,32 @@ def contramapInput {γ : Type uγ} (M : DynComputation.{u} p α β) (f : γ → (M : DynComputation.{u} p α β) (input : γ) : (M.contramapInput f).denote input = M.denote (f input) := rfl +/-- Replace a returning computation's initialization map, possibly changing the +input type, while keeping its dynamics untouched. Reducible so that the state +type, one-step views, and behaviors of `M.setInit g` reduce to those of `M`: +computations sharing `toMachine` share every derived step map definitionally. -/ +@[reducible] def setInit {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) : DynComputation.{u} p γ β := + ⟨M.toMachine, g⟩ + +@[simp] theorem setInit_State {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) : (M.setInit g).State = M.State := rfl + +@[simp] theorem setInit_init {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (input : γ) : (M.setInit g).init input = g input := rfl + +@[simp] theorem setInit_view {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (state : M.State) : + (M.setInit g).view state = M.view state := rfl + +@[simp] theorem setInit_denote {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (input : γ) : + (M.setInit g).denote input = M.toDynSystem.behavior (g input) := rfl + +/-- Reindexing inputs is exactly precomposing the initialization map. -/ +theorem contramapInput_eq_setInit {γ : Type uγ} (M : DynComputation.{u} p α β) + (f : γ → α) : M.contramapInput f = M.setInit (M.init ∘ f) := rfl + private def mapResultLift {γ : Type uγ} (f : β → γ) : Lens.{max uβ uA, uB, max uγ uA, uB} (C.{uβ, uB} β + p) (C.{uγ, uB} γ + p) := @@ -660,6 +686,36 @@ theorem seqComp_ofFn_obsEq {γ : Type uγ} (M : DynComputation.{u} p α β) funext value exact denote_ofFn f value +/-! ## Realizations from a raw step function -/ + +/-- Realize a returning computation from a one-step transition — returning either +a value or a visible query with an explicit state-valued continuation — together +with an initialization. + +This is the primary constructor for a hand-built machine: the supplied step +function is exactly what `view` reads back, so no repackaging is visible to the +caller. Reducible, so the state type and one-step views of a computation built +this way are transparently those of the supplied data. -/ +@[reducible] def ofStep {S : Type u} (stepFn : S → β ⊕ p.Obj S) (init : α → S) : + DynComputation.{u} p α β where + State := S + toDynSystem := + (fun state => (Resumption.pack (β := β) (stepFn state)).1) ⇆ + fun state => (Resumption.pack (β := β) (stepFn state)).2 + init := init + +@[simp] theorem ofStep_State {S : Type u} (stepFn : S → β ⊕ p.Obj S) + (init : α → S) : (ofStep (p := p) stepFn init).State = S := rfl + +@[simp] theorem ofStep_init {S : Type u} (stepFn : S → β ⊕ p.Obj S) + (init : α → S) (input : α) : + (ofStep (p := p) stepFn init).init input = init input := rfl + +@[simp] theorem view_ofStep {S : Type u} (stepFn : S → β ⊕ p.Obj S) + (init : α → S) (state : S) : + (ofStep (p := p) stepFn init).view state = stepFn state := + Resumption.unpack_pack (stepFn state) + /-! ## Resumption realizations -/ /-- Realize a family of resumptions directly, using the resumption itself as diff --git a/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean b/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean index 5a3e1ab..5f05c81 100644 --- a/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean +++ b/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean @@ -29,7 +29,7 @@ bridges inherit their existing `Classical.choice` footprint. @[expose] public section -universe u v uA uB uα uβ uγ +universe u v uA uB uA₂ uB₂ uα uβ uγ namespace PFunctor @@ -127,6 +127,93 @@ theorem isTotalRollBound_unroll (M : DynComputation.{u} p α β) rw [unroll_eq_truncate] exact Resumption.isTotalRollBound_truncate k (M.toDynSystem.behavior state) +/-! ## Transport of bounded unrolling + +Bounded unrolling commutes with each of the three reindexings of a returning +computation: replacing the initialization leaves it untouched, mapping the +returned value maps the optional result, and interface transport along a lens +transports the resulting syntax along the same lens. + +Each proof is a fuel induction rather than a definitional equality, because +`unroll` is defined by cases on the computation's one-step view and so does not +reduce until that view is exposed. +-/ + +/-- Replacing the initialization map leaves bounded unrolling from a hidden state +unchanged: the two computations share `toMachine`, hence share their views. -/ +theorem unroll_setInit {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (k : ℕ) (state : M.State) : + (M.setInit g).unroll k state = M.unroll k state := by + induction k generalizing state with + | zero => + rw [unroll_zero (M.setInit g) state, unroll_zero M state, setInit_view] + cases hview : M.view state with + | inl value => rfl + | inr query => rfl + | succ k ih => + rw [unroll_succ (M.setInit g) k state, unroll_succ M k state, setInit_view] + cases hview : M.view state with + | inl value => rfl + | inr query => + rcases query with ⟨position, next⟩ + exact congrArg (FreeM.liftBind position) + (funext fun direction => ih (next direction)) + +theorem run_setInit {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (k : ℕ) (input : γ) : + (M.setInit g).run k input = M.unroll k (g input) := + M.unroll_setInit g k (g input) + +/-- Mapping returned values maps the optional result of a bounded unrolling. -/ +@[simp] theorem unroll_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β) + (f : β → γ) (k : ℕ) (state : M.State) : + (M.mapResult f).unroll k state = + FreeM.map (Option.map f) (M.unroll k state) := by + induction k generalizing state with + | zero => + rw [unroll_zero (M.mapResult f) state, unroll_zero M state, mapResult_view] + cases hview : M.view state with + | inl value => rfl + | inr query => rfl + | succ k ih => + rw [unroll_succ (M.mapResult f) k state, unroll_succ M k state, mapResult_view] + cases hview : M.view state with + | inl value => rfl + | inr query => + rcases query with ⟨position, next⟩ + exact congrArg (FreeM.liftBind position) + (funext fun direction => ih (next direction)) + +@[simp] theorem run_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β) + (f : β → γ) (k : ℕ) (input : α) : + (M.mapResult f).run k input = FreeM.map (Option.map f) (M.run k input) := + M.unroll_mapResult f k (M.init input) + +/-- Interface transport along a lens transports bounded unrolling along the same +lens. -/ +@[simp] theorem unroll_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β) + (lens : Lens p q) (k : ℕ) (state : M.State) : + (M.wrap lens).unroll k state = (M.unroll k state).mapLens lens := by + induction k generalizing state with + | zero => + rw [unroll_zero (M.wrap lens) state, unroll_zero M state, wrap_view] + cases hview : M.view state with + | inl value => rfl + | inr query => rfl + | succ k ih => + rw [unroll_succ (M.wrap lens) k state, unroll_succ M k state, wrap_view] + cases hview : M.view state with + | inl value => rfl + | inr query => + rcases query with ⟨position, next⟩ + exact congrArg (FreeM.liftBind (lens.toFunA position)) + (funext fun direction => ih (next (lens.toFunB position direction))) + +@[simp] theorem run_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β) + (lens : Lens p q) (k : ℕ) (input : α) : + (M.wrap lens).run k input = (M.run k input).mapLens lens := + M.unroll_wrap lens k (M.init input) + /-! ## Resolution within a uniform query budget -/ /-- Every answer branch from `state` returns within `k` visible queries. -/ diff --git a/PolyFun/Realizability/Basic.lean b/PolyFun/Realizability/Basic.lean new file mode 100644 index 0000000..6324ed9 --- /dev/null +++ b/PolyFun/Realizability/Basic.lean @@ -0,0 +1,313 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Realizability.Machine +public import PolyFun.Realizability.StepClass + +/-! +# Realizability of free programs by admissible state machines + +A well-founded program family `program : α → FreeM p β` says *what* interaction +to perform. A `DynComputation p α β` says *how* a machine performs it, and +`DynComputation.Implements` says the two agree. This module adds the missing +third ingredient: a constraint on the machine's transition functions. + +`IsRealizableBy C bd program` holds when some `C`-admissible machine implements +`program`, where `C` is a `StepClass` and admissibility is asserted of the three +first-order step maps `init`, `head`, and `update?` from +`PolyFun.Realizability.Machine`. `IsRealizableWithin C bd program k` additionally +demands that every branch resolve within `k` visible queries. + +Instantiating `C` recovers a spectrum of concrete notions from one definition: +the trivial class gives back plain implementability, a finiteness class gives +finite-state realizability, a computability class gives machines with computable +transitions, and a resource-bounded class gives the polynomial-time +adversary model used in cryptography. + +## The boundary is a parameter, never an existential + +`Boundary` collects the representations of the input type, the result type, and +the interface. It is always a *parameter* of a realizability statement. A +statement of the form `∃ bd, IsRealizableBy C bd program` is vacuous, because a +representation is only required to be admissible, not canonical: an adversarially +chosen encoding can precompute across the boundary. Only the machine's own state +representation is chosen by the realization, and that choice is harmless — it is +exactly the freedom to pick a state layout. + +## Universe discipline + +`StepClass.Str` speaks about types in a single universe, so this layer is stated +at `p : PFunctor.{u, u}` with `α β : Type u` and hence `State : Type u`. Then +`p.A`, `p.Idx`, `β ⊕ p.A`, and `State × p.Idx` all live in `Type u`. The +underlying `DynComputation` API remains fully universe-polymorphic; only the +realizability predicates are pinned. + +## Provenance + +This is a `C`-relative *realization* condition in the sense of classical +(co)algebraic realization theory (Arbib–Manes 1974; Adámek–Milius–Moss–Sousa +2013) and of finite-state realizability in reactive synthesis (Pnueli–Rosner +1989), transported to the free-monad-over-a-polynomial-functor setting of +Libkind–Spivak 2025 and Aberlé 2026, with the resource bound imposed as an +admissibility predicate on the structure maps rather than as a Blum-style +measure on runs (Blum 1967). + +Two identifications make the shape of the definition inevitable. A `p`-coalgebra +on `S` *is* a way of running every `FreeM p` program in `S` (Uustalu 2015: +stateful runners are comodels, hence coalgebras), so a realization has nowhere +else to live. And the known special case at the class "given by a finite `FreeM` +term" is the alternating `νX.μY.` representation of stream processors +(Ghani–Hancock–Pattinson 2009). + +The word *realization* rather than *implementation* is deliberate: Aberlé uses +"implementation" for the free-monad Kleisli morphism, that is, for the program +side. See `REFERENCES.md`. +-/ + +@[expose] public section + +universe u v v₂ + +namespace PFunctor + +namespace DynSystem.DynComputation + +variable {p : PFunctor.{u, u}} {α β : Type u} + +/-! ## The boundary of a realizability statement -/ + +/-- The pinned representations at the boundary of a realizability statement: the +input type, the returned-value type, and the interface's query positions and +index space. + +The positions and the index space are supplied independently — nothing derives +one from the other, since a class need not represent dependent sums. -/ +structure Boundary (C : StepClass.{u, v}) (p : PFunctor.{u, u}) (α β : Type u) : + Type v where + /-- Representation of the input type. -/ + input : C.Str α + /-- Representation of the returned-value type. -/ + out : C.Str β + /-- Representation of the interface's query positions. -/ + pos : C.Str p.A + /-- Representation of the interface's index space `Idx p = Σ a, p.B a`. -/ + idx : C.Str p.Idx + +namespace Boundary + +variable {C : StepClass.{u, v}} + +/-- The representation of a machine's one-step readout `β ⊕ p.A`, assembled from +the result and position representations. -/ +def head [S : C.HasSum] (bd : Boundary C p α β) : C.Str (β ⊕ p.A) := + S.sum bd.out bd.pos + +/-- The representation of the flattened transition's domain: a machine state +paired with the interface's index space. -/ +def stateIdx [P : C.HasProd] (bd : Boundary C p α β) {S : Type u} + (state : C.Str S) : C.Str (S × p.Idx) := + P.prod state bd.idx + +/-- Replace the input representation of a boundary, keeping the result and +interface representations. -/ +def withInput {γ : Type u} (bd : Boundary C p α β) (inputRep : C.Str γ) : + Boundary C p γ β := + ⟨inputRep, bd.out, bd.pos, bd.idx⟩ + +/-- Replace the result representation of a boundary, keeping the input and +interface representations. -/ +def withOut {γ : Type u} (bd : Boundary C p α β) (outRep : C.Str γ) : + Boundary C p α γ := + ⟨bd.input, outRep, bd.pos, bd.idx⟩ + +@[simp] theorem withInput_input {γ : Type u} (bd : Boundary C p α β) + (inputRep : C.Str γ) : (bd.withInput inputRep).input = inputRep := rfl + +@[simp] theorem withOut_out {γ : Type u} (bd : Boundary C p α β) + (outRep : C.Str γ) : (bd.withOut outRep).out = outRep := rfl + +@[simp] theorem withInput_head [C.HasSum] {γ : Type u} (bd : Boundary C p α β) + (inputRep : C.Str γ) : (bd.withInput inputRep).head = bd.head := rfl + +@[simp] theorem withOut_input {γ : Type u} (bd : Boundary C p α β) + (outRep : C.Str γ) : (bd.withOut outRep).input = bd.input := rfl + +/-- The middle boundary of a sequential composition: the second phase reads the +first's results and shares its interface. + +Derived rather than constrained. Representations are *data*, so a `Prop`-valued +equality between two boundaries would force `subst` transport at every use site; +deriving the middle boundary makes every compatibility fact hold by `rfl`. The +composite boundary of a sequential composition is then simply +`bd.withOut outRep`. -/ +def mid {γ : Type u} (bd : Boundary C p α β) (outRep : C.Str γ) : + Boundary C p β γ := + (bd.withOut outRep).withInput bd.out + +@[simp] theorem mid_input {γ : Type u} (bd : Boundary C p α β) + (outRep : C.Str γ) : (bd.mid outRep).input = bd.out := rfl + +@[simp] theorem mid_out {γ : Type u} (bd : Boundary C p α β) + (outRep : C.Str γ) : (bd.mid outRep).out = outRep := rfl + +@[simp] theorem mid_pos {γ : Type u} (bd : Boundary C p α β) + (outRep : C.Str γ) : (bd.mid outRep).pos = bd.pos := rfl + +@[simp] theorem mid_idx {γ : Type u} (bd : Boundary C p α β) + (outRep : C.Str γ) : (bd.mid outRep).idx = bd.idx := rfl + +/-- Two boundaries compose when the second reads the first's results and both +describe the same interface. A convenience wrapper over `mid`, for use sites that +already have both boundaries in hand. -/ +structure Composable {γ : Type u} (bd₁ : Boundary C p α β) + (bd₂ : Boundary C p β γ) : Prop where + /-- The second phase reads the first's results. -/ + input_eq : bd₂.input = bd₁.out + /-- Both phases describe the same query positions. -/ + pos_eq : bd₂.pos = bd₁.pos + /-- Both phases describe the same index space. -/ + idx_eq : bd₂.idx = bd₁.idx + +theorem eq_mid_of_composable {γ : Type u} {bd₁ : Boundary C p α β} + {bd₂ : Boundary C p β γ} (h : bd₁.Composable bd₂) : + bd₂ = bd₁.mid bd₂.out := by + obtain ⟨input, out, pos, idx⟩ := bd₂ + obtain ⟨hinput, hpos, hidx⟩ := h + subst hinput + subst hpos + subst hidx + rfl + +/-- Replace the interface representations of a boundary, keeping the input and +result representations. This is the target boundary of an interface transport. -/ +def withInterface (bd : Boundary C p α β) {q : PFunctor.{u, u}} + (posRep : C.Str q.A) (idxRep : C.Str q.Idx) : Boundary C q α β := + ⟨bd.input, bd.out, posRep, idxRep⟩ + +@[simp] theorem withInterface_input (bd : Boundary C p α β) + {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) : + (bd.withInterface posRep idxRep).input = bd.input := rfl + +@[simp] theorem withInterface_out (bd : Boundary C p α β) + {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) : + (bd.withInterface posRep idxRep).out = bd.out := rfl + +@[simp] theorem withInterface_pos (bd : Boundary C p α β) + {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) : + (bd.withInterface posRep idxRep).pos = posRep := rfl + +@[simp] theorem withInterface_idx (bd : Boundary C p α β) + {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) : + (bd.withInterface posRep idxRep).idx = idxRep := rfl + +/-- Translate a boundary along a refinement of step classes. -/ +def mapRefines {D : StepClass.{u, v₂}} [C.HasProd] [C.HasSum] [C.HasOption] + [D.HasProd] [D.HasSum] [D.HasOption] (Ref : C.Refines D) + (bd : Boundary C p α β) : Boundary D p α β := + ⟨Ref.str bd.input, Ref.str bd.out, Ref.str bd.pos, Ref.str bd.idx⟩ + +end Boundary + +/-! ## Admissible realizations -/ + +/-- A `C`-admissible realization of an interface-`p` computation with inputs `α` +and results `β`. + +The data is a returning dynamical computation together with a representation of +its hidden state — chosen freely by the realization — and proofs that its three +first-order step maps are `C`-morphisms: + +* `init : α → State` starts the machine. Constraining it is what forbids + smuggling precomputed advice into the initial state. +* `head : State → β ⊕ p.A` reads off a returned value or an exposed query. +* `update? : State × p.Idx → Option State` consumes a tagged answer, partially. + +By `ofStep_step_eq_of_flat_eq` those three maps determine the machine, so this is +a constraint on the machine itself rather than on a lossy projection of it. + +Nothing here constrains the machine's *behaviour*: a realization is admissible +machinery, and agreement with a program is the separate `Implements` predicate. +The two are combined by `IsRealizableBy`. -/ +structure Realization (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption] + [DecidableEq p.A] (bd : Boundary C p α β) where + /-- The underlying machine. -/ + machine : DynComputation.{u} p α β + /-- The chosen representation of the machine's hidden state. -/ + state : C.Str machine.State + /-- Initialization is admissible. -/ + init_mem : C.Hom bd.input state machine.init + /-- The one-step readout is admissible. -/ + head_mem : C.Hom state bd.head machine.head + /-- The partial flattened transition is admissible. -/ + update_mem : C.Hom (bd.stateIdx state) (StepClass.HasOption.option state) + machine.update? + +/-! ## The realizability predicates -/ + +/-- `program` is `C`-realizable: some `C`-admissible machine implements it. + +Resource bounds are deliberately not part of this predicate; see +`IsRealizableWithin` for the bounded form. -/ +def IsRealizableBy (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption] + [DecidableEq p.A] (bd : Boundary C p α β) (program : α → FreeM p β) : Prop := + ∃ R : Realization C bd, R.machine.Implements program + +/-- `program` is `C`-realizable within the uniform query budget `k`: some +`C`-admissible machine implements it and resolves every answer branch within `k` +visible queries. -/ +def IsRealizableWithin (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption] + [DecidableEq p.A] (bd : Boundary C p α β) (program : α → FreeM p β) + (k : ℕ) : Prop := + ∃ R : Realization C bd, R.machine.ImplementsWithin program k + +section Basic + +variable {C : StepClass.{u, v}} [C.HasProd] [C.HasSum] [C.HasOption] + [DecidableEq p.A] {bd : Boundary C p α β} {program : α → FreeM p β} + +/-- A bounded realization is in particular a realization. -/ +theorem IsRealizableWithin.isRealizableBy {k : ℕ} + (h : IsRealizableWithin C bd program k) : IsRealizableBy C bd program := by + obtain ⟨R, hR⟩ := h + exact ⟨R, ((implementsWithin_iff_implements_and_bound R.machine program k).mp hR).1⟩ + +/-- A bounded realization certifies that the program itself fits the budget: the +resource bound is a property of the syntax, extracted from the machine. -/ +theorem IsRealizableWithin.isTotalRollBound {k : ℕ} + (h : IsRealizableWithin C bd program k) (input : α) : + (program input).IsTotalRollBound k := by + obtain ⟨R, hR⟩ := h + exact ((implementsWithin_iff_implements_and_bound R.machine program k).mp hR).2 input + +/-- Bounded realizability is monotone in the query budget. -/ +theorem IsRealizableWithin.mono {j k : ℕ} + (h : IsRealizableWithin C bd program j) (hjk : j ≤ k) : + IsRealizableWithin C bd program k := by + obtain ⟨R, hR⟩ := h + exact ⟨R, hR.mono hjk⟩ + +/-- Realizability only depends on the program family through its values. -/ +theorem IsRealizableBy.congr {program' : α → FreeM p β} + (h : IsRealizableBy C bd program) (hprog : ∀ input, program input = program' input) : + IsRealizableBy C bd program' := by + obtain ⟨R, hR⟩ := h + exact ⟨R, fun input => (hprog input) ▸ hR input⟩ + +/-- Bounded realizability only depends on the program family through its +values. -/ +theorem IsRealizableWithin.congr {program' : α → FreeM p β} {k : ℕ} + (h : IsRealizableWithin C bd program k) + (hprog : ∀ input, program input = program' input) : + IsRealizableWithin C bd program' k := by + obtain ⟨R, hR⟩ := h + exact ⟨R, fun input => (hprog input) ▸ hR input⟩ + +end Basic + +end DynSystem.DynComputation + +end PFunctor diff --git a/PolyFun/Realizability/Closure.lean b/PolyFun/Realizability/Closure.lean new file mode 100644 index 0000000..1b7b09f --- /dev/null +++ b/PolyFun/Realizability/Closure.lean @@ -0,0 +1,378 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Realizability.Basic + +/-! +# Closure properties of admissible realizability + +Realizability is closed under the operations that leave a machine's dynamics +intact or reindex them by an admissible map, and it transports along refinements +of the ambient step class. Each theorem asks of the class exactly the structure +its construction consumes: + +* `isRealizableBy_ofFn` — an immediately returning program, realized by the + one-step machine whose states are its own results. Needs the returning map to + be admissible. +* `IsRealizableBy.precomp` / `IsRealizableWithin.precomp` — input + precomposition, realized by `setInit`. The machine, its state representation, + and both of its remaining step maps are untouched, so only the initialization + obligation changes. +* `IsRealizableBy.mapResult` / `IsRealizableWithin.mapResult` — postcomposition + on results, realized by `mapResult`. The readout gains a `Sum.map` and the + transition is unchanged. +* `IsRealizableBy.seqComp` / `IsRealizableWithin.seqComp` — **closure under + `FreeM.bind`**, realized by `seqComp`. The state is the coproduct of the two + phases' states, and budgets add. Needs `IsDistributive`. +* `IsRealizableBy.wrap` / `IsRealizableWithin.wrap` — interface transport along a + lens, realized by `wrap`. Needs the lens to be `Lens.IsAdmissible`. +* `IsRealizableBy.mono` / `IsRealizableWithin.mono'` — transport along a + `StepClass.Refines`. + +Budget monotonicity and the bridge from the bounded to the unbounded predicate +live in `PolyFun.Realizability.Basic`. + +## Where the structure is spent + +Distributivity is consumed in exactly one place, and only twice: the composite +`update?` of a sequential composition splits on the state summand, and then on the +first phase's readout, each time retaining the answer index. The *readout* side of +the same composition needs no products at all — only `comp_mem`, `elim_mem`, and +`inr_mem`. + +None of this needs a decidable-equality test on interface positions, and that is a +consequence of `update?` being partial: each phase's own transition already returns +`none` on an answer it is not waiting for, so the composite inherits the tag test +rather than performing it. With the total `updateFlat` no uniform equation holds and +an equality-test axiom would be forced; see `PolyFun.Realizability.Machine`. + +Interface transport is the one place a tag test does surface, because pulling an +answer back along a lens must compare it against the position the lens exposes. +That is why `wrap` takes a `Lens.IsAdmissible` hypothesis while `seqComp` takes +none. +-/ + +@[expose] public section + +universe u v v₂ + +namespace PFunctor + +namespace DynSystem.DynComputation + +variable {p : PFunctor.{u, u}} {α β : Type u} + {C : StepClass.{u, v}} [P : C.HasProd] [S : C.HasSum] [O : C.HasOption] + [DecidableEq p.A] {bd : Boundary C p α β} {program : α → FreeM p β} + +/-! ## Immediately returning programs -/ + +/-- An immediately returning program is realizable exactly when its returning map +is admissible. The realizing machine takes the result type itself as its state: +`head` is the left injection and the flattened transition is the first +projection. -/ +theorem isRealizableBy_ofFn {f : α → β} (hf : C.Hom bd.input bd.out f) : + IsRealizableBy C bd (fun input => FreeM.pure (f input)) := by + refine ⟨⟨ofFn (p := p) f, bd.out, hf, StepClass.HasSum.inl_mem bd.out bd.pos, ?_⟩, + ?_⟩ + · refine (StepClass.HasOption.none_mem (bd.stateIdx bd.out) bd.out).congr ?_ + intro step + exact (update?_of_view_return (ofFn (p := p) f) (view_ofFn f step.1) step.2).symm + · intro input + rw [denote_ofFn] + simp + +/-- A constant program is realizable whenever the constant is: the special case +of `isRealizableBy_ofFn` at a constant returning map. -/ +theorem isRealizableBy_pure {value : β} + (hvalue : C.Hom bd.input bd.out fun _ : α => value) : + IsRealizableBy C bd fun _ : α => (FreeM.pure value : FreeM p β) := + isRealizableBy_ofFn hvalue + +/-! ## Input precomposition -/ + +/-- Input precomposition along an admissible map. The realizing machine is the +original one with a new initialization, so its readout and transition maps — and +hence their admissibility proofs — are shared definitionally. -/ +theorem IsRealizableBy.precomp {γ : Type u} {inputRep : C.Str γ} {f : γ → α} + (h : IsRealizableBy C bd program) (hf : C.Hom inputRep bd.input f) : + IsRealizableBy C (bd.withInput inputRep) fun input => program (f input) := by + obtain ⟨R, hR⟩ := h + refine ⟨⟨R.machine.contramapInput f, R.state, ?_, R.head_mem, R.update_mem⟩, + hR.contramapInput f⟩ + change C.Hom inputRep R.state (R.machine.init ∘ f) + exact C.comp_mem hf R.init_mem + +/-- Input precomposition preserves the query budget: reindexing inputs performs +no queries of its own. -/ +theorem IsRealizableWithin.precomp {γ : Type u} {inputRep : C.Str γ} {f : γ → α} + {k : ℕ} (h : IsRealizableWithin C bd program k) + (hf : C.Hom inputRep bd.input f) : + IsRealizableWithin C (bd.withInput inputRep) (fun input => program (f input)) k := by + obtain ⟨R, hR⟩ := h + rw [implementsWithin_iff_implements_and_bound] at hR + refine ⟨⟨R.machine.contramapInput f, R.state, ?_, R.head_mem, R.update_mem⟩, ?_⟩ + · change C.Hom inputRep R.state (R.machine.init ∘ f) + exact C.comp_mem hf R.init_mem + · rw [implementsWithin_iff_implements_and_bound] + exact ⟨hR.1.contramapInput f, fun input => hR.2 (f input)⟩ + +/-! ## Result postcomposition -/ + +/-- Postcomposition on results along an admissible map. The realizing machine is +the original one with its readout postcomposed, which acts on the one-step +readout `β ⊕ p.A` by `Sum.map` and leaves the flattened transition alone. -/ +theorem IsRealizableBy.mapResult {γ : Type u} {outRep : C.Str γ} {g : β → γ} + (h : IsRealizableBy C bd program) (hg : C.Hom bd.out outRep g) : + IsRealizableBy C (bd.withOut outRep) + fun input => FreeM.map g (program input) := by + obtain ⟨R, hR⟩ := h + refine ⟨⟨R.machine.mapResult g, R.state, R.init_mem, ?_, ?_⟩, hR.mapResult g⟩ + · refine (C.comp_mem R.head_mem + (StepClass.HasSum.map_mem hg (C.id_mem bd.pos))).congr ?_ + intro state + exact (head_mapResult R.machine g state).symm + · refine R.update_mem.congr ?_ + intro step + exact (update?_mapResult R.machine g step).symm + +/-- Postcomposition on results preserves the query budget: mapping a returned +value performs no queries of its own. -/ +theorem IsRealizableWithin.mapResult {γ : Type u} {outRep : C.Str γ} {g : β → γ} + {k : ℕ} (h : IsRealizableWithin C bd program k) + (hg : C.Hom bd.out outRep g) : + IsRealizableWithin C (bd.withOut outRep) + (fun input => FreeM.map g (program input)) k := by + obtain ⟨R, hR⟩ := h + rw [implementsWithin_iff_implements_and_bound] at hR + refine ⟨⟨R.machine.mapResult g, R.state, R.init_mem, ?_, ?_⟩, ?_⟩ + · refine (C.comp_mem R.head_mem + (StepClass.HasSum.map_mem hg (C.id_mem bd.pos))).congr ?_ + intro state + exact (head_mapResult R.machine g state).symm + · refine R.update_mem.congr ?_ + intro step + exact (update?_mapResult R.machine g step).symm + · rw [implementsWithin_iff_implements_and_bound] + refine ⟨hR.1.mapResult g, fun input => ?_⟩ + exact (FreeM.isRollBound_map_iff (program input) g k _ _).mpr (hR.2 input) + +/-! ## Sequential composition -/ + +section SeqComp + +variable [D : C.IsDistributive] {γ : Type u} {outRep : C.Str γ} + {program₁ : α → FreeM p β} {program₂ : β → FreeM p γ} + +/-- The admissible realization of a sequential composition. + +The state is the coproduct of the two phases' states. The readout needs only +`comp_mem`, `elim_mem`, and `inr_mem` — no products at all. The partial transition +is where distributivity enters, twice: once to split on the state summand, once to +split on the first phase's readout while retaining the answer index. -/ +private def seqCompRealization (R₁ : Realization C bd) + (R₂ : Realization C (bd.mid outRep)) : + Realization C (bd.withOut outRep) where + machine := R₁.machine.seqComp R₂.machine + state := S.sum R₁.state R₂.state + init_mem := by + refine (C.comp_mem R₁.init_mem (S.inl_mem R₁.state R₂.state)).congr ?_ + intro input + rfl + head_mem := by + refine (S.elim_mem + (C.comp_mem R₁.head_mem + (S.elim_mem (C.comp_mem R₂.init_mem R₂.head_mem) + (S.inr_mem outRep bd.pos))) + R₂.head_mem).congr ?_ + intro state + cases state with + | inl state₁ => exact (head_seqComp_inl R₁.machine R₂.machine state₁).symm + | inr state₂ => exact (head_seqComp_inr R₁.machine R₂.machine state₂).symm + update_mem := by + -- The right summand: advance the second phase and re-tag the result. + have hRight : C.Hom (P.prod R₂.state bd.idx) + (StepClass.HasOption.option (S.sum R₁.state R₂.state)) + (fun x => Option.map Sum.inr (R₂.machine.update? x)) := + C.comp_mem R₂.update_mem + (StepClass.HasOption.omap_mem (S.inr_mem R₁.state R₂.state)) + -- The left summand, first phase still exposing a query. + have hQuery : C.Hom (P.prod bd.pos (P.prod R₁.state bd.idx)) + (StepClass.HasOption.option (S.sum R₁.state R₂.state)) + (fun y => Option.map Sum.inl (R₁.machine.update? y.2)) := + C.comp_mem (P.snd_mem bd.pos (P.prod R₁.state bd.idx)) + (C.comp_mem R₁.update_mem + (StepClass.HasOption.omap_mem (S.inl_mem R₁.state R₂.state))) + -- The left summand, first phase already returned: hand over to the second. + have hHandoff : C.Hom (P.prod bd.out (P.prod R₁.state bd.idx)) + (StepClass.HasOption.option (S.sum R₁.state R₂.state)) + (fun y => Option.map Sum.inr + (R₂.machine.update? (R₂.machine.init y.1, y.2.2))) := + C.comp_mem + (P.pair_mem + (C.comp_mem (P.fst_mem bd.out (P.prod R₁.state bd.idx)) R₂.init_mem) + (C.comp_mem (P.snd_mem bd.out (P.prod R₁.state bd.idx)) + (P.snd_mem R₁.state bd.idx))) + hRight + -- Splitting on the first phase's readout, retaining the state and the index. + have hLeft : C.Hom (P.prod R₁.state bd.idx) + (StepClass.HasOption.option (S.sum R₁.state R₂.state)) + (fun x => Sum.elim + (fun value => Option.map Sum.inr + (R₂.machine.update? (R₂.machine.init value, x.2))) + (fun _ : p.A => Option.map Sum.inl (R₁.machine.update? x)) + (R₁.machine.head x.1)) := + C.comp_mem + (P.withInput_mem (C.comp_mem (P.fst_mem R₁.state bd.idx) R₁.head_mem)) + (StepClass.IsDistributive.elimCtx_mem hHandoff hQuery) + -- Splitting on the state summand. + refine (StepClass.IsDistributive.elimCtx_mem hLeft hRight).congr ?_ + intro x + obtain ⟨state, index⟩ := x + cases state with + | inl state₁ => + exact (update?_seqComp_inl R₁.machine R₂.machine state₁ index).symm + | inr state₂ => + exact (update?_seqComp_inr R₁.machine R₂.machine state₂ index).symm + +/-- **Closure under `bind`.** A realization of the first phase and a realization of +the second compose into a realization of their sequential composition. + +The middle boundary is `bd.mid outRep`: the second phase reads the first's results +and shares its interface. Distributivity is what the composite transition needs, +and only there — the readout side needs no products at all. -/ +theorem IsRealizableBy.seqComp (h₁ : IsRealizableBy C bd program₁) + (h₂ : IsRealizableBy C (bd.mid outRep) program₂) : + IsRealizableBy C (bd.withOut outRep) + fun input => FreeM.bind (program₁ input) program₂ := by + obtain ⟨R₁, hR₁⟩ := h₁ + obtain ⟨R₂, hR₂⟩ := h₂ + exact ⟨seqCompRealization R₁ R₂, hR₁.seqComp hR₂⟩ + +/-- Sequential composition of bounded realizations, with additive budgets. The +query budget is exactly the one the underlying `ImplementsWithin.seqComp` +supplies. -/ +theorem IsRealizableWithin.seqComp {k₁ k₂ : ℕ} + (h₁ : IsRealizableWithin C bd program₁ k₁) + (h₂ : IsRealizableWithin C (bd.mid outRep) program₂ k₂) : + IsRealizableWithin C (bd.withOut outRep) + (fun input => FreeM.bind (program₁ input) program₂) (k₁ + k₂) := by + obtain ⟨R₁, hR₁⟩ := h₁ + obtain ⟨R₂, hR₂⟩ := h₂ + exact ⟨seqCompRealization R₁ R₂, hR₁.seqComp hR₂⟩ + +end SeqComp + +/-! ## Interface transport -/ + +section Wrap + +variable {q : PFunctor.{u, u}} [DecidableEq q.A] + +variable (posRep : C.Str q.A) (idxRep : C.Str q.Idx) + +/-- A lens is `C`-admissible, relative to a boundary for its source interface and +representations for its target interface, when its position map and its flattened +index pullback are `C`-morphisms. + +Two fields rather than one existential: the pullback is uniquely determined by the +lens, so it is `Lens.pullHeadIdx` and only its admissibility is a hypothesis. + +Unlike `Lens.IsCartesian` this has no `.id` and no `.comp`, and that is not an +oversight. `pullHeadIdx` compares the incoming answer's tag against the position +the lens exposes, so even the *identity* lens's pullback performs a decidable +equality test on positions — which is exactly the operation the rest of this layer +is designed not to require of a step class. Admissibility of a lens is therefore a +genuine hypothesis about the class, satisfiable by every realistic one but not +derivable from the mixins. That is also why `seqComp` needs no such hypothesis: +each phase's own `update?` performs its own tag test internally. -/ +structure _root_.PFunctor.Lens.IsAdmissible (C : StepClass.{u, v}) [C.HasProd] + [C.HasSum] [C.HasOption] {p q : PFunctor.{u, u}} [DecidableEq q.A] + {α β : Type u} (bd : Boundary C p α β) (posRep : C.Str q.A) + (idxRep : C.Str q.Idx) (lens : Lens p q) : Prop where + /-- The position map is admissible. -/ + onPos : C.Hom bd.pos posRep lens.toFunA + /-- The flattened index pullback is admissible. -/ + onPull : C.Hom (StepClass.HasProd.prod bd.head idxRep) + (StepClass.HasOption.option bd.idx) (lens.pullHeadIdx β) + +/-- Interface transport along an admissible lens. The readout is post-composed +with the lens's position map; the transition pulls an answer back along the lens +before feeding it to the underlying computation. + +The resolved case needs no constant-map axiom: `pullHeadIdx` returns `none` at a +resolved readout, and the underlying `update?` is `none` there anyway. -/ +theorem IsRealizableBy.wrap {lens : Lens p q} + (hlens : lens.IsAdmissible C bd posRep idxRep) + (h : IsRealizableBy C bd program) : + IsRealizableBy C (bd.withInterface posRep idxRep) + fun input => (program input).mapLens lens := by + obtain ⟨R, hR⟩ := h + refine ⟨⟨R.machine.wrap lens, R.state, R.init_mem, ?_, ?_⟩, hR.wrap lens⟩ + · refine (C.comp_mem R.head_mem + (S.map_mem (C.id_mem bd.out) hlens.onPos)).congr ?_ + intro state + rfl + · refine (C.comp_mem + (P.withInput_mem (C.comp_mem (P.pairRight_mem R.head_mem) hlens.onPull)) + (StepClass.HasOption.obindCtx_mem + (C.comp_mem + (P.pair_mem + (C.comp_mem (P.snd_mem bd.idx (P.prod R.state idxRep)) + (P.fst_mem R.state idxRep)) + (P.fst_mem bd.idx (P.prod R.state idxRep))) + R.update_mem))).congr ?_ + intro x + obtain ⟨state, index⟩ := x + obtain ⟨iposition, idirection⟩ := index + exact (update?_wrap R.machine lens state iposition idirection).symm + +/-- Interface transport preserves the query budget: a lens relabels positions and +reindexes directions, leaving the branching structure alone. -/ +theorem IsRealizableWithin.wrap {lens : Lens p q} {k : ℕ} + (hlens : lens.IsAdmissible C bd posRep idxRep) + (h : IsRealizableWithin C bd program k) : + IsRealizableWithin C (bd.withInterface posRep idxRep) + (fun input => (program input).mapLens lens) k := by + obtain ⟨R, hR⟩ := h + rw [implementsWithin_iff_implements_and_bound] at hR + obtain ⟨R', hR'⟩ := + IsRealizableBy.wrap (program := program) posRep idxRep hlens ⟨R, hR.1⟩ + refine ⟨R', ?_⟩ + rw [implementsWithin_iff_implements_and_bound] + exact ⟨hR', fun input => FreeM.isTotalRollBound_mapLens lens _ (hR.2 input)⟩ + +end Wrap + +/-! ## Enlarging the step class -/ + +variable {D : StepClass.{u, v₂}} [D.HasProd] [D.HasSum] [D.HasOption] + +/-- Realizability transports along a refinement of step classes: a realization by +an admissible machine for a small class is one for every larger class. -/ +theorem IsRealizableBy.mono (Ref : C.Refines D) (h : IsRealizableBy C bd program) : + IsRealizableBy D (bd.mapRefines Ref) program := by + obtain ⟨R, hR⟩ := h + refine ⟨⟨R.machine, Ref.str R.state, Ref.hom R.init_mem, ?_, ?_⟩, hR⟩ + · rw [Boundary.head, Boundary.mapRefines, ← Ref.str_sum] + exact Ref.hom R.head_mem + · rw [Boundary.stateIdx, Boundary.mapRefines, ← Ref.str_prod, ← Ref.str_option] + exact Ref.hom R.update_mem + +/-- Bounded realizability transports along a refinement of step classes. -/ +theorem IsRealizableWithin.mono' {k : ℕ} (Ref : C.Refines D) + (h : IsRealizableWithin C bd program k) : + IsRealizableWithin D (bd.mapRefines Ref) program k := by + obtain ⟨R, hR⟩ := h + refine ⟨⟨R.machine, Ref.str R.state, Ref.hom R.init_mem, ?_, ?_⟩, hR⟩ + · rw [Boundary.head, Boundary.mapRefines, ← Ref.str_sum] + exact Ref.hom R.head_mem + · rw [Boundary.stateIdx, Boundary.mapRefines, ← Ref.str_prod, ← Ref.str_option] + exact Ref.hom R.update_mem + +end DynSystem.DynComputation + +end PFunctor diff --git a/PolyFun/Realizability/Instances.lean b/PolyFun/Realizability/Instances.lean new file mode 100644 index 0000000..bb41453 --- /dev/null +++ b/PolyFun/Realizability/Instances.lean @@ -0,0 +1,512 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Realizability.Basic +public import Mathlib.Computability.Partrec +public import Mathlib.Data.Fintype.Prod +public import Mathlib.Data.Fintype.Sum + +/-! +# Concrete step classes + +Four instantiations of `PFunctor.StepClass`, in increasing order of content. + +* `StepClass.unconstrained` — every type is representable and every function + admissible. Realizability collapses to plain implementability, which + `isRealizableBy_unconstrained` confirms is never a real restriction. This is the + non-vacuity check for the whole layer. +* `StepClass.finite` — a type is representable when it is finite. Realizability in + this class is *finite-state realizability*, the notion Church's synthesis + problem asks about and which Pnueli and Rosner (1989) made precise; see + `REFERENCES.md`. +* `StepClass.computable` — Mathlib's `Primcodable` representations and + `Computable` functions: machines whose transition functions are computable. +* `StepClass.ofWordClass` — the bridge from an externally defined class of *word* + functions `W → W`. Complexity classes in the wild are almost always presented + this way, on one concrete function type such as `List Bool → List Bool`, with no + encoding-generic predicate. + +Each class carries all four mixins: `HasProd`, `HasSum`, `HasOption`, and +`IsDistributive`. For `unconstrained` and `finite` every obligation is trivial. +For `computable` they are short, because Mathlib's `Computable.sumCasesOn` and +`Computable.option_map` are already stated in *contextual* form — branches +`α → β → σ` with `α` the ambient context — which is exactly distributivity. + +## What a word class has to supply + +None of the four mixins is automatic for a monomorphic word class. Bundle the +required data as a `WordClass`: identity and composition closure, a `WordPairing` +codec, a `WordTagging` scheme with a distinguished word, and a `WordDistrib` +rearrangement moving a tag past a pairing. `WordClass.toStepClass` then carries all +four mixins as instances, so a client never names them. + +`WordDistrib` is forced by the mathematics rather than by this presentation: +`WordTagging.elim` hands each branch only the untagged payload, so its branches +cannot see the surrounding context and a tag cannot be moved past a pairing using +`elim` alone. + +What this costs a real client: `Complexity.FP` (complexitylib) and +`Cslib.Turing.PolyTimeComputable` (cslib) both supply the identity and composition +closure, and complexitylib has the pairing ingredients (`Complexity.pair`, +`unpair?`, `delimit`) — but neither exposes them as class-level closure results, +and cslib has no pairing or projection machines at all. cslib's +`PolyTimeComputable` is additionally `Type`-valued with a `Monotone` side condition +on `comp` whose removal is still a `TODO` upstream, so `Mem f := +Nonempty (PolyTimeComputable f)` needs a monotonisation lemma that does not exist +yet. +-/ + +@[expose] public section + +universe u v + +namespace PFunctor + +namespace StepClass + +/-! ## The unconstrained class -/ + +/-- The step class that constrains nothing: every type is representable, by no +data, and every function is admissible. -/ +def unconstrained : StepClass.{u, v} where + Str _ := PUnit.{v + 1} + Hom _ _ _ := True + id_mem _ := True.intro + comp_mem _ _ := True.intro + +instance : (unconstrained.{u, v}).HasProd where + prod _ _ := PUnit.unit + fst_mem _ _ := True.intro + snd_mem _ _ := True.intro + pair_mem _ _ := True.intro + +instance : (unconstrained.{u, v}).HasSum where + sum _ _ := PUnit.unit + inl_mem _ _ := True.intro + inr_mem _ _ := True.intro + elim_mem _ _ := True.intro + +instance : (unconstrained.{u, v}).HasOption where + option _ := PUnit.unit + omap_mem _ := True.intro + none_mem _ _ := True.intro + obindCtx_mem _ := True.intro + +instance : (unconstrained.{u, v}).IsDistributive where + distrib_mem _ _ _ := True.intro + +/-! ## The finite class -/ + +/-- The step class of finite representations: a type is representable exactly when +it is finite, and every function between finite types is admissible. -/ +def finite : StepClass.{u, u} where + Str := Fintype + Hom _ _ _ := True + id_mem _ := True.intro + comp_mem _ _ := True.intro + +instance : (finite.{u}).HasProd where + prod {A B} a b := @instFintypeProd A B a b + fst_mem _ _ := True.intro + snd_mem _ _ := True.intro + pair_mem _ _ := True.intro + +instance : (finite.{u}).HasSum where + sum {A B} a b := @instFintypeSum A B a b + inl_mem _ _ := True.intro + inr_mem _ _ := True.intro + elim_mem _ _ := True.intro + +instance : (finite.{u}).HasOption where + option {A} a := by + letI : Fintype A := a + exact (inferInstance : Fintype (Option A)) + omap_mem _ := True.intro + none_mem _ _ := True.intro + obindCtx_mem _ := True.intro + +instance : (finite.{u}).IsDistributive where + distrib_mem _ _ _ := True.intro + +/-! ## The computable class -/ + +/-- The step class of computable functions between `Primcodable` types. + +The representation carried by a type is its `Primcodable` structure, which is +genuine data: `Computable f` is a statement about the encodings, so the class +cannot be phrased without them. -/ +def computable : StepClass.{u, u} where + Str := Primcodable + Hom {A B} a b f := @Computable A B a b f + id_mem {A} a := by + letI : Primcodable A := a + exact Computable.id + comp_mem {A B D} {a b d} {f g} hf hg := by + letI : Primcodable A := a + letI : Primcodable B := b + letI : Primcodable D := d + have hf' : Computable f := hf + have hg' : Computable g := hg + exact hg'.comp hf' + +instance : (computable.{u}).HasProd where + prod {A B} a b := @Primcodable.prod A B a b + fst_mem {A B} a b := by + letI : Primcodable A := a + letI : Primcodable B := b + exact Computable.fst + snd_mem {A B} a b := by + letI : Primcodable A := a + letI : Primcodable B := b + exact Computable.snd + pair_mem {A B D} {a b d} {f g} hf hg := by + letI : Primcodable A := a + letI : Primcodable B := b + letI : Primcodable D := d + have hf' : Computable f := hf + have hg' : Computable g := hg + exact hf'.pair hg' + +instance : (computable.{u}).HasSum where + sum {A B} a b := @Primcodable.sum A B a b + inl_mem {A B} a b := by + letI : Primcodable A := a + letI : Primcodable B := b + exact Primrec.sumInl.to_comp + inr_mem {A B} a b := by + letI : Primcodable A := a + letI : Primcodable B := b + exact Primrec.sumInr.to_comp + elim_mem {A B D} {a b d} {f g} hf hg := by + letI : Primcodable A := a + letI : Primcodable B := b + letI : Primcodable D := d + have hf' : Computable f := hf + have hg' : Computable g := hg + refine Computable.of_eq (Computable.sumCasesOn Computable.id + (hf'.comp Computable.snd).to₂ (hg'.comp Computable.snd).to₂) ?_ + intro x + cases x <;> rfl + +instance : (computable.{u}).HasOption where + option {A} a := @Primcodable.option A a + omap_mem {A B} {a b} {f} hf := by + letI : Primcodable A := a + letI : Primcodable B := b + have hf' : Computable f := hf + refine Computable.of_eq + (Computable.option_map Computable.id (hf'.comp Computable.snd).to₂) ?_ + intro x + cases x <;> rfl + none_mem {A B} a b := by + letI : Primcodable A := a + letI : Primcodable B := b + exact Computable.const none + obindCtx_mem {A B E} {a b e} {k} hk := by + letI : Primcodable A := a + letI : Primcodable B := b + letI : Primcodable E := e + have hk' : Computable k := hk + refine Computable.of_eq + (Computable.option_bind Computable.fst + (hk'.comp (Computable.pair Computable.snd + (Computable.snd.comp Computable.fst))).to₂) ?_ + intro y + cases y.1 <;> rfl + +/-- Mathlib's sum eliminator is already stated in *contextual* form — its branches +are `α → β → σ` with `α` the ambient context — which is exactly distributivity. -/ +instance : (computable.{u}).IsDistributive where + distrib_mem {A B I} a b i := by + letI : Primcodable A := a + letI : Primcodable B := b + letI : Primcodable I := i + refine Computable.of_eq (Computable.sumCasesOn Computable.fst + (Primrec.sumInl.to_comp.comp (Computable.pair Computable.snd + (Computable.snd.comp Computable.fst))).to₂ + (Primrec.sumInr.to_comp.comp (Computable.pair Computable.snd + (Computable.snd.comp Computable.fst))).to₂) ?_ + rintro ⟨x | x, j⟩ <;> rfl + +/-! ## The bridge from a class of word functions -/ + +/-- A pairing codec on `W` whose operations the word class `Q` admits. This is the +data a monomorphic word class needs in order to represent binary products. -/ +structure WordPairing {W : Type u} (Q : (W → W) → Prop) where + /-- Pair two words. -/ + pair : W → W → W + /-- Pairing is injective in both arguments jointly. -/ + pair_inj : ∀ w₁ w₂ w₁' w₂', pair w₁ w₂ = pair w₁' w₂' → w₁ = w₁' ∧ w₂ = w₂' + /-- Recover the first component. -/ + fst : W → W + /-- Recover the second component. -/ + snd : W → W + /-- The first projection is admissible. -/ + fst_mem : Q fst + /-- The second projection is admissible. -/ + snd_mem : Q snd + /-- `fst` is a left inverse of pairing. -/ + fst_pair : ∀ w₁ w₂, fst (pair w₁ w₂) = w₁ + /-- `snd` is a right inverse of pairing. -/ + snd_pair : ∀ w₁ w₂, snd (pair w₁ w₂) = w₂ + /-- Admissible functions can be paired. -/ + pair_mem : ∀ {f g : W → W}, Q f → Q g → Q fun w => pair (f w) (g w) + +/-- A tagging scheme on `W` whose operations the word class `Q` admits. This is the +data a monomorphic word class needs in order to represent binary sums. -/ +structure WordTagging {W : Type u} (Q : (W → W) → Prop) where + /-- Tag a word as coming from the left summand. -/ + inl : W → W + /-- Tag a word as coming from the right summand. -/ + inr : W → W + /-- Left tagging is admissible. -/ + inl_mem : Q inl + /-- Right tagging is admissible. -/ + inr_mem : Q inr + /-- Left tagging is injective. -/ + inl_inj : Function.Injective inl + /-- Right tagging is injective. -/ + inr_inj : Function.Injective inr + /-- The two tags are distinguishable. -/ + inl_ne_inr : ∀ w₁ w₂, inl w₁ ≠ inr w₂ + /-- Dispatch on the tag. -/ + elim : (W → W) → (W → W) → W → W + /-- Dispatch on admissible branches is admissible. -/ + elim_mem : ∀ {f g : W → W}, Q f → Q g → Q (elim f g) + /-- Dispatch takes the left branch on a left tag. -/ + elim_inl : ∀ (f g : W → W) (w : W), elim f g (inl w) = f w + /-- Dispatch takes the right branch on a right tag. -/ + elim_inr : ∀ (f g : W → W) (w : W), elim f g (inr w) = g w + /-- A distinguished word, used as the payload of the absent optional value. -/ + pt : W + /-- The constant map at the distinguished word is admissible. -/ + const_mem : Q fun _ => pt + +/-- Moving a tag past a pairing: the word-level content of distributivity. + +This datum is forced by the mathematics rather than by the presentation. +`WordTagging.elim` hands each branch only the *untagged* payload, so its branches +cannot see the surrounding context, and a tag therefore cannot be moved past a +pairing using `elim` alone. -/ +structure WordDistrib {W : Type u} (Q : (W → W) → Prop) (P : WordPairing Q) + (T : WordTagging Q) where + /-- Move the tag of a paired word's first component outwards. -/ + distrib : W → W + /-- The rearrangement is admissible. -/ + distrib_mem : Q distrib + /-- On a left tag. -/ + distrib_inl : ∀ w v, distrib (P.pair (T.inl w) v) = T.inl (P.pair w v) + /-- On a right tag. -/ + distrib_inr : ∀ w v, distrib (P.pair (T.inr w) v) = T.inr (P.pair w v) + +/-- The step class built from a class `Q` of word functions on `W` that contains +the identity and is closed under composition. + +A type is representable by an injective encoding into `W` — injectivity is the +only semantic demand, exactly as for a raw bit encoding — and a function is +admissible when some `Q`-function intertwines the encodings. -/ +def ofWordClass (W : Type u) (Q : (W → W) → Prop) (hid : Q id) + (hcomp : ∀ {f g : W → W}, Q f → Q g → Q (g ∘ f)) : StepClass.{u, u} where + Str A := { encode : A → W // Function.Injective encode } + Hom eA eB f := ∃ q : W → W, Q q ∧ ∀ x, q (eA.1 x) = eB.1 (f x) + id_mem _ := ⟨id, hid, fun _ => rfl⟩ + comp_mem := by + rintro A B D a b d f g ⟨qf, hqf, hfEq⟩ ⟨qg, hqg, hgEq⟩ + refine ⟨qg ∘ qf, hcomp hqf hqg, fun x => ?_⟩ + simp only [Function.comp_apply, hfEq, hgEq] + +/-- All the word-level data a monomorphic class needs in order to be a +distributive step class: identity and composition closure, a pairing codec, a +tagging scheme, and the tag-past-pairing rearrangement. + +Supplying one of these is what an external complexity library has to do. The four +`StepClass` mixins are then instances on `toStepClass`, so a client never has to +name them. -/ +structure WordClass (W : Type u) where + /-- Which word functions the class admits. -/ + Mem : (W → W) → Prop + /-- The identity is admissible. -/ + id_mem : Mem id + /-- Admissible word functions compose. -/ + comp_mem : ∀ {f g : W → W}, Mem f → Mem g → Mem (g ∘ f) + /-- A pairing codec. -/ + pairing : WordPairing Mem + /-- A tagging scheme. -/ + tagging : WordTagging Mem + /-- The tag-past-pairing rearrangement. -/ + distributor : WordDistrib Mem pairing tagging + +/-- The step class presented by a bundle of word-level data. -/ +@[reducible] def WordClass.toStepClass {W : Type u} (V : WordClass W) : + StepClass.{u, u} := + ofWordClass W V.Mem V.id_mem V.comp_mem + +/-- Products for a word class, from a pairing codec. -/ +@[reducible] def ofWordClass.hasProd {W : Type u} {Q : (W → W) → Prop} {hid : Q id} + {hcomp : ∀ {f g : W → W}, Q f → Q g → Q (g ∘ f)} + (P : WordPairing Q) : (ofWordClass W Q hid hcomp).HasProd where + prod a b := + ⟨fun x => P.pair (a.1 x.1) (b.1 x.2), by + rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ h + obtain ⟨h₁, h₂⟩ := P.pair_inj _ _ _ _ h + exact Prod.ext (a.2 h₁) (b.2 h₂)⟩ + fst_mem _ _ := ⟨P.fst, P.fst_mem, fun _ => P.fst_pair _ _⟩ + snd_mem _ _ := ⟨P.snd, P.snd_mem, fun _ => P.snd_pair _ _⟩ + pair_mem := by + rintro A B D a b d f g ⟨qf, hqf, hfEq⟩ ⟨qg, hqg, hgEq⟩ + refine ⟨fun w => P.pair (qf w) (qg w), P.pair_mem hqf hqg, fun x => ?_⟩ + change P.pair (qf (a.1 x)) (qg (a.1 x)) = P.pair (b.1 (f x)) (d.1 (g x)) + rw [hfEq, hgEq] + +/-- Sums for a word class, from a tagging scheme. -/ +@[reducible] def ofWordClass.hasSum {W : Type u} {Q : (W → W) → Prop} {hid : Q id} + {hcomp : ∀ {f g : W → W}, Q f → Q g → Q (g ∘ f)} + (T : WordTagging Q) : (ofWordClass W Q hid hcomp).HasSum where + sum a b := + ⟨Sum.elim (fun x => T.inl (a.1 x)) fun y => T.inr (b.1 y), by + rintro (x | x) (y | y) h + · exact congrArg Sum.inl (a.2 (T.inl_inj h)) + · exact absurd h (T.inl_ne_inr _ _) + · exact absurd h.symm (T.inl_ne_inr _ _) + · exact congrArg Sum.inr (b.2 (T.inr_inj h))⟩ + inl_mem _ _ := ⟨T.inl, T.inl_mem, fun _ => rfl⟩ + inr_mem _ _ := ⟨T.inr, T.inr_mem, fun _ => rfl⟩ + elim_mem := by + rintro A B D a b d f g ⟨qf, hqf, hfEq⟩ ⟨qg, hqg, hgEq⟩ + refine ⟨T.elim qf qg, T.elim_mem hqf hqg, fun x => ?_⟩ + cases x with + | inl x => + change T.elim qf qg (T.inl (a.1 x)) = d.1 (f x) + rw [T.elim_inl, hfEq] + | inr y => + change T.elim qf qg (T.inr (b.1 y)) = d.1 (g y) + rw [T.elim_inr, hgEq] + +section WordClassInstances + +variable {W : Type u} (V : WordClass W) + +instance WordClass.instHasProd : V.toStepClass.HasProd := + ofWordClass.hasProd V.pairing + +instance WordClass.instHasSum : V.toStepClass.HasSum := + ofWordClass.hasSum V.tagging + +/-- Optional values for a word class: the absent value is the right tag carrying +the distinguished word. + +`obindCtx_mem` needs the tag-past-pairing rearrangement, because sequencing must +inspect the tag of the first component while retaining the second. -/ +instance WordClass.instHasOption : V.toStepClass.HasOption where + option a := + ⟨fun o => o.elim (V.tagging.inr V.tagging.pt) fun x => V.tagging.inl (a.1 x), by + rintro (_ | x) (_ | y) h + · rfl + · exact absurd h.symm (V.tagging.inl_ne_inr _ _) + · exact absurd h (V.tagging.inl_ne_inr _ _) + · exact congrArg some (a.2 (V.tagging.inl_inj h))⟩ + omap_mem := by + rintro A B a b f ⟨qf, hqf, hfEq⟩ + refine ⟨V.tagging.elim (fun w => V.tagging.inl (qf w)) V.tagging.inr, + V.tagging.elim_mem (V.comp_mem hqf V.tagging.inl_mem) V.tagging.inr_mem, fun o => ?_⟩ + cases o with + | none => + change V.tagging.elim _ _ (V.tagging.inr V.tagging.pt) = V.tagging.inr V.tagging.pt + rw [V.tagging.elim_inr] + | some x => + change V.tagging.elim _ _ (V.tagging.inl (a.1 x)) = V.tagging.inl (b.1 (f x)) + rw [V.tagging.elim_inl, hfEq] + none_mem a b := + ⟨fun _ => V.tagging.inr V.tagging.pt, + V.comp_mem V.tagging.const_mem V.tagging.inr_mem, fun _ => rfl⟩ + obindCtx_mem := by + rintro A B E a b e k ⟨qk, hqk, hkEq⟩ + refine ⟨V.tagging.elim qk (fun _ => V.tagging.inr V.tagging.pt) ∘ + V.distributor.distrib, + V.comp_mem V.distributor.distrib_mem + (V.tagging.elim_mem hqk (V.comp_mem V.tagging.const_mem V.tagging.inr_mem)), + fun y => ?_⟩ + obtain ⟨o, v⟩ := y + cases o with + | none => + change V.tagging.elim _ _ + (V.distributor.distrib (V.pairing.pair (V.tagging.inr V.tagging.pt) + (e.1 v))) = V.tagging.inr V.tagging.pt + rw [V.distributor.distrib_inr, V.tagging.elim_inr] + | some j => + change V.tagging.elim _ _ + (V.distributor.distrib (V.pairing.pair (V.tagging.inl (a.1 j)) + (e.1 v))) = _ + rw [V.distributor.distrib_inl, V.tagging.elim_inl] + exact hkEq (j, v) + +/-- Distributivity for a word class: exactly the tag-past-pairing +rearrangement. -/ +instance WordClass.instIsDistributive : V.toStepClass.IsDistributive where + distrib_mem a b i := by + refine ⟨V.distributor.distrib, V.distributor.distrib_mem, fun x => ?_⟩ + obtain ⟨s, v⟩ := x + cases s with + | inl l => + change V.distributor.distrib + (V.pairing.pair (V.tagging.inl (a.1 l)) (i.1 v)) = + V.tagging.inl (V.pairing.pair (a.1 l) (i.1 v)) + rw [V.distributor.distrib_inl] + | inr r => + change V.distributor.distrib + (V.pairing.pair (V.tagging.inr (b.1 r)) (i.1 v)) = + V.tagging.inr (V.pairing.pair (b.1 r) (i.1 v)) + rw [V.distributor.distrib_inr] + +end WordClassInstances + +end StepClass + +namespace DynSystem.DynComputation + +variable {p : PFunctor.{u, u}} {α β : Type u} + +/-! ## Non-vacuity -/ + +/-- The boundary carrying no information, over the unconstrained class. -/ +def Boundary.unconstrained (p : PFunctor.{u, u}) (α β : Type u) : + Boundary StepClass.unconstrained.{u, v} p α β := + ⟨PUnit.unit, PUnit.unit, PUnit.unit, PUnit.unit⟩ + +/-- Non-vacuity of the whole layer: with no constraint on the step maps, +realizability is exactly plain implementability, and every well-founded program +family is realized — by the canonical machine whose states are the residual +programs. + +Any *failure* of realizability is therefore attributable to the step class, never +to the shape of the definition. -/ +theorem isRealizableBy_unconstrained [DecidableEq p.A] (program : α → FreeM p β) : + IsRealizableBy StepClass.unconstrained.{u, v} + (Boundary.unconstrained p α β) program := + ⟨⟨ofFreeM program, PUnit.unit, True.intro, True.intro, True.intro⟩, + implements_ofFreeM program⟩ + +/-! ## Finite-state realizability -/ + +/-- Finite-state realizability: the program family is implemented by a machine +with a finite state set. This is the notion Church's synthesis problem asks about, +and the specialization of `IsRealizableBy` at `StepClass.finite`. -/ +abbrev IsFiniteStateRealizable [DecidableEq p.A] + (bd : Boundary StepClass.finite.{u} p α β) (program : α → FreeM p β) : Prop := + IsRealizableBy StepClass.finite bd program + +/-- Finite-state realizability within a budget bounds the program's query depth. +The machine's finiteness plays no part: the bound is carried by the budget. -/ +theorem IsFiniteStateRealizable.isTotalRollBound [DecidableEq p.A] + {bd : Boundary StepClass.finite.{u} p α β} {program : α → FreeM p β} {k : ℕ} + (h : IsRealizableWithin StepClass.finite bd program k) (input : α) : + (program input).IsTotalRollBound k := + h.isTotalRollBound input + +end DynSystem.DynComputation + +end PFunctor diff --git a/PolyFun/Realizability/Machine.lean b/PolyFun/Realizability/Machine.lean new file mode 100644 index 0000000..86e0cd9 --- /dev/null +++ b/PolyFun/Realizability/Machine.lean @@ -0,0 +1,535 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.PFunctor.Dynamical.DynComputation.Bounded + +/-! +# First-order step maps of a returning dynamical computation + +A `DynComputation`'s dynamics are carried by `view`, whose codomain +`β ⊕ p.Obj State` stores a *function-valued* continuation and whose second +component is dependent on the exposed position. Neither shape can be constrained +by a predicate on plain functions. This module presents the same dynamics as +first-order maps between plain types: + +* `head : State → β ⊕ p.A` — the one-step readout: the value returned at a + resolved state, or the query position exposed at an unresolved one. This is + *definitionally* the position map of the computation's underlying lens. +* `update? : State × p.Idx → Option State` — the continuation, flattened onto the + whole index space `p.Idx = Σ a, p.B a`. `none` means the pair is not a step the + computation can take: the state has already returned, or the answer is tagged + with a position the computation is not exposing. + +**Partiality is load-bearing.** The total variant `updateFlat`, which collapses +`none` to the unchanged state, does not compose across a state coproduct with a +handoff: at a left state whose intermediate value has been handed to the second +phase, a mismatched tag leaves the composite in the *left* summand while the +second phase alone would stay at its own initial state. Reconciling those junk +values would require the ambient class to contain a decidable-equality test on +interface positions. With `none` they agree, and `update?_seqComp_inl` becomes an +equation unconditional in the answer index. + +Nothing constrains where `none` occurs beyond what the semantics forces, and the +run semantics never feeds a direction at a position other than the exposed one, so +the flattening carries no coherence side conditions — the only cost is +`DecidableEq p.A`. + +`updateFlat`, `output`, `expose`, and `stepD` are the derived accessors a +machine-facing cost model consumes: a total state-to-state transition, an optional +readout, a total query selector, and the deterministic one-step transition against +a fixed pure handler. + +`ofStep_step_eq_of_flat_eq` records that the presentation is faithful: a step +function is determined by the `head` and `update?` it induces, so constraining +those two maps (plus `init`) is a constraint on the machine itself and not on an +arbitrary projection of it. + +Every map here is spelled with `Sum` and `Option` combinators rather than with +`match`. An auto-generated matcher abstracts the computation and blocks +unification across distinct input types, whereas combinator applications reduce +by congruence over the shared `view`; that is exactly why the `setInit` +transport lemmas below hold by `rfl`. +-/ + +@[expose] public section + +universe u v w uA uB uA₂ uB₂ uα uβ uγ + +namespace PFunctor + +namespace DynSystem.DynComputation + +variable {p : PFunctor.{uA, uB}} {α : Type uα} {β : Type uβ} + +/-! ## The one-step readout -/ + +/-- The one-step readout of a returning computation: the value returned at a +resolved state, or the query position exposed at an unresolved one. + +This is exactly the position map of the computation's underlying lens, so +computations sharing `toMachine` share it definitionally, and interface or +result transport act on it by plain post-composition. -/ +def head (M : DynComputation.{u} p α β) : M.State → β ⊕ p.A := + M.toDynSystem.expose + +theorem head_def (M : DynComputation.{u} p α β) (state : M.State) : + M.head state = M.toDynSystem.expose state := rfl + +private theorem sumMap_fst_unpack {X : Type w} + (step : (C.{uβ, uB} β + p).Obj X) : + Sum.map id Sigma.fst (Resumption.unpack (β := β) step) = step.1 := by + rcases step with ⟨position, next⟩ + cases position <;> rfl + +/-- The readout is the position component of the one-step view: it forgets the +continuation and keeps the returned value or the exposed position. -/ +theorem head_eq_sumMap_view (M : DynComputation.{u} p α β) (state : M.State) : + M.head state = Sum.map id Sigma.fst (M.view state) := + (sumMap_fst_unpack (M.toDynSystem.out state)).symm + +theorem head_eq_inl_of_view (M : DynComputation.{u} p α β) + {state : M.State} {value : β} (hview : M.view state = Sum.inl value) : + M.head state = Sum.inl value := by + rw [head_eq_sumMap_view, hview]; rfl + +theorem head_eq_inr_of_view (M : DynComputation.{u} p α β) + {state : M.State} {query : p.Obj M.State} + (hview : M.view state = Sum.inr query) : + M.head state = Sum.inr query.1 := by + rw [head_eq_sumMap_view, hview]; rfl + +/-! ## The flattened transition -/ + +/-- The continuation of a returning computation, flattened onto the whole index +space as a *partial* function. + +`none` means the pair is not a step the computation can take: the state has +already returned, or the answer is tagged with a position the computation is not +exposing. `some state'` means the answer is one the computation is waiting for and +`state'` is where it goes. + +Partiality is what makes the flattening compositional. The total variant +`updateFlat` collapses `none` to the unchanged state, which suits a cost model +that wants a plain state-to-state map, but does not compose across a state +coproduct with a handoff: at a left state whose intermediate value has been handed +over, the composite stays in the left summand on a mismatched tag while the second +phase alone would stay at its own initial state. With `none` both are `none`. -/ +def update? [DecidableEq p.A] (M : DynComputation.{u} p α β) : + M.State × p.Idx → Option M.State := fun step => + (M.view step.1).elim (fun _ => none) + (fun query => + if h : step.2.1 = query.1 then some (query.2 (h ▸ step.2.2)) else none) + +theorem update?_of_view_return [DecidableEq p.A] (M : DynComputation.{u} p α β) + {state : M.State} {value : β} (hview : M.view state = Sum.inl value) + (index : p.Idx) : M.update? (state, index) = none := by + unfold update?; rw [hview]; rfl + +theorem update?_of_view_query [DecidableEq p.A] (M : DynComputation.{u} p α β) + {state : M.State} {position : p.A} {next : p.B position → M.State} + (hview : M.view state = Sum.inr ⟨position, next⟩) + (direction : p.B position) : + M.update? (state, ⟨position, direction⟩) = some (next direction) := by + unfold update?; rw [hview] + simp only [Sum.elim_inr, dif_pos] + +theorem update?_of_view_query_of_ne [DecidableEq p.A] + (M : DynComputation.{u} p α β) {state : M.State} {query : p.Obj M.State} + (hview : M.view state = Sum.inr query) {index : p.Idx} + (hne : index.1 ≠ query.1) : M.update? (state, index) = none := by + unfold update?; rw [hview] + simp only [Sum.elim_inr, dif_neg hne] + +/-- The total variant of the flattened transition: a mismatched tag or an already +returned state leaves the state unchanged. + +This is the shape a machine-facing cost model wants, since it is a plain +state-to-state map. It is derived from `update?`, so the two never disagree about +which answers are steps. -/ +def updateFlat [DecidableEq p.A] (M : DynComputation.{u} p α β) + (step : M.State × p.Idx) : M.State := + (M.update? step).getD step.1 + +theorem updateFlat_eq_getD [DecidableEq p.A] (M : DynComputation.{u} p α β) + (step : M.State × p.Idx) : + M.updateFlat step = (M.update? step).getD step.1 := rfl + +theorem updateFlat_of_view_return [DecidableEq p.A] (M : DynComputation.{u} p α β) + {state : M.State} {value : β} (hview : M.view state = Sum.inl value) + (index : p.Idx) : M.updateFlat (state, index) = state := by + unfold updateFlat; rw [M.update?_of_view_return hview index]; rfl + +theorem updateFlat_of_view_query [DecidableEq p.A] (M : DynComputation.{u} p α β) + {state : M.State} {position : p.A} {next : p.B position → M.State} + (hview : M.view state = Sum.inr ⟨position, next⟩) + (direction : p.B position) : + M.updateFlat (state, ⟨position, direction⟩) = next direction := by + unfold updateFlat; rw [M.update?_of_view_query hview direction]; rfl + +theorem updateFlat_of_view_query_of_ne [DecidableEq p.A] + (M : DynComputation.{u} p α β) {state : M.State} {query : p.Obj M.State} + (hview : M.view state = Sum.inr query) {index : p.Idx} + (hne : index.1 ≠ query.1) : M.updateFlat (state, index) = state := by + unfold updateFlat; rw [M.update?_of_view_query_of_ne hview hne]; rfl + +/-! ## Derived machine-facing accessors -/ + +/-- The optional readout of a returning computation: the returned value at a +resolved state and `none` at an unresolved one. -/ +def output (M : DynComputation.{u} p α β) (state : M.State) : Option β := + (M.head state).getLeft? + +/-- The query a computation selects at a state. At a resolved state, where no +query is exposed, this is the interface's default position; the run semantics +never consults that value. -/ +def expose [Inhabited p.A] (M : DynComputation.{u} p α β) (state : M.State) : p.A := + (M.head state).elim (fun _ => default) id + +/-- The deterministic one-step transition of a computation against a fixed pure +handler. A resolved state is absorbing. -/ +def stepD (M : DynComputation.{u} p α β) (handler : (a : p.A) → p.B a) + (state : M.State) : M.State := + (M.view state).elim (fun _ => state) (fun query => query.2 (handler query.1)) + +@[simp] theorem output_eq_some_iff (M : DynComputation.{u} p α β) + (state : M.State) (value : β) : + M.output state = some value ↔ M.head state = Sum.inl value := by + unfold output + cases M.head state <;> simp + +@[simp] theorem stepD_of_view_return (M : DynComputation.{u} p α β) + (handler : (a : p.A) → p.B a) {state : M.State} {value : β} + (hview : M.view state = Sum.inl value) : M.stepD handler state = state := by + unfold stepD; rw [hview]; rfl + +@[simp] theorem stepD_of_view_query (M : DynComputation.{u} p α β) + (handler : (a : p.A) → p.B a) {state : M.State} {query : p.Obj M.State} + (hview : M.view state = Sum.inr query) : + M.stepD handler state = query.2 (handler query.1) := by + unfold stepD; rw [hview]; rfl + +/-! ## Transport along replacement of the initialization + +Every step map is shared definitionally by computations that share `toMachine`. +-/ + +@[simp] theorem head_setInit {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (state : M.State) : + (M.setInit g).head state = M.head state := rfl + +@[simp] theorem update?_setInit [DecidableEq p.A] {γ : Type uγ} + (M : DynComputation.{u} p α β) (g : γ → M.State) (step : M.State × p.Idx) : + (M.setInit g).update? step = M.update? step := rfl + +@[simp] theorem updateFlat_setInit [DecidableEq p.A] {γ : Type uγ} + (M : DynComputation.{u} p α β) (g : γ → M.State) (step : M.State × p.Idx) : + (M.setInit g).updateFlat step = M.updateFlat step := rfl + +@[simp] theorem output_setInit {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (state : M.State) : + (M.setInit g).output state = M.output state := rfl + +@[simp] theorem expose_setInit [Inhabited p.A] {γ : Type uγ} + (M : DynComputation.{u} p α β) (g : γ → M.State) (state : M.State) : + (M.setInit g).expose state = M.expose state := rfl + +@[simp] theorem stepD_setInit {γ : Type uγ} (M : DynComputation.{u} p α β) + (g : γ → M.State) (handler : (a : p.A) → p.B a) (state : M.State) : + (M.setInit g).stepD handler state = M.stepD handler state := rfl + +/-! ## Transport along result mapping -/ + +@[simp] theorem head_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β) + (f : β → γ) (state : M.State) : + (M.mapResult f).head state = Sum.map f id (M.head state) := rfl + +@[simp] theorem update?_mapResult [DecidableEq p.A] {γ : Type uγ} + (M : DynComputation.{u} p α β) (f : β → γ) (step : M.State × p.Idx) : + (M.mapResult f).update? step = M.update? step := by + unfold update? + rw [mapResult_view] + cases hview : M.view step.1 with + | inl value => rfl + | inr query => rfl + +@[simp] theorem updateFlat_mapResult [DecidableEq p.A] {γ : Type uγ} + (M : DynComputation.{u} p α β) (f : β → γ) (step : M.State × p.Idx) : + (M.mapResult f).updateFlat step = M.updateFlat step := by + unfold updateFlat + rw [M.update?_mapResult f step] + rfl + +/-! ## Transport along interface transport -/ + +@[simp] theorem head_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β) + (lens : Lens p q) (state : M.State) : + (M.wrap lens).head state = Sum.map id lens.toFunA (M.head state) := rfl + +/-- The flattened index pullback of a lens, absorbing the resolved case: an answer +at the position the lens exposes for `a` is pulled back to an answer at `a`, while +a resolved readout or a mismatched tag has no preimage. + +The domain carries the machine's whole readout `β ⊕ p.A` rather than just a +position. Absorbing the resolved case here is what lets interface transport avoid +`expose` and hence avoid needing an admissible constant `default`. -/ +def _root_.PFunctor.Lens.pullHeadIdx {q : PFunctor.{uA₂, uB₂}} [DecidableEq q.A] + (lens : Lens p q) (β : Type uβ) : (β ⊕ p.A) × q.Idx → Option p.Idx := fun x => + x.1.elim (fun _ => none) + (fun a => + if h : x.2.1 = lens.toFunA a then + some ⟨a, lens.toFunB a (h ▸ x.2.2)⟩ + else none) + +/-- Interface transport pulls an answer back along the lens before feeding it to +the underlying computation. The resolved case needs no special handling: the +underlying `update?` is already `none` there. -/ +theorem update?_wrap {q : PFunctor.{uA₂, uB₂}} [DecidableEq p.A] [DecidableEq q.A] + (M : DynComputation.{u} p α β) (lens : Lens p q) (state : M.State) + (iposition : q.A) (idirection : q.B iposition) : + (M.wrap lens).update? (state, ⟨iposition, idirection⟩) = + (lens.pullHeadIdx β (M.head state, ⟨iposition, idirection⟩)).bind + fun index => M.update? (state, index) := by + cases hview : M.view state with + | inl value => + rw [update?_of_view_return (M.wrap lens) + (show (M.wrap lens).view state = Sum.inl value by rw [wrap_view, hview]) + ⟨iposition, idirection⟩, + head_eq_inl_of_view M hview] + rfl + | inr query => + rcases query with ⟨position, next⟩ + have hcomp : (M.wrap lens).view state = + Sum.inr ⟨lens.toFunA position, + fun direction => next (lens.toFunB position direction)⟩ := by + rw [wrap_view, hview] + rw [head_eq_inr_of_view M hview] + by_cases h : iposition = lens.toFunA position + · subst h + rw [update?_of_view_query (M.wrap lens) hcomp idirection] + change _ = Option.bind (dite _ _ _) _ + rw [dif_pos rfl, Option.bind_some, update?_of_view_query M hview] + rfl + · rw [update?_of_view_query_of_ne (M.wrap lens) hcomp h] + change none = Option.bind (dite _ _ _) _ + rw [dif_neg h] + rfl + +/-! ## The step maps of a sequential composition -/ + +section SeqComp + +variable {γ : Type uγ} + +theorem seqComp_view_inl_of_return (M₁ : DynComputation.{u} p α β) + (M₂ : DynComputation.{v} p β γ) {state₁ : M₁.State} {value : β} + (hview : M₁.view state₁ = Sum.inl value) : + (M₁.seqComp M₂).view (Sum.inl state₁) = + Sum.map (fun result : γ => result) + (p.map (Sum.inr : M₂.State → M₁.State ⊕ M₂.State)) + (M₂.view (M₂.init value)) := by + rw [seqComp_view_inl, hview] + rfl + +theorem seqComp_view_inl_of_query (M₁ : DynComputation.{u} p α β) + (M₂ : DynComputation.{v} p β γ) {state₁ : M₁.State} + {position : p.A} {next : p.B position → M₁.State} + (hview : M₁.view state₁ = Sum.inr ⟨position, next⟩) : + (M₁.seqComp M₂).view (Sum.inl state₁) = + Sum.inr ⟨position, fun direction => Sum.inl (next direction)⟩ := by + rw [seqComp_view_inl, hview] + rfl + +@[simp] theorem head_seqComp_inr (M₁ : DynComputation.{u} p α β) + (M₂ : DynComputation.{v} p β γ) (state₂ : M₂.State) : + (M₁.seqComp M₂).head (Sum.inr state₂) = M₂.head state₂ := by + rw [head_eq_sumMap_view (M₁.seqComp M₂) (Sum.inr state₂), seqComp_view_inr, + head_eq_sumMap_view M₂ state₂] + cases M₂.view state₂ <;> rfl + +/-- At a left state the composite reads off `M₁`; a returned intermediate value +is handed over to `M₂`'s initial readout in the same observation. -/ +@[simp] theorem head_seqComp_inl (M₁ : DynComputation.{u} p α β) + (M₂ : DynComputation.{v} p β γ) (state₁ : M₁.State) : + (M₁.seqComp M₂).head (Sum.inl state₁) = + Sum.elim (fun value => M₂.head (M₂.init value)) Sum.inr (M₁.head state₁) := by + rw [head_eq_sumMap_view (M₁.seqComp M₂) (Sum.inl state₁)] + cases hview : M₁.view state₁ with + | inl value => + rw [seqComp_view_inl_of_return M₁ M₂ hview, head_eq_inl_of_view M₁ hview, + Sum.elim_inl, head_eq_sumMap_view M₂ (M₂.init value)] + cases M₂.view (M₂.init value) <;> rfl + | inr query => + rcases query with ⟨position, next⟩ + rw [seqComp_view_inl_of_query M₁ M₂ hview, head_eq_inr_of_view M₁ hview] + rfl + +@[simp] theorem update?_seqComp_inr [DecidableEq p.A] + (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ) + (state₂ : M₂.State) (index : p.Idx) : + (M₁.seqComp M₂).update? (Sum.inr state₂, index) = + Option.map Sum.inr (M₂.update? (state₂, index)) := by + obtain ⟨position, direction⟩ := index + cases hview : M₂.view state₂ with + | inl value => + rw [update?_of_view_return (M₁.seqComp M₂) + (show (M₁.seqComp M₂).view (Sum.inr state₂) = Sum.inl value by + rw [seqComp_view_inr, hview]; rfl), + update?_of_view_return M₂ hview] + rfl + | inr query => + rcases query with ⟨position₂, next₂⟩ + have hcomp : (M₁.seqComp M₂).view (Sum.inr state₂) = + Sum.inr ⟨position₂, fun direction => Sum.inr (next₂ direction)⟩ := by + rw [seqComp_view_inr, hview]; rfl + by_cases h : position = position₂ + · subst h + rw [update?_of_view_query (M₁.seqComp M₂) hcomp direction, + update?_of_view_query M₂ hview direction] + rfl + · rw [update?_of_view_query_of_ne (M₁.seqComp M₂) hcomp h, + update?_of_view_query_of_ne M₂ hview h] + rfl + +/-- At a left state the composite advances `M₁`, unless `M₁` has already returned +an intermediate value, in which case control has been handed to `M₂` initialized +at that value. + +This equation is **unconditional in the answer index**, which is exactly what +partiality buys. With the total `updateFlat` no such equation holds: on a +mismatched tag the composite stays at `Sum.inl state₁` while `M₂` alone would stay +at `M₂.init value`. With `none` both agree, and the case where `M₂` also returns +immediately is subsumed for the same reason. + +So this single lemma covers what the total variant needed three conditional ones +for — a matching-tag case, a mismatched-tag case, and a both-phases-returned case. +Only the two uniform total-variant lemmas are kept below; +`updateFlat_eq_getD` recovers the rest. -/ +@[simp] theorem update?_seqComp_inl [DecidableEq p.A] + (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ) + (state₁ : M₁.State) (index : p.Idx) : + (M₁.seqComp M₂).update? (Sum.inl state₁, index) = + Sum.elim (fun value => Option.map Sum.inr (M₂.update? (M₂.init value, index))) + (fun _ : p.A => Option.map Sum.inl (M₁.update? (state₁, index))) + (M₁.head state₁) := by + obtain ⟨position, direction⟩ := index + cases hview : M₁.view state₁ with + | inr query => + rcases query with ⟨position₁, next₁⟩ + rw [head_eq_inr_of_view M₁ hview, Sum.elim_inr] + have hcomp := seqComp_view_inl_of_query M₁ M₂ hview + by_cases h : position = position₁ + · subst h + rw [update?_of_view_query (M₁.seqComp M₂) hcomp direction, + update?_of_view_query M₁ hview direction] + rfl + · rw [update?_of_view_query_of_ne (M₁.seqComp M₂) hcomp h, + update?_of_view_query_of_ne M₁ hview h] + rfl + | inl value => + rw [head_eq_inl_of_view M₁ hview, Sum.elim_inl] + cases hview₂ : M₂.view (M₂.init value) with + | inl result => + rw [update?_of_view_return (M₁.seqComp M₂) (value := result) + (by rw [seqComp_view_inl_of_return M₁ M₂ hview, hview₂]; rfl), + update?_of_view_return M₂ hview₂] + rfl + | inr query₂ => + rcases query₂ with ⟨position₂, next₂⟩ + have hcomp : (M₁.seqComp M₂).view (Sum.inl state₁) = + Sum.inr ⟨position₂, fun d => Sum.inr (next₂ d)⟩ := by + rw [seqComp_view_inl_of_return M₁ M₂ hview, hview₂]; rfl + by_cases h : position = position₂ + · subst h + rw [update?_of_view_query (M₁.seqComp M₂) hcomp direction, + update?_of_view_query M₂ hview₂ direction] + rfl + · rw [update?_of_view_query_of_ne (M₁.seqComp M₂) hcomp h, + update?_of_view_query_of_ne M₂ hview₂ h] + rfl + +@[simp] theorem updateFlat_seqComp_inr [DecidableEq p.A] + (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ) + (state₂ : M₂.State) (index : p.Idx) : + (M₁.seqComp M₂).updateFlat (Sum.inr state₂, index) = + Sum.inr (M₂.updateFlat (state₂, index)) := by + unfold updateFlat + rw [update?_seqComp_inr] + cases M₂.update? (state₂, index) <;> rfl + +/-- At a left state exposing a query, the composite advances `M₁` inside the left +summand. -/ +theorem updateFlat_seqComp_inl_of_query [DecidableEq p.A] + (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ) + {state₁ : M₁.State} {position₁ : p.A} {next₁ : p.B position₁ → M₁.State} + (hview : M₁.view state₁ = Sum.inr ⟨position₁, next₁⟩) (index : p.Idx) : + (M₁.seqComp M₂).updateFlat (Sum.inl state₁, index) = + Sum.inl (M₁.updateFlat (state₁, index)) := by + unfold updateFlat + rw [update?_seqComp_inl, head_eq_inr_of_view M₁ hview, Sum.elim_inr] + cases M₁.update? (state₁, index) <;> rfl + +end SeqComp + +/-! ## Faithfulness of the flat presentation + +The flat step maps lose nothing: a step function is determined by the readout and +the partial transition it induces. So presenting a computation by +`(State, init, head, update?)` is a genuine presentation rather than a lossy +projection — which is why constraining those three maps is the right notion of an +admissible machine. +-/ + +/-- A step function is determined by the readout and the partial transition it +induces. -/ +theorem ofStep_step_eq_of_flat_eq [DecidableEq p.A] {S : Type u} + (step₁ step₂ : S → β ⊕ p.Obj S) (init : α → S) + (hhead : ∀ state, (ofStep (p := p) step₁ init).head state = + (ofStep (p := p) step₂ init).head state) + (hupdate : ∀ pair, (ofStep (p := p) step₁ init).update? pair = + (ofStep (p := p) step₂ init).update? pair) : + step₁ = step₂ := by + funext state + have hview₁ : (ofStep (p := p) step₁ init).view state = step₁ state := + view_ofStep step₁ init state + have hview₂ : (ofStep (p := p) step₂ init).view state = step₂ state := + view_ofStep step₂ init state + have hpos := hhead state + rw [head_eq_sumMap_view, head_eq_sumMap_view, hview₁, hview₂] at hpos + cases h₁ : step₁ state with + | inl value₁ => + cases h₂ : step₂ state with + | inl value₂ => + rw [h₁, h₂] at hpos + change Sum.inl value₁ = Sum.inl value₂ at hpos + rw [Sum.inl.inj hpos] + | inr query₂ => + rw [h₁, h₂] at hpos + change Sum.inl value₁ = Sum.inr query₂.1 at hpos + exact absurd hpos (by simp) + | inr query₁ => + cases h₂ : step₂ state with + | inl value₂ => + rw [h₁, h₂] at hpos + change Sum.inr query₁.1 = Sum.inl value₂ at hpos + exact absurd hpos (by simp) + | inr query₂ => + rcases query₁ with ⟨position₁, next₁⟩ + rcases query₂ with ⟨position₂, next₂⟩ + have hposEq : position₁ = position₂ := by + rw [h₁, h₂] at hpos + change Sum.inr position₁ = Sum.inr position₂ at hpos + exact Sum.inr.inj hpos + subst hposEq + refine congrArg Sum.inr (Sigma.ext rfl (heq_of_eq (funext fun d => ?_))) + have := hupdate (state, ⟨position₁, d⟩) + rw [update?_of_view_query _ (hview₁.trans h₁) d, + update?_of_view_query _ (hview₂.trans h₂) d] at this + exact Option.some.inj this + +end DynSystem.DynComputation + +end PFunctor diff --git a/PolyFun/Realizability/StepClass.lean b/PolyFun/Realizability/StepClass.lean new file mode 100644 index 0000000..618c183 --- /dev/null +++ b/PolyFun/Realizability/StepClass.lean @@ -0,0 +1,355 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.PFunctor.Basic + +/-! +# Classes of admissible functions + +A `PFunctor.StepClass` is a class of allowed data representations and functions +between them — a wide subcategory of `Type u`, presented pointwise by + +* `Str A`, the structure a type must carry to be representable (a bit encoding, + a finiteness witness, a `Primcodable` instance, …), and +* `Hom a b f`, the proposition that `f : A → B` is admissible between chosen + representations, + +closed under identities and composition. + +`Str` is *data* rather than a proposition because a resource bound only makes +sense relative to a chosen representation: "`f` runs in polynomial time" is a +statement about encoded inputs, not about the bare function. `Hom` is a +proposition because the realizability layer only ever asks *whether* a step map +is admissible; a cost-bearing refinement, in which witnesses carry running-time +and description-size measures, would replace it by a `Type`-valued field. + +The mixin classes `StepClass.HasProd` and `StepClass.HasSum` record that a class +represents binary products and sums with admissible projections, injections, +pairing, and case analysis. They are kept separate from `StepClass` so that each +downstream definition requires exactly the structure it consumes. + +`StepClass.Refines C D` translates `C`-representations into `D`-representations +compatibly with admissibility, so a statement proved for a small class +specializes to every larger one. + +This file is deliberately free of polynomial-functor content beyond its +namespace: the interface between a step class and the machine layer lives in +`PolyFun.Realizability.Basic`. + +Taking the resource bound as a predicate on the implementation, rather than as a +measure on runs, follows Petcher and Morrisett's Foundational Cryptography +Framework (2015), where security definitions are parameterized by an +*admissibility predicate* naming the class of allowed adversaries; the +`admissible` / `_mem` vocabulary here is theirs. See `REFERENCES.md`. +-/ + +@[expose] public section + +universe u v v₂ v₃ + +namespace PFunctor + +set_option linter.checkUnivs false in +/-- A class of admissible data representations and functions between them: a wide +subcategory of `Type u` presented by a structure on objects and a predicate on +morphisms. + +`Str A` is the representation structure carried by an admissible type, and +`Hom a b f` says that `f` is admissible from representation `a` to +representation `b`. The two closure fields make the admissible functions a +category containing every identity. -/ +-- The representation universe `v` is independent of the represented universe `u`: +-- a `Type`-valued encoding structure must be usable on types in any universe. +structure StepClass where + /-- The representation structure an admissible type must carry. -/ + Str : Type u → Type v + /-- Admissibility of a function between represented types. -/ + Hom : {A B : Type u} → Str A → Str B → (A → B) → Prop + /-- Identities are admissible. -/ + id_mem : ∀ {A : Type u} (a : Str A), Hom a a id + /-- Admissible functions compose. -/ + comp_mem : ∀ {A B D : Type u} {a : Str A} {b : Str B} {d : Str D} + {f : A → B} {g : B → D}, Hom a b f → Hom b d g → Hom a d (g ∘ f) + +namespace StepClass + +variable {C : StepClass.{u, v}} + +/-- Admissibility depends on a function only through its values: a class +constrains functions, not their syntactic presentation. + +This is the workhorse of the realizability closure theory, where a step map of a +composite machine is almost never *syntactically* the admissible combination one +builds by hand. -/ +theorem Hom.congr {A B : Type u} {a : C.Str A} {b : C.Str B} {f g : A → B} + (h : C.Hom a b f) (hfg : ∀ x, f x = g x) : C.Hom a b g := by + rwa [← funext hfg] + +/-! ## Products -/ + +/-- A step class with admissible binary products. + +The realizability layer requires this of every class it uses: the flattened +transition map of a machine is a function out of the product of the state with +the interface's index space. -/ +class HasProd (C : StepClass.{u, v}) where + /-- The representation of a binary product. -/ + prod : {A B : Type u} → C.Str A → C.Str B → C.Str (A × B) + /-- The first projection is admissible. -/ + fst_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom (prod a b) a Prod.fst + /-- The second projection is admissible. -/ + snd_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom (prod a b) b Prod.snd + /-- Admissible functions out of a common source pair. -/ + pair_mem : ∀ {A B D : Type u} {a : C.Str A} {b : C.Str B} {d : C.Str D} + {f : A → B} {g : A → D}, C.Hom a b f → C.Hom a d g → + C.Hom a (prod b d) fun x => (f x, g x) + +/-- Admissible functions act on products componentwise. -/ +theorem HasProd.map_mem [P : C.HasProd] {A B A' B' : Type u} {a : C.Str A} + {b : C.Str B} {a' : C.Str A'} {b' : C.Str B'} {f : A → A'} {g : B → B'} + (hf : C.Hom a a' f) (hg : C.Hom b b' g) : + C.Hom (P.prod a b) (P.prod a' b') (Prod.map f g) := by + refine (P.pair_mem (C.comp_mem (P.fst_mem a b) hf) + (C.comp_mem (P.snd_mem a b) hg)).congr ?_ + intro x + cases x + rfl + +/-- Pairing an admissible function with a fixed second component. -/ +theorem HasProd.pairRight_mem [P : C.HasProd] {A B D : Type u} {a : C.Str A} + {b : C.Str B} {d : C.Str D} {f : A → B} (hf : C.Hom a b f) : + C.Hom (P.prod a d) (P.prod b d) fun x => (f x.1, x.2) := + P.pair_mem (C.comp_mem (P.fst_mem a d) hf) (P.snd_mem a d) + +/-- Pairing an admissible function with a fixed first component. -/ +theorem HasProd.pairLeft_mem [P : C.HasProd] {A B D : Type u} {a : C.Str A} + {b : C.Str B} {d : C.Str D} {f : A → B} (hf : C.Hom a b f) : + C.Hom (P.prod d a) (P.prod d b) fun x => (x.1, f x.2) := + P.pair_mem (P.fst_mem d a) (C.comp_mem (P.snd_mem d a) hf) + +/-- Duplicating a value is admissible. This is what lets a closure proof retain +an input while dispatching on some function of it. -/ +theorem HasProd.diag_mem [P : C.HasProd] {A : Type u} (a : C.Str A) : + C.Hom a (P.prod a a) fun x => (x, x) := + P.pair_mem (C.id_mem a) (C.id_mem a) + +/-- Retaining an input alongside an admissible readout of it. -/ +theorem HasProd.withInput_mem [P : C.HasProd] {A B : Type u} {a : C.Str A} + {b : C.Str B} {f : A → B} (hf : C.Hom a b f) : + C.Hom a (P.prod b a) fun x => (f x, x) := + P.pair_mem hf (C.id_mem a) + +/-- Swapping the components of a product is admissible. -/ +theorem HasProd.swap_mem [P : C.HasProd] {A B : Type u} (a : C.Str A) + (b : C.Str B) : C.Hom (P.prod a b) (P.prod b a) Prod.swap := by + refine (P.pair_mem (P.snd_mem a b) (P.fst_mem a b)).congr ?_ + intro x + cases x + rfl + +/-- Reassociating a product is admissible. -/ +theorem HasProd.assoc_mem [P : C.HasProd] {A B D : Type u} (a : C.Str A) + (b : C.Str B) (d : C.Str D) : + C.Hom (P.prod (P.prod a b) d) (P.prod a (P.prod b d)) + fun x => (x.1.1, (x.1.2, x.2)) := + P.pair_mem (C.comp_mem (P.fst_mem (P.prod a b) d) (P.fst_mem a b)) + (P.pair_mem (C.comp_mem (P.fst_mem (P.prod a b) d) (P.snd_mem a b)) + (P.snd_mem (P.prod a b) d)) + +/-! ## Sums -/ + +/-- A step class with admissible binary sums. + +The realizability layer requires this of every class it uses: a machine's +one-step readout lands in `β ⊕ p.A`, a returned value or an exposed query +position. -/ +class HasSum (C : StepClass.{u, v}) where + /-- The representation of a binary sum. -/ + sum : {A B : Type u} → C.Str A → C.Str B → C.Str (A ⊕ B) + /-- The left injection is admissible. -/ + inl_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom a (sum a b) Sum.inl + /-- The right injection is admissible. -/ + inr_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom b (sum a b) Sum.inr + /-- Case analysis on admissible branches is admissible. -/ + elim_mem : ∀ {A B D : Type u} {a : C.Str A} {b : C.Str B} {d : C.Str D} + {f : A → D} {g : B → D}, C.Hom a d f → C.Hom b d g → + C.Hom (sum a b) d (Sum.elim f g) + +/-- Admissible functions act on sums summandwise. -/ +theorem HasSum.map_mem [S : C.HasSum] {A B A' B' : Type u} {a : C.Str A} + {b : C.Str B} {a' : C.Str A'} {b' : C.Str B'} {f : A → A'} {g : B → B'} + (hf : C.Hom a a' f) (hg : C.Hom b b' g) : + C.Hom (S.sum a b) (S.sum a' b') (Sum.map f g) := by + refine (S.elim_mem (C.comp_mem hf (S.inl_mem a' b')) + (C.comp_mem hg (S.inr_mem a' b'))).congr ?_ + intro x + cases x <;> rfl + +/-! ## Optional values -/ + +/-- A step class with admissible optional values. + +The realizability layer requires this of every class it uses: a machine's +flattened transition is *partial*, and `none` records that an answer is not one +the machine is waiting for. Partiality is what makes the flattening +compositional — see `PolyFun.Realizability.Machine`. + +Up to the equivalence `Option A ≃ A ⊕ PUnit` this is `HasSum` together with a +terminal representation, but it is taken as primitive: factoring it would force +a terminal representation on every instance, and nothing else needs one. For the +same reason `omap_mem` and `obindCtx_mem` are both primitive — each is derivable +from the other only through a unit representation. -/ +class HasOption (C : StepClass.{u, v}) [P : C.HasProd] where + /-- The representation of an optional value. -/ + option : {A : Type u} → C.Str A → C.Str (Option A) + /-- Admissible functions act on optional values. -/ + omap_mem : ∀ {A B : Type u} {a : C.Str A} {b : C.Str B} {f : A → B}, + C.Hom a b f → C.Hom (option a) (option b) (Option.map f) + /-- The absent value is admissible as a constant. This is the one constant map + the layer assumes: a machine that has already returned takes no step, so its + transition is constantly `none`. -/ + none_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), + C.Hom a (option b) fun _ => none + /-- Sequencing a partial value against an admissible continuation that also + reads a retained context. Needed to transport a realization along a lens, + where the pulled-back answer index is partial and the continuation still needs + the machine's state. -/ + obindCtx_mem : ∀ {A B E : Type u} {a : C.Str A} {b : C.Str B} {e : C.Str E} + {k : A × E → Option B}, C.Hom (P.prod a e) (option b) k → + C.Hom (P.prod (option a) e) (option b) fun y => y.1.bind fun j => k (j, y.2) + +/-! ## Distributivity -/ + +/-- A step class whose product and sum representations distribute. + +Equivalently — and this is the form the closure theory actually uses, available as +`IsDistributive.elimCtx_mem` — *case analysis in a context* is admissible. + +The field is the **inverse** of the map a category theorist calls canonical: the +canonical (cogap) direction is `codistrib_mem` below, which needs no axiom at all. +Both directions being admissible is exactly "the canonical map is an isomorphism +in the subcategory", so this is Cockett's distributivity verbatim rather than a +one-sided weakening. Only the binary case is required; no terminal or initial +representation is assumed, so this is weaker than +`CategoryTheory.IsCartesianDistributive`. + +Note that distributivity genuinely does not come for free: every bicartesian +*closed* category is automatically distributive because `X × (-)` is a left +adjoint, but the motivating classes here have no exponentials. -/ +class IsDistributive (C : StepClass.{u, v}) [P : C.HasProd] [S : C.HasSum] : + Prop where + distrib_mem : ∀ {A B I : Type u} (a : C.Str A) (b : C.Str B) (i : C.Str I), + C.Hom (P.prod (S.sum a b) i) (S.sum (P.prod a i) (P.prod b i)) + fun x => Sum.elim (fun l => Sum.inl (l, x.2)) (fun r => Sum.inr (r, x.2)) x.1 + +/-- The canonical direction of the distributivity map, which needs only products +and sums. Together with `IsDistributive.distrib_mem` it exhibits the canonical map +as an isomorphism in the subcategory. -/ +theorem codistrib_mem [P : C.HasProd] [S : C.HasSum] {A B I : Type u} + (a : C.Str A) (b : C.Str B) (i : C.Str I) : + C.Hom (S.sum (P.prod a i) (P.prod b i)) (P.prod (S.sum a b) i) + (Sum.elim (Prod.map Sum.inl id) (Prod.map Sum.inr id)) := + S.elim_mem (P.map_mem (S.inl_mem a b) (C.id_mem i)) + (P.map_mem (S.inr_mem a b) (C.id_mem i)) + +/-- Case analysis in a context: dispatching on a sum-valued component while +retaining the rest of the input. + +This is the workhorse of the closure theory. Distributivity is equivalent to it; +in the presence of `HasProd.diag_mem` it even implies the unparameterized +`HasSum.elim_mem`, by taking the context to be the sum itself — so the axioms are +not independent. `elim_mem` is nonetheless kept primitive, since deriving it would +churn every instance for no gain. -/ +theorem IsDistributive.elimCtx_mem [P : C.HasProd] [S : C.HasSum] + [D : C.IsDistributive] {A B E Z : Type u} {a : C.Str A} {b : C.Str B} + {e : C.Str E} {z : C.Str Z} {f : A × E → Z} {g : B × E → Z} + (hf : C.Hom (P.prod a e) z f) (hg : C.Hom (P.prod b e) z g) : + C.Hom (P.prod (S.sum a b) e) z + fun x => Sum.elim (fun l => f (l, x.2)) (fun r => g (r, x.2)) x.1 := by + refine (C.comp_mem (D.distrib_mem a b e) (S.elim_mem hf hg)).congr ?_ + intro x + cases x with + | mk s v => cases s <;> rfl + +/-- A distributive step class: a distributive category (Cockett 1993) presented +concretely over `Type u`, together with admissible optional values. + +This bundles the structure the closure theory consumes. It is a convenience only; +each individual theorem asks for exactly the mixins it uses. -/ +class Distributive (C : StepClass.{u, v}) where + /-- The class has admissible binary products. -/ + [toHasProd : C.HasProd] + /-- The class has admissible binary sums. -/ + [toHasSum : C.HasSum] + /-- The class has admissible optional values. -/ + [toHasOption : C.HasOption] + /-- The class's products and sums distribute. -/ + [toIsDistributive : C.IsDistributive] + +attribute [implicit_reducible, instance] Distributive.toHasProd + Distributive.toHasSum Distributive.toHasOption + +attribute [instance] Distributive.toIsDistributive + +/-! ## Refinement between classes -/ + +set_option linter.checkUnivs false in +/-- A refinement of step classes: a translation of representations carrying +`C`-admissibility to `D`-admissibility, compatibly with the product and sum +representations. Realizability transports forward along a refinement, so a +realization in a small class is a realization in every larger one. + +Compatibility with products and sums is not automatic and is not implied by +`hom`, but it is needed for the transport: the realizability layer's derived +representations are built from the boundary with `HasProd.prod` and +`HasSum.sum`, and a refinement that translated those to unrelated +representations would not carry a realization anywhere. -/ +-- The two representation universes are independent of each other and of the +-- represented universe: refining a `Type`-valued encoding into a `Prop`-valued +-- one is a typical use. +structure Refines (C : StepClass.{u, v}) (D : StepClass.{u, v₂}) + [C.HasProd] [C.HasSum] [C.HasOption] [D.HasProd] [D.HasSum] [D.HasOption] where + /-- Translate a `C`-representation into a `D`-representation. -/ + str : {A : Type u} → C.Str A → D.Str A + /-- Every `C`-admissible function is `D`-admissible between the translations. -/ + hom : ∀ {A B : Type u} {a : C.Str A} {b : C.Str B} {f : A → B}, + C.Hom a b f → D.Hom (str a) (str b) f + /-- The translation preserves product representations. -/ + str_prod : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), + str (HasProd.prod a b) = HasProd.prod (str a) (str b) + /-- The translation preserves sum representations. -/ + str_sum : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), + str (HasSum.sum a b) = HasSum.sum (str a) (str b) + /-- The translation preserves optional representations. -/ + str_option : ∀ {A : Type u} (a : C.Str A), + str (HasOption.option a) = HasOption.option (str a) + +/-- Refinement is reflexive. -/ +def Refines.refl (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption] : + C.Refines C where + str a := a + hom h := h + str_prod _ _ := rfl + str_sum _ _ := rfl + str_option _ := rfl + +set_option linter.checkUnivs false in +/-- Refinements compose. -/ +-- Three independent representation universes, for the same reason as `Refines`. +def Refines.trans {C : StepClass.{u, v}} {D : StepClass.{u, v₂}} + {E : StepClass.{u, v₃}} [C.HasProd] [C.HasSum] [C.HasOption] [D.HasProd] + [D.HasSum] [D.HasOption] [E.HasProd] [E.HasSum] [E.HasOption] + (R : C.Refines D) (S : D.Refines E) : C.Refines E where + str a := S.str (R.str a) + hom h := S.hom (R.hom h) + str_prod a b := by rw [R.str_prod, S.str_prod] + str_sum a b := by rw [R.str_sum, S.str_sum] + str_option a := by rw [R.str_option, S.str_option] + +end StepClass + +end PFunctor diff --git a/PolyFunTest/Realizability/Examples.lean b/PolyFunTest/Realizability/Examples.lean new file mode 100644 index 0000000..a5befff --- /dev/null +++ b/PolyFunTest/Realizability/Examples.lean @@ -0,0 +1,237 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Devon Tuma +-/ +module + +public import PolyFun.Realizability.Closure +public import PolyFun.Realizability.Instances + +/-! +# Worked examples of admissible realizability + +A hand-built two-state machine realizing a one-query program, checked against the +finite step class, plus smoke tests pinning the definitional behaviour the +closure theory relies on: + +* the flat step maps of `ofStep` read back exactly the supplied step function; +* replacing the initialization leaves every step map alone *by `rfl`*, which is + what makes `IsRealizableBy.precomp` free; +* two one-query programs compose under `bind`, with budgets adding, and the + composite transition satisfies an equation unconditional in the answer index; +* `StepClass.computable.Hom` really is Mathlib's `Computable`; +* a realization transports from the computable class to the unconstrained one + along a `StepClass.Refines`. +-/ + +@[expose] public section + +namespace PFunctor.RealizabilityExamples + +open PFunctor +open PFunctor.DynSystem +open PFunctor.DynSystem.DynComputation + +/-! ## A one-query interface and program -/ + +/-- A single-query interface: one query, answered by a bit. -/ +def coin : PFunctor.{0, 0} := + { A := Unit, B := fun _ => Bool } + +instance : DecidableEq coin.A := inferInstanceAs (DecidableEq Unit) + +/-- Ask the single query once and return its answer. -/ +def program : Unit → FreeM coin Bool := + fun _ => FreeM.lift () + +/-- The realizing machine: `none` before the query, `some answer` after. Two +states suffice, and the whole machine is given by one step function. -/ +def machine : DynComputation.{0} coin Unit Bool := + DynComputation.ofStep + (fun state => match state with + | none => Sum.inr ⟨(), fun answer => some answer⟩ + | some answer => Sum.inl answer) + fun _ => none + +example : machine.State = Option Bool := rfl + +/-! ## The flat step maps read back the supplied step function -/ + +example : machine.head none = Sum.inr () := rfl + +example (answer : Bool) : machine.head (some answer) = Sum.inl answer := rfl + +example (answer : Bool) : + machine.update? (none, ⟨(), answer⟩) = some (some answer) := + machine.update?_of_view_query rfl answer + +/-- A resolved state takes no step, and neither does a mismatched answer — with a +one-position interface only the former can occur. -/ +example (answer : Bool) : ∀ given : Bool, + machine.update? (some answer, ⟨(), given⟩) = none := + fun _ => machine.update?_of_view_return rfl _ + +/-- The total variant collapses `none` to the unchanged state. -/ +example (answer : Bool) : ∀ given : Bool, + machine.updateFlat (some answer, ⟨(), given⟩) = some answer := + fun _ => machine.updateFlat_of_view_return rfl _ + +example : machine.output none = none := rfl + +example (answer : Bool) : machine.output (some answer) = some answer := rfl + +/-! ## Finite-state realizability -/ + +/-- The boundary: every type at the boundary of this statement is finite. -/ +def finiteBoundary : Boundary StepClass.finite.{0} coin Unit Bool where + input := inferInstanceAs (Fintype Unit) + out := inferInstanceAs (Fintype Bool) + pos := inferInstanceAs (Fintype Unit) + idx := inferInstanceAs (Fintype (Σ _ : Unit, Bool)) + +/-- The machine implements the program within one query. Both sides are the same +`FreeM` term, so the check is definitional. -/ +example : machine.ImplementsWithin program 1 := fun _ => rfl + +/-- `program` is realizable by a finite-state machine within one query. -/ +theorem isRealizableWithin_finite : + IsRealizableWithin StepClass.finite finiteBoundary program 1 := + ⟨{ machine := machine + state := inferInstanceAs (Fintype (Option Bool)) + init_mem := True.intro + head_mem := True.intro + update_mem := True.intro }, fun _ => rfl⟩ + +/-- The bounded predicate implies the unbounded one. -/ +example : IsFiniteStateRealizable finiteBoundary program := + isRealizableWithin_finite.isRealizableBy + +/-- A bounded realization certifies the program's own query depth. -/ +example (input : Unit) : (program input).IsTotalRollBound 1 := + isRealizableWithin_finite.isTotalRollBound input + +/-- Budget monotonicity. -/ +example : IsRealizableWithin StepClass.finite finiteBoundary program 3 := + isRealizableWithin_finite.mono (by omega) + +/-- Result postcomposition in action: negating the returned bit stays realizable +at the same budget, because mapping a result performs no queries. -/ +example : + IsRealizableWithin StepClass.finite + (finiteBoundary.withOut (inferInstanceAs (Fintype Bool))) + (fun input => FreeM.map not (program input)) 1 := + isRealizableWithin_finite.mapResult True.intro + +/-- Input precomposition in action. -/ +example : + IsRealizableWithin StepClass.finite + (finiteBoundary.withInput (inferInstanceAs (Fintype Bool))) + (fun _ : Bool => program ()) 1 := + isRealizableWithin_finite.precomp (f := fun _ : Bool => ()) True.intro + +/-! ## Closure under `bind` + +Two one-query programs compose into a two-query one, and the realizations compose +with them. The budgets add, and the composite machine's state is the coproduct of +the two phases' states. +-/ + +/-- The second phase: the same machine, reindexed to consume the first phase's +result as its input. -/ +def machine₂ : DynComputation.{0} coin Bool Bool := + machine.contramapInput fun _ : Bool => () + +/-- Ask the query once, then ask it again — realizable by a finite-state machine +within `1 + 1` queries. -/ +example : IsRealizableWithin StepClass.finite + (finiteBoundary.withOut (inferInstanceAs (Fintype Bool))) + (fun input => FreeM.bind (program input) fun _ => program ()) (1 + 1) := + isRealizableWithin_finite.seqComp + (isRealizableWithin_finite.precomp (f := fun _ : Bool => ()) True.intro) + +/-- The composite machine's state really is the coproduct. -/ +example : + (machine.seqComp machine₂).State = (Option Bool ⊕ Option Bool) := rfl + +/-- The composite readout hands a returned intermediate value straight to the +second phase, in the same observation. -/ +example (answer : Bool) : + (machine.seqComp machine₂).head (Sum.inl (some answer)) = Sum.inr () := rfl + +/-- And the composite transition is unconditional in the answer index — the +equation that partiality buys. -/ +example (answer given : Bool) : + (machine.seqComp machine₂).update? (Sum.inl (some answer), ⟨(), given⟩) = + Option.map Sum.inr (machine₂.update? (machine₂.init answer, ⟨(), given⟩)) := + machine.update?_seqComp_inl machine₂ (some answer) ⟨(), given⟩ + +/-! ## Non-vacuity of the unconstrained class -/ + +example : + IsRealizableBy StepClass.unconstrained.{0, 0} + (Boundary.unconstrained coin Unit Bool) program := + isRealizableBy_unconstrained program + +/-! ## Replacing the initialization is definitionally transparent + +These are the `rfl` checks that make `precomp` free: a machine and its +reinitialization share every step map on the nose. If a `match` ever creeps into +one of the step-map definitions, these break. +-/ + +section SetInit + +variable (M : DynComputation.{0} coin Unit Bool) (g : Bool → M.State) + +example : (M.setInit g).head = M.head := rfl + +example : (M.setInit g).output = M.output := rfl + +example (step : M.State × coin.Idx) : + (M.setInit g).update? step = M.update? step := rfl + +example (step : M.State × coin.Idx) : + (M.setInit g).updateFlat step = M.updateFlat step := rfl + +example (handler : (a : coin.A) → coin.B a) : + (M.setInit g).stepD handler = M.stepD handler := rfl + +end SetInit + +/-! ## The computable class is Mathlib's `Computable` -/ + +example : StepClass.computable.{0}.Hom (A := ℕ) (B := ℕ) + (inferInstanceAs (Primcodable ℕ)) (inferInstanceAs (Primcodable ℕ)) id := + Computable.id + +example : StepClass.computable.{0}.Hom (A := ℕ × ℕ) (B := ℕ) + (inferInstanceAs (Primcodable (ℕ × ℕ))) (inferInstanceAs (Primcodable ℕ)) + Prod.fst := + Computable.fst + +example : StepClass.computable.{0}.Hom (A := ℕ) (B := ℕ ⊕ ℕ) + (inferInstanceAs (Primcodable ℕ)) (inferInstanceAs (Primcodable (ℕ ⊕ ℕ))) + Sum.inl := + Primrec.sumInl.to_comp + +/-! ## Transport along a refinement of step classes + +Every computable machine is in particular an unconstrained one. -/ + +/-- The computable class refines the unconstrained one. -/ +def computableRefinesUnconstrained : + StepClass.computable.{0}.Refines StepClass.unconstrained.{0, 0} where + str _ := PUnit.unit + hom _ := True.intro + str_prod _ _ := rfl + str_sum _ _ := rfl + str_option _ := rfl + +example (bd : Boundary StepClass.computable.{0} coin Unit Bool) + (h : IsRealizableBy StepClass.computable bd program) : + IsRealizableBy StepClass.unconstrained.{0, 0} + (bd.mapRefines computableRefinesUnconstrained) program := + h.mono computableRefinesUnconstrained + +end PFunctor.RealizabilityExamples diff --git a/REFERENCES.md b/REFERENCES.md index ca5120c..c72d023 100644 --- a/REFERENCES.md +++ b/REFERENCES.md @@ -70,8 +70,9 @@ free-monad-as-module-over-cofree-comonad structure made explicit (a module action, not an adjunction). Used in: `PolyFun/PFunctor/SubstMonoid.lean`, -`PolyFun/PFunctor/Free/Path.lean`, and -`PolyFun/PFunctor/PatternRunsOnMatter/`. +`PolyFun/PFunctor/Free/Path.lean`, +`PolyFun/PFunctor/PatternRunsOnMatter/`, and +`PolyFun/Realizability/Basic.lean`. ### XZHHMPZ20 — Xia, Zakowski, He, Hur, Malecha, Pierce, Zdancewic, *Interaction Trees* @@ -135,7 +136,8 @@ arXiv:2604.01303, 2026. Dependent polynomials over a base polynomial, their free displayed extension, displayed handlers, and compositional verification applications. -Used in: `PolyFun/PFunctor/Display/`. +Used in: `PolyFun/PFunctor/Display/`, +`PolyFun/Realizability/Basic.lean`. ### Spi12 — Spivak, *Functorial data migration* @@ -162,3 +164,231 @@ lens layer in `PolyFun/PFunctor/Lens/` makes dependent. Used in: `PolyFun/PFunctor/Lens/State.lean`, `PolyFun/PFunctor/Lens/Basic.lean`. + +## Realizability citations + +The realizability layer in `PolyFun/Realizability/` recombines pieces owned by +four separate communities; these are the canonical sources for each. No single +source states the combination — a machine realization whose *structure maps* are +constrained by an abstract predicate — so the layer's docstrings cite the +ingredients rather than claiming a name for the whole. + +### AM74 — Arbib and Manes, *Machines in a category* + +Michael A. Arbib and Ernest G. Manes. +*Machines in a Category: An Expository Introduction*. +*SIAM Review* 16(2):163–192, 1974. +DOI: + +A machine in an arbitrary category as an initialization / transition / readout +triple, and its induced behaviour. The `expose` / `update` / readout triple of a +`DynComputation` is an Arbib–Manes machine for the one-step polynomial functor; +what the realizability layer adds is that the structure maps must lie in a +distinguished class. Companion sources for "realization is universal": Goguen +1972/73 and Naudé, *Universal realization*, JCSS 19(3), 1979. + +Used in: `PolyFun/Realizability/Basic.lean`. + +### AMMS13 — Adámek, Milius, Moss, Sousa, *Well-pointed coalgebras* + +Jiří Adámek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. +*Well-Pointed Coalgebras*. +*Logical Methods in Computer Science* 9(3), 2013. +arXiv:1305.0576 + +The coalgebraic use of the word *realization*: a pointed coalgebra realizes the +corresponding element of the terminal coalgebra, and the well-pointed coalgebras +are exactly the minimal realizations. This is the realizability predicate of +`PolyFun/Realizability/` with the admissibility constraint removed. + +Used in: `PolyFun/Realizability/Basic.lean`. + +### PR89 — Pnueli and Rosner, *On the synthesis of a reactive module* + +Amir Pnueli and Roni Rosner. +*On the Synthesis of a Reactive Module*. +In *Principles of Programming Languages* (POPL), 1989. +DOI: + +*Realizability* as the existence of a finite-state machine meeting a +specification — the reading recovered by `StepClass.finite`, for which +`IsFiniteStateRealizable` is provided as the community's name. Ancestor: Church, +*Applications of recursive arithmetic to the problem of circuit synthesis*, 1963. + +Used in: `PolyFun/Realizability/Instances.lean`. + +### Uus15 — Uustalu, *Stateful runners of effectful computations* + +Tarmo Uustalu. +*Stateful Runners of Effectful Computations*. +*Mathematical Foundations of Programming Semantics* XXXI, +*Electronic Notes in Theoretical Computer Science* 319:403–421, 2015. +DOI: + +A stateful runner of `T`-computations is exactly a comodel, i.e. a coalgebra of +the corresponding comonad. This is why a `p`-coalgebra with state `S` *is* a way +of running every `FreeM p` program in `S`, and hence why realizability is a +statement about coalgebras. See also Katsumata, Rivas, and Uustalu, +*Interaction laws of monads and comonads*, LICS 2020 (arXiv:1912.13477). + +Used in: `PolyFun/Realizability/Basic.lean`. + +### PM15 — Petcher and Morrisett, *The Foundational Cryptography Framework* + +Adam Petcher and Greg Morrisett. +*The Foundational Cryptography Framework*. +In *Principles of Security and Trust* (POST/ESOP), LNCS 9036, 2015. +arXiv:1410.3735 + +Security definitions parameterized by an *admissibility predicate* naming the +class of allowed adversaries, over a free-monad-shaped computation type. This is +the design precedent for taking the resource bound as a predicate on the +implementation rather than as a measure on runs, and the source of the +`admissible` / `_mem` vocabulary used throughout the layer. + +Used in: `PolyFun/Realizability/StepClass.lean`. + +### Blum67 — Blum, *A machine-independent theory of complexity* + +Manuel Blum. +*A Machine-Independent Theory of the Complexity of Recursive Functions*. +*Journal of the ACM* 14(2):322–336, 1967. +DOI: + +Complexity measures axiomatized rather than fixed, with a complexity class as +"there exists a program from an enumeration satisfying a resource predicate" — +the same existential shape as `IsRealizableBy`, but quantifying over a Gödel +numbering of programs rather than over machines with constrained structure maps. + +Used in: `PolyFun/Realizability/Basic.lean`. + +### GHP09 — Ghani, Hancock, Pattinson, *Representations of stream processors* + +Neil Ghani, Peter Hancock, and Dirk Pattinson. +*Representations of Stream Processors Using Nested Fixed Points*. +*Logical Methods in Computer Science* 5(3:9), 2009. +arXiv:0905.4813 + +Continuous and computable functions on final coalgebras represented by an +alternating `νX.μY.` fixpoint — a machine whose individual steps are finite +well-founded programs. This is the known special case of admissible +realizability at the class "given by a finite `FreeM` term". + +Used in: `PolyFun/Realizability/Basic.lean`. + +## Distributive-category citations + +The closure structure a step class needs — finite products, finite coproducts, and +distributivity — is exactly a distributive category. These are the canonical +sources for the concept and for the complexity-theory vocabulary it replaces. + +### Coc93 — Cockett, *Introduction to distributive categories* + +J. Robin B. Cockett. +*Introduction to Distributive Categories*. +*Mathematical Structures in Computer Science* 3(3):277–307, 1993. +DOI: + +The definition: a category with finite products and binary coproducts in which the +canonical map has an inverse. Also the distributive / recognizable / extensive / +familial hierarchy, and the theorem that the distributive completion of a +cartesian category is its coproduct completion. + +`PFunctor.StepClass.IsDistributive` axiomatizes the inverse direction; the +canonical (cogap) direction is derivable from products and sums alone and ships as +`StepClass.codistrib_mem`, so the two together give Cockett's axiom verbatim. Only +the binary case is required here. Compare +`Mathlib.CategoryTheory.IsCartesianDistributive`, which states the axiom in the +cogap orientation. + +Used in: `PolyFun/Realizability/StepClass.lean`. + +### CLW93 — Carboni, Lack, Walters, *Extensive and distributive categories* + +Aurelio Carboni, Stephen Lack, and R. F. C. Walters. +*Introduction to Extensive and Distributive Categories*. +*Journal of Pure and Applied Algebra* 84(2):145–158, 1993. +DOI: + +Disentangles distributivity from extensivity, which had been conflated. Includes +the nullary clause `0 ≅ A × 0` that full finite distributivity also demands and +that this layer deliberately omits, extensivity being a statement about pullbacks +that a class of resource-bounded functions has no business claiming. + +Textbook companion: R. F. C. Walters, *Categories and Computer Science*, +Cambridge Computer Science Texts 28, CUP, 1991 — the treatment that made +distributive categories the CS-facing default. + +Used in: `PolyFun/Realizability/StepClass.lean`. + +### CF92 — Cockett and Fukushima, *About Charity* + +J. Robin B. Cockett and Tom Fukushima. +*About Charity*. +Yellow Series Report 92/480/18, Department of Computer Science, +University of Calgary, 1992. + +The internal language of distributive categories, as a programming language, and +the source of the reading this layer uses: distributivity is what makes *proof by +case analysis* available. `IsDistributive.elimCtx_mem` — case analysis in a +context — is that reading made into the working lemma. Companion: +Cockett and Spencer, *Strong categorical datatypes II: A term logic for +categorical programming*, TCS 139(1–2):69–113, 1995. + +Used in: `PolyFun/Realizability/StepClass.lean`. + +### CDGH12 — Cockett, Díaz-Boïls, Gallagher, Hrubeš, *Timed sets* + +J. Robin B. Cockett, Joaquín Díaz-Boïls, Jonathan Gallagher, and Pavel Hrubeš. +*Timed Sets, Functional Complexity, and Computability*. +*Electronic Notes in Theoretical Computer Science* 286:117–137, 2012 (MFPS XXVIII). +DOI: + +Categories of timed sets modulo a complexity order form distributive restriction +categories, with PTIME and LOGSPACE as worked examples. The closest existing +statement that a complexity class *is* a distributive category, and hence the +nearest prior art for treating a resource-bounded function class as one. + +Used in: `docs/wiki/realizability.md`. + +### CH08 — Cockett and Hofstra, *Introduction to Turing categories* + +J. Robin B. Cockett and Pieter J. W. Hofstra. +*Introduction to Turing Categories*. +*Annals of Pure and Applied Logic* 156(2–3):183–209, 2008. +DOI: + +Axioms for when a class of total maps is the total-map subcategory of a Turing +category, instantiated at LINTIME, PTIME, and EXPTIME. This is the precedent for +presenting a complexity class as a cartesian category with a faithful functor to +`Set` — and, by omission, evidence that the coproduct and distributivity +requirements here are not inherited from that tradition: the Turing-category +axioms mention neither, using two disjoint points of a universal object as a +hand-rolled stand-in for `1 ⊕ 1`. + +Companion: Cockett, Hofstra, and Hrubeš, *Total maps of Turing categories*, +ENTCS 308:129–146, 2014. + +Used in: `docs/wiki/realizability.md`. + +### Clo99 — Clote, *Computation models and function algebras* + +Peter Clote. +*Computation Models and Function Algebras*. +In *Handbook of Computability Theory* (E. R. Griffor, ed.), +Studies in Logic and the Foundations of Mathematics 140, +Elsevier, 1999, pp. 589–681. +DOI: + +The complexity-native vocabulary for a class of functions closed under +composition: a *function algebra*. Foundational instances: Cobham, *The intrinsic +computational difficulty of functions*, 1965 (FP by bounded recursion on +notation), and Bellantoni and Cook, *A new recursion-theoretic characterization of +the polytime functions*, Computational Complexity 2:97–110, 1992. + +Function algebras are single-sorted, so branching enters as a *base function* +(`caseBit`, Bellantoni–Cook's `C`) and distributivity is invisible in that +tradition. Making the axiom visible is a consequence of this layer being +multi-sorted and representation-indexed. + +Used in: `docs/wiki/realizability.md`. diff --git a/docs/wiki/README.md b/docs/wiki/README.md index b327be5..67a3268 100644 --- a/docs/wiki/README.md +++ b/docs/wiki/README.md @@ -46,6 +46,9 @@ See the *Wiki Maintenance Contract* section in - [`interaction.md`](interaction.md): the generic interaction framework (sequential `TypeTree`, two-party, multiparty local views, concurrent processes, UC open systems). +- [`realizability.md`](realizability.md): realizability of free programs by + state machines whose transition functions satisfy a given predicate + (`StepClass`, `Realization`, `IsRealizableBy`). ## Cross-Cutting Notes @@ -69,6 +72,7 @@ See the *Wiki Maintenance Contract* section in - `ipfunctor.md` for the state-indexed `IPFunctor` / `FreeM` / `FreeM₂` substrate. - `itree.md` for interaction trees, bisimulation, and handlers. - `interaction.md` for the interaction framework above `FreeM`. + - `realizability.md` for step classes and machine realizability. - `notation.md` for notation cross-references. - `gotchas.md` for recurring traps. - Add new pages when a recurring topic no longer fits cleanly in an existing diff --git a/docs/wiki/realizability.md b/docs/wiki/realizability.md new file mode 100644 index 0000000..54e0fe3 --- /dev/null +++ b/docs/wiki/realizability.md @@ -0,0 +1,298 @@ +# Realizability By Admissible State Machines + +`PolyFun/Realizability/` answers the question "can this program be run by a +machine whose transition functions satisfy a given predicate?" — generically in +the predicate. It is the missing third ingredient above the existing machine +layer: + +| Question | Where it is answered | +| --- | --- | +| *What* interaction does the program perform? | `PFunctor.FreeM p β` | +| *How* does a machine perform it? | `PFunctor.DynSystem.DynComputation p α β` | +| Do the two agree (and within what budget)? | `Implements` / `ImplementsWithin` | +| Is the machine's *machinery* allowed? | **this subtree** | + +Instantiating the predicate recovers a spectrum of notions from one definition: +finite-state realizability, machines with computable transitions, and — the +motivating case downstream — the polynomial-time adversary model used in +cryptography. + +## The Four Modules + +```text +PolyFun/Realizability/ + StepClass.lean PFunctor.StepClass; HasProd / HasSum / HasOption / + IsDistributive mixins; the Distributive bundle; Refines + Machine.lean the first-order step maps: head, update?, updateFlat, + output, expose, stepD, their transport lemmas, and + faithfulness of the flat presentation + Basic.lean Boundary, Realization, IsRealizableBy, IsRealizableWithin + Closure.lean closure under ofFn, precomp, mapResult, seqComp (bind), + wrap (interface transport), and class refinement + Instances.lean unconstrained, finite, computable, WordClass +``` + +`Machine.lean` and `StepClass.lean` are independent; `Basic.lean` joins them. + +## `StepClass`: A Class Of Admissible Functions + +```lean +structure PFunctor.StepClass where + Str : Type u → Type v + Hom : {A B : Type u} → Str A → Str B → (A → B) → Prop + id_mem : ∀ {A} (a : Str A), Hom a a id + comp_mem : Hom a b f → Hom b d g → Hom a d (g ∘ f) +``` + +A wide subcategory of `Type u`, presented pointwise. Two deliberate choices: + +- **`Str` is data, not a proposition.** A resource bound only makes sense + relative to a chosen representation: "`f` runs in polynomial time" is a + statement about encoded inputs, not about the bare function. +- **`Hom` is a proposition.** The realizability layer only ever asks *whether* a + step map is admissible. A cost-bearing refinement — witnesses carrying + running-time and description-size measures — would replace it by a + `Type`-valued field. That refinement is deliberately not in this subtree. + +`StepClass.Hom.congr` transports admissibility along pointwise equality of +functions. It is the workhorse of the closure theory: a step map of a derived +machine is almost never *syntactically* the admissible combination one builds by +hand. + +## Four mixins, and what each one buys + +| Mixin | Required by | Content | +| --- | --- | --- | +| `HasProd` | the core | the flattened transition has a product domain | +| `HasSum` | the core | the one-step readout lands in a sum | +| `HasOption` | the core | the flattened transition is *partial* | +| `IsDistributive` | `seqComp` only | case analysis in a context | + +They are kept out of `StepClass` so that a cost-bearing successor can require +different structure, and split so that each theorem asks for exactly what it +consumes. + +### It really is a distributive category + +A class with `HasProd`, `HasSum`, and `IsDistributive` is exactly a **distributive +category** in the sense of Cockett (MSCS 1993) and Carboni–Lack–Walters (JPAA +1993), presented concretely — i.e. with a faithful functor to `Type` preserving +finite products and coproducts. Two points worth knowing: + +* **This is not a one-sided weakening.** The *other* direction of the canonical + map, the cogap `(A × I) ⊕ (B × I) → (A ⊕ B) × I`, is derivable from `HasProd` + and `HasSum` alone and ships as `StepClass.codistrib_mem`. Both directions + being admissible is literally "the canonical map is an isomorphism in the + subcategory", which is Cockett's axiom verbatim. +* **Mathlib's canonical orientation is the opposite one.** Mathlib does have this + concept — `CategoryTheory.IsCartesianDistributive`, citing the same two papers — + and states the axiom in the cogap direction. Our `distrib_mem` field is the + *inverse*. Do not read the arrow as a mistake. + +We deliberately do **not** import Mathlib's version. `MorphismProperty (Type u)` +cannot type our `Hom`, which is indexed by *representations* and not just by +types; the `BundledHom` framework that matched this pattern exactly was +deprecated to nothing in February 2026; and `IsCartesianDistributive` has zero +consumers in Mathlib, so adopting it would cost a full monoidal/limit-cone layer +for no new theorem. Only the binary case is axiomatized here — no terminal or +initial representation is required, and none is needed — so +`StepClass.Distributive` is deliberately weaker than `IsCartesianDistributive`. + +Distributivity is a real axiom, not a theorem: every bicartesian *closed* category +is automatically distributive because `X × (−)` is a left adjoint, but the +motivating classes have no exponentials. + +### A note on the complexity-theory tradition + +The complexity-native presentation of a class of functions is a **function +algebra** (Cobham 1965; Bellantoni–Cook 1992; Clote's handbook survey). Those are +*single-sorted*, so branching enters as a *base function* (`caseBit`, +Bellantoni–Cook's `C`) and distributivity is invisible. Making the axiom visible +is a consequence of being multi-sorted and representation-indexed. The closest +existing statement that a complexity class *is* a distributive category is +Cockett–Díaz-Boïls–Gallagher–Hrubeš (ENTCS 286, 2012), which exhibits PTIME and +LOGSPACE that way. + +## The First-Order Step Maps + +`DynComputation`'s dynamics live in `view : State → β ⊕ p.Obj State`, whose +second component stores a *function-valued* continuation and is *dependent* on +the exposed position. Neither shape can be constrained by a predicate on plain +functions, so `Machine.lean` re-presents the same dynamics first-order: + +```lean +def head (M : DynComputation p α β) : M.State → β ⊕ p.A := + M.toDynSystem.expose + +def update? [DecidableEq p.A] (M : DynComputation p α β) : + M.State × p.Idx → Option M.State +``` + +`head` is not a new definition — it is *definitionally* the position map of the +machine's underlying lens. That is why it transports so well: + +| Operation | Effect on `head` | Holds by | +| --- | --- | --- | +| `setInit g` | unchanged | `rfl` | +| `mapResult f` | `Sum.map f id ∘ head` | `rfl` | +| `wrap lens` | `Sum.map id lens.toFunA ∘ head` | `rfl` | + +**`head`, not an `output` / `expose` pair.** Splitting the readout into +`output : State → Option β` and `expose : State → p.A` forces a `default` +convention at resolved states, and that convention breaks compositionality: +`(M.wrap lens).expose` is *not* `lens.toFunA ∘ M.expose`, because the two +disagree exactly at resolved states. `head` has no such wart. `output`, `expose`, +and `stepD` are still provided, as the derived accessors a machine-facing cost +model consumes. + +**`update?` is partial, and that is load-bearing.** `none` means the pair is not a +step the machine can take: the state has already returned, or the answer is tagged +with a position the machine is not exposing. The total variant `updateFlat` +(retained, derived as `(update? step).getD step.1`, because that is the shape a +machine-facing cost model wants) does **not** compose across a state coproduct with +a handoff: + +| answer tag | composite `updateFlat` | `Sum.inr (M₂.updateFlat (M₂.init v, i))` | +| --- | --- | --- | +| matches `M₂`'s exposed position | `Sum.inr (next₂ d)` | `Sum.inr (next₂ d)` ✓ | +| does not match | `Sum.inl s₁` | `Sum.inr (M₂.init v)` ✗ | + +Reconciling those junk values would require the class to contain a decidable +equality test on interface positions — provably not derivable from products, +coproducts, and distributivity, since in the free distributive category on one +object `Hom(X × X, 1 ⊕ 1)` contains only the two constants, and `StepClass` has no +terminal object. With `none` both rows agree, the both-resolved case is subsumed +(`M₂.update?` is `none` at a resolved state), and `update?_seqComp_inl` becomes an +equation *unconditional in the answer index*. That is the whole reason for the +partiality; the only cost is `DecidableEq p.A`. + +**The presentation is faithful.** `ofStep_step_eq_of_flat_eq`: a step function is +determined by the `head` and `update?` it induces. So constraining those two maps +plus `init` constrains the machine, not a lossy projection of it. + +**Spell the step maps with combinators, never `match`.** `Sum.elim`, +`Option.getLeft?`, `Sigma.fst`, and `dite` all reduce by congruence over the +shared `view`. An auto-generated matcher instead abstracts the computation and +blocks unification across distinct input types, which would cost the `rfl` +transport above. `PolyFunTest/Realizability/Examples.lean` pins those `rfl`s so a +regression fails the test build. + +## The Boundary Is A Parameter, Never An Existential + +```lean +structure Boundary (C : StepClass) (p : PFunctor) (α β : Type u) where + input : C.Str α + out : C.Str β + pos : C.Str p.A + idx : C.Str p.Idx +``` + +A `Boundary` is always a *parameter* of a realizability statement. A statement +of the form `∃ bd, IsRealizableBy C bd program` is **vacuous**: a representation +is only required to be admissible, not canonical, so an adversarially chosen +encoding can precompute across the boundary. Only the machine's own state +representation is chosen by the realization — and that choice is harmless, being +exactly the freedom to pick a state layout. + +`pos` and `idx` are supplied independently. Nothing derives one from the other, +since a step class is not assumed to represent dependent sums. + +## The Predicates + +```lean +def IsRealizableBy (C) (bd) (program : α → FreeM p β) : Prop := + ∃ R : Realization C bd, R.machine.Implements program + +def IsRealizableWithin (C) (bd) (program : α → FreeM p β) (k : ℕ) : Prop := + ∃ R : Realization C bd, R.machine.ImplementsWithin program k +``` + +A `Realization` bundles a machine, a representation of its hidden state, and +three admissibility proofs — for `init`, `head`, and `updateFlat`. Constraining +`init` is what forbids smuggling precomputed advice into the initial state. + +`IsRealizableWithin.isTotalRollBound` extracts a bound on the *program*'s query +depth from the machine, and `IsRealizableWithin.isRealizableBy` drops the budget. + +## Universe Discipline + +`StepClass.Str` speaks about types in a single universe, so the realizability +predicates are stated at `p : PFunctor.{u, u}` with `α β : Type u`, hence +`State : Type u`. Then `p.A`, `p.Idx`, `β ⊕ p.A`, and `State × p.Idx` all live in +`Type u`. The underlying `DynComputation` API stays fully universe-polymorphic; +only this layer is pinned. Every intended instantiation target is monomorphic +anyway. + +## Instantiating With An External Complexity Class + +Complexity classes in the wild are presented on one concrete function type — +`Complexity.FP : Set (List Bool → List Bool)` in complexitylib, +`Cslib.Turing.PolyTimeComputable` on `List Symbol → List Symbol` in cslib — with +no encoding-generic predicate. `StepClass.ofWordClass` is the bridge: + +```lean +def ofWordClass (W : Type u) (Q : (W → W) → Prop) (hid : Q id) + (hcomp : ∀ {f g}, Q f → Q g → Q (g ∘ f)) : StepClass.{u, u} where + Str A := { encode : A → W // Function.Injective encode } + Hom eA eB f := ∃ q, Q q ∧ ∀ x, q (eA.1 x) = eB.1 (f x) +``` + +Injectivity of the encoding is the only semantic demand, exactly as for a raw bit +encoding. + +Products and sums are *not* automatic. They need a pairing codec and a tagging +scheme whose operations the word class admits, supplied as `WordPairing` and +`WordTagging` and consumed by `ofWordClass.hasProd` / `ofWordClass.hasSum`. As of +this writing complexitylib has the ingredients (`Complexity.pair`, `unpair?`, +`delimit`) but has not exposed them as a class-level closure result, and cslib's +`PolyTimeComputable` has `id` and `comp` but no pairing or projection machines at +all. So a cslib instantiation is blocked upstream, not here. + +`StepClass.computable` — Mathlib's `Primcodable` representations and `Computable` +functions — is the in-repo instance that works today and exercises every mixin. + +## Known Gaps + +- **No cost-bearing layer.** `Hom` is `Prop`-valued, so nothing here measures + running time or description size. The successor layer needs `Hom` replaced by a + `Type`-valued witness field carrying measures in an ordered semiring, with + `size` additive under composition and `time` composing by substitution. +- **`ImplementsWithin` is pinned to a uniform `ℕ` budget.** `FreeM.IsRollBound` + is already generic in the budget type; `ImplementsWithin` is not. +- **No terminal or initial representation**, hence only binary distributivity and + no unparameterized equality test. Nothing needs them; adding them would tax + every instance. +- **Constant maps are not assumed admissible**, with one exception: `HasOption` + asserts `none_mem`, because a machine that has returned takes no step and so has + a constantly-`none` transition. Everything else — `isRealizableBy_pure`, for + instance — takes constant-admissibility as a per-theorem hypothesis. +- **`Lens.IsAdmissible` has no `.id` and no `.comp`.** This is not an oversight: + `pullHeadIdx` compares the incoming answer's tag against the position the lens + exposes, so even the identity lens's pullback performs an equality test on + positions. Admissibility of a lens is a genuine hypothesis about the class, + satisfiable by every realistic one but not derivable from the mixins. It is also + why `wrap` needs the hypothesis and `seqComp` does not. +- **No internal-language presentation.** An inductive syntax for the free + distributive category over the class's own maps, with one induction discharging + all plumbing, is real prior art on paper (Cockett–Fukushima's Charity; Vigna, + *Distributive computability*, 2003) and appears to be unformalized in any proof + assistant. It would replace the hand-assembled combinator chains in + `Closure.lean` with "exhibit a term". Worth doing if the combinator lemmas start + multiplying; over-engineering for the five closure theorems here. + +## References + +See [`REFERENCES.md`](../../REFERENCES.md) — `AM74`, `AMMS13`, `PR89`, `Uus15`, +`PM15`, `Blum67`, `GHP09` for the realizability notion, and `Coc93`, `CLW93`, +`Wal91`, `CF92`, `CDGH12`, `CH08`, `Clo99` for the distributive-category and +function-algebra vocabulary; plus `SN24`, `LS25`, and `Abe26`. + +Terminology follows classical (co)algebraic *realization* theory rather than the +word "implementation", which Aberlé (2026) uses for the free-monad Kleisli +morphism — that is, for the program side. + +One clash worth flagging: in computable analysis *admissible representation* is a +fixed technical term (Weihrauch 1985), where "admissible" qualifies the +representation rather than the function class. This layer uses "admissible" in the +sense of Petcher–Morrisett's FCF admissibility predicate — a property of a +function, relative to chosen representations. diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index 0be98fe..61ab20a 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -22,6 +22,8 @@ PolyFun/ Multiparty/ per-party local view modes, observation kernels Concurrent/ structural and dynamic concurrent semantics UC/ open-process / open-theory layer (no security content) + Realizability/ step classes and realizability of free programs by + machines whose transition functions are admissible Control/ monad/comonad and LTS infrastructure (Coalgebra, Comonad, Lawful, Free, Iter, Bisimulation, LTS/Trace) Logic/ small logic helpers (HEq) @@ -183,6 +185,14 @@ Interaction/{Concurrent, Basic} -> Interaction/UC/{Interface, Emulates, MachineId, EnvAction, EnvOpenProcess, CorruptionModel, MomentaryCorruption, Leakage} + +PFunctor/Basic -> Realizability/StepClass +PFunctor/Dynamical/DynComputation/Bounded -> Realizability/Machine +Realizability/{StepClass, Machine} -> Realizability/Basic + -> Realizability/Closure + -> Realizability/Instances + (Instances additionally draws on Mathlib's Computability and Fintype layers; + nothing under PFunctor/, ITree/, or Interaction/ depends on Realizability/) ``` `PolyFun.lean` is a generated umbrella import file, not a hand-maintained diff --git a/lake-manifest.json b/lake-manifest.json index c780044..140d685 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "197a7be621263b84c67ca4f803f69205b36d06df", + "rev": "93aa05752a62ad3498e734d5b75fcbff965891ce", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.0", + "inputRev": "v4.32.2", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lakefile.toml b/lakefile.toml index c4df044..f5596e8 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -28,16 +28,16 @@ weak.linter.allScriptsDocumented = false linter.mathlibStandardSet = true linter.style.longFile = 1500 -# Pinned to Lean v4.32.0 (matches `lean-toolchain`). +# Pinned to Lean v4.32.2 (matches `lean-toolchain`). [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.32.0" +rev = "v4.32.2" [[require]] name = "cslib" scope = "leanprover" -rev = "v4.32.0" +rev = "v4.32.2" [[lean_lib]] name = "PolyFun"