Inceptions

Vikraman Choudhury

[email protected]

MSP, University of Strathclyde, Glasgow, UK

Gregor Feierabend

[email protected]

Computer Lab, University of Cambridge, UK

Marcelo Fiore

[email protected]

Computer Lab, University of Cambridge, UK

Mar 2, 2026

Overview

Examples of Algebraic Theories
- First-order theories
- Exceptions
- State
- Continuations
Substitution as an effect
Generalising Substitution Algebras to Inception Algebras

Groups are Monoids with Inverses

A group is a set $G$ with:

a unit element $e : G$;
and a binary operation $\text{-}\mathbin{\ast}\text{-}: G \times G \to G$,

such that

$\forall x : G,\, e \mathbin{\ast}x = x$ and $x \mathbin{\ast}e = x$;
$\forall x, y, z : G,\, (x \mathbin{\ast}y) \mathbin{\ast}z = x \mathbin{\ast}(y \mathbin{\ast}z)$; and
$\forall x : G,\, \exists y : G,\, x \mathbin{\ast}y = e$ and $y \mathbin{\ast}x = e$.

Groups with Explicit Inverses

A group is a set $G$ with:

a unit element $e : G$;
a binary operation $\text{-}\mathbin{\ast}\text{-}: G \times G \to G$;
and a unary operation ${(\text{-})}^{-1} : G \to G$;

such that:

$\forall x : G,\, e \mathbin{\ast}x = x$ and $x \mathbin{\ast}e = x$;
$\forall x, y, z : G,\, (x \mathbin{\ast}y) \mathbin{\ast}z = x \mathbin{\ast}(y \mathbin{\ast}z)$; and
$\forall x : G,\, x \mathbin{\ast}x^{-1} = e$ and $x^{-1} \mathbin{\ast}x = e$.

This is an equivalent presentation of groups, but as an “algebraic theory”.

Lattices are Posets with Joins and Meets

A lattice is a poset $(L, \leq)$ such that:

$\forall x, y : L,\, \exists \ell : L,\, \forall z : L,\, z \leq \ell \iff z \leq x$ and $z \leq y$; and
$\forall x, y : L,\, \exists u : L,\, \forall z : L,\, u \leq z \iff x \leq z$ and $y \leq z$.

Lower bounds and upper bounds are unique.

We can write $x \wedge y$ and $x \vee y$ for the meet and join of $x$ and $y$.

Lattices with Explicit Joins and Meets

A lattice is a set $L$ with:

a binary operation $\text{-}\wedge\text{-}: L \times L \to L$;
a binary operation $\text{-}\vee\text{-}: L \times L \to L$;

such that

$\forall x, y, z : L,\, (x \wedge y) \wedge z = x \wedge (y \wedge z)$;
$\forall x, y, z : L,\, (x \vee y) \vee z = x \vee (y \vee z)$; and
$\forall x, y : L,\, x \wedge y = y \wedge x$;
$\forall x, y : L,\, x \vee y = y \vee x$; and
$\forall x, y : L,\, x \wedge x = x$; and
$\forall x, y : L,\, x \vee x = x$.

These presentations are equivalent because $a \leq b \iff a \wedge b = a$ and $a \vee b = b$.

Torsion Groups

A torsion group is a group $G$ such that every element has finite order:

$\forall x : G,\, \exists n \geq 1,\, x^n = e$.

This is not an algebraic theory.

We could add $\mathrm{ord} : G \to \mathbb{N}$ such that:

$\forall x : G,\, \mathrm{ord}(x) \geq 1$,
$\forall x : G,\, x^{\mathrm{ord}(x)} = e$.

Every operation should be $G^n \to G$

Natural Deduction

Algebraic operations can be turned into typing rules.

For example, monoids can be written in two different ways:

as an algebraic structure:

