Programs that know themselves, and the limits of description.
"자기 소스 코드를 그대로 출력하는 프로그램을 짜라"는 장난 같은 문제가 있습니다. 불가능해 보이지만 — 어느 언어에서든 반드시 존재합니다. 그걸 보장하는 게 클레이니 재귀정리이고, 그 정리는 괴델·튜링·칸토어와 똑같은 한 수법 위에 서 있죠. 이어서 "이 데이터를 만드는 가장 짧은 프로그램은?"이라는 질문(콜모고로프 복잡도)이 무작위성의 정의와 계산 불가능성의 벽으로 우리를 데려갑니다. 이어서 언어 자체를 들여다보면 — 람다 계산법은 함수 하나로 지은 수학이고, 타입은 명제이며 프로그램은 증명이고(커리–하워드), 여러분이 매일 쓰는 정규식은 오토마타입니다. 프로그래밍이 사실은 수학이 사는 집이라는 이야기.
콰인(quine)은 실행하면 자기 소스 코드를 한 글자도 안 틀리고 출력하는 프로그램입니다(철학자 콰인의
이름에서). 입력도 파일 읽기도 없이요. 처음 들으면 불가능해 보입니다 — print("...")의 "..."
안에 프로그램 전체가 들어가야 하는데, 그 프로그램에는 다시 print("...")가 있고, 그 안에 또… 무한 러시아
인형이죠.
탈출구는 코드와 데이터를 분리하는 것입니다. 프로그램 본문을 문자열(데이터)로 딱 한 벌 저장해 두고, 코드는 그 데이터를 두 번 쓰게 합니다 — 한 번은 따옴표 친 문자열로(데이터 부분 재현), 한 번은 실행되는 코드로(코드 부분 재현). 파이썬으로 쓰면 딱 한 줄이에요:
s = 's = %r; print(s %% s)'; print(s % s)
여기서 %r은 "문자열을 따옴표까지 붙여 그대로 되살려라"는 뜻입니다. s % s가 s를 자기
자신에 끼워 넣어, 데이터였던 s가 코드 자리에도 그대로 복제되죠. 이 "한 벌을 두 군데에 붙여넣기"가
콰인의 심장입니다. 아래는 자바스크립트 콰인 — 진짜로 실행해 보세요.
콰인이 특정 언어의 잔재주처럼 보이지만, 아닙니다. 어떤 언어든 (튜링 완전하기만 하면) 콰인이 존재한다는 건 정리예요. 1938년 클레이니의 재귀정리가 그 뿌리입니다.
즉 여러분은 이렇게 쓸 수 있습니다 — "변수 me에 내 소스 코드가 이미 들어 있다고 치고 나머지를
짜라." 그러면 print(me)는 콰인이고, print("내 길이는 " + len(me))는 자기 길이를 정확히 아는
프로그램이 되죠. 증명은 1장의 "한 벌을 두 군데 붙여넣기"를 일반화한 것뿐입니다.
콰인의 "자기 자신을 데이터로 받아 자기에게 먹인다"는 손놀림은, 놀랍게도 수학사의 가장 유명한 폭탄들과 정확히 같은 동작입니다.
이 모두를 한 정리로 묶는 게 로비어의 부동점 정리인데 — 그건 "대각선, 그 하나의 수법" 페이지에서 통째로 다룹니다. 여기선 프로그래밍에 가장 가까운 얼굴, 람다 계산법의 Y 결합자만 보죠.
이 \((x\,x)\)의 자기적용이 도대체 어떻게 "함수 하나로 지은 수학" 위에서 재귀를 낳는지 — 그 무대인 람다 계산법을 다음 장에서 제대로 봅니다.
콰인이 "자기를 재생하는 가장 짧은 코드"였다면, 이번엔 대상을 넓힙니다 — 어떤 데이터 \(x\)를 출력하는 가장 짧은 프로그램의 길이. 이걸 \(x\)의 콜모고로프 복잡도 \(K(x)\)라 부릅니다(1965, 콜모고로프·솔로모노프·차이틴).
예를 들어 0을 백만 번 쓴 문자열은 "0"*1000000이라는 짧은 프로그램으로 만들어지니 \(K\)가 작습니다.
원주율 \(\pi\)의 앞 백만 자리도 — 무작위처럼 보이지만 — \(\pi\)를 계산하는 짧은 프로그램이 있으니 \(K\)가 작죠.
반면 동전을 백만 번 던진 진짜 무작위열은, "그냥 그 문자열을 통째로 담은" 프로그램보다 짧게 못 씁니다.
| 데이터 (64비트 예시) | 가장 짧은 설명(생성기) | 복잡도 |
|---|---|---|
| 0000…0000 (전부 0) | "0을 64번 찍어라" | 작음 |
| 0101…0101 (교대) | "01을 32번 찍어라" | 작음 |
| π의 이진전개 앞 64비트 | "π를 계산해 64비트 잘라라" | 작음 |
| 1101001011…0110 (동전 던지기) | 없음 — 통째로 담는 수밖에 | ≈ 64 |
1930년대, 튜링이 "기계"로 계산을 정의하던 그때 처치는 전혀 다른 길을 갔습니다 — 오직 함수만으로요. 재료는 딱 셋입니다: 변수(\(x\)), 함수 정의(\(\lambda x.\,M\), "\(x\)를 받아 \(M\)"), 적용(\(M\,N\)). 숫자도, 참·거짓도, 데이터도 없습니다. 그런데 그것만으로 다 지어져요.
숫자는 "함수를 몇 번 적용하는가"로 정의합니다(처치 수): \(\;n=\lambda f.\lambda x.\,\underbrace{f(f(\cdots f}_{n}(x)))\). 그러면 \(0=\lambda f.\lambda x.\,x\)(안 적용), \(1=\lambda f.\lambda x.\,f\,x\). 산술도 함수 조작으로 떨어집니다:
\[ \text{add}=\lambda m.\lambda n.\lambda f.\lambda x.\,m\,f\,(n\,f\,x),\quad \text{mul}=\lambda m.\lambda n.\lambda f.\,m\,(n\,f),\quad m^{\,n}=\lambda m.\lambda n.\,n\,m. \]참·거짓조차 함수예요 — \(\text{참}=\lambda x.\lambda y.\,x\)(둘 중 앞을 고름), \(\text{거짓}=\lambda x.\lambda y.\,y\),
그러면 if는 그냥 \(\lambda b.\lambda t.\lambda e.\,b\,t\,e\). 계산은 오직 β-축약 한 규칙 —
\((\lambda x.M)\,N \to M[x:=N]\), "인자를 몸통에 대입"뿐입니다. 아래에서 진짜 처치 수로 계산해 보세요(자바스크립트
함수로 그대로 구현했습니다).
여기서 프로그래밍과 논리학이 같은 것임이 드러납니다. 1930~60년대 커리와 하워드가 발견한 사전(辭典) 하나 — 타입은 명제, 프로그램은 그 명제의 증명입니다.
| 타입 (프로그래밍) | 명제 (논리) | 뜻 |
|---|---|---|
| \(A\to B\) | \(A\Rightarrow B\) | A의 증거를 받아 B의 증거를 내놓는 함수 = "A이면 B"의 증명 |
| \(A\times B\) (쌍) | \(A\wedge B\) | 둘 다의 증거를 함께 쥠 |
| \(A+B\) (합/Either) | \(A\vee B\) | 둘 중 하나의 증거 + 어느 쪽인지 |
| \(\mathtt{Unit}\) / \(\mathtt{Void}\) | 참 \(\top\) / 거짓 \(\bot\) | 증거 하나뿐 / 증거 없음 |
그래서 프로그램을 실행하는 것 = 증명을 간단히 하는 것(컷 제거)이고, 타입 검사 = 증명 검사입니다. 이게 Coq·Lean·Agda 같은 증명 보조기가 수학을 컴퓨터로 검증하는 원리예요 — 정리를 타입으로 적고 증명을 그 타입의 프로그램으로 짠 뒤, 컴파일러가 타입만 맞춰 주면 정리가 참인 거죠. 실제로 4색정리(Coq), 케플러 추측(Flyspeck), 파이트–톰프슨 정리가 이렇게 기계 검증됐습니다.
타입엔 놀랍게도 대수(algebra)가 있습니다. 타입의 값이 몇 개인지 세어 보면 — 곱·합·함수 타입이 곱셈·덧셈·거듭제곱 그 자체예요:
\[ |A\times B|=|A|\cdot|B|,\qquad |A+B|=|A|+|B|,\qquad |A\to B|=|B|^{|A|}. \]그래서 Bool\(=1{+}1=2\), Maybe A\(=1{+}A\), 그리고 리스트는 \(L(A)=1+A\cdot L(A)\)를 풀면
\(L(A)=\dfrac1{1-A}\) — 생성함수가 여기서도 나옵니다! 타입을 미분하면 "구멍
뚫린 자료구조"(지퍼)가 나오는 것까지 진짜입니다. 아래에서 값의 개수를 직접 세어 보세요.
타입은 논리로도 이어집니다. 힌들리–밀너 타입 추론은 우리가 타입을 안 써도 컴파일러가 알아맞히는 마법인데, 그 정체는 방정식을 푸는 단일화(unification) 알고리즘(로빈슨) — 논리 프로그래밍(Prolog)과 같은 엔진입니다. 한 걸음 더, 타입이 값에 의존하게 하면(\(\mathtt{Vec}\,n\) = 길이 \(n\)짜리 리스트) \(\forall,\exists\)가 \(\Pi,\Sigma\) 타입이 되어 완전한 술어논리가 됩니다 — Lean·Agda가 정리를 표현하는 바로 그 언어죠.
마지막은 가장 친숙한 얼굴. 여러분이 로그를 뒤질 때 쓰는 정규식(regex)은 사실 수학적 대상입니다. 클레이니 정리가 말합니다 — 정규식 = 유한 오토마타 = 정규언어, 이름만 셋이지 같은 하나예요.
정규식의 연산 \(+\)(택일)·\(\cdot\)(이어붙임)·\({}^{*}\)(반복)은 클레이니 대수라는 대수 구조를 이루고, 각 정규식은 상태 기계(오토마타) 하나로 바뀝니다. 아래는 "이 이진수는 \(3\)의 배수인가?"를 판정하는 세 상태짜리 오토마타 — 비트를 하나 읽을 때마다 \(s\leftarrow(2s+b)\bmod 3\), 끝에서 상태가 \(0\)이면 3의 배수죠.
자기 소스를 뱉는 장난(콰인)에서 출발해, 그게 요행이 아니라 재귀정리임을 봤고, 그 정리가 괴델·튜링과 같은 대각선 손놀림이며 람다의 Y 결합자로 이어짐을 봤고, "가장 짧은 설명"이라는 질문(콜모고로프 복잡도)이 무작위성의 정의와 계산 불가능성의 벽까지 데려가는 걸 봤습니다. 그다음 언어 자체를 열어 — 람다 계산법은 함수 하나로 지은 수학이고, 타입은 명제이자 프로그램은 증명이며(Coq·Lean이 수학을 검증하는 이유), 타입엔 대수가 있고, 정규식은 오토마타라는 걸 봤죠. 프로그래밍은 수학을 응용하는 도구이기 전에, 수학이 살아 움직이는 무대였던 거예요.
같은 대각선의 다른 얼굴들은 로비어 부동점 정리에서, 계산의 한계(정지 문제·튜링 완전· P vs NP)는 컴퓨터가 못 푸는 문제에서, 자기지시 역설의 원류는 패러독스에서 이어집니다.