Abstract rewriting systems are frequently viewed through the lens of operational semantics—a set of terms governed by directed reduction relations. However, when implementing translations between heterogeneous calculi, such as compiling the Lambda calculus into SKI combinators, one is forced to reconcile this purely behavioral view with a rigid, algebraic one.
While sketching out some ideas recently, I architected a formal, type-safe Scala 3 framework that cleanly decouples term syntax (topology), semantic reduction (axioms), and evaluation strategies (traversal).
Here is an overview of the implementation and the mathematical justification behind it.
To prevent the normalization engine from being tightly coupled to
specific ASTs, the evaluation strategy is abstracted using a
Leibniz typeclass.
The traversal mechanism mathematically mimics the Leibniz product
rule for derivation: \((fg)' = f'g +
fg'\). Just as differentiation distributes across a product,
our Derivation engine visits each subterm of a composite
structure to propagate state changes.
// 1. Rewriting
trait ReWriting[T]:
def step(term: T): Option[T]
// Bounded iteration to prevent Turing divergence.
@annotation.tailrec
final def normalize(x: Option[T], depth: Int = 1000): Option[T] =
if depth < 1 then None
else x.flatMap(step) match
case Some(next) => normalize(Some(next), depth - 1)
case None => x
// 2. Leibniz structures
trait Leibniz[T]:
def derive(term: T, d: T => Option[T]): Option[T]
object Derivation:
def apply[T](base: ReWriting[T])(using topology: Leibniz[T]): ReWriting[T] =
new ReWriting[T]:
def step(term: T): Option[T] =
base.step(term).orElse(topology.derive(term, step))By passing Leibniz as a given topology, we elevate a
localized “head” rewriting rule into a deep structural derivation.
For pure combinatory logic systems like SKI and Iota, the syntactic
structures strictly utilize binary application. Topologically, these can
be elegantly modeled as a FreeMagma.
enum FreeMagma[A]:
case Gen(a: A)
case App(left: FreeMagma[A], right: FreeMagma[A])
given [A]: Leibniz[FreeMagma[A]] with
def derive(term: FreeMagma[A], d: FreeMagma[A] => Option[FreeMagma[A]]): Option[FreeMagma[A]] =
term match
case FreeMagma.App(l, r) => d(l).map(FreeMagma.App(_, r)).orElse(d(r).map(FreeMagma.App(l, _)))
case FreeMagma.Gen(_) => NoneWith the topology defined, we can now explicitly declare the alphabets and semantic reduction axioms for both the SKI and Iota calculi:
// SKI Calculus Implementation
enum SKIAlphabet:
case S, K, I
object SKIAxioms extends ReWriting[FreeMagma[SKIAlphabet]]:
import FreeMagma.{App, Gen}
import SKIAlphabet.*
val s = Gen(S); val k = Gen(K); val i = Gen(I)
def step(term: FreeMagma[SKIAlphabet]): Option[FreeMagma[SKIAlphabet]] = term match
case App(`i`, x) => Some(x)
case App(App(`k`, x), _) => Some(x)
case App(App(App(`s`, x), y), z) => Some(App(App(x, z), App(y, z)))
case _ => None
val SKICalculus = Derivation(SKIAxioms)
// Iota Calculus Implementation
enum IotaAlphabet:
case Iota
object IotaAxioms extends ReWriting[FreeMagma[IotaAlphabet]]:
import FreeMagma.{App, Gen}
import IotaAlphabet.Iota
val i = Gen(Iota)
val k_iota = App(i, App(i, App(i, i)))
val s_iota = App(i, App(i, App(i, App(i, i))))
def step(term: FreeMagma[IotaAlphabet]): Option[FreeMagma[IotaAlphabet]] = term match
case App(`i`, x) => Some(App(App(x, s_iota), k_iota))
case _ => None
val IotaCalculus = Derivation(IotaAxioms)Because the primitive SKI combinators are terminal, evaluation relies
entirely on pattern matching their geometric arrangement. Iota is
particularly interesting here; while SKI primitives terminate cleanly,
Iota’s localized relation \(\iota x \to x
\iota_{S} \iota_{K}\) inherently triggers massive macro
expansions. These infinite expansions are handled safely by conflating
undefined inputs with fuel exhaustion in our bounded
normalize iteration.
Unlike SKI, the Lambda calculus introduces a unary geometry: the
variable binder. To ensure type safety and eliminate alpha-equivalence
complexities, the calculus uses a De Bruijn encoding with
Var, Abs, and App
constructors.
To power the evaluation, we define core substitution mechanics and wrap them in the standard \(\beta\)-reduction axioms:
enum Lambda:
case Var(index: Int)
case Abs(body: Lambda)
case App(left: Lambda, right: Lambda)
given Leibniz[Lambda] with
def derive(term: Lambda, d: Lambda => Option[Lambda]): Option[Lambda] =
term match
case Lambda.App(l, r) => d(l).map(Lambda.App(_, r)).orElse(d(r).map(Lambda.App(l, _)))
case Lambda.Abs(body) => d(body).map(Lambda.Abs(_))
case Lambda.Var(_) => None
object LambdaCore:
import Lambda.*
def shift(term: Lambda, d: Int, c: Int = 0): Lambda = term match
case Var(k) => if k < c then Var(k) else Var(k + d)
case Abs(body) => Abs(shift(body, d, c + 1))
case App(l, r) => App(shift(l, d, c), shift(r, d, c))
def subst(term: Lambda, j: Int, sub: Lambda): Lambda = term match
case Var(k) =>
if k == j then sub
else if k > j then Var(k - 1)
else Var(k)
case Abs(body) => Abs(subst(body, j + 1, shift(sub, 1)))
case App(l, r) => App(subst(l, j, sub), subst(r, j, sub))
object LambdaAxioms extends ReWriting[Lambda]:
import Lambda.*
def step(term: Lambda): Option[Lambda] = term match
case App(Abs(body), arg) => Some(LambdaCore.subst(body, 0, arg))
case _ => None
val LambdaCalculus = Derivation(LambdaAxioms)This is where the theoretical friction usually occurs. If we treat the calculus strictly as an Abstract Rewriting System (ARS), a translation must only preserve the reduction relation: \(x \to_{\Lambda}^* y \implies h(x) \to_{SKI}^* h(y)\).
However, compiling compositionally requires structural recursion, forcing us into the realm of Universal Algebra. To bridge the differing arities—Lambda’s unary abstraction node versus SKI’s pure binary application—we must abandon a strict \(\Sigma\)-algebra homomorphism. Instead, we conceptualize the mappings as morphisms of Lawvere theories (or operads).
Bracket Abstraction does exactly this. It maps the structural arity-1 node into a dynamically generated, derived polynomial operation within the SKI magma.
def freeMagmaHom[A, B](f: A => FreeMagma[B]): FreeMagma[A] => FreeMagma[B] =
def go(t: FreeMagma[A]): FreeMagma[B] = t match
case FreeMagma.Gen(a) => f(a)
case FreeMagma.App(l, r) => FreeMagma.App(go(l), go(r))
go
val IotaToSKI: FreeMagma[IotaAlphabet] => FreeMagma[SKIAlphabet] =
import SKIAxioms.{s, k, i}
import FreeMagma.App
freeMagmaHom {
case IotaAlphabet.Iota => App(App(s, App(App(s, i), App(k, s))), App(k, k))
}In the quotient partial-algebra defined by normal order reduction, these syntactical translations resolve back into strict, elegant homomorphisms.
To prove the architecture is sound, we must test both the internal coherence of each calculus and the structural preservation of the homomorphisms. The suite verifies that when projected down into the quotient space via normal order reduction, the strict semantic mappings hold true.
We assert that \(I x \to x\) and that \(S K K x\) semantically evaluates to \(x\) (acting as \(I\)).
import SKIAxioms.{s, k, i}
import FreeMagma.App
assert(SKICalculus.normalize(Some(App(i, k))) == Some(k), "Identity failed")
assert(SKICalculus.normalize(Some(App(App(k, i), s))) == Some(i), "Constant K failed")
val skk_x = App(App(App(s, k), k), i)
assert(SKICalculus.normalize(Some(skk_x)) == Some(i), "S K K != I equivalence failed")1. Testing SKI Calculus...
✓ SKI tests passed.
Because pure Iota diverges rapidly on macro expansion, we test its head evaluation and explicitly check that infinite combinatorial structures correctly exhaust the normalizer’s fuel limit.
import IotaAxioms.{i as iota, s_iota, k_iota}
import FreeMagma.App
val expectedOneStep = App(App(iota, s_iota), k_iota)
assert(IotaCalculus.step(App(iota, iota)) == Some(expectedOneStep), "Iota head evaluation failed")
assert(IotaCalculus.normalize(Some(App(iota, iota)), depth = 50) == None, "Divergence check failed: Fuel was not exhausted")2. Testing Iota Calculus...
✓ Iota tests passed.
We ensure the untyped lambda calculus structural evaluation accurately resolves the Identity function and Church encodings for booleans.
import Lambda.*
val id = Abs(Var(0))
assert(LambdaCalculus.normalize(Some(App(id, id))) == Some(id), "Lambda Identity failed")
val churchTrue = Abs(Abs(Var(1)))
val termA = Var(10)
val termB = Var(20)
val trueApp = App(App(churchTrue, termA), termB)
assert(LambdaCalculus.normalize(Some(trueApp)) == Some(termA), "Church Boolean TRUE failed")
val churchFalse = Abs(Abs(Var(0)))
val falseApp = App(App(churchFalse, termA), termB)
assert(LambdaCalculus.normalize(Some(falseApp)) == Some(termB), "Church Boolean FALSE failed")3. Testing Lambda Calculus (De Bruijn)...
✓ Lambda tests passed.
Barker’s \(\iota\) behaves semantically as \(\lambda x.\ x S K\). We verify that the encoded translation dynamically maps evaluation to the equivalent SKI primitives.
import IotaAxioms.i as iota
import SKIAxioms.{s, k, i}
import FreeMagma.App
// (encoded ι) x should reduce to x S K. Test with x = I.
val lhs = SKICalculus.normalize(Some(App(IotaToSKI(iota), i)))
val rhs = SKICalculus.normalize(Some(App(App(i, s), k)))
assert(lhs == rhs, s"IotaToSKI: ι x should reduce to x S K (got $lhs vs $rhs)")4. Testing Iota → SKI translation...
✓ Iota → SKI tests passed.
Because Iota calculus inherently diverges, we test the encoding syntactically rather than semantically, verifying that SKI generators map perfectly to their deep Iota tree equivalents.
import SKIAxioms.{s, k, i}
import IotaAxioms.{s_iota, k_iota}
import FreeMagma.App
assert(SKIToIota(s) == s_iota, "SKIToIota(S) should be Barker's s_iota")
assert(SKIToIota(k) == k_iota, "SKIToIota(K) should be Barker's k_iota")
assert(SKIToIota(i) == App(App(s_iota, k_iota), k_iota), "SKIToIota(I) should be (encoded S) K K")5. Testing SKI → Iota translation...
✓ SKI → Iota tests passed.
This mapping pulls the combinators back into a binding geometry. We test that \(K\) properly drops arguments through \(\beta\)-reduction and that the encoded \(S K K\) operates perfectly as a lambda identity.
import SKIAxioms.{s, k, i}
import FreeMagma.App
val termA = Lambda.Var(10)
val termB = Lambda.Var(20)
// K applied to two arguments β-reduces to the first.
val K_lam = SKIToLambda(k)
val kApp = Lambda.App(Lambda.App(K_lam, termA), termB)
assert(LambdaCalculus.normalize(Some(kApp)) == Some(termA), "SKIToLambda(K) should behave as K")
// SKK applied to any argument β-reduces to that argument (it's I).
val SKK_lam = SKIToLambda(App(App(s, k), k))
val skkApp = Lambda.App(SKK_lam, termA)
assert(LambdaCalculus.normalize(Some(skkApp)) == Some(termA), "SKIToLambda(SKK) should behave as I")6. Testing SKI → Lambda translation...
✓ SKI → Lambda tests passed.
The most mathematically complex mapping is validated by applying translated Church booleans to SKI primitives and observing exact semantic reduction.
import Lambda.{Abs, Var}
import SKIAxioms.{s, k, i}
import FreeMagma.App
// λx. x, translated and applied to K, reduces to K.
val id = Abs(Var(0))
val idSKI = LambdaToSKI(id)
assert(SKICalculus.normalize(Some(App(idSKI, k))) == Some(k), "LambdaToSKI(λx.x) applied to K should be K")
// λx y. x (Church true), translated and applied to S, I, reduces to S.
val churchTrue = Abs(Abs(Var(1)))
val trueSKI = LambdaToSKI(churchTrue)
assert(SKICalculus.normalize(Some(App(App(trueSKI, s), i))) == Some(s), "LambdaToSKI(λxy.x) applied to S, I should be S")
// λx y. y (Church false), translated and applied to S, I, reduces to I.
val churchFalse = Abs(Abs(Var(0)))
val falseSKI = LambdaToSKI(churchFalse)
assert(SKICalculus.normalize(Some(App(App(falseSKI, s), i))) == Some(i), "LambdaToSKI(λxy.y) applied to S, I should be I")7. Testing Lambda → SKI translation...
✓ Lambda → SKI tests passed.