Arend - HoTT- आधारित आश्रित भाषा (भाग 2)

आर्टेंड भाषा के बारे में लेख के पहले भाग में , हमने सबसे सरल आगमनात्मक प्रकारों, पुनरावर्ती कार्यों, कक्षाओं और सेटों की जांच की।

2. Arend में क्रमबद्ध सूची

2.1 Arend में सूचीबद्ध सूचियाँ

हम एक जोड़ी के रूप में क्रमबद्ध सूचियों के प्रकार को परिभाषित करते हैं जिसमें एक सूची और उसके क्रम का प्रमाण होता है। जैसा कि हमने पहले ही कहा है, Arend में, निर्भर जोड़े को the \Sigma कीवर्ड का उपयोग करके परिभाषित किया गया है। हम नमूने के साथ तुलना के माध्यम से Sorted प्रकार की परिभाषा देते हैं, आदेशित सूचियों के बारे में पहले से उल्लेखित लेख से परिभाषा से प्रेरित है ।

 \func SortedList (O : LinearOrder.Dec) => \Sigma (l : List O) (Sorted l) \data Sorted {A : LinearOrder.Dec} (xs : List A) \elim xs | nil => nilSorted | :-: x nil => singletonSorted | :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs)) 

नोट: Arend स्वचालित रूप से यह पता लगाने में सक्षम था कि Sorted प्रकार \Prop ब्रह्मांड में समाहित है। ऐसा इसलिए हुआ क्योंकि Sorted परिभाषा में सभी तीन पैटर्न परस्पर अनन्य हैं, और consSorted कंस्ट्रक्टर के दो पैरामीटर हैं, दोनों का संबंध \Prop ।
हमें Sorted विधेय की कुछ स्पष्ट संपत्ति साबित करते हैं, कहते हैं कि एक ऑर्डर की गई सूची की पूंछ खुद एक ऑर्डर की गई सूची है (यह संपत्ति भविष्य में हमारे लिए उपयोगी होगी)।

 \func tail-sorted {O : LinearOrder.Dec} (x : O) (xs : List O) (A : Sorted (x :-: xs)) : Sorted xs \elim xs, A | nil, _ => nilSorted | :-: _ _, consSorted _ xs-sorted => xs-sorted 

tail-sorted हमने एक ही समय में xs सूची और Sorted विधेय पर मिलान वाले पैटर्न का उपयोग किया, इसके अलावा, हमने "_" स्किप वर्ण का उपयोग किया , जिसे अप्रयुक्त चर के लिए प्रतिस्थापित किया जा सकता है।

कोई पूछ सकता है कि क्या अर्नेंड में आदेशित सूचियों की संपत्ति को साबित करना संभव है, धारा 1.3 में वर्णित एक तथ्य के उदाहरण के रूप में जो बिना सार के अनाउंसमेंट के एजडा में साबित नहीं हो सकता है। स्मरण करो कि यह संपत्ति दावा करती है कि निर्भर जोड़े के माध्यम से परिभाषित आदेश सूचियों की समानता को साबित करने के लिए, यह जोड़े के पहले घटकों की समानता की जांच करने के लिए पर्याप्त है।

यह तर्क दिया जाता है कि Arend में यह संपत्ति उपर्युक्त उल्लिखित inProp निर्माण और आश्रित SigmaExt जोड़े के लिए SigmaExt संपत्ति का SigmaExt ।

 \func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P 

SigmaPropExt संपत्ति मानक पुस्तकालय के पथ मॉड्यूल में साबित होती है, और HoTT पुस्तक के दूसरे अध्याय से कई अन्य तथ्य, जिसमें कार्यात्मक बहुआयामी की संपत्ति भी शामिल है, सिद्ध होते हैं।

.n ऑपरेटर .n उपयोग Arend में सिग्मा टाइप प्रोजेक्टर को नंबर n (हमारे मामले में, सिग्मा टाइप SortedList A जाता है और एक्सप्रेशन l1.1 अर्थ है कि इस प्रकार का पहला घटक टाइप List A की अभिव्यक्ति है)।

2.2 "क्रमपरिवर्तन" संपत्ति का कार्यान्वयन

