शुभ दिन, प्रिय habrayuzer!
टाइप किए गए लंबो कैलकुलस पर कई किताबें पढ़ने के बाद, निर्भर प्रकारों पर, मैंने एक दिलचस्प नियमितता देखी: हर जगह पहला उदाहरण क्रमबद्ध सूची प्रकार की परिभाषा देता है। सबकुछ ठीक हो जाएगा, लेकिन इस परिभाषा से परे कुछ भी नहीं था। इसलिए मैं इस अंतर के साथ आया और एक फ़ंक्शन को लागू करता हूं जो एक सूची लेता है और दूसरी सूची और दो प्रमाण लौटाता है। एक साबित करता है कि परिणाम इनपुट का एक क्रमचय है, और दूसरा साबित करता है कि परिणाम एक क्रमबद्ध सूची है।
औपचारिक विवरण
इस भाग में मैं मुख्य प्रकार दूंगा जिनका उपयोग बाद में किया जाएगा, और कुछ सहायक कार्य। साथ ही, अगड़ा के कुछ दिलचस्प वाक्यात्मक आकर्षण यहां दिखाए जाएंगे। जो लोग
अगाडा से बहुत परिचित नहीं हैं, उनके लिए मैं
SPBHUG / FProg 2012-07 की मीटिंग
में जन
मालाखोव्स्की के
वीडियो / स्लाइड्स को देखने की सलाह देता हूं - मेरे विचार से यह रूसी में
अगाडा का एकमात्र परिचय है (खैर, मैंने इसे अब तक नहीं देखा है)। या
एजडा वेबसाइट (यह बड़ा नहीं है) या
इस ट्यूटोरियल से मैनुअल के माध्यम से फ्लिप
करें ।
सूची परिभाषाएँ
data List {a} (A : Set a) : Set a where [] : List A _∷_ : (x : A) (xs : List A) → List A [_] : ∀ {a} {A : Set a} → A → List A [ x ] = x ∷ [] _++_ : ∀ {a} {A : Set a} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
यहाँ हमारे पास एक सूची है। मानक पुस्तकालय से ली गई परिभाषा। जैसा कि आप देख सकते हैं, सूची आइटम किसी भी प्रकार, यहां तक कि प्रकार और प्रकार के मूल्य हो सकते हैं। उच्च-क्रम के बहुरूपता के उपयोग के कारण यह संभव है: एक पैरामीटर पेश किया जाता है जो स्तर के लिए जिम्मेदार होता है, अर्थात, सामान्य प्रकार प्रकार के होते हैं
सेट 0 ,
सेट 0 टाइप
1 का प्रकार है, आदि।
इसके अलावा इस परिभाषा में आप देख सकते हैं कि ऑपरेटर्स को एगडा में घोषित किया गया है, अर्थात् अंडरस्कोर के माध्यम से, जिसके स्थान पर तर्क होंगे। यह ध्यान दिया जाना चाहिए कि यह विधि आपको कई दिलचस्प रूपों को परिभाषित करने की अनुमति देती है, जैसे कि एक फ़ंक्शन जो किसी एकल तत्व
[_] से सूची लौटाता है।
यह ध्यान दिया जाना चाहिए कि सभी ऑपरेटरों (अंडरस्कोर वाले कॉम्बिनेटर) के लिए, आप प्राथमिकता और संबद्धता निर्दिष्ट कर सकते हैं। इसके अलावा, Agda में, रिक्त स्थान और कोष्ठक (गोल और घुंघराले) के बिना कोई भी यूनिकोड अनुक्रम एक शब्द है।
आपको कोष्ठक और घुंघराले ब्रेसिज़ पर भी ध्यान देना चाहिए: प्रकार संकेत में घुंघराले कोष्ठक कहते हैं कि यह तर्क निहित है और संकलक द्वारा आउटपुट होगा।
"सॉर्ट की गई सूची" टाइप करें
data Sorted {A} (_≤_ : A → A → Set) : List A → Set where nil : Sorted _≤_ [] one : {x : A} → Sorted _≤_ [ x ] two : {x : A} → ∀ {yl} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l)
यह एक क्रमबद्ध सूची की परिभाषा विधेय है। डिजाइनरों को स्वयंसिद्ध माना जाना चाहिए। हमारे पास
शून्य का स्वयंसिद्ध और
एक है जो कहता है कि रिक्त सूची और एक तत्व से सूची को क्रमबद्ध किया गया है। हम यह भी देखते हैं कि
सॉर्ट किया गया प्रकार विधेय
_ ,
_ पर निर्भर करता है, जो आदेश के लिए जिम्मेदार है - एक तुलनात्मक फ़ंक्शन जैसा कुछ, लेकिन एक आश्रित प्रकार (तर्क सामान्य प्रकार के मान हैं, और परिणाम कुछ प्रकार है जिसका मूल्य प्रमाण है)। एक्सिओम
दो निम्नलिखित कहता है: अगर हमारे पास सबूत है कि
x x y (
x a y एक प्रकार है, और टाइप
x type
y का मान इस बात का प्रमाण है कि
x Cur y ।
करी-हावर्ड Isomorphism देखें), और उस का प्रमाण। , ताकि हेड
वाई के साथ कुछ सूची को सॉर्ट किया जाए (यह प्रमाण प्रकार
सॉर्ट किए गए _ some_ (y then l) का मान है) , फिर सूची
x ∷ y will l भी सॉर्ट की जाएगी।
"क्रमचय" टाइप करें
data Permutation {A} : List A → List A → Set where refl : ∀ {l} → Permutation ll perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂)
प्रकार (विधेय) "क्रमचय"। तर्क दो सूचियाँ हैं। पेश किए गए स्वयंसिद्ध हैं:
refl - सूची स्वयं का एक क्रमचय है;
पर्म - यदि हमारे पास प्रमाण है कि कुछ सूची
l एक अन्य सूची
l₂ ++ x we ∷ x₁ of l this (इस का प्रमाण है कि
क्रमपरिवर्तन l (l₁ ++ x₂ ₁ x₁ ∷ l₂) प्रकार का मान है), तो यदि हम दो मनमाने तरीके से पुनर्व्यवस्थित करते हैं। स्थानों में तत्व, हम पाते हैं कि नई सूची पहले की क्रमपरिवर्तन है।
"राशि" टाइप करें
data _⊎_ {ab} (A : Set a) (B : Set b) : Set (a ⊔ b) where inj₁ : (x : A) → A ⊎ B inj₂ : (y : B) → A ⊎ B
खैर, यहां सब कुछ सरल है - यह एक आश्रित प्रकार नहीं है - या तो हास्केल का एक एनालॉग।
उत्पाद प्रकार
record Σ {ab} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where constructor _,_ field proj₁ : A proj₂ : B proj₁ syntax Σ A (λ x → B) = Σ[ x ∶ A ] B _×_ : ∀ {ab} (A : Set a) (B : Set b) → Set (a ⊔ b) A × B = Σ[ _ ∶ A ] B
यह टूप्ले का एक एनालॉग है।
रिकॉर्ड का उपयोग किया जाता है क्योंकि इस प्रकार का केवल एक निर्माता हो सकता है। यह परिभाषा एक आश्रित प्रकार का उपयोग करती है: पहला तत्व एक निश्चित मूल्य है, और दूसरा इस तत्व पर कुछ विधेय के निष्पादन का प्रमाण है। लेकिन, निश्चित रूप से, इसे उस तरह से उपयोग करने के लिए आवश्यक नहीं है, यह एक नियमित रूप से ट्यूपल (
_ × _ के माध्यम से) की तरह किया जा सकता है - फिर तत्वों के बीच निर्भरता को अनदेखा किया जाता है।
सिंटैक्स आपको नए सिंटैक्स कंस्ट्रक्शंस को परिभाषित करने की अनुमति देता है यदि सरल संभावनाएं कम हैं।
क्रमबद्ध करें
sort : {A : Set} {_≤_ : A → A → Set} → (∀ xy → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l')
अंत में, हम सॉर्टिंग फ़ंक्शन के प्रकार का वर्णन करते हैं: यह फ़ंक्शन एक (अनुमानित) को स्वीकार करता है जो आदेश को निर्धारित करता है, यह भी एक फ़ंक्शन है, जो इनपुट मानों के लिए, एक प्रमाण देता है कि पहला दूसरे से बड़ा है या दूसरा पहले से बड़ा है। मुझे लगता है कि पाठक ने अनुमान लगाया है कि इस फ़ंक्शन का उपयोग क्रमबद्ध सूची-परिणाम के प्रमाण के निर्माण के लिए किया जाएगा। इसके अलावा, ज़ाहिर है, इनपुट मापदंडों में से एक एक सूची है जिसे क्रमबद्ध किया जाएगा।
सॉर्ट फ़ंक्शन एक सूची और दो प्रमाण (सॉर्टिंग और क्रमपरिवर्तन) देता है।
प्रकार्य कार्यान्वयन
बेशक, यहां इस फ़ंक्शन का कोई कार्यान्वयन नहीं होगा - ऐसा नहीं है कि मुझे कोड दिखाने के लिए खेद होगा, मुझे खुद को समझाने के लिए खेद है। इसलिए, मैं कुछ सहायक कार्यों के प्रमाण (कार्यान्वयन) दूंगा जिन्हें मुझे क्रमबद्ध कार्य लिखते समय आवश्यक था।
एक कामकाजी स्रोत यहां पाया जा सकता है।Agda-2.3.1 और मानक पुस्तकालय-0.6 का उपयोग किया
{-# OPTIONS --no-termination-check #-} module QuickSort where open import IO.Primitive using () renaming (putStrLn to putCoStrLn) open import Data.String using (toCostring; String) renaming (_++_ to _+s+_) open import Data.List open import Data.Nat open import Data.Nat.Show open import Data.Sum open import Data.Product open import Relation.Binary.Core open import Function data Sorted {A} (_≤_ : A → A → Set) : List A → Set where nil : Sorted _≤_ [] one : {x : A} → Sorted _≤_ [ x ] two : {x : A} → ∀ {yl} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l) data Permutation {A} : List A → List A → Set where refl : ∀ {l} → Permutation ll perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂) ≡-elim : ∀ {l} {A : Set l} {xy : A} → x ≡ y → (P : A → Set l) → P x → P y ≡-elim refl _ p = p ≡-sym : ∀ {l} {A : Set l} {xy : A} → x ≡ y → y ≡ x ≡-sym refl = refl ≡-trans : ∀ {l} {A : Set l} {xyz : A} → x ≡ y → y ≡ z → x ≡ z ≡-trans refl refl = refl ++-assoc : ∀ {l} {A : Set l} (l₁ l₂ l₃ : List A) → (l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃) ++-assoc [] l₂ l₃ = refl ++-assoc (h ∷ t) l₂ l₃ = ≡-elim (≡-sym $ ++-assoc t l₂ l₃) (λ x → h ∷ x ≡ h ∷ t ++ (l₂ ++ l₃)) refl decNat : (xy : ℕ) → (x ≤ y) ⊎ (y ≤ x) decNat zero y = inj₁ z≤n decNat (suc x) (suc y) with decNat xy ... | inj₁ p = inj₁ (s≤sp) ... | inj₂ p = inj₂ (s≤sp) decNat (suc x) zero = inj₂ z≤n perm-trans : ∀ {A} {l₁ l₂ l₃ : List A} → Permutation l₁ l₂ → Permutation l₂ l₃ → Permutation l₁ l₃ perm-trans p refl = p perm-trans p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm l₁ x₁ x₂ l₂ $ perm-trans p₁ p₂ perm-sym : ∀ {A} {l₁ l₂ : List A} → Permutation l₁ l₂ → Permutation l₂ l₁ perm-sym refl = refl perm-sym (perm l₁ x₁ x₂ l₂ p) = perm-trans (perm l₁ x₂ x₁ l₂ refl) (perm-sym p) perm-del-ins-r : ∀ {A} (l₁ : List A) (x : A) (l₂ l₃ : List A) → Permutation (l₁ ++ x ∷ l₂ ++ l₃) (l₁ ++ l₂ ++ x ∷ l₃) perm-del-ins-r l₁ x [] l₃ = refl perm-del-ins-r l₁ x (h ∷ t) l₃ = perm-trans p₀ p₅ where p₀ : Permutation (l₁ ++ x ∷ h ∷ t ++ l₃) (l₁ ++ h ∷ x ∷ t ++ l₃) p₀ = perm l₁ hx (t ++ l₃) refl p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃) p₁ = perm-del-ins-r (l₁ ++ [ h ]) xt l₃ p₂ : (l₁ ++ [ h ]) ++ t ++ x ∷ l₃ ≡ l₁ ++ h ∷ t ++ x ∷ l₃ p₂ = ++-assoc l₁ [ h ] (t ++ x ∷ l₃) p₃ : (l₁ ++ [ h ]) ++ x ∷ t ++ l₃ ≡ l₁ ++ h ∷ x ∷ t ++ l₃ p₃ = ++-assoc l₁ [ h ] (x ∷ t ++ l₃) p₄ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃) p₄ = ≡-elim p₂ (λ y → Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) y) p₁ p₅ : Permutation (l₁ ++ h ∷ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃) p₅ = ≡-elim p₃ (λ y → Permutation y (l₁ ++ h ∷ t ++ x ∷ l₃)) p₄ perm-del-ins-l : ∀ {A} (l₁ l₂ : List A) (x : A) (l₃ : List A) → Permutation (l₁ ++ l₂ ++ x ∷ l₃) (l₁ ++ x ∷ l₂ ++ l₃) perm-del-ins-l l₁ l₂ x l₃ = perm-sym $ perm-del-ins-r l₁ x l₂ l₃ perm-++ : ∀ {A} {x₁ y₁ x₂ y₂ : List A} → Permutation x₁ y₁ → Permutation x₂ y₂ → Permutation (x₁ ++ x₂) (y₁ ++ y₂) perm-++ refl refl = refl perm-++ (perm {x₁} l₁ e₁ e₂ l₂ p) (refl {z₂}) = perm-trans p₅ p₇ where p₁ : Permutation (x₁ ++ z₂) ((l₁ ++ e₂ ∷ e₁ ∷ l₂) ++ z₂) p₁ = perm-++ p refl p₂ : (l₁ ++ e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂ p₂ = ++-assoc l₁ (e₂ ∷ e₁ ∷ l₂) z₂ p₃ : l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂ p₃ = ≡-elim (++-assoc [ e₂ ] (e₁ ∷ l₂) z₂) (λ x → l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ x) refl p₄ : l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂ p₄ = ≡-elim (++-assoc [ e₁ ] l₂ z₂) (λ x → l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ x) refl g₂ : (l₁ ++ e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂ g₂ = ++-assoc l₁ (e₁ ∷ e₂ ∷ l₂) z₂ g₃ : l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂ g₃ = ≡-elim (++-assoc [ e₁ ] (e₂ ∷ l₂) z₂) (λ x → l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ x) refl g₄ : l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ e₂ ∷ l₂ ++ z₂ g₄ = ≡-elim (++-assoc [ e₂ ] l₂ z₂) (λ x → l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ x) refl p₅ : Permutation (x₁ ++ z₂) (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂) p₅ = ≡-elim (≡-trans p₂ $ ≡-trans p₃ p₄) (Permutation (x₁ ++ z₂)) p₁ p₆ : Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂) (l₁ ++ e₁ ∷ e₂ ∷ l₂ ++ z₂) p₆ = perm l₁ e₁ e₂ (l₂ ++ z₂) refl p₇ : Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂) ((l₁ ++ e₁ ∷ e₂ ∷ l₂) ++ z₂) p₇ = ≡-elim (≡-sym $ ≡-trans g₂ $ ≡-trans g₃ g₄) (Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂)) p₆ perm-++ {_} {x₁} {y₁} .{_} .{_} p₁ (perm {x₂} l₁ e₁ e₂ l₂ p₂) = ≡-elim p₇ (Permutation (x₁ ++ x₂)) p₆ where p' : Permutation (x₁ ++ x₂) (y₁ ++ l₁ ++ e₂ ∷ e₁ ∷ l₂) p' = perm-++ p₁ p₂ p₃ : y₁ ++ l₁ ++ e₂ ∷ e₁ ∷ l₂ ≡ (y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂ p₃ = ≡-sym $ ++-assoc y₁ l₁ (e₂ ∷ e₁ ∷ l₂) p₄ : Permutation (x₁ ++ x₂) ((y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂) p₄ = ≡-elim p₃ (Permutation (x₁ ++ x₂)) p' p₅ : Permutation ((y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂) ((y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂) p₅ = perm (y₁ ++ l₁) e₁ e₂ l₂ refl p₆ : Permutation (x₁ ++ x₂) ((y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂) p₆ = perm-trans p₄ p₅ p₇ : (y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂ ≡ y₁ ++ l₁ ++ e₁ ∷ e₂ ∷ l₂ p₇ = ++-assoc y₁ l₁ (e₁ ∷ e₂ ∷ l₂) ++-[] : ∀ {l} {A : Set l} (l : List A) → l ++ [] ≡ l ++-[] [] = refl ++-[] (h ∷ t) = ≡-trans p₀ p₁ where p₀ : (h ∷ t) ++ [] ≡ h ∷ t ++ [] p₀ = ++-assoc [ h ] t [] p₁ : h ∷ t ++ [] ≡ h ∷ t p₁ = ≡-elim (++-[] t) (λ x → h ∷ t ++ [] ≡ h ∷ x) refl data ConstrainedList {A} (P : A → Set) : List A → Set where [] : ConstrainedList P [] _∷_ : {x : A} {xs : List A} (p : P x) → ConstrainedList P xs → ConstrainedList P (x ∷ xs) infix 2 _∈_ data _∈_ {A} : A → List A → Set where exact : ∀ ht → h ∈ h ∷ t cons : ∀ h {xl} → x ∈ l → x ∈ h ∷ l create-∈ : ∀ {A} (l₁ : List A) (x : A) (l₂ : List A) → x ∈ (l₁ ++ x ∷ l₂) create-∈ [] x l₂ = exact x l₂ create-∈ (h₁ ∷ t₁) x l₂ = cons h₁ $ create-∈ t₁ x l₂ perm-∈ : ∀ {A l l'} {x : A} → x ∈ l → Permutation l' l → x ∈ l' perm-∈ p refl = p perm-∈ {A} .{l₁ ++ x₁ ∷ x₂ ∷ l₂} {l'} {x} p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm-∈ (loop l₁ x₁ x₂ l₂ p₁) p₂ where loop : ∀ l₁ x₁ x₂ l₂ → x ∈ l₁ ++ x₁ ∷ x₂ ∷ l₂ → x ∈ l₁ ++ x₂ ∷ x₁ ∷ l₂ loop [] .x x₂ l₂ (exact .x .(x₂ ∷ l₂)) = cons x₂ $ exact x l₂ loop [] .x₁ .x .l₂ (cons x₁ (exact .x l₂)) = exact x (x₁ ∷ l₂) loop [] .x₁ .x₂ l₂ (cons x₁ (cons x₂ p)) = cons x₂ $ cons x₁ p loop (.x ∷ t₁) x₁ x₂ l₂ (exact .x .(t₁ ++ x₁ ∷ x₂ ∷ l₂)) = exact x (t₁ ++ x₂ ∷ x₁ ∷ l₂) loop (.h₁ ∷ t₁) x₁ x₂ l₂ (cons h₁ p) = cons h₁ $ loop t₁ x₁ x₂ l₂ p constr-∈ : ∀ {A l} {x : A} → ∀ {P} → ConstrainedList P l → x ∈ l → P x constr-∈ [] () constr-∈ (p ∷ _) (exact _ _) = p constr-∈ (_ ∷ cl) (cons _ p) = constr-∈ cl p sortedHelper₂ : ∀ {A _≤_} {h : A} → ∀ {l'} → Sorted _≤_ l' → ∀ {l} → Permutation ll' → ConstrainedList (λ x → x ≤ h) l → ∀ {g'} → Sorted _≤_ (h ∷ g') → Sorted _≤_ (l' ++ h ∷ g') sortedHelper₂ {_} {_≤_} {h} {l'} sl' pll' cl {g'} sg' = loop [] l' refl sl' where loop : ∀ l₁ l₂ → l₁ ++ l₂ ≡ l' → Sorted _≤_ l₂ → Sorted _≤_ (l₂ ++ h ∷ g') loop _ .[] _ nil = sg' loop l₁ .(x ∷ []) p (one {x}) = two (constr-∈ cl $ perm-∈ x∈l' pll') sg' where x∈l' : x ∈ l' x∈l' = ≡-elim p (λ l → x ∈ l) (create-∈ l₁ x []) loop l₁ .(x ∷ y ∷ l) p≡ (two {x} {y} {l} x≤y ps) = two x≤y $ loop (l₁ ++ [ x ]) (y ∷ l) p' ps where p' : (l₁ ++ [ x ]) ++ y ∷ l ≡ l' p' = ≡-trans (++-assoc l₁ [ x ] (y ∷ l)) p≡ sortedHelper₁ : ∀ {A _≤_} {h : A} → ∀ {l'} → Sorted _≤_ l' → ∀ {l} → Permutation ll' → ConstrainedList (λ x → x ≤ h) l → ∀ {g'} → Sorted _≤_ g' → ∀ {g} → Permutation gg' → ConstrainedList (λ x → h ≤ x) g → Sorted _≤_ (l' ++ h ∷ g') sortedHelper₁ sl' pll' cl nil _ _ = sortedHelper₂ sl' pll' cl one sortedHelper₁ sl' pll' cl {h ∷ t} sg' pgg' cg = sortedHelper₂ sl' pll' cl $ two (constr-∈ cg $ perm-∈ (exact ht) pgg') sg' quickSort : {A : Set} {_≤_ : A → A → Set} → (∀ xy → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l') quickSort _ [] = [] , nil , refl quickSort {A} {_≤_} _≤?_ (h ∷ t) = loop t [] [] [] [] refl where loop : ∀ ilg → ConstrainedList (λ x → x ≤ h) l → ConstrainedList (λ x → h ≤ x) g → Permutation t ((l ++ g) ++ i) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation (h ∷ t) l') loop [] lg cl cg p = l' ++ h ∷ g' , sortedHelper₁ sl' pll' cl sg' pgg' cg , perm-trans p₃ p₄ where lSort = quickSort _≤?_ l gSort = quickSort _≤?_ g l' = proj₁ lSort g' = proj₁ gSort sl' = proj₁ $ proj₂ lSort sg' = proj₁ $ proj₂ gSort pll' = proj₂ $ proj₂ lSort pgg' = proj₂ $ proj₂ gSort p₁ : Permutation (l ++ g) (l' ++ g') p₁ = perm-++ pll' pgg' p₂ : Permutation t (l' ++ g') p₂ = perm-trans (≡-elim (++-[] (l ++ g)) (λ x → Permutation tx) p) p₁ p₃ : Permutation (h ∷ t) (h ∷ l' ++ g') p₃ = perm-++ (refl {_} {[ h ]}) p₂ p₄ : Permutation (h ∷ l' ++ g') (l' ++ h ∷ g') p₄ = perm-del-ins-r [] hl' g' loop (h' ∷ t) lg cl cg p with h' ≤? h ... | inj₁ h'≤h = loop t (h' ∷ l) g (h'≤h ∷ cl) cg (perm-trans p p') where p' : Permutation ((l ++ g) ++ h' ∷ t) (h' ∷ (l ++ g) ++ t) p' = perm-del-ins-l [] (l ++ g) h' t ... | inj₂ h≤h' = loop tl (h' ∷ g) cl (h≤h' ∷ cg) (perm-trans p p') where p₁ : l ++ g ++ h' ∷ t ≡ (l ++ g) ++ h' ∷ t p₁ = ≡-sym $ ++-assoc lg (h' ∷ t) p₂ : l ++ (h' ∷ g) ++ t ≡ (l ++ h' ∷ g) ++ t p₂ = ≡-sym $ ++-assoc l (h' ∷ g) t p₃ : (h' ∷ g) ++ t ≡ h' ∷ g ++ t p₃ = ++-assoc [ h' ] gt p₄ : l ++ h' ∷ g ++ t ≡ l ++ (h' ∷ g) ++ t p₄ = ≡-sym $ ≡-elim p₃ (λ x → l ++ x ≡ l ++ h' ∷ g ++ t) refl p₅ : Permutation (l ++ g ++ h' ∷ t) (l ++ h' ∷ g ++ t) p₅ = perm-del-ins-l lgh' t p₆ : Permutation ((l ++ g) ++ h' ∷ t) (l ++ h' ∷ g ++ t) p₆ = ≡-elim p₁ (λ x → Permutation x (l ++ h' ∷ g ++ t)) p₅ p' : Permutation ((l ++ g) ++ h' ∷ t) ((l ++ h' ∷ g) ++ t) p' = ≡-elim (≡-trans p₄ p₂) (λ x → Permutation ((l ++ g) ++ h' ∷ t) x) p₆ showl : List ℕ → String showl [] = "[]" showl (h ∷ t) = show h +s+ "∷" +s+ showl t l₁ : List ℕ l₁ = 19 ∷ 6 ∷ 13 ∷ 2 ∷ 8 ∷ 15 ∷ 1 ∷ 10 ∷ 11 ∷ 2 ∷ 17 ∷ 4 ∷ [ 3 ] l₂ = quickSort decNat l₁ main = putCoStrLn ∘ toCostring $ showl $ proj₁ l₂
प्रस्तावक तुल्यता
data _≡_ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x ≡-cong : ∀ {ab} {A : Set a} {B : Set b} {xy} → x ≡ y → (f : A → B) → fx ≡ fy ≡-cong refl _ = refl ≡-elim : ∀ {l} {A : Set l} {xy : A} → x ≡ y → (P : A → Set l) → P x → P y ≡-elim refl _ p = p ≡-sym : ∀ {l} {A : Set l} {xy : A} → x ≡ y → y ≡ x ≡-sym refl = refl ≡-trans : ∀ {l} {A : Set l} {xyz : A} → x ≡ y → y ≡ z → x ≡ z ≡-trans refl refl = refl
जैसा कि आप यहां देख सकते हैं, सब कुछ सरल है: केवल एक स्वयंसिद्ध है, जो कहता है कि दो वस्तुएं समान हैं यदि वे एक और समान हैं। यह तुल्यता के प्रमाण के साथ काम करने के लिए सहायक कार्यों को भी परिभाषित करता है। मुझे लगता है कि यहां सब कुछ स्पष्ट है। मैं केवल
≡-elim के उदाहरण के साथ
समझाऊंगा : प्रकार
x can
y के तर्क का एकमात्र मान
refl हो सकता है, जिसका एक निहित पैरामीटर है, जिसमें
≡-elim refl _ p लाइन एक ही समय में
x और
y के बराबर है, इसलिए
p का मान दोनों है। प्रकार और
पी एक्स और
पी वाई , और यदि
पी का मूल्य
पी वाई का है , तो इस स्थिति में यह result
-elim फ़ंक्शन का परिणाम होगा।
संबद्धता संघनन ऑपरेशन
++-assoc : ∀ {l} {A : Set l} (l₁ l₂ l₃ : List A) → (l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃) ++-assoc [] l₂ l₃ = refl ++-assoc (h ∷ t) l₂ l₃ = ≡-cong (++-assoc t l₂ l₃) (λ x → h ∷ x)
यहां
$ एक एप्लीकेशन ऑपरेटर से ज्यादा कुछ नहीं है, जैसा कि हास्केल में है। परिभाषा से यह स्पष्ट है कि यह कार्य (या हम लेम्मा कह सकते हैं) तीन मनमाना सूचियों के लिए संघटन संचालन की संगति सिद्ध करता है। मैं यह नोट करना चाहता हूं कि संकलन के दौरान मौजूदा परिभाषाओं का उपयोग करके शर्तों को आंशिक रूप से कम किया जाता है। इस फ़ंक्शन में, निम्न होता है:
थेर्म
≡-cong (++-assoc t l₂ l₃) (λ x → h ∷ x)
प्रकार है
h ∷ (t ++ l₂) ++ l₃ ≡ h ∷ t ++ (l₂ ++ l₃)
और हमें एक प्रकार की आवश्यकता है
(l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃)
या
((h ∷ t) ++ l₂) ++ l₃ ≡ (h ∷ t) ++ (l₂ ++ l₃)
यह दिया गया
l₁ = h ∷ t
इसके अलावा, संकलक, संघनन की परिभाषा का उपयोग करते हुए, इन शर्तों को कुछ सामान्य रूप में कम कर देता है।
अवधि की परिभाषा का उपयोग करके शब्द के साथ प्रयास करें,
((h ∷ t) ++ l₂) ++ l₃ ≡ (h ∷ t) ++ (l₂ ++ l₃)
एक शब्द मिलता है
h ∷ (t ++ l₂) ++ l₃ ≡ h ∷ t ++ (l₂ ++ l₃)
आपको यह भी विचार करने की आवश्यकता है कि समवर्ती ऑपरेशन साहचर्य रूप से सही है - लेकिन यह समझने के लिए आवश्यक नहीं है।
परिवर्तनशीलता और क्रमचय की समरूपता
perm-trans : ∀ {A} {l₁ l₂ l₃ : List A} → Permutation l₁ l₂ → Permutation l₂ l₃ → Permutation l₁ l₃ perm-trans p refl = p perm-trans p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm l₁ x₁ x₂ l₂ $ perm-trans p₁ p₂ perm-sym : ∀ {A} {l₁ l₂ : List A} → Permutation l₁ l₂ → Permutation l₂ l₁ perm-sym refl = refl perm-sym (perm l₁ x₁ x₂ l₂ p) = perm-trans (perm l₁ x₂ x₁ l₂ refl) (perm-sym p)
"लंबे" क्रमचय बाएं और दाएं
perm-del-ins-r : ∀ {A} (l₁ : List A) (x : A) (l₂ l₃ : List A) → Permutation (l₁ ++ x ∷ l₂ ++ l₃) (l₁ ++ l₂ ++ x ∷ l₃) perm-del-ins-r l₁ x [] l₃ = refl perm-del-ins-r l₁ x (h ∷ t) l₃ = perm-trans p₀ p₅ where p₀ : Permutation (l₁ ++ x ∷ h ∷ t ++ l₃) (l₁ ++ h ∷ x ∷ t ++ l₃) p₀ = perm l₁ hx (t ++ l₃) refl p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃) p₁ = perm-del-ins-r (l₁ ++ [ h ]) xt l₃ p₂ : (l₁ ++ [ h ]) ++ t ++ x ∷ l₃ ≡ l₁ ++ h ∷ t ++ x ∷ l₃ p₂ = ++-assoc l₁ [ h ] (t ++ x ∷ l₃) p₃ : (l₁ ++ [ h ]) ++ x ∷ t ++ l₃ ≡ l₁ ++ h ∷ x ∷ t ++ l₃ p₃ = ++-assoc l₁ [ h ] (x ∷ t ++ l₃) p₄ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃) p₄ = ≡-elim p₂ (λ y → Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) y) p₁ p₅ : Permutation (l₁ ++ h ∷ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃) p₅ = ≡-elim p₃ (λ y → Permutation y (l₁ ++ h ∷ t ++ x ∷ l₃)) p₄ perm-del-ins-l : ∀ {A} (l₁ l₂ : List A) (x : A) (l₃ : List A) → Permutation (l₁ ++ l₂ ++ x ∷ l₃) (l₁ ++ x ∷ l₂ ++ l₃) perm-del-ins-l l₁ l₂ x l₃ = perm-sym $ perm-del-ins-r l₁ x l₂ l₃
ये विशेषताएँ अधिक रोचक हैं। यहाँ मैं केवल यह नोट करना चाहता हूं कि यदि हम प्रकारों को प्रमेय या नींबू के रूप में मानते हैं, और इसी प्रकार के शब्दों को प्रमाण के रूप में मानते हैं, तो यह स्पष्ट है कि किसी निश्चित कथन के प्रमाण (साथ ही संबंधित प्रकार के) की कोई भी संख्या हो सकती है। उदाहरण के लिए, यह मुझे लगता है कि ऊपर दिए गए कार्य को आसान साबित किया जा सकता है। यह भी दिलचस्प है कि मैंने जिस प्रकार की सूची का हवाला दिया है वह एक प्रकार का सिंगलटन है: प्रत्येक प्रकार का एक प्रतिनिधि होता है। क्रमपरिवर्तन के लिए, एक प्रकार के लिए अलग-अलग शब्दों की एक अनंत संख्या हो सकती है (उदाहरण के लिए, आप एक ही तत्वों को दो बार पुनर्व्यवस्थित कर सकते हैं ताकि सूचियां न बदलें)।
प्राकृतिक संख्या पर आदेश
data ℕ : Set where zero : ℕ suc : ℕ → ℕ data _≤_ : ℕ → ℕ → Set where z≤n : ∀ {n} → zero ≤ n s≤s : ∀ {mn} (m≤n : m ≤ n) → suc m ≤ suc n decNat : (xy : ℕ) → (x ≤ y) ⊎ (y ≤ x) decNat zero y = inj₁ z≤n decNat (suc x) (suc y) with decNat xy ... | inj₁ p = inj₁ (s≤sp) ... | inj₂ p = inj₂ (s≤sp) decNat (suc x) zero = inj₂ z≤n
और अंत में, प्राकृतिक संख्याओं पर आदेश का निर्धारण करने के लिए समाधान प्रक्रिया। (चर का नाम कैसे दिया जाता है, इस पर ध्यान दें - वह सब कुछ जिसमें बिना रिक्त स्थान के एक शब्द है।) विधेय
_≤_ का उपयोग किया जाता है । दो स्वयंसिद्ध शब्द पेश किए गए हैं, जिनमें से एक का कहना है कि कोई भी संख्या शून्य से अधिक या उसके बराबर है, और दूसरा यह है कि यदि एक संख्या दूसरे से अधिक है, तो अनुपात को संरक्षित किया जाएगा यदि उनमें से एक जोड़ा जाता है।
निर्माण के
साथ यहां भी उपयोग किया जाता है - लेकिन मुझे लगता है कि इसका उपयोग बेहद स्पष्ट है।
वह सब है :)
मैं खुद से कहूंगा कि इस तरह के कार्यक्रम लिखना बहुत दिलचस्प है।