$\begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {A^0} \&\& A \&\& {A^2} \arrow["{e}", from=1-1, to=1-3] \arrow["{\mult}"', from=1-5, to=1-3] \end{tikzcd} \qquad\qquad \begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {A\times A\times A} \&\& {A\times A} \\ \\ {A\times A} \&\& A \arrow["{\ast\times{\id}}"', from=1-1, to=3-1] \arrow["{{\id}\times\ast}", from=1-1, to=1-3] \arrow["\ast", from=1-3, to=3-3] \arrow["\ast"', from=3-1, to=3-3] \end{tikzcd} \qquad\qquad \begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {A\times A^0} \&\& {A\times A} \&\& {A^0\times A} \\ \\ \&\& A \arrow["{\id\times e}", from=1-1, to=1-3] \arrow["\cong"', from=1-1, to=3-3] \arrow["\ast"{description}, from=1-3, to=3-3] \arrow["\cong", from=1-5, to=3-3] \arrow["e\times\id"', from=1-5, to=1-3] \end{tikzcd}$

and as natural deduction judgements: \[ {\vdash e} \qquad\qquad {x_1, x_2 \vdash x_1 \mathbin{\ast}x_2} \] \[ x \vdash e \mathbin{\ast}x = x \qquad\qquad x \vdash x \mathbin{\ast}e = x \qquad\qquad x, y, z \vdash (x \mathbin{\ast}y) \mathbin{\ast}z = x \mathbin{\ast}(y \mathbin{\ast}z) \]

Monoid Actions

A (left) monoid action of a monoid $M$ on a set $A$ is:

a two-sorted algebraic operation $\text{-}\mathbin{\triangleright}\text{\rule[.35ex]{4pt}{0.4pt}\kern-4pt\rule[.65ex]{4pt}{0.4pt}}: M \times A \to A$;

such that

$\forall a : A,\, e \mathbin{\triangleright}a = a$; and
$\forall m_1, m_2 : M,\, \forall a : A,\, (m_1 \mathbin{\ast}m_2) \mathbin{\triangleright}a = m_1 \mathbin{\triangleright}(m_2 \mathbin{\triangleright}a)$.

Exceptions

The exception monad for a set of errors $E$: \[T(X)=E+X\]

as an algebraic theory with operations:

$\operatorname{throw}_e:A^0\rightarrow A$

for each error $e:E$, and no equations.

Global State

The state monad for a set of states $S$:

$\begin{tikzcd} {\Set} && {\Set} \arrow[""{name=0, anchor=center, inner sep=0}, "{S\times(-)}", curve={height=-12pt}, from=1-1, to=1-3] \arrow[""{name=1, anchor=center, inner sep=0}, "{(-)^S}", curve={height=-12pt}, from=1-3, to=1-1] \arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=0, to=1] \end{tikzcd}$

\[T(X)=(S\times X)^S\]

The global state monad has $S = V^L$, for countable values $V$ and finite locations $L$:

\[T(X) = (V^L\times X)^{V^L}\]

as an algebraic theory with operations:

Lookup: $\mathrm{lk}_l : X^V \to X$ – read location $l$ and branch on result; and
Update: $\mathrm{upd}_{l,v} : X \to X$ – write $v$ to $l:L$ and continue,

Global State (cont.)

satisfying seven equations:

$\begin{tikzcd}[ampersand replacement=\&, column sep=15mm, row sep=12mm] X^{V \times V} \arrow[r, "\lk_l^V"] \arrow[d, "\Delta_V^*"'] \& X^V \arrow[d, "\lk_l"] \\ X^V \arrow[r, "\lk_l"'] \& X \end{tikzcd} \qquad\qquad \begin{tikzcd}[ampersand replacement=\&, column sep=15mm, row sep=12mm] X \arrow[r, "\upd_{l{,}v}"] \arrow[rd, "\upd_{l{,}w}"'] \& X \arrow[d, "\upd_{l{,}w}"] \\ \& X \end{tikzcd} \qquad\qquad \begin{tikzcd}[ampersand replacement=\&, column sep=15mm, row sep=12mm] X^V \arrow[r, "\lk_l"] \arrow[d, "\mathrm{ev}_v"'] \& X \arrow[d, "\upd_{l{,}v}"] \\ X \arrow[r, "\upd_{l{,}v}"'] \& X \end{tikzcd} \qquad\qquad \begin{tikzcd}[ampersand replacement=\&, column sep=15mm, row sep=12mm] X \arrow[r, "{\langle\upd_{l{,}v}\rangle_v}"] \arrow[rd, "\mathrm{id}"'] \& X^V \arrow[d, "\lk_l"] \\ \& X \end{tikzcd}$

