[%] Coq vs Agda vs Lean

[익명(223.39)]

차이점 깔끔하게 설명해주는사람 반포자이

[익명(220.70)]

알아서 뭐함?

[익명(59.12)]

몰?루 vs 몰?루 va 몰?루 - dc App

[익명(223.39)]

agda는 순수 하스켈 느낌이 더 강하고 coq와 lean은 tactic monad가 있어서, 증명을 읽기는 어렵지만 만들어내기는 조금 더 편함. lean은 coq랑 비슷한데 문법이 조금 더 최근에 나왔고 급진적. quotient type을 위해 normalizing property 중 일부를 희생함.

[익명(223.39)]

coq는 타입이론적인 기반을 다지는 데 더 집중하는 반면 lean은 수학자들 끌어들이려고 정조를 버린 느낌. 표준 라이브러리부터 classical reasoning 위주로 짜여 있는 거 보면...

[익명(223.39)]

감사함다

[다믜(damhiya)]

Lean은 subject reduction(reduction이 일어나도 타입이 유지되는 성질)이 성립 안하지만 quotient type을 쓰기 편함. Coq하고 Agda는 dependent pattern matching이 다름. Coq은 패턴매칭이 그냥 match expression이고 Agda는 pattern matching lambda라서 생기는 차이점. 이것 때문에 tactic 없이 써야하는건 Agda가 더 편함. Coq, Lean은 tactic 덕분에 자동화에 더 유리. Coq은 universe level을 자동으로 추론하고 Agda는 명시적인 universe polymorphism을 사용함.

[익명(223.39)]

감사함니다