Documentation

Mathlib.Computability.TMConfig

Modelling partial recursive functions using Turing machines #

The files TMConfig and TMToPartrec define a simplified basis for partial recursive functions, and a Turing.TM2 model Turing machine for evaluating these functions. This amounts to a constructive proof that every Partrec function can be evaluated by a Turing machine.

Main definitions #

A simplified basis for partrec #

This section constructs the type Code, which is a data type of programs with List ℕ input and output, with enough expressivity to write any partial recursive function. The primitives are:

This basis is convenient because it is closer to the Turing machine model - the key operations are splitting and merging of lists of unknown length, while the messy n-ary composition operation from the traditional basis for partial recursive functions is absent - but it retains a compositional semantics. The first step in transitioning to Turing machines is to make a sequential evaluator for this basis, which we take up in the next section.

source
inductive Turing.ToPartrec.Code :
Type

The type of codes for primitive recursive functions. Unlike Nat.Partrec.Code, this uses a set of operations on List ℕ. See Code.eval for a description of the behavior of the primitives.

Instances For
    source
    instance Turing.ToPartrec.instDecidableEqCode :
    DecidableEq Code
    Equations
    source
    def Turing.ToPartrec.instDecidableEqCode.decEq (x✝ x✝¹ : Code) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      instance Turing.ToPartrec.instInhabitedCode :
      Inhabited Code
      Equations
      source
      def Turing.ToPartrec.instInhabitedCode.default :
      Code
      Equations
      Instances For
        source
        def Turing.ToPartrec.Code.eval :
        Code → List ℕ →. List ℕ

        The semantics of the Code primitives, as partial functions List ℕ →. List ℕ. By convention we functions that return a single result return a singleton [n], or in some cases n :: v where v will be ignored by a subsequent function.

        • zero' appends a 0 to the input. That is, zero' v = 0 :: v.
        • succ returns the successor of the head of the input, defaulting to zero if there is no head:
        • tail returns the tail of the input
        • cons f fs calls f and fs on the input and conses the results:
        • comp f g calls f on the output of g:
          • comp f g v = f (g v)
        • case f g cases on the head of the input, calling f or g depending on whether it is zero or a successor (similar to Nat.casesOn).
          • case f g [] = f []
          • case f g (0 :: v) = f v
          • case f g (n+1 :: v) = g (n :: v)
        • fix f calls f repeatedly, using the head of the result of f to decide whether to call f again or finish:
          • fix f v = [] if f v = []
          • fix f v = w if f v = 0 :: w
          • fix f v = fix f w if f v = n+1 :: w (the exact value of n is discarded)
        Equations
        Instances For
          source
          @[simp]
          theorem Turing.ToPartrec.Code.zero'_eval :
          zero'.eval = fun (v : List ℕ) => pure (0 :: v)
          source
          @[simp]
          theorem Turing.ToPartrec.Code.succ_eval :
          succ.eval = fun (v : List ℕ) => pure [v.headI.succ]
          source
          @[simp]
          theorem Turing.ToPartrec.Code.tail_eval :
          tail.eval = fun (v : List ℕ) => pure v.tail
          source
          @[simp]
          theorem Turing.ToPartrec.Code.cons_eval (f fs : Code) :
          (f.cons fs).eval = fun (v : List ℕ) => do let n ← f.eval v let ns ← fs.eval v pure (n.headI :: ns)
          source
          @[simp]
          theorem Turing.ToPartrec.Code.comp_eval (f g : Code) :
          (f.comp g).eval = fun (v : List ℕ) => g.eval v >>= f.eval
          source
          @[simp]
          theorem Turing.ToPartrec.Code.case_eval (f g : Code) :
          (f.case g).eval = fun (v : List ℕ) => Nat.rec (f.eval v.tail) (fun (y : ℕ) (x : Part (List ℕ)) => g.eval (y :: v.tail)) v.headI
          source
          @[simp]
          theorem Turing.ToPartrec.Code.fix_eval (f : Code) :
          f.fix.eval = PFun.fix fun (v : List ℕ) => Part.map (fun (v : List ℕ) => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
          source
          def Turing.ToPartrec.Code.nil :
          Code

          nil is the constant nil function: nil v = [].

          Equations
          Instances For
            source
            @[simp]
            theorem Turing.ToPartrec.Code.nil_eval (v : List ℕ) :
            nil.eval v = pure []
            source
            def Turing.ToPartrec.Code.id :
            Code

            id is the identity function: id v = v.

            Equations
            Instances For
              source
              @[simp]
              theorem Turing.ToPartrec.Code.id_eval (v : List ℕ) :
              id.eval v = pure v
              source
              def Turing.ToPartrec.Code.head :
              Code

              head gets the head of the input list: head [] = [0], head (n :: v) = [n].

              Equations
              Instances For
                source
                @[simp]
                theorem Turing.ToPartrec.Code.head_eval (v : List ℕ) :
                head.eval v = pure [v.headI]
                source
                def Turing.ToPartrec.Code.zero :
                Code

                zero is the constant zero function: zero v = [0].

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Turing.ToPartrec.Code.zero_eval (v : List ℕ) :
                  zero.eval v = pure [0]
                  source
                  def Turing.ToPartrec.Code.pred :
                  Code

                  pred returns the predecessor of the head of the input: pred [] = [0], pred (0 :: v) = [0], pred (n+1 :: v) = [n].

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Turing.ToPartrec.Code.pred_eval (v : List ℕ) :
                    pred.eval v = pure [v.headI.pred]
                    source
                    def Turing.ToPartrec.Code.rfind (f : Code) :
                    Code

                    rfind f performs the function of the rfind primitive of partial recursive functions. rfind f v returns the smallest n such that (f (n :: v)).head = 0.

                    It is implemented as:

                    rfind f v = pred (fix (fun (n::v) => f (n::v) :: n+1 :: v) (0 :: v))

                    The idea is that the initial state is 0 :: v, and the fix keeps n :: v as its internal state; it calls f (n :: v) as the exit test and n+1 :: v as the next state. At the end we get n+1 :: v where n is the desired output, and pred (n+1 :: v) = [n] returns the result.

                    Equations
                    Instances For
                      source
                      def Turing.ToPartrec.Code.prec (f g : Code) :
                      Code

                      prec f g implements the prec (primitive recursion) operation of partial recursive functions. prec f g evaluates as:

                      • prec f g [] = [f []]
                      • prec f g (0 :: v) = [f v]
                      • prec f g (n+1 :: v) = [g (n :: prec f g (n :: v) :: v)]

                      It is implemented as:

                      G (a :: b :: IH :: v) = (b :: a+1 :: b-1 :: g (a :: IH :: v) :: v)
F (0 :: f_v :: v) = (f_v :: v)
F (n+1 :: f_v :: v) = (fix G (0 :: n :: f_v :: v)).tail.tail
prec f g (a :: v) = [(F (a :: f v :: v)).head]

                      Because fix always evaluates its body at least once, we must special case the 0 case to avoid calling g more times than necessary (which could be bad if g diverges). If the input is 0 :: v, then F (0 :: f v :: v) = (f v :: v) so we return [f v]. If the input is n+1 :: v, we evaluate the function from the bottom up, with initial state 0 :: n :: f v :: v. The first number counts up, providing arguments for the applications to g, while the second number counts down, providing the exit condition (this is the initial b in the return value of G, which is stripped by fix). After the fix is complete, the final state is n :: 0 :: res :: v where res is the desired result, and the rest reduces this to [res].

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem Turing.ToPartrec.Code.exists_code.comp {m n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : Fin n → List.Vector ℕ m →. ℕ} (hf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v) (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) :
                        ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((List.Vector.mOfFn fun (i : Fin n) => g i v) >>= f)
                        source
                        theorem Turing.ToPartrec.Code.exists_code {n : ℕ} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) :
                        ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v

                        From compositional semantics to sequential semantics #

                        Our initial sequential model is designed to be as similar as possible to the compositional semantics in terms of its primitives, but it is a sequential semantics, meaning that rather than defining an eval c : List ℕ →. List ℕ function for each program, defined by recursion on programs, we have a type Cfg with a step function step : Cfg → Option cfg that provides a deterministic evaluation order. In order to do this, we introduce the notion of a continuation, which can be viewed as a Code with a hole in it where evaluation is currently taking place. Continuations can be assigned a List ℕ →. List ℕ semantics as well, with the interpretation being that given a List ℕ result returned from the code in the hole, the remainder of the program will evaluate to a List ℕ final value.

                        The continuations are:

                        The type Cfg of evaluation states is:

                        The main theorem of this section is that for each code c, the state stepNormal c halt v steps to v' in finitely many steps if and only if Code.eval c v = some v'.

                        source
                        inductive Turing.ToPartrec.Cont :
                        Type

                        The type of continuations, built up during evaluation of a Code expression.

                        Instances For
                          source
                          instance Turing.ToPartrec.instInhabitedCont :
                          Inhabited Cont
                          Equations
                          source
                          def Turing.ToPartrec.instInhabitedCont.default :
                          Cont
                          Equations
                          Instances For
                            source
                            def Turing.ToPartrec.Cont.eval :
                            Cont → List ℕ →. List ℕ

                            The semantics of a continuation.

                            Equations
                            Instances For
                              source
                              inductive Turing.ToPartrec.Cfg :
                              Type

                              The set of configurations of the machine:

                              • halt v: The machine is about to stop and v : List ℕ is the result.
                              • ret k v: The machine is about to pass v : List ℕ to continuation k : Cont.

                              We don't have a state corresponding to normal evaluation because these are evaluated immediately to a ret "in zero steps" using the stepNormal function.

                              Instances For
                                source
                                instance Turing.ToPartrec.instInhabitedCfg :
                                Inhabited Cfg
                                Equations
                                source
                                def Turing.ToPartrec.instInhabitedCfg.default :
                                Cfg
                                Equations
                                Instances For
                                  source
                                  def Turing.ToPartrec.stepNormal :
                                  Code → Cont → List ℕ → Cfg

                                  Evaluating c : Code in a continuation k : Cont and input v : List ℕ. This goes by recursion on c, building an augmented continuation and a value to pass to it.

                                  • zero' v = 0 :: v evaluates immediately, so we return it to the parent continuation
                                  • succ v = [v.headI.succ] evaluates immediately, so we return it to the parent continuation
                                  • tail v = v.tail evaluates immediately, so we return it to the parent continuation
                                  • cons f fs v = (f v).headI :: fs v requires two sub-evaluations, so we evaluate f v in the continuation k (_.headI :: fs v) (called Cont.cons₁ fs v k)
                                  • comp f g v = f (g v) requires two sub-evaluations, so we evaluate g v in the continuation k (f _) (called Cont.comp f k)
                                  • case f g v = v.head.casesOn (f v.tail) (fun n => g (n :: v.tail)) has the information needed to evaluate the case statement, so we do that and transition to either f v or g (n :: v.tail).
                                  • fix f v = let v' := f v; if v'.headI = 0 then k v'.tail else fix f v'.tail needs to first evaluate f v, so we do that and leave the rest for the continuation (called Cont.fix f k)
                                  Equations
                                  Instances For
                                    source
                                    def Turing.ToPartrec.stepRet :
                                    Cont → List ℕ → Cfg

                                    Evaluating a continuation k : Cont on input v : List ℕ. This is the second part of evaluation, when we receive results from continuations built by stepNormal.

                                    • Cont.halt v = v, so we are done and transition to the Cfg.halt v state
                                    • Cont.cons₁ fs as k v = k (v.headI :: fs as), so we evaluate fs as now with the continuation k (v.headI :: _) (called cons₂ v k).
                                    • Cont.cons₂ ns k v = k (ns.headI :: v), where we now have everything we need to evaluate ns.headI :: v, so we return it to k.
                                    • Cont.comp f k v = k (f v), so we call f v with k as the continuation.
                                    • Cont.fix f k v = k (if v.headI = 0 then k v.tail else fix f v.tail), where v is a value, so we evaluate the if statement and either call k with v.tail, or call fix f v with k as the continuation (which immediately calls f with Cont.fix f k as the continuation).
                                    Equations
                                    Instances For
                                      source
                                      def Turing.ToPartrec.step :
                                      Cfg → Option Cfg

                                      If we are not done (in Cfg.halt state), then we must be still stuck on a continuation, so this main loop calls stepRet with the new continuation. The overall step function transitions from one Cfg to another, only halting at the Cfg.halt state.

                                      Equations
                                      Instances For
                                        source
                                        def Turing.ToPartrec.Cont.then :
                                        Cont → Cont → Cont

                                        In order to extract a compositional semantics from the sequential execution behavior of configurations, we observe that continuations have a monoid structure, with Cont.halt as the unit and Cont.then as the multiplication. Cont.then k₁ k₂ runs k₁ until it halts, and then takes the result of k₁ and passes it to k₂.

                                        We will not prove it is associative (although it is), but we are instead interested in the associativity law k₂ (eval c k₁) = eval c (k₁.then k₂). This holds at both the sequential and compositional levels, and allows us to express running a machine without the ambient continuation and relate it to the original machine's evaluation steps. In the literature this is usually where one uses Turing machines embedded inside other Turing machines, but this approach allows us to avoid changing the ambient type Cfg in the middle of the recursion.

                                        Equations
                                        Instances For
                                          source
                                          theorem Turing.ToPartrec.Cont.then_eval {k k' : Cont} {v : List ℕ} :
                                          (k.then k').eval v = k.eval v >>= k'.eval
                                          source
                                          def Turing.ToPartrec.Cfg.then :
                                          Cfg → Cont → Cfg

                                          The then k function is a "configuration homomorphism". Its operation on states is to append k to the continuation of a Cfg.ret state, and to run k on v if we are in the Cfg.halt v state.

                                          Equations
                                          Instances For
                                            source
                                            theorem Turing.ToPartrec.stepNormal_then (c : Code) (k k' : Cont) (v : List ℕ) :
                                            stepNormal c (k.then k') v = (stepNormal c k v).then k'

                                            The stepNormal function respects the then k' homomorphism. Note that this is an exact equality, not a simulation; the original and embedded machines move in lock-step until the embedded machine reaches the halt state.

                                            source
                                            theorem Turing.ToPartrec.stepRet_then {k k' : Cont} {v : List ℕ} :
                                            stepRet (k.then k') v = (stepRet k v).then k'

                                            The stepRet function respects the then k' homomorphism. Note that this is an exact equality, not a simulation; the original and embedded machines move in lock-step until the embedded machine reaches the halt state.

                                            source
                                            def Turing.ToPartrec.Code.Ok (c : Code) :
                                            Prop

                                            This is a temporary definition, because we will prove in code_is_ok that it always holds. It asserts that c is semantically correct; that is, for any k and v, eval (stepNormal c k v) = eval (Cfg.ret k (Code.eval c v)), as an equality of partial values (so one diverges iff the other does).

                                            In particular, we can let k = Cont.halt, and then this asserts that stepNormal c Cont.halt v evaluates to Cfg.halt (Code.eval c v).

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              theorem Turing.ToPartrec.Code.Ok.zero {c : Code} (h : c.Ok) {v : List ℕ} :
                                              Turing.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v
                                              source
                                              theorem Turing.ToPartrec.stepNormal.is_ret (c : Code) (k : Cont) (v : List ℕ) :
                                              ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
                                              source
                                              theorem Turing.ToPartrec.cont_eval_fix {f : Code} {k : Cont} {v : List ℕ} (fok : f.Ok) :
                                              eval step (stepNormal f (Cont.fix f k) v) = do let v ← f.fix.eval v eval step (Cfg.ret k v)
                                              source
                                              theorem Turing.ToPartrec.code_is_ok (c : Code) :
                                              c.Ok
                                              source
                                              theorem Turing.ToPartrec.stepNormal_eval (c : Code) (v : List ℕ) :
                                              eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v
                                              source
                                              theorem Turing.ToPartrec.stepRet_eval {k : Cont} {v : List ℕ} :
                                              eval step (stepRet k v) = Cfg.halt <$> k.eval v