🌐 한국어로 읽기

Background for chapter 01.

Bracket abstraction

lambda-calculus-and-ski.md established that eval.c can only run combinator terms — no Var, no Lam. Bracket abstraction is the algorithm that gets you from one to the other: given Lam x body, it produces a combinator expression E with no free x such that E applied to any argument behaves like body did with x bound to that argument. Do this recursively from the inside out and every Lam in a term disappears, variable by variable.

1. compile and abstract

ccb31388:Lam.hs, lines 92–101, quoted whole (both functions together are ten lines):

compile :: Exp -> Exp
compile (App f a) = App (compile f) (compile a)
compile (Lam x a) = abstract x a
compile e = e

abstract :: Ident -> Exp -> Exp
abstract x e@(Var y) | x == y = CI
abstract x (App f a) = App2 CS (abstract x f) (abstract x a)
abstract x (Lam y e) = abstract x $ improveC $ abstract y e
abstract x e = App CK e

compile walks the term recursing into App and, on hitting a Lam x a, hands off to abstract x a — "eliminate x from a." compile e = e covers Var/Int/Comb/Prim: nothing left to do to a term with no App/Lam at its root.

abstract x e has exactly four equations, and each one is a standard bracket-abstraction rule:

• abstract x (Var y) | x == y = CI — abstracting x out of x itself gives the identity: (\x. x) = I.
• abstract x (App f a) = App2 CS (abstract x f) (abstract x a) — to abstract x out of an application, abstract it out of both sides and glue them with S, since S is exactly "apply both branches to the same argument": S (abstract x f) (abstract x a) y = (abstract x f) y ((abstract x a) y).
• abstract x (Lam y e) = abstract x $ improveC $ abstract y e — a nested Lam is abstracted from the inside out: first eliminate the inner bound variable y (recursively), simplify what comes out (improveC, section 3), then eliminate x from that.
• abstract x e = App CK e (the catch-all: e is Var y with y /= x, or Int/Comb/Prim) — x doesn't occur free in e at all, so the result must ignore whatever it's applied to and always yield e: that's K e, since K e y = e.

Together these four equations are a complete, mechanical proof that abstract never leaves a Var x behind: every case either replaces x directly (CI), or recurses into strictly smaller subterms (App, Lam), or removes x because it isn't there (App CK e).

2. Worked trace: compile e1

e1 = Lam "x" $ App2 (Prim "+") (Var "x") (Var "x"), i.e. \x. + x x. compile e1 = abstract "x" (App (App (Prim "+") (Var "x")) (Var "x")). Applying the App equation, then recursing into both sides:

abstract x (App (Prim "+") (Var "x"))
  = App2 CS (abstract x (Prim "+")) (abstract x (Var "x"))
  = App2 CS (App CK (Prim "+"))     CI
  = S (K +) I

abstract x (Var "x") = CI

compile e1 = App2 CS (S (K +) I) CI = S (S (K +) I) I

Machine-verified (nix develop $MICROHS -c ghci Lam.hs, then pp (compile e1)):

ghci> pp (compile e1)
S (S (K +) I) I

matches the hand trace exactly. And it runs: reduce (App (compile e1) (Int 5)) gives 10, confirmed in ghci — the combinator form does what \x. + x x applied to 5 should.

3. improve

S (S (K +) I) I is already redundant: S (K f) I is the classic identity S (K f) I x = (K f) x (I x) = f (I x) = f x, i.e. S (K f) I and f behave identically — the S (K f) I wrapper buys nothing. improveC (ccb31388:Lam.hs, lines 106–117) spots exactly this and similar patterns and rewrites them away:

