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

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

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

रूपरेखा

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

(प्रकार) τ ::= α | τ₁ → वि₂ | टी₁ × वर्ग₂

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

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

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

(वाक्यविन्यास शर्तें) s,t,… ::= 'var' x | 'लाम' (एक्स, टी) | 'ऐप' (एस, टी) | 'जोड़ी' (स, टी) | 'फस्ट' टी | 'एसएंड' टी

यहाँ '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

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

(शब्दार्थ शब्द) S,T,... ::= LAM (λx. S x) | जोड़ी (एस, टी) | एसवाईएन टी

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

 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∥ लिखा गया है_Γ, जहां Γ बाइंडिंग का संदर्भ है, केवल शब्द संरचना पर प्रेरण द्वारा आगे बढ़ता है:

<ब्लॉककोट>${\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

विविधताएं

अवशिष्ट सिंटैक्स में नामों के बजाय de Bruijn index#Alternatives_to_De_Bruijn_indices का उपयोग करना बनाता है reify एक विशुद्ध रूप से कार्यात्मक जिसमें इसकी कोई आवश्यकता नहीं है fresh_var. अवशिष्ट शर्तों का डेटा प्रकार सामान्य रूप में अवशिष्ट शर्तों का डेटा प्रकार भी हो सकता है। के जैसा reify (और इसलिए nbe) तो यह स्पष्ट करता है कि परिणाम सामान्यीकृत है। और यदि सामान्य प्रपत्रों का डेटाटाइप टाइप किया जाता है, तो इसका प्रकार reify (और इसलिए nbe) तो यह स्पष्ट करता है कि सामान्यीकरण टाइप संरक्षित है। मूल्यांकन द्वारा सामान्यीकरण भी सरल रूप से टाइप किए गए लैम्ब्डा कैलकुस को रकम के साथ मापता है (+),सीमांकित निरंतरता का उपयोग करना shift और reset.

यह भी देखें

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