기술 요약: 순수 $\lambda$-계산에서의 순환 그래프와 메모이제이션

1. 문제 정의

표준적인 연산 의미론을 따르는 순수 $\lambda$-계산은 외부 확장 없이는 순환 데이터 구조나 무한 계산을 표현하거나 효율적으로 조작하는 것이 근본적으로 불가능하다.

• 순환 데이터 표현: 표준적인 축약(예: $Y(\text{cons } 0)$)은 무한한 스트림을 유한한 순환 그래프로 접는 대신, 무한한 트리($0, 0, 0, \dots$)로 펼쳐버린다. 유한한 순환을 얻기 위해서는 전통적인 방식처럼 letrec이나 $\mu$-바인더와 같은 재귀 구문을 추가해야 한다.
• 메모이제이션 및 동적 계획법: 동적 계획법(예: 편집 거리)이나 그래프 순회(예: 순환 리스트에 대한 map)를 구현하는 순수 함수형 프로그램은 지수 시간 복잡도를 갖거나 종료되지 않는 문제를 겪는다. 기존의 해결책들은 메모이제이션을 위한 가변 캐시, 순환 탐지를 위한 참조 동일성 프리미티브 등 불순한(impure) 메커니즘을 필요로 한다. 이는 순수 함수형 언어의 핵심 원칙인 참조 투명성을 위반한다.
• 핵심 장애물: 본 논문은 일반적인 축약 과정에는 이전에 방문한 항(term)을 인식할 수 있는 메커니즘이 결여되어 있음을 지적한다. "상태 동일성(state identity)"을 순수하게 감지할 방법이 없다면, 계산 체계는 반복되는 하위 문제들을 자동으로 공유하거나 무한한 전개를 유한한 순환으로 접을 수 없다.

2. 방법론

저자들은 순수 $\lambda$-계산에 대한 새로운 연산 의미론을 제안하며, 이는 **테이블링된 약헤드 축약(tabling weak-head reduction)**에 기반한다. 이 접근 방식은 계산 체계에 어떠한 확장(no letrec, no impurity)도 요구하지 않으며, 단지 인터프리터가 항을 실행하는 방식을 변경한다.

2.1 테이블링된 약헤드 축약 (Tabled Weak-Head Reduction)

이 방법론은 두 가지 개념을 결합한다:

1. 약헤드 축약 (Weak-Head Reduction): 인터프리터는 항의 한 "층(layer)"(즉, 약헤드 정규형의 최상위 생성자)을 그 즉각적인 하위 항들에 대해 노출한다. 이것이 "일층 맵(one-layer map)" ($out$)을 정의한다.
2. 테이블링 (상태 동일성에 의한 메모이제이션): 인터프리터는 축약 중에 마주치는 상태(하위 항)들의 테이블을 유지한다.
   • 상태 동일성: 상태는 구조적 동일성(de Bruijn 항의 interning/hash-consing을 통한)에 의해 식별된다. 이는 결정 가능하며 상수 시간의 포인터 테스트이다.
   • 해결 (Resolution): 항이 마주쳤을 때:
     • 만약 그것이 새로운 상태라면, 인터프리터는 그 층을 계산하고 재귀한다.
     • 만약 그것이 이미 테이블에 존재하는 재방문된 상태라면, 인터프리터는 기존 항목을 재사용한다.
     • 만약 그것이 현재 스택 위에 있는 재방문된 상태(back-edge)라면, 인터프리터는 이를 무한히 펼치는 대신 그래프의 순환을 닫는다(close a cycle).

2.2 알고리즘

평가는 $\bot$ (정의되지 않음)에서 최소 고정점으로 향하는 클레이니 반복(Kleene iteration)을 통해 진행된다.

• 알고리즘 1 (드라이버): 항들을 반복적으로 해결한다. 이는 계산된 층들을 딥 머지 연산자($\sqcup$)를 사용하여 실행 중인 근사치에 병합한다. 만약 어떤 항이 스택 상에 있는 동안 다시 진입하면, 현재의 근사치를 반환한다(초기값은 $\bot$).
• 알고리 알고리즘 2 (WHNF): 약헤드 축약을 위한 특정 일층 맵이다. 헤드 레드엑스(head redex)를 생성자(변수, 추상화 또는 적용)가 노출될 때까지 축약한다.
• 알고리즘 3 (평가기): 드라이버와 맵을 합성한다. 이는 노드가 항을 나타내고 에지가 하위 항을 나타내는 유한한 그래프를 반환한다.

2.3 이론적 기초

• 건전성 (Soundness): 평가기에 의해 반환된 그래프는 해당 항의 Lévy–Longo 트리로 펼쳐진다. 이 그래프는 항의 데노테이션 의미론(denotational semantics)에 대한 유한한 표현이다.
• 유일성 (Uniqueness): 솔루션은 유일하다. 왜냐하면 축약이 "가드(guarded)" 되어 있기 때문이다(루트가 하위 항을 읽기 전에 확정됨). 이는 계산된 최소 고정점이 코인덕티브(coinductive) 트리인 최대 고정점과 같음을 보장하며, 결과가 축약 순서에 독립적임을 보장한다.
• 종료성 (Termination): 만약 항이 유한한 수의 서로 다른 상태(구조적 동일성)에 도달한다면, 평가기는 유한한 순환 그래프와 함께 종료된다. 만약 서로 다른 상태에 무한히 도달한다면, 표준적인 축약처럼 동작한다(잠재적 발산).

