Difference between revisions of "प्रोग्राम सिंथेसिस"

Revision as of 22:19, 14 March 2023

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

उत्पत्ति

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

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

21वीं सदी के विकास

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

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

Non-clausal resolution rules (unifying substitutions not shown)
Nr	Assertions	Goals	Program	Origin
51	$E[p]$
52	$F[p]$
53		$G[p]$	s
54		$H[p]$	t
55	$E[{\text{true}}]\lor F[{\text{false}}]$			Resolve(51,52)
56		$\lnot F[{\text{true}}]\land G[{\text{false}}]$	s	Resolve(52,53)
57		$\lnot F[{\text{false}}]\land G[{\text{true}}]$	s	Resolve(53,52)
58		$G[{\text{true}}]\land H[{\text{false}}]$	p ? s : t	Resolve(53,54)

1980 में प्रकाशित ज़ोहर मन्ना और रिचर्ड वाल्डिंगर की रूपरेखा,^[7]^[8] उपयोगकर्ता द्वारा दिए गए प्रथम-क्रम तर्क | प्रथम-क्रम विनिर्देश सूत्र से शुरू होता है। उस सूत्र के लिए, एक प्रमाण का निर्माण किया जाता है, जिससे एकीकरण (कंप्यूटर विज्ञान) से एक कार्यात्मक कार्यक्रम का संश्लेषण भी होता है # प्रथम-क्रम के शब्दों के प्रतिस्थापन का वाक्यात्मक एकीकरण।

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

संदर्भ उद्देश्यों के लिए एक पंक्ति संख्या (Nr)।
सुगठित सूत्र # विधेय तर्क जो पहले से ही स्थापित हो चुका है, जिसमें स्वयंसिद्ध और पूर्व शर्त शामिल हैं, (अभिकथन)
फॉर्मूले अभी भी साबित होने बाकी हैं, पोस्टकंडिशन सहित, (लक्ष्य),^{[note 1]}
टर्म (तर्क) एक वैध आउटपुट वैल्यू ( कार्यक्रम) को दर्शाता है^{[note 2]}
वर्तमान लाइन के लिए एक औचित्य (उत्पत्ति)

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

सबूत नियम

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

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

उदाहरण के लिए, अभिकथन सूत्रों को हल करके पंक्ति 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}

. यह नियम पहले क्रम के तर्क में संकल्प (तर्क) #संकल्प का सामान्यीकरण करता है।^[17]

पैरेंट फ़ार्मुलों की कार्यक्रमशर्तों को संयोजित किया जाता है, जैसा कि पंक्ति 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'))

.^[18] इस अभिकथन के साथ समाधान करने के लिए एक पुनरावर्ती कॉल का परिचय दिया जा सकता है

f

कार्यक्रम अवधि में।

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

(n',d')\prec (n,d)

द्वारा परिभाषित

0\leq n'<n

(पृष्ठ 110)।

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

उदाहरण

Example synthesis of maximum function
Nr	Assertions	Goals	Program	Origin
1	$A=A$			Axiom
2	$A\leq A$			Axiom
3	$A\leq B\lor B\leq A$			Axiom
10		$x\leq M\land y\leq M\land (x=M\lor y=M)$	M	Specification
11		$(x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)$	M	Distr(10)
12		$x\leq M\land y\leq M\land x=M$	M	Split(11)
13		$x\leq M\land y\leq M\land y=M$	M	Split(11)
14		$x\leq x\land y\leq x$	x	Resolve(12,1)
15		$y\leq x$	x	Resolve(14,2)
16		$\lnot (x\leq y)$	x	Resolve(15,3)
17		$x\leq y\land y\leq y$	y	Resolve(13,1)
18		$x\leq y$	y	Resolve(17,2)
19		${\textit {true}}$	x<y ? y : x	Resolve(18,16)

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

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

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

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

$p$ सामान्य उदाहरण होने के नाते $x=x$ का $A=A$ और $x=M$ , वाक्य-विन्यास एकीकरण (कंप्यूटर विज्ञान) द्वारा प्राप्त # पहले-क्रम की शर्तों के बाद के सूत्रों का वाक्य-विन्यास एकीकरण,
$F[$ $p$ $]$ प्राणी $true \land$ $x=x$ , प्रतिस्थापन (तर्क) से प्राप्त # प्रथम-क्रम तर्क पंक्ति 1 (संदर्भ बनाने के लिए उचित रूप से गद्देदार $F[\cdot]$ आस-पास $p$ दृश्यमान), और
$G[$ $p$ $]$ प्राणी $x \leq x \land y \leq x \land$ $x = x$ , तात्कालिक रेखा 12 से प्राप्त,

