Nouns

Inductive proper binary trees with Nat atoms (main.tex:318–349).

inductive Nock.Noun : Type

Def:noun (main.tex:347–349). n := (t, dt) ∈ L_dk^{2·(λ−1)} × DT(F)^λ := N^λ(F) is a noun of size λ over field F. (paper: field F; Lean: Nat leaves.)

• atom : Nat → Noun
• cell : Noun → Noun → Noun

@[instance_reducible]

instance Nock.instReprNoun : Repr Noun

Equations

• Nock.instReprNoun = { reprPrec := Nock.instReprNoun.repr }

def Nock.instReprNoun.repr : Noun → Nat → Std.Format

Equations

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

def Nock.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Nock.instDecidableEqNoun.decEq (Nock.Noun.atom a) (Nock.Noun.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Nock.instDecidableEqNoun.decEq (Nock.Noun.atom a) (a_1.cell a_2) = isFalse ⋯
• Nock.instDecidableEqNoun.decEq (a.cell a_1) (Nock.Noun.atom a_2) = isFalse ⋯

@[instance_reducible]

instance Nock.instDecidableEqNoun : DecidableEq Noun

Equations

• Nock.instDecidableEqNoun = Nock.instDecidableEqNoun.decEq

@[instance_reducible]

instance Nock.instInhabitedNoun : Inhabited Noun

Equations

• Nock.instInhabitedNoun = { default := Nock.instInhabitedNoun.default }

def Nock.Noun.isCell : Noun → Bool

? in Nock terms: is this noun a cell?

Equations

• (a.cell a_1).isCell = true
• (Nock.Noun.atom a).isCell = false

def Nock.Noun.isAtom (n : Noun) : Bool

Test whether a noun is an atomic value rather than a cell.

Equations

• n.isAtom = !n.isCell

def Nock.Noun.leaves : Noun → Nat

Def:tree_nodes (main.tex:329–331). Given t ∈ L_full_BT, a node with no children is a leaf; a non-leaf is an internal node.

Equations

• (Nock.Noun.atom a).leaves = 1
• (l.cell r).leaves = l.leaves + r.leaves

def Nock.Noun.size : Noun → Nat

Total node count.

Equations

• (Nock.Noun.atom a).size = 1
• (l.cell r).size = 1 + l.size + r.size

def Nock.Noun.internal : Noun → Nat

Def:tree_nodes (main.tex:329–331). Given t ∈ L_full_BT, a node with no children is a leaf; a non-leaf is an internal node.

Equations

• (Nock.Noun.atom a).internal = 0
• (l.cell r).internal = 1 + l.internal + r.internal

Lem:pbt_size (main.tex:333–335)

theorem Nock.Noun.size_add_one (n : Noun) : n.size + 1 = 2 * n.leaves

theorem Nock.Noun.pbt_size (n : Noun) : n.size = 2 * n.leaves - 1 ∧ n.internal = n.leaves - 1

Lem:pbt_size (main.tex:333–335). A tree t ∈ L_full_BT^{2λ−1} has λ−1 internal and λ leaf nodes.

theorem Nock.Noun.pbt_size_of_size {n : Noun} {lam : Nat} (hlam : 1 ≤ lam) (h : n.size = 2 * lam - 1) : n.leaves = lam ∧ n.internal = lam - 1

Lem:pbt_size (main.tex:333–335). A tree t ∈ L_full_BT^{2λ−1} has λ−1 internal and λ leaf nodes.

theorem Nock.Noun.size_eq_leaves_add_internal (n : Noun) : n.size = n.leaves + n.internal

Every node of a proper binary tree is a leaf or an internal node: size = leaves + internal.

theorem Nock.Noun.one_le_leaves (n : Noun) : 1 ≤ n.leaves

Every noun has at least one leaf (atoms contribute 1; cells sum positive leaf counts).

The circular S-expression object at main.tex:305–312 is out of scope: the paper restricts subsequent use to proper binary trees.

Proper n-ary trees (main.tex:351–364)

The paper includes this unused generalization for completeness.

inductive Nock.NAryTree (k : Nat) : Type

Def proper n-ary (main.tex:355–363). L_full_T,n = { t ∈ T^n | (size(t)=1) ∪ ((⋂_{1≤i≤n} child_i(t) ∈ L_full_T^n) ∩ (∅ = ⋂_{1≤i≤n} child_i(t))) }; L^λ_full_T,n = { t ∈ L_full_T^n | size(t)=λ }. Unused in paper body.

• leaf {k : Nat} : NAryTree k
• node {k : Nat} : (Fin k → NAryTree k) → NAryTree k

def Nock.NAryTree.childi {k : Nat} (i : Fin k) : NAryTree k → Option (NAryTree k)

Return the indexed child of an internal n-ary tree, or none at a leaf.

Equations

• Nock.NAryTree.childi i Nock.NAryTree.leaf = none
• Nock.NAryTree.childi i (Nock.NAryTree.node f) = some (f i)