3. 주요 결과 및 사례 연구

저자들은 이 의미론을 Co-Lambda라는 인터프리터로 구현하였으며, 세 가지 영역에서 그 능력을 입증하였다.

1. 동적 계획법 (편집 거리):

   • 나이브하게 구현할 경우 지수 시간을 소요하는 편집 거리를 위한 순수 $\lambda$-항이 $O(mn)$ 시간 및 공간 내에 평가된다.
   • 인터프리터는 하위 문제(접미사 쌍)들이 구조적으로 동일한 interned node임을 자동으로 공유한다. 소스 코드에 명시적인 메모이제이션 테이블이나 방문 집합(visited set)을 작성할 필요가 없다. "테이블"은 인터프리터의 내부 상태 테이블이다.
   • 결과: 지수적 호출 트리가 표준 DP 테이블을 나타내는 유한한 그래프로 붕괴된다.

2. 순환 데이터 (0의 스트림):

   • 표준 축약 시 무한한 0의 스트림으로 펼쳐지는 $r = Y(\text{cons } 0)$ 항이 유한한 순환 그래프로 평가된다.
   • 인터프리터는 스트림의 tail이 현재 계산과 동일한 interned node임을 감지하여 back-edge를 닫는다.
   • 결과: 항 $r$은 무한한 메모리 사용 없이 무한한 스트림을 표현하는 self-loop를 가진 유한한 그래프로 평가된다.

3. 생산적이지 않은 루프 ($\Omega$):

   • $\Omega = (\lambda x. x x)(\lambda x. x x)$ 항은 생성자 층을 노출하지 않고 자기 자신으로 축약된다.
   • 표준 축약은 발산한다. 테이블링 평가기는 생성자 층이 노출되지 않은 채 스택에 재진입함을 감지하고, 해당 상태가 생산적이지 않음을 식별하여 유한한 시간 내에 $\bot$을 반환한다.
   • 결과: 인터프리터는 데이터를 생성하지 않는 특정 루프에 대해 비종료(non-termination)를 결정한다.

4. 기여

• 구축: 순환 무한 트리를 유한한 순환 그래프로 자동 폴딩하고 생산적이지 않은 루프를 결정하는, 테이블링 기반의 순수 $\lambda$-계산을 구축하였다.
• 이론: 건전성(그래프가 Lévy–Longo 트리로 펼쳐짐), 유일성(최소 고정점 = 최대 고정점), 종료 경계(유한한 도달 가능 상태를 가질 때 유한한 그래프)에 대한 증명을 제공한다.
• 응용:
  • 그래프 계산을 위한 DSL: 이 인터프리터는 메모이제이션, 트랜스포지션 테이블(게임 탐색), 방문 집합(그래프 도달 가능성)이 상태 동일성의 암묵적 결과로서 나타나는 도메인 특화 언어(DSL) 역할을 한다.
  • 자기 컴파일 컴파일러: 저자들은 자신의 소스 코드를 Python으로 컴파일하는 부트스트랩 컴파일러(순수 $\lambda$-항으로 작성됨)를 구축하였다. 이 컴파일러는 동일한 테이블링 메커니즘을 사용하여 컴파일 과정을 최적화(defunctionalization)하며, 이를 통해 인터프리터 버전 대비 상당한 속도 향상(약 5배)과 메모리 절감을 달aba.

5. 의의 및 주장

본 논문은 다음 두 가지 방식으로 "순수성의 대가(price of purity)"를 해결한다고 주장한다.

1. 확장 제거: 순환 그래프와 메모이제이션이 재귀 구문(letrec)이나 불순한 프리미티브(포인터 동일성)를 언어에 추가하지 않고도 달성될 수 있음을 보여준다. "인식"은 용어(term)가 아닌 솔버(인터프리터)에 의해 수행된다.
2. 유리한 파편 (Rational Fragment): 이 계산 체계는 "유리한(rational)" 계산(유한한 수의 서로 다른 서브트리를 갖는 계산)을 위한 작은 DSL이 된다. 이러한 계산에 대해 인터프리터는 자동적인 동적 계획법과 순환 폴딩을 제공한다.
3. 한계: 본 논문은 구조적 동일성(결정 가능)에 의존한다는 "유리한 천장(rational ceiling)"을 인정한다. 이 방법은 행동적으로 동등($\beta$-equal)하지만 구조적으로는 다른 항들을 폴딩할 수는 없다. $\beta$-동등성은 결정 불가능하기 때문이다. 따라서 이 방식은 전체 무한 행동 공간이 아닌 유리한 파편(rational fragment)을 해결한다.

이 연구는 $\lambda$-계산을 단순히 단계별 축약(imperating computation)을 위한 언어가 아니라, **그래프 생성을 선언(declaring)**하는 언어로 재정의한다. 즉, 솔버가 그래프 구축의 효율성과 종료를 처리하도록 한다.