Logické programování

Note	Logické programovací paradigma (princip výpočtu, unifikace, výpočetní stromy, dotazy, volné proměnné). Schopnost elementárního programování v Prologu. IB015,IB101

Logické programování je příkladem deklarativního programovacího paradigmatu. Prográmator popisuje, co má výsledek splňovat, a nikoliv, jak se k němu dopočítat. Má své využití v umělé inteligenci.

Výpočet

Program je databáze faktů a cíl, který nás zajímá.
Výpočet je dokazování cíle pomocí unifikace a SLD rezoluce.
Výsledek je true/false/seznam hodnot volných proměnných.

Je to mechanická dedukce nových informací odpovídající logickému dokazování sporem.

Zápis

Nejzákladnější jsou termy — konstanty, proměnné a funkce, jejíž argumenty jsou termy.

Využívá k zápisu Hornovy klauzule — disjunkce literálů s nejvýše jedním pozitivním literálem, např.: $(P \lor \neg Q \lor \neg R) = {P, \neg Q, \neg R}$ . Dělí se dále na:

fakta, mající právě jeden pozitivní literál, např. p., pocasi(prsi). nebo rodice(matka, otec).,
pravidla, mající právě jeden pozitivní a alespoň jeden negativní literál, např. stav(mokro) :- pocasi(prsi).,
cíle, nemající žádný pozitivní literál, např. ?-stav(prsi). nebo třeba ?-stav(X)..

Unifikace

Dva termy jsou unifikovatelné, pokud jsou stejné, nebo je možné zvolit hodnoty proměnných použitých v unifikovaných termech tak, aby po dosazení hodnot byly termy identické.

Prolog pro unifikaci používá operátor =, pro neunifikaci \=.

Algoritmus

Pokud jsou $t_{1}$ a $t_{2}$ konstanty a jsou shodné, unifikují se.
Pokud $t_{1}$ proměnná a $t_{2}$ term, unifikují se, $t_{1}$ je nahrazená hodnotou $t_{2}$ .
Pokud $t_{1}$ a $t_{2}$ jsou strukturované termy, unifikují se pokud:
- mají stejný funktor,
- mají stejnou aritu,
- všechny korespondující páry argumentů se unifikují,
- všechna nahrazení proměnných z vnořených unifikací jsou kompatibilní (např. nestane se, že by X mělo být a i b naráz).
Jindy se nic neunifikuje.

Note	Při dotazu `?- X = otec(X).` by k unifikaci dojít nemělo, neboť po dosazení za `X` nedojde k identitě. Nicméně podle algoritmu výše dojde k `X = otec(X).`. Algoritmus tedy není korektní. Dá se použít `unify_with_occurs_check`, ale z výkonnostních důvodů se to nedělá.

SLD rezoluce

Při výpočtu dochází k Selective Linear Definite (SLD) rezoluci, při které vzniká výpočetní strom. Fakta se dosazují v pořadí, v jakém je Prolog přečetl.

Algoritmus

Do kořenu stromu dej cíl.
Prohledej databázi faktů pro první podcíl v aktuálním vrcholu.
Vytvoř nový vrchol pro další vyhovující položku.
První podcíl nového vrcholu unifikuj s hlavou nalezené položky a na místo prvního podcíle zapiš tělo položky.
Na hranu zapiš unifikační přiřazení/čerstvou proměnnou.
Prázdný list znamená úspěch. Vrať se k 3., pokud chceš další výsledky.
Pokud nenalezneme vyhovující položku, vytvoříme list "fail". Vrať se k 3., pokud chceš další výsledky.
Pokud všechny cesty vedou k prázdnému seznamu nebo fail, skonči.

Note	Algoritmus není kvůli problému se sebereferencí (viz poznámka výše) korektní a, jelikož se může zacyklit, tak ani úplný.

Vlastnosti

Strom je procházen do hloubky.
Pokud narazí na nekonečnou větev, přeteče mu zásobník.
Levorekurzivní pravidla (odkazují na sebe hned v prvním podcíli těla) často vedou k nekonečným větvím.
Je to důkaz sporem. Cíl udává negaci toho, co ve skutečnosti chceme, a SLD strom se nám snaží tuhle negaci vyvrátit příklady.
Pokud nám ve vrcholu nic nezbude, narazili jsme na spor, protože všechny předpoklady se nám podařilo vyvrátit.

Řezy

Hinty Prologu, že tudy cesta nevede.

Značí se ! a zapisuje se jako prvek klazule, který vždy uspěje.
Pokud na něj Prolog narazí, upne se k větvi vytvořené unifikací s pravidlem obsahujícím !. Další fakta ani pravidla pro právě řešený cíl nehledá. Nadřazené cíle (rodiče v SLD stromu) tohle netrápí.
Unifikace provedené před nalezením ! se stávají fixními — Prolog už se k nim nevrací.

Zelené řezy: Takové řezy, které nemění množinu výsledků. Čistě optimalizace.
Červené řezy: Kdyby tam nebyly, našly by se i další vyhovující výsledky.

Prolog

Logický programovací jazyk s ujetou syntaxí, kterou vymysleli Francouzi.

% fakta
man(heno).
chytry(heno).
umi(heno, programovat).

% pravidla
informatik(X) :- \+ umi(X, prasekdopeciva); umi(X, programovat). % negace a disjunkce
idealman(X) :- man(X), informatik(X), chytry(X). % konjunkce

% dotaz
?- idealman(X).

% odpověď
X = heno ; % protože neumí používat prášek do pečiva
X = heno. % protože umí programovat

Seznamy

[a, b, c]

[a, b, c] = [H|T].
H = a, T= [b, c].

?-length([a, b, c], X).
X = 3.

?-islist([a, b, c]).
true.

member(X, [X|]).
member(X, [|T]) :- member(X, T).

Anonymní proměnná

Značíme podtržítkem.

Termy

Atomy — 'pepa_1', pepa, '2'
Čísla — 2, 5
Proměnné — X
Strukturované termy (funktory s danou aritou následované sekvencí argumentů — termů — v závorkách) — pocasi(prsi)