Storia della programmazione logica anni 60: le origini anni 70: Kowalski e Prolog anni 80: il boom anni 90: i raffinamenti anni 00: tutto passa di moda, ma le idee giuste restano Gli eventi scientifici fondamentali 1965: Resolution Method, Alan Robinson, CACM 1969: Cordell Green, Hewitt (Planner), IJCAI 1971: SL-Resolution, Kowalski&Kuehner, AI 1972: interprete Prolog, Colmerauer&Roussel con Kowalski 1974: “Logic as a programming language” Kowalski, IFIP 1976: semantica, Kowalski&vanEmden, JACM 1977: compilatore Edinburgh Prolog (Warren) 1978: Negation as Failure, Clark 1987: CLP, Jaffar&Lassez, POPL La comunità si assesta 1982:First International Conference on Logic Programming (ICLP), Marseille 1984: Lloyd, Foundations of Logic Programming, Springer 1984: Journal of Logic Programming (JLP), Alan Robinson (poi TPLP) 1986: Sterling & Shapiro, The art of Prolog, MIT Press 1986: Association for Logic Programming (ALP) 1987: GULP I progetti ed i consorzi 1982:Fifth Generation Computer Systems, ICOT 1982: MCC (Microelectronics and Computer Technology Corporation), Austin (NSA, CIA) ~1985: Compulog 1 e altri progetti ESPRIT ~1985: European Computer-Industry Research Centre (ECRC), Monaco ~1995: Compulog NoE Theorem proving via Resolution insieme di fbf (logica del prim’ordine) --> clausole skolemizzazione, eliminazione quantificatori universali equivalente per l’insoddisfacibilità dimostrazioni per assurdo la formula da provare si nega si tenta di derivare la contraddizione (clausola vuota) la risoluzione di Robinson è una regola corretta e completa insoddisfacibilità <--> derivazione clausola vuota La Risoluzione di Robinson A1 V B1 V … V Bn ~A2 V C1 V … V Cm senza variabili, se A1 = A2 il risolvente è B1 V … V BnV C1 V … V Cm con variabili, bisogna prima applicare alle clausole la sostituzione unificante più generale (mgu) di A1 e A2 l’mgu è calcolato dall’algoritmo di unificazione (Robinson) Nessuno è perfetto l’uso dell’unificazione riduce drasticamente il numero di clausole inferite da una coppia di clausole derivo risolventi solo istanziandole con l’mgu ogni risolvente sta per un numero (possibilmente infinito) di sue istanze comunque esplosione combinatoria ricerca di strategie (possibilmente complete) la risoluzione lineare è una specie di riscrittura nondeterministica (purtroppo incompleta) M.I.T. contro Stanford l’M.I.T. odia la logica ed il theorem proving con il metodo di risoluzione e sostiene la filosofia della rappresentazione procedurale della conoscenza (micro)PLANNER (Hewitt): un vero linguaggio dotato di interprete non è logica, ma sciaguratamente risulterà molto simile alle clausole Horn definite (la programmazione logica, ormai dietro l’angolo) Stanford ama la logica e la dimostrazione di teoremi il sistema di question answering di Cordell Green: usa il metodo di Risoluzione per calcolare le risposte ma certe risposte sono difficili da calcolare (proprio quelle che risulteranno essere fuori dal potere espressivo della programmazione logica) Vince Edinburgh Bob Kowalski identifica un sottoinsieme (le clausole Horn definite, clausole con al più un letterale positivo), per cui la risoluzione lineare è completa una dimostrazione è una derivazione della clausola vuota (terminazione!) attraverso una riscrittura nondeterministica (risoluzione SLD, semantica operazionale) i vari tipi di clausole hanno una naturale interpretazione procedurale definizione e chiamata di sottoprogrammi, passaggio di parametri sofisticato (unificazione, non distinzione tra input e output, strutture dati parziali) i sottoprogrammi sono nondeterministici un programma logico ha un modello minimo di Herbrand (unico, la semantica!) tale modello può essere costruito con un calcolo di punto fisso (bottomup) nello stile della semantica denotazionale Un programma logico sort(X,Y) :- sorted(Y), perm(X, Y). sorted([]). sorted([X]). sorted([X, Y|Z]) :- X <= Y, sorted(Y|Z). perm([], []). perm(X|Y, U|V) :- delete(U, X|Y, Z), perm(Z, V). delete(X, X|Y, Y). delete(X, Y|Z, Y|W) :- delete(X, Z, W). un goal ?- sort([1, 0, 2], X). Vince anche Marsiglia Kowalski visita Alain Colmerauer a Marsiglia interessato alla formalizzazione del linguaggio naturale Kowalski non ha ancora capito proprio tutto, ma Colmerauer (con l’aiuto di Roussel) implementa il linguaggio che gli serve PROLOG = clausole Horn definite + un po’ di cose strane ma utilissime (assert, retract, !, primitive meta) + almeno un errore prolifico (l’unificazione senza occur check) Un capolavoro tecnologico: il compilatore Edinburgh-Prolog i meccanismi operazionali di Prolog (unificazione, nondeterminismo) offrono grandi margini di ottimizzazione David Warren (Edinburgo) progetta una macchina target per la compilazione, chiamata WAM (Warren Abstract Machine) dotata di pila, heap, garbage collector ricostruita dal punto di vista teorico con la valutazione parziale ed un compilatore molto astuto i programmi Prolog diventano anche efficienti! Tante belle implementazioni! altri compilatori, anche più sofisticati per esempio, SICSTUS-Prolog molta ricerca su analisi statica e ottimizzazioni banco di prova teorico e pratico dell’interpretazione astratta (Ciao-Prolog) molta ricerca sulle implementazioni parallele Non monotonic reasoning nelle applicazioni di intelligenza artificiale (e data base deduttivi), farebbe comodo poter usare la negazione nel corpo di una clausola si ricade nel caso generale e si perdono le proprietà delle clausole Horn definite in Prolog, c’è la negazione come fallimento finito Clark la giustifica dal punto di vista logico con il completamento altre negazioni (negazione costruttiva) altre semantiche (modelli stabili, modelli well-founded) una grande comunità di non-monotonic reasoning con una propria autonomia Prolog con insiemi di equazioni perm([], []). perm(X|Y, U|V) :- delete(U, X|Y, Z), perm(Z, V). perm(X, Y) :- X = [], Y = []. perm(X, Y) :- X = X1|Y1, Y = U|V # delete(U, X, Z), (Z, V). perm l’unificazione è resa esplicita, specificando equazioni fra termini il calcolo accumula, risolve e restituisce insiemi di equazioni l’algoritmo di unificazione verifica la soddisfacibilità e genera la forma risolta Da Prolog a CLP rimpiazziamo gli insiemi di equazioni con altri “sistemi di vincoli” equazioni e disequazioni su termini equazioni su termini razionali (senza occur check!) vincoli su domini finiti numerici equazioni e disequazioni su numeri reali rimpiazziamo l’algoritmo di unificazione con un algoritmo che verifica la soddisfacibilità e genera una forma semplificata (normale, se possibile) ricicliamo algoritmi classici (per esempio, il simplesso) otteniamo potenti strumenti per formalizzare e risolvere problemi di tipo combinatorio su domini numerici Semantica la semantica è molto semplice con varie formulazioni alternative tra loro equivalenti in realtà, come sempre, si utilizzano semantiche diverse secondo le necessità ambiente ideale su cui studiare le relazioni fra semantiche (interpretazione astratta) le varie tecniche semantics-based analisi trasformazione ottimizzazione La groundness motivato dalla compilazione vogliamo sapere se una variabile verrà legata ad un termine ground semantica concreta deve modellare le risposte calcolate (non-ground) è utile una formulazione goal independent la S-semantica punto fisso tanti domini astratti per la groundness per studiarne la precisione relativa risultati generali per i raffinamenti di domini Basi di dati deduttive padre(haran, lot). padre(haran, milcah). padre(haran, yiscah). maschio(lot). genitore(X, Y) :- padre(X, Y). genitore(X, Y) :- madre(X, Y). figlio(X, Y) :- genitore(Y, X), maschio(X). estensione dei data base relazionali anche con update (assert, retract) interfacce tra Prolog e DBMS Datalog semantiche bottom-up sottoinsiemi con negazione (stratificazione) vincoli d’integrità Parallelismo, concorrenza, architetture parallelismo And e Or importante anche per possibili architetture linguaggi logici (o con vincoli) concorrenti semantica logica della sincronizzazione alla fine, normali calcoli per la concorrenza Metaprogrammazione come in LISP le clausole sono rappresentate come dati (termini) primitive meta per accedere, visitare e modificare i programmi metainterprete di Prolog in Prolog: tre clausole facilissimo definire via metainterpreti estensioni del linguaggio strumenti Uno splendido linguaggio di specifica eseguibile il formalismo delle clausole Horn definite coincide praticamente con il metalinguaggio della semantica operazionale (regole di transizione) relazioni nondeterminismo ed è eseguibile una specifica (di un linguaggio o di un sistema) data mediante regole di transizione è anche un prototipo funzionante l’applicazione industriale più diffusa di Prolog! l’essenza del dichiarativo vs. procedurale! Mille linguaggi logici l’essenza della programmazione logica calcolare = dimostrare è comune anche ad altri paradigmi programmazione funzionale si possono definire linguaggi logici a partire da logiche diverse logica lineare, interessante per la concorrenza Bibliografia fondamentale 1 John Alan Robinson, "A Machine-Oriented Logic Based on the Resolution Principle", Communications of the ACM, 5:23–41, 1965. Robert Kowalski, “Predicate Logic as a Programming Language”, Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569-574. R. Kowalski, M. Van Emden, “The Semantics of Predicate Logic as a Programming Language”, JACM, vol. 23, n. 4, Oct. 1976, p. 733-743. K. L. Clark, “Negation as failure”, Logic and Data Bases (eds. Gallaire & Minker) Plenum Press, New York, 293-322 pp, 1978. J. Jaffar, J.-L. Lassez: Constraint Logic Programming. POPL 1987: 111-119 Bibliografia fondamentale 2 J. W. Lloyd. “Foundations of Logic Programming” (2nd edition). Springer-Verlag 1987. L. Sterling & E. Shapiro. “The art of PROLOG, Second Edition: Advanced Programming Technologies”. MIT Press 1994.