लैम्ब्डा कैलकुस में मूल्य से कॉल करें

Question

मैं Types and Programming Languages के माध्यम से अपना रास्ता काम कर रहा हूं, और पिएर्स, मूल्य कमी रणनीति द्वारा कॉल के लिए, id (id (λz. id z)) शब्द का उदाहरण देता है। आंतरिक रेडएक्स पहले को घटा दिया गया है, पहले रेडएक्स को सामान्य रूप λz. id z पर कम करने से पहले, पहली कमी के परिणामस्वरूप id (λz. id z) दे रहा है।

लेकिन मूल्य आदेश द्वारा कॉल को 'केवल बाहरीतम रेडएक्स कम कर दिया गया है' के रूप में परिभाषित किया गया है, और 'एक रेडएक्स केवल तभी कम हो जाता है जब उसके दाएं हाथ को पहले से ही एक मूल्य में कम कर दिया गया हो'। उदाहरण में id (λz. id z) बाहरीतम रेडएक्स के दाईं ओर दिखाई देता है, और कम हो जाता है। इस नियम के साथ कैसे वर्ग किया जाता है कि केवल बाहरी रेडएक्स कम हो जाते हैं?

क्या उत्तर 'बाहरीतम' और 'innermost' केवल lambda abstractions को संदर्भित करता है? तो tλz. t में t को घटाया नहीं जा सकता है, लेकिन एक रेडएक्स s t, t को v पर घटा दिया गया है, और फिर s v कम हो गया है?

Answer 1

संक्षिप्त उत्तर: हाँ। आप लैम्ब्डा-टर्म के अंदर कभी भी कम नहीं कर सकते हैं, आप केवल सही से शुरू होने वाले शब्द को कम कर सकते हैं।

E = [ ] | (λ.t)E | Et 

ई आप क्या कर सकते हैं मूल्य है .. उदाहरण के लिए लैम्ब्डा पथरी में नाम से मूल्यांकन संदर्भ है

:

लैम्ब्डा-पथरी मूल्य द्वारा में मूल्यांकन संदर्भों की सेट के रूप में परिभाषित किया गया है का पालन :

E = [ ] | Et | fE 

क्योंकि आप एक नियम नहीं मानते हैं, भले ही आप एक आवेदन को कम कर सकते हैं। उदाहरण के लिए (λx.x)(z λx.x) मूल्य से कॉल में फंस गया है लेकिन नाम से कॉल में यह (z λx.x) तक कम हो जाता है, जो एक सामान्य रूप है। पियर्स की 19.5.3 अध्याय में

f = λx.t | L 
L = x | L f 

आप संदर्भों की एक और परिभाषा देख सकते हैं:
संदर्भ व्याकरण f में एक सामान्य प्रपत्र (नाम से कॉल में) के रूप में परिभाषित किया गया है।

Answer 2

क्या उत्तर 'बाहरीतम' और 'innermost' केवल लैम्बडा abstractions को संदर्भित करता है? तो λz में एक शब्द टी के लिए। टी, टी को कम नहीं किया जा सकता है, लेकिन एक रेडेक्स एस टी में, टी को एक मूल्य v में घटा दिया जाता है यदि यह संभव है, और फिर एस वी कम हो गया है?

हाँ, यह बिल्कुल सही है।