कॉल-विद-करंट-कॉन्टीनुअशन: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
Line 9: Line 9:
कंप्यूटर विज्ञान में, इस प्रकार की अंतर्निहित प्रोग्राम स्थिति को वस्तु के रूप में दृश्यमान बनाना [[रीफिकेशन (कंप्यूटर विज्ञान)]] कहा जाता है। (स्कीम (प्रोग्रामिंग लैंग्वेज) निरंतरता या कार्यों को प्रयुक्त करने के मध्य वाक्यात्मक रूप से अंतर नहीं करती है।)
कंप्यूटर विज्ञान में, इस प्रकार की अंतर्निहित प्रोग्राम स्थिति को वस्तु के रूप में दृश्यमान बनाना [[रीफिकेशन (कंप्यूटर विज्ञान)]] कहा जाता है। (स्कीम (प्रोग्रामिंग लैंग्वेज) निरंतरता या कार्यों को प्रयुक्त करने के मध्य वाक्यात्मक रूप से अंतर नहीं करती है।)


कॉल/सीसी के साथ विभिन्न प्रकार के जटिल नियंत्रण ऑपरेटरों को कोड की कुछ पंक्तियों के माध्यम से अन्य लैंग्वेजों से कार्यान्वित किया जा सकता है, उदाहरण के लिए, [[जॉन मैक्कार्थी (कंप्यूटर वैज्ञानिक)]] <code>amb</code> [[गैर-नियतात्मक प्रोग्रामिंग]] के लिए [[ऑपरेटर (कंप्यूटर प्रोग्रामिंग)]], [[प्रोलॉग]]-शैली [[ बैक ट्रैकिंग |बैक ट्रैकिंग]] , [[ शुरुआत |सिमुला]] 67-शैली कोरआउट्स और उसके सामान्यीकरण, आइकन (प्रोग्रामिंग लैंग्वेज) शैली [[जेनरेटर (कंप्यूटर प्रोग्रामिंग)]], या [[इंजन (कंप्यूटर विज्ञान)]] और [[थ्रेड (कंप्यूटिंग)]] एस या यहां तक ​​कि अव्यक्त [[COMEFROM|कमफ्रॉम]] अदि है।
कॉल/सीसी के साथ विभिन्न प्रकार के जटिल नियंत्रण ऑपरेटरों को कोड की कुछ पंक्तियों के माध्यम से अन्य लैंग्वेजों से कार्यान्वित किया जा सकता है, उदाहरण के लिए, [[जॉन मैक्कार्थी (कंप्यूटर वैज्ञानिक)]] <code>amb</code> [[गैर-नियतात्मक प्रोग्रामिंग]] के लिए [[ऑपरेटर (कंप्यूटर प्रोग्रामिंग)]], [[प्रोलॉग]]-स्टाइल [[ बैक ट्रैकिंग |बैक ट्रैकिंग]] , [[ शुरुआत |सिमुला]] 67-स्टाइल कोरआउट्स और उसके सामान्यीकरण, आइकन (प्रोग्रामिंग लैंग्वेज) स्टाइल [[जेनरेटर (कंप्यूटर प्रोग्रामिंग)]], या [[इंजन (कंप्यूटर विज्ञान)]] और [[थ्रेड (कंप्यूटिंग)]] एस या यहां तक ​​कि अव्यक्त [[COMEFROM|कमफ्रॉम]] अदि है।


