मैक्कार्थी 91 फ़ंक्शन

मैक्कार्थी 91 फ़ंक्शन एक रिकर्सन (कंप्यूटर विज्ञान) है, जिसे कंप्यूटर वैज्ञानिक जॉन मैक्कार्थी (कंप्यूटर वैज्ञानिक) रिकर्सन (कंप्यूटर विज्ञान) के भीतर औपचारिक सत्यापन के लिए एक परीक्षण मामले के रूप में परिभाषित किया है।

मैक्कार्थी 91 फ़ंक्शन को इस प्रकार परिभाषित किया गया है

$M(n)={\begin{cases}n-10,&{\mbox{if }}n>100{\mbox{ }}\\M(M(n+11)),&{\mbox{if }}n\leq 100{\mbox{ }}\end{cases}}$

फ़ंक्शन के मूल्यांकन के परिणाम सभी पूर्णांक तर्क n ≤ 100 के लिए M(n) = 91, और n > 100 के लिए M(n) = n − 10 द्वारा दिए गए हैं। वास्तव में, M(101) का परिणाम भी 91 (101 - 10 = 91) है। n = 101 के बाद M(n) के सभी परिणाम लगातार 1 से बढ़ रहे हैं, उदाहरण के लिए एम(102) = 92, एम(103) = 93।

इतिहास

91 फ़ंक्शन को 1970 में जोहार मन्ना, अमीर पनुएली और जॉन मैक्कार्थी (कंप्यूटर वैज्ञानिक) द्वारा प्रकाशित पत्रों में पेश किया गया था। ये कागजात औपचारिक सत्यापन के लिए औपचारिक तरीकों के आवेदन की दिशा में शुरुआती विकास का प्रतिनिधित्व करते थे। 91 फ़ंक्शन को नेस्टेड-रिकर्सिव (एकल प्रत्यावर्तन के विपरीत, जैसे कि परिभाषित करना) के लिए चुना गया था $f(n)$ के माध्यम से $f(n-1)$). यह उदाहरण मन्ना की पुस्तक, मैथमैटिकल थ्योरी ऑफ कंप्यूटेशन (1974) द्वारा लोकप्रिय हुआ। जैसे-जैसे औपचारिक तरीकों का क्षेत्र आगे बढ़ा, यह उदाहरण शोध साहित्य में बार-बार सामने आया। विशेष रूप से, इसे स्वचालित प्रोग्राम सत्यापन के लिए एक चुनौती समस्या के रूप में देखा जाता है।

पूँछ प्रत्यावर्तन |टेल-रिकर्सिव नियंत्रण प्रवाह के बारे में तर्क करना आसान है, यह एक समतुल्य (विस्तारकता) परिभाषा है:

$M_{t}(n)=M_{t}'(n,1)$

$M_{t}'(n,c)={\begin{cases}n,&{\mbox{if }}c=0\\M_{t}'(n-10,c-1),&{\mbox{if }}n>100{\mbox{ and }}c\neq 0\\M_{t}'(n+11,c+1),&{\mbox{if }}n\leq 100{\mbox{ and }}c\neq 0\end{cases}}$

इस तरह के तर्क को प्रदर्शित करने के लिए उपयोग किए गए उदाहरणों में से एक के रूप में, मन्ना की पुस्तक में नेस्टेड-रिकर्सिव 91 फ़ंक्शन के बराबर एक टेल-रिकर्सिव एल्गोरिदम शामिल है। 91 फ़ंक्शन के स्वचालित सत्यापन (या समाप्ति प्रमाण) की रिपोर्ट करने वाले कई दस्तावेज़ केवल टेल-रिकर्सिव संस्करण को संभालते हैं।

यह एक समतुल्य पारस्परिक पुनरावर्तन पूँछ-पुनरावर्ती परिभाषा है:

$M_{mt}(n)=M_{mt}'(n,0)$

$M_{mt}'(n,c)={\begin{cases}M_{mt}''(n-10,c),&{\mbox{if }}n>100{\mbox{ }}\\M_{mt}'(n+11,c+1),&{\mbox{if }}n\leq 100{\mbox{ }}\end{cases}}$

$M_{mt}''(n,c)={\begin{cases}n,&{\mbox{if }}c=0{\mbox{ }}\\M_{mt}'(n,c-1),&{\mbox{if }}c\neq 0{\mbox{ }}\end{cases}}$

नेस्टेड-रिकर्सिव से पारस्परिक रूप से टेल-रिकर्सिव संस्करण की औपचारिक व्युत्पत्ति 1980 के एक लेख में मिशेल वैंड द्वारा निरंतरता के उपयोग के आधार पर दी गई थी।

उदाहरण

उदाहरण ए:

एम(99) = एम(एम(110)) चूँकि 99 ≤ 100
      = एम(100) चूँकि 110 > 100
      = एम(एम(111)) चूँकि 100 ≤ 100
      = एम(101) 111 > 100 से
      = 91 चूँकि 101 > 100

उदाहरण बी:

एम(87) = एम(एम(98))
      = एम(एम(एम(109)))
      = एम(एम(99))
      = एम(एम(एम(110)))
      = एम(एम(100))
      = एम(एम(एम(111)))
      = एम(एम(101))
      = एम(91)
      = एम(एम(102))
      = एम(92)
      = एम(एम(103))
      = एम(93)
   .... पैटर्न एम(99), एम(100) और एम(101) तक बढ़ता रहता है, बिल्कुल वैसा ही जैसा हमने उदाहरण ए में देखा था)
      = एम(101) 111 > 100 से
      = 91 चूँकि 101 > 100

