توليف البرامج

في عام ٢٠١٣، اقترح باحثون من جامعة بنسلفانيا ، وجامعة كاليفورنيا في بيركلي ، ومعهد ماساتشوستس للتكنولوجيا إطار عمل موحدًا لمشاكل توليف البرامج يُسمى التوليف الموجه بالبنية (SyGuS). ^{[ ٦ ]} تتكون مدخلات خوارزمية SyGuS من مواصفات منطقية بالإضافة إلى قواعد نحوية خالية من السياق للتعبيرات التي تقيد بنية الحلول الصحيحة. ^{[ ٧ ]} على سبيل المثال، لتوليف دالة f تُرجع أكبر عدد صحيح من عددين، قد تبدو المواصفات المنطقية كما يلي:

( f ( x , y ) = x ∨ f ( x , y ) = y ) ∧ f ( x , y ) ≥ x ∧ f ( x , y ) ≥ y

وقد تكون القواعد النحوية كالتالي:

<Exp> :: = x | y | 0 | 1 | <Exp> + <Exp> | ite ( <Cond> , <Exp> , <Exp> ) <Cond> :: = <Exp> < = <Exp>​​​​​​

حيث يرمز "ite" إلى "if-then-else". التعبير

ite(x <= y, y, x)

سيكون حلاً صحيحاً، لأنه يتوافق مع القواعد والمواصفات.

من عام ٢٠١٤ إلى عام ٢٠١٩، قارنت مسابقة توليف البرامج الموجهة بالبنية النحوية (SyGuS-Comp) السنوية بين الخوارزميات المختلفة لتوليف البرامج في حدث تنافسي. ^{[ ٨ ]} استخدمت المسابقة تنسيق إدخال موحدًا، SyGuS-IF، قائمًا على مكتبة SMT-Lib ٢. على سبيل المثال، يشفر تنسيق SyGuS-IF التالي مشكلة توليف أكبر عدد صحيح من عددين (كما هو موضح أعلاه):

(مجموعة منطق LIA) (دالة اصطناعية f ((x عدد صحيح) (y عدد صحيح)) عدد صحيح ((i عدد صحيح) (c عدد صحيح) (b منطقي)) ((i Int (cxy (+ ii) (ite bii))) (c Int (0 1)) (b Bool ((<= ii))))) (declare-var x Int) (declare-var y Int) (constraint (>= (fxy) x)) (constraint (>= (fxy) y)) (قيد (أو (= (fxy) x) (= (fxy) y))) (check-synth)

قد يُعيد برنامج حل متوافق المخرجات التالية:

((define-fun f ((x Int) (y Int)) Int (ite (<= xy) yx)))

يُعدّ التوليف الاستقرائي الموجّه بالأمثلة المضادة (CEGIS) منهجًا فعالًا لبناء مُركِّبات برامج صوتية. ^{[ 9 ] [ 10 ]} يتضمن CEGIS تفاعل مُكوِّنَين: مُولِّد يُنشئ برامج مُرشَّحة، ومُدقِّق يتحقق مما إذا كانت هذه البرامج تُلبّي المواصفات.

بفرض وجود مجموعة من المدخلات I ، ومجموعة من البرامج الممكنة P ، ومواصفات S ، فإن هدف توليف البرامج هو إيجاد برنامج p في P بحيث يتحقق الشرط S ( p , i ) لجميع المدخلات i في I. يتم تحديد معلمات CEGIS بناءً على مولد ومُدقِّق.

• يأخذ المولد مجموعة من المدخلات T ، ويخرج برنامجًا مرشحًا c يكون صحيحًا على جميع المدخلات في T ، أي مرشح بحيث يكون S ( c , t ) صحيحًا لجميع المدخلات t في T.
• يأخذ المدقق برنامجًا مرشحًا c ويعيد القيمة true إذا كان البرنامج يفي بـ S على جميع المدخلات، وإلا فإنه يعيد مثالًا مضادًا ، أي مدخل e في I بحيث يفشل S ( c , e ).

يقوم برنامج CEGIS بتشغيل المولد والمُدقِّق في حلقة، مما يؤدي إلى تراكم الأمثلة المضادة:

خوارزمية cegis هي المدخلات : مولد البرنامج generate ، المُدقِّق يُدقِّق ، المواصفات spec ، الناتج : برنامج يفي بالمواصفات ، أو فشل المدخلات := مجموعة فارغة حلقة المرشح := توليد ( المواصفات ، المدخلات ) إذا تحقق ( المواصفات ، المرشح ) فأرجع المرشح وإلا فإن التحقق ينتج مثالًا مضادًا e أضف e إلى المدخلات نهاية إذا

