증명언어는 Agda Coq 밖에 안써봤고 둘다 그렇게 깊이 아는건 아니지만 암튼 함 비교해봄


문법

Agda는 Haskell, Coq는 Ocaml의 영향을 받았지만

Agda는 Haskell 문법에서 거의 달라지지 않았고, Coq는 좋은쪽으로 상당히 바뀜

(적어도 Coq는 ML에서 쓰는 'a list 같은 구시대적 문법은 없음)

근데 사실 Agda는 연산자 정의를 미친듯이 쓰고 Coq는 어차피 tactic을 쓰기때문에 둘다 Haskell/Ocaml 이랑은 상당히 다르게 보임.


설탕

일단 Coq는 소스에 유니코드 특수문자은 잘 안씀. 아마 나온지가 오래되서 그럴지도 몰라.

반면 Agda는 그리스 문자나 수학기호로 떡칠함.

좀 더 고차원의 설탕이 필요할때는 Agda에는 연산자 정의랑 syntax 키워드, Coq에는 Notation이 있음.

agda 연산자 정의는 identifier 자체를 연산자로 정의하는거고, notation은 그냥 표기법만 바꿔주는거.

둘다 기능은 비슷한것 같은데. 개인적으로는 Agda가 훨씬 편했음. Coq Notation은 점심 나가서 먹을것 같아


재귀

증명언어에서는 모든 함수가 종료해야 하기때문에 재귀에 제약이 걸림.

근데 Agda랑 Coq는 컴파일러가 종료를 보장해주는 범위가 살짝 다름.

Agda는 structural recursion, Coq은 primitive recursion을 쓰는데

결론만 말하자면 structural recursion이 좀 더 유연하지만 둘다 할수 있는건 같음.


primitive recursion은 팩토리얼, structural recursion은 피보나치를 생각하면 된다

fac 0 = 1 fac (S n) = (S n) * fac n fib 0 = 0 fib 1 = 1 fib (S (S n)) = fib n + fib (S n)

fac (S n) 은 fac n 을 재귀적으로 호출하고 이때 S n -> n으로 정확하 1단계만큼 destruct가 일어남.

반면 fib (S (S n)) 은 fib n과 fib (S n) 을 재귀적으로 호출하기 때문에 S (S n) -> n, S n 으로 1단계, 혹은 2단계의 destruct가 일어남.

이것처럼 생성자가 정확히 1단계만 벗겨지면 primitive recursion, 생성자가 임의의 상수 횟수만큼 벗겨지면 structural recursion이라고 부름.

당연히 structural recursion이 primitive recursion을 포함함.

(structural induction은 자연수의 strong induction 보다는 약함.

자연수에서 structural induction을 쓸때 n에서 n/2 로 재귀호출을 하는건 불가능함.)


Coq는 primitive recursion만 가능해서 위에서 보여준 fib같은걸 정의하려면 저걸 primitive recursion으로 변환해서 정의해야 함.

예를들어서

fib_aux 0 = (0,1) fib_aux (S n) = let (x,y) = fib_aux n in (y, x+y) fib n = fst (fib_aux n)

Agda는 그냥 structural recursion 쓰면 알아서 종료검사 해줌.


뭐 어차피 둘다 ackermann 함수같은 더 복잡한 재귀는 well-foundedness 써서 primitive/structural recursion으로 변환해서 해야됨

(이것도 Coq는 Program Fixpoint같은게 따로 있고, Agda는 별다른 키워드 없음)

타입체커가 작을수록 검증하기 쉽다는점에서는 primitive recursion만 제공하는게 나을지도..

근데 어차피 내가 증명언어 타입체커에서 에러찾을 확률은 없으니까 아무거나 맘놓고 쓰자.


증명

Agda랑 Coq이 제일 차이 나는 부분임.

Agda는 손으로 직접 재귀함수 작성해서 깡으로 증명하고 Coq는 tactic 써서 함.

(Agda도 tactic이 있는것 같던데 이건 증명이 끝나면 tactic상태로 저장하는게 아니라 Agda 함수 정의로 변환해서 저장하는듯)

이건 둘다 장단점이 있기 때문에 다 있어야 좋을것 같은데 Agda나 Coq는 그렇지가 못한것 같음.

term가지고 직접 프로그래밍을 해야하면 Agda가 압도적으로 편함.

왜냐면 agda는 아까 말했듯이 structural recursion이 있고,

dependent pattern matching에서 타입체커가 자동으로 해주는게 많아서 굉장히 해볼만 함.

coq에서 match로 복잡한거 하기에는 상당히 괴로움.

그냥 tactic 쓰면 되지 않느냐 할 수 있는데, relevant 할때, 그니까 가능한 증명이 여러개이고 프로그램의 성격을 가질때는 tactic이 별로임.

tactic은 어떤 증명을 하는지가 아니라 증명 가능 여부에 최적화되있음.

대신 tactic은 훨씬 인간 친화적임.

tactic은 간단히 말해서 증명을 명령형으로 하는거라 리눅스 명령어 치듯 증명할 수 있음.

agda에도 hole이 있기는 하지만 tactic이 더 interactive함.


메타프로그래밍 (증명 자동화)

coq는 tactic 자체가 메타프로그래밍이기 때문에 이걸로 증명 자동화같은걸 되게 쉽게 할 수 있음

tactic을 잘 작성해서 자동화해두면 무지성 증명 가능.

다만 문제도 있는데, 복잡한 tactic은 시간이 굉장히 오래걸릴 수 있음. 증명에서 스텝 하나가 수분씩 걸리면 끔찍함.

agda도 메타프로그래밍 기능이 있는데 이건 내가 아직 못해봄. 그래서 비교하긴 힘들듯.


표준 라이브러리

증명언어에서 표준 아닌 라이브러리는 겁나 특수목적이니까 패스. 애초에 난 써본게 별로 읎음 (ex. HoTT, 4색정리, Verified C)

표준라이브러리는 개인적으로 생각할때 Agda가 훨씬 좋음.

일단 체계화가 굉장히 잘되있는데 예를들어서

IsPartialEquivalence

IsEquivalence

IsDecEquivalence

IsPreorder

IsTotalPreorder

IsPartialOrder

IsDecPartialOrder

IsStrictPartialOrder

IsDecStrictPartialOrder

IsTotalOrder

IsDecTotalOrder

IsStrictTotalOrder

이게 전부 equality/ordering 관련된 property 정의임.

솔직히 처음에는 질려버렸는데; 쓰다보니 필요성이 체감 됨


Coq는 표준 라이브러리에서 저런거 못봄.

그리고 맘에 안드는 함수가 많은데 가령

nth (n:nat) (l:list A) (default:A) : A

이런거. 리스트 인덱싱 하는 함수인데 리스트 범위 벗어낫을때 리턴할 값을 default 로 넘겨줘야됨.

하다못해 option 만 썼어도 이거보다는 나을듯.

대응되는 Agda 표준라이브러리 정의는 훨씬 깔끔함.

lookup : ∀ (xs : List A) → Fin (length xs) → A

애초에 인자로 리스트 범위 안에 들어오는 인덱스만 받도록 강제해줌.