التطبيع عن طريق التقييم

في دلالات لغات البرمجة ، يُعدّ التطبيع بالتقييم (NBE) طريقةً للحصول على الشكل الطبيعي للمصطلحات في حساب لامدا (λ-calculus) بالاستناد إلى دلالاتها الدلالية . يُفسَّر المصطلح أولًا إلى نموذج دلالي لبنية مصطلح لامدا، ثم يُستخرج ممثلٌ معياري (β-normal و η-long) بتجسيد الدلالة. يختلف هذا النهج الدلالي، الخالي من الاختزال، عن الوصف النحوي التقليدي للتطبيع، القائم على الاختزال، باعتباره اختزالات في نظام إعادة كتابة المصطلحات، حيث يُسمح بالاختزالات β-reductions في أعماق مصطلحات لامدا.

وُصفت نظرية NBE لأول مرة لحساب لامدا ذي النوع البسيط . ^{[ 1 ]} ومنذ ذلك الحين، تم توسيعها لتشمل أنظمة أنواع أضعف ، مثل حساب لامدا غير المُنمذج ^{[ 2 ]} باستخدام منهج نظرية المجال ، وأنظمة أنواع أكثر ثراءً، مثل العديد من متغيرات نظرية مارتن-لوف للأنواع . ^{[ 3 ] [ 4 ] [ 5 ] [ 6 ]}

ضع في اعتبارك حساب لامدا البسيط ، حيث يمكن أن تكون الأنواع τ أنواعًا أساسية (α)، أو أنواع دوال (→)، أو منتجات (×)، معطاة بواسطة قواعد باكوس-ناور التالية (→ ربط إلى اليمين، كالمعتاد):

(أنواع) τ  ::= α | τ ₁ → τ ₂ | τ ₁ × τ ₂

يمكن تطبيق هذه كنوع بيانات في اللغة الوصفية؛ على سبيل المثال، بالنسبة للغة Standard ML ، قد نستخدم:

نوع البيانات ty = أساسي السلسلة | سهم ty * ty | ضرب ty * ty​​

يتم تعريف المصطلحات على مستويين. ^{[ 7 ]} المستوى النحوي الأدنى (يسمى أحيانًا المستوى الديناميكي ) هو التمثيل الذي ينوي المرء توحيده.

(مصطلحات بناء الجملة) s ، t ، ...  ::= var x | lam ( x , t ) | app ( s , t ) | pair ( s , t ) | fst t | snd t

هنا، يمثل lam / app (على التوالي pair / fst ، snd ) صيغتي الإدخال والحذف لـ → (على التوالي ×)، و x متغيرات . من المفترض أن يتم تنفيذ هذه المصطلحات كنوع بيانات من الدرجة الأولى في اللغة الوصفية.

نوع البيانات tm = متغير من نوع سلسلة نصية | lam من نوع سلسلة نصية * tm | app من نوع tm * tm | pair من نوع tm * tm | fst من نوع tm | snd من نوع tm

تُفسر الدلالات الدلالية للمصطلحات (المغلقة) في اللغة الوصفية بنى النحو من حيث خصائص اللغة الوصفية؛ وبالتالي، يُفسر lam على أنه تجريد، وapp على أنه تطبيق، وما إلى ذلك. الكائنات الدلالية التي تم إنشاؤها هي كما يلي:

(المصطلحات الدلالية) S ، T ، ...  ::= LAM (λ x . S x ) | PAIR ( S ، T ) | SYN t

لاحظ أنه لا توجد متغيرات أو صيغ حذف في الدلالات؛ فهي ممثلة ببساطة كبنية نحوية. يتم تمثيل هذه الكائنات الدلالية بنوع البيانات التالي:

نوع البيانات sem = LAM من ( sem -> sem ) | زوج من sem * sem | مرادف من tm

توجد دالتان مُفهرستان حسب النوع، تنتقلان ذهابًا وإيابًا بين الطبقة النحوية والدلالية. الدالة الأولى، والتي تُكتب عادةً ↑ _τ ، تعكس مصطلح "النحو" في الطبقة الدلالية، بينما تُجسد الثانية الدلالة كمصطلح نحوي (تُكتب ↓ ^τ ). تعريفاتهما متداخلة ومتكررة كما يلي:

${\displaystyle {\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 . هذه العملية، المكتوبة ∥ s ∥ _Γ ، حيث Γ هو سياق الارتباطات، تتم بالاستقراء فقط على بنية المصطلح.

${\displaystyle {\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(* المعنى: السياق -> العلامة -> الدلالة *) دالة المعنى G t = حالة t من المتغير x => البحث عن G x | lam ( x , s ) => LAM ( دالة S => المعنى ( إضافة ( G , ( x , S ))) s ) | app ( s , t ) => ( حالة المعنى G s من LAM S => S ( المعنى G t )) | pair ( s , t ) => PAIR ( المعنى G s , المعنى G t ) | fst s => ( حالة المعنى G s من PAIR ( S , T ) => S ) | snd t => ( حالة المعنى G t من PAIR ( S , T ) => T )

لاحظ أن هناك العديد من الحالات غير الشاملة؛ ومع ذلك، عند تطبيقها على مصطلح مغلق ذي نوع صحيح، لا يتم مواجهة أي من هذه الحالات المفقودة. وتكون عملية NBE على المصطلحات المغلقة كما يلي:

(* 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

تكون النتيجة في الواقع على شكل η-long، كما يمكن رؤيته بسهولة من خلال تطبيعها عند نوع هوية مختلف:

- 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. ^{[ 8 ]}

يمكن أن يكون نوع بيانات الحدود المتبقية هو نفسه نوع بيانات الحدود المتبقية في الصيغة الطبيعية . ويُوضح نوع reify(وبالتالي نوع ) أن النتيجة مُعَيَّرة. وإذا كان نوع بيانات الصيغ الطبيعية مُحددًا، فإن نوع (وبالتالي نوع ) يُوضح أن التعيير يحافظ على النوع. ^{[ 9 ]}nbereifynbe

كما أن التطبيع عن طريق التقييم يتوسع إلى حساب لامدا المكتوب ببساطة مع المجاميع ( +)، ^{[ 7 ]} باستخدام عوامل التحكم المحددةshift و reset. ^{[ 10 ]}

• MINLOG ، وهو مساعد إثبات يستخدم NBE كمحرك إعادة كتابة.