비 종료 계산을 허용하지 않기 때문에 Coq는 반드시 Turing-complete가 아닙니다. Coq가 계산할 수있는 함수 클래스는 무엇입니까? (재미있는 흥미로운 특징이 있습니까?)
답변
Benjamin Werner는 그의 논문에서 Set in Types, Types in Sets에서 ZFC의 수많은 접근 불가능 성과 유도 구조 계산법을 통해 상호 해석 성을 입증했습니다 .
이는 대략적으로 액세스 할 수없는 많은 수의 ZFC에서 보여 질 수있는 모든 기능이 Coq. 따라서 큰 카디널에서 작업하는 세트 이론가가 아니라면 Coq에서 원하는 계산 기능을 정의 할 수 없을 것입니다.