Documentation

LeanPool.DomainTheory.Neighborhood.Theorem76

Theorem 7.6 (Scott 1981, PRG-19, ยง7) โ€” fix : (๐’Ÿ โ†’ ๐’Ÿ) โ†’ ๐’Ÿ is computable #

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19, Lecture VII.

Theorem 7.6. For any effectively given domain ๐’Ÿ, the combinator fix : (๐’Ÿ โ†’ ๐’Ÿ) โ†’ ๐’Ÿ is computable.

Scott's proof reads off the neighbourhood relation of fix from the fixed-point construction of Theorem 4.1/4.2: writing ๐’Ÿ = {Xโ‚™} effectively given,

โ‹‚_{i<q} [X_{nแตข}, X_{mแตข}] fix X_โ„“ iff for some finite sequence ฮ” = X_{kโ‚€}, โ€ฆ, X_{k_p} = X_โ„“ we have, for each j < p, โ‹‚{ X_{mแตข} โˆฃ X_{kโฑผ} โŠ† X_{nแตข} } โŠ† X_{kโฑผโ‚Šโ‚}.

Inside "for some finite sequence" all the checks are decidable (by the effective presentation), and the existential quantification of a decidable predicate is recursively enumerable. (Since there is no bound on the length of the sequence, this is genuinely r.e. and not generally recursive.)

Strategy (choice-free) #

The function-space neighbourhood F = Xenum c (Theorem 7.5) is a finite intersection โ‹‚[X_{nแตข}, X_{mแตข}]; its least map is ฤ = toApproxMap (โ†‘F), and (fix V).rel F (X_โ„“) unfolds via rel_iff_mem_principal + fixMap_toElementMap + mem_fixElement to

โˆƒ p, (ฤแต–).rel ฮ” (X_โ„“).

The one-step relation ฤ.rel (X_a) (X_b) โ†” F โŠ† [X_a, X_b] is exactly Scott's โ‹‚{X_{mแตข} โˆฃ X_a โŠ† X_{nแตข}} โŠ† X_b, and โ€” crucially โ€” it is recursively decidable, because [X_a, X_b] = Xenum (codePair a b) (a one-entry, always-consistent function-space neighbourhood) so the test is the decidable function-space inclusion Xenum c โŠ† Xenum (codePair a b) (funPresentation.incl_computable, Theorem 7.5).

We model a finite ฤ-chain by a list of indices (using surj to name each intermediate neighbourhood) and prove the characterisation (fix V).rel (Xenum c) (X_โ„“) โ†” โˆƒ full, gStepsOK โ€ฆ (soundness/completeness over the list, choice-free). The existential over the list is then realised as the r.e. โˆƒ i, q (pair i n), where q decodes i to the chain, runs a single primitive-recursive foldCode (fixChainChar) threading the previous index and a {0,1} consistency flag, and checks the flag together with the final inclusion X_{last} โŠ† X_โ„“. Everything audits โŠ† {propext, Quot.sound}.

A finite g-chain over presentation indices. #

gStepsOK g P a full says: starting from the index a, the consecutive g-steps along the index list full all hold, and gLastOf a full is the final index reached.

source
def Domain.Neighborhood.gLastOf :
โ„• โ†’ List โ„• โ†’ โ„•

The last index of the chain a, fullโ‚€, fullโ‚, โ€ฆ.