अब आइए Arend पर सूची सॉर्टिंग फ़ंक्शन को लागू करने का प्रयास करें। स्वाभाविक रूप से, हम छँटाई एल्गोरिथ्म का एक सरल कार्यान्वयन नहीं करना चाहते हैं, लेकिन कुछ गुणों के प्रमाण के साथ एक कार्यान्वयन।

स्पष्ट रूप से, इस एल्गोरिथ्म में कम से कम 2 गुण होने चाहिए:
1. एल्गोरिथ्म का परिणाम एक आदेशित सूची होना चाहिए।
2. परिणामी सूची को मूल सूची का क्रमचय होना चाहिए।

पहले, आइए, Arend पर सूचियों की "क्रमपरिवर्तन" संपत्ति को लागू करने का प्रयास करें। ऐसा करने के लिए, हम Arend के लिए यहाँ से ली गई परिभाषा को अपनाते हैं।

 \truncated \data InsertSpec {A : \Set} (xs : List A) (a : A) (ys : List A) : \Prop \elim xs, ys | xs, :-: y ys => insertedHere (a = y) (xs = ys) | :-: x xs, :-: y ys => insertedThere (x = y) (InsertSpec xs a ys) \truncated \data Perm {A : \Set} (xs ys : List A) : \Prop | permInsert (xs' ys' : List A) (a : A) (Perm xs' ys') (InsertSpec xs' a xs) (InsertSpec ys' a ys) | permTrivial (xs = ys) 

हमारे द्वारा शुरू की गई InsertSpec विधेय का निम्नलिखित सहज अर्थ है: InsertSpec xs a ys ठीक-ठीक अर्थ है कि सूची ys तत्व को सूची xs (किसी भी स्थिति में) के अंदर डालने का परिणाम है। इस प्रकार, InsertSpec सम्मिलित फ़ंक्शन के विनिर्देश के रूप में लिया जा सकता है।

यह स्पष्ट है कि Perm डेटा प्रकार वास्तव में "क्रमपरिवर्तन" संबंध को परिभाषित करता है: permInsert कंस्ट्रक्टर वास्तव में permInsert है कि यदि xs और ys को कुछ लिस्ट xs' और ys' में एक ही तत्व डालने पर xs और ys परस्पर permInsert हैं। ys' छोटी लंबाई, जो पहले से ही एक दूसरे के क्रमपरिवर्तन हैं।

हमारे "क्रमपरिवर्तन" संपत्ति की परिभाषा के लिए, समरूपता संपत्ति को सत्यापित करना आसान है।

 \func Perm-symmetric {A : \Set} {xs ys : List A} (P : Perm xs ys) : Perm ys xs \elim P | permTrivial xs=ys => permTrivial (inv xs=ys) | permInsert perm-xs'-ys' xs-spec ys-spec => permInsert (Perm-symmetric perm-xs'-ys') ys-spec xs-spec 

पर्मिटेशन प्रॉपर्टी भी Perm लिए संतुष्ट है, लेकिन इसका सत्यापन बहुत अधिक जटिल है। चूंकि यह संपत्ति हमारे छंटाई एल्गोरिथ्म के कार्यान्वयन में कोई भूमिका नहीं निभाती है, इसलिए हम इसे एक अभ्यास के रूप में पाठक पर छोड़ देते हैं।

 \func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?} 

2.3 नमूने के साथ तुलना करने पर होमोटॉप्टी के स्तर में बदलाव

