Hurford's universal numeral grammar

[Hur75] [IM06]

[Hur75]'s phrase-structure grammar for number-names (his (2), p. 19), proposed as the universal base of numeral systems:

• NUMBER → {one | PHRASE} (NUMBER)
• PHRASE → NUMBER M
• M → {ten | NUMBER M}

with the three projection rules of his (23) (pp. 29–30): the value of a NUMBER is the sum of its immediate constituents, of a PHRASE the product, and of an M the second constituent raised to the power of the first. So twenty-three is [[two ten] three] = 2·10 + 3, thousand is [three ten] = 10³.

His deeper claim ((26)–(29)): the three rules are one operation, CALCULATE, indexed by constituent depth — NUMBERs (depth 1) add, PHRASEs (depth 2) multiply, Ms (depth 3) exponentiate, each operation the iteration of the one before. value_eq_calculate states the unification; calculate_succ_iterate states the iteration ladder its complexity ordering rests on.

Consumers: Studies/IoninMatushansky2006.lean (their §3.3 adopts Hurford's cardinals-as-nouns; their §4.3 order conventions constrain which of these structures surface) and Studies/JansenPollmann2001.lean (10-ness as digit×M expressibility).

Main declarations

• Number, Phrase, M: the three syntactic categories, with value
• Number.tally, M.tenPow: canonical digit and base-power structures
• calculate: the depth-indexed arithmetic (his (26))

Main results

• value_eq_calculate: the three projection rules are calculate at depths 1–3
• calculate_succ_iterate: each operation iterates the previous one
• Number.exists_value_eq: every positive number is expressible (the tally structure his rule schema (6) generates)

The phrase-structure categories (his (2))

inductive Syntax.Numeral.Number : Type

NUMBER → {one | PHRASE} (NUMBER).

• one : Number

  NUMBER → one.

• oneAnd (rest : Number) : Number

  NUMBER → one NUMBER.

• phrase (p : Phrase) : Number

  NUMBER → PHRASE.

• phraseAnd (p : Phrase) (rest : Number) : Number

  NUMBER → PHRASE NUMBER — e.g. twenty-three.

partial def Syntax.Numeral.instReprM.repr_3 : M → ℕ → Std.Format

@[implicit_reducible]

instance Syntax.Numeral.instReprM : Repr M

Equations

• Syntax.Numeral.instReprM = { reprPrec := Syntax.Numeral.instReprM.repr_3 }

partial def Syntax.Numeral.instReprPhrase.repr_1 : Number → ℕ → Std.Format

partial def Syntax.Numeral.instReprM.repr_1 : Number → ℕ → Std.Format

partial def Syntax.Numeral.instReprNumber.repr_2 : Phrase → ℕ → Std.Format

@[implicit_reducible]

instance Syntax.Numeral.instReprPhrase : Repr Phrase

Equations

• Syntax.Numeral.instReprPhrase = { reprPrec := Syntax.Numeral.instReprPhrase.repr_2 }

partial def Syntax.Numeral.instReprNumber.repr_3 : M → ℕ → Std.Format

partial def Syntax.Numeral.instReprNumber.repr_1 : Number → ℕ → Std.Format

partial def Syntax.Numeral.instReprM.repr_2 : Phrase → ℕ → Std.Format

@[implicit_reducible]

instance Syntax.Numeral.instReprNumber : Repr Number

Equations

• Syntax.Numeral.instReprNumber = { reprPrec := Syntax.Numeral.instReprNumber.repr_1 }

partial def Syntax.Numeral.instReprPhrase.repr_3 : M → ℕ → Std.Format

partial def Syntax.Numeral.instReprPhrase.repr_2 : Phrase → ℕ → Std.Format

inductive Syntax.Numeral.Phrase : Type

PHRASE → NUMBER M — e.g. two hundred.

• mk (n : Number) (m : M) : Phrase

inductive Syntax.Numeral.M : Type

M → {ten | NUMBER M} — the base-word hierarchy: ten, hundred ([two ten] = 10²), thousand ([three ten] = 10³), ….

• ten : M
• mk (n : Number) (m : M) : M

The projection rules (his (23))

def Syntax.Numeral.Number.value : Number → ℕ

The value of a NUMBER: the sum of its immediate constituents.

Equations

• Syntax.Numeral.Number.one.value = 1
• a.oneAnd.value = 1 + a.value
• (Syntax.Numeral.Number.phrase a).value = a.value
• (Syntax.Numeral.Number.phraseAnd a a_1).value = a.value + a_1.value

def Syntax.Numeral.Phrase.value : Phrase → ℕ

The value of a PHRASE: the product of its immediate constituents.

Equations

• (Syntax.Numeral.Phrase.mk a a_1).value = a.value * a_1.value

def Syntax.Numeral.M.value : M → ℕ

The value of an M: the second constituent raised to the power of the first.

Equations

• Syntax.Numeral.M.ten.value = 10
• (Syntax.Numeral.M.mk a a_1).value = a_1.value ^ a.value

Canonical structures

def Syntax.Numeral.Number.tally : ℕ → Number

The bare tally NUMBER: n + 1 iterations of one — the structures his rule schema (6) generates before lexicalization compresses them.

Equations

• Syntax.Numeral.Number.tally 0 = Syntax.Numeral.Number.one
• Syntax.Numeral.Number.tally n.succ = (Syntax.Numeral.Number.tally n).oneAnd

@[simp]

theorem Syntax.Numeral.Number.value_tally (n : ℕ) : (tally n).value = n + 1

theorem Syntax.Numeral.Number.exists_value_eq (n : ℕ) (hn : 1 ≤ n) : ∃ (e : Number), e.value = n

Every positive number is expressible — numeral systems name the whole of ℕ⁺ (his ch. 1 universal).

def Syntax.Numeral.M.tenPow : ℕ → M

The base-power M: tenPow k is the M of value 10^(k+1) — ten, hundred ([two ten]), thousand ([three ten]), ….

Equations

• Syntax.Numeral.M.tenPow 0 = Syntax.Numeral.M.ten
• Syntax.Numeral.M.tenPow n.succ = Syntax.Numeral.M.mk (Syntax.Numeral.Number.tally (n + 1)) Syntax.Numeral.M.ten

@[simp]

theorem Syntax.Numeral.M.value_tenPow (k : ℕ) : (tenPow k).value = 10 ^ (k + 1)

theorem Syntax.Numeral.M.value_pos (m : M) : 0 < m.value

theorem Syntax.Numeral.Phrase.value_tally_tenPow (m k : ℕ) : (mk (Number.tally m) (M.tenPow k)).value = (m + 1) * 10 ^ (k + 1)

A digit×base PHRASE — four hundred as [[four] [two ten]] — has value m × 10^(k+1).

CALCULATE: one depth-indexed operation (his (26)–(29))

The three projection rules order themselves by complexity — addition, multiplication, exponentiation — and each is the iteration of the one before, bottoming out in incrementing (adding a tally mark). His (29): a constituent of depth d with immediate constituents x, y is valued CALCULATE d x y, so the semantic component is a single rule.

def Syntax.Numeral.calculate : ℕ → ℕ → ℕ → ℕ

The depth-indexed arithmetic: depth 1 adds (NUMBER), depth 2 multiplies (PHRASE), depth 3 and beyond exponentiates (M).

Equations

• Syntax.Numeral.calculate 1 x✝¹ x✝ = x✝¹ + x✝
• Syntax.Numeral.calculate 2 x✝¹ x✝ = x✝¹ * x✝
• Syntax.Numeral.calculate x✝² x✝¹ x✝ = x✝ ^ x✝¹

theorem Syntax.Numeral.value_eq_calculate (p : Phrase) (rest n : Number) (m : M) : (Number.phraseAnd p rest).value = calculate 1 p.value rest.value ∧ (Phrase.mk n m).value = calculate 2 n.value m.value ∧ (M.mk n m).value = calculate 3 n.value m.value

His (29): the three projection rules are calculate at the constituent's depth — NUMBERs at depth 1, PHRASEs at depth 2, Ms at depth 3.

theorem Syntax.Numeral.calculate_succ_iterate (x y : ℕ) : calculate 2 x y = (calculate 1 y)^[x] 0 ∧ calculate 3 x y = (calculate 2 y)^[x] 1

The complexity ladder behind the depth-indexing: each operation is the iteration of the one below — multiplication iterates addition, exponentiation iterates multiplication.