해스켈 커리(Haskell Curry)

해스켈 커리는 1900년 미국 매사추세츠주 밀리스에서 태어났습니다. 그의 부모는 보스턴에서 화술 학교를 운영했습니다. 1920년대에 논리학을 공부하던 그는 한 가지가 마음에 걸렸습니다. 러셀과 화이트헤드의 『수학 원리』는 수학 전체를 논리에서 끌어내려 했는데, 그 바탕에 있는 '변수에 식을 대입한다'는 규칙이 뜻밖에 까다로웠습니다. $\forall y\, (x \lt y)$의 $x$에 $y + 1$을 그대로 넣으면 $\forall y\, (y + 1 \lt y)$가 되어, 바깥의 $y$가 안쪽 한정기호에 붙잡히며 뜻이 바뀝니다. 커리는 대입이라는 조작을 더 작은 부품으로 쪼개 분석하려 했고, 그 끝에서 변수가 아예 없는 논리, 곧 조합 논리에 이르렀습니다.

나이 세 ·

그는 1920년 하버드 수학과를 졸업한 뒤 MIT에서 전기공학을, 하버드에서 물리학을 공부했다가 논리학으로 돌아왔습니다. 1927년 무렵 그는 러시아의 모제스 쇤핑클이 1924년 발표한 논문을 알게 되었는데, 쇤핑클은 커리가 찾던 것과 같은 부품을 이미 내놓고 있었습니다. 커리는 그 생각을 체계로 키우기로 하고 1928년 괴팅겐으로 가서, 힐베르트를 지도 교수로, 실제로는 주로 파울 베르나이스와 의논하며 1930년 박사 논문 「조합 논리의 기초⁠(basics)⁠」를 발표했습니다. 1929년부터 1966년까지 펜실베이니아 주립 대학에서 가르쳤고, 그 뒤 1970년까지 암스테르담 대학에 있었습니다.

조합 논리의 부품은 두 개면 충분합니다. $\mathbf{K}\,x\,y = x$는 둘째 인자를 버리고, $\mathbf{S}\,x\,y\,z = x\,z\,(y\,z)$는 셋째 인자를 두 곳에 나누어 줍니다. 변수에 이름을 붙여 '$x$를 받아 무엇을 돌려준다'고 적는 람다 계산⁠(lambda calculus)⁠의 함수는 모두 이 두 가지를 이어 붙인 식으로 바꿀 수 있습니다. 가장 간단한 예가 받은 것을 그대로 돌려주는 함수입니다. $\mathbf{S}\,\mathbf{K}\,\mathbf{K}\,x = \mathbf{K}\,x\,(\mathbf{K}\,x) = x$이므로 $\mathbf{SKK}$가 곧 항등 함수입니다. 변수가 없으니 변수가 붙잡히는 문제도 처음부터 생기지 않습니다. 같은 생각에서 나온 것이 인자 두 개짜리 함수 $f(x, y)$를 '$x$를 받아, $y$를 받는 함수를 돌려주는 함수'로 보는 방식이고, 이것이 그의 이름을 딴 커링입니다. 이 방식은 프레게와 쇤핑클이 먼저 썼고 이름은 뒤에 붙었습니다. 프로그래밍 언어 하스켈과 커리도 그의 이름을 땄습니다.

1934년 논문 「조합 논리의 함수성」에서 그는 조합자에 타입을 붙였습니다. $\mathbf{K}$는 $A$형의 값을 받아 '$B$형의 값을 받아 $A$형을 돌려주는 함수'를 돌려주므로 타입이 $A \to (B \to A)$이고, $\mathbf{S}$의 타입은 위의 식의 둘째 것입니다. 커리는 이 두 타입의 화살표를 '이면'으로 읽으면, 힐베르트식 명제 논리⁠(propositional logic)⁠에서 함의에 관한 두 공리와 글자 하나 다르지 않다는 것을 알아차렸습니다. 함수를 값에 적용하는 규칙($f : A \to B$이고 $a : A$이면 $f\,a : B$)은 '$A$이면 $B$'와 '$A$'에서 '$B$'를 끌어내는 추론 규칙, 곧 전건 긍정(modus ponens)과 같습니다.

그러면 $\mathbf{SKK}$의 타입을 셈하는 일은 '$A$이면 $A$'를 증명하는 일과 한 줄씩 겹칩니다. 첫 $\mathbf{K}$를 $A \to ((B \to A) \to A)$로 쓰고, $\mathbf{S}$를 $(A \to ((B \to A) \to A)) \to ((A \to (B \to A)) \to (A \to A))$로 쓰면, 적용 한 번에 $\mathbf{SK} : (A \to (B \to A)) \to (A \to A)$를 얻습니다. 여기에 둘째 $\mathbf{K} : A \to (B \to A)$를 적용하면 $\mathbf{SKK} : A \to A$입니다. 논리학 교과서에서 $A \to A$를 증명하는 다섯 줄, 곧 공리를 세 번(두 공리꼴 가운데 하나는 두 번) 쓰고 전건 긍정을 두 번 쓰는 증명이 정확히 이 계산입니다. 프로그램 $\mathbf{SKK}$는 그 증명을 압축해 적은 이름표인 셈입니다. 커리는 1958년 로베르 페이스와 함께 펴낸 『조합 논리』에서 이 대응을 더 넓게 적었지만, 그에게 이것은 공리 쪽의 흥미로운 일치였습니다. 증명을 간단히 하는 과정까지 계산과 맞아떨어진다는 더 깊은 절반은 1969년 하워드가 채웠고, 두 사람의 이름을 딴 커리–하워드 대응이 되었습니다.

