🌐 Read in English

1장의 배경지식.

브래킷 추상화

lambda-calculus-and-ski.md에서 eval.c는 오직 컴비네이터 항만 실행할 수 있다는 것을 확인했다 — Var도 Lam도 없이. 브래킷 추상화는 하나에서 다른 하나로 가는 알고리즘이다: Lam x body가 주어지면, 자유 변수 x가 없는 컴비네이터 식 E를 만들어내는데, 이 E는 어떤 인자에 적용하든 body에서 x가 그 인자에 속박되었을 때와 똑같이 동작한다. 이를 안쪽에서 바깥쪽으로 재귀적으로 수행하면 항 안의 모든 Lam이 변수 하나씩 사라진다.

1. compile과 abstract

ccb31388:Lam.hs, 92–101행, 전문 인용 (두 함수를 합쳐 열 줄):

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은 항을 순회하며 App으로 재귀하고, Lam x a를 만나면 abstract x a에게 넘긴다 — "a에서 x를 제거하라." compile e = e는 Var/Int/Comb/Prim을 커버한다: 뿌리에 App/Lam이 없는 항에는 더 할 일이 없다.

abstract x e는 정확히 네 개의 방정식으로 이루어져 있으며, 각각이 표준 브래킷 추상화 규칙이다:

  • abstract x (Var y) | x == y = CI — x 자신에서 x를 추상화하면 항등원이 나온다: (\x. x) = I.
  • abstract x (App f a) = App2 CS (abstract x f) (abstract x a) — 적용에서 x를 추상화하려면, 양쪽 모두에서 x를 추상화한 뒤 S로 이어 붙인다. S는 정확히 "두 갈래 모두를 같은 인자에 적용"하는 것이기 때문이다: 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 — 중첩된 Lam은 안쪽에서 바깥쪽으로 추상화한다: 먼저 안쪽 속박 변수 y를 (재귀적으로) 제거하고, 나온 결과를 단순화한 다음(improveC, 3절), 그다음 그것에서 x를 제거한다.
  • abstract x e = App CK e (나머지 모든 경우: e가 y /= x인 Var y이거나 Int/Comb/Prim인 경우) — x가 e에 자유 변수로 아예 나타나지 않으므로, 결과는 무엇에 적용되든 무시하고 항상 e를 내놓아야 한다: 그것이 바로 K e다, K e y = e이므로.

이 네 방정식을 합치면 abstract가 Var x를 결코 남기지 않는다는 것에 대한 완전하고 기계적인 증명이 된다: 모든 경우가 x를 직접 대체하거나(CI), 엄밀히 더 작은 부분항으로 재귀하거나(App, Lam), x가 거기 없으므로 제거한다(App CK e).

2. 예시 추적: compile e1

e1 = Lam "x" $ App2 (Prim "+") (Var "x") (Var "x"), 즉 \x. + x x다. compile e1 = abstract "x" (App (App (Prim "+") (Var "x")) (Var "x"))이다. App 방정식을 적용한 뒤 양쪽으로 재귀하면:

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

기계로 검증 (nix develop $MICROHS -c ghci Lam.hs 실행 후 pp (compile e1)):

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

손으로 계산한 것과 정확히 일치한다. 그리고 실제로 실행된다: reduce (App (compile e1) (Int 5))는 10을 내놓는다, ghci에서 확인했다 — 컴비네이터 형태가 \x. + x x를 5에 적용했을 때와 똑같이 동작하는 것이다.

3. improve

S (S (K +) I) I는 이미 중복이 있다: S (K f) I는 고전적인 항등식 S (K f) I x = (K f) x (I x) = f (I x) = f x를 만족한다, 즉 S (K f) I와 f는 동일하게 동작한다 — S (K f) I 래퍼는 아무 이득도 없다. improveC(ccb31388:Lam.hs, 106–117행)는 바로 이런 패턴과 비슷한 패턴을 찾아내 없애버린다:

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(104행)다; improveT(119–135행)는 같은 방식으로 한 번 더 훑는다. 그 첫 번째 방정식은 또 하나의, 더 작은 래퍼 제거 규칙이다 (improveC 자신의 사본은 위 115행에서 주석 처리되어 있다 — 이것이 실제로 동작하는 버전이다):

    (CK,                     CI)        -> CT

S/C/B로 둘러싸인 K와 I가 함께 있으면 단일 컴비네이터 T로 뭉쳐진다 (T x y = y, lambda-calculus-and-ski.md 참고). improveT의 나머지 부분은 교환 가능/뒤집기 가능한 프리미티브를 정규형으로 만들어 improveC의 CC 규칙도 적용될 수 있게 하는데 — 여기 전문을 싣지는 않지만, 같은 "패턴을 찾아 재작성한다"는 방식이다.

S (S (K +) I) I에 적용해 보면: 안쪽의 S (K +) I는 (App CS (App CK e1), CI) -> e1에 매치되어 곧바로 +로 뭉쳐진다. 이제 바깥쪽 적용은 App2 CS (Prim "+") CI인데, 이 조각들(App CS (Prim "+"), CI)은 위의 다섯 가지 특수 패턴 중 어느 것에도 매치되지 않으므로 (왼쪽은 App CS (App CK e1)도 App CS (App2 CB e1 e2)도 아니고, 오른쪽은 App CK e2도 아니다), 안쪽 뭉침 외에는 그대로 기본 케이스로 떨어져 S + I가 된다. 기계로 검증:

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

