यह Agda के इंटरैक्टिव मोड का उपयोग करने के लिए एक महान समय है। यह एक खेल की तरह है। आप इसे मैन्युअल रूप से भी कर सकते हैं लेकिन यह अधिक काम है। यहाँ मैं क्या किया है:
f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = ?
Goal: B
x : (((A -> B) -> A) -> A) -> B
मूल रूप से केवल कदम हमारे पास x
लागू होते हैं, तो चलो कि कोशिश करते है।
f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x ?
Goal: ((A -> B) -> A) -> A
x : (((A -> B) -> A) -> A) -> B
अब हमारा लक्ष्य एक फ़ंक्शन प्रकार है, तो चलिए लैम्ब्डा आज़माएं।
f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> ?)
Goal: A
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A
हम एक A
की जरूरत है, और y
इसे हमें दे सकते हैं अगर हम सही तर्क के साथ प्रदान करते हैं। सुनिश्चित नहीं हैं कि क्या है कि अभी तक है, लेकिन y
हमारे सबसे अधिक उपयुक्त रहेगी:
f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y ?)
Goal: A -> B
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A
हमारा लक्ष्य एक समारोह प्रकार तो चलो एक लैम्ब्डा का उपयोग करते हैं है।
f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y (\z -> ?))
Goal: B
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A
z : A
अब हम एक B
की जरूरत है, और केवल एक चीज है कि हम एक B
दे सकते हैं x
है, इसलिए की है कि फिर से कोशिश करते हैं।
f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y (\z -> x ?))
Goal: ((A -> B) -> A) -> A
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A
z : A
अब हमारा लक्ष्य A
वाला फ़ंक्शन प्रकार है, लेकिन हम जो एक A
तो हम तर्क का उपयोग करने की जरूरत नहीं है z
है। हम इसे अनदेखा करेंगे और z
वापस कर देंगे।
f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y (\z -> x (\_ -> z)))
और वहां आप जाते हैं!
यह एक जटिल समस्या है। अंतर्ज्ञानवादी अनुक्रम कैलकुलेशन एलजे और इसके संबंधित परिणाम इसके "मानक" समाधान में महत्वपूर्ण भूमिका निभाते हैं। डीजिन उपकरण इस प्रणाली (लगभग मोटे तौर पर) में एक सबूत खोज का "प्रसिद्ध" कार्यान्वयन है, और करी-हॉवर्ड आइसोमोर्फिज्म इन प्रमाणों को लैम्ब्डा शब्दों के रूप में प्रस्तुत करने की अनुमति देता है। – chi
आगे, एक सूत्र को "रूपांतरित" करने के रूप में ऐसी कोई चीज़ नहीं है जो लैम्ब्डा अभिव्यक्ति में हो।यह प्रमेय को अपने सबूतों में "रूपांतरित करने" की मात्रा होगी, जो बकवास है - प्रमेय सामान्य रूप से कई अलग-अलग सबूत स्वीकार करते हैं। सबसे अच्छा, आप सबूत खोज कर सकते हैं, जहां आप एक ऐसे सबूत की तलाश करते हैं। – chi
स्पष्टीकरण के लिए धन्यवाद। मैं कम समय में बहुत उपयोगी जानकारी के लिए वास्तव में खुश हूँ। –