Documentation

Cslib.Languages.CombinatoryLogic.PartrecToSKI

Partial Recursive → SKI-computable (Nat.Partrec) #

This file translates Nat.Partrec.Code to SKI terms and proves the translation correct, showing that every partial recursive function is SKI-computable in the sense of SKI.Computes (from Cslib.Languages.CombinatoryLogic.Computable).

Main definitions #

Main results #

Helper terms for Code.prec and Code.rfind' #

source
def Cslib.SKI.PrecStepPoly (tg : SKI) :
SKI.Polynomial 3

Step function for primitive recursion: λ a cn prev. tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev)) Variables: &0 = a, &1 = cn, &2 = prev

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Cslib.SKI.PrecStep (tg : SKI) :
    SKI

    SKI term for the primitive recursion step function.

    Equations
    Instances For
      source
      theorem Cslib.SKI.precStep_def (tg a cn prev : SKI) :
      Relation.ReflTransGen Red (((tg.PrecStep.app a).app cn).app prev) (tg.app ((NatPair.app a).app ((NatPair.app (Pred.app cn)).app prev)))
      source
      def Cslib.SKI.PrecTransPoly (tf tg : SKI) :
      SKI.Polynomial 1

      Full primitive recursion translation: λ n. Rec (tf (left n)) (PrecStep tg (left n)) (right n)

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cslib.SKI.PrecTrans (tf tg : SKI) :
        SKI

        SKI term for primitive recursion via Rec with pair/unpair plumbing.

        Equations
        Instances For
          source
          theorem Cslib.SKI.precTrans_def (tf tg cn : SKI) :
          Relation.ReflTransGen Red ((tf.PrecTrans tg).app cn) (((Rec.app (tf.app (NatUnpairLeft.app cn))).app (tg.PrecStep.app (NatUnpairLeft.app cn))).app (NatUnpairRight.app cn))
          source
          def Cslib.SKI.RFindTransPoly (tf : SKI) :
          SKI.Polynomial 1

          Unbounded search translation: λ n. RFindAbove ⬝ (NatUnpairRight ⬝ n) ⬝ (B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ n)))

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cslib.SKI.RFindTrans (tf : SKI) :
            SKI

            SKI term for unbounded search (μ-recursion).

            Equations
            Instances For
              source
              theorem Cslib.SKI.rfindTrans_def (tf cn : SKI) :
              Relation.ReflTransGen Red (tf.RFindTrans.app cn) ((RFindAbove.app (NatUnpairRight.app cn)).app ((B.app tf).app (NatPair.app (NatUnpairLeft.app cn))))

              Translation from Nat.Partrec.Code to SKI #

              source
              def Nat.Partrec.Code.toSKI :
              Code → Cslib.SKI

              Translate Nat.Partrec.Code to SKI terms operating on Church numerals.

              Equations
              Instances For

                Correctness proofs #

                source
                theorem Nat.Partrec.Code.toSKI_correct (c : Code) :
                c.toSKI.Computes c.eval

                Main correctness theorem: Code.toSKI correctly computes Code.eval.

                Main result #

                source
                theorem Cslib.SKI.natPartrec_skiComputable (f : ℕ →. ℕ) (hf : Nat.Partrec f) :
                Computable f

                Every partial recursive function on ℕ is SKI-computable.