증명언어 얘기를 해도 대부분 사람들은 증명언어가 어떤건지 감도 안잡힐 거라고 생각해
근데 지난번에 증명하다가 설명하기 괜찮은 예시를 찾아서 글 써봄

우선 내가 구현하고자 하는건 "α라는 nonempty 문자열이 있을 때, α의 nonempty prefix들 중에서 α와 commute하는 가장 짧은 문자열 ω를 찾는 알고리즘" 이야.
여기서 α와 β가 commute한다는건 α ++ β = β ++ α를 뜻해. 간단하게 [α, β] 라고 표기하겠음.
척 보면 알겠지만 그리 어려운 문제는 아님.
α의 nonempty prefix 들을 길이 순서대로 쭉 나열해두고, 짧은것부터 α와 commute하는지를 테스트해서 성공할 경우 해당 문자열을 결과로 주면 되.

예를들어서 α = [1,2,3,1,2,3] 이라 고 하자. α의 nonempty prefix는
[1], [1,2], [1,2,3], [1,2,3,1], [1,2,3,1,2], [1,2,3,1,2,3] 가 전부다.
[1,2,3,1,2,3] ++ [1,2,3] = [1,2,3] ++ [1,2,3,1,2,3] = [1,2,3,1,2,3,1,2,3] 이므로 [1,2,3]은 α와 commute하고 이게 α와 commute하는 가장 짧은 문자열이야.

하스켈로 구현해보자면 아래처럼 할 수 있음.

commute xs ys = xs ++ ys == ys ++ xs generator xs = case find (commute xs) (tail . inits $ xs) of Just ys -> ys Nothing -> xs

inits xs 는 xs의 모든 prefix를 길이순으로 담은 리스트를 리턴하는 함수인데, nonempty prefix만 구하고 싶으니까 앞에 tail을 붙인거야.

이 리스트를 앞에서부터 훑으면서 commute xs 를 만족하는 원소를 리턴하면 원하는 문자열을 얻을 수 있음.
미묘한 부분은 Nothing 케이스에서 리턴하는 xs인데, 이거는 사실 필요가 없다.
α ++ α = α ++ α 는 자명하기 때문에 [α, α]는 항상 만족됨.
또 α는 inits α 의 마지막 원소이기 때문에 find가 Nothing을 리턴하는 일은 일어나지 않아.

즉 위 코드를

generator xs = case find (commute xs) (tail . inits $ xs) of Just ys -> ys Nothing -> error "xs == []"

이렇게 바꿔도 전혀 문제되지 않음. xs가 []면 결과가 undefined가 되기는 하지만, 애초에 xs를 nonempty list로 가정했으니 이건 무시하자.

뭐 아무튼 하스켈에서의 undefined, error 혹은 C/C++의 assert(false) 같은게 프로그래밍을 하다보면 심심치 않게 등장하는데,
사실 이런 코드는 어찌 보면 언어의 표현력이 부족해서 발생하는 일임.
프로그래머는 프로그램의 행동을 논증할 수 있지만, 프로그래밍 언어에 그런걸 표현할 방법이 없으니 프로그래머의 사고와 실제 코드 사이에 갭이 생기는거지.

반명 증명언어에서는 프로그래머의 사고와 실제 코드가 완전히 매치가 됨.

아래는 agda로 위 알고리즘을 구현한 코드야

αs : List (V *) αs = inits′′ α αs-Any : Any ([ α ,_]) αs αs-Any = subst (Any [ α ,_]) (cong inits′′ (++-identityʳ α)) (lookup-any (inits′′ (α ++ [])) i p) where i = indexOfInits′′[ α ++ [] ] α≢ε eq = lookup-indexOfInits′′[ α ++ [] ] α≢ε p = subst [ α ,_] (sym eq) ([,]-refl α) αs-First : First (∁ [ α ,_]) [ α ,_] αs αs-First = Sum.[ id , (λ αs-All → ⊥-elim (All¬⇒¬Any αs-All αs-Any)) ]′ (first (Sum.swap ∘ Sum.fromDec ∘ [ α ,_]?) αs) i : Fin (length αs) i = First.index αs-First ω : V * ω = lookup αs i

