Categorical Realizability

A partial combinatory algebra is a set $\mathcal{A}$ together with a partial operation $\mathcal{A} \times \mathcal{A} \to \mathcal{A}$ , denoted by juxtaposition, $(a,b)\mapsto a\ b$ , such that there exist elements $K$ and $S$ satisfying:

$(K\ a)\ b = a$ for all $a, b \in \mathcal{A}$
$((S\ f)\ g)$ is defined for all $f,g \in\mathcal{A}$ and
$((S\ f)\ g)\ a \cong (f\ a)(g\ a)$ for all $f,g,a \in\mathcal{A}$

$\cong$ here stands for Kleene equality and means: either both sides are undefined, or both are defined and are equal elements of $\mathcal{A}$ .

Example trivial pca [local-0]

The trivial pca is a set $\{ \star \}$ with application map $(\star, \star) \mapsto \star$ . For sure, $K := \star$ and $S := \star$ .

Example untyped $\lambda$ -calculus as pca $\Lambda$ [local-1]

Write $\Lambda$ for closed terms of untyped lambda calculus quotiented by the equivalence relation generated by $\beta$ -reduction. With application of lambda calculus the set $\Lambda$ forms a pca with $K$ and $S$ given by the equivalence classes of $\lambda xy.x$ and $\lambda xyz.(xz)(yz)$ , respectively.

Definition. Partial combinatory algebra (pca) [math-NYGO]

Example trivial pca [local-0]

Example untyped λ\lambdaλ-calculus as pca Λ\LambdaΛ [local-1]

Example untyped $\lambda$ -calculus as pca $\Lambda$ [local-1]