क्या बिना एज के एजडा कम शक्तिशाली है?

Question

What is Axiom K? पर फॉलो-अप के रूप में, मुझे आश्चर्य है कि जब आप --without-k विकल्प के साथ एग्डा का उपयोग करते हैं तो क्या होता है। क्या परिणाम कम शक्तिशाली है? क्या यह एक अलग भाषा है या क्या पिछले सभी कार्यक्रम अभी भी चेक टाइप करते हैं?

Answer 1

मार्टिन-लोफ प्रकार सिद्धांत और एक्सीओम के साथ स्थिति यूक्लिडियन ज्यामिति और समांतर डाकू के समान कुछ तरीकों से है। समांतर पोस्टलेट के साथ अधिक प्रमेय साबित हो सकते हैं, लेकिन वे केवल यूक्लिडियन रिक्त स्थान के बारे में हैं। समांतर पोस्टलेट के बिना सिद्ध प्रमेय भी गैर-युक्लिडियन रिक्त स्थान के बारे में सच हैं, और किसी को स्पष्ट रूप से गैर-यूक्लिडियन सिद्धांतों को जोड़ने की आजादी है।

एक्सिसॉम के मोटे तौर पर कहते हैं कि समानता प्रमाणों में कोई गैर-मामूली जानकारी नहीं होती है और इसमें कोई कम्प्यूटेशनल सामग्री नहीं होती है। स्वाभाविक रूप से

-- 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 

से ये दोनों --without-K साथ unprovable हैं: यह दोनों निम्नलिखित बयानों को तार्किक रूप से बराबर है। मैं यहाँ कि कश्मीर के बिना unprovable हैं एक जोड़े को और अधिक विशिष्ट बयान, और जिसका unprovability पहली नजर में जवाबी सहज ज्ञान युक्त लग सकता है दे:

{-# 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 

स्वयंसिद्ध कश्मीर सहज लगता है, के बाद से हम एक ही refl निर्माता के साथ AGDA के प्रोपोज़िशनल समानता को परिभाषित किया। रहस्यमय गैर-refl समानता प्रमाणों से भी परेशान क्यों है जिसका अस्तित्व हम के बिना अस्वीकार नहीं कर सकते?

यदि हमारे पास वसंत के पास नहीं है, तो हम उन सिद्धांतों को जोड़ने के लिए स्वतंत्र हैं जो कि के विपरीत हैं, जिससे हमें प्रकार की धारणा को सामान्य रूप से सामान्यीकृत करने में मदद मिलती है। हम एकता के सिद्धांत और उच्च-अपरिवर्तनीय प्रकारों को पोस्ट कर सकते हैं, जो अनिवार्य रूप से हमें टाइप सिद्धांत देता है कि Homotopy Type Theory पुस्तक लगभग है।

यूक्लिडियन समानता पर वापस लौटना: समांतर डाकू यह मानता है कि अंतरिक्ष सपाट है, इसलिए हम ऐसी चीजों को साबित कर सकते हैं जो अंतरिक्ष की समतलता पर निर्भर करते हैं, लेकिन गैर-फ्लैट रिक्त स्थानों के बारे में कुछ भी नहीं कह सकते हैं। एक्सिओम के मानते हैं कि सभी प्रकारों में तुच्छ समानता प्रमाण होते हैं, इसलिए हम उस पर निर्भर बयान साबित कर सकते हैं, लेकिन हमारे पास उच्च-आयामी संरचनाओं वाले प्रकार नहीं हो सकते हैं। गैर-युक्लिडियन रिक्त स्थान और उच्च-आयामी प्रकारों में समान रूप से अजीबता का कुछ कारक होता है लेकिन वे अंततः विचारों के समृद्ध और उपयोगी स्रोत होते हैं।

यदि हम "पुस्तक" होमोटॉपी प्रकार सिद्धांत पर स्विच करते हैं, तो "छोटी समानताएं" एक ऐसी संपत्ति बन जाती है जिसे हम आंतरिक रूप से बात कर सकते हैं और उस विशिष्ट प्रकार के लिए साबित कर सकते हैं जिसमें उस संपत्ति है।