Canonical forms of combinators

Question

Binders are painful when dealing with metatheory. Combinators are one potential approach to avoid the pain of binders. But it'd be nice if I could normalize combinators to canonical forms. Is there something like hereditary substitution and canonical forms for combinators like SKI or BCKW?

The STLC is easy to give canonical forms with a bidirectional style.

Inductive type := pt | fn (_ _: pt).

Inductive var: list type -> type -> Type :=
| Z {G A}: var (A :: G) A
| S {G A B}: var G A -> var (B :: G) A.

Inductive con: list type -> type -> Type :=
| lam {G A B}: con (A :: G) B -> con G (fn A B)
| neu {G}: val G pt -> con G pt
with val: list type -> type -> Type :=
| get {G A}: var G A -> val G A
| app {G A B}: val G (fn A B) -> con G A -> val B.

But I'm not really sure how you'd do the same sort of thing for combinators.

Answer 1

Combinators all have a predefined arity, and normal forms consist of underapplied combinators, whose arguments are normal forms. This is different from lambda calculi, where you also need neutral forms.

Also, this notion of normal form does not agree with observational equality: SKK is normal, but it is observationally equivalent to SKS, which is also normal; but by confluence SKK cannot be equal to SKS via any sequence of reduction/anti-reduction. Formalizing this would again require variables.

Here is my formalization of combinator normalization in Agda. It also adds combinators for natural numbers and recursion, if you should need that.

Combinators inherently cannot deal with variables. So there is only canonicity (i.e. normalization in closed terms), and no analogue of normalization.

---

Here is an approach that is equivalent but more generalizable.

For simply typed combinators with products the situation is different, and indeed it is more like the case in lambda calculus.

First, you consider the free cartesian category $\mathcal A$ generated by the objects of the original cartesian closed category $\mathcal T$. This category encodes the variables and renamings. And since the original category is also cartesian, by freeness we have a functor preserving products $\rho : \mathcal A \to \mathcal T$ that acts as "inclusion" of $\mathcal A$ to $\mathcal T$.

In more concrete terms, you can define the contexts $\mathcal A$ as lists of types (or a binary tree if you prefer binary products) like here, and define reordering on lists as morphisms. Then you can write a functor mapping a list to the product of the list elements, mapping the reorderings to combinators of fst, snd and fanout. In this way you regain the ability to talk about contexts and variables.

Note that for every type with universal property, you can break the property into two parts, one states how to create morphisms into the type, and another states how to create those out from the type. For example, we have the (***) turning two morphisms a -> b and a -> c to a morphism a -> b * c into products, and the two projections out from products. As another example, inl and inr creates morphisms into coproducts, and case out from coproducts.

Therefore you can define neutral and normal terms (they are of type $\mathcal A \to \mathcal T \to \mathsf{Set}$) more or less like in lambda calculus: Neutral forms takes the eliminators, and normal form takes the constructors. In this way every type with universal property is "tore apart" into neutral and normal forms. You can see an example here.

All of this more or less follows the lines of Sterling's thesis, particularly sections 5.5.1 and 5.4.1, just in slightly more concrete terms.

---

Some additional thoughts on this matter:

• Why cartesian? Perhaps the simply typed case is too degenerate for me to see the pattern. Cartesian (i.e. finite product) categories seem to be the "correct" formalization of non-dependent variable structures.
• This is actually where contextual categories are useful. Contextual categories (of the simply typed case) is simply a CCC, but for every object we already chose a split of it into a list. So $[A, B\times C]$ and $[A,B,C]$ are different objects, but are isomorphic in the cartesian closed category. In this case the variable structure is already there, see Astra's work on this.
• Although this looks like combinators, actually it's only the "variable-free" syntax that looks like combinators. I guess you really can't call them that, because we use composition, not application to create bigger terms. It just happens that the composition operation can also be expressed internally in STLC. But generally it need not be so.

Answer 2

Combo does precisely that - if you ask it to. I'll explain how that works.

First, λ-expressions are rendered in combinator form $λx·a = Λx·a$, where $$ Λx·x = I,\quad Λx·a = Ka,\quad Λx·ax = a,\quad Λx·av = Bab,\\ Λx·xx = D,\quad Λx·xb = Tb,\quad Λx·xv = Ub,\\ Λx·ux = Wa,\quad Λx·ub = Cab,\quad Λx·uv = Sab, $$ where $a$, $b$ are combinator terms with no occurrences of $x$ in them, $u$, $v$ are combinator terms each with at least one occurrence of $x$ in them, with $u ≠ x ≠ v$, and $Λx·u = a$ and $Λx·v = b$. This conversion is applied from bottom-up.