== उदाहरण ==
== उदाहरण ==
जैसा कि अगले उदाहरण में दिखाया गया है, कॉल/सीसी का उपयोग [[सी (प्रोग्रामिंग भाषा)|सी (प्रोग्रामिंग लैंग्वेज)]]-शैली लैंग्वेजों से ज्ञात [[ वापसी विवरण |रिटर्न स्टेटमेंट]] के फ़ंक्शन का अनुकरण करने के लिए किया जा सकता है, जो स्कीम (प्रोग्रामिंग लैंग्वेज) में लुप्त है:
जैसा कि अगले उदाहरण में दिखाया गया है, कॉल/सीसी का उपयोग [[सी (प्रोग्रामिंग भाषा)|सी]] -स्टाइल लैंग्वेजों [[सी (प्रोग्रामिंग भाषा)|(प्रोग्रामिंग लैंग्वेज)]] से ज्ञात [[ वापसी विवरण |रिटर्न स्टेटमेंट]] के फ़ंक्शन का अनुकरण करने के लिए किया जा सकता है, जो स्कीम (प्रोग्रामिंग लैंग्वेज) में लुप्त है:


<syntaxhighlight lang="scheme">
<syntaxhighlight lang="scheme">
Line 66: Line 66:
(generate-digit) ;; you-fell-off-the-end
(generate-digit) ;; you-fell-off-the-end
</syntaxhighlight>
</syntaxhighlight>
इस प्रकार जब लूप सूची से किसी अन्य आइटम को संसाधित करने वाला होता है, तो फ़ंक्शन वर्तमान निरंतरता को पकड़ लेता है, और इसे वेरिएबल 'कंट्रोल-स्टेट' को असाइन कर देता है। यह वेरिएबल प्रारंभ में [[ समापन (कंप्यूटर प्रोग्रामिंग) |समापन (कंप्यूटर प्रोग्रामिंग)]] है जो सूची के सभी अवयवो के माध्यम से पुनरावृत्त होता है। जैसे-जैसे गणना आगे बढ़ती है, यह समापन बन जाता है जो दी गई सूची के प्रत्यय के माध्यम से पुनरावृत्त होता है। जबकि रैखिक संग्रह के लिए कॉल/सीसी का उपयोग अनावश्यक है, जैसे <code>[LISTOF X]</code>, कोड किसी भी संग्रह को सामान्यीकृत करता है जिसे ट्रैवर्स किया जा सकता है।
इस प्रकार जब लूप सूची से किसी अन्य आइटम को संसाधित करने वाला होता है, तो फ़ंक्शन वर्तमान निरंतरता को पकड़ लेता है, और इसे वेरिएबल 'कंट्रोल-स्टेट' को असाइन कर देता है। यह वेरिएबल प्रारंभ में वह [[ समापन (कंप्यूटर प्रोग्रामिंग) |क्लोजर (कंप्यूटर प्रोग्रामिंग)]] है जो सूची के सभी अवयवो के माध्यम से पुनरावृत्त होता है। जैसे-जैसे गणना आगे बढ़ती है, यह समापन बन जाता है जो दी गई सूची के प्रत्यय के माध्यम से पुनरावृत्त होता है। जबकि रैखिक संग्रह के लिए कॉल/सीसी का उपयोग अनावश्यक है, जैसे <code>[LISTOF X]</code>, कोड किसी भी संग्रह को सामान्यीकृत करता है जिसे ट्रैवर्स किया जा सकता है।


