Combinatory logic for linear λ-calculus

The source code is available on github.

Combinators

• $\mathbf{I}X⊳X$
• $\mathbf{B}XYZ⊳X(YZ)$
• $\mathbf{C}XYZ⊳XZY$

Abstractions

• $[x].x\equiv \mathbf{I}$
• $[x].UV=\mathbf{C}([x].U)V\text{ if }x\in FV(U),x\notin FV(V)$
• $[x].UV=\mathbf{B}U([x].V)\text{ if }x\notin FV(U),x\in FV(V)$

$\mathbf{I}$-axiom

• $\mathbf{B}(\mathbf{BI})\mathbf{I}=\mathbf{I}\text{i.e.}[x].\mathbf{BI}x=[x].x$

Why ?

$$\begin{array}{rlrl}[v].X& =[v].\mathbf{I}U& & \\ & =\mathbf{BI}([v].U)& & \text{def of abstractions}\\ & =([x].\mathbf{BI}x)([v].U)& & \text{eval th (todo)}\\ & =([x].x)([v].U)& & \text{I-axiom}\\ & =[v].U=[v].Y& & \text{eval th (todo)}\end{array}$$

$\mathbf{B}$-axioms

1. $$\begin{gathered} \mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{B}(\mathbf{BC})(\mathbf{C}(\mathbf{BB}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})\mathbf{I})))\mathbf{I}))))\mathbf{I}=\mathbf{C}(\mathbf{BB}(\mathbf{BB}(\mathbf{BCI})))(\mathbf{C}(\mathbf{BBI})\mathbf{I}) \\ \text{i.e.}[x,V,Z].\mathbf{C}(\mathbf{C}(\mathbf{BB}x)V)Z=[x,V,Z].\mathbf{C}x(VZ) \end{gathered}$$
2. $$\begin{gathered} \mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{B}(\mathbf{BC})(\mathbf{B}(\mathbf{C}(\mathbf{BB}(\mathbf{BBI})))\mathbf{I}))))\mathbf{I}=\mathbf{B}(\mathbf{C}(\mathbf{BB}(\mathbf{BBI})))(\mathbf{C}(\mathbf{BB}(\mathbf{BCI}))\mathbf{I}) \\ \text{i.e.}[x,U,Z].\mathbf{C}(\mathbf{B}(\mathbf{B}U)x)Z=[x,U,Z].\mathbf{B}U(\mathbf{C}xZ) \end{gathered}$$
3. $$\begin{gathered} \mathbf{B}(\mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{C}(\mathbf{BB}(\mathbf{BBI}))\mathbf{I}))))\mathbf{I}=\mathbf{B}(\mathbf{C}(\mathbf{BB}(\mathbf{BBI})))(\mathbf{B}(\mathbf{C}(\mathbf{BBI}))\mathbf{I}) \\ \text{i.e.}[x,U,V].\mathbf{B}(\mathbf{B}UV)x=[x,U,V].\mathbf{B}U(\mathbf{B}Vx) \end{gathered}$$

Why ? Here, we have $X=Y$ with $X=\mathbf{B}UVZ$ and $Y=U(VZ)$. We want to show that $[v].X=[v].Y$. Let’s detail the first case, where $v\in FV(U)$ and $v\notin FV(V)$ nor $v\notin FV(Z)$.

$$\begin{array}{rlrl}[v].X& =[v].\mathbf{B}UVZ& & \\ & =\mathbf{C}([v].\mathbf{B}UV)Z& & \text{abstraction def (denoted by ad later on)}\\ & =\mathbf{C}(\mathbf{C}([v].\mathbf{B}U)V)Z& & \text{ad}\\ & =\mathbf{C}(\mathbf{C}(\mathbf{BB}([v].U))V)Z& & \text{ad}\\ & =([x,y,t].\mathbf{C}(\mathbf{C}(\mathbf{BB}x)y)t)([v].U)VZ& & \text{eval th (todo)}\\ & =([x,y,t].\mathbf{C}x(yt))([v].U)VZ& & \mathbf{B}\text{-axiom 1}\\ & =\mathbf{C}([v].U)(VZ)& & \text{eval th (todo)}\\ & =[v].U(VZ)=[v].Y& & \text{ad}\end{array}$$

