Documentation

LeanPool.DomainTheory.Neighborhood.Theorem56Full

Theorem 5.6 (Scott 1981, PRG-19, ยง5) โ€” the FULL closure: partial recursive โŸน #

ฮป-definable

Theorem56.lean builds the constructive heart (strict starting functions, the primitive-recursion and ฮผ combinators with their scheme equations). This file wires those pieces together against Mathlib's arity-aware inductive predicates Nat.Primrec'/Nat.Partrec' (over List.Vector โ„• n), whose constructors are exactly Scott's generation grammar:

We prove: every Nat.Primrec'/Nat.Partrec' function is denoted by an approximable map ฯ† : ๐’ฉ โ†’ N, where ๐’ฉ := N^โˆž (Exercise 3.16) is the universal argument domain โ€” a k-ary function is realised by a single map that depends only on coordinates 0..k-1. The realisation is very strict (Scott): โŠฅ in any relevant coordinate forces โŠฅ, which is what makes composition and minimisation compose. The capstone is partrec_lamDef and the 1-ary corollary partrec_one.

source
@[reducible, inline]
abbrev Domain.Neighborhood.Theorem56Full.๐’ฉ :
NeighborhoodSystem (โ„• ร— โ„•)

The universal argument domain ๐’ฉ = N^โˆž (Exercise 3.16). All k-ary number functions are realised as approximable maps ๐’ฉ โ†’ N depending only on coordinates 0..k-1.

