🌐 한국어로 읽기

Background for chapter 01.

Lambda calculus and SKI combinators

This is the theory Lam.hs and eval.c are built on, told through the actual first-commit code rather than abstractly. If you've never seen lambda calculus or combinators before, this is the whole prerequisite.

1. Exp: an AST for lambda calculus, plus three pragmatic extras

ccb31388:Lam.hs (lines 44–51):

data Exp
  = Var Ident
  | App Exp Exp
  | Lam Ident Exp
  | Int Integer
  | Comb String
  | Prim String
  deriving (Show, Eq)

Var, App, Lam are the three term formers of the lambda calculus, verbatim: a variable reference, a function application, and a variable-binding abstraction (Lam "x" e is \x. e). Everything you can build in the pure lambda calculus is one of these three.

The other three constructors are not lambda calculus — they're what a compiler needs to be useful. Int is a machine integer literal, so arithmetic doesn't have to be Church-encoded. Prim names a built-in operation like "+" or "-" that eval.c implements natively. Comb names a combinator constant (S, K, I, ...) — these are what compile introduces; see bracket-abstraction.md. (The file also defines pattern synonyms like App2, CI, CK — those are just readability sugar over these six constructors, not new syntax.)

2. Beta reduction, on paper

ccb31388:Lam.hs (lines 36–39):

e1 :: Exp
e1 = Lam "x" $ App2 (Prim "+") (Var "x") (Var "x")
e2 :: Exp
e2 = Lam "x" $ Lam "y" $ App2 (Prim "-") (Var "y") (Var "x")

putStrLn (toString e1) prints (\x. + x x) and putStrLn (toString e2) prints (\x. (\y. - y x)) (checked in ghci). The one computation rule of lambda calculus is beta reduction: applying a lambda to an argument substitutes the argument for the bound variable throughout the body.

(\x. + x x) 5  -->  [x := 5](+ x x)  =  + 5 5  -->  10

That's ordinary math, not a code claim. Here's the code claim, machine verified: does Lam.hs's own reduce function actually perform this step?

ghci> pp (reduce (App e1 (Int 5)))
(\x. + x x) 5

It does not reduce — the term comes back unchanged. reduce/redOne (lines 137–161) pattern-match on combinators (CI, CK, CS, ...) and on Prim applications; there is no case for Lam or for "apply a Lam to an argument." Beta reduction on raw Var/Lam terms is simply not implemented anywhere in this file. That's the subject of the next section.

3. Why variables are a problem for a machine

To implement beta reduction directly, an interpreter needs to substitute into a term while avoiding variable capture — if you naively substitute y for x in \y. x, the x you're replacing must not be captured by the enclosing \y, so a correct substitution has to rename bound variables on the fly. The usual production fix is to not substitute at all: keep the term as-is and carry an environment (a map from names to values/closures) that grows every time you enter a Lam.

eval.c's node representation has no such thing:

typedef struct node {
  enum node_mark mark;
  enum node_tag tag;
  union {
    value_t value;
    struct {
      struct node *fun;
      struct node *arg;
    } s;
  } u;
} node;

A node is a tag plus either a value or a (fun, arg) pair — nothing that looks like an environment or a closure (there is no env/closure field anywhere in the 539-line file). eval.c's reduction loop (the eval function, see section 5) never needs to look up a variable by name, because by the time a term reaches eval.c it doesn't have any variables left. That transformation — eliminating Var/Lam entirely before runtime — is exactly what compile in Lam.hs does, and it's called bracket abstraction (see the companion doc).

4. S, K, I

Three combinators are enough to express any closed lambda term:

Each rule is a pure graph rewrite: match the shape on the left, produce the shape on the right. No name lookup, no substitution, no capture to worry about — because there are no names. That's the punchline: a term built only from S, K, I, primitives, and applications can be executed by a machine that just pattern-matches on node shape, which is exactly what eval.c's eval loop does.

Concretely, compare section 2's failure to the compiled version:

ghci> pp (reduce (App (compile e1) (Int 5)))
10

compile e1 turns \x. + x x into S (S (K +) I) I (see bracket-abstraction.md for the derivation) — a term with no Var/Lam in it — and that term, reduce handles fine.

5. The extended set: B, C, S', C', B', T, Y

S/K/I are enough in principle, but S-only translations blow up in size (see the companion doc). Lam.hs and eval.c share a larger combinator set. Here is the reduction switch, trimmed to the combinator cases (ccb31388:eval.c, from the eval function, lines 380–474; each ... marks elided stack-bookkeeping lines — CHECK/GCCHECK guards, f/g/x/k argument fetches, and POP/TOP adjustments — and the unreachable break; after each GOTO is also omitted):

    case S:
      ...
      FUN(n) = new_ap(f, x);
      ARG(n) = new_ap(g, x);
      GOTO ap;
    case SS:
      ...
      FUN(n) = new_ap(k, new_ap(f, x));
      ARG(n) = new_ap(g, x);
      GOTO ap;
    case K:
      ...
      SETIND(n, x);
      GOTO ind;
    case T:
      ...
      x = ARG(TOP(2));
      ...
      SETIND(n, x);
      GOTO ind;
    case I:
      ...
      SETIND(n, x);
      GOTO ind;
    case Y:
      ...
      FUN(n) = f;
      ARG(n) = n;
      GOTO ap;
    case B:
      ...
      FUN(n) = f;
      ARG(n) = new_ap(g, x);
      GOTO ap;
    case C:
      ...
      FUN(n) = new_ap(f, x);
      ARG(n) = g;
      GOTO ap;
    case CC:
      ...
      FUN(n) = new_ap(k, new_ap(f, x));
      ARG(n) = g;
      GOTO ap;

(pretty(), lines 288–316, prints tag SS as S', BB as B', and CC as C' — the enum names and the source-language names don't match, which is worth knowing before you go looking for a case S' that doesn't exist.) Lam.hs's own reference reducer, redOne (lines 147–161; the trailing primitive-arithmetic case and the Nothing catch-all are elided, marked ...), states the same rules purely in terms of Exp:

redOne :: Exp -> Maybe Exp
redOne (App CI x) = Just x
redOne (App (App CK x) _) = Just x
redOne (App (App CT _) x) = Just x
redOne (App3 CS f g x) = Just $ App (App f x) (App g x)
redOne (App3 CB f g x) = Just $ App      f    (App g x)
redOne (App3 CC f g x) = Just $ App (App f x)      g
redOne (App4 CS' k f g x) = Just $ App2 k (App f x) (App g x)
redOne (App4 CB' k f g x) = Just $ App2 k      f    (App g x)
redOne (App4 CC' k f g x) = Just $ App2 k (App f x)      g
...

One rule per combinator, all machine-checked against the running code (reduce in Lam.hs, and the real eval binary compiled from eval.c):

One real discrepancy worth flagging, since this doc's rule is "verify, don't assume": B' (BB in the enum) is declared in eval.c's node_tag enum, has parser support ('B' followed by '), and has a pretty() case — but the eval switch has no case BB:. Feeding eval.c a term that needs to reduce a B' node crashes it:

$ ./eval test_bprime.comb      # ((((B' -) 10) I) 3)
((((B' -) 10) I) 3)
bad tag 12
ERR: eval tag

(Tag 12 is BB — count the enum node_tag list: FREE=0, IND=1, AP=2, INT=3, S=4, K=5, I=6, B=7, C=8, T=9, Y=10, SS=11, BB=12, ....) Lam.hs's own redOne does implement B', so the two files disagree here — a small, genuine gap in the very first commit, not a mistake in this doc. As the companion doc shows, it happens not to matter in practice: B' is never actually produced by compile/improve in this commit.

Next: bracket-abstraction.md — how compile turns Var/Lam terms into exactly these combinators.