अब एक फ़ंक्शन को कार्यान्वित करने का प्रयास करते हैं जो एक तत्व को एक आदेशित सूची में सम्मिलित करता है ताकि परिणामी सूची आदेशित रहे। आइए निम्नलिखित भोले कार्यान्वयन के साथ शुरू करें।

 \func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case LinearOrder.trichotomy xy \with {  | byLeft x=y => x :-: insert xs' y  | byRight (byLeft x<y) => x :-: insert xs' y  | byRight (byRight y<x) => y :-: x :-: xs' } 

\case निर्माण, एक मनमाना अभिव्यक्ति के नमूने के साथ मिलान की अनुमति देता है ( \elim केवल फ़ंक्शन परिभाषा के उच्चतम स्तर पर और केवल इसके मापदंडों के लिए उपयोग किया जा सकता है)। यदि आप insert प्रकार की जांच करने के लिए Arend से पूछते हैं, तो निम्न त्रुटि संदेश प्रदर्शित होगा।

 [ERROR] Data type '||' is truncated to the universe \Prop  which does not fit in the universe of the eliminator type: List OE In: | byLeft x-leq-y => x :-: insert xs' y While processing: insert 

समस्या यह है कि LinearOrder.Dec वर्ग में LinearOrder.Dec परिभाषा LinearOrder.Dec ऑपरेटर का उपयोग करके दी गई है || , जो बदले में, प्रपोजल ट्रंकेशन का उपयोग करके निर्धारित किया जाता है। जैसा कि पहले से ही उल्लेख किया गया है, \Prop ब्रह्मांड से संबंधित प्रकारों के लिए, Arend में एक पैटर्न के साथ मिलान की अनुमति केवल तभी दी जाती है जब परिणामस्वरूप अभिव्यक्ति का प्रकार स्वयं एक अभिकथन हो (ऊपर दिए गए फ़ंक्शन के लिए, परिणाम प्रकार List OE , और यह प्रकार एक सेट है)।

क्या इस समस्या के आसपास कोई रास्ता है? इसे हल करने का सबसे आसान तरीका ट्राइकोटॉमी की संपत्ति की परिभाषा को बदलना है। ट्रिकोटॉमी की निम्न परिभाषा पर विचार करें, बिना-क्रंचित प्रकार का उपयोग करके Or ट्रंकित के बजाय || :

 \func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x) 

क्या यह परिभाषा मूल trichotomy परिभाषा से किसी भी चीज़ में trichotomy है || ? अगर हम केवल हमारे जीवन को जटिल बनाते हैं और हमें पैटर्न मिलान का उपयोग करने से रोकते हैं, तो हमने एक प्रस्तावित प्रकार का उपयोग क्यों किया?

आइए एक शुरुआत के लिए पहले सवाल का जवाब देने की कोशिश करें: सख्त StrictPoset आदेशों के लिए StrictPoset और set-trichotomy StrictPoset बीच StrictPoset अंतर वास्तव में बिल्कुल नहीं है। ध्यान दें कि set-trichotomy प्रकार एक बयान है। यह तथ्य इस तथ्य से अनुसरण करता है कि ट्राइकोटॉमी की परिभाषा में सभी तीन विकल्प क्रम के स्वयंसिद्ध होने के कारण पारस्परिक रूप से अनन्य हैं, और प्रत्येक तीन प्रकार के x = y, x < y, y < x अपने आप में एक कथन है ( x = y एक कथन है, इसलिए BaseSet क्लास की परिभाषा में BaseSet हमने मांग की कि मीडिया E एक सेट हो!)।

 \func set-trichotomy-isProp {A : StrictPoset} (xy : A) (l1 l2 : set-trichotomy xy): l1 = l2 \elim l1, l2 | inl (inl l1), inl (inl l2) => pmap (\lam z => inl (inl z)) (Path.inProp l1 l2) | inl (inr l1), inl (inr l2) => pmap (\lam z => inl (inr z)) (Path.inProp l1 l2) | inr l1, inr l2 => pmap inr (Path.inProp l1 l2) | inl (inl l1), inl (inr l2) => absurd (lt-eq-false l1 l2) | inl (inr l1), inl (inl l2) => absurd (lt-eq-false l2 l1) | inl (inl l1), inr l2 => absurd (lt-eq-false (inv l1) l2) | inr l1, inl (inl l2) => absurd (lt-eq-false (inv l2) l1) | inl (inr l1), inr l2 => absurd (lt-lt-false l1 l2) | inr l1, inl (inr l2) => absurd (lt-lt-false l2 l1) \where {  \func lt-eq-false {A : StrictPoset} {xy : A} (l1 : x = y) (l2 : x < y) : Empty =>    A.<-irreflexive x (transport (x <) (inv l1) l2)  \func lt-lt-false {A : StrictPoset} {xy : A} (l1 : x < y) (l2 : y < x) : Empty =>   A.<-irreflexive x (A.<-transitive _ _ _ l1 l2) } 

ऊपर की सूची में, absurd एक्स फॉल्सो क्वॉडलिबेट सिद्धांत के लिए पदनाम है, जिसे तर्क मॉड्यूल में परिभाषित किया गया है। चूंकि Empty प्रकार की परिभाषा में कंस्ट्रक्टर नहीं हैं (अनुभाग 1.2 देखें), absurd की परिभाषा में मामलों से गुजरना आवश्यक नहीं है:

 \func absurd {A : \Type} (x : Empty) : A 