inits′′는 nonempty prefix들의 리스트를 구해주는 함수야 (tail . inits 랑 같다고 생각해도 됨)
그러니까 αs를 α의 nonempty prefix들로 정의한거지.


agda에서 조건을 만족하는 첫번째 원소를 찾는 함수는

first : Π[ P ∪ Q ] → Π[ First P Q ∪ All P ]

인데 간단하게 설명을 해줄게.

우선 P, Q는 리스트의 원소 A에 대한 predicate고 First P Q랑 All P는 List A에 대한 predicate임.

First P Q는 P를 만족하는 원소들이 연달아 나온 뒤 Q를 만족하는 원소가 하나 나온다는 뜻이고

All P는 리스트의 모든 원소가 P를 만족한다는 뜻임.

정규식 같은 슈도 코드로 표현해보자면

First P Q = [P]*[Q].* All P = [P]*

정도로 쓸 수 있겠음.


이제 first가 의미하는 바를 설명하자면

임의의 x : A 에 대해서 P x 혹은 Q x 둘중에 하나는 반드시 참이라는 조건이 있어.
그러면 임의의 리스트 xs : List A는 First P Q, 나 All P 둘중 하나를 만족한다는 퍽 당연한 소리다.
하스켈 find 하고 비교하자면 결과값이 Just x 가 되는 케이스는 First P Q를 만족하는거고, Nothing이 되는것은 All P를 만족하는 경우라고 생각하면 되.

find :: Foldable t => (a -> Bool) -> t a -> Maybe a

first는 일반화를 위해서 P, Q라는 두 predicate에 대해 정의가 되어 있는거라서 P = ¬ Q 인 경우, 즉

first : Π[ ¬Q ∪ Q ] → Π[ First ¬Q Q ∪ All ¬Q ]

으로 생각해야 하스켈 find하고 대응이 더 잘 될거야.

(Q에 대해서 배중률이 성립한다면 Q를 만족하는 첫번째 원소가 존재하거나, 모든 원소가 Q를 만족하지 않는다.)


다시 위 구현으로 돌아가서, 증명하고 싶은건 αs가 First ¬P P 를 만족 한다는거야. 여기서 P β = [ α , β ].

그러니까 αs의 원소중 α와 commute하는 첫번째 문자열이 존재한다는거임.


이걸 어떻게 증명하느냐? 이 코드를 다시 생각해 보면 됨.

generator xs = case find (commute xs) (tail . inits $ xs) of Just ys -> ys Nothing -> error "xs == []"

여기서는 case에서 Nothing에 매칭되는 일이 발생할 수 없음을 확신했으니까 error를 사용하는게 문제없다고 할 수 있었음.

agda에서 error같은걸 쓰려면 저게 불가능한 일이란걸 진짜로 증명해야 해.

그니까 first의 결과로 나오는 두가지 케이스 First ¬P P, All ¬P 중에서 All ¬P 가 나오는게 불가능 하단걸 증명하는거지.


αs의 마지막 원소인 α가 P를 만족하므로 All ¬P가 거짓이란건 간단하게 증명할 수 있다.
agda 코드를 보면 먼저 αs-Any를 증명한 다음 αs-All과 αs-Any로 부터 모순을 이끌어내서 αs-First를 증명하고 있음.
αs-First를 증명 했으면 그냥 리스트 인덱싱으로 ω를 바로 구할 수 있음


전체 agda 코드는 여기서 볼 수 있음 (예전에 올린적 있음)

https://github.com/damhiya/AgdaFormalLanguage/blob/master/FormalLanguage.agda


설명이 길었는데, 결국 말하고 싶었던건 증명언어는 프로그래머의 논리를 주석이 아닌 소스코드에 100% 표현할 수 있는 프로그래밍 언어라는 거야.