تستخدم تطبيقات CEGIS عادةً محللات SMT كأدوات تحقق.

استُلهمت منهجية CEGIS من منهجية تحسين التجريد الموجهة بالأمثلة المضادة (CEGAR). ^{[ 11 ]}

تشمل قواعد الإثبات ما يلي:

• حل غير شرطي (انظر الجدول).

على سبيل المثال، يتم الحصول على السطر 55 عن طريق حل صيغ التأكيد.${\displaystyle E}$من 51 و${\displaystyle F}$من 52 والتي تشترك كلتاهما في بعض الصيغ الفرعية المشتركة${\displaystyle p}$يتشكل المُحلِّل نتيجةً لانفصال${\displaystyle E}$، مع${\displaystyle p}$تم استبدالها بـ${\displaystyle {\it {true}}}$، و${\displaystyle F}$، مع${\displaystyle p}$تم استبدالها بـ${\displaystyle {\it {false}}}$وينتج هذا الحل منطقياً من اقتران${\displaystyle E}$و${\displaystyle F}$وبشكل عام،${\displaystyle E}$و${\displaystyle F}$لا يلزم سوى صيغتين فرعيتين موحدتين${\displaystyle p_{1}}$و${\displaystyle p_{2}}$على التوالي؛ ثم يتم تكوين المذيب الخاص بهما من${\displaystyle E\theta }$و${\displaystyle F\theta }$كما كان من قبل، حيث${\displaystyle \theta }$وهو العامل الأكثر عمومية لتوحيد${\displaystyle p_{1}}$و${\displaystyle p_{2}}$تعمم هذه القاعدة حل البنود . ^{[ 22 ]}

يتم دمج حدود البرنامج للصيغ الأصلية كما هو موضح في السطر 58 لتشكيل مخرجات المُحلِّل. في الحالة العامة،${\displaystyle \theta }$وينطبق ذلك على الأخير أيضاً. بما أن الصيغة الفرعية${\displaystyle p}$يظهر في المخرجات، ويجب توخي الحذر لحل الصيغ الفرعية فقط التي تتوافق مع الخصائص القابلة للحساب .

• التحويلات المنطقية.

على سبيل المثال،${\displaystyle E\land (F\lor G)}$يمكن تحويلها إلى${\displaystyle (E\land F)\lor (E\land G)}$) في التأكيدات وكذلك في الأهداف، لأن كليهما متكافئان.

• فصل التأكيدات الاقترانية والأهداف الانفصالية.

يظهر مثال على ذلك في الأسطر من 11 إلى 13 من مثال اللعبة أدناه.

• الاستقراء البنيوي .

تسمح هذه القاعدة بتوليف الدوال التكرارية . لشرط مسبق وشرط لاحق معينين "معطى${\displaystyle x}$بحيث${\displaystyle {\textit {pre}}(x)}$، يجد${\displaystyle f(x)=y}$بحيث${\displaystyle {\textit {post}}(x,y)}$"، وترتيب مناسب يُمنح للمستخدم${\displaystyle \prec }$من نطاق${\displaystyle x}$من الجيد دائمًا إضافة تأكيد.${\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}$[ ^{23 ] يمكن أن يؤدي الحل باستخدام هذا التأكيد إلى} استدعاء متكرر لـ${\displaystyle f}$في الفصل الدراسي للبرنامج.

