람다 계산(Lambda calculus)

1930년대 초 미국 논리학자 알론조 처치는 함수를 만드는 것과 적용하는 것 두 가지만으로 이루어진 체계를 내놓았습니다. $\lambda x.\,M$은 'x를 받아 M을 돌려주는 함수'이고, $M\,N$은 'M에 N을 넣는다'입니다. 함수에 이름도, 수도, 참·거짓도 따로 없습니다. 계산 규칙은 단 하나, β-축약입니다. $(\lambda x.\,M)\,N$을 만나면 M 안의 x를 모두 N으로 바꿉니다. 예를 들어 $(\lambda x.\,x\,x)\,y$는 $y\,y$가 됩니다. λ 바로 뒤에 적혀 함수의 입력 자리를 가리키는 변수를 묶인 변수라고 하는데, 대입할 때 N 안의 변수가 M 안의 λ에 붙잡히지 않도록 필요하면 묶인 변수⁠(bound variable)⁠의 이름을 바꿉니다(그림에서 ′가 붙는 변수). $(\lambda x.\,\lambda y.\,x)\,y$를 그대로 대입하면 '무엇을 받든 바깥의 y를 돌려주는 함수'여야 할 결과가 $\lambda y.\,y$, 곧 '받은 것을 그대로 돌려주는 함수'로 뜻이 바뀌어 버립니다. 그래서 먼저 안쪽 y를 y′으로 바꿔 $\lambda y'.\,y$를 얻습니다.

수는 '몇 번 되풀이하는가'로 나타냅니다. 처치 수⁠(Church numeral)⁠ n은 함수 f를 받아 x에 n번 적용하는 함수입니다. n = 이면 입니다. 그러면 SUCC = λn.λf.λx.f (n f x)는 '한 번 더', PLUS = λm.λn.λf.λx.m f (n f x)는 'n번 한 뒤 m번 더', TIMES = λm.λn.λf.m (n f)는 'n번 적용하기를 m번 되풀이'입니다. 막대를 세는 1진법⁠(positional notation)⁠과 같아서 큰 수일수록 길어집니다. 실제 계산기는 이진법⁠(binary)⁠을 쓰지만, 원리를 보는 데는 이것으로 충분합니다.

줄일 식은 , 보는 방식은 입니다.

참과 거짓도 함수입니다. TRUE = λa.λb.a는 둘 중 앞의 것을, FALSE = λa.λb.b는 뒤의 것을 고릅니다. 그러면 AND = λp.λq.p q p가 됩니다. p가 참이면 q를 보고, 거짓이면 곧바로 거짓입니다. 불 대수⁠(Boolean algebra)⁠ 전체가 함수만으로 지어지는 셈입니다. 반면 Ω = (λx.x x)(λx.x x)는 한 번 줄이면 자기 자신으로 돌아와 끝나지 않습니다. 이렇게 더 줄일 수 없는 모양(정규형⁠, normal form⁠)이 없는 항도 있고, 주어진 항이 정규형에 닿는지 판정하는 일반적인 방법은 없습니다. 처치는 1936년 이것으로 정지 문제⁠(halting problem)⁠와 같은 종류의 불가능성을 보였습니다. 처치와 그의 제자 J. 바클리 로서가 증명한 처치–로서 정리(1936)에 따르면, 어디부터 줄이든 정규형에 닿기만 하면 그 결과는 (묶인 변수의 이름만 다른 것을 같게 보면) 언제나 같습니다. 줄이는 순서가 결과를 바꾸지는 못하지만, 닿느냐 마느냐는 바꿀 수 있습니다. 가장 바깥·왼쪽부터 줄이는 정규 순서는 정규형이 있으면 반드시 찾아낸다는 것이 알려져 있습니다(표준화⁠(standardization)⁠ 정리).

