Evaluation traces

Def:eval_trace–Thm:deterministic_Trace (main.tex:1114–1157).

Trace, consistency, completeness (Def:eval_trace, main.tex:1114–1127)

def Nock.Verb.Step (a b : Verb) : Prop

Def:eval_trace (main.tex:1118). Consistent step: Nock(tᵢ, tᵢ₊₁) = 0.

Equations

• a.Step b = (a.next = some b)

theorem Nock.Verb.Step.det {a b b' : Verb} (h : a.Step b) (h' : a.Step b') : b = b'

The transition relation is deterministic: next is a function.

def Nock.Verb.Consistent : List Verb → Prop

Def:eval_trace (main.tex:1114–1127). Consistent: ∀ i ∈ [n], Nock(tᵢ, tᵢ₊₁) = 0.

Equations

• Nock.Verb.Consistent [] = True
• Nock.Verb.Consistent [head] = True
• Nock.Verb.Consistent (a :: b :: rest) = (a.Step b ∧ Nock.Verb.Consistent (b :: rest))

def Nock.Verb.Complete (T : List Verb) : Prop

Def:eval_trace (main.tex:1114–1127). Complete: tₙ is in terminal state or null.

Equations

• Nock.Verb.Complete T = ∃ (v : Nock.Verb), T.getLast? = some v ∧ v.next = none

def Nock.Verb.TraceOf (F : Verb) (T : List Verb) : Prop

Def:eval_trace (main.tex:1114–1127). Consistent trace of F: t₀ = F and ∀ i ∈ [n], Nock(tᵢ, tᵢ₊₁) = 0.

Equations

• F.TraceOf T = (T.head? = some F ∧ Nock.Verb.Consistent T)

def Nock.Verb.Continuation (F c : Verb) : Prop

Def:eval_trace (main.tex:1114–1127). If c ∈ T(F), c is a continuation (of F).

Equations

• F.Continuation c = ∃ (T : List Nock.Verb), F.TraceOf T ∧ c ∈ T

def Nock.Verb.Valid (F : Verb) : Prop

Def:eval_trace (main.tex:1114–1127). Valid: T complete and tₙ is not null.

Equations

• F.Valid = ∃ (T : List Nock.Verb), ∃ (v : Nock.Verb), F.TraceOf T ∧ T.getLast? = some v ∧ v.next = none ∧ v.isTerminal = true

def Nock.Verb.Invalid (F : Verb) : Prop

Def:eval_trace (main.tex:1114–1127). Invalid: T complete and tₙ is null.

Equations

• F.Invalid = ∃ (T : List Nock.Verb), ∃ (v : Nock.Verb), F.TraceOf T ∧ T.getLast? = some v ∧ v.next = none ∧ v.isTerminal = false

def Nock.Verb.Finite (F : Verb) : Prop

Def:Nock (main.tex:1130–1134). F terminates (is finite) if F ∈ NockVM^Λ := {F | ∃ complete T=(t₀,…,tₙ) s.t. t₀=F, λ≤Λ}.

Equations

• F.Finite = ∃ (T : List Nock.Verb), F.TraceOf T ∧ Nock.Verb.Complete T

def Nock.Verb.FiniteTransition (F : Verb) : Prop

FiniteTransitions^Λ (main.tex:1147). FiniteTransitions^Λ := {F | F is a continuation of a finite verb and λ ≤ Λ}.

Equations

• F.FiniteTransition = ∃ (F0 : Nock.Verb), ∃ (T : List Nock.Verb), F0.TraceOf T ∧ Nock.Verb.Complete T ∧ F ∈ T

Small list helpers (Lean core only)

Lem:domain (main.tex:1141–1142)

theorem Nock.Verb.domain {c t : Verb} (h : c.Step t) : ∃ (i : Nat), ∃ (sub : Verb), c.getIndex = some i ∧ map i c = some sub ∧ sub.inDomain = true

Lem:domain (main.tex:1141–1142). Let c be a continuation not followed by a null operator in a consistent evaluation trace. Then map(c, getIndex(c)) ∈ D(V).

lemma:equiv_continuations (main.tex:1150–1153)

theorem Nock.Verb.equiv_continuations (F : Verb) : F.Finite ↔ F.FiniteTransition

lemma:equiv_continuations (main.tex:1150–1153). NockVM^Λ ≡ FiniteTransitions^Λ.

Thm:deterministic_Trace (main.tex:1156–1157)

theorem Nock.Verb.trace_unique (T1 T2 : List Verb) : Consistent T1 → Consistent T2 → T1.head? = T2.head? → T1.length = T2.length → T1 = T2

Inductive core of determinism: Step is functional, so equal heads and lengths force equality.

theorem Nock.Verb.deterministic_Trace {F : Verb} {n : Nat} {T1 T2 : List Verb} (h1 : F.TraceOf T1) (h2 : F.TraceOf T2) (hn1 : T1.length = n + 1) (hn2 : T2.length = n + 1) : T1 = T2

Thm:deterministic_Trace (main.tex:1156–1157). If map enforces a strict ordering on finite verbs, then for every finite verb F and integer n, there exists at most one consistent evaluation trace of size n for F.

Conditional deterministic-trace theorem (main.tex:1156–1157)

def Nock.Verb.ConsistentR (R : Verb → Verb → Prop) : List Verb → Prop

Consistency of a trace with respect to an arbitrary transition relation R (Consistent is the special case R = Step).

Equations

• Nock.Verb.ConsistentR R [] = True
• Nock.Verb.ConsistentR R [head] = True
• Nock.Verb.ConsistentR R (a :: b :: rest) = (R a b ∧ Nock.Verb.ConsistentR R (b :: rest))

theorem Nock.Verb.trace_unique_of_det {R : Verb → Verb → Prop} (hdet : ∀ {a b b' : Verb}, R a b → R a b' → b = b') (T1 T2 : List Verb) : ConsistentR R T1 → ConsistentR R T2 → T1.head? = T2.head? → T1.length = T2.length → T1 = T2

Trace uniqueness for any deterministic transition relation. Determinism of the relation is the only hypothesis; this is the inductive core shared by the functional and the strict-order forms.

def Nock.Verb.TraceOfR (R : Verb → Verb → Prop) (F : Verb) (T : List Verb) : Prop

A trace w.r.t. an arbitrary transition relation R (generalizing TraceOf).

Equations

• Nock.Verb.TraceOfR R F T = (T.head? = some F ∧ Nock.Verb.ConsistentR R T)

theorem Nock.Verb.selStep_deterministic_Trace {lt : Nat → Nat → Prop} (hs : StrictSelect lt) {F : Verb} {n : Nat} {T1 T2 : List Verb} (h1 : TraceOfR (SelStep lt) F T1) (h2 : TraceOfR (SelStep lt) F T2) (hn1 : T1.length = n + 1) (hn2 : T2.length = n + 1) : T1 = T2

Thm:deterministic_Trace (main.tex:1156–1157). If map enforces a strict ordering on finite verbs, then for every finite verb F and integer n, there exists at most one consistent evaluation trace of size n for F.

theorem Nock.Verb.consistent_iff_selStep (T : List Verb) : Consistent T ↔ ConsistentR (SelStep dfsLt) T

The concrete consistency (Consistent, via next) is exactly SelStep dfsLt consistency, because next realizes the DFS selection step (next_eq_some_iff).

theorem Nock.Verb.deterministic_Trace_strict {F : Verb} {n : Nat} {T1 T2 : List Verb} (h1 : F.TraceOf T1) (h2 : F.TraceOf T2) (hn1 : T1.length = n + 1) (hn2 : T2.length = n + 1) : T1 = T2

Thm:deterministic_Trace (main.tex:1156–1157). If map enforces a strict ordering on finite verbs, then for every finite verb F and integer n, there exists at most one consistent evaluation trace of size n for F.

Corollary: valid and invalid verbs are finite (main.tex:1137–1138)

theorem Nock.Verb.finite_of_valid {F : Verb} (h : F.Valid) : F.Finite

Corr (main.tex:1137–1138). All valid and invalid verbs are finite.

theorem Nock.Verb.finite_of_invalid {F : Verb} (h : F.Invalid) : F.Finite

Corr (main.tex:1137–1138). All valid and invalid verbs are finite.

theorem Nock.Verb.finite_of_valid_or_invalid {F : Verb} (h : F.Valid ∨ F.Invalid) : F.Finite

Corr (main.tex:1137–1138). All valid and invalid verbs are finite.

Size bound λ ≤ Λ on paper languages (main.tex:1130–1147)

def Nock.Verb.size (F : Verb) : Nat

The paper's length λ of a verb: the number of leaves of its noun.

Equations

• F.size = F.leaves

def Nock.Verb.FiniteΛ (Λ : Nat) (F : Verb) : Prop

Def:Nock (main.tex:1130–1134). NockVM^Λ := {F ∈ V^λ | ∃ complete T with t₀=F, and λ ≤ Λ}.

Equations

• Nock.Verb.FiniteΛ Λ F = (F.Finite ∧ F.size ≤ Λ)

def Nock.Verb.FiniteTransitionΛ (Λ : Nat) (F : Verb) : Prop

FiniteTransitions^Λ (main.tex:1147). FiniteTransitions^Λ := {F | F is a continuation of a finite verb and λ ≤ Λ}.

Equations

• Nock.Verb.FiniteTransitionΛ Λ F = (F.FiniteTransition ∧ F.size ≤ Λ)

theorem Nock.Verb.equiv_continuationsΛ (Λ : Nat) (F : Verb) : FiniteΛ Λ F ↔ FiniteTransitionΛ Λ F

lemma:equiv_continuations (main.tex:1150–1153). NockVM^Λ ≡ FiniteTransitions^Λ.

NockProgram^Λ / NockValidProgram^Λ (main.tex:1090–1149)

def Nock.Verb.IsNockProgram (Λ : Nat) (F : Verb) : Prop

Def:NockProgram (main.tex:1090–1098). F = *[subject, formula] with subject, formula terminal; NockProgram^Λ := {F | λ ≤ Λ}.

Equations

• One or more equations did not get rendered due to their size.

def Nock.Verb.NockValidProgramΛ (Λ : Nat) (F : Verb) : Prop

F ∈ NockValidProgram^Λ (main.tex:1145): a Nock program that is a valid verb.

Equations

• Nock.Verb.NockValidProgramΛ Λ F = (Nock.Verb.IsNockProgram Λ F ∧ F.Valid)

def Nock.Verb.SubLang (P Q : Verb → Prop) : Prop

Subset of verb-languages (⊆): every verb in P is in Q.

Equations

• Nock.Verb.SubLang P Q = ∀ ⦃F : Nock.Verb⦄, P F → Q F

def Nock.Verb.SSubLang (P Q : Verb → Prop) : Prop

Strict inclusion of verb-languages (⊊): P ⊆ Q together with a witness in Q ∖ P. This is exactly the meaning of the set-theoretic ⊊ (proper subset = subset + a strictly separating element), spelled out at the predicate level.

Equations

• Nock.Verb.SSubLang P Q = (Nock.Verb.SubLang P Q ∧ ∃ (F : Nock.Verb), Q F ∧ ¬P F)

theorem Nock.Verb.finite_leaf (n : Nat) : (leaf n).Finite

A terminal leaf is finite: its one-element trace [leaf n] is complete.

theorem Nock.Verb.nockValidProgram_ssubset_nockVM {Λ : Nat} (hΛ : 1 ≤ Λ) : SSubLang (NockValidProgramΛ Λ) (FiniteΛ Λ)

Strict inclusion (main.tex:1145). NockValidProgram^Λ ⊊ NockVM^Λ: every valid program is finite of length ≤ Λ (⊆, via finite_of_valid), and the containment is strict — e.g. the terminal leaf 0 is a finite verb of length 1 ≤ Λ that is not a Nock program (it is not of the form *[subject, formula]; main.tex:1145 "not all elements of NockVM^Λ are actually programs"). The side condition 1 ≤ Λ is necessary: for Λ = 0 both languages are empty (every verb has ≥ 1 leaf), so ∅ ⊊ ∅ fails; the paper's ⊊ is meant for the non-degenerate range.

NockVMROM^Λ at the verb level (main.tex:1160)

def Nock.Verb.StepROM (a b : Verb) : Prop

A single NockVMROM step (next restricted to exclude OP₁₀).

Equations

• a.StepROM b = (a.nextROM = some b)

theorem Nock.Verb.step_of_stepROM {a b : Verb} (h : a.StepROM b) : a.Step b

Every ROM step is a Nock step (nextROM ⊆ next; main.tex:1160).

def Nock.Verb.CompleteROM (T : List Verb) : Prop

A trace is ROM-complete iff its last verb has no nextROM-successor.

Equations

• Nock.Verb.CompleteROM T = ∃ (v : Nock.Verb), T.getLast? = some v ∧ v.nextROM = none

def Nock.Verb.TraceOfROM (F : Verb) (T : List Verb) : Prop

T is a consistent ROM trace of F (uses StepROM for consistency).

Equations

• F.TraceOfROM T = (T.head? = some F ∧ Nock.Verb.ConsistentR Nock.Verb.StepROM T)

theorem Nock.Verb.consistent_of_consistentROM (T : List Verb) : ConsistentR StepROM T → Consistent T

Every consistent ROM trace is a consistent Nock trace (ROM steps are Nock steps).

theorem Nock.Verb.traceOf_of_traceOfROM {F : Verb} {T : List Verb} (h : F.TraceOfROM T) : F.TraceOf T

Every ROM trace of F is a Nock trace of F.

def Nock.Verb.FiniteROM (F : Verb) : Prop

F is ROM-finite (F ∈ NockVMROM): it has a complete ROM trace.

Equations

• F.FiniteROM = ∃ (T : List Nock.Verb), F.TraceOfROM T ∧ Nock.Verb.CompleteROM T

def Nock.Verb.FiniteROMΛ (Λ : Nat) (F : Verb) : Prop

F ∈ NockVMROM^Λ: ROM-finite and of length λ ≤ Λ (Def:Nock without OP₁₀).

Equations

• Nock.Verb.FiniteROMΛ Λ F = (F.FiniteROM ∧ F.size ≤ Λ)

def Nock.Verb.ValidROM (F : Verb) : Prop

F is ROM-valid: it has a complete ROM trace ending in a terminal (non-crash) verb.

Equations

• F.ValidROM = ∃ (T : List Nock.Verb), ∃ (v : Nock.Verb), F.TraceOfROM T ∧ T.getLast? = some v ∧ v.nextROM = none ∧ v.isTerminal = true

theorem Nock.Verb.finite_of_validROM {F : Verb} (h : F.ValidROM) : F.Finite

ROM-valid ⇒ finite. A verb that terminates in a terminal state using only ROM steps is Nock-finite: its ROM trace is a Nock trace (traceOf_of_traceOfROM), and its terminal last verb has no Nock successor either (next_none_of_terminal), so the trace is Nock-complete.

The two-verb checker Nock matches Step (App A, main.tex:1639)

theorem Nock.Verb.nockCheck_iff_step {a : Verb} {b : Option Verb} : a.NockCheck b = true ↔ (∃ (v : Verb), b = some v ∧ a.Step v) ∨ b = none ∧ a.Crashes

Nock checker ↔ trace consistency (Step) + crash. NockCheck a b = true (paper's accept 0, main.tex:1118) iff b is a Step-successor of a (Step a v, i.e. a consistent transition Nock(a,v)=0) or a crashes and b = ⊥ (b = none). This is the genuine biconditional making the two-verb checker 1-1 with the forward semantics Step plus the crash branch (defeq to Verb.nockCheck_eq_true_iff, since Step a v := next a = some v).

Verifiable crash ↔ the paper's ⊥ (Invalid, main.tex:1124)

Nock.Verb.eval reports a three-way Outcome; a crash result is tied here to the paper's program-level ⊥: the evaluated program v is Invalid — its trace is complete and ends at a stuck, non-terminal state (main.tex:1124). Soundness (eval_crash_invalid), completeness (eval_crash_complete), and their biconditional (eval_crash_iff_invalid) pin eval's crash to exactly that object; eval_crash_checked further exhibits the reached ⊥ state and its NockCheck-accepted crash edge.

theorem Nock.Verb.crash_of_trace (S : List Verb) (u w : Verb) : S.head? = some u → Consistent S → S.getLast? = some w → w.next = none → w.isTerminal = false → eval S.length u = Outcome.crash

If S is a consistent trace of u (head u, Consistent S) whose last state w is a stuck non-terminal (next w = none, ¬terminal), then eval reports a crash at fuel S.length.

theorem Nock.Verb.eval_crash_invalid {n : Nat} {v : Verb} (h : eval n v = Outcome.crash) : v.Invalid

Crash soundness (program-tied). A crash reported by eval for the program v means v is Invalid: its evaluation trace is complete and ends at a stuck non-terminal — the paper's ⊥ (main.tex:1124). Unlike a bare "some crashing verb exists", the witness is the trace of v.

theorem Nock.Verb.eval_crash_complete {v : Verb} (h : v.Invalid) : ∃ (n : Nat), eval n v = Outcome.crash

Crash completeness. Every Invalid program (complete trace ending stuck non-terminal, main.tex:1124) is eventually reported as a crash by eval — at fuel = its trace length.

theorem Nock.Verb.eval_crash_iff_invalid {v : Verb} : (∃ (n : Nat), eval n v = Outcome.crash) ↔ v.Invalid

Verifiable crash ↔ ⊥. eval crashes on v (at some fuel) iff v is Invalid — the clean soundness/completeness biconditional at the paper's ⊥ (main.tex:1124).

theorem Nock.Verb.eval_crash_checked {n : Nat} {v : Verb} (h : eval n v = Outcome.crash) : ∃ (T : List Verb), ∃ (w : Verb), v.TraceOf T ∧ T.getLast? = some w ∧ w.Crashes ∧ w.NockCheck none = true

The reported crash is a checked ⊥ (program-tied). A crash for v exhibits the trace of v reaching a state w that genuinely Crashes and whose ⊥-edge is accepted by the two-verb checker (NockCheck w none = true) — verifiability tied to the evaluated program.