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βB$
with total functions
$Aβ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βB$
as total functions from a subobject
$Xβͺ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,$ the category of sets and partial functions. The key insight is that every partial function $f:AβB$ is defined on some domain $XβA;$ this yields a partial function $fβ:AβA$ that maps $x$ to itself iff $f(x)$ is defined. We can generalize this insight to an arbitrary category $C$ by equipping $C$ with an operation $(β)_{β}:C(x,y)β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 $(β)_{β}$ satisfies 4 axioms: - $ff_{β}=f.$ In $Par,$ this corresponds to the fact that $f_{β}(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_{β}g_{β}=g_{β}f_{β}.$ In $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_{β})_{β}=g_{β}f_{β}.$ This axiom holds in the $Par,$ as $(gf_{β})_{β}(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_{β}g=g(fg)_{β}.$ This is the trickiest of the bunch to understand in $Par.$ Note that if we postcompose $g$ with a domain map $f_{β},$ 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!β©οΈ