자기 자신의 소스 코드를 그대로 출력하는 프로그램, 이른바 쿼인(Quine)은 프로그래머들에게 일종의 지적 유희로 알려져 있다. 그러나 이론적으로 보면 쿼인의 존재는 클리니의 제2 재귀 정리(Kleene's second recursion theorem)에서 따라 나오는 하나의 따름정리다. 한 연구자가 이 사실이 실제 구성에서 얼마나 쉽게 혹은 어렵게 다뤄지는지 궁금해 직접 형식화(formalization)를 시도한 작업을 정리했는데, 그 과정에서 드러나는 설계상의 선택들이 실무적으로도 곱씹어볼 만하다.
글쓴이는 형식화를 단순한 전사(轉寫) 작업으로 보는 통념에 반대한다. 정의가 어설프거나 논증 구조가 엉성하면 증명 과정에서 곧바로 고통이 느껴지기 때문에, 형식화는 수학자가 정의와 증명을 더 명료하고 간결하게 구조화하도록 자연스럽게 유도한다는 것이다. 즉 '빠른 증명'과 '잘 구조화된 증명'이라는 목표가 서로 어긋나지 않고 정렬된다. 이런 관점에서 그는 그동안 막연하게만 알던 정리를 깔끔하게 드러낼 수 있는 형식화를 찾던 중, 비타입 람다 계산(untyped lambda calculus)에서 이 구성을 수행하는 방법을 제시한 프리프린트를 발견했다고 전한다.
수를 넘어, 구조를 보는 관점
재귀 정리의 전통적 서술은 부분 재귀 함수들의 실효적 번호 매김 $\{\varphi_i\}$ 위에서 전개된다. 이때 쿼인은 정리에 등장하는 함수 $\psi$를 항등함수로 두었을 때의 따름정리로 떨어진다. 색인 $e$는 함수 $\varphi_e$의 표현으로 볼 수 있고, 따라서 $\varphi_e$는 입력 없이도 자기 자신의 '소스 코드'인 $e$를 출력하는 프로그램이 된다. 문제는 이런 전통적 전개가 쌍, 리스트, 구문 객체 같은 모든 이산 구조를 자연수로 환원한다는 점이다. 그 결과 세부를 생략하고 싶은 지루한 인코딩이 쌓이고, 강연자는 '어차피 모든 계산 모델은 동치'라며 손을 흔들고 넘어가게 된다. 글쓴이는 이런 태도가 자칫 형식 체계 전반을 '다 똑같이 임의적이고 못생긴 것'으로 치부하는 허무주의로 이어질 수 있다고 경고한다.
이에 대한 대안으로 그는 형식 체계의 구조를 진지하게 다루는 분야인 증명론(proof theory)을 끌어온다. 형식 체계를 어떻게 구조화하느냐에 상당한 내용이 담길 수 있다는 것이 증명론의 큰 교훈이며, 그 연장선에서 가장 증명론적인 계산 모델인 람다 계산에 도달하게 된다는 논리다. 최종적으로는 비타입 람다 계산에서 작업하지만, 타입을 명시한 버전을 거치면 다른 결과들과의 연결이 더 잘 보인다. 비타입 세계에서 타입은 '도덕적 타입'으로서 배경에 깔린다.
쿼인을 넘어서는 일반성
함수적 버전의 정리는 자기 반영(self-reflection)이 가능한 언어 $L$을 전제한다. 타입 $T$와 함수 $P:\mathsf{AST}\rightarrow T$가 주어지면 $P\lceil t\rceil = t$를 만족하는 항 $t:T$가 존재한다는 것이 핵심이다. 구성은 $d := \lambda e.\,P(e\cdot \mathsf{q}\,e)$로 두고 고정점 표현 $t := d\lceil d\rceil$를 잡는 방식이다. 여기서 $P$를 항등함수로 두면 익숙한 쿼인이 나오지만, 정리의 쓸모는 그보다 넓다. $P$를 크기 계산 함수로 두면 자기 크기를 출력하는 프로그램이, 예쁜 출력 함수로 두면 자기 소스를 텍스트로 찍어내는 전형적 쿼인이 나온다. 요컨대 프로그램의 '구문적 성질'이라면 무엇에 대해서든 고정점을 찾을 수 있는 도구인 셈이다.
주목할 점은 이 증명이 $L$의 튜링 완전성을 가정하지 않는다는 것이다. 그래서 전체 언어(total language)인 산술 체계의 항 언어에서도 성립하며, 여기서 논리학의 다른 영역과 중요한 연결이 생긴다. 명제 타입 $\mathsf{Prop}$을 갖춘 고차 산술에서 $T=\mathsf{Prop}$으로 두면, 이 정리는 괴델의 제1 불완전성 정리와 타르스키의 정의 불가능성 정리의 핵심 재료인 대각선 보조정리(diagonal lemma)의 함수적 서술이 된다. 증명 가능성 술어 $\mathsf{Prov}$에 대해 $P:=\neg\circ\mathsf{Prov}$로 두면 괴델의 문장이, 진리 술어 $\mathsf{Tr}$에 대해 $P:=\neg\circ\mathsf{Tr}$로 두면 타르스키의 결과가 같은 틀에서 흘러나온다. 쿼인이라는 장난처럼 보이던 대상이 20세기 논리학의 거대한 정리들과 한 뿌리임을 한눈에 보여주는 대목이다.
구현의 실제: 언어를 언어 안에 담기
이 증명을 실제로 돌리려면 언어 자신의 AST 표현이 필요한데, 비타입 람다 계산은 처치 인코딩(Church encoding)으로 트리형 데이터를 무리 없이 다룬다. 변수·적용·람다 추상이라는 세 생성자는 인코딩에서 $\lambda v\,a\,l.\cdots$ 형태의 세 람다 추상으로 나타나며, 본문은 원래 항의 구조를 그대로 반영하도록 $v,a,l$로 쌓아 올린다. 변수의 de Bruijn 색인은 처치 수로 표현된다. 가장 까다로운 부분은 준인용기(quasi-quoter)인데, 이는 결국 AST의 트리 구조에 대한 접기(fold)로 서술되고, 처치 인코딩이 접기를 자연스럽게 처리하므로 단일 항으로 변환할 수 있다.
이 모든 구성과 추론은 증명 보조기 Rocq에서 수행되었고, 결과로 얻은 쿼인은 de Bruijn 표기로 제시되었다. 실무자 입장에서 이 작업의 함의는 분명하다. 자기 참조와 메타프로그래밍은 '마법'이 아니라 명시적으로 구성 가능한 대상이며, 모델의 선택이 증명의 명료함을 좌우한다는 점이다. 다만 한계도 있다. 여기서 다룬 것은 순수 람다 계산 위의 깔끔한 수학적 뼈대일 뿐, 실제 언어의 입출력이나 런타임, 성능 같은 공학적 현실은 논의 밖에 있다. 그럼에도 '왜 하필 이렇게 서술하는가'라는 질문을 끝까지 밀어붙이면 지루한 인코딩 뒤에 숨은 구조가 보인다는 점은, 이론과 구현을 오가는 이들에게 작지 않은 교훈이다.