haskell - क्या हास्क या एजडा में बराबरी है?




agda category-theory (2)

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

तो, हम जानते हैं कि हस्क के उत्पाद हैं, कम या ज्यादा (मैं आदर्श-हस्क के साथ काम कर रहा हूं, यहां, निश्चित रूप से)। मुझे इस बात में दिलचस्पी है कि इसमें बराबरी है या नहीं (किस स्थिति में इसकी सभी सीमित सीमाएँ होंगी)।

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

अब, एग्दा थोड़ा अधिक आशाजनक लगता है: वहाँ उप-विषय बनाना आसान है। क्या स्पष्ट सिग्मा प्रकार Σ A (λ x → fx == gx) एक तुल्यकारक है? यदि विवरण काम नहीं करता है, तो क्या यह नैतिक रूप से एक तुल्यकारक है?


Hask

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

मैंने एक वास्तविक रक्षात्मक प्रतिधारण के साथ आने की कोशिश करते हुए कुछ समय बिताया, और पाया कि कुछ संदर्भों से यह पता चलता है कि ऐसा नहीं किया जा सकता है, लेकिन सबूतों के साथ। हालाँकि, अगर आपके पास कुछ "नैतिक" प्रतिपक्ष हैं; मैं यह साबित नहीं कर सकता कि हास्केल में कोई तुल्यकारक मौजूद नहीं है, लेकिन यह निश्चित रूप से असंभव लगता है!

उदाहरण 1

f, g: ([Int], Int) -> Int

f (p,v) = treat p as a polynomial with given coefficients, and evaluate p(v).
g _ = 0

तुल्यकारक "सभी जोड़े (पी, एन) का प्रकार होना चाहिए जहां पी (एन) = 0, साथ ही एक फ़ंक्शन इन जोड़ियों को ([इंट], इंट) में इंजेक्ट करता है। हिल्बर्ट की 10 वीं समस्या से, यह सेट अविश्वसनीय है। यह मुझे लगता है कि इसे हास्केल प्रकार होने की संभावना को बाहर करना चाहिए, लेकिन मैं यह साबित नहीं कर सकता कि (क्या यह संभव है कि इस प्रकार का निर्माण करने का कोई विचित्र तरीका है जिसे किसी ने नहीं खोजा है?)। शायद यह मैंने एक डॉट या दो से नहीं जोड़ा है - शायद यह साबित करना असंभव है कि यह कठिन नहीं है?

उदाहरण 2

कहते हैं कि आपके पास एक प्रोग्रामिंग भाषा है। आपके पास एक कंपाइलर है जो स्रोत कोड और एक इनपुट लेता है और एक फ़ंक्शन का उत्पादन करता है, जिसके लिए फ़ंक्शन का निश्चित बिंदु आउटपुट है। (जबकि हमारे पास इस तरह के कंपाइलर नहीं हैं, इस तरह के शब्दार्थों को निर्दिष्ट करना अनसुना नहीं है)। मतलब आपके पास है

compiler : String -> Int -> (Int -> Int)

(संयुक्त राष्ट्र) करी कि एक समारोह में

compiler' : (String, Int, Int) -> Int

और एक फ़ंक्शन जोड़ें

id' : (String, Int, Int) -> Int
id' (_,_,x) = x

तब संकलक ', आईडी' का तुल्यकारक स्रोत प्रोग्राम, इनपुट, आउटपुट के तीनों का संग्रह होगा - और यह अविश्वसनीय है क्योंकि प्रोग्रामिंग भाषा पूरी तरह से सामान्य है।

और ज्यादा उदाहरण

अपनी पसंदीदा अनिर्णायक समस्या चुनें: इसमें आम तौर पर यह तय करना शामिल होता है कि कोई वस्तु किसी सेट का सदस्य है या नहीं। आपके पास अक्सर एक कुल फ़ंक्शन होता है जिसका उपयोग किसी विशेष ऑब्जेक्ट के लिए इस संपत्ति की जांच करने के लिए किया जा सकता है। आप इस फ़ंक्शन का उपयोग एक इक्विलाइज़र बनाने के लिए कर सकते हैं जहाँ प्रकार आपके अविभाज्य सेट में सभी आइटम होना चाहिए। यहीं से पहले दो उदाहरण आए, और टन अधिक हैं।

AGDA