चूंकि अब हम जानते हैं कि set-trichotomy एक बयान है, हम set-trichotomy संपत्ति को सामान्य आदेशों की सामान्य trichotomy संपत्ति से प्राप्त कर सकते हैं। ऐसा करने के लिए, हम \return \level निर्माण का उपयोग कर सकते हैं, जो Arend टाइमर को बताता है कि इस बिंदु पर, पैटर्न के साथ मिलान एक अनुमत ऑपरेशन है (इस मामले में, हमें सबूत दिखाना होगा कि set-trichotomy-property फ़ंक्शन का परिणाम एक बयान है)।

 \func set-trichotomy-property {A : LinearOrder.Dec} (xy : A) : set-trichotomy xy => \case A.trichotomy xy \return \level (set-trichotomy xy) (set-trichotomy-isProp xy) \with {  | byLeft x=y => inl (inl x=y)  | byRight (byLeft x<y) => inl (inr x<y)  | byRight (byRight y<x) => inr (y<x) } 

आइए अब हम दूसरे प्रश्न का उत्तर देने का प्रयास करते हैं, अर्थात्, क्यों, गणितीय वस्तुओं के गुणों का निर्माण करते समय, यह सामान्य नहीं, बल्कि प्रस्तावित रूप से काटे गए निर्माणों का उपयोग करने के लिए बेहतर है। इसके लिए गैर-रैखिक रैखिक आदेशों की परिभाषा के एक टुकड़े पर विचार करें (रैखिक और TotalOrder की पूरी परिभाषाएँ रैखिकऑर्डर मॉड्यूल में पाई जा सकती हैं):

 \class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x } 

आइए अब यह कल्पना करने की कोशिश करें कि अगर हमने संयुक्त राष्ट्र के कुल-क्षेत्र की परिभाषा को अन-ट्रुनेटेड Or निर्माण के माध्यम से बदल दिया है तो इसका अर्थ कैसे बदल जाएगा।

 \class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) } 

इस मामले में, टाइप (x <= y) `Or` (y <= x) अब एक बयान नहीं है, क्योंकि x और y के समान मूल्यों के मामले में y badTotality की परिभाषा में दोनों विकल्पों को लागू किया जा सकता है, और badTotality के प्रमाण में बाएं या दाएं शाखा का badTotality बिल्कुल मनमाना है और उपयोगकर्ता के विवेक पर रहता है। एक Or दूसरे को पसंद करने का कोई कारण नहीं है।

अब यह स्पष्ट है कि TotalOrder और BadTotalOrder क्या अंतर BadTotalOrder । दो ऑर्डर किए गए सेट O1 O2 : TotalOrder हमेशा समान होते हैं जब सेट O1.E, O2.E और ऑर्डर O1.<, O2.< की समानता साबित करना संभव होता है O1.<, O2.< उन्हें देखते हुए (यह वांछित संपत्ति है)। दूसरी ओर, O1 O2 : BadTotalOrder केवल O1 और O2 की समानता को साबित करना BadTotalOrder है, जब E से सभी तत्वों x अलावा E समानता O1.badTotality xx और O2.badTotality xx ।

इस प्रकार, यह पता चलता है कि क्लास BadTotalOrder सहज रूप से "रैखिक रूप से आदेशित सेट" के रूप में नहीं माना जाना चाहिए, लेकिन एक "रैखिक रूप से आदेशित के साथ-साथ बाएं या दाएं x क्षेत्र E प्रत्येक तत्व x लिए विकल्प के साथ Or badTotality xx के कार्यान्वयन में"।

२.४ सॉर्ट एल्गोरिथ्म

अब हम छँटाई एल्गोरिथ्म को लागू करने के लिए आगे बढ़ते हैं। आइए, सिद्ध set-trichotomy-property (इस मामले में, set-trichotomy की परिभाषा में कोष्ठक की अधिक सफल व्यवस्था के कारण, हमने माना मामलों की संख्या कम कर दी है) का उपयोग करके पिछले अनुभाग से insert फ़ंक्शन के भोले कार्यान्वयन को ठीक करने का प्रयास करें।

 \func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case set-trichotomy-property xy \with {  | inr y<x => y :-: x :-: xs'  | inl x<=y => x :-: insert xs' y } 

