Partial Combinatory Algebra

A partial combinatory algebra is a Partial Applicative System $(A,\cdot)$ equipped with a function $\langle-\rangle:\mathsf{Term}_{A}(n+1)\to\mathsf{Term}_{A}(n)$ called bracket abstraction such that:

• $\llbracket{\langle e\rangle}\rrbracket\;\rho\downarrow$
• $\llbracket{\langle e\cdot x\rangle}\rrbracket\;\rho=\llbracket{e[x]}\rrbracket\;\rho$

Where $\llbracket{e}\rrbracket\;\rho$ denotes the interpretation of a term with $n$ variables as a Partial Element of $A$, and $e[x]$ denotes substitution of the final variable of $e$ with $x$.

Note that this presentation of PCAs is different from the one often found in the literature, which encodes a sort of simultaneous bracket abstraction.

The bracket abstraction operation axiomatizes the S-M-N Theorem for $A$, which essentially lets us form Closures.