순수 $\lambda$-Calculus에서의 순환 그래프와 메모이제이션 (Memoization)

$λ$-calculus (람다 계산법)는 일반적으로 그래프 축약 (graph reduction)을 위해 추가적인 재귀 구조인 \texttt{letrec}, $\mu$-binder, 또는 내장된 $Y$ combinator를 필요로 하며, 메모이제이션 (memoized) 또는 동적 계획법 (dynamic-programming) 함수의 반복되는 작업을 공유하기 위해서는 일반적으로 비순수 (impure) 캐시가 필요합니다. 우리는 어떠한 확장도 필요하지 않음을 보여줍니다. 우리는 최소 고정점 방정식 (least-fixpoint equation)을 해결하는 표준 방법인 테이블링 (tabling)을 약한 헤드 축약 (weak-head reduction)에 적용합니다. 이는 각 항의 표준적인 게으른 의미 (lazy meaning)를 유지하면서 순수 $λ$-calculus를 위한 새로운 연산 의미론 (operational semantics)을 정의합니다. 유한한 수의 서로 다른 상태에 도달하는 항은 유한한 그래프로 출력되며, 이는 순환적 (cyclic)일 수 있습니다. 이 계산법은 순수성을 유지하며, 해당 그래프는 건전하고 축약 순서에 독립적입니다. 우리는 이 연산 의미론을 $λ$-calculus 인터프리터로 구현했습니다. 이는 별도의 메모이제이션 테이블 없이도 반복되는 하위 문제들을 공유하며 동적 계획법 (dynamic programming)을 자동으로 수행합니다. 또한 추가적인 재귀 구조 없이 순환 그래프를 생성하고 변형합니다. 그리고 생산적이지 않은 루프 (unproductive loop)를 판별하여, $\Omega$에 대해 유한한 시간 내에 $\bot$을 반환합니다. 평가기 (evaluator)가 반환하는 것은 그래프이므로, $λ$-calculus는 그래프 계산을 위한 DSL (Domain Specific Language)이 됩니다. 동적 계획법의 메모 테이블, 게임 탐색의 전치 테이블 (transposition table), 그리고 그래프 도달 가능성 (graph reachability) 및 포인터 분석 (points-to analysis)의 방문 집합 (visited set)은 모두 상태 동일성 (state identity)에 기반한 테이블링 (tabling)이며, 이 중 어느 것도 수동으로 작성되지 않습니다. 컴파일 (Compilation) 또한 이러한 문제 중 하나입니다. 우리는 자신의 소스 코드를 컴파일하는 부트스트랩 컴파일러 (bootstrap compiler)를 작성하며, 이 모든 것은 순수한 $λ$-term (람다 항)으로 이루어집니다.