Core Concepts
쿼셔넌트 타입 등가성을 활용하여 기존 증명을 새로운 타입으로 수리할 수 있는 알고리즘을 제안한다.
Abstract
이 논문은 증명 수리 문제를 확장하여 쿼셔넌트 타입 등가성을 다룬다. 기존 연구에서는 타입 등가성을 활용하여 증명을 수리할 수 있었지만, 이는 제한적이었다. 이 논문에서는 쿼셔넌트 타입 등가성을 활용하여 증명을 수리할 수 있는 알고리즘을 제안한다.
논문은 두 가지 접근법을 제시한다:
큐비컬 아그다의 내부 관점: 큐비컬 아그다는 쿼셔넌트 타입을 내부적으로 지원하므로, 증명 수리 알고리즘을 큐비컬 아그다의 타입 이론 일부에 적용할 수 있다. 이를 통해 수리된 증명의 정확성을 내부적으로 증명할 수 있다.
코크의 외부 관점: 코크는 쿼셔넌트 타입을 지원하지 않으므로, 세토이드를 활용하여 외부적으로 쿼셔넌트 타입을 표현한다. 증명 수리 알고리즘을 확장하여 세토이드를 지원하며, 프로토타입 자동화를 구현한다.
논문은 두 접근법의 장단점을 비교하고, 이전에 지원되지 않았던 변경 사항에 대한 증명 수리 사례 연구를 보여준다.
Stats
큐비컬 아그다는 쿼셔넌트 타입을 내부적으로 지원한다.
코크는 쿼셔넌트 타입을 지원하지 않으므로, 세토이드를 활용하여 외부적으로 표현한다.
큐비컬 아그다의 증명 수리 알고리즘은 간단하지만 자동화가 없다.
코크의 증명 수리 알고리즘은 확장되었지만 프로토타입 자동화를 구현했다.
Quotes
"쿼셔넌트 타입 등가성은 수학적 구조의 표현 변경과 데이터 구조의 기본 구현 변경을 표현하는 데 유용하다."
"큐비컬 아그다에서는 수리된 증명의 정확성을 내부적으로 증명할 수 있지만, 이를 조합하는 것이 어렵다."
"코크에서는 세토이드 기반 접근법을 통해 프로토타입 자동화를 구현했다."