기술 요약: pruning과 memoization을 통한 miniKanren에서의 bottom-up enumeration을 향하여

문제 정의

현대의 프로그램-예시-기반(Program-by-Example, PBE) 합성기들은 일반적으로 관찰적 중복 제거(observational deduplication)를 동반한 bottom-up enumeration에 의존한다. 이 접근 방식은 후보 표현식들의 worklist를 유지하며, 예시 입력들에 대한 동작을 기준으로 이들을 중복 제거하고, 매칭되는 결과가 발견될 때까지 레벨별로 확장해 나간다. 이러한 전략은 명령형 및 함수형 환경에서는 매우 효과적이지만, 자연스러운 탐색 규칙이 공정한(fair) 후보 스트림에 대한 top-down resolution인 관계형 프로그래밍(특히 miniKanren)에서는 다소 어색하게 자리 잡고 있다.

관계형 인터프리터를 작성하여 이를 "역방향"으로 실행하거나 깊이 제한(depth bounds)을 사용하는 "enumerate-and-test" 방식을 사용하는 기존의 miniKanren PBE 레시피들은 현실적인 탐색 깊이에서 상당한 비효율성을 겪는다. 주요 문제는 탐색 트리에 행동적으로 동일한(behaviorally equivalent) 표현식들이 너무 많다는 점이다. 단순한 깊이 제한 enumerator는 매 재귀 레벨마다 새로운 중복 제거 테이블을 생성하므로, 이전 레벨에서 수행된 작업을 재사용하지 못한다. 이는 행동적으로 동일한 후보들이 반복적으로 재평가됨으로써 발생하는 지수적 탐색 공간 팽창을 초-래한다.

방법론

저자들은 수정되지 않은 $\mu$Kanren 코어 위에 구축된 두 개의 작은 라이브러리 combinator를 제안하여, bottom-up PBE 합성와 관계형 프로그래밍 사이의 간극을 메운다. 이 combinator들은 호스트 탐색 규칙을 변경하지 않으면서 bottom-up enumeration과 관찰적 중복 제거를 도입한다.

1. prune Combinator

첫 번째 combinator인 prune은 사용자 제공 키 함수(key function)를 기반으로 답변 스트림을 필터링한다.

• 메커니즘: 하나의 goal을 감싸며, 키 함수의 서로 다른 값(예: 후보 표현식의 입출력 동작)당 최대 하나의 상태(state)만을 방출한다.
• Logic Variable 처리: 키가 결합되지 않은(unbound) 논리 변수에 의존하는 경우를 처리하기 위해, prce는 sentinel 값(skip-prune)을 사용한다. 만약 term이 아직 ground가 아니어서 키를 계산할 수 없는 경우, 해당 상태는 중복 제거 테이블에 기록되지 않은 채 방출된다. 이 상태는 변수가 바인딩되어 term이 ground가 된 후에야 중복 제거의 대상이 된다.
• 범위: 중복 제거는 호출당 엄격하게 적용된다. "외부 변수로 보임"과 "내부 변수로 보임"을 혼동하여 재귀적 정의의 완전성(completeness)을 해치는 것을 방지하기 위해, 각 prune 호출 시마다 새로운 해시 테이블이 생성된다.

2. defrel/bank Combinator

두 번째 combinator인 defrel/bank는 prune을 확장하여, relation의 모든 호출 지점에서 공유되는 중복 제거를 통해 진정한 bottom-up enumeration을 달성한다.