कोड

यहां लिस्प (प्रोग्रामिंग भाषा) में नेस्टेड-रिकर्सिव एल्गोरिदम का कार्यान्वयन है:

(defun mc91 (n)
  (cond ((<= n 100) (mc91 (mc91 (+ n 11))))
        (t (- n 10))))

हास्केल (प्रोग्रामिंग भाषा) में नेस्टेड-रिकर्सिव एल्गोरिदम का कार्यान्वयन यहां दिया गया है:

mc91 n 
  | n > 100   = n - 10
  | otherwise = mc91 $ mc91 $ n + 11

यहां OCaml (प्रोग्रामिंग भाषा) में नेस्टेड-रिकर्सिव एल्गोरिदम का कार्यान्वयन है:

let rec mc91 n =
  if n > 100 then n - 10
  else mc91 (mc91 (n + 11))

यहां OCaml (प्रोग्रामिंग भाषा) में टेल-रिकर्सिव एल्गोरिदम का कार्यान्वयन है:

let mc91 n =
  let rec aux n c =
    if c = 0 then n
    else if n > 100 then aux (n - 10) (c - 1)
    else aux (n + 11) (c + 1)
  in
  aux n 1

यहां पायथन (प्रोग्रामिंग भाषा) में नेस्टेड-रिकर्सिव एल्गोरिदम का कार्यान्वयन है:

def mc91(n: int) -> int:
    """McCarthy 91 function."""
    if n > 100:
        return n - 10
    else:
        return mc91(mc91(n + 11))

यहां C (प्रोग्रामिंग भाषा) में नेस्टेड-रिकर्सिव एल्गोरिदम का कार्यान्वयन है:

int mc91(int n)
{
    if (n > 100) {
        return n - 10;
    } else {
        return mc91(mc91(n + 11));
    }
}

यहां C (प्रोग्रामिंग भाषा) में टेल-रिकर्सिव एल्गोरिदम का कार्यान्वयन दिया गया है:

int mc91(int n)
{
    return mc91taux(n, 1);
}

int mc91taux(int n, int c)
{
    if (c != 0) {
        if (n > 100) {
            return mc91taux(n - 10, c - 1);
        } else {
            return mc91taux(n + 11, c + 1);
        }
    } else {
        return n;
    }
}

प्रमाण

यहाँ इसका प्रमाण है

$M(n)={\begin{cases}n-10,&{\mbox{if }}n>100{\mbox{ }}\\91,&{\mbox{if }}n\leq 100{\mbox{ }}\end{cases}}$

जो गणना करने के लिए एक समतुल्य गैर-पुनरावर्ती एल्गोरिदम प्रदान करता है $M$.

n > 100 के लिए, समानता की परिभाषा से अनुसरण करती है $M$. n ≤ 100 के लिए, 100 से नीचे की ओर एक मजबूत प्रेरण का उपयोग किया जा सकता है।

90 ≤ एन ≤ 100 के लिए,

एम(एन) = एम(एम(एन + 11)), परिभाषा के अनुसार
     = एम(एन + 11 - 10), चूँकि एन + 11 > 100
     = एम(एन + 1)

तो M(n) = M(101) = 91 90 ≤ n ≤ 100 के लिए। इसे बेस केस के तौर पर इस्तेमाल किया जा सकता है.

प्रेरण चरण के लिए, मान लीजिए n ≤ 89 और सभी n < i ≤ 100 के लिए M(i) = 91 मान लें, तो

एम(एन) = एम(एम(एन + 11)), परिभाषा के अनुसार
     = एम(91), परिकल्पना के अनुसार, चूँकि n < n + 11 ≤ 100
     = 91, आधार स्थिति के अनुसार।

यह नकारात्मक मानों सहित सभी n ≤ 100 के लिए M(n) = 91 साबित करता है।

नुथ का सामान्यीकरण

डोनाल्ड नुथ ने अतिरिक्त मापदंडों को शामिल करने के लिए 91 फ़ंक्शन को सामान्यीकृत किया। जॉन काउल्स (गणितज्ञ) ने ACL2 प्रमेय कहावत का उपयोग करते हुए एक औपचारिक प्रमाण विकसित किया कि नुथ का सामान्यीकृत कार्य कुल था।

संदर्भ

• Manna, Zohar; Pnueli, Amir (July 1970). "Formalization of Properties of Functional Programs". Journal of the ACM. 17 (3): 555–569. doi:10.1145/321592.321606. S2CID 5924829.
• Manna, Zohar; McCarthy, John (1970). "Properties of programs and partial function logic". Machine Intelligence. 5. OCLC 35422131.
• Manna, Zohar (1974). Mathematical Theory of Computation (4th ed.). McGraw-Hill. ISBN 9780070399105.
• Wand, Mitchell (January 1980). "Continuation-Based Program Transformation Strategies". Journal of the ACM. 27 (1): 164–180. doi:10.1145/322169.322183. S2CID 16015891.