Supporting results for pointwise provable equality.
Structural bridges for the primitive-recursion constructor #
Constructor number 6 is primitive recursion. This file supplies structural
infrastructure for it, in two parts.
The first part, in CategoricalRiceShapiro.PartialRecursive, defines
canonicalPartrecPrecIndex fCode gCode, the canonical index of the primitive
recursion whose base program is named by fCode and whose step program is named
by gCode. It proves the decoder and ranking facts for that index: its closed
form 2 * (2 * Nat.pair fCode gCode) + 1 + 4, its constructor number 6, its
payload Nat.pair fCode gCode with components fCode and gCode, and the strict
bounds fCode < canonicalPartrecPrecIndex fCode gCode and
gCode < canonicalPartrecPrecIndex fCode gCode. It also proves the
corresponding readings of the payload, the constructor number and the two
components inside a model of 𝐏𝐀⁻.
The second part, in CategoricalRiceShapiro.Evaluator, proves the zero and
successor success equivalences for the primitive-recursion evaluator cell
codePrecEvaluatorCell, over 𝐏𝐀 and 𝐈𝐎𝐩𝐞𝐧. For a zero recursion argument,
when the argument evaluates to ⟪z, 0⟫, the cell succeeds with y + 1 exactly
when the base lookup does. For a successor recursion argument, when the argument
evaluates to ⟪z, a + 1⟫, the cell succeeds with y + 1 exactly when, for one
intermediate value x, the lookup of the same index at the previous fuel on
⟪z, a⟫ succeeds with x + 1 and the step-program lookup at the current fuel on
⟪z, ⟪a, x⟫⟫ succeeds with y + 1.
The first part also proves, for an arbitrary natural number q with
constructor number 6, that q is the canonical primitive-recursion index of
its decoded payload components, q = canonicalPartrecPrecIndex (partrecCodePayload₁ q) (partrecCodePayload₂ q), and that both decoded payloads
are strictly smaller than q.
eval_prec_predecessor_lookup_succ_iff_codeHistoryEvaluator identifies the
same-index lookup of the successor equivalence, in the history before the cell
at k + 1, q and at input ⟪z, a + 1⟫, with a successful codeHistoryEvaluator
evaluation at stage k on ⟪z, a⟫, through
eval_predecessor_lookup_succ_iff_codeHistoryEvaluator.
This is structural infrastructure. The file proves neither tag-6 persistence of the evaluator certificate nor persistence for every standard index.
The index of the primitive recursion whose base program is named by fCode
and whose step program is named by gCode.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The closed form of the canonical primitive-recursion index.
The base subindex is below the canonical primitive-recursion index.
The step subindex is below the canonical primitive-recursion index.
The payload of the canonical primitive-recursion index is the pair of the base and step subindices.
The canonical primitive-recursion index has constructor number 6.
bodd.toNat and % 2 are related by Nat.mod_two_of_bodd.
The first subcode of the canonical primitive-recursion index is the base program.
The second subcode of the canonical primitive-recursion index is the step program.
A natural number q of constructor number 6 is the canonical
primitive-recursion index of its two payload components.
Both payload components of a natural number q of constructor number 6
are strictly smaller than q.
Evaluation in an arbitrary model #
The payload of the canonical primitive-recursion index, read inside a model.
The constructor number of the canonical primitive-recursion index, read
inside a model: it is 6, the number of primitive recursion.
The base subcode of the canonical primitive-recursion index, read inside a model.
The step subcode of the canonical primitive-recursion index, read inside a model.
Part B: success semantics of the primitive-recursion cell #
Zero recursion argument. When the argument code dn evaluates to
⟪z, 0⟫, the primitive-recursion cell succeeds with output y + 1 exactly when
the base lookup succeeds with output y + 1: the table at fuel k' + 1, the
base program dcf, and input z.
Successor recursion argument. When the argument code dn evaluates to
⟪z, a + 1⟫, the primitive-recursion cell succeeds with output y + 1 exactly
when, for one intermediate value x, the predecessor lookup of the same index
dq at fuel k' on ⟪z, a⟫ succeeds with output x + 1, and the step lookup
of dcg at fuel k' + 1 on ⟪z, ⟪a, x⟫⟫ succeeds with output y + 1.
The same-index lookup of the successor branch #
The same-index lookup of the primitive-recursion successor branch. With
the input pair z (a + 1), the predecessor lookup of
eval_codePrecEvaluatorCell_succ_iff_of_succ, at the dispatcher's decremented
stage and program index and at the input pair z a, succeeds with output
x + 1 exactly when codeHistoryEvaluator succeeds at x + 1, k, q, pair z a.