उपज $\lnot ($ $true \land$ $false$ $) \land ($ $x \leq x \land y \leq x \land$ $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 कहती है case $y\leq x$ , उत्पादन $x$ यह सही है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं।^{[note 5]} चूँकि 16 और 18 दोनों पंक्तियाँ एक कार्यक्रमटर्म के साथ आती हैं, a ?: कार्यक्रमकॉलम में परिणाम देता है। लक्ष्य सूत्र के बाद से ${\textit {true}}$ व्युत्पन्न किया गया है, प्रमाण किया गया है, और का कार्यक्रम स्तंभ ${\textit {true}}$ लाइन में कार्यक्रम शामिल है।

यह भी देखें

↑ The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of proof by contradiction, a Goal $F$ is equivalent to an assertion $\lnot F$ .
↑ When $F$ and $s$ is the Goal formula and the Program term in a line, respectively, then in all cases where $F$ holds, $s$ is a valid output of the program to be synthesized. This invariant is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.
↑ Only the conditional operator (?:) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of $=$ and $\leq$ that are actually needed in the proof have been axiomatized, in line 1 to 3.
↑ While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.
↑ Axiom 3 was needed for that; in fact, if $\leq$ wasn't a total order, no maximum could be computed for uncomparable inputs $x,y$ .

संदर्भ

↑ Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट. LNCS. Vol. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.
↑ Alonzo Church (1957). "परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग". Summaries of the Summer Institute of Symbolic Logic. 1: 3–50.
↑ Richard Büchi, Lawrence Landweber (Apr 1969). "परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना". Transactions of the American Mathematical Society. 138: 295–311. doi:10.2307/1994916. JSTOR 1994916.
↑ Solar-Lezama, Armando (2008). स्केचिंग द्वारा प्रोग्राम संश्लेषण (PDF) (Ph.D.). University of California, Berkeley.
↑ Alur, Rajeev; al., et (2013). "सिंटेक्स-निर्देशित संश्लेषण". Proceedings of Formal Methods in Computer-Aided Design. IEEE. p. 8.
↑ SyGuS-Comp (Syntax-Guided Synthesis Competition)
↑ Zohar Manna, Richard Waldinger (Jan 1980). "कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.
↑ Zohar Manna and Richard Waldinger (Dec 1978). कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण (PDF) (Technical Note). SRI International. Archived (PDF) from the original on January 27, 2021.
↑ See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.
↑ Boyer, Robert S.; Moore, J. Strother (May 1983). शुद्ध लिस्प की ट्यूरिंग पूर्णता का एक यांत्रिक प्रमाण (PDF) (Technical report). Institute for Computing Science, University of Texas at Austin. 37. Archived (PDF) from the original on 22 September 2017.
↑ Manna, Waldinger (1980), p.108-111
↑ Zohar Manna and Richard Waldinger (Aug 1987). "एक द्विआधारी-खोज प्रतिमान की उत्पत्ति". Science of Computer Programming. 9 (1): 37–83. doi:10.1016/0167-6423(87)90025-6.
↑ Daniele Nardi (1989). "निगमनात्मक-झांकी विधि द्वारा एक एकीकरण एल्गोरिथम का औपचारिक संश्लेषण". Journal of Logic Programming. 7: 1–43. doi:10.1016/0743-1066(89)90008-3.
↑ Daniele Nardi and Riccardo Rosati (1992). "Deductive Synthesis of Programs for Query Answering". In Kung-Kiu Lau and Tim Clement (ed.). तर्क कार्यक्रम संश्लेषण और परिवर्तन पर अंतर्राष्ट्रीय कार्यशाला (LOPSTR). Workshops in Computing. Springer. pp. 15–29. doi:10.1007/978-1-4471-3560-9_2.
↑ Jonathan Traugott (1986). "Deductive Synthesis of Sorting Programs". स्वचालित कटौती पर अंतर्राष्ट्रीय सम्मेलन की कार्यवाही. LNCS. Vol. 230. Springer. pp. 641–660.
↑ Jonathan Traugott (Jun 1989). "छँटाई कार्यक्रमों का निगमनात्मक संश्लेषण". Journal of Symbolic Computation. 7 (6): 533–572. doi:10.1016/S0747-7171(89)80040-9.
↑ Manna, Waldinger (1980), p.99
↑ Manna, Waldinger (1980), p.104
↑ Manna, Waldinger (1980), p.103, referring to: Neil V. Murray (Feb 1979). A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. 2-79.
↑ Zohar Manna, Richard Waldinger (Jan 1986). "स्वचालित कटौती में विशेष संबंध". Journal of the ACM. 33: 1–59. doi:10.1145/4904.4905. S2CID 15140138.
↑ Zohar Manna, Richard Waldinger (1992). "The Special-Relations Rules are Incomplete". प्रक्रिया। सीएडीई 11. LNCS. Vol. 607. Springer. pp. 492–506.

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.

[9] The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of proof by contradiction, a Goal $F$ is equivalent to an assertion $\lnot F$ .

[10] When $F$ and $s$ is the Goal formula and the Program term in a line, respectively, then in all cases where $F$ holds, $s$ is a valid output of the program to be synthesized. This invariant is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.

[13] Only the conditional operator (?:) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of $=$ and $\leq$ that are actually needed in the proof have been axiomatized, in line 1 to 3.

[25] While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.

[26] Axiom 3 was needed for that; in fact, if $\leq$ wasn't a total order, no maximum could be computed for uncomparable inputs $x,y$ .

[1] Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट. LNCS. Vol. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.

[2] Alonzo Church (1957). "परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग". Summaries of the Summer Institute of Symbolic Logic. 1: 3–50.

[3] Richard Büchi, Lawrence Landweber (Apr 1969). "परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना". Transactions of the American Mathematical Society. 138: 295–311. doi:10.2307/1994916. JSTOR 1994916.

[4] Solar-Lezama, Armando (2008). स्केचिंग द्वारा प्रोग्राम संश्लेषण (PDF) (Ph.D.). University of California, Berkeley.

[5] Alur, Rajeev; al., et (2013). "सिंटेक्स-निर्देशित संश्लेषण". Proceedings of Formal Methods in Computer-Aided Design. IEEE. p. 8.

[6] SyGuS-Comp (Syntax-Guided Synthesis Competition)

[7] Zohar Manna, Richard Waldinger (Jan 1980). "कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण". ACM Transactions on Programming Languages and Systems. 2: 90–121. doi:10.1145/357084.357090. S2CID 14770735.

[8] Zohar Manna and Richard Waldinger (Dec 1978). कार्यक्रम संश्लेषण के लिए एक निगमनात्मक दृष्टिकोण (PDF) (Technical Note). SRI International. Archived (PDF) from the original on January 27, 2021.

[11] See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.

[12] Boyer, Robert S.; Moore, J. Strother (May 1983). शुद्ध लिस्प की ट्यूरिंग पूर्णता का एक यांत्रिक प्रमाण (PDF) (Technical report). Institute for Computing Science, University of Texas at Austin. 37. Archived (PDF) from the original on 22 September 2017.

[14] Manna, Waldinger (1980), p.108-111

[15] Zohar Manna and Richard Waldinger (Aug 1987). "एक द्विआधारी-खोज प्रतिमान की उत्पत्ति". Science of Computer Programming. 9 (1): 37–83. doi:10.1016/0167-6423(87)90025-6.

[16] Daniele Nardi (1989). "निगमनात्मक-झांकी विधि द्वारा एक एकीकरण एल्गोरिथम का औपचारिक संश्लेषण". Journal of Logic Programming. 7: 1–43. doi:10.1016/0743-1066(89)90008-3.

[17] Daniele Nardi and Riccardo Rosati (1992). "Deductive Synthesis of Programs for Query Answering". In Kung-Kiu Lau and Tim Clement (ed.). तर्क कार्यक्रम संश्लेषण और परिवर्तन पर अंतर्राष्ट्रीय कार्यशाला (LOPSTR). Workshops in Computing. Springer. pp. 15–29. doi:10.1007/978-1-4471-3560-9_2.

[18] Jonathan Traugott (1986). "Deductive Synthesis of Sorting Programs". स्वचालित कटौती पर अंतर्राष्ट्रीय सम्मेलन की कार्यवाही. LNCS. Vol. 230. Springer. pp. 641–660.

[19] Jonathan Traugott (Jun 1989). "छँटाई कार्यक्रमों का निगमनात्मक संश्लेषण". Journal of Symbolic Computation. 7 (6): 533–572. doi:10.1016/S0747-7171(89)80040-9.

[20] Manna, Waldinger (1980), p.99

[21] Manna, Waldinger (1980), p.104

[22] Manna, Waldinger (1980), p.103, referring to: Neil V. Murray (Feb 1979). A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. 2-79.

[23] Zohar Manna, Richard Waldinger (Jan 1986). "स्वचालित कटौती में विशेष संबंध". Journal of the ACM. 33: 1–59. doi:10.1145/4904.4905. S2CID 15140138.

[24] Zohar Manna, Richard Waldinger (1992). "The Special-Relations Rules are Incomplete". प्रक्रिया। सीएडीई 11. LNCS. Vol. 607. Springer. pp. 492–506.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[note 1]

[note 2]

[9]

[10]

[note 3]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[note 4]

[note 5]

@@ Line 1: / Line 1: @@
-[[कंप्यूटर विज्ञान]] में, प्रोग्राम संश्लेषण एक ऐसा [[कंप्यूटर प्रोग्राम|प्रोग्राम]] बनाने का कार्य है किसी दिए गए उच्च-स्तरीय औपचारिक विनिर्देश को प्रमाणित करता है। [[कार्यक्रम सत्यापन]] के विपरीत, कार्यक्रम दिए जाने के बजाय निर्मित किया जाना है; तथापि, दोनों क्षेत्र औपचारिक प्रमाण तकनीकों का उपयोग करते हैं, और दोनों में स्वचालितकरण की विभिन्न डिग्री के दृष्टिकोण सम्मिलित हैं। [[स्वचालित प्रोग्रामिंग]] तकनीकों के विपरीत, प्रोग्राम संश्लेषण में विनिर्देश सामान्यतः एक उपयुक्त तार्किक कलन में गैर-एल्गोरिदमिक कथन होते हैं।<ref>{{cite book |last1= Basin |first1= D. |last2= Deville |first2= Y. |last3= Flener |first3 = P. |last4= Hamfelt |first4= A. |last5= Fischer Nilsson |first5= J. |chapter= Synthesis of programs in computational logic |editor=M. Bruynooghe and K.-K. Lau | publisher=Springer | series=LNCS | volume=3049 | pages=30&ndash;65 |citeseerx=10.1.1.62.4976 |title= कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट| year = 2004 }}</ref>
+[[कंप्यूटर विज्ञान]] में, कार्यक्रम संश्लेषण एक ऐसा कार्यक्रम बनाने का कार्य है किसी दिए गए उच्च-स्तरीय औपचारिक विनिर्देश को प्रमाणित करता है। [[कार्यक्रम सत्यापन]] के विपरीत, कार्यक्रम दिए जाने के बजाय निर्मित किया जाना है; तथापि, दोनों क्षेत्र औपचारिक प्रमाण तकनीकों का उपयोग करते हैं, और दोनों में स्वचालितकरण की विभिन्न डिग्री के दृष्टिकोण सम्मिलित हैं। [[स्वचालित प्रोग्रामिंग]] तकनीकों के विपरीत, कार्यक्रम संश्लेषण में विनिर्देश सामान्यतः एक उपयुक्त तार्किक कलन में गैर-एल्गोरिदमिक कथन होते हैं।<ref>{{cite book |last1= Basin |first1= D. |last2= Deville |first2= Y. |last3= Flener |first3 = P. |last4= Hamfelt |first4= A. |last5= Fischer Nilsson |first5= J. |chapter= Synthesis of programs in computational logic |editor=M. Bruynooghe and K.-K. Lau | publisher=Springer | series=LNCS | volume=3049 | pages=30&ndash;65 |citeseerx=10.1.1.62.4976 |title= कम्प्यूटेशनल लॉजिक में प्रोग्राम डेवलपमेंट| year = 2004 }}</ref>
 == उत्पत्ति ==
-में कॉर्नेल विश्वविद्यालय में समर इंस्टीट्यूट ऑफ सिंबॉलिक लॉजिक के दौरान, [[अलोंजो चर्च]] ने गणितीय आवश्यकताओं से एक सर्किट को संश्लेषित करने की समस्या को परिभाषित किया।<ref>{{cite journal| author=Alonzo Church| title=परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग| journal=Summaries of the Summer Institute of Symbolic Logic|date=1957| volume=1| pages=3–50}}</ref> भले ही काम केवल सर्किट को संदर्भित करता है और प्रोग्राम को नहीं, काम को प्रोग्राम सिंथेसिस के शुरुआती विवरणों में से एक माना जाता है और कुछ शोधकर्ता प्रोग्राम सिंथेसिस को चर्च की समस्या के रूप में संदर्भित करते हैं। 1960 के दशक में, आर्टिफिशियल इंटेलिजेंस में शोधकर्ताओं द्वारा एक स्वचालित प्रोग्रामर के लिए इसी तरह के विचार की खोज की गई थी।{{Citation needed|date=June 2010}}
+में कॉर्नेल विश्वविद्यालय में समर इंस्टीट्यूट ऑफ सिंबॉलिक लॉजिक के दौरान, [[अलोंजो चर्च]] ने गणितीय आवश्यकताओं से एक सर्किट को संश्लेषित करने की समस्या को परिभाषित किया।<ref>{{cite journal| author=Alonzo Church| title=परिपथ संश्लेषण की समस्या के लिए पुनरावर्ती अंकगणित के अनुप्रयोग| journal=Summaries of the Summer Institute of Symbolic Logic|date=1957| volume=1| pages=3–50}}</ref> भले ही काम केवल सर्किट को संदर्भित करता है और कार्यक्रम को नहीं, काम को कार्यक्रम संश्लेषण के प्रारंभिक विवरणों में से एक माना जाता है और कुछ शोधकर्ता कार्यक्रम संश्लेषण को "चर्च की समस्या" के रूप में संदर्भित करते हैं। 1960 के दशक में, आर्टिफिशियल इंटेलिजेंस में शोधकर्ताओं द्वारा "स्वचालित प्रोग्रामर" के लिए एक समान विचार की खोज की गई थी।{{Citation needed|date=June 2010}}
-तब से, विभिन्न अनुसंधान समुदायों ने कार्यक्रम संश्लेषण की समस्या पर विचार किया। उल्लेखनीय कार्यों में जूलियस रिचर्ड बुच्ची द्वारा 1969 का ऑटोमेटा-सैद्धांतिक दृष्टिकोण शामिल है। बुच्ची और [[लॉरेंस लैंडवेबर]],<ref>{{cite journal| author=Richard Büchi, Lawrence Landweber| title=परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना| journal=Transactions of the American Mathematical Society|date=Apr 1969| volume=138| pages=295–311| doi=10.2307/1994916| url=http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1087&context=cstech| jstor=1994916}}</ref> और [[ जौहर मन्ना ]] और [[रिचर्ड वाल्डिंगर]] (सी। 1980) द्वारा काम करता है। आधुनिक उच्च-स्तरीय प्रोग्रामिंग भाषाओं के विकास को प्रोग्राम सिंथेसिस के एक रूप के रूप में भी समझा जा सकता है।
+तब से, विभिन्न अनुसंधान समुदायों ने कार्यक्रम संश्लेषण की समस्या पर विचार किया। उल्लेखनीय कार्यों में बुच्ची और लैंडवेबर द्वारा 1969 ऑटोमेटा-सैद्धांतिक दृष्टिकोण,<ref>{{cite journal| author=Richard Büchi, Lawrence Landweber| title=परिमित-राज्य रणनीतियों द्वारा अनुक्रमिक स्थितियों को हल करना| journal=Transactions of the American Mathematical Society|date=Apr 1969| volume=138| pages=295–311| doi=10.2307/1994916| url=http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1087&context=cstech| jstor=1994916}}</ref> और मन्ना और वाल्डिंगर (सी। 1980) द्वारा कार्य सम्मिलित हैं। आधुनिक उच्च-स्तरीय प्रोग्रामिंग भाषाओं के विकास को कार्यक्रम संश्लेषण के एक रूप के रूप में भी समझा जा सकता है।
 == 21वीं सदी के विकास ==
-वीं सदी की शुरुआत में [[औपचारिक सत्यापन]] समुदाय और संबंधित क्षेत्रों में कार्यक्रम संश्लेषण के विचार में व्यावहारिक रुचि में वृद्धि देखी गई है। अरमांडो सोलर-लेज़ामा ने दिखाया कि [[ बूलियन तर्क ]] में प्रोग्राम सिंथेसिस समस्याओं को एनकोड करना संभव है और [[बूलियन संतुष्टि समस्या]] के लिए एल्गोरिदम का उपयोग स्वचालित रूप से प्रोग्राम खोजने के लिए किया जाता है।<ref>{{cite thesis |last=Solar-Lezama |first=Armando |date=2008 |title=स्केचिंग द्वारा प्रोग्राम संश्लेषण|type=Ph.D. |publisher=University of California, Berkeley |url=https://people.csail.mit.edu/asolar/papers/thesis.pdf}}</ref> 2013 में, [[UPenn]], UC बर्कले और [[MIT]] के शोधकर्ताओं द्वारा कार्यक्रम संश्लेषण समस्याओं के लिए एक एकीकृत रूपरेखा प्रस्तावित की गई थी।<ref>{{cite conference |title =सिंटेक्स-निर्देशित संश्लेषण|last1 = Alur |first1 = Rajeev| last2 = al.| first2 = et| date = 2013| publisher = IEEE| book-title = Proceedings of Formal Methods in Computer-Aided Design| pages = 8}}</ref> 2014 के बाद से एक प्रतिस्पर्धी कार्यक्रम, सिंटैक्स-गाइडेड सिंथेसिस प्रतियोगिता या SyGuS-Comp में प्रोग्राम सिंथेसिस के लिए विभिन्न एल्गोरिदम की तुलना करते हुए एक वार्षिक प्रोग्राम सिंथेसिस प्रतियोगिता हुई है।<ref>[https://sygus.org/ SyGuS-Comp (Syntax-Guided Synthesis Competition)]</ref> फिर भी, उपलब्ध एल्गोरिदम केवल छोटे प्रोग्रामों को संश्लेषित करने में सक्षम हैं।
+वीं सदी की शुरुआत में [[औपचारिक सत्यापन]] समुदाय और संबंधित क्षेत्रों में कार्यक्रम संश्लेषण के विचार में व्यावहारिक रुचि में वृद्धि देखी गई है। अरमांडो सोलर-लेज़ामा ने दिखाया कि [[ बूलियन तर्क ]] में कार्यक्रमसंश्लेषण समस्याओं को एनकोड करना संभव है और [[बूलियन संतुष्टि समस्या]] के लिए एल्गोरिदम का उपयोग स्वचालित रूप से कार्यक्रमखोजने के लिए किया जाता है।<ref>{{cite thesis |last=Solar-Lezama |first=Armando |date=2008 |title=स्केचिंग द्वारा प्रोग्राम संश्लेषण|type=Ph.D. |publisher=University of California, Berkeley |url=https://people.csail.mit.edu/asolar/papers/thesis.pdf}}</ref> 2013 में, [[UPenn]], UC बर्कले और [[MIT]] के शोधकर्ताओं द्वारा कार्यक्रम संश्लेषण समस्याओं के लिए एक एकीकृत रूपरेखा प्रस्तावित की गई थी।<ref>{{cite conference |title =सिंटेक्स-निर्देशित संश्लेषण|last1 = Alur |first1 = Rajeev| last2 = al.| first2 = et| date = 2013| publisher = IEEE| book-title = Proceedings of Formal Methods in Computer-Aided Design| pages = 8}}</ref> 2014 के बाद से एक प्रतिस्पर्धी कार्यक्रम, सिंटैक्स-गाइडेड संश्लेषण प्रतियोगिता या SyGuS-Comp में कार्यक्रमसंश्लेषण के लिए विभिन्न एल्गोरिदम की तुलना करते हुए एक वार्षिक कार्यक्रमसंश्लेषण प्रतियोगिता हुई है।<ref>[https://sygus.org/ SyGuS-Comp (Syntax-Guided Synthesis Competition)]</ref> फिर भी, उपलब्ध एल्गोरिदम केवल छोटे प्रोग्रामों को संश्लेषित करने में सक्षम हैं।
 == मन्ना और वाल्डिंगर की रूपरेखा ==
@@ Line 38: / Line 38: @@
 * सुगठित सूत्र # विधेय तर्क जो पहले से ही स्थापित हो चुका है, जिसमें स्वयंसिद्ध और पूर्व शर्त शामिल हैं, (अभिकथन)
 * फॉर्मूले अभी भी साबित होने बाकी हैं, पोस्टकंडिशन सहित, (लक्ष्य),<ref group="note">The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of [[proof by contradiction]], a Goal <math>F</math> is equivalent to an assertion <math> \lnot F</math>.</ref>
-* टर्म (तर्क) एक वैध आउटपुट वैल्यू ( प्रोग्राम ) को दर्शाता है<ref group="note">When <math>F</math> and <math>s</math> is the Goal formula and the Program term in a line, respectively, then in all cases where <math>F</math> holds, <math>s</math> is a valid output of the program to be synthesized. This [[invariant (computer science)|invariant]] is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.</ref>
+* टर्म (तर्क) एक वैध आउटपुट वैल्यू ( कार्यक्रम) को दर्शाता है<ref group="note">When <math>F</math> and <math>s</math> is the Goal formula and the Program term in a line, respectively, then in all cases where <math>F</math> holds, <math>s</math> is a valid output of the program to be synthesized. This [[invariant (computer science)|invariant]] is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.</ref>
 * वर्तमान लाइन के लिए एक औचित्य (उत्पत्ति)
 प्रारंभ में, पृष्ठभूमि ज्ञान, पूर्व-शर्तें और पश्च-शर्तें तालिका में दर्ज की जाती हैं। उसके बाद, उपयुक्त प्रूफ नियम मैन्युअल रूप से लागू किए जाते हैं। ढांचे को मध्यवर्ती सूत्रों की मानव पठनीयता को बढ़ाने के लिए डिज़ाइन किया गया है: [[संकल्प (तर्क)]] के विपरीत, इसे [[क्लॉसल सामान्य रूप]] की आवश्यकता नहीं होती है, लेकिन मनमाना संरचना के सूत्रों के साथ तर्क करने की अनुमति देता है और किसी भी जंक्शनर्स ([[गैर-खंड संकल्प]]) को शामिल करता है। प्रमाण कब पूरा होता है <math>\it true</math> लक्ष्य कॉलम में प्राप्त किया गया है, या, समकक्ष, <math>\it false</math> अभिकथन कॉलम में। इस दृष्टिकोण से प्राप्त कार्यक्रम से शुरू होने वाले विनिर्देश सूत्र को पूरा करने की गारंटी है; इस अर्थ में वे निर्माण द्वारा सही हैं।<ref>See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.</ref> केवल एक न्यूनतावादी, फिर भी [[ट्यूरिंग-पूर्ण]],<ref>{{cite techreport |last1=Boyer |first1=Robert S. |last2=Moore |first2=J. Strother |title=शुद्ध लिस्प की ट्यूरिंग पूर्णता का एक यांत्रिक प्रमाण|number=37 |institution=Institute for Computing Science, University of Texas at Austin |date=May 1983 |url=http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |format=PDF |url-status=live |archive-date=22 September 2017 |archive-url=https://web.archive.org/web/20170922044624/http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf |df=dmy-all }}</ref> [[विशुद्ध रूप से कार्यात्मक प्रोग्रामिंग भाषा]], जिसमें सशर्त, पुनरावर्तन और अंकगणित और अन्य ऑपरेटर शामिल हैं<ref group="note">Only the conditional operator ([[?:]]) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of <math>=</math> and <math>\leq</math> that are actually needed in the proof have been axiomatized, in line 1 to 3.</ref> समर्थित है।
@@ Line 48: / Line 48: @@
 *नॉन-क्लॉज़ल रेज़ोल्यूशन (तर्क) (तालिका देखें)।
 : उदाहरण के लिए, अभिकथन सूत्रों को हल करके पंक्ति 55 प्राप्त की जाती है <math>E</math> 51 से और <math>F</math> 52 से जो दोनों कुछ सामान्य उपसूत्र साझा करते हैं <math>p</math>. विलायक के विघटन के रूप में बनता है <math>E</math>, साथ <math>p</math> द्वारा प्रतिस्थापित <math>\it true</math>, और <math>F</math>, साथ <math>p</math> द्वारा प्रतिस्थापित <math>\it false</math>. यह विलायक तार्किक रूप से के संयोजन से अनुसरण करता है <math>E</math> और <math>F</math>. आम तौर पर अधिक, <math>E</math> और <math>F</math> केवल दो अविवेकी उपसूत्रों की आवश्यकता है <math>p_1</math> और <math>p_2</math>, क्रमश; उनके विलायक तब से बनते हैं <math>E \theta</math> और <math>F \theta</math> पहले की तरह, कहाँ <math>\theta</math> का सबसे सामान्य एकीकरणकर्ता है <math>p_1</math> और <math>p_2</math>. यह नियम पहले क्रम के तर्क में संकल्प (तर्क) #संकल्प का सामान्यीकरण करता है।<ref>Manna, Waldinger (1980), p.99</ref>
-:पैरेंट फ़ार्मुलों की प्रोग्राम शर्तों को संयोजित किया जाता है, जैसा कि पंक्ति 58 में दिखाया गया है ताकि रिज़ॉल्वेंट का आउटपुट तैयार किया जा सके। सामान्य मामले में, <math>\theta</math> बाद पर भी लागू होता है। सबफॉर्मूला के बाद से <math>p</math> आउटपुट में दिखाई देता है, गणना योग्य गुणों के अनुरूप केवल उप सूत्रों पर हल करने के लिए देखभाल की जानी चाहिए।
+:पैरेंट फ़ार्मुलों की कार्यक्रमशर्तों को संयोजित किया जाता है, जैसा कि पंक्ति 58 में दिखाया गया है ताकि रिज़ॉल्वेंट का आउटपुट तैयार किया जा सके। सामान्य मामले में, <math>\theta</math> बाद पर भी लागू होता है। सबफॉर्मूला के बाद से <math>p</math> आउटपुट में दिखाई देता है, गणना योग्य गुणों के अनुरूप केवल उप सूत्रों पर हल करने के लिए देखभाल की जानी चाहिए।
 * तार्किक परिवर्तन।
 :उदाहरण के लिए, <math>E \land (F \lor G)</math> में परिवर्तित किया जा सकता है <math>(E \land F) \lor (E \land G)</math>) अभिकथन के साथ-साथ लक्ष्यों में भी, क्योंकि दोनों समतुल्य हैं।
@@ Line 110: / Line 110: @@
 इसी तरह, लाइन 14 से लाइन 15 और फिर लाइन 16 रेजोल्यूशन से मिलती है। साथ ही, दूसरा मामला, <math>x \leq M \land y \leq M \land y = M</math> लाइन 13 में, इसी तरह से संभाला जाता है, अंत में लाइन 18 की उपज होती है।
-अंतिम चरण में, दोनों स्थितियाँ (यानी पंक्तियाँ 16 और 18) जुड़ जाती हैं, पंक्ति 58 से संकल्प नियम का उपयोग करते हुए; उस नियम को लागू करने के लिए प्रारंभिक चरण 15→16 की आवश्यकता थी। सहज रूप से, लाइन 18 को मामले की तरह पढ़ा जा सकता है <math>x \leq y</math>, उत्पादन <math>y</math> मान्य है (मूल विनिर्देशन के संबंध में), जबकि पंक्ति 15 कहती है case <math>y \leq x</math>, उत्पादन <math>x</math> यह सही है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं।<ref group="note">Axiom 3 was needed for that; in fact, if <math>\leq</math> wasn't a [[total order]], no maximum could be computed for uncomparable inputs <math>x,y</math>.</ref> चूँकि 16 और 18 दोनों पंक्तियाँ एक प्रोग्राम टर्म के साथ आती हैं, a ?: प्रोग्राम कॉलम में परिणाम देता है। लक्ष्य सूत्र के बाद से <math>\textit{true}</math> व्युत्पन्न किया गया है, प्रमाण किया गया है, और का कार्यक्रम स्तंभ<math>\textit{true}</math>लाइन में कार्यक्रम शामिल है।
+अंतिम चरण में, दोनों स्थितियाँ (यानी पंक्तियाँ 16 और 18) जुड़ जाती हैं, पंक्ति 58 से संकल्प नियम का उपयोग करते हुए; उस नियम को लागू करने के लिए प्रारंभिक चरण 15→16 की आवश्यकता थी। सहज रूप से, लाइन 18 को मामले की तरह पढ़ा जा सकता है <math>x \leq y</math>, उत्पादन <math>y</math> मान्य है (मूल विनिर्देशन के संबंध में), जबकि पंक्ति 15 कहती है case <math>y \leq x</math>, उत्पादन <math>x</math> यह सही है; चरण 15→16 ने स्थापित किया कि दोनों मामले 16 और 18 पूरक हैं।<ref group="note">Axiom 3 was needed for that; in fact, if <math>\leq</math> wasn't a [[total order]], no maximum could be computed for uncomparable inputs <math>x,y</math>.</ref> चूँकि 16 और 18 दोनों पंक्तियाँ एक कार्यक्रमटर्म के साथ आती हैं, a ?: कार्यक्रमकॉलम में परिणाम देता है। लक्ष्य सूत्र के बाद से <math>\textit{true}</math> व्युत्पन्न किया गया है, प्रमाण किया गया है, और का कार्यक्रम स्तंभ<math>\textit{true}</math>लाइन में कार्यक्रम शामिल है।
 == यह भी देखें ==

Difference between revisions of "प्रोग्राम सिंथेसिस"

Revision as of 22:19, 14 March 2023

Contents