कॉल-विथ-वर्तमान-निरंतरता अन्य परिष्कृत आदिमताओं को भी व्यक्त कर सकती है। उदाहरण के लिए, अगला प्रतिरूप निरंतरता का उपयोग करके सहायक  मल्टीटास्किंग करता है:
कॉल-विथ-वर्तमान-निरंतरता अन्य परिष्कृत आदिमताओं को भी व्यक्त कर सकती है। उदाहरण के लिए, अगला प्रतिरूप निरंतरता का उपयोग करके सहायक  मल्टीटास्किंग करता है:
Line 148: Line 148:
प्रमाण और फंक्शनों के मध्य करी-हावर्ड पत्राचार कॉल/सीसी को पीयर्स के नियम से जोड़ता है, जो [[अंतर्ज्ञानवादी तर्क]] को गैर-रचनात्मक, [[शास्त्रीय तर्क|मौलिक तर्क]] ((α → β) → α) → α तक विस्तारित करता है। यहां, ((α → β) → α) फ़ंक्शन f का प्रकार है, जो या तो सीधे α प्रकार का मान लौटा सकता है या प्रकार (α → β) की निरंतरता के लिए तर्क प्रयुक्त कर सकता है। चूंकि निरंतरता प्रयुक्त होने पर उपस्थित संदर्भ हटा दिया जाता है, इसलिए प्रकार β का उपयोग कभी नहीं किया जाता है और इसे ⊥, खाली प्रकार के रूप में लिया जा सकता है।
प्रमाण और फंक्शनों के मध्य करी-हावर्ड पत्राचार कॉल/सीसी को पीयर्स के नियम से जोड़ता है, जो [[अंतर्ज्ञानवादी तर्क]] को गैर-रचनात्मक, [[शास्त्रीय तर्क|मौलिक तर्क]] ((α → β) → α) → α तक विस्तारित करता है। यहां, ((α → β) → α) फ़ंक्शन f का प्रकार है, जो या तो सीधे α प्रकार का मान लौटा सकता है या प्रकार (α → β) की निरंतरता के लिए तर्क प्रयुक्त कर सकता है। चूंकि निरंतरता प्रयुक्त होने पर उपस्थित संदर्भ हटा दिया जाता है, इसलिए प्रकार β का उपयोग कभी नहीं किया जाता है और इसे ⊥, खाली प्रकार के रूप में लिया जा सकता है।


