Sintesi del programma - Program synthesis

In informatica , la sintesi del programma è il compito di costruire un programma che soddisfi in modo dimostrabile una data specifica formale di alto livello . Contrariamente alla verifica del programma, il programma deve essere costruito piuttosto che dato; tuttavia, entrambi i campi fanno uso di tecniche di prova formale ed entrambi comprendono approcci con diversi gradi di automazione. Contrariamente alle tecniche di programmazione automatica , le specifiche nella sintesi del programma sono solitamente affermazioni non algoritmiche in un calcolo logico appropriato .

Origine

Durante il Summer Institute of Symbolic Logic della Cornell University nel 1957, Alonzo Church definì il problema di sintetizzare un circuito a partire da requisiti matematici. Anche se il lavoro si riferisce solo ai circuiti e non ai programmi, il lavoro è considerato una delle prime descrizioni della sintesi del programma e alcuni ricercatori si riferiscono alla sintesi del programma come "Problema della Chiesa". Negli anni '60, un'idea simile per un "programmatore automatico" è stata esplorata dai ricercatori nell'intelligenza artificiale.

Da allora, varie comunità di ricerca hanno considerato il problema della sintesi dei programmi. Opere degne di nota includono l'approccio teorico degli automi del 1969 di Büchi e Landweber e le opere di Manna e Waldinger (c. 1980). Lo sviluppo di moderni linguaggi di programmazione di alto livello può essere inteso anche come una forma di sintesi di programmi.

Sviluppi del 21° secolo

L'inizio del 21° secolo ha visto un'ondata di interesse pratico per l'idea di sintesi del programma nella comunità della verifica formale e nei campi correlati. Armando Solar-Lezama ha mostrato che è possibile codificare problemi di sintesi di programmi in logica booleana e utilizzare algoritmi per il problema di soddisfacibilità booleana per trovare automaticamente i programmi. Nel 2013, i ricercatori di UPenn , UC Berkeley e MIT hanno proposto un quadro unificato per i problemi di sintesi dei programmi . Dal 2014 si tiene una competizione annuale di sintesi del programma che confronta i diversi algoritmi per la sintesi del programma in un evento competitivo, la Syntax-Guided Synthesis Competition o SyGuS-Comp. Tuttavia, gli algoritmi disponibili sono in grado di sintetizzare solo piccoli programmi.

Il quadro di Manna e Waldinger

Regole di risoluzione non clausole (sostituzioni unificanti non mostrate)

Nr	asserzioni	Obiettivi	Programma	Origine
51	${\displaystyle E[p]}$
52	${\displaystyle F[p]}$
53		${\displaystyle G[p]}$	S
54		${\displaystyle H[p]}$	T
55	${\displaystyle E[{\text{true}}]\lor F[{\text{false}}]}$			Risolvi(51,52)
56		${\displaystyle \lnot F[{\text{true}}]\land G[{\text{false}}]}$	S	Risolvi(52,53)
57		${\displaystyle \lnot F[{\text{false}}]\land G[{\text{true}}]}$	S	Risolvi(53,52)
58		${\displaystyle G[{\text{true}}]\land H[{\text{false}}]}$	p ? s : t	Risolvi(53,54)

Il framework di Manna e Waldinger , pubblicato nel 1980, parte da una formula di specifica del primo ordine data dall'utente . Per quella formula si costruisce una dimostrazione, sintetizzando così anche un programma funzionale da sostituzioni unificanti .

Il framework è presentato in un layout di tabella, le colonne contenenti:

• Un numero di riga ("Nr") a scopo di riferimento
• Formule già stabilite, inclusi assiomi e precondizioni, ("Asserzioni")
• Formule ancora da provare, comprese le postcondizioni, ("Obiettivi"),
• Termini che indicano un valore di output valido ("Programma")
• Una giustificazione per la riga corrente ("Origine")

