मूल्यांकन द्वारा सामान्यीकरण

प्रोग्रामिंग भाषा में प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ मूल्यांकन द्वारा सामान्यीकरण (एनबीई) लैम्ब्डा कैलकुलस में शब्दों के बीटा सामान्य रूप को प्राप्त करने की एक शैली है। एक शब्द को पहले λ-अवधि संरचना के एक सांकेतिक मॉडल में व्याख्या किया जाता है और फिर एक विहित (β-सामान्य और η-लॉन्ग) प्रतिनिधि को पुनर्स्थापना द्वारा निरूपित किया जाता है। इस तरह के एक अनिवार्य रूप से सिमेंटिक पराभव-मुक्त दृष्टिकोण अधिक पारंपरिक सिंटैक्टिक कमी-आधारित सामान्यीकरण के वर्णन से भिन्न होता है जो एक शब्द पुनर्लेखन प्रणाली में कमी के रूप में होता है जहां λ-नियमो के अंदर β-कटौती की अनुमति होती है।

एनबीई को पहली बार केवल टाइप किए गए लैम्ब्डा कैलकुस के लिए वर्णित किया गया था। इसके बाद से इसे अशक्त प्रकार की प्रणालियों जैसे कि अनटाइप्ड लैम्ब्डा कैलकुलस दोनों में विस्तारित किया गया है एक डोमेन सिद्धांत दृष्टिकोण का उपयोग करना और मार्टिन-लोफ प्रकार सिद्धांत के कई रूपों जैसे समृद्ध प्रकार की प्रणालियों के लिए है ।

रूपरेखा

बस टाइप किए गए लैम्ब्डा कैलकुस पर विचार करें जहां प्रकार τ मूल प्रकार (α), कार्य प्रकार (→), या उत्पाद (×) हो सकते हैं जो निम्न बैकस-नौर फॉर्म व्याकरण द्वारा दिए गए हैं (→ सदैव की तरह दाईं ओर संबद्ध):

(Types) τ ::= α | τ₁ → τ₂ | τ₁ × τ₂

इन्हें मेटा-लैंग्वेज में डेटा प्रकार के रूप में प्रयुक्त किया जा सकता है; उदाहरण के लिए मानक एमएल के लिए हम इसका उपयोग कर सकते हैं:

 datatype ty = Basic of string
             | Arrow of ty * ty
             | Prod of ty * ty

नियमो को दो स्तरों पर परिभाषित किया गया है। निचला सिंटैक्टिक स्तर (कभी-कभी गतिशील स्तर कहा जाता है) वह प्रतिनिधित्व है जिसे सामान्य बनाना चाहता है।

(Syntax Terms) s,t,… ::= var x | lam (x, t) | app (s, t) | pair (s, t) | fst t | snd t

यहाँ 'l lam/app (resp. pair/fst,snd) → (resp. ×) के लिए परिचय उन्मूलन नियम रूप हैं और x चर (प्रोग्रामिंग) हैं। इन नियमो को मेटा-भाषा में प्रथम-क्रम तर्क | प्रथम-क्रम डेटा प्रकार के रूप में प्रयुक्त करने का उद्देश्य है:

 datatype tm = var of string
             | lam of string * tm | app of tm * tm
             | pair of tm * tm | fst of tm | snd of tm

मेटा-लैंग्वेज में (क्लोज्ड) नियम का डेनोटेशनल सिमेंटिक्स मेटा-लैंग्वेज की विशेषताओं के संदर्भ में सिंटैक्स के निर्माण की व्याख्या करता है; इस प्रकार लैम की व्याख्या अमूर्त के रूप में की जाती है ऐप को एप्लिकेशन आदि के रूप में निर्मित शब्दार्थ वस्तुएँ इस प्रकार हैं:

(Semantic Terms) S,T,… ::= LAM (λx. S x) | PAIR (S, T) | SYN t

ध्यान दें कि शब्दार्थ में कोई चर या उन्मूलन रूप नहीं हैं उन्हें सिंटैक्स के रूप में दर्शाया जाता है। इन सिमेंटिक वस्तु को निम्न डेटाटाइप द्वारा दर्शाया गया है:

 datatype sem = LAM of (sem -> sem)
              | PAIR of sem * sem
              | SYN of tm