Similar reasonings can be made to find the other axioms.

$\mathbf{C}$-axioms

1. $$\begin{gathered} \mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{B}(\mathbf{BC})(\mathbf{C}(\mathbf{BB}(\mathbf{BC}(\mathbf{B}(\mathbf{BC})\mathbf{I})))\mathbf{I}))))\mathbf{I}=\mathbf{C}(\mathbf{BB}(\mathbf{BC}(\mathbf{B}(\mathbf{BC})(\mathbf{C}(\mathbf{BB}(\mathbf{BCI}))\mathbf{I}))))\mathbf{I} \\ \text{i.e.}[x,V,Z].\mathbf{C}(\mathbf{C}(\mathbf{BC}x)V)Z=[x,V,Z].\mathbf{C}(\mathbf{C}xZ)V \end{gathered}$$
2. $$\begin{gathered} \mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{B}(\mathbf{BC})(\mathbf{B}(\mathbf{C}(\mathbf{BB}(\mathbf{BCI})))\mathbf{I}))))\mathbf{I}=\mathbf{B}(\mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{C}(\mathbf{BBI})\mathbf{I}))))\mathbf{I} \\ \text{i.e.}[x,U,Z].\mathbf{C}(\mathbf{B}(\mathbf{C}U)x)Z=[x,U,Z].\mathbf{B}(UZ)x \end{gathered}$$
3. $$\begin{gathered} \mathbf{B}(\mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{C}(\mathbf{BB}(\mathbf{BCI}))\mathbf{I}))))\mathbf{I}=\mathbf{C}(\mathbf{BC}(\mathbf{B}(\mathbf{BB})(\mathbf{B}(\mathbf{BC})(\mathbf{B}(\mathbf{C}(\mathbf{BBI}))\mathbf{I}))))\mathbf{I} \\ \text{i.e.}[x,U,V].\mathbf{B}(\mathbf{C}UV)x=[x,U,V].C(\mathbf{B}Ux)V \end{gathered}$$

Similar reasonings to the one above.

$\eta$-axiom

• $\mathbf{C}(\mathbf{BBI})\mathbf{I}=\mathbf{I}\text{i.e.}[u,x].ux=\mathbf{I}$

Justification :

• $\eta$-rule : for all terms $U$, $[x].Ux=U$
• as specified above, the rule is an axiom-scheme representing an infinite number of axioms
• let’s close it, our closed $\eta$-rule is $[u,x].ux=[u].u$
• $[u].u=\mathbf{I}$
• $[u,x].ux=[u].\mathbf{B}u\mathbf{I}=\mathbf{C}(\mathbf{BBI})\mathbf{I}$

Example : deriving $\mathbf{BI}=\mathbf{I}$ from $(\mathbf{I}+\eta )$-axioms

$$\begin{array}{rlrl}\mathbf{C}(\mathbf{BBI})\mathbf{I}(\mathbf{BI})& =\mathbf{I}(\mathbf{BI})& & \text{using }\eta \text{-axiom}\\ & =\mathbf{BI}& & \text{on one hand}\\ & =\mathbf{BBI}(\mathbf{BI})\mathbf{I}& & \text{on the other hand, applying }\mathbf{C}\\ & =\mathbf{B}(\mathbf{I}(\mathbf{BI}))\mathbf{I}& & \text{applying }\mathbf{B}\\ & =\mathbf{B}(\mathbf{BI})\mathbf{I}& & \text{applying }\mathbf{I}\\ & =\mathbf{I}& & \text{using }\mathbf{I}\text{-axiom}\\ \text{Thus }\mathbf{BI}& =\mathbf{I}& & \end{array}$$