يُقدّم مثال على ذلك في كتاب مانا، والدينجر (1980)، الصفحات 108-111، حيث تمّ توليف خوارزمية لحساب ناتج قسمة وباقي قسمة عددين صحيحين معطيين، باستخدام الترتيب الجيد.${\displaystyle (n',d')\prec (n,d)}$محدد بواسطة${\displaystyle 0\leq n'<n}$(ص 110).

أثبت موراي أن هذه القواعد كاملة لمنطق الرتبة الأولى . ^{[ 24 ]} في عام 1986، أضاف مانا ووالدينجر قواعد الاستدلال المعممة E وقواعد التعديل البارامتري للتعامل مع المساواة أيضًا؛ ^{[ 25 ]} لاحقًا، تبين أن هذه القواعد غير كاملة (لكنها مع ذلك سليمة ). ^{[ 26 ]}

مثال على توليف الدالة القصوى

رقم	التأكيدات	الأهداف	برنامج	أصل
1	${\displaystyle A=A}$			بديهية
2	${\displaystyle A\leq A}$			بديهية
3	${\displaystyle A\leq B\lor B\leq A}$			بديهية
10		${\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}$	م	مواصفة
11		${\displaystyle (x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)}$	م	Distr(10)
12		${\displaystyle x\leq M\land y\leq M\land x=M}$	م	Split(11)
13		${\displaystyle x\leq M\land y\leq M\land y=M}$	م	Split(11)
14		${\displaystyle x\leq x\land y\leq x}$	x	Resolve(12,1)
15		${\displaystyle y\leq x}$	x	Resolve(14,2)
16		${\displaystyle \lnot (x\leq y)}$	x	Resolve(15,3)
17		${\displaystyle x\leq y\land y\leq y}$	y	Resolve(13,1)
18		${\displaystyle x\leq y}$	y	Resolve(17,2)
19		${\displaystyle {\textit {true}}}$	x<y ? y : x	Resolve(18,16)

كمثال توضيحي، برنامج وظيفي لحساب القيمة القصوى${\displaystyle M}$من رقمين${\displaystyle x}$و${\displaystyle y}$يمكن اشتقاقها على النحو التالي.

انطلاقًا من وصف المتطلبات " الحد الأقصى أكبر من أو يساوي أي عدد معطى، وهو أحد الأعداد المعطاة "، صيغة الدرجة الأولى${\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}$يتم الحصول على هذه الصيغة كترجمة رسمية. يجب إثبات هذه الصيغة. وباستخدام عملية سكوليم العكسية ، ^{[ ملاحظة 4 ]} نحصل على الصيغة في السطر 10، حيث يشير الحرف الكبير إلى متغير، بينما يشير الحرف الصغير إلى ثابت سكوليم .

بعد تطبيق قاعدة التحويل لقانون التوزيع في السطر 11، يكون هدف البرهان هو الفصل، وبالتالي يمكن تقسيمه إلى حالتين، وهما السطران 12 و 13.

بالانتقال إلى الحالة الأولى، فإن حل السطر 12 باستخدام البديهية الواردة في السطر 1 يؤدي إلى إنشاء متغير البرنامج${\displaystyle M}$في السطر 14. وبشكل بديهي، يحدد الجزء الأخير من السطر 12 القيمة التي${\displaystyle M}$يجب أخذ ذلك في هذه الحالة. رسميًا، يتم تطبيق قاعدة الحل غير الشرطية الموضحة في السطر 57 أعلاه على السطرين 12 و1، مع

• p هو المثال المشترك x=x لـ A=A و x=M ، والذي تم الحصول عليه من خلال توحيد الصيغ الأخيرةنحويًا
• F[ p ] صحيحة ∧ x=x ، تم الحصول عليها من السطر 1 المُنشأ (مع إضافة حشو مناسب لجعل سياق F[⋅] حول p مرئيًا )، و
• G[ p ] حيث x ≤ x ∧ y ≤ x ∧ x = x ، تم الحصول عليها من السطر 12 المُنشأ،

الاستسلام ${\displaystyle \lnot (}$صحيح ∧ خطأ ) ∧ ( x ≤ x ∧ y ≤ x ∧ صحيح${\displaystyle )}$، وهو ما يتبسط إلى${\displaystyle x\leq x\land y\leq x}$.

وبالمثل، ينتج عن السطر 14 السطر 15 ثم السطر 16 بالتحليل. وكذلك في الحالة الثانية،${\displaystyle x\leq M\land y\leq M\land y=M}$في السطر 13، يتم التعامل معها بشكل مماثل، مما يؤدي في النهاية إلى السطر 18.

في الخطوة الأخيرة، يتم دمج الحالتين (أي السطرين 16 و18) باستخدام قاعدة الحل من السطر 58؛ ولجعل هذه القاعدة قابلة للتطبيق، كانت الخطوة التحضيرية 15 ← 16 ضرورية. وبشكل بديهي، يمكن قراءة السطر 18 على أنه "في حالة${\displaystyle x\leq y}$الناتج${\displaystyle y}$صحيح (بالنسبة للمواصفات الأصلية)، بينما يقول السطر 15 "في حالة${\displaystyle y\leq x}$الناتج${\displaystyle x}$صحيح؛ أثبتت الخطوة 15 ← 16 أن الحالتين 16 و18 متكاملتان. ^{[ ملاحظة 5 ]} بما أن السطرين 16 و18 يحتويان على مصطلح برمجي، فإن التعبير الشرطي ينتج في عمود البرنامج. بما أن صيغة الهدف${\displaystyle {\textit {true}}}$تم التوصل إلى النتيجة، وتم إثباتها، وعمود البرنامج في "${\displaystyle {\textit {true}}}$يحتوي السطر على البرنامج.