이름 없는 함수로는 되부름(재귀⁠, recursion⁠)을 어떻게 할까요? 함수 g에 넣었을 때 그대로 돌아오는 값, 곧 $g\,z = z$인 z를 g의 고정점⁠(fixed point)⁠이라고 합니다. 고정점 조합자⁠(fixed-point combinator)⁠ Y = λf.(λx.f (x x))(λx.f (x x))는 $Y\,g = g\,(Y\,g)$를 만족하므로, 어떤 g를 주든 그 고정점 Y g를 만들어 줍니다. 이것이 함수가 자기 자신을 부르는 효과를 냅니다. 계승(n!)을 예로 들면, g = λf.λn.(n이 0이면 1, 아니면 n × f(n − 1))로 두고 FACT = Y g라 하면 FACT n은 g FACT n, 곧 n × FACT(n − 1)로 펼쳐집니다. Y g를 줄이면 앞에 g가 하나 붙은 같은 모양이 다시 나오는데, Ω가 자기 자신으로 돌아오는 것과 같은 되풀이 구조입니다. Ω와 모양이 닮은 것은 그래서 우연이 아닙니다. 처치가 처음 람다 계산을 담으려던 논리 체계는 1935년 처치의 두 제자 스티븐 클리니(뒤에 정규 표현식⁠(regular expression)⁠을 만든 미국 논리학자)와 로서가 러셀의 역설⁠(Russell's paradox)⁠과 비슷한 방법으로 모순을 찾아내 버려졌고, 계산 부분만 살아남았습니다. 람다 항의 문법 자체는 짧은 문맥 자유 문법⁠(context-free grammar)⁠으로 적힙니다.

이어지는 곳. 1936–37년 튜링은 람다로 정의할 수 있는 함수와 튜링 기계⁠(Turing machine)⁠로 계산할 수 있는 함수가 정확히 같음을 보였고, 이것이 처치–튜링 논제⁠(Church–Turing thesis)⁠의 기둥이 되었습니다. 계산을 함수의 적용과 조합으로 적는 프로그래밍 언어를 함수형 언어라 하는데, 1958년 존 매카시가 만든 Lisp는 람다 표기를 빌려 왔고, 오늘날의 Haskell 같은 함수형 언어⁠(functional programming language)⁠는 람다 계산을 핵심으로 삼습니다. 파이썬의 lambda처럼 여러 언어가 이름 없는 함수를 가리키는 말로 이 이름을 물려받았습니다. 타입⁠(type)⁠ 없는 람다 계산에는 오랫동안 수학적 모형이 없었습니다. 모든 항이 함수이면서 인자라서 값의 집합⁠(set)⁠ D가 D에서 D로 가는 함수 전체와 같아야 하는데, 원소⁠(element)⁠가 둘 이상이면 대각선 논법⁠(diagonal argument)⁠이 그것을 막기 때문입니다. 1969년 데이나 스콧은 연속 함수만 모으면 된다는 것을 보여 이 문제를 풀었고, 여기서 영역 이론⁠(domain theory)⁠이 시작되었습니다. 변수마다 '수', '참·거짓' 같은 종류(타입)를 붙인 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠에서는 모든 계산이 반드시 끝나는 대신 Y 조합자⁠(Y combinator)⁠ 같은 끝없는 되부름을 적을 수 없고, 타입이 명제, 프로그램이 그 명제의 증명이 되는 대응이 드러납니다. 미국 논리학자 해스켈 커리와 윌리엄 하워드의 이름을 따 커리–하워드 대응⁠(Curry–Howard correspondence)⁠이라 합니다. 예를 들어 A를 받아 B를 돌려주는 함수의 타입 A → B는 명제 'A이면 B'에 대응하고, 그 함수에 A 타입의 값을 넣어 B를 얻는 일은 'A'와 'A이면 B'에서 'B'를 끌어내는 추론에 대응합니다. 이 대응은 Coq(Rocq)나 Lean처럼 컴퓨터로 증명을 검사하는 도구(증명 보조기⁠, proof assistant⁠)의 바탕이 되었습니다. 그런 도구가 다루는 형식 증명으로도 넘을 수 없는 한계를 말해 주는 것이 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠입니다.