• Canonical Variables: 이 방식은 가장 일반적인(most general) relation 호출을 나타내는 canonical fresh variables(빈 상태의 첫 $N$개 fresh variable)에 대해 relation을 메모이제이션한다.
• "Bank": relation의 본체(body)는 이 canonical variables에 대해 단 한 번 실행되어 canonical stream("bank")을 생성한다. 이 스트림은 bottom-up으로 구축되며, 각 동치류(equivalence class)당 정확히 하나의 대표자를 포함한다(결정 기준은 #:prune 키).
• Replay: 이후의 호출은 본체를 다시 실행하지 않는다. 대신, canonical substitution을 호출자의 특정 인자들에 대해 **재생(replay)**한다. 이는 canonical substitution을 순회하고, 내부 변수들을 호출자의 네임스페이스로 이름 변경하며, 결과를 호출자의 인자와 유니파이(unify)하는 과정을 포함한다.
• 효율성: 이 접근 방식은 (run ...) 쿼리당 중복 제거 작업이 단 한 번만 수행되도록 보장한다.

3. defrel/bank-w 변형 (Best-First)

표준 defrel/bank는 depth-first recursion을 사용하여 enumeration 순서에 편향(bias)을 준다(예: 덧셈보다 곱셈의 right-spine chain을 선호함). target solution이 canonical order 상에서 깊은 곳에 위치하는 경우를 해결하기 위해, 저자들은 가중치가 부여된 defrel/bank-w를 도입한다.

• Weighted Streams: 이 변형은 미성숙한(immature) 스트림 셀에 허용 가능한 상한값(admissible upper bounds, weights)을 부착한다.
• Depth-Decay: 재귀 호출 지점에서 가중치에 decay factor가 적용된다. 이는 더 얕은(shallower) 대표자들이 더 낮은 가중치를 갖게 하여, 정렬된 merge 로직(mplus-w)에 의해 먼저 방출되도록 보장한다.
• Lazy Heuristics: 시스템은 가중치를 peek만 하고 underlying thunk를 강제(force)하지 않는 "lazy-ceiling" discipline을 사용하여, canonical stream 구축 중에 무한 루프에 빠지는 것을 방지한다. 이는 가중치 ceiling이 허용 가능한 휴리스틱 역할을 하는 A*-style 탐색을 구현한다.

주요 기여

1. prune: 사용자 제공 함수에 의해 키가 결정되는, 범용적인 answer-stream 중복 제거 combinator이며, term-level 함수를 prune 키로 격상시키기 위한 헬퍼(ground-key, when-ground)를 지원한다.
2. defrel/memo 및 defrel/bank: Canonical fresh variables에 대한 relation memoization을 위한 combinator이다. defrel/bank는 특히 공유된 중복 제거를 가진 bottom-up enumeration을 제공하여, 표준 PBE의 "worklist" 패턴을 관계형 환경으로 성공적으로 이식한다.
3. defrel/bank-w: 미성숙한 스트림에 가중치를 사용하는 depth-decayed best-first 변형으로, 이를 통해 canonical order에서 놓칠 수 있는 compact한 대표자들을 찾을 수 있게 한다.
4. Implementation Tricks: 메모이제이션된 방식이 depth-bounded baseline과 경쟁할 수 있도록, 정렬된 merge를 위한 pairing heap 사용 및 "thunk-collapse" 기법과 같은 엔지니어링 최적화를 상세히 설명한다.

결과

저자들은 산술 및 문자열 PBE 벤치마크(깊이 0–6)에 대한 예비적 경험적 평가를 제시한다.

• 성능 향상: 8개의 심층 산술 타겟 중 6개에 대해, defrel/bank는 depth-bounded baseline(bounded)보다 9–99배 빠르다. 이는 bank가 매 재귀 레벨마다 sub-expression을 재차 pruning하는 것을 방지하기 때문이다.
• Enumeration Order Bias: defrel/bank의 성능은 enumeration 순서에 크게 의존한다. 이 방식은 target solution이 canonical depth-first order의 앞부분에 위치할 때(예: $x^k$ 또는 $x^k + c$) 탁월한 성능을 보인다. 그러나 $(1+x)^k$와 같이 canonical stream의 매우 늦은 위치(예: depth 4에서 243,158번째 위치)에 나타나는 타겟에 대해서는 어려움을 겪거나 타임아웃이 발생한다.
• Best-First Trade-offs: defrel/bank-w는 $(1+x)^k$와 같은 타겟에 대해 compact한 대표자를 조기에 찾아낸다. 그러나 "breadth-first cost"를 수반한다. 즉, depth-$K$ 셀을 방출하려면 depth $<K$인 모든 셀을 방출해야 한다. 행동 공간이 넓은 경우(depth 3에서 수천 개의 서로 다른 behavior 존재), 이는 defrel/bank가 성공하는 깊은 산술 타겟에서 타임아웃을 유발한다.
• Host Baseline과의 비교: 비관계형 호스트 언어 baseline(host-bank)은 얕은 타겟과 $(1+x)^k$ 계열에서는 잘 작동하지만, 관계형 엔진 외부에서 exhaustive한 bank를 구축하는 비용 때문에 깊은 right-spine 타겟에서는 처참하게 실패한다. defrel/bank는 관계형 인터페이스를 유지하면서도, enumeration bias가 유리한 경우 host-bank의 속도 향상을 대부분 회복한다.

의의 및 주장

본 논문은 이러한 combinator들이 호스트 탐색 규칙을 변경하거나 관계형 패러다임을 떠나지 않고도, 관찰적 중복 제거를 동반한 bottom-up enumeration이라는 표준 도구를 관계형 설정으로 성공적으로 가져왔음을 주장한다.

• Opt-in Semantics: 이 접근 방식은 엄격하게 선택적(opt-in)이다. 이는 표준 miniKanren relation의 의미론을 변경하지 않으며, 중복 제거는 prune으로 감싸거나 defrel/bank로 정의된 relation에만 적용된다.
• 완전성(Completeness): 저자들은 pruning이 사용자 제공 동치 관계에 대해 완전성을 보존한다고 주장한다. 즉, 모든 behavior에 대해 적어도 하나의 대표자가 발견된다.
• 한계점: 저자들은 평가가 예비적이며, 두 가지 도메인(산술 및 문자열)에 국한되어 있고 특정 문법에 의존한다는 점을 언급하며 연구의 범위를 겸허히 밝힌다. 또한 defrel/bank가 보편적인 솔루션은 아니라는 점을 인정하는데, 그 성공 여부는 target의 형태와 enumeration order 사이의 상호작용에 달려 있기 때문이다. 그들은 fair conjunction이 defrel/bank의 enumeration bias를 해결할 수 없다고 명시하는데, 이는 bias가 cell이 어떻게 interleaving되는가가 아니라, bank에 어떤 cell이 존재하는가에 있기 때문이다.
• 향ari Work: 논문은 $(1+x)^k$ bias를 breadth-first cost 없이 해결하기 위한 canonical body에 대한 iterative deepening, saturation detection, 그리고 더 풍부한 constraint store 및 기타 PBE 도메인(예: bit-vectors, lists)으로의 확장 등 향후 연구 방향을 제시한다.

요약하자면, 본 논문은 canonical 변수들에 대해 relation을 메모이제이션하고 관찰적 동치성에 의해 pruning함으로써, enumeration order가 target의 구조와 일치하는 경우 관계형 PBE 합성에서 상당한 성능 향상을 달성할 수 있음을 보여준다.