Contents

dankogai/swift-combinators

Combinator calculus in Swift — the SKI combinator calculus, Curry's BCKW system, Barker's Iota and Jot, the [one-point basis](

Synopsis

import Combinators

let x = Term.variable("x"), y = Term.variable("y")

// The three primitives:  I x → x,  K x y → x,  S x y z → x z (y z)
try Term.i(x).normalize()        // x
try Term.k(x, y).normalize()     // x
try Term("SKK")(x).normalize()   // x — SKK behaves like I

// Terms parse from the classic notation (string literals too):
let flip: Term = "S(K(SI))K"
try flip(x, y).normalize()       // yx

// Lambdas are eliminated into S, K and I by bracket abstraction:
let three = try Term(parsing: #"\fx.f(f(fx))"#)
three.naturalValue()             // 3

// Church arithmetic:
Term.add(.church(2), .church(3)).naturalValue()       // 5
Term.multiply(.church(2), .church(3)).naturalValue()  // 6

// Reduction is normal-order and bounded; Ω = SII(SII) has no normal form:
try Term.omega.normalize()       // throws ReductionError.stepLimitExceeded

// Watch a reduction, step by step:
for step in Term("SKKx").reductions { print(step) }
// SKKx
// Kx(Kx)
// x

BCKW

B, C and W are primitives too — B x y z → x (y z), C x y z → x z y, W x y → x y y — so terms may mix both bases freely, and either basis can be targeted or eliminated:

// Bracket abstraction into Curry's basis instead of Schönfinkel's:
try Term(parsing: #"\xy.yx"#, basis: .bckw)   // C(WK), pure BCKW
Term.lambda("f", "x", body: .variable("f")(x, x), in: .bckw)   // W

// Rewrite a term into a single basis:
Term.b.rewritten(in: .ski)    // S(KS)K
Term.s.rewritten(in: .bckw)   // B(BW)(BBC)
Term.i.rewritten(in: .bckw)   // WK

Term("B(SW)x").rewritten(in: .ski).isExpressed(in: .ski)   // true

Iota and Jot

ι is a primitive too, with the rule ι x → x S K; the whole calculus folds into it (I = ιι, K = ι(ι(ιι)), S = ι(ι(ι(ιι)))):

// Barker's Iota language: i (or ι) and prefix application *FG
try Term(iota: "*i*i*ii")     // ι(ι(ιι)), which behaves like K
Term.k.iotaEncoding           // "*i*i*ii"
Term.s.rewritten(in: .iota)   // ι(ι(ι(ιι)))

// Jot: every string of 0s and 1s is a program —
// [] = I, [F0] = FSK, [F1] = λxy.F(xy)
try Term(jot: "11100")        // behaves like K
try Term(jot: "11111000")     // behaves like S
Term.s.jotEncoding            // "11111000" — a Gödel numbering of all terms

Both encoders return nil for terms with free variables, which the languages cannot express. (Note that iota terms rarely stay iota-pure under reduction: ι's own rule reintroduces S and K.)

The X combinator

Another one-point basis, with an even tidier bootstrap than ι's: X a → a K S K, so the whole calculus falls out of self-application — exactly, not merely extensionally:

try Term("XXX").normalize()     // K — literally the primitive
try Term("X(XX)").normalize()   // S
Term.k.rewritten(in: .x)        // XXX
Term.s.rewritten(in: .x)        // X(XX)
try Term(parsing: #"\xy.yx"#, basis: .x).isExpressed(in: .x)   // true

The λ-calculus front-end

Lambda keeps its abstractions instead of eliminating them: named binders, normal-order β-reduction with capture-avoiding substitution, α-equivalence, and conversions to and from combinators in either direction:

let two: Lambda = "λfx.f(fx)"
two.naturalValue()                          // 2
try Lambda("(λxy.xy)y").normalize()         // λy′.y y′ — capture avoided
try Lambda("(λx.xx)(λx.xx)").normalize()    // throws: Ω has no β-normal form

// λ → combinators (any basis), and combinators → λ:
Lambda("λxy.yx").combinator(in: .bckw)      // C(WK)
try Lambda(Term("S(KS)K")).normalize().alphaNormalized()   // λabc.a(bc)

// α-equivalence and canonical renaming:
Lambda("λx.x").isAlphaEquivalent(to: "λy.y")   // true
Lambda("λx y′.y′x").alphaNormalized()          // λab.ba

In the REPL, :lam β-reduces a pure λ-term (-v shows every step) and :to lambda decompiles a combinator term back into a tidy λ-normal form:

ski> :lam (λxy.xy)y
λy′.y y′
ski> :to lambda J
λabcd.ab(adc)

The aviary

Every bird from To Mock a Mockingbird, each built by the book's own construction and named on Term:

Term.thrush              // CI       — T a b → b a
Term.robin               // BBT      — R a b c → b c a
Term.jay                 // B(BC)(W(BC(B(BBB)))) — J a b c d → a b (a d c)
Term.turingBird          // LO       — U a b → b (a a b)
Term.theta               // UU       — Turing's sage bird, Θ a → a (Θ a)

// The book's famous puzzle: a robin composed with itself thrice is a cardinal.
try Term.robin(.robin, .robin, x, y, z).normalize()   // xzy — behaves like C

Term.aviary lists all 46 by name, and the REPL's :birds prints them; D E G H J L O Q R U V come predefined (M the mockingbird and Y the sage were already there). Every bird's law is verified in the test suite.

The REPL

swift run ski                # interactive
swift run ski 'SKKx'         # one-shot
swift run ski -v 'SKKx'      # …showing every step
ski> :v S(K(SI))Kxy
  S(K(SI))Kxy
  K(SI)x(Kx)y
  SI(Kx)y
  Iy(Kxy)
  y(Kxy)
  yx
yx
ski> \fx.f(fx)
S(S(KS)K)(S(S(KS)K)(KI))    -- 2
ski> :let A = \mnfx.mf(nfx)
ski> A23
S(S(KS)(S(KK)(S(S(KS)K)I)))(S(S(KS)K)(S(S(KS)K)I))    -- 5

The REPL predefines M Y, the booleans T F, and the digits 0–9 as Church numerals; S K I B C W are the primitives. :basis bckw switches which basis lambdas are eliminated into, and :to <basis> <expr> rewrites a term into a basis:

ski> :basis bckw
ski> \xy.yx
C(WK)
ski> :to bckw S
B(BW)(BBC)
ski> :iota *i*i*ii
K    -- true
ski> :jot 11111000
S
ski> :jot S(K(SI))K
11111110001111001111110001111111000111001110011100

:iota and :jot evaluate a program in those languages, or — given an ordinary expression — encode it into one.

:help lists the commands.

What's inside

  • Term — an indirect enum over the primitives S K I B C W ι X, free

variables and application, with parsing ("S(K(SI))K", λ-syntax) and minimal-parenthesis printing.

  • Normal-order (leftmost-outermost) reduction: reduced(), the lazy

reductions sequence, and bounded normalize(maxSteps:) — total, because terms like Ω never terminate.

  • Bracket abstraction (Term.lambda/Term.abstract) with the η-rule, into

either basis: the classic SKI translation or Curry's BCKW one.

  • Basis — .ski, .bckw, .iota and the one-point .x, with

rewritten(in:) to translate any term into a single basis and isExpressed(in:) to check membership.

  • Iota and Jot codecs — Term(iota:)/iotaEncoding for the *FG prefix

language and Term(jot:)/jotEncoding for the binary Gödel numbering.

  • A prelude: M, Y, Church booleans, numerals and pairs, plus decoders

(booleanValue(), naturalValue()) to read results back.

  • The aviary — all 46 birds of To Mock a Mockingbird as named terms, from

bluebird to theta, each obeying its law under test.

  • Lambda — the untyped λ-calculus with named binders: normal-order

β-reduction with capture-avoiding substitution, α-equivalence and canonical renaming, plus Lambda(term) / combinator(in:) to move between the λ-world and any combinator basis.

Requirements

Swift 6.0 or later.

swift build
swift test

License

MIT. Copyright (c) 2026 Dan Kogai.

Package Metadata

Repository: dankogai/swift-combinators

Default branch: main

README: README.md