Axiom K 란 무엇입니까?

Question

HoTT 이후 "Axiom K"에 대한 논의가 더 자주 일어났습니다. 패턴 일치와 관련 있다고 생각합니다. TAPL, ATAPL 또는 PFPL에서 참조를 찾을 수 없다는 것에 놀랐습니다. 공리 K는 무엇

• 입니까?
• 는 SML (또는 의존하는 패턴 매칭)에서와 같이 ML-스타일의 패턴 매칭에 사용인가?
• Axiom K에 대한 적절한 참고 자료는 무엇입니까?

Answer 1

공리 K는 정체성의 고유성의 원칙이 입증한다, 그것은 마틴 LOF의 의존의 형태 이론의 정체성 유형의 성격에 대한 공리이다라고합니다. 이 유형은 System F와 같은 더 간단한 유형 이론에서는 존재하지 않으며 실제로 정의 될 수 없습니다. 따라서 아마도 언급 한 책에서 그 유형을 발견하지 못했을 것입니다.

아이덴티티 유형 Id(A,x,y)로 쓰여지거나 및도 x = y합니다 (Curry-Howard correspondence 이하) 및 xy가 동일한 특성을 인코딩한다. 이 신원 유형의 증거를 제공하는 한 가지 기본적인 방법이며, 그 즉 x 자체가 같다는 것을 증명, refl : Id(A,x,x)입니다.

Thomas Streicher는 자신의 thesis에서 ID 유형을 조사 할 때 K (신원 유형의 표준 제거기 인 J 다음의 알파벳에서 다음 문자로)라고하는 ID 유형에 대한 새로운 제거 기능을 도입했습니다. x = x 형식의 항등 형 p은 그 자체가 간단한 증명 refl과 같습니다. 이것으로부터, 임의의 두 증거 p 및 어떤 식x = y의 q은 그러므로 다른 이름은 "신원 증명의 고유성"동일한 것을 따른다. 주목할만한 점은 그가 이 아니고이 아님을 증명했으며, 이론의 표준 규칙을 따릅니다. 나는 이유를 이해하고 싶다면 Dan Licata의 article on the homotopy type theory blog을 읽는 것이 좋습니다. 그는 내가 할 수있는 것보다 훨씬 더 잘 설명합니다.

는 질문의 두 번째 부분에 대답하려면 : ML 스타일의 패턴 매칭 K는 관계가, ML에도 K 공리를 공식화 할 수 따라서 신원 유형을 가지고 있지 않기 때문에. 반면 K는 Thierry Coquand가 "종속 유형과의 패턴 일치 (1992)"에서 소개 한 종속 패턴 일치에 필요합니다. 그 이유는 그것이 신원 형식의 생성자 refl에 패턴 매칭에 의해 K를 증명하기가 매우 쉽다는 점이다 : 사실

K : (p : x = x) -> p = refl 
K refl = refl 

, 코너 맥브라이드는 "(자신의 논문에서 보여 의존적으로는 기능 프로그램과 자신의 증명을 입력 (2000) ") K는 종속 패턴 매칭이 실제로 의존형 이론에 추가되는 것. 의존 패턴 매칭이 K를 필요로하는 이유 그것은 더 이상하지 않도록이 제한 될 수있는 방법이 주제에

내 자신의 관심을 정확하게 이해하는 것입니다. 그 결과 Agoda에서 paper 옵션과 --without-K 옵션이 새로 구현되었습니다. 기본 아이디어는 의존 패턴 매칭 중에 케이스 분석에 사용 된 통일 알고리즘이 x = x 형태의 방정식을 삭제해서는 안되기 때문에 K가 필요하기 때문입니다. 더 알고 싶다면 종이의 소개를 읽어 보는 것이 좋습니다.