$\begin{tikzcd}[ampersand replacement=\&, column sep=15mm, row sep=12mm] X^{V \times V} \arrow[r, "{(\lk_{l'})^V}"] \arrow[d, "{(\lk_l)^V \circ \sigma}"'] \& X^V \arrow[d, "\lk_l"] \\ X^V \arrow[r, "\lk_{l'}"'] \& X \end{tikzcd} \qquad\qquad \begin{tikzcd}[ampersand replacement=\&, column sep=15mm, row sep=12mm] X \arrow[r, "\upd_{l{,}v}"] \arrow[d, "\upd_{l'{,}w}"'] \& X \arrow[d, "\upd_{l'{,}w}"] \\ X \arrow[r, "\upd_{l{,}v}"'] \& X \end{tikzcd} \qquad\qquad \begin{tikzcd}[ampersand replacement=\&, column sep=15mm, row sep=12mm] X^V \arrow[r, "\lk_l"] \arrow[d, "{\upd_{l'{,}w}^V}"'] \& X \arrow[d, "\upd_{l'{,}w}"] \\ X^V \arrow[r, "\lk_l"'] \& X \end{tikzcd}$

Global State (cont.)

For $L=1$ and $V=2$, the operations are:

$\mathrm{lk}: X^2 \to X$;
$\mathrm{upd}_0 : X \to X$; and
$\mathrm{upd}_1 : X \to X$;

satisfying the equations:

\[ \begin{align*} \text{(LL)} \quad & \mathrm{lk}(\mathrm{lk}(a,b),\, \mathrm{lk}(c,d)) = \mathrm{lk}(a,\, d) \\ \text{(UU)} \quad & \mathrm{upd}_v(\mathrm{upd}_w(x)) = \mathrm{upd}_w(x) \\ \text{(UL)} \quad & \mathrm{upd}_v(\mathrm{lk}(x_0, x_1)) = \mathrm{upd}_v(x_v) \\ \text{(LU)} \quad & \mathrm{lk}(\mathrm{upd}_0(x),\, \mathrm{upd}_1(x)) = x \end{align*} \]

Continuations

The continuation monad for a set of responses $R$ is given by the adjunction

$\begin{tikzcd} {\textbf{Set}^{\op}} && {\textbf{Set}} \arrow[""{name=0, anchor=center, inner sep=0}, "{R^{(-)}}", curve={height=-12pt}, from=1-1, to=1-3] \arrow[""{name=1, anchor=center, inner sep=0}, "{R^{(-)}}", curve={height=-12pt}, from=1-3, to=1-1] \arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=0, to=1] \end{tikzcd}$

\[T_R(X)=R^{R^X}\]

What operations does this monad have?

Control Operators

Control operators allow programs to jump

$\mathcal{C}_{\tau} : 0^{0^\tau} \to \tau$
$\mathcal{C}_{\tau} : \tau^{0^\tau} \to \tau$
$\mathsf{callcc}_{\tau} : \tau^{\neg\tau} \to \tau$
$\mathsf{callCC}_{\tau,\sigma} : \tau^{\tau^\sigma} \to \tau$
$\mathsf{colam}_{\tau,\sigma} : \tau^{\neg\sigma} \to \tau + \sigma$

$\mathcal{A}_{\tau} : 0 \to \tau$
$\mathsf{abort}_{\tau,\sigma} : \tau \times \neg\tau \to \sigma$
$\mathsf{coapp}_{\tau,\sigma} : (\tau + \sigma) \times \neg\sigma \to \tau$

and produce control effects:

$\mathsf{callcc}(\lambda k.\, 3)$ returns $3$;
$\mathsf{callcc}(\lambda k.\, \mathsf{abort}(5, k))$ returns $5$; but
$\mathsf{callcc}(\lambda k.\, 4 + \mathsf{abort}(2, k))$ returns $2$.

Axioms for Control Operators