improveC :: Exp -> Exp
improveC (App f a) =
  case (improveC f, improveC a) of
    (App CS (App CK e1),     App CK e2) -> improve (App CK (App e1 e2))
    (App CS (App CK e1),     CI)        -> e1
    (App CS (App CK e1),     e2)        -> improve (App2 CB e1 e2)
    (App CS         e1,      App CK e2) -> improve (App2 CC e1 e2)
    (App CS (App2 CB e1 e2), e3)        -> improve (App3 CS' e1 e2 e3)
    (App CC (App2 CB e1 e2), e3)        -> improve (App3 CC' e1 e2 e3)
--    (CK,                     CI)        -> CT
    (e1,                     e2)        -> App e1 e2
improveC e = e

improve = improveT . improveC (line 104); improveT (lines 119–135) does one more pass in the same style. Its first equation is a second, smaller wrapper-removal rule (improveC's own copy of it, at line 115 above, is commented out — this is the live version):

    (CK,                     CI)        -> CT

K and I glued together by an enclosing S/C/B collapse to the single combinator T (T x y = y, from lambda-calculus-and-ski.md). The rest of improveT canonicalizes commutative/flippable primitives so improveC's CC-rules apply to them too — not shown here in full, but the same "spot a pattern, rewrite it" style.

Applied to S (S (K +) I) I: the inner S (K +) I matches (App CS (App CK e1), CI) -> e1 and collapses straight to +. The outer application is now App2 CS (Prim "+") CI, whose pieces (App CS (Prim "+"), CI) don't match any of the five special patterns above (the left side isn't App CS (App CK e1) or App CS (App2 CB e1 e2), and the right side isn't App CK e2), so it falls through to the default case unchanged apart from the inner collapse, giving S + I. Machine-verified:

ghci> pp (improve (compile e1))
S + I

Three combinators instead of five, and reduce (App (improve (compile e1)) (Int 5)) still gives 10.

4. Why this matters: naive S-only translation explodes

The plain S/K/I bracket-abstraction rules (abstract's four equations, using only CS/CK/CI) are enough on their own — the App/Lam equations never need improveC to terminate. But every Lam you abstract wraps its whole body in another layer of Ss, and nested Lams multiply that: abstract x (Lam y e) first fully abstracts y out of e (an S/K/I term the size of e), and then abstracts x out of that whole term — so k nested lambdas can blow the combinator count up exponentially in k. Concretely, in abstract's own App case, App2 CS (abstract x f) (abstract x a) duplicates every occurrence of x's eventual argument once per S, even when x doesn't occur in f or a at all (that's exactly the S (K _) I/S (K _) e waste improveC is cleaning up above).

improveC's extra combinators are the standard Kiselyov-style fix:

• B f g x = f (g x) — used when x occurs only in the second argument (App CK e1 on the left with a non-trivial right side): no need for S to duplicate x into both branches when only one branch uses it.
• C f g x = f x g — the mirror case: x occurs only in the first argument.
• S' k f g x = k (f x) (g x) and C' k f g x = k (f x) g — these arise when the left side of an S-node is itself a B-combinator application (App CS (App2 CB e1 e2) e3 / App CC (App2 CB e1 e2) e3): instead of stacking a B inside an S, fuse them into one combinator that does the composition and the branching in a single reduction step.

Each rewrite either removes a redundant S/K/I wrapper outright or merges two combinator applications into one, so the output shrinks instead of growing with nesting depth. One member of the extended set is notably absent: nothing in abstract, improveC, or improveT ever constructs B' (B' k f g x = k f (g x)) — the only mentions of CB' in the whole file are its pattern-synonym declaration (lines 62 and 70) and its redOne reduction case (line 155). So in this commit B' can never appear in compiled output, which is why the missing case BB: in eval.c's switch (see the companion doc's section 5) goes unnoticed. A real, non-toy example: this commit's nfib function (eNfib, line 225 of Lam.hs) compiles via comp = improve . compile . toLam to (from ./eval nfib.comb):

((Y (((C' C) ((B (S (> 2))) (((C' (C' +)) (((S' (S' +)) ((C B) (-' 1))) ((C B) (-' 2)))) 1))) 1)) 35)

— dense with B, C, S', C', and only two bare S/K/I-free uses of S, for a function with three variables (nfib, n, and the implicit recursion argument) referenced many times. Without improve, every one of those references would cost a separate S (K _) _ wrapper.

5. Check your understanding

e3 = Lam "x" $ Lam "y" $ Var "y", i.e. \x. \y. y — a function that ignores its first argument. Before running anything, use abstract's four equations from section 1 to predict compile e3, then predict what improve does to your answer (hint: section 3's (CK, CI) -> CT rule). Then check yourself:

nix develop $MICROHS -c ghci Lam.hs
ghci> pp (compile e3)
ghci> pp (improve (compile e3))

Machine-verified expected answers (do not peek until you've predicted): compile e3 is K I, and improve (compile e3) is T — the two-argument "return the second argument" combinator, T x y = y, which lambda-calculus-and-ski.md already covered. That match (improveC's commented-out (CK, CI) -> CT rule at line 115 is dead in improveC, but the live (CK, CI) -> CT rule in improveT, line 122, catches it) is itself a small confirmation that abstract + improve really do collapse \x. \y. y down to the simplest combinator that has that behavior.