Kleene의 제2 재귀 정리로 Quine을 직접 만들어 봤다

Constructing a Quine from Kleene's Second Recursion Theorem

Quine이 존재한다는 사실은 Kleene의 제2 재귀 정리의 따름정리지만, 실제로 이 구성이 얼마나 다루기 쉬운지는 잘 알려져 있지 않다. 저자는 Rocq에서 정리를 형식화하며 증명을 깔끔하게 다듬고, 타입이 있는 함수형 관점에서 고정점 구성이 Gödel의 불완전성 정리와 Tarski의 정의 불가능성 정리로 이어지는 대각선 보조정리의 함수형 표현임을 보여준다. 이어서 Church 인코딩과 quasi-quoter를 이용해 untyped lambda calculus 안에서 자기 자신을 출력하는 Quine을 구현한다.