🌐 Read in English

1장의 배경지식.

람다 대수와 SKI 컴비네이터

이 글은 Lam.hs와 eval.c가 기반하는 이론을, 추상적으로가 아니라 실제 첫 커밋 코드를 통해 설명한다. 람다 대수나 컴비네이터를 한 번도 본 적이 없다면, 이 글이 필요한 사전 지식의 전부다.

1. Exp: 람다 대수를 위한 AST, 그리고 실용적인 확장 세 가지

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

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

Var, App, Lam은 람다 대수의 세 가지 항 구성자를 그대로 옮긴 것이다: 변수 참조, 함수 적용, 그리고 변수를 속박하는 추상화(Lam "x" e는 \x. e)다. 순수 람다 대수에서 만들 수 있는 모든 것은 이 셋 중 하나다.

나머지 세 생성자는 람다 대수가 아니다 — 컴파일러가 쓸모 있으려면 필요한 것들이다. Int는 기계 정수 리터럴이라, 산술 연산을 처치 인코딩(Church encoding)으로 표현하지 않아도 된다. Prim은 eval.c가 네이티브로 구현하는 "+"나 "-" 같은 내장 연산의 이름이다. Comb은 컴비네이터 상수(S, K, I, ...)의 이름인데 — 이들은 compile이 도입하는 것들이다; bracket-abstraction.md를 보라. (이 파일은 App2, CI, CK 같은 패턴 동의어도 정의하는데, 이는 이 여섯 생성자 위에 가독성을 위해 얹은 설탕일 뿐, 새로운 문법이 아니다.)

2. 종이 위의 베타 축약

ccb31388:Lam.hs (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)은 (\x. + x x)를 출력하고, putStrLn (toString e2)는 (\x. (\y. - y x))를 출력한다 (ghci에서 확인). 람다 대수의 유일한 계산 규칙은 베타 축약이다: 람다를 인자에 적용하면 본문 전체에서 속박 변수를 그 인자로 치환한다.

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

이건 그냥 수학일 뿐, 코드에 대한 주장이 아니다. 다음은 코드에 대한 주장이며 기계로 검증한 것이다: Lam.hs 자체의 reduce 함수가 실제로 이 단계를 수행하는가?

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

축약되지 않는다 — 항이 그대로 돌아온다. reduce/redOne(137–161행)은 컴비네이터(CI, CK, CS, ...)와 Prim 적용에 대해서만 패턴 매칭한다; Lam에 대한 케이스도, "Lam을 인자에 적용"하는 케이스도 없다. 순수한 Var/Lam 항에 대한 베타 축약은 이 파일 어디에도 구현되어 있지 않다. 그것이 다음 절의 주제다.

3. 왜 변수는 기계에게 문제가 되는가

베타 축약을 직접 구현하려면 인터프리터는 변수 포획을 피하면서 항 안으로 치환해야 한다 — \y. x에서 x를 y로 순진하게 치환하면, 치환 대상인 x가 바깥의 \y에 포획되어서는 안 되므로, 올바른 치환은 그때그때 속박 변수의 이름을 바꿔줘야 한다. 실전에서 흔히 쓰는 해결책은 아예 치환을 하지 않는 것이다: 항을 그대로 두고, Lam에 들어갈 때마다 커지는 환경(이름을 값/클로저에 대응시키는 맵)을 따로 들고 다닌다.

eval.c의 노드 표현에는 그런 것이 없다:

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;

노드는 태그 하나와, 값 또는 (fun, arg) 쌍 중 하나로 이루어진다 — 환경이나 클로저처럼 보이는 것은 전혀 없다 (539행짜리 파일 어디에도 env/closure 필드가 없다). eval.c의 축약 루프(eval 함수, 5절 참고)는 이름으로 변수를 찾아볼 필요가 전혀 없는데, 항이 eval.c에 도달할 때쯤이면 이미 변수가 하나도 남아 있지 않기 때문이다. 그 변환 — 런타임 이전에 Var/Lam을 완전히 제거하는 것 — 이 바로 Lam.hs의 compile이 하는 일이며, 이를 브래킷 추상화라 부른다 (짝을 이루는 문서 참고).

4. S, K, I

세 개의 컴비네이터만으로 닫힌 람다 항은 모두 표현할 수 있다:

각 규칙은 순수한 그래프 재작성이다: 왼쪽 모양에 맞으면 오른쪽 모양을 만들어낸다. 이름 조회도, 치환도, 걱정할 포획도 없다 — 애초에 이름이 없기 때문이다. 이것이 핵심이다: S, K, I, 프리미티브, 적용만으로 이루어진 항은 노드 모양을 패턴 매칭하기만 하는 기계로 실행할 수 있으며, 이것이 정확히 eval.c의 eval 루프가 하는 일이다.

구체적으로, 2절에서 실패했던 사례를 컴파일된 버전과 비교해 본다:

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

compile e1은 \x. + x x를 S (S (K +) I) I로 바꾸는데 (유도 과정은 bracket-abstraction.md 참고) — 이 항에는 Var/Lam이 전혀 없다 — 그리고 이 항은 reduce가 문제없이 처리한다.

5. 확장 집합: B, C, S', C', B', T, Y

S/K/I만으로 원리상 충분하지만, S만 쓰는 변환은 크기가 폭발적으로 커진다 (짝을 이루는 문서 참고). Lam.hs와 eval.c는 이보다 더 큰 컴비네이터 집합을 공유한다. 다음은 컴비네이터 케이스만 추려낸 축약 스위치문이다 (ccb31388:eval.c, eval 함수, 380–474행; 각 ...는 생략된 스택 관리 코드를 나타낸다 — CHECK/GCCHECK 가드, f/g/x/k 인자 가져오기, POP/TOP 조정 — 그리고 각 GOTO 뒤에 나오는 도달 불가능한 break;도 생략했다):

    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(), 288–316행은 태그 SS를 S'로, BB를 B'로, CC를 C'로 출력한다 — enum 이름과 소스 언어상의 이름이 서로 다르다는 점은, 존재하지도 않는 case S'를 찾아 헤매기 전에 알아두면 좋다.) Lam.hs 자체의 참조 축약기 redOne(147–161행; 마지막의 프리미티브 산술 케이스와 Nothing catch-all은 생략했으며 ...로 표시)은 같은 규칙을 순전히 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
...

컴비네이터마다 규칙이 하나씩 있으며, 모두 실제로 동작하는 코드(Lam.hs의 reduce, 그리고 eval.c를 컴파일한 실제 eval 바이너리)에 대해 기계로 검증했다:

이 글의 원칙이 "가정하지 말고 검증하라"인 만큼, 짚고 넘어갈 만한 진짜 불일치가 하나 있다: B'(enum상 BB)는 eval.c의 node_tag enum에 선언되어 있고, 파서 지원도 있으며('B' 뒤에 '), pretty() 케이스도 있다 — 그러나 eval 스위치문에는 case BB:가 없다. B' 노드를 축약해야 하는 항을 eval.c에 넣으면 죽어버린다:

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

(태그 12가 BB다 — enum node_tag 목록을 세어보라: 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 자체의 redOne은 B'를 실제로 구현하고 있으니, 두 파일이 여기서 서로 어긋난다 — 첫 커밋에 있는 작지만 진짜인 틈이지, 이 글의 실수가 아니다. 짝을 이루는 문서에서 보이듯, 실제로는 문제가 되지 않는다: 이 커밋에서 compile/improve는 B'를 결코 만들어내지 않기 때문이다.

다음: bracket-abstraction.md — compile이 Var/Lam 항을 정확히 이 컴비네이터들로 바꾸는 방법.