मैं अगाडा से परिचित नहीं हूँ। मेरा अंतर्ज्ञान यह है कि आपका सिग्मा-प्रकार एक तुल्यकारक होना चाहिए: आप आवश्यक इंजेक्शन फ़ंक्शन के साथ-साथ नीचे लिख सकते हैं, और ऐसा लगता है कि यह पूरी तरह से परिभाषा को संतुष्ट करता है। हालांकि, कोई व्यक्ति जो अगाडा का उपयोग नहीं करता है, मुझे नहीं लगता कि मैं वास्तव में विवरण की जांच करने के लिए योग्य हूं।

हालांकि असली व्यावहारिक मुद्दा यह है कि उस प्रकार का सिग्माटेकिंग हमेशा टाइप करने योग्य नहीं होगा, इसलिए ऐसा करना हमेशा उपयोगी नहीं होता है। उपरोक्त सभी उदाहरणों में, आप अपने द्वारा दिए गए सिग्मा प्रकार को लिख सकते हैं, लेकिन यदि कोई प्रमाण के बिना उस प्रकार का सदस्य है तो आप आसानी से जांच नहीं कर पाएंगे।

संयोग से, यही कारण है कि हास्केल को समतुल्य होने में सक्षम नहीं होना चाहिए: यदि यह किया गया, तो टाइपेकिटिंग अनिर्दिष्ट होगा! आश्रित प्रकार वह है जो सब कुछ टिक कर देता है। वे इसके प्रकारों में दिलचस्प गणितीय संरचनाओं को व्यक्त करने में सक्षम होना चाहिए, जबकि हास्केल तब से नहीं कर सकता है जब तक कि इसके प्रकार का सिस्टम निर्णायक नहीं है। इसलिए, मैं स्वाभाविक रूप से आदर्शित एजडा को सभी परिमित सीमाओं की अपेक्षा करूंगा (मुझे अन्यथा निराश होना पड़ेगा)। वही अन्य निर्भर प्रकार की भाषाओं के लिए जाता है; उदाहरण के लिए, कोक को निश्चित रूप से सभी सीमाएं होनी चाहिए।


tl; डॉ प्रस्तावित अभ्यर्थी काफी समतुल्य नहीं है, लेकिन इसका अप्रासंगिक समकक्ष है

अगड़ा में बराबरी का उम्मीदवार अच्छा लग रहा है। तो चलिए इसे आजमाते हैं। हमें कुछ बुनियादी किट की आवश्यकता होगी। यहाँ मेरे refusenik ASCII निर्भर जोड़ी प्रकार और सजातीय अंतरंग समानता हैं।

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg

data _==_ {X : Set}(x : X) : X -> Set where
  refl : x == x

यहां दो कार्यों के लिए एक इक्विलाइज़र के लिए आपका उम्मीदवार है

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Sg S \ s -> f s == g s

fst प्रोजेक्शन के साथ Q fg को S में भेजना।

यह क्या कहता है: Q fg का एक तत्व स्रोत प्रकार का एक तत्व है, साथ में एक प्रमाण के साथ जो fs == gs । लेकिन क्या यह एक तुल्यकारक है? आइए इसे बनाने की कोशिश करते हैं।

यह कहने के लिए कि एक तुल्यकारक क्या है, मुझे फ़ंक्शन संरचना को परिभाषित करना चाहिए।

_o_ : {R S T : Set} -> (S -> T) -> (R -> S) -> R -> T
(f o g) x = f (g x)

इसलिए अब मुझे यह दिखाने की जरूरत है कि कोई भी h : R -> S जो पहचानता है कि foh और goh को उम्मीदवार fst : Q fg -> S माध्यम से कारक होना चाहिए fst : Q fg -> S मुझे दोनों अन्य घटक देने की आवश्यकता है, u : R -> Q fg और सबूत जो वास्तव में fst ou रूप में कारक हैं। यहां चित्र है: (Q fg , fst) एक तुल्यकारक है यदि जब भी आरेख बिना u के चलता है, तो u साथ u को जोड़ने का एक अनूठा तरीका है जो अभी भी आ रहा है।

यहाँ मध्यस्थता u का अस्तित्व है।

mediator : {R S T : Set}(f g : S -> T)(h : R -> S) ->
           (q : (f o h) == (g o h)) ->
           Sg (R -> Q f g) \ u -> h == (fst o u)

स्पष्ट रूप से, मुझे S के उसी तत्व को चुनना चाहिए जो h उठाता है।

mediator f g h q = (\ r -> (h r , ?0)) , ?1

