SKI 콤비네이터 계산기

dev/lambda-calculus-reducer가 다루는 람다대수는 변수·람다·적용으로 이루어져 있어, 축소할 때마다 변수 이름이 우연히 겹쳐 포획당하는 문제(알파 변환)를 신경 써야 합니다. SKI 콤비네이터 계산법은 변수 자체가 없는 형식체계입니다 — S·K·I 세 콤비네이터와 그 적용만으로 이루어져 있어 이 문제가 원천적으로 사라집니다.

딱 세 개입니다. I x → x, K x y → x, S x y z → x z (y z). 이 세 규칙만 반복 적용하면 어떤 항도 더 이상 줄지 않는 정규형(또는 영원히 줄지 않는 항)에 이릅니다.

S K K x를 규칙대로 축소하면 K x (K x) → x가 되어, 결국 아무 x에 대해서나 I x와 똑같이 x를 돌려줍니다. 즉 콤비네이터 I 없이 S와 K만으로도 I와 똑같이 동작하는 항을 만들 수 있다는, 손으로 검산할 수 있는 유명한 사실입니다.

모든 람다식은 브라켓 추상화라는 표준 절차로 SKI 항으로 다시 쓸 수 있다는 것이 증명돼 있습니다(S=λx.λy.λz.xz(yz), K=λx.λy.x, I=λx.x). 이 계산기는 입력한 SKI 항을 이 대응으로 람다식으로 바꿔 dev/lambda-calculus-reducer와 같은 축소기로 돌린 결과와, SKI 규칙으로 먼저 정규형까지 줄인 뒤 같은 방식으로 바꿔 돌린 결과를 대조해 검산합니다.

람다대수에서는 (λx.λy.x) y처럼 치환할 값의 자유변수가 몸통의 묶인 변수와 이름이 겹치면 포획이 일어나 틀린 결과가 나올 수 있어, 항상 알파 변환을 신경 써야 합니다. SKI에는 애초에 이름이 없으니 이 문제 자체가 생기지 않습니다 — 대신 항이 훨씬 길어지고 사람이 읽기 어려워진다는 대가가 있습니다.