Documentation

LeanPool.PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.CanonicalComposition

Supporting results for pointwise provable equality.

The canonical index of a composed partial-recursive program #

canonicalPartrecCompIndex f g is the Mathlib index of Nat.Partrec.Code.comp applied to the programs those two indices name. Its constructor number is 5 and its two subcodes are the given indices, which the three theorems below record. Each rests on the same closed form,

canonicalPartrecCompIndex f g = 2 * (2 * Nat.pair f g + 1) + 4,

proved once in canonicalPartrecCompIndex_eq.

The evaluation results then read those numbers off inside an arbitrary model of 𝐏𝐀⁻: a code whose graph holds at the canonical index has, at the same assignment, the graph of the constructor number at 5 and of the two subcodes at fCode and gCode.

source
def PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex (fCode gCode : ℕ) :
ℕ

The index of the composition of the programs named by fCode and gCode.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex_eq (fCode gCode : ℕ) :
    canonicalPartrecCompIndex fCode gCode = 2 * (2 * Nat.pair fCode gCode + 1) + 4

    The closed form of the canonical composition index.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex_outer_lt (fCode gCode : ℕ) :
    fCode < canonicalPartrecCompIndex fCode gCode

    The outer subindex is below the canonical composition index.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex_inner_lt (fCode gCode : ℕ) :
    gCode < canonicalPartrecCompIndex fCode gCode

    The inner subindex is below the canonical composition index.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.partrecCodePayload_canonicalPartrecCompIndex (fCode gCode : ℕ) :
    ArithmeticCode.partrecCodePayload (canonicalPartrecCompIndex fCode gCode) = Nat.pair fCode gCode

    The payload of the canonical composition index is the pair of subindices.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex_constructor_number (fCode gCode : ℕ) :
    ArithmeticCode.partrecCodeTag (canonicalPartrecCompIndex fCode gCode) = 5

    The canonical composition index has constructor number 5.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex_outer_index (fCode gCode : ℕ) :
    ArithmeticCode.partrecCodePayload₁ (canonicalPartrecCompIndex fCode gCode) = fCode

    The first subcode of the canonical composition index is the outer one.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex_inner_index (fCode gCode : ℕ) :
    ArithmeticCode.partrecCodePayload₂ (canonicalPartrecCompIndex fCode gCode) = gCode

    The second subcode of the canonical composition index is the inner one.

    Evaluation in an arbitrary model #

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.eval_codePartrecPayload_canonicalPartrecCompIndex {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (d : Nat.ArithPart₁.Code r) (fCode gCode : ℕ) (v : Fin r → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (↑(canonicalPartrecCompIndex fCode gCode) :> v)) (FFL.FirstOrder.Arithmetic.code d)) :
    (FFL.FirstOrder.Semiformula.Evalb (↑(Nat.pair fCode gCode) :> v)) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codePartrecPayload d))

    The payload of the canonical composition index, read inside a model.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.eval_codePartrecTag_canonicalPartrecCompIndex {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (d : Nat.ArithPart₁.Code r) (fCode gCode : ℕ) (v : Fin r → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (↑(canonicalPartrecCompIndex fCode gCode) :> v)) (FFL.FirstOrder.Arithmetic.code d)) :
    (FFL.FirstOrder.Semiformula.Evalb (5 :> v)) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codePartrecTag d))

    The constructor number of the canonical composition index, read inside a model: it is 5, the number of composition.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.eval_codePartrecPayload₁_canonicalPartrecCompIndex {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (d : Nat.ArithPart₁.Code r) (fCode gCode : ℕ) (v : Fin r → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (↑(canonicalPartrecCompIndex fCode gCode) :> v)) (FFL.FirstOrder.Arithmetic.code d)) :
    (FFL.FirstOrder.Semiformula.Evalb (↑fCode :> v)) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codePartrecPayload₁ d))

    The outer subcode of the canonical composition index, read inside a model.

    source
    theorem PointwiseComposition.CategoricalRiceShapiro.PartialRecursive.eval_codePartrecPayload₂_canonicalPartrecCompIndex {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (d : Nat.ArithPart₁.Code r) (fCode gCode : ℕ) (v : Fin r → M) (hd : (FFL.FirstOrder.Semiformula.Evalb (↑(canonicalPartrecCompIndex fCode gCode) :> v)) (FFL.FirstOrder.Arithmetic.code d)) :
    (FFL.FirstOrder.Semiformula.Evalb (↑gCode :> v)) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codePartrecPayload₂ d))

    The inner subcode of the canonical composition index, read inside a model.