Documentation

LeanPool.PointwiseComposition.FailureOfComposition.BoundedSemidecision

Supporting results for pointwise provable equality.

Sequential bounded universal semidecision in arbitrary models of PA. Each body call must return zero. A primitive-recursion program combines these calls, and PA induction proves its graph equation also at nonstandard bounds.

source
def PointwiseComposition.FailureOfComposition.BoundedSemidecision.zeroOnlyProgram :
Nat.Partrec.Code

Return zero precisely on input zero; diverge on every other input.

Equations
Instances For
    source
    def PointwiseComposition.FailureOfComposition.BoundedSemidecision.acceptZeroProgram (c : Nat.Partrec.Code) :
    Nat.Partrec.Code

    Run a program and accept precisely its zero output.

    Equations
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.BoundedSemidecision.boundedStepProgram (c : Nat.Partrec.Code) :
      Nat.Partrec.Code

      The recursion step supplies pair candidate environment to the body.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def PointwiseComposition.FailureOfComposition.BoundedSemidecision.boundedAllProgram (c : Nat.Partrec.Code) :
        Nat.Partrec.Code

        Check every candidate below the bound, with input pair environment bound.

        Equations
        Instances For
          source
          @[simp]
          theorem PointwiseComposition.FailureOfComposition.BoundedSemidecision.computes_zeroOnly {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (x y : M) :
          ProgramGraph.Computes zeroOnlyProgram x y ↔ x = 0 ∧ y = 0
          source
          @[simp]
          theorem PointwiseComposition.FailureOfComposition.BoundedSemidecision.computes_acceptZero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : Nat.Partrec.Code) (x y : M) :
          ProgramGraph.Computes (acceptZeroProgram c) x y ↔ y = 0 ∧ ProgramGraph.Computes c x 0
          source
          @[simp]
          theorem PointwiseComposition.FailureOfComposition.BoundedSemidecision.computes_boundedStep {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : Nat.Partrec.Code) (a k z y : M) :
          ProgramGraph.Computes (boundedStepProgram c) ⟪a, ⟪k, z⟫⟫ y ↔ y = 0 ∧ ProgramGraph.Computes c ⟪k, a⟫ 0
          source
          theorem PointwiseComposition.FailureOfComposition.BoundedSemidecision.computes_boundedAll {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : Nat.Partrec.Code) (a b y : M) :
          ProgramGraph.Computes (boundedAllProgram c) ⟪a, b⟫ y ↔ y = 0 ∧ ∀ k < b, ProgramGraph.Computes c ⟪k, a⟫ 0

          The complete graph equation for bounded universal semidecision. No termination or zero-output assumption on the body program is required.