Logické programování

Z Multimediaexpo.cz

Nemáte oprávnění „upravit tuto stránku“. Důvod:

Můžete si prohlédnout a zkopírovat zdrojový kód této stránky:

'''Logické programování''' je v širším významu použití [[matematická logika|matematické logiky]] jako prostředku pro [[programování]]. Jeho počátky můžeme vystopovat až k návrhu Johna McCarthse '''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: :<tt>B₁ a … a B_n implies H</tt> zachází s touto implikací jako s cíl redukující (goal-reduction) procedurou. :ukaž/vyřeš <tt>H</tt>, ukaž/vyřeš <tt>B₁</tt> a … a <tt>B_n</tt>. 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. Tím, že logické programovaní používá program k řízení chování vykonavatele programu (program executor) se podobá tradičnímu [[imperativní programování|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í programování|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 [[interpret (software)|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. 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á inteligence|umělé inteligenci]]. Obhájci deklarativního přístupu působili především na [[Stanford University|Stanfordské univerzitě]] ([[John McCarthy|John McCarth]], Bertram Raphael a Cordell Green) a [[University of Edinburgh|Edinburgské univerzitě]] ( [[J. Alan Robinson|Alane Robinsonem]], [[Patrick J. Hayes]] a [[Robert Kowalski]]). Obhájci procedurální reprezentace se soustředili zejména okolo [[Massachusetts Institute of Technology|MIT]], pod vedením [[Marvin Minsky|Marvina Minskyho]] a [[Seymour Papert|Seymoura Paperta]]. V roce [[1960]] [[Carl Hewitt]] v [[Massachusetts Institute of Technology|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 [[paradigma]]tem. Nejvýznamnější implementací [[Planner]]u byla jeho podmnožina s názvem Micro-Planner, vytvořená [[Gerald Jay Sussman|Gerry Sussmanem]], [[Eugene Charniak]]em a [[Terry Winograd]]em. 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 [[elektronická paměť|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. 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 (programming language)|ALF]], [[Fril]], [[Gödel (programming language)|Gödel]], [[Mercury programming language|Mercury]], [[Oz (programming language)|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|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ří: * [http://www.cs.kuleuven.ac.be/~maurice/ Maurice Bruynooghe], Belgie * [http://www.cs.brandeis.edu/~jc/ Jacques Cohen], USA * [[Alain Colmerauer]], Francie * [[Keith Clark]], Velká Británie * [http://www.cs.sfu.ca/~veronica/index.html Veronica Dahl], Kanada / Argentina * [http://csr.uvic.ca/~vanemden/index.html Maarten van Emden], Kanada * [http://www.inria.fr/personnel/Herve.Gallaire.en.html Herve Gallaire], Francie * [[Robert Kowalski]], Velká Británie * [[Jack Minker]], USA * [http://www.cis.upenn.edu/~pereira/ Fernando Pereira], USA * [http://centria.di.fct.unl.pt/~lmp/ Luis Moniz Pereira], Portugalsko * [[Ray Reiter]], Canada * [[J. Alan Robinson|Alan Robinson]], USA * [http://www.cs.bme.hu/~szeredi/english/index.html Peter Szeredi], Maďarsko * [[David H. D. Warren|David H.D. Warren]], Velká Británie == Prolog == {{hlavní článek|Prolog (programovací jazyk)}} Jazyk Prolog byl vyvinut [[Alain Colmerauer|Alainem Colmerauerem]] v roce [[1972]]. Vzešel ze spolupráce mezi Colmerauerem z Univerisity v Marseille a Robertem Kowalskim z Edinburské university. 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í gramatika|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: :<tt>H :- B₁, …, B_n.</tt> 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 :<tt>H</tt>, <tt>B₁</tt>, …, <tt>B_n</tt> 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. Zásadním impulsem pro použití Prologu jako praktického programovacího jazyka bylo vytvoření překladače Davidem Warrenem v [[Edinburk]]u 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 [[International Organization for Standardization|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í'''. 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 můžou vyskytnout jako podmínka not(B_i) 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. Vyplnitelnost se zhruba vyhodnocuje vzhledem k množině všech klauzulí, které mají stejný predikát na levé straně, řekněme: :<tt>H :- Body₁.</tt> :<tt> …</tt> :<tt>H :- Body_k.</tt> jako definice predikátu :<tt>H iff (Body₁ or … or Body_k)</tt> 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. 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(B_i) znamená doslovně, že B_i není známé nebo je neověřitelné. 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 (graf)|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. 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í, [[Zásobník (datová struktura|LIFO]] a backtracking strategii, při které najednou zpracovává pouze jeden mezi-cíl a alternativní cestu. 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. 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á logika|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. 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 [[počítač páté generace|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. 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). == Související články == * [[Prolog (programovací jazyk)]] * [[procedurální programování]] * [[deklarativní programování]] * [[funkcionální programování]] * [[logika]] == Externí odkazy == * [http://axpsu.fpf.slu.cz/~vav10ui/obsahy/log2/skriptalast/logika.pdf Logika a logické programování] (skripta Slezské univerzity v Opavě) * [http://web.ff.cuni.cz/~pelis/CRL.pdf Teorie racionálního usuzování] (skripta Karlovy univerzity v Praze) {{Článek z Wikipedie}} [[Kategorie:Paradigmata programování]]

Návrat na stránku „Logické programování“.