module Cat.Restriction.Base where

Restriction CategoriesπŸ”—

Much of computer science involves the study of partial functions. Unfortunately, partial functions are somewhat tedious to work with, as they aren’t really functions; they’re relations! Furthermore, we are often interested in computable partial functions; this means that we can not identify partial functions A⇀BA \rightharpoonup B with total functions Aβ†’Maybe(B)A \to \mathrm{Maybe}(B)1. This leaves us with a few possible approaches. The most first approach that may come to mind is to encode partial functions A⇀BA \rightharpoonup B as total functions from a subobject Xβ†ͺAX \hookrightarrow A. Alternatively, we could find some construction that classifies partial maps; this is what the naive Maybe approach attempted to do. We could also just work with functional relations directly, though this is ill-advised.

Each of these approaches has its own benefits and drawbacks, which makes choosing one difficult. Restriction categories offer an alternative, algebraic approach to the problem, allowing us to neatly sidestep any questions about encodings.

Our prototypical restriction category will be Par\mathbf{Par}, the category of sets and partial functions. The key insight is that every partial function f:A⇀Bf : A \rightharpoonup B is defined on some domain XβŠ†AX \subseteq A; this yields a partial function f↓:A⇀Af \downarrow : A \rightharpoonup A that maps xx to itself iff f(x)f(x) is defined. We can generalize this insight to an arbitrary category C\mathcal{C} by equipping C\mathcal{C} with an operation (βˆ’)↓:C(x,y)β†’C(x,x)(-)^{\downarrow} : \mathcal{C}(x,y) \to \mathcal{C}(x,x).

–

record Restriction-category
  {o β„“} (C : Precategory o β„“)
  : Type (o βŠ” β„“) where
  no-eta-equality
  open Precategory C
  field
    _↓ : βˆ€ {x y} β†’ Hom x y β†’ Hom x x

  infix 50 _↓

We require that (βˆ’)↓(-)^{\downarrow} satisfies 4 axioms: - ff↓=fff^{\downarrow} = f. In Par\mathbf{Par}, this corresponds to the fact that f↓(x)f^{\downarrow}(x) is defined to be xx iff ff is defined, so precomposing with it does nothing.

  field
    ↓-dom : βˆ€ {x y} β†’ (f : Hom x y) β†’ f ∘ (f ↓) ≑ f
  • f↓g↓=g↓f↓f^{\downarrow}g^{\downarrow} = g^{\downarrow}f^{\downarrow}. In Par\mathbf{Par}, this falls out of the fact that restriction maps do not modify their arguments, and it doesn’t matter if ff diverges first or gg does; all that matters is that it diverges!
  field
    ↓-comm : βˆ€ {x y z} β†’ (f : Hom x z) (g : Hom x y) β†’ f ↓ ∘ g ↓ ≑ g ↓ ∘ f ↓
  • (gf↓)↓=g↓f↓(gf^{\downarrow})^{\downarrow} = g^{\downarrow}f^{\downarrow}. This axiom holds in the Par\mathbf{Par}, as (gf↓)↓(x)(gf^{\downarrow})^{\downarrow}(x) ignores the action of gg on xx, and focuses only on its termination.
  field
    ↓-smashr : βˆ€ {x y z} β†’ (f : Hom x z) (g : Hom x y) β†’ (g ∘ f ↓) ↓ ≑ g ↓ ∘ f ↓
  • f↓g=g(fg)↓f^{\downarrow} g = g (f g)^{\downarrow}. This is the trickiest of the bunch to understand in Par\mathbf{Par}. Note that if we postcompose gg with a domain map f↓f^{\downarrow}, then we still need to take into account the action of gg; furthermore, its domain of definition needs to be restricted to image of gg.
  field
    ↓-swap : βˆ€ {x y z} β†’ (f : Hom y z) (g : Hom x y) β†’ f ↓ ∘ g ≑ g ∘ (f ∘ g) ↓

  1. We can easily determine if functions into Maybe β€œdiverge” by checking if they return nothing. If we identify partial functions with total functions into Maybe, we can decide if a partial function terminates, which is extremely uncomputable!β†©οΈŽ