2015-02-08 24 views
5

मुझे साधारण तर्क सूत्र को लैम्ब्डा अभिव्यक्ति (उस सूत्र का सबूत) में परिवर्तित करते समय एक गलतफहमी है।हास्केल लैम्ब्डा अभिव्यक्तियां और सरल तर्क सूत्र

तो, मेरे पास निम्न सूत्र है: ((((ए-> बी) -> ए) -> ए) -> बी) -> बी कहां -> मतलब तार्किक ऑपरेटर का मतलब है।

मैं किसी भी कार्यात्मक भाषा (हास्केल, अधिमानतः) में कुछ लैम्ब्डा अभिव्यक्ति कैसे लिख सकता हूं?

मैं कुछ "परिणाम" है, लेकिन मैं वास्तव में यकीन नहीं है कि यह ऐसा करने का सही तरीका है हूँ:

  • (((लैम्ब्डा एफ -> लैम्ब्डा ए) -> ए) -> लैम्ब्डा बी) -> बी
  • ((((लैम्ब्डा A -> लैम्ब्डा बी) -> ए) -> ए) -> बी) -> बी

यह कैसे लैम्ब्डा में सूत्र tranform करने के लिए संभव हो सकता है अभिव्यक्ति? यदि आप जानते हैं कि कुछ समस्या इस मुद्दे को संदर्भित करती है तो यह बहुत उपयोगी होगा।

धन्यवाद

+2

यह एक जटिल समस्या है। अंतर्ज्ञानवादी अनुक्रम कैलकुलेशन एलजे और इसके संबंधित परिणाम इसके "मानक" समाधान में महत्वपूर्ण भूमिका निभाते हैं। डीजिन उपकरण इस प्रणाली (लगभग मोटे तौर पर) में एक सबूत खोज का "प्रसिद्ध" कार्यान्वयन है, और करी-हॉवर्ड आइसोमोर्फिज्म इन प्रमाणों को लैम्ब्डा शब्दों के रूप में प्रस्तुत करने की अनुमति देता है। – chi

+3

आगे, एक सूत्र को "रूपांतरित" करने के रूप में ऐसी कोई चीज़ नहीं है जो लैम्ब्डा अभिव्यक्ति में हो।यह प्रमेय को अपने सबूतों में "रूपांतरित करने" की मात्रा होगी, जो बकवास है - प्रमेय सामान्य रूप से कई अलग-अलग सबूत स्वीकार करते हैं। सबसे अच्छा, आप सबूत खोज कर सकते हैं, जहां आप एक ऐसे सबूत की तलाश करते हैं। – chi

+1

स्पष्टीकरण के लिए धन्यवाद। मैं कम समय में बहुत उपयोगी जानकारी के लिए वास्तव में खुश हूँ। –

उत्तर

10

यह 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))) 

और वहां आप जाते हैं!

+0

वाह! यह वास्तव में सबसे अच्छा और तेज़ उत्तर है जिसे मैंने कभी देखा है। आपका बहुत बहुत धन्यवाद। मैंने कोक स्थापित किया है और इसे इस्तेमाल करने का प्रयास किया है लेकिन मैं आउटपुट नहीं पढ़ सकता। यह बहुत जटिल है :( –

+0

मैं आपकी सलाह के बाद आगाडा का उपयोग करने की कोशिश करूंगा। यह अजीब बात है कि हम इस तरह के अनुप्रयोगों पर विचार नहीं करते हैं और बिना किसी नियम के भी हाथों से सभी चीजें करते हैं! बहुत धन्यवाद। –

+0

एहम, अगर मैं समझ गया आप सही उत्तर को निम्न तरीके से फिर से लिख सकते हैं: एक्स (लैम्ब्डा वाई -> वाई (\ lambda z -> x (z))) –

संबंधित मुद्दे