타입을 붙이지 않은 조합 논리를 그대로 논리로 쓰면 모순이 생깁니다. 1935년 처치의 제자 스티븐 클리니와 바클리 로서는 처치와 커리의 초기 체계가 모순임을 보였고, 1942년 커리는 훨씬 짧은 역설을 내놓았습니다. 문장 $X$를 '$X$가 참이면 $Y$이다'로 정의합니다. $X$를 가정하면 그 뜻에 따라 '$X$이면 $Y$'이고, 가정한 $X$와 전건 긍정으로 $Y$가 나옵니다. 그러므로 가정 없이 '$X$이면 $Y$'가 성립하고, 이것이 곧 $X$이니 다시 전건 긍정으로 $Y$입니다. $Y$는 아무 문장이나 될 수 있습니다. 러셀의 역설⁠(Russell's paradox)⁠과 달리 부정이 전혀 쓰이지 않는다는 것이 요점입니다. 자기 자신을 가리키는 문장을 만들 수 있고(조합 논리에서는 고정점⁠(fixed point)⁠ 조합자가 이것을 해 줍니다), 가정을 두 번 쓰는 일이 허락되면 그것만으로 모순입니다. 그래서 타입을 붙여 자기 적용을 막거나, 가정을 한 번만 쓰게 제한하는 지라르의 선형 논리⁠(linear logic)⁠ 같은 길이 필요해집니다.

2차 세계대전 중 그는 응용 물리학 일을 했고, 1946년 무렵 동료와 함께 첫 전자식 범용 컴퓨터 에니악으로 역보간을 계산하는 프로그램을 설계한 보고서를 썼습니다. 큰 프로그램을 작은 프로그램들을 조합해 만드는 방법을 논한 이 보고서들은 프로그래밍 역사 연구에서 다시 주목받고 있습니다. 철학에서 그는 수학을 형식 체계⁠(formal system)⁠에 관한 학문으로 보는 형식주의⁠(formalism)⁠의 편에 섰고, 역설 앞에서도 체계를 버리기보다 어디서 무엇이 잘못되는지를 끝까지 분석하는 쪽을 택했습니다. 그는 1982년 펜실베이니아주 스테이트 칼리지에서 세상을 떠났습니다.

이어지는 곳. 조합자와 같은 일을 변수로 하는 언어가 람다 계산이고, 거기에 타입을 붙인 체계가 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠입니다. 조합자의 타입과 공리의 일치는 커리–하워드 대응과 직관주의 논리⁠(intuitionistic logic)⁠에서 증명 전체로 넓어지고, 그 대응을 완성한 사람은 하워드입니다. 커리의 역설이 기대는 자기 참조⁠(self-reference)⁠는 러셀의 역설, 고정점, 자기 참조와 같은 뿌리이고, 가정을 쓰는 횟수를 제한하는 논리는 지라르의 페이지에 있습니다. 함수형 언어⁠(functional programming language)⁠가 인자를 하나씩 받는 방식의 범주론적 설명은 데카르트 닫힌 범주⁠(cartesian closed category)⁠가 줍니다.

관계.

• 스승 다비트 힐베르트 — 1928–29년 괴팅겐에서 힐베르트를 공식 지도 교수로, 실제로는 주로 파울 베르나이스와 의논하며 조합 논리에 관한 박사 논문을 썼습니다.
• 영향을 줌 윌리엄 하워드 — 커리가 1934년과 1958년 책에서 적은 '조합자의 타입 = 함의 논리의 공리'라는 관찰을, 하워드가 1969년 증명 전체와 계산 전체의 대응으로 넓혔습니다.

연표.

• 1920년 하버드 대학에서 수학 학사 학위를 받다
• 1924년 하버드에서 물리학 석사 학위를 받은 뒤 논리학으로 방향을 바꾸다
• 1927년 쇤핑클의 1924년 조합자 논문을 알게 되다
• 1928년 괴팅겐으로 가서 힐베르트와 베르나이스 밑에서 연구하다
• 1929년 펜실베이니아 주립 대학에 자리를 잡다
• 1930년 박사 논문 「조합 논리의 기초」를 발표하다
• 1934년 「조합 논리의 함수성」에서 조합자의 타입이 논리의 공리와 같은 모양임을 적다
• 1942년 부정 없이 함의만으로 모순을 만드는 '커리의 역설'을 발표하다
• 1946년 에니악으로 역보간을 계산하는 프로그램을 설계한 보고서를 쓰다
• 1958년 로베르 페이스와 『조합 논리』 1권을 펴내다
• 1966년 암스테르담 대학으로 옮기다
• 1980년 하워드의 원고가 실린 기념 논문집 『H. B. 커리에게』가 나오다