प्रोग्राम सिंथेसिस

कंप्यूटर विज्ञान में, कार्यक्रम संश्लेषण एक ऐसा कार्यक्रम बनाने का कार्य है किसी दिए गए उच्च-स्तरीय औपचारिक विनिर्देश को प्रमाणित करता है। कार्यक्रम सत्यापन के विपरीत, कार्यक्रम दिए जाने के बजाय निर्मित किया जाना है; तथापि, दोनों क्षेत्र औपचारिक प्रमाण तकनीकों का उपयोग करते हैं, और दोनों में स्वचालितकरण की विभिन्न डिग्री के दृष्टिकोण सम्मिलित हैं। स्वचालित प्रोग्रामिंग तकनीकों के विपरीत, कार्यक्रम संश्लेषण में विनिर्देश सामान्यतः एक उपयुक्त तार्किक कलन में गैर-एल्गोरिदमिक कथन होते हैं।

उत्पत्ति

1957 में कॉर्नेल विश्वविद्यालय में समर इंस्टीट्यूट ऑफ सिंबॉलिक लॉजिक के दौरान, अलोंजो चर्च ने गणितीय आवश्यकताओं से एक सर्किट को संश्लेषित करने की समस्या को परिभाषित किया। भले ही काम केवल सर्किट को संदर्भित करता है और कार्यक्रम को नहीं, काम को कार्यक्रम संश्लेषण के प्रारंभिक विवरणों में से एक माना जाता है और कुछ शोधकर्ता कार्यक्रम संश्लेषण को "चर्च की समस्या" के रूप में संदर्भित करते हैं। 1960 के दशक में, आर्टिफिशियल इंटेलिजेंस में शोधकर्ताओं द्वारा "स्वचालित प्रोग्रामर" के लिए एक समान विचार की खोज की गई थी।

तब से, विभिन्न अनुसंधान समुदायों ने कार्यक्रम संश्लेषण की समस्या पर विचार किया। उल्लेखनीय कार्यों में बुच्ची और लैंडवेबर द्वारा 1969 ऑटोमेटा-सैद्धांतिक दृष्टिकोण, और मन्ना और वाल्डिंगर (सी। 1980) द्वारा कार्य सम्मिलित हैं। आधुनिक उच्च-स्तरीय प्रोग्रामिंग भाषाओं के विकास को कार्यक्रम संश्लेषण के एक रूप के रूप में भी समझा जा सकता है।

21वीं सदी के घटनाक्रम

21 वीं सदी के प्रारंभ में औपचारिक सत्यापन समुदाय और संबंधित क्षेत्रों में कार्यक्रम संश्लेषण के विचार में व्यावहारिक रुचि में वृद्धि देखी गई है। अरमांडो सोलर-लेज़ामा ने दिखाया कि बूलियन तर्क में कार्यक्रम संश्लेषण समस्याओं को एनकोड करना संभव है और बूलियन संतुष्टि समस्या के लिए एल्गोरिदम का उपयोग स्वचालित रूप से कार्यक्रम खोजने के लिए किया जाता है। 2013 में, यूपीएन, यूसी बर्कले और एमआईटी के शोधकर्ताओं द्वारा कार्यक्रम संश्लेषण समस्याओं के लिए एक एकीकृत रूपरेखा प्रस्तावित की गई थी। 2014 के बाद से एक प्रतिस्पर्धी कार्यक्रम, सिंटैक्स-गाइडेड संश्लेषण प्रतियोगिता या एसयगस-कॉमपी में कार्यक्रम संश्लेषण के लिए विभिन्न एल्गोरिदम की तुलना करने वाली एक वार्षिक कार्यक्रम संश्लेषण प्रतियोगिता हुई है। फिर भी, उपलब्ध एल्गोरिदम केवल छोटे प्रोग्रामों को संश्लेषित करने में सक्षम हैं।

मन्ना और वाल्डिंगर की रूपरेखा

गैर-क्लॉज़ल रिज़ॉल्यूशन नियम (एकीकृत प्रतिस्थापन नहीं दिखाए गए)