Inizialmente, nella tabella vengono inserite le conoscenze di base, le pre-condizioni e le post-condizioni. Successivamente, vengono applicate manualmente le regole di prova appropriate. Il framework è stato progettato per migliorare la leggibilità umana delle formule intermedie: contrariamente alla risoluzione classica , non richiede la forma normale claustrale , ma consente di ragionare con formule di struttura arbitraria e contenenti eventuali giuntori (" risoluzione non claustrale "). La dimostrazione è completa quando è stata derivata nella colonna Obiettivi o, equivalentemente, nella colonna Asserzioni . I programmi ottenuti con questo approccio sono garantiti per soddisfare la formula di specifica da cui si è partiti; in questo senso sono corretti per costruzione . È supportato solo un linguaggio di programmazione minimalista, ma completo di Turing , puramente funzionale , composto da condizionale, ricorsione, aritmetica e altri operatori. I casi di studio eseguiti all'interno di questa struttura hanno sintetizzato algoritmi per calcolare, ad esempio , divisione , resto , radice quadrata , unificazione dei termini , risposte a query di database relazionali e diversi algoritmi di ordinamento . ${\displaystyle {\it {vero}}}$${\displaystyle {\it {false}}}$

Regole di prova

Le regole di prova includono:

• Risoluzione non claustrale (vedi tabella).

Ad esempio, la riga 55 si ottiene risolvendo le formule di asserzione da 51 e da 52 che condividono entrambe una sottoformula comune . Il risolvente si forma come la disgiunzione di , con sostituito da e , con sostituito da . Questo risolvente segue logicamente dalla congiunzione di e . Più in generale, e devono avere solo due sottoformule unificabili e , rispettivamente; il loro risolvente è quindi formato da e come prima, dove è l' unificatore più generale di e . Questa regola generalizza la risoluzione delle clausole .${\displaystyle E}$${\displaystyle F}$${\displaystyle p}$${\displaystyle E}$${\displaystyle p}$${\displaystyle {\it {vero}}}$${\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}}$

I termini del programma delle formule padre vengono combinati come mostrato nella riga 58 per formare l'output del risolvente. Nel caso generale, si applica anche a quest'ultimo. Poiché la sottoformula compare nell'output, occorre prestare attenzione a risolvere solo su sottoformule corrispondenti a proprietà calcolabili .${\displaystyle \theta}$${\displaystyle p}$

• Trasformazioni logiche.

Ad esempio, può essere trasformato in ) in Asserzioni e in Obiettivi, poiché entrambi sono equivalenti.${\displaystyle E\land (F\lor G)}$${\displaystyle (E\land F)\lor (E\land G)}$

• Scissione di asserzioni congiuntive e di obiettivi disgiuntivi.

Un esempio è mostrato nelle righe da 11 a 13 dell'esempio del giocattolo di seguito.

• Induzione strutturale .

Questa regola consente la sintesi di funzioni ricorsive . Per una data pre- e postcondizione "Dato tale che , trova tale che ", e un appropriato ordinamento del dominio di , dato dall'utente , è sempre corretto aggiungere un'asserzione " ". La risoluzione con questa asserzione può introdurre una chiamata ricorsiva a nel termine Program.${\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'))}$${\displaystyle f}$

Un esempio è dato in Manna, Waldinger (1980), p.108-111, dove viene sintetizzato un algoritmo per calcolare quoziente e resto di due dati interi, usando l'ordine definito da (p.110).${\displaystyle (n',d')\prec (n,d)}$${\displaystyle 0\leq n'<n}$

Murray ha mostrato che queste regole sono complete per la logica del primo ordine . Nel 1986, Manna e Waldinger aggiunsero regole generalizzate di risoluzione elettronica e paramodulazione per gestire anche l'uguaglianza; in seguito, queste regole si sono rivelate incomplete (ma comunque valide ).

Esempio

Esempio di sintesi della massima funzione