Equations
Instances For
    source
    theorem Domain.Neighborhood.Theorem56Full.T_bot_eq :
    Example43.T.bot = Example23.botElt

    T.bot = Example23.botElt (both least); bridges zeroMap_bot (lands in T.bot) with cond_bot (phrased with Example23.botElt).

    Element builders. #

    source
    def Domain.Neighborhood.Theorem56Full.optElem :
    Option โ„• โ†’ Example43.N.Element

    none โ†ฆ โŠฅ, some n โ†ฆ nฬ‚.

    Equations
    Instances For
      source
      def Domain.Neighborhood.Theorem56Full.argElem {n : โ„•} (a : Fin n โ†’ Option โ„•) :
      ๐’ฉ.Element

      The argument element of ๐’ฉ whose first n coordinates are optElem (a i) and the rest โŠฅ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Domain.Neighborhood.Theorem56Full.vecElem {n : โ„•} (v : List.Vector โ„• n) :
        ๐’ฉ.Element

        The argument element of ๐’ฉ carrying a List.Vector โ„• n in its first n coordinates.

        Equations
        Instances For
          source
          @[simp]
          theorem Domain.Neighborhood.Theorem56Full.component_argElem {n : โ„•} (a : Fin n โ†’ Option โ„•) (i : โ„•) :
          component (argElem a) i = if h : i < n then optElem (a โŸจi, hโŸฉ) else Example43.N.bot
          source
          @[simp]
          theorem Domain.Neighborhood.Theorem56Full.component_vecElem {n : โ„•} (v : List.Vector โ„• n) (i : โ„•) :
          component (vecElem v) i = if h : i < n then Example43.natElem (v.get โŸจi, hโŸฉ) else Example43.N.bot
          source
          theorem Domain.Neighborhood.Theorem56Full.eq_of_component_eq {z z' : ๐’ฉ.Element} (h : โˆ€ (n : โ„•), component z n = component z' n) :
          z = z'

          Two ๐’ฉ-elements are equal iff all components agree.

          source
          def Domain.Neighborhood.Theorem56Full.ArgLike (z : ๐’ฉ.Element) :
          Prop

          A ๐’ฉ-element is arg-like if every coordinate is total or โŠฅ (true of all argElem).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Domain.Neighborhood.Theorem56Full.argElem_argLike {n : โ„•} (a : Fin n โ†’ Option โ„•) :
            ArgLike (argElem a)

            Components through push. #

            source
            theorem Domain.Neighborhood.Theorem56Full.component_push_zero (x : Example43.N.Element) (s : ๐’ฉ.Element) :
            component ((Exercise511.push Example43.N).toElementMap (pair x s)) 0 = x
            source
            theorem Domain.Neighborhood.Theorem56Full.component_push_succ (x : Example43.N.Element) (s : ๐’ฉ.Element) (j : โ„•) :
            component ((Exercise511.push Example43.N).toElementMap (pair x s)) (j + 1) = component s j

            The strictifier guard1/strictGuardN (Scott's cond(zero(x),ยท,ยท) #

            device).

            guard1 j ฯ† z = cond(zero(zโฑผ), ฯ† z, ฯ† z): equals ฯ† z when zโฑผ is total, โŠฅ when zโฑผ = โŠฅ. Composing the guards for j = 0..n-1 makes a map very strict in its first n coordinates.

            source
            def Domain.Neighborhood.Theorem56Full.guard1 (j : โ„•) (ฯ† : ApproximableMap ๐’ฉ Example43.N) :
            ApproximableMap ๐’ฉ Example43.N

            Test coordinate j: cond(zero(zโฑผ), ฯ† z, ฯ† z).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Domain.Neighborhood.Theorem56Full.guard1_apply (j : โ„•) (ฯ† : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) :
              (guard1 j ฯ†).toElementMap z = (Exercise326.cond Example43.N).toElementMap (pair (Example43.zeroMap.toElementMap (component z j)) (pair (ฯ†.toElementMap z) (ฯ†.toElementMap z)))
              source
              theorem Domain.Neighborhood.Theorem56Full.guard1_total (j : โ„•) (ฯ† : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) {k : โ„•} (h : component z j = Example43.natElem k) :
              (guard1 j ฯ†).toElementMap z = ฯ†.toElementMap z
              source
              theorem Domain.Neighborhood.Theorem56Full.guard1_bot (j : โ„•) (ฯ† : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) (h : component z j = Example43.N.bot) :
              (guard1 j ฯ†).toElementMap z = Example43.N.bot
              source
              theorem Domain.Neighborhood.Theorem56Full.guard1_inner_bot (j : โ„•) (ฯ† : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) (hz : component z j = Example43.N.bot โˆจ โˆƒ (k : โ„•), component z j = Example43.natElem k) (h : ฯ†.toElementMap z = Example43.N.bot) :
              (guard1 j ฯ†).toElementMap z = Example43.N.bot

              If ฯ† z = โŠฅ and zโฑผ is total-or-โŠฅ, the guard stays โŠฅ.

              source
              def Domain.Neighborhood.Theorem56Full.strictGuardN :
              โ„• โ†’ ApproximableMap ๐’ฉ Example43.N โ†’ ApproximableMap ๐’ฉ Example43.N

              Test coordinates 0..n-1.

              Equations
              Instances For
                source
                theorem Domain.Neighborhood.Theorem56Full.strictGuardN_total (n : โ„•) (ฯ† : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) (h : โˆ€ j < n, โˆƒ (k : โ„•), component z j = Example43.natElem k) :
                (strictGuardN n ฯ†).toElementMap z = ฯ†.toElementMap z

                On arguments whose first n coordinates are all total, the guard is transparent.

                source
                theorem Domain.Neighborhood.Theorem56Full.strictGuardN_strict (n : โ„•) (ฯ† : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) (hz : ArgLike z) {i : โ„•} (hi : i < n) (hb : component z i = Example43.N.bot) :
                (strictGuardN n ฯ†).toElementMap z = Example43.N.bot

                If some coordinate i < n is โŠฅ (and z is arg-like), the guard forces โŠฅ.

                tupleMap: assemble n scalar maps into the first n coordinates of #

                ๐’ฉ.

                source
                def Domain.Neighborhood.Theorem56Full.tupleMap (n : โ„•) :
                (Fin n โ†’ ApproximableMap ๐’ฉ Example43.N) โ†’ ApproximableMap ๐’ฉ ๐’ฉ

                โŸจgโ‚€, โ€ฆ, g_{n-1}โŸฉ : ๐’ฉ โ†’ ๐’ฉ placing gแตข at coordinate i (< n) and โŠฅ beyond.

                Equations
                Instances For
                  source
                  theorem Domain.Neighborhood.Theorem56Full.tupleMap_succ (n : โ„•) (gs : Fin (n + 1) โ†’ ApproximableMap ๐’ฉ Example43.N) :
                  tupleMap (n + 1) gs = (Exercise511.push Example43.N).comp (paired (gs 0) (tupleMap n fun (i : Fin n) => gs i.succ))
                  source
                  theorem Domain.Neighborhood.Theorem56Full.component_tupleMap (n : โ„•) (gs : Fin n โ†’ ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) (i : โ„•) (hi : i < n) :
                  component ((tupleMap n gs).toElementMap z) i = (gs โŸจi, hiโŸฉ).toElementMap z

                  Coordinate i < n of the tuple is exactly gแตข.

                  The ฮป-definability specification. #

                  source
                  structure Domain.Neighborhood.Theorem56Full.LamDef {n : โ„•} (ฯ† : ApproximableMap ๐’ฉ Example43.N) (f : List.Vector โ„• n โ†’. โ„•) :
                  Prop

                  ฯ† : ๐’ฉ โ†’ N realises the n-ary partial function f (a very strict ฮป-definition): ฯ† returns f's value on total arguments, โŠฅ where f is undefined, and โŠฅ on any arg-like input with a โŠฅ among its first n coordinates.

                  Instances For
                    source
                    theorem Domain.Neighborhood.Theorem56Full.component_vecElem_lt {n : โ„•} (v : List.Vector โ„• n) {j : โ„•} (hj : j < n) :
                    component (vecElem v) j = Example43.natElem (v.get โŸจj, hjโŸฉ)

                    Every coordinate j < n of vecElem v is the total v.get j.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.vecElem_totals {n : โ„•} (v : List.Vector โ„• n) (j : โ„•) :
                    j < n โ†’ โˆƒ (k : โ„•), component (vecElem v) j = Example43.natElem k

                    vecElem v has total coordinates throughout its arity.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.component_argElem_none {n : โ„•} (a : Fin n โ†’ Option โ„•) (i : Fin n) (hi : a i = none) :
                    component (argElem a) โ†‘i = Example43.N.bot

                    A coordinate that an argElem sets to none is โŠฅ.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_of_inner {n : โ„•} (inner : ApproximableMap ๐’ฉ Example43.N) (f : List.Vector โ„• n โ†’. โ„•) (hdef : โˆ€ (v : List.Vector โ„• n), โˆ€ c โˆˆ f v, inner.toElementMap (vecElem v) = Example43.natElem c) (hundef : โˆ€ (v : List.Vector โ„• n), ยฌ(f v).Dom โ†’ inner.toElementMap (vecElem v) = Example43.N.bot) :
                    LamDef (strictGuardN n inner) f

                    Master constructor. Wrapping an inner map (correct on total arguments) in strictGuardN n yields a full, very strict ฮป-definition. The strict clause is then automatic.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_total {n : โ„•} (ฯˆ : ApproximableMap ๐’ฉ Example43.N) (g : List.Vector โ„• n โ†’ โ„•) (hval : โˆ€ (v : List.Vector โ„• n), ฯˆ.toElementMap (vecElem v) = Example43.natElem (g v)) :
                    LamDef (strictGuardN n ฯˆ) โ†‘g

                    The total-function specialisation of lamDef_of_inner.

                    Primitive recursive base cases: zero, succ, get. #

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_zero :
                    LamDef (strictGuardN 0 (constMap ๐’ฉ (Example43.natElem 0))) โ†‘fun (x : List.Vector โ„• 0) => 0

                    zero : Vector โ„• 0 โ†’ โ„•, the constant 0 (nullary).

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_succ :
                    LamDef (strictGuardN 1 (Example43.succMap.comp (projN Example43.N 0))) โ†‘fun (v : List.Vector โ„• 1) => v.head.succ

                    succ : Vector โ„• 1 โ†’ โ„•, v โ†ฆ v.head + 1.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_get {n : โ„•} (i : Fin n) :
                    LamDef (strictGuardN n (projN Example43.N โ†‘i)) โ†‘fun (v : List.Vector โ„• n) => v.get i

                    get i : Vector โ„• n โ†’ โ„•, the i-th projection.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_congr {n : โ„•} {ฯ† : ApproximableMap ๐’ฉ Example43.N} {f f' : List.Vector โ„• n โ†’. โ„•} (h : โˆ€ (v : List.Vector โ„• n), f v = f' v) (hf : LamDef ฯ† f) :
                    LamDef ฯ† f'

                    Transport a ฮป-definition along pointwise equality of the realised function.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.realizer_value {n : โ„•} {ฯ† : ApproximableMap ๐’ฉ Example43.N} {f : List.Vector โ„• n โ†’. โ„•} (h : LamDef ฯ† f) (v : List.Vector โ„• n) :
                    ฯ†.toElementMap (vecElem v) = Example43.N.bot โˆจ โˆƒ (k : โ„•), ฯ†.toElementMap (vecElem v) = Example43.natElem k

                    The value a realiser takes on a total argument is total-or-โŠฅ (arg-like).

                    Composition. #

                    source
                    theorem Domain.Neighborhood.Theorem56Full.component_bot (i : โ„•) :
                    component ๐’ฉ.bot i = Example43.N.bot

                    Coordinates of the bottom stack are โŠฅ.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.tupleMap_zero (gs : Fin 0 โ†’ ApproximableMap ๐’ฉ Example43.N) :
                    tupleMap 0 gs = constMap ๐’ฉ ๐’ฉ.bot
                    source
                    theorem Domain.Neighborhood.Theorem56Full.component_tupleMap_ge (n : โ„•) (gs : Fin n โ†’ ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) (i : โ„•) :
                    n โ‰ค i โ†’ component ((tupleMap n gs).toElementMap z) i = Example43.N.bot

                    Coordinates โ‰ฅ n of the tuple are โŠฅ.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.tupleMap_vecElem_eq {m nn : โ„•} (ฯ†g : Fin nn โ†’ ApproximableMap ๐’ฉ Example43.N) (g : Fin nn โ†’ List.Vector โ„• m โ†’. โ„•) (hg : โˆ€ (i : Fin nn), LamDef (ฯ†g i) (g i)) (v : List.Vector โ„• m) (w : List.Vector โ„• nn) (hw : โˆ€ (i : Fin nn), w.get i โˆˆ g i v) :
                    (tupleMap nn ฯ†g).toElementMap (vecElem v) = vecElem w

                    The tuple of realisers, applied to a total argument, equals vecElem w where wแตข = gแตข(v).

                    source
                    theorem Domain.Neighborhood.Theorem56Full.tupleMap_argLike {m nn : โ„•} (ฯ†g : Fin nn โ†’ ApproximableMap ๐’ฉ Example43.N) (g : Fin nn โ†’ List.Vector โ„• m โ†’. โ„•) (hg : โˆ€ (i : Fin nn), LamDef (ฯ†g i) (g i)) (v : List.Vector โ„• m) :
                    ArgLike ((tupleMap nn ฯ†g).toElementMap (vecElem v))

                    The tuple of realisers, applied to a total argument, is arg-like.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.mem_mOfFn {n : โ„•} (p : Fin n โ†’ Part โ„•) (w : List.Vector โ„• n) :
                    w โˆˆ List.Vector.mOfFn p โ†” โˆ€ (i : Fin n), w.get i โˆˆ p i

                    Membership in mOfFn (Part monad): a vector is produced iff each coordinate is a value.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_comp {m nn : โ„•} (f : List.Vector โ„• nn โ†’. โ„•) (g : Fin nn โ†’ List.Vector โ„• m โ†’. โ„•) (ฯ†f : ApproximableMap ๐’ฉ Example43.N) (hf : LamDef ฯ†f f) (ฯ†g : Fin nn โ†’ ApproximableMap ๐’ฉ Example43.N) (hg : โˆ€ (i : Fin nn), LamDef (ฯ†g i) (g i)) :
                    LamDef (strictGuardN m (ฯ†f.comp (tupleMap nn ฯ†g))) fun (v : List.Vector โ„• m) => (List.Vector.mOfFn fun (i : Fin nn) => g i v) >>= f

                    Composition (Scott's multivariate composition). If f and each gแตข are ฮป-defined, so is v โ†ฆ (โŸจgโ‚€ v, โ€ฆ, g_{nn-1} vโŸฉ) >>= f.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_coe_val {n : โ„•} {ฯ† : ApproximableMap ๐’ฉ Example43.N} {g : List.Vector โ„• n โ†’ โ„•} (h : LamDef ฯ† โ†‘g) (v : List.Vector โ„• n) :
                    ฯ†.toElementMap (vecElem v) = Example43.natElem (g v)

                    A realiser of a total function evaluates to its value.

                    source
                    theorem Domain.Neighborhood.Theorem56Full.lamDef_primComp {m nn : โ„•} (fโ‚€ : List.Vector โ„• nn โ†’ โ„•) (gโ‚€ : Fin nn โ†’ List.Vector โ„• m โ†’ โ„•) (ฯ†f : ApproximableMap ๐’ฉ Example43.N) (hf : LamDef ฯ†f โ†‘fโ‚€) (ฯ†g : Fin nn โ†’ ApproximableMap ๐’ฉ Example43.N) (hg : โˆ€ (i : Fin nn), LamDef (ฯ†g i) โ†‘(gโ‚€ i)) :
                    LamDef (strictGuardN m (ฯ†f.comp (tupleMap nn ฯ†g))) โ†‘fun (a : List.Vector โ„• m) => fโ‚€ (List.Vector.ofFn fun (i : Fin nn) => gโ‚€ i a)

                    Composition of total functions (the Nat.Primrec'.comp shape).

                    vecElem of a cons is a push. #

                    source
                    theorem Domain.Neighborhood.Theorem56Full.push_natElem_vecElem {n : โ„•} (a : โ„•) (u : List.Vector โ„• n) :
                    (Exercise511.push Example43.N).toElementMap (pair (Example43.natElem a) (vecElem u)) = vecElem (a ::แตฅ u)

                    Primitive recursion. #

                    The recursion lives over prod (funSpace ๐’ฉ N) ๐’ฉ: k is the unknown, z the argument stack whose head is the recursion variable and whose tail carries the parameters. The body is M(k, z) = cond(zero(head z), f(tail z), g(โŸจpred(head z), โŸจk(โŸจpred(head z), tail zโŸฉ), tail zโŸฉโŸฉ)).

                    source
                    def Domain.Neighborhood.Theorem56Full.precBody (ฯ†f ฯ†g : ApproximableMap ๐’ฉ Example43.N) :
                    ApproximableMap (prod (funSpace ๐’ฉ Example43.N) ๐’ฉ) Example43.N

                    The primitive-recursion body.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem Domain.Neighborhood.Theorem56Full.precBody_apply (ฯ†f ฯ†g : ApproximableMap ๐’ฉ Example43.N) (k : (funSpace ๐’ฉ Example43.N).Element) (z : ๐’ฉ.Element) :
                      (precBody ฯ†f ฯ†g).toElementMap (pair k z) = (Exercise326.cond Example43.N).toElementMap (pair (Example43.zeroMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) (pair (ฯ†f.toElementMap ((Exercise511.tail Example43.N).toElementMap z)) (ฯ†g.toElementMap ((Exercise511.push Example43.N).toElementMap (pair (Example43.predMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) ((Exercise511.push Example43.N).toElementMap (pair ((toApproxMap k).toElementMap ((Exercise511.push Example43.N).toElementMap (pair (Example43.predMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) ((Exercise511.tail Example43.N).toElementMap z)))) ((Exercise511.tail Example43.N).toElementMap z))))))))
                      source
                      def Domain.Neighborhood.Theorem56Full.recOp (ฯ†f ฯ†g : ApproximableMap ๐’ฉ Example43.N) :
                      ApproximableMap (funSpace ๐’ฉ Example43.N) (funSpace ๐’ฉ Example43.N)

                      The primitive-recursion operator R(k) = ฮปz. โ€ฆ.

                      Equations
                      Instances For
                        source
                        def Domain.Neighborhood.Theorem56Full.recMap (ฯ†f ฯ†g : ApproximableMap ๐’ฉ Example43.N) :
                        ApproximableMap ๐’ฉ Example43.N

                        recMap : ๐’ฉ โ†’ N, the least fixed point of recOp (before strictifying).

                        Equations
                        Instances For
                          source
                          theorem Domain.Neighborhood.Theorem56Full.recMap_rec (ฯ†f ฯ†g : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) :
                          (recMap ฯ†f ฯ†g).toElementMap z = (Exercise326.cond Example43.N).toElementMap (pair (Example43.zeroMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) (pair (ฯ†f.toElementMap ((Exercise511.tail Example43.N).toElementMap z)) (ฯ†g.toElementMap ((Exercise511.push Example43.N).toElementMap (pair (Example43.predMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) ((Exercise511.push Example43.N).toElementMap (pair ((recMap ฯ†f ฯ†g).toElementMap ((Exercise511.push Example43.N).toElementMap (pair (Example43.predMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) ((Exercise511.tail Example43.N).toElementMap z)))) ((Exercise511.tail Example43.N).toElementMap z))))))))

                          The defining recursion equation.

                          source
                          theorem Domain.Neighborhood.Theorem56Full.recMap_eval (ฯ†f ฯ†g : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} (fโ‚€ : List.Vector โ„• n โ†’ โ„•) (gโ‚€ : List.Vector โ„• (n + 2) โ†’ โ„•) (hf : LamDef ฯ†f โ†‘fโ‚€) (hg : LamDef ฯ†g โ†‘gโ‚€) (u : List.Vector โ„• n) (d : โ„•) :
                          (recMap ฯ†f ฯ†g).toElementMap (vecElem (d ::แตฅ u)) = Example43.natElem (Nat.rec (fโ‚€ u) (fun (y IH : โ„•) => gโ‚€ (y ::แตฅ IH ::แตฅ u)) d)

                          Primitive recursion computes. recMap(โŸจd, uโŸฉ) = (Nat.rec (f u) (g โ€ฆ) d).

                          source
                          theorem Domain.Neighborhood.Theorem56Full.lamDef_prec (ฯ†f ฯ†g : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} (fโ‚€ : List.Vector โ„• n โ†’ โ„•) (gโ‚€ : List.Vector โ„• (n + 2) โ†’ โ„•) (hf : LamDef ฯ†f โ†‘fโ‚€) (hg : LamDef ฯ†g โ†‘gโ‚€) :
                          LamDef (strictGuardN (n + 1) (recMap ฯ†f ฯ†g)) โ†‘fun (v : List.Vector โ„• (n + 1)) => Nat.rec (fโ‚€ v.tail) (fun (y IH : โ„•) => gโ‚€ (y ::แตฅ IH ::แตฅ v.tail)) v.head

                          Primitive recursion (Nat.Primrec'.prec shape).

                          Closure of the primitive recursive functions. #

                          source
                          theorem Domain.Neighborhood.Theorem56Full.primrec_lamDef {n : โ„•} {f : List.Vector โ„• n โ†’ โ„•} (h : Nat.Primrec' f) :
                          โˆƒ (ฯ† : ApproximableMap ๐’ฉ Example43.N), LamDef ฯ† โ†‘f

                          Every Nat.Primrec' function is ฮป-definable by a (very strict) approximable map.

                          Minimisation (rfind). #

                          The ฮผ-operator searches upward for the least k with f(k ::แตฅ v) = 0. We carry the counter in the head coordinate of the stack. The search body over prod (funSpace ๐’ฉ N) ๐’ฉ is

                          S(k, z) = cond(zero(f z), head z, k(push(succ(head z), tail z))) :

                          if the current value f z is 0, return the counter head z; otherwise recurse with the counter bumped by one. searchMap is the least fixed point, and findMap kicks the search off at counter 0. The hard direction is divergence: when no k zeroes f, every finite approximant Sโฟ(โŠฅ) returns โŠฅ along the search trace, so the directed sup (Theorem 4.2(iii)) is โŠฅ too.

                          source
                          def Domain.Neighborhood.Theorem56Full.findBody (ฯ†f : ApproximableMap ๐’ฉ Example43.N) :
                          ApproximableMap (prod (funSpace ๐’ฉ Example43.N) ๐’ฉ) Example43.N

                          The search body S(k, z) = cond(zero(f z), head z, k(push(succ(head z), tail z))).

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem Domain.Neighborhood.Theorem56Full.findBody_apply (ฯ†f : ApproximableMap ๐’ฉ Example43.N) (k : (funSpace ๐’ฉ Example43.N).Element) (z : ๐’ฉ.Element) :
                            (findBody ฯ†f).toElementMap (pair k z) = (Exercise326.cond Example43.N).toElementMap (pair (Example43.zeroMap.toElementMap (ฯ†f.toElementMap z)) (pair ((Exercise511.head Example43.N).toElementMap z) ((toApproxMap k).toElementMap ((Exercise511.push Example43.N).toElementMap (pair (Example43.succMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) ((Exercise511.tail Example43.N).toElementMap z))))))
                            source
                            def Domain.Neighborhood.Theorem56Full.findOp (ฯ†f : ApproximableMap ๐’ฉ Example43.N) :
                            ApproximableMap (funSpace ๐’ฉ Example43.N) (funSpace ๐’ฉ Example43.N)

                            The search operator S(k) = ฮปz. โ€ฆ, whose least fixed point is the running search.

                            Equations
                            Instances For
                              source
                              def Domain.Neighborhood.Theorem56Full.searchMap (ฯ†f : ApproximableMap ๐’ฉ Example43.N) :
                              ApproximableMap ๐’ฉ Example43.N

                              searchMap : ๐’ฉ โ†’ N, the least fixed point of findOp (the counter lives in coordinate 0).

                              Equations
                              Instances For
                                source
                                theorem Domain.Neighborhood.Theorem56Full.searchMap_rec (ฯ†f : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) :
                                (searchMap ฯ†f).toElementMap z = (Exercise326.cond Example43.N).toElementMap (pair (Example43.zeroMap.toElementMap (ฯ†f.toElementMap z)) (pair ((Exercise511.head Example43.N).toElementMap z) ((searchMap ฯ†f).toElementMap ((Exercise511.push Example43.N).toElementMap (pair (Example43.succMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) ((Exercise511.tail Example43.N).toElementMap z))))))

                                The defining recursion equation of the search.

                                source
                                def Domain.Neighborhood.Theorem56Full.findMap (ฯ†f : ApproximableMap ๐’ฉ Example43.N) :
                                ApproximableMap ๐’ฉ Example43.N

                                findMap : ๐’ฉ โ†’ N starts the search with counter 0.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  theorem Domain.Neighborhood.Theorem56Full.findMap_vecElem (ฯ†f : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} (v : List.Vector โ„• n) :
                                  (findMap ฯ†f).toElementMap (vecElem v) = (searchMap ฯ†f).toElementMap (vecElem (0 ::แตฅ v))
                                  source
                                  theorem Domain.Neighborhood.Theorem56Full.searchMap_step_found (ฯ†f : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} {f : List.Vector โ„• (n + 1) โ†’ โ„•} (hf : LamDef ฯ†f โ†‘f) (v : List.Vector โ„• n) (k : โ„•) (h0 : f (k ::แตฅ v) = 0) :
                                  (searchMap ฯ†f).toElementMap (vecElem (k ::แตฅ v)) = Example43.natElem k

                                  Search step (found). If f(k ::แตฅ v) = 0, the search returns the counter k.

                                  source
                                  theorem Domain.Neighborhood.Theorem56Full.searchMap_step_next (ฯ†f : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} {f : List.Vector โ„• (n + 1) โ†’ โ„•} (hf : LamDef ฯ†f โ†‘f) (v : List.Vector โ„• n) (k : โ„•) (hne : f (k ::แตฅ v) โ‰  0) :
                                  (searchMap ฯ†f).toElementMap (vecElem (k ::แตฅ v)) = (searchMap ฯ†f).toElementMap (vecElem ((k + 1) ::แตฅ v))

                                  Search step (continue). If f(k ::แตฅ v) โ‰  0, the search advances to counter k + 1.

                                  source
                                  theorem Domain.Neighborhood.Theorem56Full.searchMap_climb (ฯ†f : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} {f : List.Vector โ„• (n + 1) โ†’ โ„•} (hf : LamDef ฯ†f โ†‘f) (v : List.Vector โ„• n) (m : โ„•) (hm0 : f (m ::แตฅ v) = 0) (hmin : โˆ€ i < m, f (i ::แตฅ v) โ‰  0) (d j : โ„•) :
                                  j + d = m โ†’ (searchMap ฯ†f).toElementMap (vecElem (j ::แตฅ v)) = Example43.natElem m

                                  Capstone (least zero โŸน value). If m is a zero of f(ยท ::แตฅ v) and nothing below it is, then starting from any counter j โ‰ค m the search returns m. (Downward induction on m - j.)

                                  Divergence via the directed sup of approximants. #

                                  source
                                  theorem Domain.Neighborhood.Theorem56Full.toApproxMap_bot (z : ๐’ฉ.Element) :
                                  (toApproxMap (funSpace ๐’ฉ Example43.N).bot).toElementMap z = Example43.N.bot

                                  The least map of the function space evaluates to โŠฅ everywhere.

                                  source
                                  def Domain.Neighborhood.Theorem56Full.evalAt (z : ๐’ฉ.Element) :
                                  ApproximableMap (funSpace ๐’ฉ Example43.N) Example43.N

                                  evalAt z evaluates a function-space element at the fixed argument z.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.evalAt_apply (z : ๐’ฉ.Element) (ฯ† : (funSpace ๐’ฉ Example43.N).Element) :
                                    (evalAt z).toElementMap ฯ† = (toApproxMap ฯ†).toElementMap z
                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.findOp_iterElem_zero (ฯ†f : ApproximableMap ๐’ฉ Example43.N) :
                                    (findOp ฯ†f).iterElem 0 = (funSpace ๐’ฉ Example43.N).bot

                                    The 0-th approximant Sโฐ(โŠฅ) is the bottom map.

                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.iterVal_zero (ฯ†f : ApproximableMap ๐’ฉ Example43.N) (z : ๐’ฉ.Element) :
                                    (toApproxMap ((findOp ฯ†f).iterElem 0)).toElementMap z = Example43.N.bot

                                    Value of the 0-th approximant: โŠฅ.

                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.iterVal_succ (ฯ†f : ApproximableMap ๐’ฉ Example43.N) (m : โ„•) (z : ๐’ฉ.Element) :
                                    (toApproxMap ((findOp ฯ†f).iterElem (m + 1))).toElementMap z = (Exercise326.cond Example43.N).toElementMap (pair (Example43.zeroMap.toElementMap (ฯ†f.toElementMap z)) (pair ((Exercise511.head Example43.N).toElementMap z) ((toApproxMap ((findOp ฯ†f).iterElem m)).toElementMap ((Exercise511.push Example43.N).toElementMap (pair (Example43.succMap.toElementMap ((Exercise511.head Example43.N).toElementMap z)) ((Exercise511.tail Example43.N).toElementMap z))))))

                                    Recursion equation for the approximant values: S^{m+1}(โŠฅ) unfolds one search step using Sแต(โŠฅ) as the continuation.

                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.iterVal_bot (ฯ†f : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} {f : List.Vector โ„• (n + 1) โ†’ โ„•} (hf : LamDef ฯ†f โ†‘f) (v : List.Vector โ„• n) (hdiv : โˆ€ (k : โ„•), f (k ::แตฅ v) โ‰  0) (m k : โ„•) :
                                    (toApproxMap ((findOp ฯ†f).iterElem m)).toElementMap (vecElem (k ::แตฅ v)) = Example43.N.bot

                                    Along a no-zero trace, every finite approximant returns โŠฅ (induction on the approximant index, with the counter universally quantified since the search advances it).

                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.searchMap_diverge (ฯ†f : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} {f : List.Vector โ„• (n + 1) โ†’ โ„•} (hf : LamDef ฯ†f โ†‘f) (v : List.Vector โ„• n) (hdiv : โˆ€ (k : โ„•), f (k ::แตฅ v) โ‰  0) (k : โ„•) :
                                    (searchMap ฯ†f).toElementMap (vecElem (k ::แตฅ v)) = Example43.N.bot

                                    Divergence. If f(ยท ::แตฅ v) has no zero, the search is โŠฅ from every counter. The fixed point is the directed union of the approximants Sแต(โŠฅ) (Theorem 4.2(iii)); pushing the evaluation at vecElem (k ::แตฅ v) through this sup (continuity, toElementMap_iSupDirected) reduces the claim to iterVal_bot.

                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.lamDef_rfind (ฯ†f : ApproximableMap ๐’ฉ Example43.N) {n : โ„•} {f : List.Vector โ„• (n + 1) โ†’ โ„•} (hf : LamDef ฯ†f โ†‘f) :
                                    LamDef (strictGuardN n (findMap ฯ†f)) fun (v : List.Vector โ„• n) => Nat.rfind fun (k : โ„•) => Part.some (decide (f (k ::แตฅ v) = 0))

                                    Minimisation (Nat.Partrec'.rfind shape). Given a (very strict) realiser of a total f : Vector โ„• (n+1) โ†’ โ„•, strictGuardN n (findMap ฯ†f) ฮป-defines v โ†ฆ ฮผk. f(k ::แตฅ v) = 0.

                                    Closure of the partial recursive functions โ€” the full meta-theorem. #

                                    source
                                    theorem Domain.Neighborhood.Theorem56Full.partrec_lamDef {n : โ„•} {f : List.Vector โ„• n โ†’. โ„•} (h : Nat.Partrec' f) :
                                    โˆƒ (ฯ† : ApproximableMap ๐’ฉ Example43.N), LamDef ฯ† f

                                    Theorem 5.6 (Scott 1981, PRG-19) โ€” every partial recursive function is ฮป-definable. For each Nat.Partrec' function f : Vector โ„• n โ†’. โ„• there is an approximable map ฯ† : ๐’ฉ โ†’ N that is a very strict ฮป-definition of f: it returns f's value on total arguments, โŠฅ where f is undefined, and โŠฅ on any arg-like input with a โŠฅ among its first n coordinates.

                                    Scott's 1-ary statement. #

                                    Every partial recursive h : โ„• โ†’. โ„• is realised by an approximable map ฯ„ : N โ†’ N over the flat naturals: ฯ„(nฬ‚) = mฬ‚ when h n = m, ฯ„(nฬ‚) = โŠฅ when h n diverges, and ฯ„(โŠฅ) = โŠฅ (strictness).

                                    source
                                    def Domain.Neighborhood.Theorem56Full.oneArg :
                                    ApproximableMap Example43.N ๐’ฉ

                                    Inject N โ†’ ๐’ฉ as the stack whose only nonzero coordinate is the head.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      theorem Domain.Neighborhood.Theorem56Full.oneArg_natElem (a : โ„•) :
                                      oneArg.toElementMap (Example43.natElem a) = vecElem (a ::แตฅ List.Vector.nil)
                                      source
                                      theorem Domain.Neighborhood.Theorem56Full.oneArg_bot :
                                      oneArg.toElementMap Example43.N.bot = ๐’ฉ.bot
                                      source
                                      theorem Domain.Neighborhood.Theorem56Full.partrec_one {h : โ„• โ†’. โ„•} (H : Nat.Partrec' fun (v : List.Vector โ„• 1) => h v.head) :
                                      โˆƒ (ฯ„ : ApproximableMap Example43.N Example43.N), (โˆ€ (a m : โ„•), m โˆˆ h a โ†’ ฯ„.toElementMap (Example43.natElem a) = Example43.natElem m) โˆง (โˆ€ (a : โ„•), ยฌ(h a).Dom โ†’ ฯ„.toElementMap (Example43.natElem a) = Example43.N.bot) โˆง ฯ„.toElementMap Example43.N.bot = Example43.N.bot

                                      Scott's 1-ary meta-theorem. A partial recursive h : โ„• โ†’. โ„• (presented as a unary Nat.Partrec') is denoted by a single approximable map ฯ„ : N โ†’ N that is correct on values, divergent where h diverges, and strict.