एनआर	अभिकथन	लक्ष्य	कार्यक्रम	मूल
51	$E[p]$
52	$F[p]$
53		$G[p]$	s
54		$H[p]$	t
55	$E[{\text{true}}]\lor F[{\text{false}}]$			संकल्प(51,52)
56		$\lnot F[{\text{true}}]\land G[{\text{false}}]$	s	संकल्प(52,53)
57		$\lnot F[{\text{false}}]\land G[{\text{true}}]$	s	संकल्प(53,52)
58		$G[{\text{true}}]\land H[{\text{false}}]$	p ? s : t	संकल्प(53,54)

1980 में प्रकाशित मन्ना और वाल्डिंगर का ढांचा, उपयोगकर्ता द्वारा दिए गए पहले-क्रम विनिर्देश सूत्र से प्रारंभ होता है। उस सूत्र के लिए, एक प्रमाण का निर्माण किया जाता है, जिससे एक कार्यात्मक कार्यक्रम को एकीकृत प्रतिस्थापन से भी संश्लेषित किया जाता है।

ढांचे को तालिका लेआउट में प्रस्तुत किया गया है, जिसमें कॉलम सम्मिलित हैं:

• संदर्भ उद्देश्यों के लिए एक पंक्ति संख्या ("एनआर")।
• सूत्र जो पहले से ही स्थापित किए जा चुके हैं, जिनमें स्वयंसिद्ध और पूर्व शर्त सम्मिलित हैं, ("अभिकथन")
• फॉर्मूले अभी भी सिद्ध होने बाकी हैं, पोस्टकंडिशन (लक्ष्य), सम्मिलित हैं
• वैध आउटपुट वैल्यू ("प्रोग्राम") को दर्शाने वाली शर्तें
• वर्तमान पंक्ति के लिए एक औचित्य ("उत्पत्ति")

प्रारंभ में, पृष्ठभूमि ज्ञान, पूर्व-शर्तें और पश्च-शर्तें तालिका में दर्ज की जाती हैं। उसके बाद, उपयुक्त प्रमाण नियम मैन्युअल रूप से लागू किए जाते हैं। ढांचे को मध्यवर्ती सूत्रों की मानव पठनीयता को बढ़ाने के लिए डिज़ाइन किया गया है: शास्त्रीयसंकल्प के विपरीत, इसे क्लॉसल सामान्य रूप की आवश्यकता नहीं होती है, लेकिन मनमाना संरचना के सूत्रों के साथ तर्क करने की अनुमति देता है और किसी भी जंक्शनर्स ("गैर-खंड संकल्प") को सम्मिलित करता है। प्रमाण कब पूरा होता है ${\it {true}}$ लक्ष्य स्तंभ में व्युत्पन्न किया गया है, या, समकक्ष रूप से, ${\it {false}}$ अभिकथन कॉलम में। इस दृष्टिकोण से प्राप्त कार्यक्रम से प्रारंभ होने वाले विनिर्देश सूत्र को पूरा करने की गारंटी है; इस अर्थ में वे निर्माण द्वारा सही हैं। केवल एक न्यूनतावादी, अभी तक ट्यूरिंग-पूर्ण, विशुद्ध रूप से कार्यात्मक प्रोग्रामिंग भाषा, जिसमें सशर्त, पुनरावर्तन और अंकगणित और अन्य ऑपरेटर सम्मिलित हैं समर्थित है। इस ढांचे के भीतर किए गए मामले के अध्ययन ने गणना करने के लिए एल्गोरिदम को संश्लेषित किया उदाहरण के लिए विभाजन, शेष, वर्गमूल, एकीकरण, संबंधपरक डेटाबेस प्रश्नों के उत्तर और कई छँटाई एल्गोरिदम।

प्रमाण नियम

प्रमाण नियमों में सम्मिलित हैं:

• नॉन-क्लॉज़ल रेज़ोल्यूशन (तालिका देखें)।

उदाहरण के लिए, अभिकथन सूत्रों को हल करके पंक्ति 55 प्राप्त की जाती है $E$ 51 से और $F$ 52 से जो दोनों कुछ सामान्य उपसूत्र साझा करते हैं $p$. विलायक के विघटन के रूप में बनता है $E$, साथ $p$ द्वारा प्रतिस्थापित किया गया ${\it {true}}$, और $F$, साथ $p$ द्वारा प्रतिस्थापित किया गया ${\it {false}}$। यह विलायक तार्किक रूप से के संयोजन से अनुसरण करता है $E$ और $F$। अधिक सामान्यतः, $E$ और $F$ को केवल दो अविवेकी उपसूत्रों की आवश्यकता है $p_{1}$ और $p_{2}$, क्रमश; उनके विलायक तब से बनते हैं $E\theta$ और $F\theta$ पहले की तरह, जहाँ $\theta$ का सबसे सामान्य एकीकृतकर्ता है $p_{1}$और $p_{2}$। यह नियम खंडों के समाधान का सामान्यीकरण करता है।

