Cesko.wiki Logické programování
Author
Albert FloresLogické programování je v širším významu použití matematické logiky jako prostředku pro programování. Jeho počátky můžeme vystopovat až k návrhu Johna McCarthyho advice taker (rádce) [1958]. V tomto návrhu slouží logika pro čistě deklarativní reprezentaci jazyka a dokazovač vět (theorem-prover) nebo generátor modelů (model-generator) se používá jako řešitel problémů (problem-solver). Řešení problému se tak dělí mezi programátora (ručí za správnost programu vyjádřené v logické formě) a dokazovač vět nebo generátor modelů (odpovídá za efektivní řešení problému).
Častěji se však logické programování chápe v užším smyslu, kdy se logika používá na deklarativní i procedurální reprezentaci jazyka. Vychází z faktu, že zpětně usuzující dokazovač vět (backwards reasoning theorem-prover) použitý na deklarativní větu ve tvaru implikace:
:B1 a … a Bn implies H
zachází s touto implikací jako s cíl redukující (goal-reduction) procedurou.
:ukaž/vyřeš H, ukaž/vyřeš B1 a … a Bn.
Programátor neručí pouze za správnost programu, ale i za jeho efektivitu. Často je pro dosažení efektivity nezbytné, aby se programátor seznámil se způsobem, jakým dokazovač vět řeší problém a uměl jej využívat. +more Tím, že logické programovaní používá program k řízení chování vykonavatele programu (program executor) se podobá tradičnímu imperativnímu programování. Od imperativních programů s pouze procedurální interpretací se však logické programy liší existencí deklarativní logické interpretace, která pomáhá zajistit jejich korektnost. Díky tomu, že jsou tyto programy deklarativní (tedy deklarují, co je vstupem a výstupem, a nezabývají se tím, jak výpočet probíhá), jsou na mnohem vyšší konceptuální úrovni než čistě imperativní programy, a jejich vykonavatelé, kteří jsou vlastně dokazovači vět, operují na konceptuálně vyšší úrovni než běžné překladače a interprety.
Historie
Logické programování v širším smyslu dalo vzniknout mnoha implementacím. Například systémy odpovídající na dotazy (question-answering systems) Fischera Blacka (1964), Jamese Slagla (1965) a Cordella Greena (1969) stvořené v duchu McCarthyho návrhu advice taker. +more Fosterův a Elcockův Absys (1969) byl pravděpodobně první jazyk explicitně vyvíjený jako výrazový programovací jazyk (assertional programming language).
Počátky logického programování v užším slova smyslu můžeme vystopovat do konce šedesátých a počátku sedmdesátých let, kdy se vedly debaty o deklarativní nebo procedurální reprezentaci znalostí v umělé inteligenci. Obhájci deklarativního přístupu působili především na Stanfordově univerzitě (John McCarth, Bertram Raphael a Cordell Green) a Edinburské univerzitě ( +more_Alan_Robinson'>Alane Robinsonem, Patrick J. Hayes a Robert Kowalski). Obhájci procedurální reprezentace se soustředili zejména okolo MIT, pod vedením Marvina Minskyho a Seymoura Paperta.
V roce 1960 Carl Hewitt v MIT vyvinul jazyk Planner. I když byl Planner první jazyk založený na logice v užším chápaní, byl silně ovlivněn procedurálním paradigmatem. +more Nejvýznamnější implementací Planneru byla jeho podmnožina s názvem Micro-Planner, vytvořená Gerry Sussmanem, Eugene Charniakem a Terry Winogradem. Micro-Planner byl použit k implementaci Winogradova programu pro porozumění přirozenému jazyku (SHRDLU), což byl důležitý mezník té doby. Planner byl vybaven vzorově řízeným (pattern-directed) vyvoláváním procedurálních plánů z výrazů i cílů. Protože systémy dostupné v době vývoje byly limitovány velmi malou pamětí, používal Planner backtraking řídící strukturu a bylo možné ukládat pouze jednu výpočetní cestu. Z Planeru vzešly další programovací jazyky, například QA-4, Popler, Conniver, QLISP a paralelní Ether.
Hayes a Kowalski z Edinburské univerzity se pokusili spojit logicky založený deklarativní přístup reprezentace znalostí s procedurálním přístupem Planneru. Hayes (1973) vyvinul jazyk Golux pro řešení rovnic (equational language), ve kterém je možné získat různé procedury změnou chování dokazovače vět. +more Kowalski ukázal jak SL-rezoluce zachází s implikacemi jako s cíl redukujícími (goal-reduction) procedurami. Kowalski spolupracoval s Colmerauerem z Marseille, který rozvinul tyto myšlenky v návrhu a implementaci programovacího jazyka Prolog. Z Prologu se vyvinulo mnoho dalších jazyků: ALF, Fril, Gödel, Mercury, Oz, Ciao, Visual Prolog, XSB, a λProlog. Stejně tak i množství paralelních logických programovacích jazyků, logických programovacích jazyků s omezujícími podmínkami a datalogů.
V roce 1997 udělila Asociace logického programování patnácti významným vědcům v oboru logického programování titul Zakladatel logického programování, aby ocenila jejich průkopnickou činnost v oboru. Mezi tyto vědce patří:
* [url=http://www. cs. +morekuleuven. ac. be/~maurice/]Maurice Bruynooghe[/url] , Belgie * [url=http://www. cs. brandeis. edu/~jc/]Jacques Cohen[/url], USA * Alain Colmerauer, Francie * Keith Clark, Velká Británie * [url=http://www. cs. sfu. ca/~veronica/index. html]Veronica Dahl[/url], Kanada / Argentina * [url=https://web. archive. org/web/20070407174144/http://csr. uvic. ca/~vanemden/index. html]Maarten van Emden[/url], Kanada * [url=https://web. archive. org/web/20071103234600/http://www. inria. fr/personnel/Herve. Gallaire. en. html]Herve Gallaire[/url], Francie * Robert Kowalski, Velká Británie * Jack Minker, USA * [url=https://web. archive. org/web/20070701222314/http://www. cis. upenn. edu/~pereira/]Fernando Pereira[/url], USA * [url=http://centria. di. fct. unl. pt/~lmp/]Luis Moniz Pereira[/url], Portugalsko * Ray Reiter, Canada * Alan Robinson, USA * [url=http://www. cs. bme. hu/~szeredi/english/index. html]Peter Szeredi[/url], Maďarsko * David H. D. Warren, Velká Británie.
Prolog
Jazyk Prolog byl vyvinut Alainem Colmerauerem v roce 1972. Vzešel ze spolupráce mezi Colmerauerem z University v Marseille a Robertem Kowalskim z Edinburské university. +more Colmerauer pracoval na porozumění přirozeného jazyka. Logiku používal pro reprezentaci sémantiky a rezoluci pro získávaní odpovědí na dotazy (question-answering). Během léta 1971, Colmerauer a Kowalski objevili, že klauzální logika může být použita k reprezentaci formální gramatiky a že rezoluční dokazovač vět (resolution theorem prover) může být využit pro parsování. Zjistili, že některé dokazovače vět jako například hyper rezoluce (hyper-resolution) se chovají jako bottom-up parsery a jiné třeba SL rezoluce (1971) se chovají jako top-down parsery.
Následující léto roku 1972 Kowalski opět za spolupráce s Colmerauerem, vytvořil procedurální interpretaci implikace. Tato duálně deklarativní/procedurální interpretace byla později formalizována v notaci Prologu:
:H :- B1, …, Bn.
která může být čtena a použita deklarativně i procedurálně. Bylo také jasné, že tyto klauzule mohou být omezeny pouze na definitní klauzule nebo Hornovské klauzule, kde
:H, B1, …, Bn
jsou všechno atomické predikáty logické rovnice a SL rezoluce může být zobecněna na LUSH nebo SLD rezoluci. Kowalskeho procedurální interpretace a LUSH byly popsány v jeho poznámkách v roce 1973 a publikovány následujícího roku.
Colmerauer s Philippem Rousselem použili tuto duální interpretaci jako základ pro Prolog, který byl implementován během léta a podzimu roku 1972. První program v Prologu byl rovněž napsán roku 1972 v Marseille a jednalo se o francouzský systém odpovídání na dotazy. +more Zásadním impulsem pro použití Prologu jako praktického programovacího jazyka bylo vytvoření překladače Davidem Warrenem v Edinburku roku 1977. Experimenty ukázaly, že Edinburský Prolog může výkonem soupeřit s jinými symbolickými programovacími jazyky, jako je Lisp. Edinburský Prolog se stal de facto standardem a silně ovlivnil znění standardu ISO pro Prolog.
Negace jako selhání
Micro-planner obsahoval konstrukci nazvanou "thot", která po aplikaci na výraz vracela "pravda", pouze když vyhodnocování výrazu selhalo. Ekvivalentní operátor je součástí všech moderních implementací prologu a byl nazýván negace jako selhání. +more Běžně se značí not(p), kde p je atom, jehož proměnně jsou vytvořeny v době, kdy je not(p) zavolán. Zastaralá, ale standardní syntax je \+ p. Literály negace jako selhání se mohou vyskytnout jako podmínka not(Bi) v těle programu klauzulí.
Logický status negace jako selhání zůstával dlouho nevyřešen. Až Keith Clark [1978] dokázal, že za určitých podmínek se jedná o korektní (a někdy úplnou) implementaci klasické negace s ohledem na vyplnitelnost (completion) programu. +more Vyplnitelnost se zhruba vyhodnocuje vzhledem k množině všech klauzulí, které mají stejný predikát na levé straně, řekněme:.
:H :- Body1. : … :H :- Bodyk.
jako definice predikátu
:H iff (Body1 or … or Bodyk)
kde "iff" znamená "tehdy a jen tehdy když". Stanovení vyplnitelnosti vyžaduje explicitní použití predikátu rovnosti a inkluzi množiny příslušných axiomů rovnosti. +more Naštěstí implementace negace jako selhání vyžaduje pouze "if" části definic bez axiomu rovnosti.
Pojem vyplnitelnosti je úzce spjat s McCarthyho vymezovací sémantikou pro výchozí usuzování (circumscription semantics for default reasoning) a hypotézou uzavřeného světa (closed world assumption).
Alternativou k sémantice vyplnitelnosti, může být negace jako selhání interpretována epistemicky jako v modelu stabilní sémantiky v programování množinou dotazů (answer set programming). V této interpretaci not(Bi) znamená doslovně, že Bi není známé nebo je neověřitelné. +more Epistemická interpretace má tu výhodu, že může být snadno zkombinovaná s klasickou negací, jako v případě "rozšířeného logické programování". Můžeme tak formalizovat tvrzení jako "opak nemůže být prokázán", kde "opak" je klasická negace a "nemůže být prokázán" je epistemická interpretace negace jako selhání.
Řešení problému
Ve zjednodušeném případě, kdy pracujeme s výrokovou logikou a logický program ani hlavní cíl atomický neobsahují proměnné, zpětné usuzování (backward reasoning) určí logický a-nebo strom, který stanovuje prostor řešení cíle.
Hlavní cíl je vrchol stromu. Za předpokladu, že nějaký uzel ve stromu odpovídá hlavě klauzule, pak existuje množina potomků tohoto uzlu, která odpovídá mezi-cílům v těle této klauzuli. +more Potomci uzlu jsou spojení logickou spojkou a. Alternativní množina potomků odpovídající alternativní cestě řešení uzlu je spojeni pomocí logického nebo.
K prohledání prostoru řešení mohou být použity různé strategie. Prolog využívá sekvenční, LIFO a backtracking strategii, při které najednou zpracovává pouze jeden mezi-cíl a alternativní cestu. +more K hledaní řešení je možné využívat i jiné strategie jako paralelní vyhledávání, inteligentní backtracking anebo hledaní metodou nejlepší-první (best-first).
V více obecném případě, kdy mezi-cíle sdílejí proměnné, mohou být použity další strategie. Například výběr mezi-cíle, který je nejvíce rozvinut nebo je rozvinut do té míry, že může být použita pouze jedna procedura. +more Tyto strategie se využívají například v paralelním logickém programování.
Fakt existence několika cest jak vykovávat logický program je vyjádřen rovnicí:
Algoritmus = Logika + Řízení
kde Logika představuje logický program a Řízení různé strategie dokazování vět.
Reprezentace znalostí
Skutečnost, že Hornovské klauzule mohou nabývat procedurální interpretace a zároveň že cíl redukující procedura může být chápána jako Hornovské klauzule spojené se zpětným usuzováním, znamená, že logický program kombinuje deklarativní a procedurální reprezentaci znalostí. Inkluze negace jako selhání znamená, že logické programovaní je druh nemonotonické logiky.
Navzdory své jednoduchosti (v porovnání s klasickou logikou) se kombinace Hornovských klauzulí a negace jako selhání prokázala být překvapivě expresivní. Například bylo ukázáno, že s několika rozšířeními poměrně přirozeně odpovídá poloformálnímu jazyku legislativy. +more Je to také přirozený jazyk pro vyjadřování zákona příčiny a následků v rámci běžného uvažování, podobně jako v situačním a událostním kalkulu.
Paralelní logické programování
Keith Clark, Steve Gregory, Vijay Saraswat, Udi Shapiro, Kazunori Ueda a další vyvinuli rodinu paralelních systémů zasílání zpráv podobnou Prologu používající unifikaci sdílených proměnných a proudů datových struktur pro zprávy. Snahou bylo postavit tyto systémy na matematické logice a posloužily jako základ pro Japonský projekt počítače páté generace (ICOT).
Logické programování vyšších řádů
Řada výzkumů rozšířila logické programování o vlastnosti programování vyšších řádů odvozených z logiky vyšších řádů, jakými jsou například predikátové proměnné. Mezi tyto jazyky patří rozšíření Prologu HiLog a λProlog.
Lineární logické programování
Základní logické programování ve spojení s lineární logikou vyústilo v návrh logických programovacích jazyků, které mají o poznání silnější vyjadřovací prostředky než jazyky založené na klasické logice. Programy sestavené z Hornovských klauzulí reprezentují pouze změnu stavu způsobenou změnou v argumentech vzhledem k predikátům. +more V lineárním logickém programování je možné použít ambientní lineární logiku pro podporu změny stavu. Mezi některé z raných návrhů logických programovacích jazyků založených na lineární logice patří: LO [Andreoli & Pareschi, 1991], Lolli [Hodas & Miller, 1994], ACL [Kobayashi & Yonezawa, 1994] a Forum [Miller, 1996]. Forum nabízí interpretaci veškeré lineární logiky zaměřenou na cíl (goal-direct).
Externí odkazy
[url=https://web. archive. +moreorg/web/20090521031634/http://axpsu. fpf. slu. cz/~vav10ui/obsahy/log2/skriptalast/logika. pdf]Logika a logické programování[/url] (skripta Slezské univerzity v Opavě) * [url=https://web. archive. org/web/20070613174812/http://web. ff. cuni. cz/~pelis/CRL. pdf]Teorie racionálního usuzování[/url] (skripta Karlovy univerzity v Praze).