Denoting the normal form of a combinator expression $a$ by $[a]$, the following are used: $$ [Ra⋯b] = [Ca⋯b],\quad [xa⋯b] = x[a]⋯[b],\quad [Aa⋯b] = Λy·[Aa⋯by], $$ where $a$, ..., $b$ are combinator expressions, $x$ is a variable, $y$ is an otherwise-unused variable, and $A$ is a combinator followed by fewer arguments $a⋯b$ than it requires for reduction. The last clause is how the η-rule is implemented, if it is requested.

The relation $R → C$ is either a previously-encountered reduction (because no term is ever reduced twice) or else is an instance of one of the forms (assuming the specific instance hasn't yet been encountered): $$ Ix → x,\quad Kxy → x,\quad Txyz → yx,\\ Dx → xx,\quad Wxy → xyy,\quad Uxy → y(xy),\\ Bxyz → x(yz),\quad Cxyz → xzy,\quad Sxyz → xz(yz). $$ For instance, $$\begin{align} [S(Ka)I] &= Λx·[S(Ka)Ix]\\ &= Λx·[Kax(Ix)]\\ &= Λx·[a(Ix)]\\ &= Λx·a[Ix]\\ &= Λx·a[x]\\ &= Λx·ax\\ &= a, \end{align}$$ assuming $a$ is a free variable. Otherwise, more generally $[S(Ka)I] = [a]$.

A pre-condition for this to work consistently is that the abstraction conversion satisfy the property that $Λx·[ax] = [a]$, for all combinator terms $a$, particularly for the cases listed above, e.g. $[Bab] = Λx·[Babx] = Λx·[a(bx)]$, as is the case. At bare minimum, consistency requires that the identities $[S(Ka)I] = [a]$ and $[S(Ka)(Kb)] = [K(ab)]$ be true.

Following the approach by Barendregt, I believe that, in fact, the following $$ SII = D,\quad Λb·SI(Kb) = T,\quad Λb·SIb = U,\\ Λa·S(Ka)I = Λa·a,\quad Λa·Λb·S(Ka)(Kb) = Λa·Λb·K(ab),\\ Λa·Λb·S(Ka)b = B,\quad Λa·SaI = W,\quad Λa·Λb·Sa(Kb) = C, $$ along with $$ Λa·Λx·I(ax) = Λa·Λx·ax,\\ Λa·Λx·D(ax) = Λa·Λx·ax(ax),\\ Λa·Λb·Λx·K(ax)(bx) = Λa·Λb·Λx·ax,\\ Λa·Λb·Λx·T(ax)(bx) = Λa·Λb·Λx·bx(ax),\\ Λa·Λb·Λx·U(ax)(bx) = Λa·Λb·Λx·bx(ax(bx)),\\ Λa·Λb·Λx·W(ax)(bx) = Λa·Λb·Λx·ax(bx)(bx),\\ Λa·Λb·Λc·Λx·B(ax)(bx)(cx) = Λa·Λb·Λc·Λx·ax(bx(cx)),\\ Λa·Λb·Λc·Λx·C(ax)(bx)(cx) = Λa·Λb·Λc·Λx·ax(cx)(bx),\\ Λa·Λb·Λc·Λx·S(ax)(bx)(cx) = Λa·Λb·Λc·Λx·ax(cx)(bx(cx)), $$ should suffice as an equational axiomatization of the η-rule.

As yet, there is no co-inductive step, so if Combo encounters a reduction of the form $[a] = φ([a])$, where $φ(\_)$ is a context in some combinator expression, it will just simply stop and block the reduction ... because nothing is ever reduced twice. The correct way to proceed is to fold it into an infinitary λ-expression and re-write $a$ as $x: a$, and reduce $[a] = x:φ(x)$, where the occurrence of $x$ in the context $φ(\_)$ refers to the entire already-reduced expression $[a]$. For instance, $$\begin{align} [S(CBD)f] &= [CBDf(CBDf)]\\ &= [BfD(BfD)]\\ &= [f(D(BfD))]\\ &= [f(BfD(BfD))]\\ &= f[BfD(BfD)]\\ &= x:fx, \end{align}$$ assuming that $f$ is a free variable. This stands for the term $f(f(f(⋯)))$.

In particular, the normal form for $Y = S(CBD)$ would be $$\begin{align} [Y] &= [S(CBD)]\\ &= Λy·[S(CBD)y]\\ &= Λy·x:yx\\ &= Λy·y(x:yx)\\ &= U(Λy·x:yx)\\ &= z:Uz, \end{align}$$ where it applies another co-inductive step even during λ-abstraction, once it encounters $Λy·x$ a second time within its first encounter ... thus reducing $Y$ to $U(U(U(⋯)))$. So, the abstraction algorithm would require a co-induction rule of its own: that if $Λx·a = φ(Λx·a)$, then $Λx·a = z:φ(z)$.

If the co-inductive steps are permitted, the weirdest normal form would be for $Ω ≡ D D$. We have $[Ω] = [D D] = [D D] = x:x$. It loops on itself.