특히 지금, 수학 분야에서 AI의 성공이 대대적으로 알려지면서, 저는 왜 여전히 Rocq를 사용하고 하이프에 굴복하여 Lean으로 전환하지 않는지에 대한 질문을 받습니다. 이 포스트의 대부분은 최근 LangSec 기조연설의 도발적인 제목 슬라이드로 시작되었습니다: “프로그램 검증을 위해 Rocq가 Lean보다 나은 이유.”
여기서 논쟁을 일으키려는 것은 아닙니다. 저보다 성숙한 분이라면, 아래에서 ‘더 낫다(better)’라는 단어를 마음속으로 ‘오늘 제 작업에 더 적합하다(a better fit for my work today)’로 대체해도 괜찮습니다. 시작하기 전에 한 가지 주의사항이 더 있습니다: 이 포스트는 수학을 형식화하는 것이 아니라 프로그램 검증에 관한 것입니다. 이 점에 대해서는 Lean이 실제로 큰 추진력을 가지고 있다는 것을 기꺼이 인정하겠습니다.
언어 수준의 문제점
Coinductive 타입과 cofixpoint
Wojciech Różowski와 Joachim Breitner가 Lean FRO에서 개발한 바에 따르면, Lean은 coinductive predicate를 지원하게 되었습니다. 이 기능은 coinductive 명령어로 (구현) Lean 4.25에 포함되었습니다. 이는 bisimulation 및 기타 coinductive 증명에 유용하지만, 실행 가능한 cofixpoint나 추출할 수 있는 프로그램은 제공하지 않습니다.
저는 또한 실제로 실행할 수 있는 Type 내의 codata를 원합니다. Rocq는 이를 CoInductive와 CoFixpoint로 직접 제공합니다. Lean에는 이에 상응하는 선언이 Type에 없습니다. 그 대안들은 일반 함수나 구조체, 또는 라이브러리 인코딩을 사용합니다.
제가 찾은 Rocq 스타일의 codata 선언과 가장 유사한 Lean 실험적인 기능은 Alex Keizer의 QPFTypes입니다. 이는 범용 codata를 위한 개념 증명 패키지입니다. 이 패키지의 codata 명령은 사양(specification)을 라이브러리 인코딩으로 변환하고 소멸자(destructor), corecursor, 그리고 bisimulation 원리를 생성합니다. Rocq의 CoInductive와 달리, 이는 커널 선언이 아닙니다. 예제들은 QPFTypes가 고정된 Lean 4.25.0 툴체인(포스트 작성 시점 기준 최신 지원 버전)을 사용합니다.
codata 선언하기
QPFTypes가 고정된 Lean 4.25.0 툴체인(포스트 작성 시점 기준 최신 지원 버전)을 사용합니다.
codata 선언하기
이것을 QPFTypes에 대한 비난으로 말씀드리는 것은 아닙니다. README에 '개념 증명(proof of concept)'이라고 명시되어 있습니다. 하지만 Rocq에서는 완전히 평범한 예제에서도 그 거친 부분이 빠르게 드러납니다. 예를 들어, Rocq는 이 매개변수 없는 coinductive type을 직접 허용합니다:
CoInductive co_unit : Type :=
| co_unit_loop : co_unit.
codata CoUnit where
| loop : CoUnit
/--
...
이것은 구현 버그로 치부할 수 있지만, 다음 두 가지는 구조적인 문제입니다. 상호 coinductive 선언은 Rocq에서는 일상적이지만 QPFTypes에서는 지원되지 않습니다:
CoInductive tree (a : Type) : Type :=
| node : a -> forest a -> tree a
with forest (a : Type) : Type :=
...
mutual
codata Tree α where
| node : α → Forest α → Tree α
...
인덱싱된 coinductive family 역시 Rocq의 일반적인 coinductive 조각에 속하지만 QPF 인코딩 외부입니다. 이 예시에서 인덱스는 매 단계마다 증가하는 클럭이며, 이러한 패턴은 프로토콜, 페이즈, 크기 및 상태 기계에서도 발생합니다:
CoInductive istream (a : Type) : nat -> Type :=
| icons : forall n, a -> istream a (S n) -> istream a n.
codata IStream α : Nat → Type where
| icons : α → IStream α (n + 1) → IStream α n
/--
...
내부적으로 QPFTypes는 Cofix 메커니즘을 생성합니다. codata 명령어는 간단하고, 상호적이지 않으며, 인덱싱되지 않은 경우 대부분을 숨겨주지만, 이 조각을 벗어나면 저수준의 MvQPF.Cofix.corec 및 bisim API를 직접 호출하거나 운이 좋지 않습니다. Rocq에서는 위의 예제들이 단지 선언일 뿐입니다.
Rocq의 직접적인 지원이 순탄하지 않다는 것은 누구나 알고 있습니다. 그 가드성 검사기(guardedness checker)와 논쟁해 본 사람은 모두 그렇게 압니다. 증명 측면에서도 Rocq 사용자는 Paco나 Damien Pous의 coinduction 라이브러리와 같은 성숙한 도구를 가지고 있습니다. 이들은 coinductive 술어 및 관계에 도움이 되지만, 프로그램용 CoFixpoint을 대체하지는 못합니다.
cofixpoints 추출하기
네이티브 Rocq cofixpoint는 실제 지연(lazy) OCaml 값으로 추출됩니다. 예를 들어, 제가 작업했던 게임 트리 라이브러리에서 Rocq의 unfold_cotree 함수는 다음과 같이 추출됩니다:
type 'a cotree = 'a __cotree Lazy.t
and 'a __cotree =
of 'a * 'a cotree colist
...
반면, QPFTypes를 사용하면 구성(construction)과 관찰(observation) 과정은 일반적인 MvQPF.Cofix.corec 및 MvQPF.Cofix.dest 연산을 거칩니다. 이 경우 프로그램은 위와 같은 직접적인 지연 트리 형태가 되는 대신, 일반적인 Cofix 표현을 유지합니다. 이는 수학적으로는 괜찮지만, 제가 손으로 작성할 프로그램은 아닙니다.
만약 QPFTypes를 직접 살펴보고 싶다면, BadCoinduction.lean 파일에 이 섹션의 전체 실험 내용이 담겨 있습니다. 여기에는 Colist 및 Cotree 정의, 생성된 인터페이스 예시, 그리고 매개변수 없는(parameterless), 상호(mutual), 인덱싱된(indexed) 코데이터에 대한 검증 실패 사례가 포함되어 있습니다. 이 파일의 헤더는 테스트를 다시 실행하는 데 필요한 정확한 QPFTypes 커밋과 명령을 기록하고 있습니다.
현재 Lean 대안들
이 지점에서, 한 Lean 개발자는 화면을 향해 소리칠지도 모릅니다. 'QPFTypes를 단지 스트림을 작성하기 위해 사용하는 사람은 아무도 없다!' 충분히 이해합니다. QPFTypes가 존재하는 이유는 Rocq 스타일의 코데이터 선언에 가장 가깝기 때문입니다. 일상적인 Lean 사용에서는 몇 가지 다른 트릭들을 사용합니다.
스트림(stream)의 경우, mathlib의 Stream'이 명백한 답입니다. 이는 단순히 위치 n을 요청하여 요소를 하나 얻는 Nat → α와 같습니다. 이 코드는 실행되며, mathlib은 확장성(extensionality), 비시뮬레이션(bisimulation), 그리고 coinduction 보조정리들을 함께 제공하므로 증명하기에 편리합니다. 하지만 이는 꼬리가 또 다른 스트림인 지연 생성자(lazy constructor)는 아닙니다. 이는 임의의 상호 또는 인덱싱된 코데이터를 해결하는 것이 아니라, 스트림을 해결합니다.
또 다른 옵션은 명시적인 상태 기계(state machine)입니다. 일부 상태를 유지하고, 단계 함수(step function)를 작성한 다음, 이를 corecursor로 사용하는 것입니다. Lean의 현재 Iter 인터페이스는 이러한 패턴을 시퀀스에 패키징하여, 필요할 때마다 한 단계씩 계산합니다. 이터레이터(iterator)는 결국 값을 산출하거나 종료될 것이라는 Productive 증명을 가질 수 있습니다. Iter.repeat
이미 가지고 있습니다. 사용자 정의 이터레이터(iterator)를 사용할 경우, 저는 스텝 인터페이스(step interface), 그 불변성(invariants), 그리고 어쩌면 그 생산성 증명(productivity proof)까지 제공해야 합니다. 이것은 작동하지만, 이제 제가 상태 기계(state machine)와 시퀀스 사이의 배관 작업(plumbing)을 직접 해야 합니다. Rocq의 CoFixpoint는 재귀 호출에 대해 가드된지(guardedness) 확인하고 공수적 값(coinductive value)을 직접 제공합니다.
Thunk는 게으름(laziness)은 사주지만, 공수적 추론(coinduction)은 해주지 않습니다. 컴파일된 Lean은 thunk가 강제될 때까지 지연시키고 그 결과를 캐시합니다. 이 논리(logic)는 Unit → α를 보게 되는데, 이는 thunks를 포함하는 전체 정의(total definitions)가 증명에 계속 사용 가능함을 의미하지만, 캐싱은 눈에 보이지 않습니다. thunk는 재귀를 허용하지도 않고, 재귀가 결국 생성자(constructor)를 산출한다는 것을 확인해주지도 않습니다. 추출된 Rocq cofixpoint는 그 재귀가 가드됨 검사기(guardedness checker)를 통과한 후에만 유사한 런타임 게으름을 사용합니다.
partial def는 투박한 도구입니다. 컴파일러가 재귀 본문(recursive body)을 실행하지만, 논리(logic)는 불투명한 상수(opaque constant)만을 얻습니다. Lean은 여기서 종결성(termination)이나 생산성(productivity)을 확인하지 않습니다. 자연수(natural numbers)의 thunk를 생성하는 프로듀서와 즉시 자신을 무한히 호출하는 프로듀서를 모두 받아들입니다. unsafe def도 실행되지만, 정리 안전(theorem-safe) 선언에서는 전혀 언급할 수 없습니다. Batteries의 MLList는 일반적인 구성을 보여줍니다: 비공개 unsafe lazy 구현, 불투명한 공개 인터페이스, 그리고 fix와 iterate 같은 프로듀서들은 partial def로 작성됩니다. 이 프로듀서들은 관찰된 Rocq cofixpoint가 할 수 있는 방식대로 증명에서 전개(unfold)될 수 없습니다. Lean에는 방정식(equations)을 유지하는 partial_fixpoint도 있지만, 이러한 종류의 생성자-thunk 재귀는 받아들이지 않습니다.
QPFTypes는 그 불투명성(opacity)을 피합니다: 코어커서(corecursor)와 비시뮬레이션 원리(bisimulation principles)를 제공합니다. 하지만 그러면 저는 다시 일반적인 Cofix 표현과 제가 위에서 테스트한 선언 제한에 직면하게 됩니다.
왜 저는 스트림(streams) 이상의 것에 대해 걱정하고 있을까요? 상호작용 트리(Interaction trees)가 그렇습니다. Rocq의 상호작용 트리 라이브러리는 효과적이며, 종료되지 않을 수도 있는 프로그램들을 공귀납적 트리(coinductive trees)로 표현합니다. 저는 이를 사용하여 프로그램을 작성할 수 있고, 해석하며, 일반적으로 약한 비동일성(weak bisimulation)까지 동일한 트리에 대한 방정식을 증명할 수 있습니다. Stream'
그리고 Iter는 저에게 시퀀스만을 제공할 뿐, 효과에 필요한 분기되는 연속(branching continuations)은 주지 못합니다. 저는 손으로 작성한 효과 트리(effect tree)를 Thunk와 partial def로 실행할 수는 있지만, 그러면 재귀 프로듀서가 증명에는 불투명하게 됩니다. 이 모든 것을 Lean에 구현하려면 코데이터(codata)의 라이브러리 인코딩이 필요합니다.
MIT PLV의 lean4-itree는 Mathlib의 PFunctor.M를 사용하여 상호작용 트리에 대해 이를 수행합니다. 더 새로운 PolyFun은 핸들러, 재귀 절차, 추적(traces), 강한 비동일성 및 약한 비동일성을 추가하고 모나드(monad)와 반복 법칙(iteration laws)의 증명을 제공합니다. 저는 이 트리들을 사용하여 계산하고 그들에 대해 Lean에서 무언가를 증명할 수 있습니다. 하지만 여전히 라이브러리 인코딩된 M-타입입니다. Lean에는 여기에 네이티브 코데이터 선언이 없으며, 계산은 Rocq가 추출하는 직접적인 지연 프로그램(lazy program)을 생성하기보다는 일반적인 표현을 유지합니다.
HITrees는 이 문제의 해결책이 아닙니다. 저자들은 ITrees에서 사용된 공귀납적 지연 모나드(coinductive Delay-monad) 접근 방식을 고려하지만, Lean에 네이티브 공귀납적 타입이 없기 때문에 배제됩니다. 그들의 트리는 대신 귀납적(inductive)이며, 비종료성(nontermination)은 고계 재귀 효과(higher-order recursion effect)가 됩니다. 재귀 계산은 더 이상 제가 관찰하고 펼칠 수 있는 무한한 트리가 아니며, 그 재귀는 핸들러가 효과를 해석할 때만 의미를 갖게 됩니다. 모나드적 해석은 그것을 실행할 수 있고, 증명은 상태 기계 해석(state-machine interpretation)을 거칠 수 있지만, HITree의 방정식 이론은 일반적인 재귀 전개 방정식을 제공하지 않습니다. 작동합니다. 또한 비종료성을 트리 밖으로, 인터프리터 안으로 옮기는데, 저는 이것이 가드된 Rocq 코픽스포인트(guarded Rocq cofixpoint)를 작성하는 것보다 더 어색하다고 생각합니다.
Lean의 경우, 저는 이 중 하나를 포기하거나 일반적인 메커니즘 위에 다시 구축해야 합니다. Rocq는 제가 코데이터(codata)를 선언하고, 가드된 프로듀서(guarded producer)를 작성하며, 관찰을 통해 그것에 대해 추론하고, 직접적인 지연 코드(lazy code)를 추출할 수 있게 해줍니다. 이것이 바로 제가 코귀납법(coinduction)에서 원하는 것입니다.
중첩 유도 타입 및 술어 (Nested inductive types and predicates)
Meven Lennon-Bertrand가 이 점을 지적해 주었고, 저는 아래 예시를 확장했습니다. Lean은 많은 중첩된 유도 정의(nested inductive definitions)를 수용하지만, 그 검사기(checker)는 Rocq가 허용하는 일부 정의들을 거부합니다. 제가 A Rose Tree Is Blooming이라는 증명 작품을 작성하던 중에 이 문제에 부딪혔는데, 이는 Rocq의 특정 부분을 활용하며 Lean에서는 상당히 보기 흉하게 작성되었을 것입니다. 장미나무 예시는 이번 포스팅에는 너무 크므로, 여기서는 JSON 스키마를 이용한 동일한 문제를 보여드리겠습니다.
JSON 스키마 언어를 가지고 있고 검증(validation)에 관한 일반적인 것들—필드 이름이 일치하고, 스키마에서 필드를 제거하는 것이 안전하며, 접두사(prefix)를 검증하는 것이 작동한다는 것—을 증명하고 싶다고 가정해 봅시다. 이는 검증된 시스템을 구축할 때의 루틴한 작업입니다. JSON과 스키마를 정의하는 것은 두 언어 모두에서 어려움이 없습니다:
Inductive json : Type :=
| jnull : json
| jstr : string -> json
...
inductive JSON where
| null : JSON
| str : String → JSON
...
흥미로운 부분은 검증 관계(validation relation)입니다. { "name": string, "age": number }와 같은 객체 스키마는 필드 이름을 쌍별로 확인하고 각 값이 해당 하위 스키마에 대해 유효한지 검사함으로써 { "name": "Alice", "age": 30 }과 같은 객체를 검증해야 합니다. Rocq는 이 모든 것을 하나의 Forall2 전개(derivation) 안에 저장할 수 있습니다:
Inductive valid : schema -> json -> Prop :=
| valid_any : forall j, valid sany j
| valid_str : forall s, valid sstr (jstr s)
...
여기서 투영(projections)은 의도적입니다. Rocq 9.0은 재귀 발생 지점 주변의 동등한 튜플 패턴 람다를 비엄격하게 양수(non-strictly positive)로 거부합니다. 그 구문 검사기(syntactic checker)는 이 패턴 매치를 통과하지 못합니다. 위의 투영 기반 선언은 컴파일됩니다.
Lean 4.32.1은 상응하는 객체 생성자(object constructor)를 거부합니다:
inductive ValidCombined : Schema → JSON → Prop where
| obj :
Forall₂
...
error: (kernel) invalid nested inductive datatype 'And',
nested inductive datatypes parameters cannot contain local variables.
Lean은 여러 유사한 형태를 허용합니다: Forall₂ ParRed,
And를 통한 직접 재귀(direct recursion) 및 Exists,
그리고 Forall₂ (fun sf jf => Valid sf.2 jf.2)입니다. 거부된 선언에서는, 재귀적 발생이 Forall₂와 And를 모두 통과하며, 커널은 내부의 And를 보고합니다. 다른 경우인 Forall₂ (Eval env)는 Forall₂에서 실패하는데, 이는 그 관계 매개변수(relation parameter)가 생성자-지역 변수(constructor-local)인 env를 포획하기 때문입니다.
Lean은 결합된 관계(combined relation)를 두 개의 Forall₂ 도출(derivation)로 분리하여 리스트 구조를 유지할 수 있습니다:
inductive Valid : Schema → JSON → Prop where
| obj :
Forall₂
...
인덱스나 별도의 길이 증명(length proof)이 필요하지 않습니다. 헤드(head)를 제거하는 것은 구조적(structural)으로 남아 있지만, Lean은 두 도출을 모두 분해해야 합니다:
Lemma Forall2_tail :
forall (A B : Type) (R : A -> B -> Prop)
(a : A) (b : B) xs ys,
...
theorem Valid.dropHead
(hv : Valid (.objS ((k, s) :: schemaFields))
(.obj ((k', j) :: jsonFields))) :
...