कोक परस्पर अपरिवर्तनीय प्रकारों को समान पैरामीटर क्यों होना चाहिए?

Question

Arthur's suggestion के बाद, मैंने अपने Fixpoint को पारस्परिक Inductive संबंध के संबंध में बदल दिया जो "ड्रिलिंग डाउन" के बजाय गेम के बीच अलग-अलग तुलना "बनाता है"।

लेकिन अब मैं पूरी तरह से नया त्रुटि संदेश मिल रहा हूँ:

Error: Parameters should be syntactically the same for each inductive type. 

मुझे लगता है कि त्रुटि संदेश कह रही है कि मैं इन आपसी आगमनात्मक परिभाषाओं के सभी के लिए एक ही सटीक मानकों की जरूरत है।

मुझे एहसास है कि इस के आसपास पाने के लिए सरल हैक्स (अप्रयुक्त डमी चर, forall के अंदर सब कुछ के साथ लंबे कार्यात्मक प्रकार), लेकिन मुझे नहीं पता कि मुझे क्यों करना चाहिए।

क्या कोई आपसी अप्रत्यक्ष प्रकारों पर इस प्रतिबंध के पीछे तर्क को समझा सकता है? क्या यह लिखने का एक और शानदार तरीका है? क्या यह प्रतिबंध यह भी दर्शाता है कि एक-दूसरे के लिए अपरिवर्तनीय कॉल सभी एक ही पैरामीटर का उपयोग कर सकते हैं (इस मामले में मुझे किसी भी हैक के बारे में पता नहीं है जो कोड डुप्लिकेशन की भयानक मात्रा को बचाता है)?

(सभी प्रकार के और इस तरह के compare_quest, खेल, g1side आदि के रूप में शब्दों की परिभाषा क्या वे मेरी first question में थे से अपरिवर्तित रहे हैं।

Inductive gameCompare (c : compare_quest) : game -> game -> Prop := 
| igc : forall g1 g2 : game, 
    innerGCompare (nextCompare c) (compareCombiner c) (g1side c) (g2side c) g1 g2 -> 
    gameCompare c g1 g2 
with innerGCompare (next_c : compare_quest) (cbn : combiner) (g1s g2s : side) 
    : game -> game -> Prop := 
| compBoth : forall g1 g2 : game, 
    cbn (listGameCompare next_c cbn (g1s g1) g2) 
     (gameListCompare next_c cbn g1 (g2s g2)) -> 
    innerGCompare next_c cbn g1s g2s g1 g2 
with listGameCompare (c : compare_quest) (cbn : combiner) : gamelist -> game -> Prop := 
| emptylgCompare : cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2 
| otlgCompare : forall (g1_cdr : gamelist) (g1_car g2 : game), 
    (cbn (listGameCompare c cbn g1_cdr g2) (gameCompare c g1_car g2)) -> 
    listGameCompare c cbn (listCons g1_car g1_cdr) g2 
with gameListCompare (c : compare_quest) (cbn : combiner) : game -> gamelist -> Prop := 
| emptyglCompare : cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist 
| otglCompare : forall (g1 g2_car : game) (g2_cdr : gamelist), 
    (cbn (gameListCompare c cbn g1 g2_cdr) (gameCompare c g1 g2_car)) -> 
    gameListCompare c cbn g1 (listCons g2_car g2_cdr). 

CGT में, आम तौर पर दो खिलाड़ियों (Left और Right नामित) एक खेल खेलना शुरू कर देता है जहां खिलाड़ी आखिरी कदम जीतता है। प्रत्येक गेम (जिसका अर्थ है खेल में प्रत्येक स्थिति) को Left के विकल्पों के सेट के रूप में पढ़ा जा सकता है और के रूप में लिखे गए Right के विकल्प के सेट के रूप में पढ़ा जा सकता है। दो गेम की तुलना में, वे चार अलग-अलग तरीकों से तुलना कर सकते हैं: <, >, =, या ||।

एक खेल A < B है अगर B सख्ती से Left के लिए A तुलना में बेहतर है, जो पहली बार चला जाता है की परवाह किए बिना। A > BAB से Left के लिए बेहतर है। A = B यदि दो गेम समकक्ष हैं (इस अर्थ में कि गेम A + -B का योग शून्य-गेम है ताकि खिलाड़ी जो पहले हार जाए)। और, A || B यदि Left के लिए कौन सा गेम बेहतर है तो यह निर्भर करता है कि पहले कौन जाता है। A के सभी अगर सही बच्चों के Left बच्चों <| B और A <|B के सभी कर रहे हैं '

• A <= B: दो मैचों के बीच तुलना की जाँच करने के

  एक तरह से इस प्रकार है।

• A <| BA एक सही बच्चे जो <= B या यदि A <=B के बाईं बच्चों के किसी भी रखता है।

• और इसी तरह >= और >| के लिए।

तो, तो देखकर जो इन संबंधों की जोड़ी दो मैचों A और B पर लागू होते हैं, यह निर्धारित करने के लिए संभव है कि क्या A < B (A<=B और A<|B), A=B (A<=B और A>=B), A > B (A>=B और A>|B) , या A || B (A<|B और A>|B)।

यहां wiki article on CGT है।

Answer 1

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

शायद इसे कोक क्लब मेलिंग सूची में अग्रेषित किया जाना चाहिए? :)