टाइप-इंडेक्स्ड फलन की एक जोड़ी है जो सिंटैक्टिक और सिमेंटिक लेयर के बीच आगे और पीछे चलती है। पहला कार्य सामान्यतः ↑_τ लिखा जाता है सिंटैक्स शब्द को शब्दार्थ में दर्शाता है जबकि दूसरा शब्दार्थ को वाक्य-विन्यास के रूप में दर्शाता है (↓^τ के रूप में लिखा गया है) उनकी परिभाषाएँ पारस्परिक रूप से पुनरावर्ती हैं:

${\begin{aligned}\uparrow _{\alpha }t&=\mathbf {SYN} \ t\\\uparrow _{\tau _{1}\to \tau _{2}}v&=\mathbf {LAM} (\lambda S.\ \uparrow _{\tau _{2}}(\mathbf {app} \ (v,\downarrow ^{\tau _{1}}S)))\\\uparrow _{\tau _{1}\times \tau _{2}}v&=\mathbf {PAIR} (\uparrow _{\tau _{1}}(\mathbf {fst} \ v),\uparrow _{\tau _{2}}(\mathbf {snd} \ v))\\[1ex]\downarrow ^{\alpha }(\mathbf {SYN} \ t)&=t\\\downarrow ^{\tau _{1}\to \tau _{2}}(\mathbf {LAM} \ S)&=\mathbf {lam} \ (x,\downarrow ^{\tau _{2}}(S\ (\uparrow _{\tau _{1}}(\mathbf {var} \ x)))){\text{ where }}x{\text{ is fresh}}\\\downarrow ^{\tau _{1}\times \tau _{2}}(\mathbf {PAIR} \ (S,T))&=\mathbf {pair} \ (\downarrow ^{\tau _{1}}S,\downarrow ^{\tau _{2}}T)\end{aligned}}$

इन परिभाषाओं को मेटा-भाषा में आसानी से कार्यान्वित किया जाता है:

 (* fresh_var : unit -> string *)
 val variable_ctr = ref ~1
 fun fresh_var () = 
      (variable_ctr := 1 + !variable_ctr; 
       "v" ^ Int.toString (!variable_ctr))

 (* reflect : ty -> tm -> sem *)
 fun reflect (Arrow (a, b)) t =
       LAM (fn S => reflect b (app (t, (reify a S))))
   | reflect (Prod (a, b)) t =
       PAIR (reflect a (fst t), reflect b (snd t))
   | reflect (Basic _) t =
       SYN t

 (* reify   : ty -> sem -> tm *)
 and reify (Arrow (a, b)) (LAM S) =
       let val x = fresh_var () in
         lam (x, reify b (S (reflect a (var x))))
       end
   | reify (Prod (a, b)) (PAIR (S, T)) =
       pair (reify a S, reify b T)
   | reify (Basic _) (SYN t) = t

प्रकार की संरचना पर गणितीय प्रेरण द्वारा यह इस प्रकार है कि यदि सिमेंटिक वस्तु S टाइप τ के एक अच्छी तरह से टाइप किए गए शब्द को दर्शाता है तो वस्तु को संशोधित करना (अर्थात ↓^τ S) s का β-सामान्य η-लंबा रूप उत्पन्न करता है। इसलिए जो कुछ बचा है वह प्रारंभिक शब्दार्थ व्याख्या S को एक वाक्यात्मक शब्द s से बनाना है। यह ऑपरेशन ∥s∥_Γ लिखा गया है जहां Γ बाइंडिंग का संदर्भ है केवल शब्द संरचना पर प्रेरण द्वारा आगे बढ़ता है:

${\begin{aligned}\|\mathbf {var} \ x\|_{\Gamma }&=\Gamma (x)\\\|\mathbf {lam} \ (x,s)\|_{\Gamma }&=\mathbf {LAM} \ (\lambda S.\ \|s\|_{\Gamma ,x\mapsto S})\\\|\mathbf {app} \ (s,t)\|_{\Gamma }&=S\ (\|t\|_{\Gamma }){\text{ where }}\|s\|_{\Gamma }=\mathbf {LAM} \ S\\\|\mathbf {pair} \ (s,t)\|_{\Gamma }&=\mathbf {PAIR} \ (\|s\|_{\Gamma },\|t\|_{\Gamma })\\\|\mathbf {fst} \ s\|_{\Gamma }&=S{\text{ where }}\|s\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\\\|\mathbf {snd} \ t\|_{\Gamma }&=T{\text{ where }}\|t\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\end{aligned}}$

कार्यान्वयन में:

 datatype ctx = empty 
              | add of ctx * (string * sem)

 (* lookup : ctx -> string -> sem *)
 fun lookup (add (remdr, (y, value))) x = 
       if x = y then value else lookup remdr x

 (* meaning : ctx -> tm -> sem *)
 fun meaning G t =
       case t of
         var x => lookup G x
       | lam (x, s) => LAM (fn S => meaning (add (G, (x, S))) s)
       | app (s, t) => (case meaning G s of
                          LAM S => S (meaning G t))
       | pair (s, t) => PAIR (meaning G s, meaning G t)
       | fst s => (case meaning G s of
                     PAIR (S, T) => S)
       | snd t => (case meaning G t of
                     PAIR (S, T) => T)

ध्यान दें कि कई गैर-संपूर्ण स्थिति हैं; चूँकि यदि एक बंद अच्छी तरह से टाइप किए गए शब्द पर प्रयुक्त किया जाता है तो इनमें से कोई भी अनुपस्थित स्थिति कभी सामने नहीं आता है। बंद नियमो पर एनबीई ऑपरेशन तब होता है:

 (* nbe : ty -> tm -> tm *)
 fun nbe a t = reify a (meaning empty t)

इसके उपयोग के उदाहरण के रूप में वाक्य-विन्यास शब्द SKK पर विचार करें नीचे परिभाषित:

 val K = lam ("x", lam ("y", var "x"))
 val S = lam ("x", lam ("y", lam ("z", app (app (var "x", var "z"), app (var "y", var "z")))))
 val SKK = app (app (S, K), K)

यह संयोजन तर्क में पहचान कार्य का प्रसिद्ध एन्कोडिंग है। पहचान प्रकार पर इसे सामान्यीकृत करने से यह उत्पन्न होता है:

 - nbe (Arrow (Basic "a", Basic "a")) SKK;
 val it = lam ("v0",var "v0") : tm

परिणाम वास्तव में η-लंबे रूप में है जैसा कि इसे एक अलग पहचान प्रकार पर सामान्यीकृत करके आसानी से देखा जा सकता है:

 - nbe (Arrow (Arrow (Basic "a", Basic "b"), Arrow (Basic "a", Basic "b"))) SKK;
 val it = lam ("v1",lam ("v2",app (var "v1",var "v2"))) : tm

विविधताएं

अवशिष्ट सिंटैक्स में नामों के अतिरिक्त डी ब्रुजन स्तरों का उपयोग करनाreify एक विशुद्ध रूप से कार्यात्मक बनाता है जिसमें fresh_varकी कोई आवश्यकता नहीं है।

अवशिष्ट शर्तों का डेटा प्रकार सामान्य रूप में अवशिष्ट शर्तों का डेटा प्रकार भी हो सकता है। reifyका प्रकार (और इसलिए nbeका) तब यह स्पष्ट करता है कि परिणाम सामान्यीकृत है। और यदि सामान्य रूपों का डेटाटाइप टाइप किया जाता है, तो reifyका प्रकार (और इसलिए nbeका) यह स्पष्ट करता है कि सामान्यीकरण टाइप संरक्षित है।

मूल्यांकन द्वारा सामान्यीकरण भी सीमांकित निरंतरता ऑपरेटरों shift और reset का उपयोग करके रकम (+) के साथ सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस को मापता है।

यह भी देखें

• मिनलॉग, एक प्रमाण सहायक जो एनबीई को अपने पुनर्लेखन इंजन के रूप में उपयोग करता है।