कोक

Question

में नकारात्मक अपरिवर्तनीय प्रकारों के साथ झूठा प्रदान करना सीपीडीटी का तीसरा अध्याय संक्षेप में चर्चा करता है कि कोक में नकारात्मक अपरिवर्तनीय प्रकार क्यों प्रतिबंधित हैं। अगर हम

Inductive term : Set := 
| App : term -> term -> term 
| Abs : (term -> term) -> term. 

था तो हम आसानी से एक समारोह

Definition uhoh (t : term) : term := 
    match t with 
    | Abs f => f t 
    | _ => t 
    end. 

निर्धारित कर सकते हैं ताकि अवधि uhoh (Abs uhoh) गैर-सांत है, जो के साथ "हम हर प्रमेय साबित करने में सक्षम हो जाएगा" होगा।

मैं गैर-समाप्ति भाग को समझता हूं, लेकिन मुझे नहीं पता कि हम इसके साथ कुछ कैसे साबित कर सकते हैं। उपरोक्त परिभाषित term का उपयोग करके False कैसे साबित होगा?

Answer 1

अपने प्रश्न को पढ़ने से मुझे एहसास हुआ कि मुझे एडम के तर्क को समझ में नहीं आया। लेकिन इस मामले में असंगतता कैंटोर के सामान्य diagonal argument (विरोधाभासों और तर्क में पहेली का कभी खत्म होने वाला स्रोत) से काफी आसानी से परिणाम देती है।

Section Diag. 

Variable T : Type. 

Variable test : T -> bool. 

Variables x y : T. 

Hypothesis xT : test x = true. 
Hypothesis yF : test y = false. 

Variable g : (T -> T) -> T. 
Variable g_inv : T -> (T -> T). 

Hypothesis gK : forall f, g_inv (g f) = f. 

Definition kaboom (t : T) : T := 
    if test (g_inv t t) then y else x. 

Lemma kaboom1 : forall t, kaboom t <> g_inv t t. 
Proof. 
    intros t H. 
    unfold kaboom in H. 
    destruct (test (g_inv t t)) eqn:E; congruence. 
Qed. 

Lemma kaboom2 : False. 
Proof. 
    assert (H := @kaboom1 (g kaboom)). 
    rewrite -> gK in H. 
    congruence. 
Qed. 

End Diag. 

यह एक सामान्य विकास कि term प्रकार CPDT में परिभाषित के साथ instantiated किया जा सकता है: निम्नलिखित मान्यताओं पर विचार करें T होगा term, x और y है कि हम में भेद परीक्षण कर सकते हैं term के दो घटकों को होगा (उदाहरण के लिए App (Abs id) (Abs id) और Abs id)। मुख्य बिंदु आखिरी धारणा है: हम मानते हैं कि हमारे पास एक उलटा कार्य g : (T -> T) -> T है, जो आपके उदाहरण में Abs होगा। उस फ़ंक्शन का उपयोग करके, हम सामान्य विकर्णकरण चाल चलाते हैं: हम एक फ़ंक्शन kaboom परिभाषित करते हैं जो कि प्रत्येक कार्य T -> T से अलग है, जिसमें स्वयं भी शामिल है। उस से विरोधाभास परिणाम।