आपको इसे काम करने के लिए तीर के दाईं ओर सबकुछ रखना नहीं है। एक चीज जो आप कर सकते हैं वह है सब कुछ डालने के लिए compare_quest पैरामीटर दाईं ओर। आप एक ही प्रकार आप एक निर्माता में तय कर रहे हैं की एक आगमनात्मक उपयोग करते हैं, पैरामीटर आप दे एक आप शीर्षक पर देने के रूप में ही नहीं है, तो यह है कि ठीक है:

Inductive gameCompare (c : compare_quest) : game -> game -> Prop := 
| igc : forall g1 g2 : game, 
    innerGCompare (nextCompare c) (compareCombiner c) (g1side c) (g2side c) g1 g2 -> 
    gameCompare c g1 g2 

with innerGCompare (c : compare_quest) : combiner -> side -> side -> 
    game -> game -> Prop := 
| compBoth : forall cbn g1s g2s (g1 g2 : game), 
    cbn (listGameCompare c cbn (g1s g1) g2) 
     (gameListCompare c cbn g1 (g2s g2)) -> 
    innerGCompare c cbn g1s g2s g1 g2 

with listGameCompare (c : compare_quest) : combiner -> gamelist -> game -> Prop := 
| emptylgCompare : forall cbn, cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2 
| otlgCompare : forall cbn (g1_cdr : gamelist) (g1_car g2 : game), 
    (cbn (listGameCompare c cbn g1_cdr g2) (gameCompare c g1_car g2)) -> 
    listGameCompare c cbn (listCons g1_car g1_cdr) g2 

with gameListCompare (c : compare_quest) : combiner -> game -> gamelist -> Prop := 
| emptyglCompare : forall cbn, cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist 
| otglCompare : forall cbn (g1 g2_car : game) (g2_cdr : gamelist), 
    (cbn (gameListCompare c cbn g1 g2_cdr) (gameCompare c g1 g2_car)) -> 
    gameListCompare c cbn g1 (listCons g2_car g2_cdr). 

दुर्भाग्य से , इस का मूल्यांकन करने की कोशिश कर रहा एक नया त्रुटि :(

Error: Non strictly positive occurrence of "listGameCompare" in 
"forall (cbn : Prop -> Prop -> Prop) (g1s g2s : game -> gamelist) 
    (g1 g2 : game), 
    cbn (listGameCompare c cbn (g1s g1) g2) (gameListCompare c cbn g1 (g2s g2)) -> 
    innerGCompare c cbn g1s g2s g1 g2". 

यह त्रुटि भी बहुत कुछ Coq में आम है देता है। यह शिकायत है कि आप cbn के प्रकार आप एक तर्क के रूप परिभाषित कर रहे हैं गुजर रहे हैं, क्योंकि वह यह है कि हो सकता है पर एक तीर (एक नकारात्मक घटना) के को छोड़कर टाइप करें, जो तार्किक I nconsistencies।

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

अद्यतन: मैंने कोक में कुछ सीजीटी को औपचारिक बनाने के बारे में लेखों की एक श्रृंखला शुरू की है। आप पहले एक here पा सकते हैं।