रिज़ॉल्वेंट के आउटपुट को बनाने के लिए पैरेंट फ़ार्मुलों के प्रोग्राम टर्म्स को लाइन 58 में दिखाए अनुसार संयोजित किया जाता है। सामान्य मामले में, $\theta$ बाद वाले पर भी लागू होता है। सबफॉर्मूला के बाद से $p$ आउटपुट में दिखाई देता है, गणना योग्य गुणों के अनुरूप केवल उप सूत्रों पर हल करने के लिए देखभाल की जानी चाहिए।

• तार्किक परिवर्तन।

उदाहरण के लिए, $E\land (F\lor G)$ को रूपांतरित किया जा सकता है $(E\land F)\lor (E\land G)$) अभिकथन और साथ ही लक्ष्यों में, क्योंकि दोनों समान हैं।

• संयोजक अभिकथनों और वियोजनात्मक लक्ष्यों का विभाजन।

एक उदाहरण नीचे दिए गए खिलौने के उदाहरण की 11 से 13 पंक्तियों में दिखाया गया है।

• संरचनात्मक प्रेरण।

यह नियम पुनरावर्ती कार्यों के संश्लेषण की अनुमति देता है। किसी दिए गए पूर्व और बाद की स्थिति के लिए "दिया गया $x$ ऐसा है कि ${\textit {pre}}(x)$, ढूंढें $f(x)=y$ ऐसा है कि ${\textit {post}}(x,y)$", और एक उपयुक्त उपयोगकर्ता द्वारा दिया गया सुव्यवस्थित आदेश $\prec$ के डोमेन $x$, एक अभिकथन जोड़ना हमेशा अच्छा होता है$x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))$. इस अभिकथन के साथ समाधान करने के लिए एक पुनरावर्ती कॉल प्रस्तुत कर सकता है $f$ कार्यक्रम अवधि में।

मन्ना, वाल्डिंगर (1980), पृष्ठ 108-111 में एक उदाहरण दिया गया है, जहां दो दिए गए पूर्णांकों के भागफल और शेष की गणना करने के लिए एक एल्गोरिथ्म को अच्छी तरह से क्रम का उपयोग करके संश्लेषित किया जाता है। $(n',d')\prec (n,d)$ द्वारा परिभाषित $0\leq n'<n$ (पृष्ठ 110)।

मुर्रे ने इन नियमों को प्रथम-क्रम तर्क के लिए पूर्ण दिखाया है। 1986 में, मन्ना और वाल्डिंगर ने समानता को संभालने के लिए सामान्यीकृत ई-रिज़ॉल्यूशन और पैरामॉड्यूलेशन नियम जोड़े; बाद में, ये नियम अधूरे निकले (लेकिन फिर भी सही थे)।

उदाहरण

अधिकतम कार्य का उदाहरण संश्लेषण

एनआर	अभिकथन	लक्ष्य	कार्यक्रम	मूल
1	$A=A$			स्वयंसिद्ध
2	$A\leq A$			स्वयंसिद्ध
3	$A\leq B\lor B\leq A$			स्वयंसिद्ध
10		$x\leq M\land y\leq M\land (x=M\lor y=M)$	M	विनिर्देश
11		$(x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)$	M	डीआईएसटीआर(10)
12		$x\leq M\land y\leq M\land x=M$	M	विभाजित करना(11)
13		$x\leq M\land y\leq M\land y=M$	M	विभाजित करना(11)
14		$x\leq x\land y\leq x$	x	संकल्प(12,1)
15		$y\leq x$	x	संकल्प(14,2)
16		$\lnot (x\leq y)$	x	संकल्प(15,3)
17		$x\leq y\land y\leq y$	y	संकल्प(13,1)
18		$x\leq y$	y	संकल्प(17,2)
19		${\textit {true}}$	x<y ? y : x	संकल्प(18,16)