अब आइए सूचीबद्ध सूचियों के लिए इस परिभाषा के एक एनालॉग को लागू करने का प्रयास करें। हम निर्माण \let … \in विशेष \let … \in उपयोग करेंगे, जो हमें संदर्भ में नए स्थानीय चर जोड़ने की अनुमति देता है।

 \func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : SortedList O \elim xs | (nil, _) => (y :-: nil, singletonSorted) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with {  | inr y<x => (y :-: x :-: xs', consSorted (byRight y<x) xs-sorted)  | inl x<=y => \let (result, result-sorted) => insert (xs', tail-sorted x xs' xs-sorted) y         \in (x :-: result, {?}) 

हम प्रमाण में एक अपूर्ण टुकड़ा (अभिव्यक्ति द्वारा इंगित {?} ) में छोड़ दिया, उस स्थान पर जहां आप यह दिखाना चाहते हैं कि सूची x :-: result आदेश दिया गया है। हालाँकि संदर्भ में result सूची के क्रम के साक्ष्य हैं, यह हमारे लिए यह सत्यापित करने के लिए रहता है कि x result सूची के पहले तत्व के मूल्य से अधिक नहीं है, जो संदर्भ में परिसर से पालन करना इतना आसान नहीं है (वर्तमान लक्ष्य में सभी परिसरों को देखने के लिए - यह वही है जिसे हम कहते हैं गणना की वर्तमान शाखा - आपको insert फ़ंक्शन से प्रकार की जांच का अनुरोध करने की आवश्यकता है)।

यह पता चलता है कि insert लागू insert बहुत आसान है यदि हम insert विनिर्देश के प्रमाण के साथ परिणामी सूची के क्रम को सिद्ध करते हैं। insert के हस्ताक्षर बदलें और सरलतम मामलों में इस विनिर्देश का प्रमाण लिखें:

 \func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with {  | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp)  | inl x<=y =>   \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y   \in ((x :-: result, {?}), insertedThere idp result-spec) 

प्रमाण के बिना छोड़े गए एकल खंड के लिए, Arend निम्नलिखित संदर्भ मूल्य का उत्पादन करेगा:

 Expected type: Sorted (x :-: (insert (\this, tail-sorted x \this \this) \this).1.1) Context:  result-sorted : Sorted (insert (\this, tail-sorted \this \this \this) \this).1.1  xs-sorted : Sorted (x :-: xs')  x : O  x<=y : Or (x = y) (O.< xy)  O : Dec  result : List O  y : O  xs' : List O  result-spec : InsertSpec xs' y (insert (xs', tail-sorted \this xs' \this) y).1.1 

सबूत को पूरा करने के लिए, हमें \case ऑपरेटर की पूरी शक्ति का उपयोग करना होगा: हम 5 अलग-अलग चर के साथ मिलान वाले पैटर्न का उपयोग करेंगे, और चूंकि कुछ चर के प्रकार अन्य चर के मूल्यों पर निर्भर हो सकते हैं, हम निर्भर पैटर्न मिलान का उपयोग करेंगे।

बृहदान्त्र निर्माण स्पष्ट रूप से इंगित करता है कि किस प्रकार की तुलना में कुछ चर का प्रकार अन्य चर के मूल्यों पर निर्भर करता है (इस प्रकार, चर के प्रकार में xs-sorted, result-spec और result-sorted गए प्रत्येक के \case xs' बजाय xs' result इसी नमूने से मेल खाएगा)।

\return निर्माण, वैरिएबल को अपेक्षित परिणाम के प्रकार के साथ पैटर्न से मेल खाने के लिए जोड़ता है। दूसरे शब्दों में, वर्तमान लक्ष्य में, प्रत्येक \case क्लॉज में, परिणामी चर के लिए संबंधित नमूने को प्रतिस्थापित किया जाएगा। इस निर्माण के बिना, इस तरह के प्रतिस्थापन को नहीं किया जाएगा, और सभी \case क्लॉज़ का लक्ष्य स्वयं \case अभिव्यक्ति के स्थान पर लक्ष्य के साथ मेल खाएगा।

 \func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs  | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp)  | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with {   | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp)   | inl x<=y =>     \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y     \in ((x :-: result,       \case result \as result, xs' \as xs', xs-sorted : Sorted (x :-: xs'), result-spec : InsertSpec xs' y result, result-sorted : Sorted result       \return Sorted (x :-: result) \with {        | nil, _, _, _, _ => singletonSorted        | :-: r rs, _, _, insertedHere y=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) y=r (Or-to-|| x<=y)) result-sorted        | :-: r rs, :-: x' _, consSorted x<=x' _, insertedThere x2=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) x2=r x<=x') result-sorted }), insertedThere idp result-spec) 

कोड के उपरोक्त ब्लॉक में, पैटर्न तुलना के अंतिम दो पैराग्राफ में consSorted कंस्ट्रक्टर के जटिल पहले तर्क अतिरिक्त टिप्पणी के लायक हैं। यह समझने के लिए कि इन दोनों अभिव्यक्तियों का क्या अर्थ है, हम उन्हें अभिव्यक्ति {?} प्रतिस्थापित करते हैं और दोनों स्थितियों में लक्ष्य निर्धारित करने के लिए अरिड टाइमर से पूछते हैं।

आप देख सकते हैं कि वहां और वर्तमान लक्ष्य दोनों प्रकार (x = r) || O.< xr (x = r) || O.< xr । इसके अलावा, पहले लक्ष्य के संदर्भ में, परिसर हैं

 x<=y : Or (x = y) (O.< xy) y=r : y = r 

और दूसरे के संदर्भ में - परिसर

 x<=x' : (x = x') || O.< xx' x2=r : x' = r. 

सहज रूप से स्पष्ट: पहला लक्ष्य साबित करने के लिए, यह वेरिएबल r को सही स्टेटमेंट में बदलने के लिए पर्याप्त है Or (x = y) (O.< xy) y वेरिएबल के बजाय Or (x = y) (O.< xy) , और फिर प्रोपोज़ली ट्रंकेटेड टाइप पर स्विच करें || धारा 1.3 में परिभाषित Or-to-|| फ़ंक्शन का उपयोग करना । दूसरा लक्ष्य साबित करने के लिए, बस (x = x') || O.< x x' में स्थानापन्न करें (x = x') || O.< x x' (x = x') || O.< x x' वेरिएबल x' बजाय वेरिएबल r x' ।

वर्णित अभिव्यक्ति प्रतिस्थापन ऑपरेशन को औपचारिक रूप देने के लिए, मानक अरेंड लाइब्रेरी में एक विशेष transport फ़ंक्शन मौजूद है। उसके हस्ताक्षर पर विचार करें:

 \func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a' 

हमारे मामले में, OE को चर A लिए प्रतिस्थापित किया जाना चाहिए (यह स्पष्ट रूप से छोड़ा जा सकता है यदि अन्य transport तर्क निर्दिष्ट किए गए हैं), और अभिव्यक्ति \lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) ।

विनिर्देश के साथ सम्मिलन सॉर्टिंग एल्गोरिथ्म का कार्यान्वयन अब किसी विशेष कठिनाइयों का कारण नहीं बनता है: सूची x :-: xs' को क्रमबद्ध करने के लिए x :-: xs' , हम पहले सूची x :-: xs' की सूची को सम्मिलित करने के लिए एक पुनरावर्ती कॉल का उपयोग करते हैं, और फिर इस सूची के अंदर एलिमेंट को सम्मिलित करते हुए तत्व x को क्रम को संरक्षित करते हुए सम्मिलित करते हैं। पहले से लागू insert फ़ंक्शन तक पहुंच में मदद करें।

 \func insertSort {O : LinearOrder.Dec} (xs : List O) : \Sigma (result : SortedList O) (Perm xs result.1) \elim xs | nil => ((nil, nilSorted), permTrivial idp) | :-: x xs' => \let | (ys, perm-xs'-ys) => insertSort xs'                      | (zs, zs-spec) => insert ys x                  \in (zs, permInsert perm-xs'-ys (insertedHere idp idp) zs-spec) 

हमने प्रारंभिक लक्ष्य को पूरा किया और Arend पर सूचियों को क्रमबद्ध करना लागू किया। इस पैराग्राफ में दिया गया पूरा Arend कोड यहाँ से एक फाइल में डाउनलोड किया जा सकता है ।

कोई यह पूछ सकता है कि सख्त LinearOrder.Dec बजाय अगर कोई insert फ़ंक्शन के कार्यान्वयन को कैसे बदलना होगा? जैसा कि हम याद करते हैं, समग्रता फ़ंक्शन की परिभाषा में, काटे गए ऑपरेशन का उपयोग || काफी महत्वपूर्ण था, अर्थात्, यह परिभाषा एक परिभाषा के बराबर नहीं है, जिसमें इसके बजाय || द्वारा उपयोग किया जाता है।

इस सवाल का जवाब इस प्रकार है: TotalOrder लिए TotalOrder एनालॉग बनाना अभी भी संभव है, हालाँकि, इसके लिए हमें यह साबित करना होगा कि insert फंक्शन का प्रकार एक स्टेटमेंट है (यह हमें totality xy स्टेटमेंट के अनुसार सैंपल के साथ तुलना insert लिए insert की अनुमति देगा)।

दूसरे शब्दों में, हमें यह साबित करना होगा कि समानता के लिए केवल एक ही ऑर्डर की गई सूची है, जो एलिमेंट लिस्ट में दिए गए xs में तत्व y डालने का परिणाम है। यह देखना आसान है कि यह एक सच्चा तथ्य है, लेकिन इसका औपचारिक प्रमाण अब इतना तुच्छ नहीं है। हम इस तथ्य के सत्यापन को इच्छुक पाठक के लिए एक अभ्यास के रूप में छोड़ देते हैं।

3. टिप्पणियों को छोड़कर

इस परिचय में, हम Arend भाषा के मुख्य निर्माण से परिचित हुए, और यह भी सीखा कि कक्षा तंत्र का उपयोग कैसे किया जाए। हम इसके विनिर्देशन के प्रमाण के साथ सरलतम एल्गोरिथ्म को लागू करने में कामयाब रहे। इस प्रकार, हमने दिखाया है कि "रोजमर्रा की" समस्याओं को हल करने के लिए Arend काफी उपयुक्त है, जैसे कि, उदाहरण के लिए, प्रोग्राम सत्यापन।

हमने Arend की सभी विशेषताओं और सुविधाओं से दूर का उल्लेख किया है। उदाहरण के लिए, हमने कहा कि ऐसी स्थितियों के बारे में प्रकारों के बारे में कुछ भी नहीं है जो आपको इन निर्माणकर्ताओं के लिए कुछ विशेष पैरामीटर मानों के साथ विभिन्न प्रकार के "गोंद" करने की अनुमति देते हैं। उदाहरण के लिए, Arend में पूर्णांक प्रकार का कार्यान्वयन निम्नानुसार स्थितियों के साथ प्रकारों का उपयोग करके दिया जाता है:

 \data Int | pos Nat | neg Nat \with { zero => pos zero } 

यह परिभाषा कहती है कि पूर्णांक प्राकृतिक संख्याओं की दो प्रतियों से मिलकर बने होते हैं, जिनमें "सकारात्मक" और "नकारात्मक" शून्य की पहचान की जाती है। इस तरह की परिभाषा मानक कोक लाइब्रेरी से परिभाषा की तुलना में बहुत अधिक सुविधाजनक है, जहां प्राकृतिक संख्याओं की "नकारात्मक प्रतिलिपि" को "एक के द्वारा स्थानांतरित" किया जाता है ताकि इन प्रतियों को प्रतिच्छेद न करें (यह तब और अधिक सुविधाजनक है जब नकारात्मक neg 1 संकेतन का अर्थ संख्या -1, नहीं -2 है) ।

हमने कक्षाओं और उनके उदाहरणों में विधेय और होमोटोपी स्तरों को प्राप्त करने के लिए एल्गोरिथम के बारे में कुछ नहीं कहा। हमने शायद ही अंतराल के प्रकार I का उल्लेख किया है, हालांकि यह अंतराल के साथ प्रकारों के सिद्धांत में एक महत्वपूर्ण भूमिका निभाता है, जो कि Arend का तार्किक आधार है। यह समझने के लिए कि यह प्रकार कितना महत्वपूर्ण है, यह उल्लेख करने के लिए पर्याप्त है कि Arend प्रकार की समानता को एक अंतराल की अवधारणा के माध्यम से परिभाषित किया गया है। , , , (.. ).

: , HoTT JetBrains Research.