Nr	asserzioni	Obiettivi	Programma	Origine
1	${\displaystyle A=A}$			Assioma
2	${\displaystyle A\leq A}$			Assioma
3	${\displaystyle A\leq B\lor B\leq A}$			Assioma
10		${\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}$	m	Specifiche
11		${\displaystyle (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		${\displaystyle x\leq M\land y\leq M\land x=M}$	m	Spalato(11)
13		${\displaystyle x\leq M\land y\leq M\land y=M}$	m	Spalato(11)
14		${\displaystyle x\leq x\land y\leq x}$	X	Risolvi(12,1)
15		${\displaystyle y\leq x}$	X	Risolvi(14,2)
16		${\displaystyle \lnot (x\leq y)}$	X	Risolvi(15,3)
17		${\displaystyle x\leq y\land y\leq y}$	sì	Risolvi(13,1)
18		${\displaystyle x\leq y}$	sì	Risolvi(17,2)
19		${\displaystyle {\textit {vero}}}$	x<y ? y : x	Risolvi(18,16)

Come esempio giocattolo, un programma funzionale per calcolare il massimo di due numeri e può essere derivato come segue. ${\displaystyle M}$${\displaystyle x}$${\displaystyle y}$

Partendo dalla descrizione del requisito " Il massimo è maggiore o uguale a qualsiasi numero dato, ed è uno dei numeri dati ", si ottiene la formula del primo ordine come sua traduzione formale. Questa formula è da dimostrare. Con la Skolemization inversa si ottiene la specifica nella riga 10, una lettera maiuscola e minuscola che denota rispettivamente una variabile e una costante di Skolem . ${\ Displaystyle \ forall X \ forall Y \ esiste M: X \ leq M \ land Y \ leq M \ land (X = M \ lor Y = M)}$

Dopo aver applicato una regola di trasformazione per la legge distributiva nella riga 11, l'obiettivo della dimostrazione è una disgiunzione e quindi può essere suddiviso in due casi, vale a dire. righe 12 e 13.

Passando al primo caso, la risoluzione della riga 12 con l'assioma della riga 1 porta all'istanziazione della variabile di programma nella riga 14. Intuitivamente, l'ultimo congiuntivo della riga 12 prescrive il valore che deve assumere in questo caso. Formalmente, alle righe 12 e 1 si applica la regola di risoluzione non claustrale mostrata al rigo 57 di cui sopra, con ${\displaystyle M}$${\displaystyle M}$

• p essendo l'istanza comune x=x di A=A e x=M , ottenuta unificando sintatticamentequeste ultime formule,
• essendo F[ p ] vero ∧ x=x , ottenuto dallariga 1 istanziata (opportunamente imbottita per renderevisibileil contesto F[⋅] attorno a p ), e
• G[ p ] essendo x ≤ x ∧ y ≤ x ∧ x = x , ottenuto dalla riga istanziata 12,

ottenendo vero ∧ falso ) ∧ ( x ≤ x ∧ y ≤ x ∧ vero , che semplifica a . ${\displaystyle \lnot (}$${\displaystyle )}$${\displaystyle x\leq x\land y\leq x}$

In modo simile, la riga 14 fornisce la riga 15 e quindi la riga 16 per risoluzione. Inoltre, il secondo caso, nella riga 13, viene gestito in modo simile, ottenendo infine la riga 18. ${\displaystyle x\leq M\land y\leq M\land y=M}$

In un'ultima fase vengono uniti entrambi i casi (cioè le righe 16 e 18), utilizzando la regola di risoluzione della riga 58; per rendere applicabile tale norma era necessaria la fase preparatoria 15→16. Intuitivamente, la riga 18 potrebbe essere letta come "nel caso in cui l'output sia valido (rispetto alla specifica originale), mentre la riga 15 dice "nel caso in cui l'output sia valido; il passo 15→16 ha stabilito che entrambi i casi 16 e 18 sono complementari. Poiché sia ​​la riga 16 che la riga 18 vengono fornite con un termine di programma, un'espressione condizionale risulta nella colonna del programma. Poiché la formula dell'obiettivo è stata derivata, la dimostrazione è eseguita e la colonna programma della riga " " contiene il programma. ${\displaystyle x\leq y}$${\displaystyle y}$${\displaystyle y\leq x}$${\displaystyle x}$${\displaystyle {\textit {vero}}}$${\displaystyle {\textit {vero}}}$

Guarda anche

• Programmazione induttiva
• metaprogrammazione
• Derivazione del programma
• Programmazione in linguaggio naturale
• Sintesi reattiva

Appunti

Riferimenti

• Zohar Manna, Richard Waldinger (1975). "Conoscenza e ragionamento nella sintesi del programma". Intelligenza Artificiale . 6 (2): 175-208. doi : 10.1016/0004-3702(75)90008-9 .