module Cat.Instances.OFE.Complete where

Limits and complete OFEsπŸ”—

Since OFEs are metric-space-like1 structures, there is a natural notion of sequences getting closer to a value: we say a sequence is a chain if, given we have Looking at the case where this says that we have a sequence

where the metric interpretation of OFEs lets us read this as the distance between successive points approaching

  is-chain : (x : Nat β†’ A) β†’ Type _
  is-chain f = βˆ€ m n β†’ n ≀ m β†’ f m β‰ˆ[ n ] f n

However, in a general OFE, there is not necessarily anything β€œat ”: the values of the sequence get closer to each other, but there’s no specific point they’re getting closer to. An example of chain without limit is as follows: let be an element of a set, and consider the sequence

in the OFE of finite sequences. Clearly this satisfies the chain condition: w.l.o.g. we can assume for some and certainly shares the first elements with However, there is no single list of which shares its first elements with must have a definite length, independent of which bounds the size of its prefixes. Choosing any results in a value of has more elements than the length- prefix of

The previous paragraph contains an unfolding of the definition of a sequence having a limit, or, more specifically, it contains a definition of what it means for a point to be the limit of a sequence: is the limit of if, for all

  is-limit : (x : Nat β†’ A) β†’ A β†’ Type _
  is-limit f a = βˆ€ n β†’ a β‰ˆ[ n ] f n

It follows at once that the limit of a sequence is uniquely determined: if and both claim to be limits of we have, for arbitrary meaning

  limit-is-unique
    : βˆ€ (f : Nat β†’ A) {x y}
    β†’ is-limit f x β†’ is-limit f y β†’ x ≑ y
  limit-is-unique f l1 l2 = P.limit _ _ Ξ» n β†’
    P.β‰ˆ-trans n (P.β‰ˆ-sym n (l2 n)) (l1 n)

However, some OFEs do have limits for all chains: the OFE of infinite sequences is one, for example. We refer to such an OFE as a complete ordered family of equivalences, or COFE2 for short.

  is-cofe : Type _
  is-cofe = βˆ€ (f : Nat β†’ A) β†’ is-chain f β†’ Limit f

We can actually compute the limit of a sequence of sequences pretty easily: we have a function our sequence, and the chain condition says that, given and we get Our limit is the sequence we must show that which means that, given we must have This follows by the chain condition: and so we conclude

  Sequences-is-cofe : is-cofe (Sequences X-set)
  Sequences-is-cofe seq chain = (Ξ» j β†’ seq (suc j) j) , Ξ» n k k<n β†’
    sym (chain _ _ k<n _ ≀-refl)

In passing, let us note that non-expansive maps preserve both chains and their limits.

  non-expansive→chain
    : (f : A β†’ B) (s : Nat β†’ A)
    β†’ is-non-expansive f P Q β†’ is-chain P s β†’ is-chain Q (Ξ» n β†’ f (s n))
  non-expansiveβ†’chain f s ne p m n n≀m = ne .pres-β‰ˆ (p m n n≀m)

  non-expansive→limit
    : (f : A β†’ B) (s : Nat β†’ A) (x : A)
    β†’ is-non-expansive f P Q β†’ is-limit P s x β†’ is-limit Q (Ξ» n β†’ f (s n)) (f x)
  non-expansiveβ†’limit f s x ne lim n = ne .pres-β‰ˆ (lim n)

Banach’s fixed point theoremπŸ”—

Banach’s fixed point theorem, in our setting, says that any contractive on an inhabited COFE has a unique fixed point. We’ll start with uniqueness: suppose that some satisfy and It will suffice to show that and, working in an OFE, this further reduces to for an arbitrary

By induction, with a trivial base case, we can assume to show but is contractive, so it acts on the induction hypothesis to produce But we assumed both and are fixed points, so this is exactly what we want.

  banach : βˆ₯ A βˆ₯ β†’ (f : P β†’αΆœα΅’βΏ P) β†’ Ξ£ A Ξ» x β†’ f .map x ≑ x
  banach inhab f = βˆ₯-βˆ₯-proj fp-unique fp' where
    fp-unique : is-prop (Ξ£ A Ξ» x β†’ f .map x ≑ x)
    fp-unique (a , p) (b , q) =
      Ξ£-prop-path (Ξ» x β†’ from-ofe-on P .fst .is-tr _ _)
        (sym p Β·Β· P.limit _ _ climb Β·Β· q) where
      climb : βˆ€ n β†’ f .map a β‰ˆ[ n ] f .map b
      climb zero    = P.bounded _ _
      climb (suc n) = transport (Ξ» i β†’ f .map (p i) β‰ˆ[ suc n ] f .map (q i)) (f .contract n (climb n))

The point of showing uniqueness is that the fixed point is independent of how is inhabited: in other words, for a contractive mapping on a COFE to have a fixed point, we needn’t β€” will suffice. That aside justifes this sentence: Fix a starting point and consider the sequence

which is a chain again by an inductive argument involving contractivity (formalised below for the curious).

    approx : A β†’ Nat β†’ A
    approx a zero    = a
    approx a (suc n) = f .map (approx a n)

    chain : βˆ€ a β†’ is-chain P (approx a)
    chain a m zero x                = P.bounded (approx a m) a
    chain a (suc m) (suc n) (s≀s x) = f .contract n (chain a m n x)

I claim that the limit of is a fixed point of we can calculate

where we have, in turn, that non-expansive mappings preserve limits, the very definition of and the fact that limits are insensitive to dropping an element at the start.

    fp' : βˆ₯ _ βˆ₯
    fp' = do
      pt ← inhab
      let
        (it , is) = lim (approx pt) (chain pt)

        ne : is-non-expansive (f .map) P P
        ne = record { pres-β‰ˆ = Ξ» p β†’ P.step _ _ _ (f .contract _ p) }

        prf : f .map it ≑ it
        prf =
          f .map it                               β‰‘βŸ¨ limit-is-unique P _ (non-expansiveβ†’limit _ _ _ _ _ ne is) (lim _ _ .snd) βŸ©β‰‘
          lim (Ξ» n β†’ f .map (approx pt n)) _ .fst β‰‘βŸ¨ ap fst (ap (lim _) (Ξ» i β†’ non-expansiveβ†’chain _ _ _ _ ne (chain pt))) βŸ©β‰‘
          lim (Ξ» n β†’ approx pt (suc n)) _ .fst    β‰‘βŸ¨ limit-is-unique P _ (lim _ _ .snd) (limit-to-tail P (approx pt) _ (chain pt) is) βŸ©β‰‘
          it                                      ∎

      pure (it , prf)

  1. An OFE is a 1-bounded, bisected ultrametric space.β†©οΈŽ

  2. Feel free to pronounce it β€œcoffee”.β†©οΈŽ