C-NAT: \[\Gamma, f : \sigma \to \tau \vdash f(\mathcal{C}_\sigma(M)) = \mathcal{C}_\tau(\lambda \kappa : \tau \to 0.\, M(\lambda x : \sigma.\, \kappa(f\, x)))\]
C-APP: \[\Gamma \vdash \mathcal{C}_\sigma(\lambda \kappa : \sigma \to 0.\, \kappa\, M) = M\]
A-ABS: \[\Gamma \vdash V \mathcal{A}_\sigma(M)=_\mathcal{C}\mathcal{A}_\tau(M)\]
A-ID: \[\mathcal{A}_0(M)=\mathcal{C}M\]

Axioms for Control Operators (cont.)

$\mathsf{colam}$-const:

\[\mathsf{colam}(x.M[]) = \mathsf{inr}(M[])\]

$\mathsf{colam}$-pass:

\[\mathsf{colam}\bigl(x.\textsf{let }y=\mathsf{coapp}(\mathsf{inr}(M[]),x)\textsf{ in }N[y]\bigr)=\textsf{let }y=M[]\textsf{ in }N[y]\]

$\mathsf{colam}$-jump:

\[\mathsf{colam}\bigl(x.\textsf{let }y=\mathsf{coapp}(\mathsf{inl}(M[]),x)\textsf{ in }N[y]\bigr)=M[]\]

Axioms for Control Operators (cont.)

$\mathsf{colam}$-$\zeta$:

\[ \mathsf{case}\bigl(\mathsf{colam}(x.V[x])\bigr)\mathsf{of} \begin{cases}\mathsf{inl}(a)\rightarrow M[a]\\\mathsf{inr}(b)\rightarrow N[b]\end{cases} \\\\ \;=\; \\\\ \mathsf{case}\bigl(\mathsf{colam}(x.N\bigl[V[x]\bigr])\bigr)\textsf{of} \begin{cases}\mathsf{inl}(a)\rightarrow M[a]\\\mathsf{inr}(b)\rightarrow b\end{cases} \]

Substitution Algebras

A $V$-substitution algebra is an object $X$ with:

$\operatorname{var}:V\rightarrow X$; and
$\operatorname{sub}:X^V\times X\rightarrow X$;

such that the following axioms hold:

Weakening:

$% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYXjFcXHRpbWVzIFgiXSxbMiwwLCJYXFx0aW1lcyBYIl0sWzIsMiwiWCJdLFswLDIsIlheVlxcdGltZXMgWCJdLFszLDIsIlxcb3BlcmF0b3JuYW1le3N1Yn0iLDJdLFswLDEsIlxcY29uZyJdLFsxLDIsIlxccGlfMSJdLFswLDMsIlheeyFWfVxcdGltZXNcXGlkX1giLDJdXQ== \begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {X^1\times X} \&\& {X\times X} \\ \\ {X^V\times X} \&\& X \arrow["\cong", from=1-1, to=1-3] \arrow["{X^{!V}\times\id_X}"', from=1-1, to=3-1] \arrow["{\pi_1}", from=1-3, to=3-3] \arrow["{\operatorname{sub}}"', from=3-1, to=3-3] \end{tikzcd}$

\[M[N/x]=M,\text{ if }x\notin\operatorname{fv}(M)\]

Substitution:

$% https://q.uiver.app/#q=WzAsMyxbMCwwLCIxXFx0aW1lcyBYIl0sWzIsMiwiWCJdLFswLDIsIlheVlxcdGltZXMgWCJdLFsyLDEsIlxcb3BlcmF0b3JuYW1le3N1Yn0iLDJdLFswLDEsIlxcY29uZyJdLFswLDIsIlxcb3BlcmF0b3JuYW1le3Zhcn1eXFxmbGF0XFx0aW1lczEiLDJdXQ== \begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {1\times X} \&\& \\ \\ {X^V\times X} \&\& X \arrow["{\operatorname{var}^\flat\times\id_X}"', from=1-1, to=3-1] \arrow["\cong", from=1-1, to=3-3] \arrow["{\operatorname{sub}}"', from=3-1, to=3-3] \end{tikzcd}$

\[x[N/x]=N\]

Extensionality:

