SPTree: Syntactic Computation Trees for SPComp

This file defines SPTree α, a syntactic (free-monad-like) representation of stateful probabilistic computations. Unlike SPComp α = Heap → SDistr (α × Heap) (which is denotational), SPTree preserves syntactic structure, enabling cost analysis by structural recursion.

Main definitions

• SPTree — syntactic computation tree (ret, sample, get, set, fail)
• SPTree.compile — denotational semantics (→ SPComp)
• SPTree.queryCost — worst-case operation count (structural recursion)
• SPTree.bind — monadic composition (substitution at leaves)

Main results

• compile_bind — compilation commutes with bind
• queryCost_bind — cost of bind ≤ cost of tree + bound on continuation

SPTree Definition

inductive CatCrypt.Core.SPTree : Type → Type 1

Syntactic computation tree for stateful probabilistic programs.

Lives in Type 1 because sample quantifies over β : Type.

• ret {α : Type} : α → SPTree α
• sample {α : Type} (β : Type) (finβ : Fintype β) (neβ : Nonempty β) : (β → SPTree α) → SPTree α
• get {α : Type} (l : Location) : (l.ty → SPTree α) → SPTree α
• set {α : Type} (l : Location) : l.ty → SPTree α → SPTree α
• fail {α : Type} : SPTree α

Compilation to SPComp

noncomputable def CatCrypt.Core.SPTree.compile {α : Type} : SPTree α → SPComp α

Compile a syntax tree to its denotational semantics.

Equations

• (CatCrypt.Core.SPTree.ret a).compile = CatCrypt.Core.SPComp.pure a
• (CatCrypt.Core.SPTree.sample β finβ neβ k).compile = (CatCrypt.Core.SPComp.sample β).bind fun (b : β) => (k b).compile
• (CatCrypt.Core.SPTree.get l k).compile = (CatCrypt.Core.SPComp.get l).bind fun (v : l.ty) => (k v).compile
• (CatCrypt.Core.SPTree.set l v t).compile = (CatCrypt.Core.SPComp.set l v).bind fun (x : Unit) => t.compile
• CatCrypt.Core.SPTree.fail.compile = CatCrypt.Core.SPComp.fail

Query Cost

def CatCrypt.Core.SPTree.queryCost {α : Type} : SPTree α → ℕ

Worst-case operation count: counts sample + get + set operations. Uses Finset.univ.sup for branching to take the maximum cost across all possible continuations. Structurally recursive.

Equations

• (CatCrypt.Core.SPTree.ret a).queryCost = 0
• (CatCrypt.Core.SPTree.sample β finβ neβ k).queryCost = 1 + Finset.univ.sup fun (b : β) => (k b).queryCost
• (CatCrypt.Core.SPTree.get l k).queryCost = 1 + Finset.univ.sup fun (v : l.ty) => (k v).queryCost
• (CatCrypt.Core.SPTree.set l v t).queryCost = 1 + t.queryCost
• CatCrypt.Core.SPTree.fail.queryCost = 0

Monadic Bind (Substitution at Leaves)

def CatCrypt.Core.SPTree.bind {α β : Type} : SPTree α → (α → SPTree β) → SPTree β

Monadic bind: substitute f at every ret leaf of s.

Equations

• (CatCrypt.Core.SPTree.ret a).bind x✝ = x✝ a
• (CatCrypt.Core.SPTree.sample γ finγ neγ k).bind x✝ = CatCrypt.Core.SPTree.sample γ finγ neγ fun (c : γ) => (k c).bind x✝
• (CatCrypt.Core.SPTree.get l k).bind x✝ = CatCrypt.Core.SPTree.get l fun (v : l.ty) => (k v).bind x✝
• (CatCrypt.Core.SPTree.set l v t).bind x✝ = CatCrypt.Core.SPTree.set l v (t.bind x✝)
• CatCrypt.Core.SPTree.fail.bind x✝ = CatCrypt.Core.SPTree.fail

Simp Lemmas

@[simp]

theorem CatCrypt.Core.SPTree.compile_ret {α : Type} (a : α) : (ret a).compile = SPComp.pure a

@[simp]

theorem CatCrypt.Core.SPTree.compile_fail {α : Type} : fail.compile = SPComp.fail

@[simp]

theorem CatCrypt.Core.SPTree.queryCost_ret {α : Type} (a : α) : (ret a).queryCost = 0

@[simp]

theorem CatCrypt.Core.SPTree.queryCost_fail {α : Type} : fail.queryCost = 0

@[simp]

theorem CatCrypt.Core.SPTree.bind_ret_val {α β : Type} (a : α) (f : α → SPTree β) : (ret a).bind f = f a

@[simp]

theorem CatCrypt.Core.SPTree.bind_fail {α β : Type} (f : α → SPTree β) : fail.bind f = fail

Compile-Bind Correctness

theorem CatCrypt.Core.SPTree.compile_bind {α β : Type} (s : SPTree α) (f : α → SPTree β) : (s.bind f).compile = s.compile.bind fun (a : α) => (f a).compile

Compilation commutes with monadic bind.

Query Cost Bound for Bind

theorem CatCrypt.Core.SPTree.queryCost_bind {α β : Type} (s : SPTree α) (f : α → SPTree β) (bound : ℕ) (hf : ∀ (a : α), (f a).queryCost ≤ bound) : (s.bind f).queryCost ≤ s.queryCost + bound

Cost of bind ≤ cost of tree + uniform bound on continuation.

Monad Laws

theorem CatCrypt.Core.SPTree.ret_bind {α β : Type} (a : α) (f : α → SPTree β) : (ret a).bind f = f a

theorem CatCrypt.Core.SPTree.bind_ret {α : Type} (s : SPTree α) : s.bind ret = s

theorem CatCrypt.Core.SPTree.bind_assoc {α β γ : Type} (s : SPTree α) (f : α → SPTree β) (g : β → SPTree γ) : (s.bind f).bind g = s.bind fun (a : α) => (f a).bind g