Primcodable for Semiterm and Semiformula (issue #506) #
Semiterm.ofNat/Semiformula.ofNat are strong recursions on the code: the func branch reads an
argument vector out of the code and calls itself on each entry. Their Primrec versions go
through Primrec.nat_strong_rec (terms) and Primrec.nat_omega_rec' (formulas), whose step
functions this file builds. Two design points:
Everything happens at the level of codes. The table entry for a sub-code j is
encode (ofNat n j), and encode on Option is 0 for none and encode t + 1 for some t,
so a successful entry already contains the argument's toNat, one less than itself, and the
argument-vector code is rebuilt by arithmetic alone. No term is ever reconstructed, and nothing
here needs L or ξ decidable.
Option is kept out of the folds. stepVec returns ℕ with 0 for failure and r + 1 for
success with value r: with Option ℕ as the fold's accumulator, the Primrec combinators must
synthesise Primcodable for towers of products ending in Option ℕ, and elaboration diverges.
The ℕ encoding costs one - 1 per lookup and elaborates immediately.
Nat.natToList (Vorspiel/Nat/Matrix.lean) is used throughout for the same reason:
Nat.natToVec produces a Fin k → ℕ whose length lives in its type, which no Primrec
combinator can consume, so natToList is the same decoding without the dependency, and
natToVec_eq_some_iff lets the correctness proofs move between them.
Primitive-recursiveness of a language's symbol encodings, uniformly in the arity.
This is strictly stronger than [(k : ℕ) → Primcodable (L.Func k)], necessarily so:
Semiterm.ofNat reads the arity k out of the code being decoded and then calls
decode : ℕ → Option (L.Func k) at that k, so simulating it needs
(k, e) ↦ encode (decode e : Option (L.Func k)) to be primitive recursive as a function of the
pair. A per-arity family gives primitive recursiveness only at each fixed k, with no uniformity
across k.
- func : Primrec₂ fun (k e : ℕ) => Encodable.encode (Encodable.decode e)
- rel : Primrec₂ fun (k e : ℕ) => Encodable.encode (Encodable.decode e)
Instances
Equations
- FFL.FirstOrder.instPrimcodableFunc L k = { toEncodable := FFL.FirstOrder.Language.Encodable.func k, prim := ⋯ }
Equations
- FFL.FirstOrder.instPrimcodableRel L k = { toEncodable := FFL.FirstOrder.Language.Encodable.rel k, prim := ⋯ }
ℒₒᵣ satisfies the uniform condition: encode ∘ decode is
fun k e ↦ if (k = 0 ∨ k = 2) ∧ e < 2 then e + 1 else 0.
The argument-vector fold of the func branch. T is the table of values already computed by
the strong recursion, l the list of argument codes.
The result is 0 for failure and r + 1 for success with vector code r; see the module
docstring for why this is ℕ and not Option ℕ. A lookup that is absent or 0 — that is, an
argument whose own decoding failed — fails the whole fold.
Equations
Instances For
The four branches of Semiterm.ofNat at the level of codes, with d + 1 the code being
decoded. Branch 2 is the func case: it checks that the argument vector decodes to the recorded
arity, that the function symbol decodes, and that every argument's own decoding succeeded — the
last through stepVec, reading the table.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One step of the course-of-values recursion, at the level of codes: given the table T of the
values encode (ofNat n j) for every j < T.length, it returns encode (ofNat n T.length).
Equations
Instances For
Equations
- FFL.FirstOrder.Semiterm.table n e = List.map (fun (j : ℕ) => Encodable.encode (FFL.FirstOrder.Semiterm.ofNat n j)) (List.range e)
Instances For
On the table of all previously computed values, the step function returns the next one — the
obligation Primrec.nat_strong_rec asks for.
Four branches, matching ofNat's; the two atomic ones are arithmetic. In the func branch,
natToVec succeeding is tested as natToList having the recorded length
(natToVec_isSome_of_length/natToVec_eq_none_of_length), the function symbol's decoding is read
off encode ∘ decode being non-zero, and each argument's decoding is read out of the table, so
the branch never reconstructs a term; the argument-vector code comes from stepVec_ofFn, and when
an argument fails to decode, its table entry is 0 and stepVec_eq_zero collapses the fold,
matching Matrix.getM returning none on the other side.
fun n e ↦ encode (Semiterm.ofNat n e) is primitive recursive: the term half of
issue #506.
The instance sits on the Encodable instance already in Basic/Coding.lean, so nothing
downstream sees a new encode; the examples below check that, and that decode is still
ofNat.
Equations
- FFL.FirstOrder.Semiterm.primcodable = { toEncodable := FFL.FirstOrder.Semiterm.encodable, prim := ⋯ }
The rel/nrel argument fold, the term-decoding sibling of Semiterm.stepVec. Where the
term version reads each argument out of the strong-recursion table, this decodes each argument
code as a term of Semiterm L ξ n — the arguments of a relation are terms, not sub-formulas, so
they are in no table. 0 is failure and r + 1 success, as there.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The formula step function #
Semiformula.ofNat cannot use Primrec.nat_strong_rec: the ∀/∃ branches recurse at
ofNat (n + 1), so the arity changes as the recursion descends, while nat_strong_rec holds its
parameter fixed and tabulates one arity only. The recursion is therefore run by
Primrec.nat_omega_rec' over pairs (n, e), with e as the measure and subArgs naming the
immediate sub-formulas — two at the same arity for ⋏/⋎, one at the successor arity for
∀/∃, and none elsewhere. The measure obligation subArgs_ord is ofNat's own internal
< e + 1 bounds read back.
step is written with an if rather than a Nat.casesOn: a casesOn adds a level to the tower
of products the ambient argument lives in (((ℕ × ℕ) × List ℕ) × ℕ instead of
(ℕ × ℕ) × List ℕ), and elaboration of the Primrec combinators diverges on it, exactly as it
did on an Option-valued fold in the term half.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- FFL.FirstOrder.Semiformula.step n e vs = if e = 0 then 0 else FFL.FirstOrder.Semiformula.stepBody n (e - 1) vs
Instances For
fun n e ↦ encode (Semiformula.ofNat n e) is primitive recursive. With
Semiterm.encode_ofNat_primrec this closes issue #506: Primcodable instances for both
Semiterm L ξ n and Semiformula L ξ n, for every language satisfying the uniform-in-arity
condition Language.Primcodable.
As with the term instance, this sits on Semiformula.encodable rather than introducing a
second Encodable; the examples below check that, and that encode and decode are still
toNat and ofNat definitionally.
Equations
- FFL.FirstOrder.Semiformula.primcodable = { toEncodable := FFL.FirstOrder.Semiformula.encodable, prim := ⋯ }