다섯 개 대신 세 개의 컴비네이터가 되었고, reduce (App (improve (compile e1)) (Int 5))는 여전히 10을 낸다.

4. 왜 이게 중요한가: S만 쓰는 순진한 변환은 폭발한다

순수한 S/K/I 브래킷 추상화 규칙(abstract의 네 방정식, CS/CK/CI만 사용)만으로도 그 자체로 충분하다 — App/Lam 방정식이 종료하는 데 improveC가 필요한 것은 전혀 아니다. 하지만 Lam 하나를 추상화할 때마다 그 본문 전체를 또 한 겹의 S로 감싸게 되고, 중첩된 Lam은 이를 곱해서 늘린다: abstract x (Lam y e)는 먼저 e에서 y를 완전히 추상화하고(e 크기만 한 S/K/I 항이 된다), 그다음 그 항 전체 에서 x를 추상화한다 — 그래서 k겹 중첩된 람다는 컴비네이터 개수를 k에 대해 지수적으로 부풀릴 수 있다. 구체적으로, abstract의 App 케이스에서 App2 CS (abstract x f) (abstract x a)는, x가 f나 a에 전혀 나타나지 않을 때조차 x의 최종 인자가 될 것을 S마다 한 번씩 중복시킨다 (이것이 정확히 위에서 improveC가 청소하고 있는 S (K _) I/S (K _) e 낭비다).

improveC의 추가 컴비네이터들은 표준적인 키셀료프(Kiselyov) 방식의 해법이다:

  • B f g x = f (g x) — x가 두 번째 인자에만 나타날 때 쓰인다 (왼쪽이 App CK e1이고 오른쪽이 사소하지 않은 경우): 한쪽 갈래만 x를 쓸 때는 S가 x를 양쪽 갈래에 중복시킬 필요가 없다.
  • C f g x = f x g — 거울상 경우: x가 첫 번째 인자에만 나타난다.
  • S' k f g x = k (f x) (g x)와 C' k f g x = k (f x) g — 이들은 S-노드의 왼쪽이 그 자체로 B-컴비네이터 적용일 때 발생한다 (App CS (App2 CB e1 e2) e3 / App CC (App2 CB e1 e2) e3): S 안에 B를 쌓는 대신, 합성과 분기를 한 축약 단계에서 함께 하는 컴비네이터 하나로 융합한다.

각 재작성은 중복된 S/K/I 래퍼를 아예 없애거나, 두 컴비네이터 적용을 하나로 합친다. 그래서 출력은 중첩 깊이에 따라 커지는 대신 줄어든다. 확장 집합의 구성원 중 하나는 눈에 띄게 빠져 있다: abstract, improveC, improveT 어디에서도 B'(B' k f g x = k f (g x))를 만들어내지 않는다 — 파일 전체에서 CB'가 언급되는 곳은 패턴 동의어 선언(62행과 70행)과 redOne 축약 케이스(155행)뿐이다. 그래서 이 커밋에서는 B'가 컴파일된 출력에 결코 나타날 수 없고, 이것이 eval.c 스위치문에서 case BB:가 빠져 있는 것(짝을 이루는 문서의 5절 참고)이 눈에 띄지 않는 이유다. 장난감이 아닌 실제 예시: 이 커밋의 nfib 함수(Lam.hs의 225행, eNfib)는 comp = improve . compile . toLam을 통해 다음으로 컴파일된다 (./eval nfib.comb에서):

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

— B, C, S', C'로 빽빽하고, 벌거벗은 S/K/I 없이 쓰인 S는 단 두 곳뿐이다. 세 개의 변수(nfib, n, 그리고 암묵적인 재귀 인자)가 여러 번 참조되는 함수치고는 그렇다. improve가 없었다면, 그 참조 하나 하나가 별도의 S (K _) _ 래퍼 비용을 치렀을 것이다.

5. 이해도 확인

e3 = Lam "x" $ Lam "y" $ Var "y", 즉 \x. \y. y — 첫 번째 인자를 무시하는 함수다. 아무것도 실행하기 전에, 1절의 abstract의 네 방정식을 이용해 compile e3를 예측해 보자. 그다음 improve가 그 답에 어떤 일을 하는지 예측해 보자 (힌트: 3절의 (CK, CI) -> CT 규칙). 그리고 직접 확인해 보자:

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

기계로 검증된 정답 (예측하기 전에는 들여다보지 말 것): compile e3는 K I이고, improve (compile e3)는 T다 — 두 인자를 받아 "두 번째 인자를 돌려주는" 컴비네이터, T x y = y인데, lambda-calculus-and-ski.md에서 이미 다뤘다. 이 일치(improveC에서 주석 처리된 115행의 (CK, CI) -> CT 규칙은 죽어 있지만, improveT의 122행에 있는 살아 있는 (CK, CI) -> CT 규칙이 이를 잡아낸다) 자체가, abstract + improve가 \x. \y. y를 그 동작을 하는 가장 단순한 컴비네이터로 실제로 뭉쳐낸다는 작은 확인이다.