# reperiendi

## Reflective calculi

Posted in Category theory, Programming by Mike Stay on 2013 May 15

This is mostly for my own benefit.

We start with some term-generating functor $T(G, X)$ parametric in a set of ground terms $G$ and a set of names $X$.

Now specialize to a single ground term:

$T_2(X) = T(1, X)$

Now mod out by structural equivalence:

$T_3(X) = T_2(X) / \equiv$

Let $N$ be a set of names and let M be the set of name-equivalence classes $N / \equiv_N$ (where $\equiv_N$ is yet to be defined—it’s part of the theory of names in which we’re still parametric).

Prequoting and predereference are an algebra and coalgebra of $T_3$, respectively:

$PQ: T_3(M) \to M$

$PD: M \to T_3(M)$

such that

$PD \circ PQ: T_3(M) \to T_3(M) = 1_{T_3(M)}.$

Real quoting and dereference have to use $T_4(X)$, defined below.

Define $N = \mu X.T_2(X)$. Does $N / \equiv = \mu X.T_3(X)$? I think so; assuming it does, define

$M = \mu X.T_3(X)$

so name equivalence is structural equivalence; equivalence of prequoted predereferences is automatic by the definition above.

The fixed point gives us an isomorphism

$F: T_3(M) \to M.$

We can define $PQ = F, PD = F^{-1}$, because undecidability doesn’t come into play until we add operational semantics. It’s decidable whether two terms are structurally equivalent. Thus

$PD \circ PQ:T_3(M) \to T_3(M)$

is the identity, satisfying the condition, and

$PQ \circ PD: M \to M$

When we mod out by operational semantics (following the traditional approach rather than the 2-categorical one needed for pi calculus):

$T_4(X) = T_3(X) / \beta,$

we have the quotient map

$q_X: T_3(X) \to T_4(X)$

and a map

$r_X: T_4(X) \to T_3(X)$

that picks a representative from the equivalence class.

It’s undecidable whether two terms are in the same operational equivalence class, so $q_X$ may not halt. However, it’s true by construction that

$q_X \circ r_X: T_4(X) \to T_4(X)$

is the identity.

We can extend prequoting and predereference to quoting and dereference on $T_4$ by

$Q: T_4(M) \stackrel{r_M}{\to} T_3(M) \stackrel{PQ}{\to} M$

$D: M \stackrel{PD}{\to} T_3(M) \stackrel{q_M}{\to} T_4(M)$

and then

$D \circ Q$

$= T_4(M) \stackrel{r_M}{\to} T_3(M) \stackrel{PQ}{\to} M \stackrel{PD}{\to} T_3(M) \stackrel{q_M}{\to} T_4(M)$

$= T_4(M) \stackrel{r_M}{\to} T_3(M) \stackrel{q_M}{\to} T_4(M)$

$= T_4(M) \stackrel{id}{\to} T_4(M)$

which is what we want for quoting and dereference. The other way around involves undecidability.