Equations
Instances For
    source
    def Domain.Neighborhood.gStepsOK {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (g : ApproximableMap V V) (P : ComputablePresentation V) :
    โ„• โ†’ List โ„• โ†’ Prop

    The consecutive g-steps g.rel (X_a) (X_{fullโ‚€}), g.rel (X_{fullโ‚€}) (X_{fullโ‚}), โ€ฆ all hold.

    Equations
    Instances For
      source
      theorem Domain.Neighborhood.gStepsOK_sound {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (g : ApproximableMap V V) (P : ComputablePresentation V) (full : List โ„•) (a : โ„•) :
      gStepsOK g P a full โ†’ (g.iterMap full.length).rel (P.X a) (P.X (gLastOf a full))

      Soundness of a chain. A valid g-chain from a realises the iterate relation (gแต).rel (X_a) (X_{last}) with k the chain length.

      source
      theorem Domain.Neighborhood.gStepsOK_complete {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (g : ApproximableMap V V) (P : ComputablePresentation V) (n a โ„“ : โ„•) :
      (g.iterMap n).rel (P.X a) (P.X โ„“) โ†’ โˆƒ (full : List โ„•), gStepsOK g P a full โˆง P.X (gLastOf a full) โŠ† P.X โ„“

      Completeness of a chain. If (gโฟ).rel (X_a) (X_โ„“), then there is a valid g-chain from a whose final neighbourhood is contained in X_โ„“. (The intermediate neighbourhoods are named via surj; the relaxed final condition X_{last} โŠ† X_โ„“ handles the n = 0 base.)

      source
      theorem Domain.Neighborhood.fixElement_mem_iff_chain {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (g : ApproximableMap V V) (P : ComputablePresentation V) (a0 : โ„•) (ha0 : P.X a0 = V.master) (โ„“ : โ„•) :
      g.fixElement.mem (P.X โ„“) โ†” โˆƒ (full : List โ„•), gStepsOK g P a0 full โˆง P.X (gLastOf a0 full) โŠ† P.X โ„“

      Chain characterisation of g's least fixed point. A neighbourhood X_โ„“ is in fix(g) iff a valid g-chain (from a master index aโ‚€ with X_{aโ‚€} = ฮ”) reaches a final neighbourhood inside X_โ„“.

      The least map of Xenum c and its decidable one-step relation. #

      source
      def Domain.Neighborhood.codePair (a b : โ„•) :
      โ„•

      The one-entry function-space code: Xenum (codePair a b) = [X_a, X_b].

      Equations
      Instances For
        source
        theorem Domain.Neighborhood.Xenum_codePair {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (gN : โ„• โ†’ โ„•) (hgN : โˆ€ (c : โ„•), gN c = 1 โ†” (stepFun (funListOf P P (Recursive.decodeList c))).Nonempty) (a b : โ„•) :
        Xenum P P gN (codePair a b) = step (P.X a) (P.X b)

        Xenum (codePair a b) = [X_a, X_b] (a one-entry, always-consistent function-space neighbourhood); a thin wrapper around Xenum_singleton.

        source
        theorem Domain.Neighborhood.leastMap_Xenum_rel {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (gN : โ„• โ†’ โ„•) (hgN : โˆ€ (c : โ„•), gN c = 1 โ†” (stepFun (funListOf P P (Recursive.decodeList c))).Nonempty) (c a b : โ„•) :
        (toApproxMap ((funSpace V V).principal โ‹ฏ)).rel (P.X a) (P.X b) โ†” Xenum P P gN c โŠ† step (P.X a) (P.X b)

        The least map ฤ of the function-space neighbourhood Xenum c relates X_a to X_b exactly when Xenum c โŠ† [X_a, X_b] (Scott's โ‹‚{X_{mแตข} โˆฃ X_a โŠ† X_{nแตข}} โŠ† X_b).

        source
        theorem Domain.Neighborhood.fixMap_rel_iff {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (gN : โ„• โ†’ โ„•) (hgN : โˆ€ (c : โ„•), gN c = 1 โ†” (stepFun (funListOf P P (Recursive.decodeList c))).Nonempty) (c โ„“ : โ„•) :
        (fixMap V).rel (Xenum P P gN c) (P.X โ„“) โ†” โˆƒ (full : List โ„•), gStepsOK (toApproxMap ((funSpace V V).principal โ‹ฏ)) P P.masterIdx full โˆง P.X (gLastOf P.masterIdx full) โŠ† P.X โ„“

        The fix neighbourhood relation, chain form. (fix V).rel (Xenum c) (X_โ„“) holds iff there is a valid least-map chain from the master index reaching a neighbourhood inside X_โ„“. This is Scott's "โ‹‚[X_{nแตข}, X_{mแตข}] fix X_โ„“ iff for some finite sequence โ€ฆ".

        The decidable chain predicate and its primitive-recursive foldCode. #

        source
        def Domain.Neighborhood.chainDec (fincl : โ„• โ†’ โ„•) (c : โ„•) :
        โ„• โ†’ List โ„• โ†’ Prop

        The decidable mirror of gStepsOK, phrased with the function-space inclusion char fincl.

        Equations
        Instances For
          source
          theorem Domain.Neighborhood.chainDec_iff_gStepsOK {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (gN : โ„• โ†’ โ„•) (hgN : โˆ€ (c : โ„•), gN c = 1 โ†” (stepFun (funListOf P P (Recursive.decodeList c))).Nonempty) (fincl : โ„• โ†’ โ„•) (hfincl : โˆ€ (s : โ„•), fincl s = 1 โ†” Xenum P P gN (Nat.unpair s).1 โŠ† Xenum P P gN (Nat.unpair s).2) (c : โ„•) (full : List โ„•) (a : โ„•) :
          chainDec fincl c a full โ†” gStepsOK (toApproxMap ((funSpace V V).principal โ‹ฏ)) P a full

          chainDec is equivalent to gStepsOK of the least map, via the inclusion char's spec and Xenum (codePair a b) = [X_a, X_b].

          source
          def Domain.Neighborhood.fixStp (fincl : โ„• โ†’ โ„•) (w : โ„•) :
          โ„•

          One packed foldCode step: state pair acc params with acc = pair prev flag, current element x. Updates the flag with the one-step consistency test and advances prev to x.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Domain.Neighborhood.fixPStep (fincl : โ„• โ†’ โ„•) (c acc x : โ„•) :
            โ„•

            The pure left-fold step corresponding to fixStp (parameter c, accumulator acc = pair prev flag, current element x).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Domain.Neighborhood.fixStp_eq (fincl : โ„• โ†’ โ„•) (c acc x : โ„•) :
              fixStp fincl (Nat.pair x (Nat.pair acc c)) = fixPStep fincl c acc x
              source
              theorem Domain.Neighborhood.primrec_fixStp (fincl : โ„• โ†’ โ„•) (hfinclp : Nat.Primrec fincl) :
              Nat.Primrec (fixStp fincl)
              source
              def Domain.Neighborhood.fixChainChar {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (fincl : โ„• โ†’ โ„•) (c i : โ„•) :
              โ„•

              The chain foldCode: starts from pair masterIdx 1, threads the parameter c, over the list coded by i. Returns pair lastIdx flag.

              Equations
              Instances For
                source
                theorem Domain.Neighborhood.fixChainChar_eq {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (fincl : โ„• โ†’ โ„•) (c i : โ„•) :
                fixChainChar P fincl c i = List.foldl (fixPStep fincl c) (Nat.pair P.masterIdx 1) (Recursive.decodeList i)
                source
                theorem Domain.Neighborhood.primrec_fixChainChar {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (fincl : โ„• โ†’ โ„•) (hfinclp : Nat.Primrec fincl) :
                Nat.Primrec fun (t : โ„•) => fixChainChar P fincl (Nat.unpair t).1 (Nat.unpair t).2
                source
                theorem Domain.Neighborhood.fixPStep_foldl_fst (fincl : โ„• โ†’ โ„•) (c : โ„•) (full : List โ„•) (prev fl : โ„•) :
                (Nat.unpair (List.foldl (fixPStep fincl c) (Nat.pair prev fl) full)).1 = gLastOf prev full

                The foldCode tracks the last index reached.

                source
                theorem Domain.Neighborhood.fixPStep_foldl_snd (fincl : โ„• โ†’ โ„•) (c : โ„•) (full : List โ„•) (prev fl : โ„•) :
                fl โ‰ค 1 โ†’ ((Nat.unpair (List.foldl (fixPStep fincl c) (Nat.pair prev fl) full)).2 = 1 โ†” fl = 1 โˆง chainDec fincl c prev full)

                The foldCode flag is 1 iff the start flag is 1 and the whole chain is consistent.

                source
                theorem Domain.Neighborhood.fixChainChar_spec {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (fincl : โ„• โ†’ โ„•) (c i : โ„•) :
                (Nat.unpair (fixChainChar P fincl c i)).1 = gLastOf P.masterIdx (Recursive.decodeList i) โˆง ((Nat.unpair (fixChainChar P fincl c i)).2 = 1 โ†” chainDec fincl c P.masterIdx (Recursive.decodeList i))

                Read-off of the foldCode: its .1 is the last index of decodeList i, and its .2 = 1 iff the decoded chain is consistent.

                source
                theorem Domain.Neighborhood.fixMap_isComputable {ฮฑ : Type u_1} {V : NeighborhoodSystem ฮฑ} (P : ComputablePresentation V) (gN incl eq : โ„• โ†’ โ„•) (hgN : โˆ€ (c : โ„•), gN c = 1 โ†” (stepFun (funListOf P P (Recursive.decodeList c))).Nonempty) (hgNp : Nat.Primrec gN) (hincl : โˆ€ (s : โ„•), incl s = 1 โ†” P.X (Nat.unpair s).1 โŠ† P.X (Nat.unpair s).2) (hinclp : Nat.Primrec incl) (heq : โˆ€ (s : โ„•), eq s = 1 โ†” P.X (Nat.unpair s).1 = P.X (Nat.unpair s).2) (heqp : Nat.Primrec eq) :
                IsComputableMap (funPresentation P P gN incl incl eq hgN hgNp hincl hinclp hincl hinclp heq heqp) P (fixMap V)

                Theorem 7.6 (Scott 1981, PRG-19) โ€” fix is computable (choice-free). For any effectively given domain ๐’Ÿ (here a computable presentation P of V, together with the function-space consistency/inclusion/equality chars of Theorem 7.5), the combinator fix : (๐’Ÿ โ†’ ๐’Ÿ) โ†’ ๐’Ÿ is computable: its neighbourhood relation is the recursively-enumerable existential โˆƒ chain over the decidable least-map step relation.