Axiom K là gì?

Question

Tôi nhận thấy cuộc thảo luận về "Axiom K" xuất hiện thường xuyên hơn từ HoTT. Tôi tin rằng nó có liên quan đến kết hợp mẫu. Tôi ngạc nhiên rằng tôi không thể tìm thấy một tài liệu tham khảo trong TAPL, ATTAPL hoặc PFPL.

• Axiom K là gì?
• Được sử dụng để đối sánh mẫu kiểu ML như trong SML (hoặc chỉ phù hợp với mẫu phụ thuộc)?
• Tham chiếu thích hợp cho Axiom K là gì?

Answer 1

Axiom K còn được gọi là nguyên tắc độc đáo của bản sắc chứng minh, và nó là một câu châm ngôn về bản chất của các loại sắc về mặt lý thuyết loại phụ thuộc Martin-LOF của. Loại này không tồn tại (và trên thực tế không thể được định nghĩa) trong các lý thuyết kiểu đơn giản hơn như System F, vì vậy đó có lẽ là lý do tại sao bạn chưa gặp nó trong các sách bạn đề cập.

Các loại sắc được viết như Id(A,x,y) hoặc cũng x = y và mã hóa các tài sản mà x và y đều bình đẳng (dưới Curry-Howard correspondence). Có một cách cơ bản để cung cấp bằng chứng về loại danh tính và đó là refl : Id(A,x,x), tức là bằng chứng rằng x bằng với chính nó.

Khi điều tra loại nhận dạng trong số thesis, Thomas Streicher đã giới thiệu loại bỏ mới cho loại nhận dạng mà ông gọi là K (là chữ cái tiếp theo trong bảng chữ cái sau chữ J, tiêu chuẩn loại bỏ). Nó nói rằng bất kỳ bằng chứng nào p về sự bình đẳng của biểu mẫu x = x là chính nó bằng chứng minh tầm thường refl. Từ đó, sau hai chứng minh p và q của bất kỳ phương thức nào là x = y đều bằng nhau, do đó thay thế "tính duy nhất của chứng minh danh tính". Điều đáng chú ý là ông đã chứng minh rằng điều này không không tuân theo các quy tắc tiêu chuẩn của lý thuyết loại. Tôi khuyên bạn nên đọc article on the homotopy type theory blog của Dan Licata nếu bạn muốn hiểu tại sao không, ông giải thích nó tốt hơn nhiều so với tôi có thể.

Để trả lời phần thứ hai của câu hỏi: Kết hợp mẫu kiểu ML không liên quan đến K, vì ML không có loại nhận dạng và do đó không thể xây dựng tiên đề K. Mặt khác, K được yêu cầu cho phù hợp với mẫu phụ thuộc như được giới thiệu bởi Thierry Coquand trong "Mẫu phù hợp với các kiểu phụ thuộc (1992)". Lý do cho điều này là rằng nó là rất dễ dàng để chứng minh K bằng mô hình kết hợp trên constructor refl loại sắc:

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

Trong thực tế, Conor McBride thể hiện trong luận án của mình ("lệ thuộc gõ chương trình chức năng và chứng minh của họ (2000) ") rằng K là chỉ điều phù hợp với mô hình phụ thuộc thực sự bổ sung vào lý thuyết loại phụ thuộc.

Sở thích của riêng tôi trong chủ đề này là để hiểu chính xác lý do khớp mẫu phụ thuộc yêu cầu K và cách nó có thể bị hạn chế để không còn nữa. Kết quả là một paper và một triển khai mới của tùy chọn --without-K trong Agda. Ý tưởng cơ bản là thuật toán hợp nhất được sử dụng để phân tích trường hợp trong khớp mẫu phụ thuộc không nên xóa phương trình của biểu mẫu x = x, bởi vì làm như vậy yêu cầu K. Tôi khuyên bạn nên đọc (giới thiệu) giấy nếu bạn muốn biết thêm.