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 \rightharpoonup B$
with total functions
$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 \rightharpoonup B$
as total functions from a subobject
$X \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 $\mathbf{Par}$, the category of sets and partial functions. The key insight is that every partial function $f : A \rightharpoonup B$ is defined on some domain $X \subseteq A$; this yields a partial function $f \downarrow : A \rightharpoonup A$ that maps $x$ to itself iff $f(x)$ is defined. We can generalize this insight to an arbitrary category $\mathcal{C}$ by equipping $\mathcal{C}$ with an operation $(-)^{\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^{\downarrow} = f$. In $\mathbf{Par}$, this corresponds to the fact that $f^{\downarrow}(x)$ is defined to be $x$ iff $f$ is defined, so precomposing with it does nothing.

field β-dom : β {x y} β (f : Hom x y) β f β (f β) β‘ f

- $f^{\downarrow}g^{\downarrow} = g^{\downarrow}f^{\downarrow}$. In $\mathbf{Par}$, this falls out of the fact that restriction maps do not modify their arguments, and it doesnβt matter if $f$ diverges first or $g$ 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^{\downarrow})^{\downarrow} = g^{\downarrow}f^{\downarrow}$. This axiom holds in the $\mathbf{Par}$, as $(gf^{\downarrow})^{\downarrow}(x)$ ignores the action of $g$ on $x$, and focuses only on its termination.

field β-smashr : β {x y z} β (f : Hom x z) (g : Hom x y) β (g β f β) β β‘ g β β f β

- $f^{\downarrow} g = g (f g)^{\downarrow}$. This is the trickiest of the bunch to understand in $\mathbf{Par}$. Note that if we postcompose $g$ with a domain map $f^{\downarrow}$, then we still need to take into account the action of $g$; furthermore, its domain of definition needs to be restricted to image of $g$.

field β-swap : β {x y z} β (f : Hom y z) (g : Hom x y) β f β β g β‘ g β (f β g) β

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!β©οΈ