$% https://q.uiver.app/#q=WzAsMyxbMCwwLCJYXlZcXHRpbWVzIFYiXSxbMiwyLCJYIl0sWzAsMiwiWF5WXFx0aW1lcyBYIl0sWzIsMSwiXFxvcGVyYXRvcm5hbWV7c3VifSIsMl0sWzAsMSwiXFxvcGVyYXRvcm5hbWV7ZXZ9Il0sWzAsMiwiXFxpZF97WF5WfVxcdGltZXNcXG9wZXJhdG9ybmFtZXtzdWJ9XlZcXHRpbWVzXFxpZF9YIiwyXSxbMCwxLCJcXG9wZXJhdG9ybmFtZXtzdWJ9IiwyXSxbMiwxLCJcXG9wZXJhdG9ybmFtZXtzdWJ9Il1d \begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {X^V\times V} \&\& \\ \\ {X^V\times X} \&\& X \arrow["{\id_{X^V}\times\operatorname{var}}"', from=1-1, to=3-1] \arrow["{\operatorname{ev}}", from=1-1, to=3-3] \arrow["{\operatorname{sub}}"', from=3-1, to=3-3] \end{tikzcd}$

\[M[y/x][N/y]=M[N/x]\]

Associativity:

$% https://q.uiver.app/#q=WzAsNSxbMCw0LCJYXlZcXHRpbWVzIFgiXSxbMiw0LCJYIl0sWzIsMiwiWF5WXFx0aW1lcyBYIl0sWzAsMiwiKFheVlxcdGltZXMgWCleVlxcdGltZXMgWCJdLFsxLDAsIihYXlZcXHRpbWVzIFgpXlZcXHRpbWVzKFheVlxcdGltZXMgWCkiXSxbMyw0LCJcXHZhcnRoZXRhIl0sWzQsMiwiXFxvcGVyYXRvcm5hbWV7c3VifV5WXFx0aW1lc1xcb3BlcmF0b3JuYW1le3N1Yn0iXSxbMywwLCJcXG9wZXJhdG9ybmFtZXtzdWJ9XlZcXHRpbWVzXFxpZF9YIiwyXSxbMCwxLCJcXG9wZXJhdG9ybmFtZXtzdWJ9IiwyXSxbMiwxLCJcXG9wZXJhdG9ybmFtZXtzdWJ9Il1d \begin{tikzcd}[ampersand replacement=\&, column sep=12mm, row sep={12mm,between origins}] \& {(X^V\times X)^V\times(X^V\times X)} \& \\ \\ {(X^V\times X)^V\times X} \&\& {X^V\times X} \\ \\ {X^V\times X} \&\& X \arrow["{\operatorname{sub}^V\times\operatorname{sub}}", from=1-2, to=3-3] \arrow["\varphi", from=3-1, to=1-2] \arrow["{\operatorname{sub}^V\times\id_X}"', from=3-1, to=5-1] \arrow["{\operatorname{sub}}", from=3-3, to=5-3] \arrow["{\operatorname{sub}}"', from=5-1, to=5-3] \end{tikzcd}$

where $\varphi$ is the composition:

\[ (X_1^{V_1}\times X_2)^{V_2}\times X_3 \xrightarrow{\operatorname{id}\times\Delta_{X_3}} (X_1^{V_1}\times X_1)^{V_2}\times X_3\times X_3 \] \[ \xrightarrow{\operatorname{id}\times\pi_1^\flat\times\operatorname{id}} (X_1^{V_1}\times X_2)^{V_2}\times X_3^{V_1}\times X_3 \xrightarrow{\cong} (X_1^{V_2}\times X_3)^{V_1}\times(X_2^{V_2}\times X_3) \]

\[ M[N/x][L/y]=M[L/y]\bigl[N[L/y]/x\bigr] \]

Typing rules:

\[\begin{prooftree} \AxiomC{$\Gamma\vdash_v V:\mathbb{V}$} \RightLabel{(\textup{var})} \UnaryInfC{$\Gamma\vdash_c\operatorname{\mathsf{var}}_\tau(V):\tau$} \end{prooftree}\] \[\begin{prooftree} \AxiomC{$\Gamma,a:\mathbb{V}\vdash_c M:\tau$} \AxiomC{$\Gamma\vdash_c N:\tau$} \RightLabel{(\textup{sub})} \BinaryInfC{$\Gamma\vdash_c\operatorname{\mathsf{sub}}(a.M,N):\tau$} \end{prooftree}\]