मुझे दो सबूत दायित्वों के साथ छोड़कर

?0 : f (h r) == g (h r)
?1 : h == (\ r -> h r)

अब, ?1 को केवल refl किया जा सकता है क्योंकि Agda की निश्चित समता कार्यों के लिए एटा-कानून है। के लिए ?0 , हम q द्वारा धन्य हैं। समान कार्य सम्मान आवेदन

funq : {S T : Set}{f g : S -> T} -> f == g -> (s : S) -> f s == g s
funq refl s = refl

तो हम ले सकते हैं ?0 = funq qr

लेकिन हमें समय से पहले नहीं मनाना चाहिए, क्योंकि एक मध्यस्थता के अस्तित्व के लिए पर्याप्त नहीं है। हमें इसकी विशिष्टता की भी आवश्यकता है। और यहाँ पहिया विस्की जाने की संभावना है, क्योंकि == अंतरंग है , इसलिए विशिष्टता का मतलब है कि मध्यस्थता मानचित्र को लागू करने का केवल एक ही तरीका है। लेकिन फिर, हमारी धारणाएं भी हैं ...

यहां हमारा प्रमाण दायित्व है। हमें यह दिखाना चाहिए कि किसी भी अन्य मध्यस्थता आकारिकी mediator द्वारा चुने गए के बराबर है।

mediatorUnique :
  {R S T : Set}(f g : S -> T)(h : R -> S) ->
  (qh : (f o h) == (g o h)) ->
  (m : R -> Q f g) ->
  (qm : h == (fst o m)) ->
  m == fst (mediator f g h qh)

हम तुरंत क्यूएम के माध्यम से स्थानापन्न कर सकते हैं और प्राप्त कर सकते हैं

mediatorUnique f g .(fst o m) qh m refl = ?

? :  m == (\ r -> (fst (m r) , funq qh r))

जो अच्छा लगता है, क्योंकि अगाडा के पास रिकॉर्ड के लिए एटा कानून हैं, इसलिए हम जानते हैं कि

m == (\ r -> (fst (m r) , snd (m r)))

लेकिन जब हम बनाने की कोशिश करते हैं ? = refl ? = refl , हमें शिकायत मिलती है

snd (m _) != funq qh _ of type f (fst (m _)) == g (fst (m _))

जो कि कष्टप्रद है, क्योंकि पहचान प्रमाण अद्वितीय हैं (मानक विन्यास में)। अब, आप इस बात से बाहर निकल सकते हैं कि हम अनैच्छिकता को पोस्ट कर सकते हैं और समानता के बारे में कुछ अन्य तथ्यों का उपयोग कर सकते हैं

postulate ext : {S T : Set}{f g : S -> T} -> ((s : S) -> f s == g s) -> f == g

sndq : {S : Set}{T : S -> Set}{s : S}{t t' : T s} ->
       t == t' -> _==_ {Sg S T} (s , t) (s , t')
sndq refl = refl

uip : {X : Set}{x y : X}{q q' : x == y} -> q == q'
uip {q = refl}{q' = refl} = refl

? = ext (\ s -> sndq uip)

लेकिन यह ओवरकिल है, क्योंकि एकमात्र समस्या कष्टप्रद समानता प्रमाण बेमेल है: कार्यान्वयन के कम्प्यूटेशनल भागों नाक पर मेल खाते हैं। तो तय है कि अप्रासंगिकता के साथ काम करना है। मैं Sg को Ex istential क्वांटिफायर द्वारा प्रतिस्थापित करता हूं, जिसका दूसरा घटक एक डॉट के साथ अप्रासंगिक के रूप में चिह्नित है। अब यह मायने नहीं रखता कि हम किस प्रमाण का उपयोग करते हैं कि साक्षी अच्छा है।

record Ex (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    .snd : T fst
open Ex

और नया उम्मीदवार तुल्यकारक है

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Ex S \ s -> f s == g s

संपूर्ण निर्माण पहले की तरह से गुजरता है, सिवाय पिछले दायित्व के

? = refl

स्वीकार कर लिया है!

तो हाँ, यहां तक ​​कि अंतरंग सेटिंग में, एटा कानून और क्षेत्रों को चिह्नित करने की क्षमता के रूप में अप्रासंगिक हमें बराबरी देते हैं।

इस निर्माण में कोई भी अयोग्य टाइपकास्टिंग शामिल नहीं था।





category-theory