Agda có K không mạnh hơn?

Question

Để theo dõi What is Axiom K?, tôi tự hỏi điều gì xảy ra khi bạn sử dụng Agda với tùy chọn --without-k. Kết quả có kém hiệu quả hơn không? Nó là một ngôn ngữ khác hoặc làm tất cả các chương trình trước vẫn gõ kiểm tra?

Answer 1

Tình huống với lý thuyết loại Martin-Löf và Axiom K theo một số cách tương tự với hình học Euclide và định đề song song. Với giả thuyết song song, nhiều định lý hơn có thể được chứng minh, nhưng đó chỉ là về không gian Euclide. Nếu không có định lý có thể chứng minh được song song cũng đúng với các không gian phi Euclide và người ta có quyền tự do thêm các tiên đề phi Euclide rõ ràng.

Axiom K gần nói rằng bằng chứng bình đẳng không mang thông tin không tầm thường và không có nội dung tính toán. Đó là một cách logic tương đương với cả hai câu lệnh sau:

-- uniqueness of identity proofs 
UIP : {A : Set}(x y : A)(p p' : x ≡ y) → p ≡ p' 

-- reflexive equality elimination 
EqRefl : {A : Set}(x : A)(p : x ≡ x) → p ≡ refl 

Đương nhiên, cả hai đều không thể chứng minh với --without-K. Tôi cho đây là một vài báo cáo cụ thể hơn đó là không thể chứng minh mà không cần K, và có unprovability có vẻ phản trực giác ngay từ cái nhìn đầu tiên:

{-# OPTIONS --without-K #-} 

open import Relation.Binary.PropositionalEquality 
open import Data.Bool 
open import Data.Empty 

-- this one is provable, we're just making use of it below 
coerce : {A B : Set} → A ≡ B → A → B 
coerce refl a = a 

coerceTrue : (p : Bool ≡ Bool) → coerce p true ≡ true 
coerceTrue = ? -- unprovable 

data PointedSet : Set₁ where 
    pointed : (A : Set) → A → PointedSet 

BoolNEq : pointed Bool true ≡ pointed Bool false → ⊥ 
BoolNEq = ? -- unprovable 

Axiom K có vẻ trực quan, vì chúng ta định nghĩa bình đẳng mệnh đề Agda với một refl constructor duy nhất. Tại sao ngay cả bận tâm với các bằng chứng không bình đẳng không refl có sự tồn tại mà chúng ta không thể bác bỏ mà không có K?

Nếu chúng ta không có tiên đề K, chúng ta được tự do thêm các tiên đề mâu thuẫn với K, cho phép chúng ta khái quát hóa khái niệm các loại của chúng ta. Chúng ta có thể mô tả tiên đề duy nhất và các loại quy nạp cao hơn, về cơ bản cho chúng ta lý thuyết loại mà cuốn sách Homotopy Type Theory là về.

Quay lại tương tự Euclide: giả thiết song song cho rằng không gian bằng phẳng, vì vậy chúng tôi có thể chứng minh những điều phụ thuộc vào độ phẳng của không gian, nhưng không thể nói gì về không gian phẳng. Axiom K thừa nhận rằng tất cả các loại có bằng chứng bình đẳng tầm thường, vì vậy chúng ta có thể chứng minh các câu lệnh phụ thuộc vào điều đó, nhưng chúng ta không thể có các loại với cấu trúc chiều cao hơn. Các không gian phi Euclide và các loại chiều cao hơn cũng có một số yếu tố kỳ quặc nhưng cuối cùng chúng là nguồn ý tưởng phong phú và hữu ích.

Nếu chúng tôi chuyển sang lý thuyết loại đồng luân "sách", thì "có tỷ lệ bình đẳng" trở thành tài sản mà chúng ta có thể nói về nội bộ và chứng minh cho các loại cụ thể có thuộc tính đó.