दोहरे निषेध उन्मूलन का सिद्धांत ((α → ⊥) → ⊥) → α कॉल-सीसी के एक प्रकार के बराबर है जो अपेक्षा करता है कि इसके तर्क f सदैव सामान्य रूप से मूल्य वापस किए बिना वर्तमान निरंतरता का मूल्यांकन करता है। मौलिक तर्क को अंतर्ज्ञानवादी तर्क में एम्बेड करना निरंतरता से निकलने वाली शैली के अनुवाद से संबंधित है।<ref name=ch-isomorphy>{{cite book|last1=Sørensen|first1=Morten Heine|last2=Urzyczyn|first2=Paweł|title=करी-हावर्ड समरूपता पर व्याख्यान|date=2007|publisher=Elsevier|location=Boston, MA|isbn=978-0444520777|edition=1st|chapter=Classical Logic and Control Operators}}</ref>
दोहरे निषेध उन्मूलन का सिद्धांत ((α → ⊥) → ⊥) → α कॉल-सीसी के एक प्रकार के बराबर है जो अपेक्षा करता है कि इसके तर्क f सदैव सामान्य रूप से मूल्य वापस किए बिना वर्तमान निरंतरता का मूल्यांकन करता है। मौलिक तर्क को अंतर्ज्ञानवादी तर्क में एम्बेड करना निरंतरता से निकलने वाली स्टाइल के अनुवाद से संबंधित है।<ref name=ch-isomorphy>{{cite book|last1=Sørensen|first1=Morten Heine|last2=Urzyczyn|first2=Paweł|title=करी-हावर्ड समरूपता पर व्याख्यान|date=2007|publisher=Elsevier|location=Boston, MA|isbn=978-0444520777|edition=1st|chapter=Classical Logic and Control Operators}}</ref>
== कॉल/सीसी प्रयुक्त करने वाली लैंग्वेजएँ ==
== कॉल/सीसी प्रयुक्त करने वाली लैंग्वेजएँ ==
* स्कीम (प्रोग्रामिंग लैंग्वेज)
* स्कीम (प्रोग्रामिंग लैंग्वेज)
Line 159: Line 159:
* [[आर प्रोग्रामिंग]]<ref>{{Cite web|url=https://stat.ethz.ch/R-manual/R-devel/library/base/html/callCC.html|title = R: Call with Current Continuation}}</ref>
* [[आर प्रोग्रामिंग]]<ref>{{Cite web|url=https://stat.ethz.ch/R-manual/R-devel/library/base/html/callCC.html|title = R: Call with Current Continuation}}</ref>
==यह भी देखें==
==यह भी देखें==
* [[जाओ|गोटू]]
* [[जाओ|गो-टू]]
* [[निरंतरता-गुजरने वाली शैली|निरंतरता-निकलने वाली शैली]]
* [[निरंतरता-गुजरने वाली शैली|कंटिन्यूएशन-पासिंग स्टाइल]]
* [[फाइबर (कंप्यूटर विज्ञान)]]
* [[फाइबर (कंप्यूटर विज्ञान)]]



Revision as of 12:28, 8 December 2023

स्कीम (प्रोग्रामिंग लैंग्वेज) कंप्यूटर प्रोग्रामिंग लैंग्वेज में, प्रक्रिया (कंप्यूटर विज्ञान) कॉल-विद-वर्तमान-निरंतरता, संक्षिप्त कॉल/सीसी, का उपयोग नियंत्रण प्रवाह ऑपरेटर के रूप में किया जाता है। इसे कई अन्य प्रोग्रामिंग लैंग्वेजों द्वारा अपनाया गया है।

किसी फंक्शन f को उसके एकमात्र तर्क के रूप में, अभिव्यक्ति के अंदर (call/cc f) को अभिव्यक्ति की वर्तमान निरंतरता पर प्रयुक्त होता है। उदाहरण के लिए ((call/cc f) e2) अभिव्यक्ति की वर्तमान निरंतरता में f लगाने के बराबर है। वर्तमान निरंतरता (call/cc f) को लैम्ब्डा एब्स्ट्रैक्शन द्वारा बंधे एक वेरिएबल c द्वारा प्रतिस्थापित करके दी गई है, इसलिए वर्तमान निरंतरता (lambda (c) (c e2)) है। फ़ंक्शन f को इसमें प्रयुक्त करने से अंतिम परिणाम (f (lambda (c) (c e2))) मिलता है।

एक पूरक उदाहरण के रूप में, अभिव्यक्ति में (e1 (call/cc f)), उप-अभिव्यक्ति (call/cc f) के लिए निरंतरता है (lambda (c) (e1 c)) निरंतरता है, इसीलिए पूरी अभिव्यक्ति (f (lambda (c) (e1 c))) के बराबर है दूसरे शब्दों में यह ऑब्जेक्ट के रूप में प्रोग्राम के वर्तमान नियंत्रण संदर्भ या नियंत्रण स्थिति का स्नैपशॉट लेता है और उस पर f प्रयुक्त होता है। निरंतरता वस्तु प्रथम श्रेणी मान है और इसे फ़ंक्शन के रूप में दर्शाया जाता है, फ़ंक्शन अनुप्रयोग इसका एकमात्र ऑपरेशन है। जब निरंतरता वस्तु को तर्क पर प्रयुक्त किया जाता है, तो उपस्थित निरंतरता समाप्त हो जाती है और प्रयुक्त निरंतरता को उसके स्थान पर पुनः प्रारंभ कर दिया जाता है, जिससे फंक्शन का प्रवाह उस बिंदु पर जारी रहे जहां निरंतरता को कैप्चर किया गया था और निरंतरता का तर्क कॉल/सीसी आह्वान का वापसी मूल्य बन जाता है। कॉल/सीसी के साथ बनाई गई निरंतरताओं को एक से अधिक बार कॉल और यहां तक ​​कि कॉल/सीसी एप्लिकेशन की गतिशील सीमा के बाहर से भी किया जा सकता है।

कंप्यूटर विज्ञान में, इस प्रकार की अंतर्निहित प्रोग्राम स्थिति को वस्तु के रूप में दृश्यमान बनाना रीफिकेशन (कंप्यूटर विज्ञान) कहा जाता है। (स्कीम (प्रोग्रामिंग लैंग्वेज) निरंतरता या कार्यों को प्रयुक्त करने के मध्य वाक्यात्मक रूप से अंतर नहीं करती है।)

कॉल/सीसी के साथ विभिन्न प्रकार के जटिल नियंत्रण ऑपरेटरों को कोड की कुछ पंक्तियों के माध्यम से अन्य लैंग्वेजों से कार्यान्वित किया जा सकता है, उदाहरण के लिए, जॉन मैक्कार्थी (कंप्यूटर वैज्ञानिक) amb गैर-नियतात्मक प्रोग्रामिंग के लिए ऑपरेटर (कंप्यूटर प्रोग्रामिंग), प्रोलॉग-स्टाइल बैक ट्रैकिंग , सिमुला 67-स्टाइल कोरआउट्स और उसके सामान्यीकरण, आइकन (प्रोग्रामिंग लैंग्वेज) स्टाइल जेनरेटर (कंप्यूटर प्रोग्रामिंग), या इंजन (कंप्यूटर विज्ञान) और थ्रेड (कंप्यूटिंग) एस या यहां तक ​​कि अव्यक्त कमफ्रॉम अदि है।

उदाहरण

जैसा कि अगले उदाहरण में दिखाया गया है, कॉल/सीसी का उपयोग सी -स्टाइल लैंग्वेजों (प्रोग्रामिंग लैंग्वेज) से ज्ञात रिटर्न स्टेटमेंट के फ़ंक्शन का अनुकरण करने के लिए किया जा सकता है, जो स्कीम (प्रोग्रामिंग लैंग्वेज) में लुप्त है:

(define (f return)                                                                                                                               
  (return 2)                                                                                                                                     
  3)

(f (lambda (x) x))
=> 3

(call-with-current-continuation f)
=> 2

नियमित फ़ंक्शन तर्क के साथ f को कॉल करने पर पहले इस फ़ंक्शन को मान 2 पर प्रयुक्त करता है, फिर 3 लौटाता है। चूँकि, जब f को कॉल/सीसी (उदाहरण की अंतिम पंक्ति में) में पास किया जाता है, तो पैरामीटर (निरंतरता) को 2 पर प्रयुक्त किया जाता है। प्रोग्राम के निष्पादन को उस बिंदु पर जाने के लिए विवश करता है जहां कॉल/सीसी को कॉल किया गया था, और कॉल/सीसी को मान 2 वापस करने का कारण बनता है। इसे फिर डिस्प्ले फ़ंक्शन द्वारा मुद्रित किया जाता है।

अगले उदाहरण में, कॉल/सीसी का उपयोग दो बार किया जाता है: एक बार पहले उदाहरण की तरह रिटर्न निरंतरता उत्पन्न करने के लिए और एक बार वस्तुओं की सूची के माध्यम से पुनरावृत्ति को निलंबित करने के लिए:

;; [LISTOF X] -> ( -> X u 'you-fell-off-the-end)
(define (generate-one-element-at-a-time lst)
  ;; Both internal functions are closures over lst

  ;; Internal variable/Function which passes the current element in a list
  ;; to its return argument (which is a continuation), or passes an end-of-list marker 
  ;; if no more elements are left. On each step the function name is 
  ;; rebound to a continuation which points back into the function body,
  ;; while return is rebound to whatever continuation the caller specifies.
  (define (control-state return)
    (for-each 
     (lambda (element)
               (set! return (call-with-current-continuation
                              (lambda (resume-here)
                                ;; Grab the current continuation
                               (set! control-state resume-here)
                               (return element))))) ;; (return element) evaluates to next return
     lst)
    (return 'you-fell-off-the-end))
  
  ;; (-> X u 'you-fell-off-the-end)
  ;; This is the actual generator, producing one item from a-list at a time.
  (define (generator)
    (call-with-current-continuation control-state))

  ;; Return the generator 
  generator)

(define generate-digit
  (generate-one-element-at-a-time '(0 1 2)))

(generate-digit) ;; 0
(generate-digit) ;; 1
(generate-digit) ;; 2
(generate-digit) ;; you-fell-off-the-end

इस प्रकार जब लूप सूची से किसी अन्य आइटम को संसाधित करने वाला होता है, तो फ़ंक्शन वर्तमान निरंतरता को पकड़ लेता है, और इसे वेरिएबल 'कंट्रोल-स्टेट' को असाइन कर देता है। यह वेरिएबल प्रारंभ में वह क्लोजर (कंप्यूटर प्रोग्रामिंग) है जो सूची के सभी अवयवो के माध्यम से पुनरावृत्त होता है। जैसे-जैसे गणना आगे बढ़ती है, यह समापन बन जाता है जो दी गई सूची के प्रत्यय के माध्यम से पुनरावृत्त होता है। जबकि रैखिक संग्रह के लिए कॉल/सीसी का उपयोग अनावश्यक है, जैसे [LISTOF X], कोड किसी भी संग्रह को सामान्यीकृत करता है जिसे ट्रैवर्स किया जा सकता है।

कॉल-विथ-वर्तमान-निरंतरता अन्य परिष्कृत आदिमताओं को भी व्यक्त कर सकती है। उदाहरण के लिए, अगला प्रतिरूप निरंतरता का उपयोग करके सहायक मल्टीटास्किंग करता है:

;; Cooperative multitasking using call-with-current-continuation
;; in 25 lines of scheme

;; The list of threads waiting to run. This is a list of one
;; argument non-returning functions (continuations, mostly)
;; A continuation is a non-returning function, just like (exit),
;; in that it never gives up control to whatever called it.

(define ready-list '())

;; A non-returning function. If there is any other thread
;; waiting to be run, it causes the next thread to run if there
;; is any left to run, otherwise it calls the original exit
;; which exits the whole environment.
(define exit
  ;; The original exit which we override.
  (let ((exit exit))
    ;; The overriding function.
    (lambda ()
      (if (not (null? ready-list))
	  ;; There is another thread waiting to be run.
	  ;; So we run it.
          (let ((cont (car ready-list)))
            (set! ready-list (cdr ready-list))
	    ;; Since the ready-list is only non-returning
	    ;; functions, this will not return.
            (cont #f))
	  ;; Nothing left to run.
	  ;; The original (exit) is a non returning function,
	  ;; so this is a non-returning function.
          (exit)))))

;; Takes a one argument function with a given
;; argument and forks it off. The forked function's new
;; thread will exit if/when the function ever exits.
(define (fork fn arg)
  (set! ready-list
        (append ready-list
		;; This function added to the 
		;; ready-list is non-returning,
		;; since exit is non returning.
		(list
		 (lambda (x)
		   (fn arg)
		   (exit))))))

;; Gives up control for the next thread waiting to be run.
;; Although it will eventually return, it gives up control
;; and will only regain it when the continuation is called.
(define (yield)
  (call-with-current-continuation
   ;; Capture the continuation representing THIS call to yield
   (lambda (cont)
     ;; Stick it on the ready list
     (set! ready-list
           (append ready-list
                   (list cont)))
     ;; Get the next thread, and start it running.
     (let ((cont (car ready-list)))
       (set! ready-list (cdr ready-list))
       ;; Run it.
       (cont #f)))))

1999 में, डेविड मैडोर (अनलैम्ब्डा प्रोग्रामिंग लैंग्वेज के आविष्कारक) ने गलती से कॉल/सीसी का उपयोग करते हुए 12-वर्ण वाले अनलैम्ब्डा शब्द की खोज की, जो सभी प्राकृतिक संख्याओं को क्रमिक रूप से एकात्मक प्रतिनिधित्व ``r`ci`.*`ci में मुद्रित करता था।[1] इस फंक्शन और इसके प्रभाव से जुड़े स्पष्ट रहस्यमय ने कुछ लोगों का ध्यान आकर्षित किया है, और इसे सामान्यतः यिन-यांग पहेली के रूप में जाना जाता है।[2] मैडोर द्वारा प्रदान किया गया स्कीम अनुवाद इस प्रकार है:

(let* ((yin
         ((lambda (cc) (display #\@) cc) (call-with-current-continuation (lambda (c) c))))
       (yang
         ((lambda (cc) (display #\*) cc) (call-with-current-continuation (lambda (c) c)))))
    (yin yang))

आलोचना

ओलेग किसलीव, ओकैमल के लिए सीमांकित निरंतरता कार्यान्वयन के लेखक और नियंत्रण ऑपरेटरों को प्रयुक्त करने के लिए सीमांकित स्टैक परिचालन के लिए अप्लिकेशन प्रोग्रामिंग इंटरफ़ेस (एपीआई) के डिजाइनर ओलेग किसलीव, पूर्ण-स्टैक निरंतरता के अतिरिक्त सीमांकित निरंतरता के उपयोग की अधिवक्ता करते हैं जो कॉल/सीसी में परिचालन करता है: कॉल/सीसी को मुख्य नियंत्रण सुविधा के रूप में प्रस्तुत करता है, जिसके संदर्भ में अन्य सभी नियंत्रण सुविधाएं प्रयुक्त की जानी चाहिए, इस प्रकार बुरा विचार सिद्ध होता है। प्रदर्शन, मेमोरी और संसाधन लीक, कार्यान्वयन में आसानी, उपयोग में आसानी, तर्क करने में आसानी सभी कॉल/सीसी के विरुद्ध तर्क देते हैं।[3]

गैर-रचनात्मक तर्क से संबंध

प्रमाण और फंक्शनों के मध्य करी-हावर्ड पत्राचार कॉल/सीसी को पीयर्स के नियम से जोड़ता है, जो अंतर्ज्ञानवादी तर्क को गैर-रचनात्मक, मौलिक तर्क ((α → β) → α) → α तक विस्तारित करता है। यहां, ((α → β) → α) फ़ंक्शन f का प्रकार है, जो या तो सीधे α प्रकार का मान लौटा सकता है या प्रकार (α → β) की निरंतरता के लिए तर्क प्रयुक्त कर सकता है। चूंकि निरंतरता प्रयुक्त होने पर उपस्थित संदर्भ हटा दिया जाता है, इसलिए प्रकार β का उपयोग कभी नहीं किया जाता है और इसे ⊥, खाली प्रकार के रूप में लिया जा सकता है।

दोहरे निषेध उन्मूलन का सिद्धांत ((α → ⊥) → ⊥) → α कॉल-सीसी के एक प्रकार के बराबर है जो अपेक्षा करता है कि इसके तर्क f सदैव सामान्य रूप से मूल्य वापस किए बिना वर्तमान निरंतरता का मूल्यांकन करता है। मौलिक तर्क को अंतर्ज्ञानवादी तर्क में एम्बेड करना निरंतरता से निकलने वाली स्टाइल के अनुवाद से संबंधित है।[4]

कॉल/सीसी प्रयुक्त करने वाली लैंग्वेजएँ

यह भी देखें

संदर्भ

  1. David Madore, "call/cc mind-boggler"
  2. Yin Wang, "Understanding the Yin-Yang Puzzle"
  3. "An argument against call/cc".
  4. Sørensen, Morten Heine; Urzyczyn, Paweł (2007). "Classical Logic and Control Operators". करी-हावर्ड समरूपता पर व्याख्यान (1st ed.). Boston, MA: Elsevier. ISBN 978-0444520777.
  5. "CONT हस्ताक्षर". Standard ML of New Jersey. Bell Labs, Lucent Technologies. 1997-10-28. Retrieved 2019-05-15.
  6. "Class: Continuation". Ruby-doc.org. Neurogami, James Britt. Retrieved 2019-05-15.
  7. Kowalke, Oliver (2014). "Context switching with call/cc". Boost.org. Retrieved 2019-05-15.
  8. "R: Call with Current Continuation".

बाहरी संबंध