Equations:

\[ \begin{align*} \operatorname{\mathsf{sub}}(a.M[],N[]) &= M[] & (\textup{weakening}) \\ \operatorname{\mathsf{sub}}(a.\operatorname{\mathsf{var}}_\tau(a), N) &= N & (\textup{substitution}) \\ \operatorname{\mathsf{sub}}(a.M[a], \operatorname{\mathsf{var}}(b)) &= M[b] & (\textup{extensionality}) \\ \operatorname{\mathsf{sub}}(a.\operatorname{\mathsf{sub}}(b.L[a,b],M[a]),N[]) &= \operatorname{\mathsf{sub}}(b.\operatorname{\mathsf{sub}}(a.L[a,b],N[]), \\ & \qquad\qquad \operatorname{\mathsf{sub}}(a.M[a],N[])) & (\textup{associativity}) \end{align*} \]

Algebraicity equations:

$\textsf{let }x=\operatorname{\mathsf{var}}(a)\textsf{ in }P[x]=\operatorname{\mathsf{var}}(a)$;
$\textsf{let }x=\operatorname{\mathsf{sub}}(a,M[a],N[])\textsf{ in }P[x] = \\ \qquad \operatorname{\mathsf{sub}}(a.\textsf{let }x=M[a]\textsf{ in }P[x],\textsf{let }x=N[]\textsf{ in }P[x])$.

Properties

V-substitution algebras are free monoids for the substitution monoidal product in $\mathsf{Set}^{\mathsf{FinSet}}$, with unit $V=y(1)$.
The free substitution algebra monad is on $\mathsf{Set}^{\mathsf{FinSet}}$.
There is a V-substitution algebra structure on $T_V(X)$ – this is the CPS translation.
$\operatorname{\mathsf{var}}: V \to T_V(X)$; and
$\operatorname{\mathsf{sub}}: \\ T_V(X)^V \times T_V(X) \\ \to T_V(1 + X) \times T_V(X) \\ \to T_V((1 + X) \times X) \\ \to T_V(1 \times X + X \times X) \\ \to T_V(X)$.

Inception algebras

A $(V,P)$-inception algebra is an object $X$ with:

$\operatorname{\mathsf{rec}}:V\times P\rightarrow X$; and
$\operatorname{\mathsf{inc}}:X^V\times X^P\rightarrow X$;

such that the following axioms hold:

Weakening:

$\begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {X^1\times X^{P}} \&\& {X\times X^{P}} \\ \\ {X^V\times X^{P}} \&\& X \arrow["\cong", from=1-1, to=1-3] \arrow["{X^{!V}\times\id_{X^{P}}}"', from=1-1, to=3-1] \arrow["{\pi_1}", from=1-3, to=3-3] \arrow["{\inc}"', from=3-1, to=3-3] \end{tikzcd}$

Substitution:

$\begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {P\times X^{P}} \&\& \\ \\ {X^V\times X^{P}} \&\& X \arrow["{\rec^\flat\times\id_{X^{P}}}"', from=1-1, to=3-1] \arrow["{ev}", from=1-1, to=3-3] \arrow["{\inc}"', from=3-1, to=3-3] \end{tikzcd}$

Extensionality:

$\begin{tikzcd}[ampersand replacement=\&, column sep={12mm,between origins}, row sep={12mm,between origins}] {X^V\times V} \&\& \\ \\ {X^V\times X^{P}} \&\& X \arrow["{\id_{X^V}\times\rec^\flat}"', from=1-1, to=3-1] \arrow["{\operatorname{ev}}", from=1-1, to=3-3] \arrow["{\inc}"', from=3-1, to=3-3] \end{tikzcd}$

Associativity:

$\begin{tikzcd}[ampersand replacement=\&, column sep=12mm, row sep={12mm,between origins}] \& {(X^V\times X^{P})^V\times(X^V\times X^{P})^{P}} \& \\ \\ {(X^V\times X^{P})^V\times X^{P}} \&\& {X^V\times X^{P}} \\ \\ {X^V\times X^{P}} \&\& X \arrow["{\inc^V\times\inc^P}", from=1-2, to=3-3] \arrow["\vartheta", from=3-1, to=1-2] \arrow["{\inc^V\times\id_{X^{P}}}"', from=3-1, to=5-1] \arrow["{\inc}", from=3-3, to=5-3] \arrow["{\inc}"', from=5-1, to=5-3] \end{tikzcd}$