एक खिलौना उदाहरण के रूप में, अधिकतम गणना करने के लिए एक कार्यात्मक कार्यक्रम दो नंबर का $M$ $x$ और $y$ को निम्नानुसार प्राप्त किया जा सकता है।

आवश्यकता विवरण से प्रारंभ करते हुए "अधिकतम किसी भी संख्या से बड़ा या उसके बराबर है, और दी गई संख्याओं में से एक है", प्रथम-क्रम सूत्र $\forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)$ इसके औपचारिक अनुवाद के रूप में प्राप्त किया जाता है। इस सूत्र को सिद्ध करना है। रिवर्स विद्वता द्वारा, पंक्ति 10 में विनिर्देश प्राप्त किया गया है, क्रमशः एक चर और एक स्कोलेम स्थिरांक को दर्शाते हुए एक बड़े और छोटे अक्षर।

पंक्ति 11 में वितरण नियम के लिए रूपांतरण नियम लागू करने के बाद, प्रमाण लक्ष्य एक संयोजन है, और इसलिए इसे दो मामलों में विभाजित किया जा सकता है, अर्थात। लाइन 12 और 13।

पहले मामले की ओर मुड़ते हुए, पंक्ति 12 को पंक्ति 1 में स्वयंसिद्ध के साथ हल करने से कार्यक्रम चर की तात्कालिकता होती है $M$ पंक्ति 14 में। सहज रूप से, पंक्ति 12 का अंतिम संयोजन मूल्य निर्धारित करता है $M$ इस मामले में लेना चाहिए। औपचारिक रूप से, उपरोक्त पंक्ति 57 में दिखाया गया गैर-खंड संकल्प नियम 12 और 1 पंक्तियों पर लागू होता है

• p का A=A और x=M का सामान्य उदाहरण x=x है, जो बाद के सूत्रों को वाक्यगत रूप से एकीकृत करके प्राप्त किया गया है,
• F[p] true ∧ x=x, तात्कालिक पंक्ति 1 से प्राप्त किया गया है (उचित रूप से पैड किया गया है ताकि संदर्भ F[⋅] को p के आसपास दिखाई दे), और
• G[p] x ≤ x ∧ y ≤ x ∧ x = x, होने के नाते, तत्काल रेखा 12 से प्राप्त किया गया है,

उपज $\lnot ($true ∧ false) ∧ (x ≤ x ∧ y ≤ x ∧ true$)$, जो करने के लिए सरल करता है $x\leq x\land y\leq x$.

इसी तरह, लाइन 14 से लाइन 15 और फिर लाइन 16 रेजोल्यूशन से मिलती है। साथ ही, दूसरा मामला, $x\leq M\land y\leq M\land y=M$ लाइन 13 में, इसी तरह से संभाला जाता है, अंत में लाइन 18 देता है।

अंतिम चरण में, दोनों स्थितियाँ (यानी पंक्तियाँ 16 और 18) जुड़ जाती हैं, पंक्ति 58 से संकल्प नियम का उपयोग करते हुए; उस नियम को लागू करने के लिए प्रारंभिक चरण 15→16 की आवश्यकता थी। सहज रूप से, पंक्ति 18 को "मामले में" के रूप में पढ़ा जा सकता है $x\leq y$, उत्पादन $y$ मान्य है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं। चूँकि दोनों पंक्तियाँ 16 और 18 एक कार्यक्रम शब्द के साथ आती हैं, एक सशर्त अभिव्यक्ति का परिणाम प्रोग्राम कॉलम में होता है। लक्ष्य सूत्र के बाद से ${\textit {true}}$ व्युत्पन्न किया गया है, प्रमाण दिया गया है, और का कार्यक्रम स्तंभ ${\textit {true}}$ पंक्ति में कार्यक्रम है।

यह भी देखें

• आगमनात्मक प्रोग्रामिंग
• मेटाप्रोग्रामिंग
• कार्यक्रम व्युत्पत्ति
• प्राकृतिक भाषा प्रोग्रामिंग
• प्रतिक्रियाशील संश्लेषण

संदर्भ

• Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning in Program Synthesis". Artificial Intelligence. 6 (2): 175–208. doi:10.1016/0004-3702(75)90008-9.