where $\vartheta$ is the composition:

\[ (X_1^{V_1}\times X_2^{P_1})^{V_2}\times X_3^{P_2} \xrightarrow{\operatorname{id}\times\Delta_{X_3^{P^2}}} (X_1^{V_1}\times X_2^{P_1})^{V_1}\times X_3^{P_2}\times X_3^{P_2} \] \[ \xrightarrow{\operatorname{id}\times\pi_1^\flat\times\pi_1^\flat} {(X_1^{V_1}\times X_2^{P_1})^{V_2}\times X_1^{P_2\times V_1}\times X_3^{P_2\times P_1}} \xrightarrow{\cong} (X_1^{V_2}\times X_3^{P_2})^{V_1}\times(X_2^{V_2}\times X_3^{P_2})^{P_1} \]

Typing rules:

\[\begin{prooftree} \AxiomC{$\Gamma\vdash_v V:\mathbb{V}$} \AxiomC{$\Gamma\vdash_v P:\mathbb{P}$} \RightLabel{(\textup{rec})} \BinaryInfC{$\Gamma\vdash_c\operatorname{\mathsf{rec}}_\tau(V,P):\tau$} \end{prooftree}\] \[\begin{prooftree} \AxiomC{$\Gamma,a:\mathbb{V}\vdash_c M:\tau$} \AxiomC{$\Gamma,x:\mathbb{P}\vdash_c N:\tau$} \RightLabel{(\textup{inc})} \BinaryInfC{$\Gamma\vdash_c\operatorname{\mathsf{inc}}(a.M,x.N):\tau$} \end{prooftree}\]

Equations:

\[ \begin{align*} \operatorname{\mathsf{inc}}(a.M[],x.N[]) &= M & (\textup{weakening}) \\ \operatorname{\mathsf{inc}}(a.\operatorname{\mathsf{rec}}_\tau(a,P[]),x.N[x]) &= N[P] & (\textup{substitution}) \\ \operatorname{\mathsf{inc}}(a.M[a],x.\operatorname{\mathsf{rec}}(k,x)) &= M[k] & (\textup{extensionality}) \\ \operatorname{\mathsf{inc}}(a.\operatorname{\mathsf{inc}}(b.P[a,b],x.K[a,x]),y.L[y]) &= \operatorname{\mathsf{inc}}(b.\operatorname{\mathsf{inc}}(a.P[a,b],y.L[y]), \\ & \qquad\qquad x.\operatorname{\mathsf{inc}}(a.K[a,x],y.L[y])) & (\textup{associativity}) \end{align*} \]

Algebraicity equations:

$\textsf{let }z=\operatorname{\mathsf{rec}}(a,x)\textsf{ in }P[z]=\operatorname{\mathsf{rec}}(a,x)$;
$\textsf{let }z=\operatorname{\mathsf{inc}}(a,M[a],x.N[x])\textsf{ in }P[z] = \\ \qquad \operatorname{\mathsf{inc}}( a.\textsf{let }z=M[a]\textsf{ in }P[z], x.\textsf{let }z=N[x]\textsf{ in }P[z] )$.

Properties

There is a $(V^P,P)$-inception algebra structure on $T_V(X)$ – this is the CPS translation.
$\operatorname{\mathsf{rec}}: V \times P \to T_V(X)$; and
$\operatorname{\mathsf{inc}}: \\ T_V(X)^{V^P} \times T_V(X)^P \\ \to T_V(P + X) \times T_V(X)^P \\ \to T_V((P + X) \times X^P) \\ \to T_V(P \times X^P + X \times X^P) \\ \to T_V(X)$.

Epilogue

a language for control operations which are second-order algebraic;
$V$ marks code-pointers, and $P$ allows data-passing;
with a CPS translation into the continuation monad;
has an abstract machine via System L (without closures);
and a low-level abstract machine;
formalisation in Agda, implementation in SML/Haskell.

Thank you!