PŘÍRODOVĚDECKÁ FAKULTA UNIVERZITY PALACKÉHOKATEDRA MATEMATICKÉ INFORMATIKY

DIPLOMOVÁ PRÁCE

LINEÁRNÍ LOGIKA

2005 Lukáš Chrpa

Katedra matematické informatiky PřF UP Olomouc

Předpis pro vypracování diplomové práce

I.

Při zpracování diplomové práce student usiluje o co nejvýstižnější a nejpřízni-vější obraz o svých schopnostech, úrovni svých znalostí a osvědčuje, jak si osvojilnezbytné návyky odborného a technického způsobu vyjadřování, jaké má znalostiodborné literatury a jak jí umí používat.

Diplomová práce se v tomto smyslu hodnotí jako celek.

II.

Student se musí ve své práci bez újmy na úplnosti vyjadřovat stručně, od-borně, slohově i gramaticky správně. Text (včetně popisků příloh) diplomovépráce musí být před odevzdáním pečlivě prohlédnut. Písařské chyby, chyby v tiskuapod., musí být opraveny.

Nedostatky diplomové práce v tomto směru snižují klasifikaci i práce jinakobsahově dobré.

III.

Text diplomové práce musí být zpracován programem LATEX s použitím makrakatedry matematické informatiky a vytištěn po jedné straně papíru formátu A4.Diplomová práce se odevzdává takto:

• 1x originál v knihařské vazbě

• 1x kopie spojená v polotuhých deskách

• 1x záznam textu diplomové práce pořízený textovým editorem na disketě,kterou si student před odevzdáním vyzvedne na sekretariátě katedry.

IV.

V originále se na stránku s místopřísežným prohlášením připojí vlastnoručnípodpis.

Došlo-li v průběhu zpracování diplomové práce k významným odchylkám odzadání diplomového úkolu, které na základě žádosti studenta schválil vedoucí

i

katedry, připojí se další list, na němž budou tyto skutečnosti uvedeny. Způsobuvedení se stanoví individuálně a v originále bude k záznamu připojen podpisvedoucího katedry. Nevýznamné odchylky uvádí student v anotaci.

V.

Uspořádání odevzdaných vyhotovení diplomové práce se předepisuje násle-dovně:

• předsádkový list

• zadání diplomové práce

• předpis pro vypracování diplomové práce

• místopřísežné prohlášení o samostatném vypracování diplomové práce

• (list s vyjádřením k odchylkám od zadání, pokud byly schváleny)

• anotace diplomové práce

• obsah diplomové práce s odkazy na odpovídající stránky nebo čísla příloh,seznam tabulek a obrázků

• rozvedení diplomového úkolu podle obsahu s dílčími závěry na konci každékapitoly

• celkový závěr diplomové práce

• cizojazyčné resumé (cca 15 řádků)

• seznam použité literatury v abecedním autorském uspořádání – tabulky,nákresy, přílohy (doklady, prospekty, elaboráty apod.)

Přední deska originálu bude potištěna stejně jako předsádkový list, je možnovypustit znak univerzity.

Diplomová práce, která nebude vyhovovat tomuto uspořádání, nemůže býtpřijata.

VI.

Použitá literatura, předlohy apod., použité při zpracování musí být na přísluš-ných místech v diplomové práci označeny odkazem na průběžné číslo ze seznamupoužité literatury, příslušná stránka se uvede v hranaté závorce. Jde-li o citát,uvedou se čísla prvního a posledního řádku citátu.

ii

Součástí řešení diplomového úkolu je zdrojový text programu. Způsobilostprovozu produktu osvědčuje student při obhajobě diplomové práce.

VII.

Všechny propočty nebo výpočty musí být podrobně a přehledně uspořádánytak, aby každý odborník byl schopen jejich správnost přezkoušet. U použitýchvzorců, součinitelů nebo hodnot z praxe musí být uveden původ. Jsou-li uváděnyúdaje, které mohou tvořit předmět hospodářského nebo státního tajemství, jetřeba tuto okolnost uvést při odevzdání diplomové práce. V takovém případě sepro přístup k diplomové práci předepíše zvláštní režim (závazný i pro oponenty).

V Olomouci dne 13. března 1996 Doc. RNDr. Josef Hosvedoucí katedry

matematické informatiky

Za správnost: Zd. Nesvadbová

iii

Místopřísežně prohlašuji, že jsem celou práci včetně příloh vypracoval samostatně.

duben 2005 Lukáš Chrpa

iv

Anotace

V této diplomové práci jsem se zabýval logickým programováním na bázi lineárnílogiky, konkrétně zkonstruováním lineárně logického programovacího jazyka SLLLa jeho překladače do jazyka Prolog.

v

Děkuji RNDr. Arnoštu Večerkovi za odborné vedení mé diplomové práce, poskyt-nutí studijních materiálů a za ochotné poskytnutí konzultací a odborné pomocipři realizaci. Dále chci poděkovat rodičům za podporu při studiu.

vi

Obsah

1. Základy logického programování 11.1. Základní koncepce . . . . . . . . . . . . . . . . . . . . . . . . . . 11.2. Historie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11.3. Logický program a uživatelský dotaz . . . . . . . . . . . . . . . . 11.4. Teoretické základy logického programování . . . . . . . . . . . . . 21.5. Základy jazyka Prolog . . . . . . . . . . . . . . . . . . . . . . . . 4

2. Lineární logika 72.1. Úvod a historie . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.2. Základní myšlenky lineární logiky . . . . . . . . . . . . . . . . . . 72.3. Operátory lineární logiky . . . . . . . . . . . . . . . . . . . . . . . 82.4. Teorie lineární logiky . . . . . . . . . . . . . . . . . . . . . . . . . 92.5. Využití lineární logiky v informatice . . . . . . . . . . . . . . . . . 112.6. Lineární logické programování . . . . . . . . . . . . . . . . . . . . 11

3. Jazyk SLLL 133.1. Úvod . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133.2. Teoretické základy překladačů . . . . . . . . . . . . . . . . . . . . 14

3.2.1. Lexikální analýza . . . . . . . . . . . . . . . . . . . . . . . 143.2.2. Syntaktická analýza . . . . . . . . . . . . . . . . . . . . . . 153.2.3. Generování kódu . . . . . . . . . . . . . . . . . . . . . . . 16

3.3. Nástroje pro analýzu kódu . . . . . . . . . . . . . . . . . . . . . . 163.3.1. Flex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163.3.2. Bison . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

3.4. Implementace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193.4.1. Lexikální analyzátor . . . . . . . . . . . . . . . . . . . . . 213.4.2. Syntaktický analyzátor . . . . . . . . . . . . . . . . . . . . 223.4.3. Úprava 2. interní formy . . . . . . . . . . . . . . . . . . . . 253.4.4. Generování kódu . . . . . . . . . . . . . . . . . . . . . . . 26

3.5. Uživatelské prostředí . . . . . . . . . . . . . . . . . . . . . . . . . 353.5.1. Soubor slll.ini . . . . . . . . . . . . . . . . . . . . . . . . . 36

3.6. Příklady . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 373.6.1. Eulerův tah . . . . . . . . . . . . . . . . . . . . . . . . . . 373.6.2. Hamiltonova kružnice . . . . . . . . . . . . . . . . . . . . . 383.6.3. Vodní nádoby . . . . . . . . . . . . . . . . . . . . . . . . . 393.6.4. Tah jezdce . . . . . . . . . . . . . . . . . . . . . . . . . . . 403.6.5. Královny . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

4. Závěr 44

Reference 46

i

1. Základy logického programování

1.1. Základní koncepce

Logické programování je samostatné paradigma, lišící se zcela od ostatníchparadigmat. Logický program je tvořen fakty a pravidly, které nám popisují urči-tou situaci (např. rodinné vztahy). Uživatelský dotaz (na tento program) spustívýpočet, který nám zjistí, zda je dotaz splnitelný, či neslpnitelný. Logické progra-mování nám tedy dává možnost poměrně jednoduchým a intuitivním způsobempopsat nějakou situaci, ve které hledáme odpovědi na otázky, zda je možné to čiono a za jakých podmínek, což programátorovi výrazně usnadňuje práci, protoženemusí vymýšlet speciální algoritmy, které by vyřešily příslušný problém.

1.2. Historie

Základní kameny logického programování položil Leibnitz1, který ve své teoriiuniverzálního jazyka představil myšlenku, že by bylo možné vytvořit mechanis-mus, který zjistí zda dané tvrzení logicky vyplývá z dané množiny již známýchfaktů. Tato myšlenka se začala realizovat až v 70. letech minulého století, kdybyl v Marseille vytvořen nejznámější logický programovací jazyk PROLOG. VJaponsku byl Prolog využit jako základní jazyk logického procesoru počítačů 5.generace a i přesto, že tento projekt nesplnil veškerá očekávání, je Prolog stálehodně používán při programování úloh umělé inteligence. Později bylo logicképrogramování rozšiřováno například o modální, temporální a konečně lineárnílogiku (o které je tato diplomová práce).

1.3. Logický program a uživatelský dotaz

V této podkapitole bude popsán logický program a uživatelský dotaz. Tentopopis bude slovní, tedy bez jakýchkoli implementačních podrobností žádnéhologického programovacího jazyka.Logický program se skládá s těchto částí:

fakty — Fakty můžeme chápat jako jevy, které jsou vždy splnitelné. Např. mů-žeme definovat, že Petr je rodičem Pavla, že Petr i Pavel jsou muži apod.

pravidla — Pravidla můžeme chápat jako mechanismus, který nám popisujenějakou část světa. Např. můžeme definovat, že otec je takový člověk, kterýje rodičem a zároveň mužem apod.

Uživatelský dotaz můžeme chápat jako otázku, na kterou hledá interpret logic-kého jazyka odpověď. Typy uživatelských dotazů:

1Gottfried Wilhelm von Leibniz (1646-1716) - Německý filozof a matematik

1

• Je Petr otcem ? - Na takovýto typ dotazu interpret odpoví, buď ANO, neboNE.

• Kdo je Pavlův rodič ? - Pokud existuje na tento dotaz odpověď ANO, pakinterpret vypíše podmínky, které k této odpovědi vedly (např. Petr).

Je dobré ještě připomenout, že za logickou správnost faktů a pravidel nese zod-povědnost programátor, nikoli programovací jazyk.

1.4. Teoretické základy logického programování

Definice 1.1: Literál je libovolná atomická formule (tzv. pozitivní literál) nebojejí negace (tzv. negativní literál).

Definice 1.2: Klauzule je libovolná disjunkce literálů. Hornovská klauzule jeklauzule obsahující nejvýše jeden pozitivní literál.

Poznámka 1.3: Prázdná klauzule se označuje symbolem 2 a v logickém pro-gramování je to symbol sporu.

Věta 1.4: P |= G, právě když je formule P,¬G sporná

Důkaz: Pomocí věty o důkazu sporem, viz. [1]

Logický program je tvořen konečnou množinou Hornovských klausulí, které ob-sahují právě jeden pozitivní literál. Z výše uvedeného textu víme, že programobsahuje fakty a pravidla. Pro fakty platí:

• Hornovská klauzule obsahuje právě jeden pozitivní literál a žádný negativníliterál a má tvar A.

Pro pravidla platí:

• Hornovská klauzule obsahuje právě jeden pozitivní literál a alespoň jedennegativní literál a má tvar A∨¬B1 ∨ · · · ∨¬Bn, což je ekvivalentní formuliB1 ∧ · · · ∧Bn ⇒ A. Ověření je prosté, stačí použít DeMorganových zákonůpro formuli ¬B1 ∨ · · · ∨ ¬Bn, čímž dostaneme formuli ¬(B1 ∧ · · · ∧ Bn) anásledně využít toho, že formule A ∨ ¬B je ekvivalentní s formulí B ⇒ A.

• Některé logické programovací jazyky (např. Prolog) umožňují v odvozova-cích pravidlech používat disjunkci. Ovšem i tato syntaxe vede k Hornov-ským klauzulím, protože platí že pravidlo B1 ∨ B2 ⇒ A je ekvivalentnípravidlům B1 ⇒ A a B2 ⇒ A (viz. výše).

2

Uživatelským dotazům odpovídá Hornovská klauzule obsahující alespoň jedennegativní literál, ale neobsahuje žádný pozitivní literál. Z této klauzule tvaru¬G1∨· · ·∨¬Gn obdržíme formuli ¬(G1∧· · ·∧Gn), což odpovídá negaci uživatel-ského dotazu G1 ∧ · · · ∧ Gn. Pokud položíme logickému programovacímu jazykudotaz, pak vlastně zjišťujeme, zda platí P |= (G1 ∧ · · · ∧ Gn). S využitím věty1.4 zkoumáme P, (¬G1 ∨ · · · ∨ ¬Gn) |= 2, což opět vede k Hornovským klauzu-lím. Tento postup lze zobecnit pokud jsou v uživatelském dotazu volné proměnnéX1, . . . , Xm. Pak má dotaz tvar P |= (∃X1 . . . ∃Xm)(G1 ∧ · · · ∧ Gn), což je ekvi-valentní s tvrzením P, (∀X1 . . . ∀Xm)(¬G1 ∨ · · · ∨ ¬Gn) |= 2.

Hornovské klauzule se využívají proto, aby zefektivnily výpočet odpovědi na za-daný uživatelský dotaz (tzv. SLD-rezoluce).

Definice 1.5: Substitucí θ = (x1/s1, . . . , xn/sn) budeme rozumět nahrazení pro-měnných xi termy si, platí-li xi 6= xj pro i 6= j. Označení ϕθ symbolizujevýsledek substituce θ na formuli ϕ. Substituce můžeme skládat, zápis ϕ(σθ)bude vyjadřovat formuli, která vznikne aplikací substituce θ na formulivzniklou aplikací substituce σ na formuli ϕ.

Definice 1.6: Substituce θ se nazývá obecnější než substituce σ, jestliže existujesubstituce τ , pro kterou σ = θτ).

Definice 1.7: Substituce θ se nazývá unifikací množiny {ϕ1, . . . , ϕn} formulí,jestliže ϕiθ = ϕjθ pro libovolné i, j ∈ {1, . . . , n}.

Definice 1.8: Unifikace θ množiny {ϕ1, . . . , ϕn} formulí, se nazývá nejobecnějšíunifikací (značíme mgu) této množiny, jestliže je obecnější, než jakákoli jináunifikace množiny {ϕ1, . . . , ϕn}.

Nyní si uvedeme algoritmus, který nám vypočítá odpověď na uživatelský dotaz.Tento algoritmus bude využívat tzv. rezoluční zásobník, který bude obsahovattrojice 〈Gij , Rij , θij〉 (cíl, číslo pravidla, substituce). Tento algoritmus využívávětšina logických programovacích jazyků jako třeba Prolog.

Algoritmus:VSTUP: uživatelský dotaz G0 ve tvaru ← G0,1, . . . , G0,n0

VÝSTUP: pokud algoritmus po n krocích skončí úspěchem, výstupem je zásobníkSn.

1. Na počátku máme dotaz G0 ve tvaru ← G0,1, . . . , G0,n0 , dále položíme R0 =1 a S0 = 〈〉. Pokračujeme krokem 2, pro i = 0.

2. Průběžný i-tý krok.Uvažujme aktuální dotaz Gi tvaru ← Gi,1, . . . , Gi,ni

a číslo pravidla Ri.Interpret se snaží unifikovat Gi1 s hlavou některé klauzule programu s číslemvětším nebo rovným Ri a postupuje vzestupně.

3

(a) Hlava žádné klauzule není unifikovatelná s Gi,1. Pokud je rezo-luční zásobník Si prázdný, pak činnost interpretu končí neúspě-chem. Pokud je rezoluční zásobník Si neprázdný, tj. ve tvaru Si =〈〈Gi1 , Ri1 , θi1〉, . . . , 〈Gik , Rik , θik〉〉, pak položíme:

Gi+1 = Gik

Ri+1 = Rik + 1

Si+1 = 〈〈Gi1 , Ri1 , θi1〉, . . . , 〈Gik−1 , Rik−1 , θik−1〉〉Dále pokračujeme bodem 2 v průběžném kroku i + 1.

(b) Hlava klauzule Cl ve tvaru Cl,0 ← Cl,1, . . . , Cl,nl, kde Ri ≤ l je unifi-

kovatelná s Gi,1. Pak položme:

Ri+1 = 1

θi+1 = mgu(Gi,1, Cl,0)

Gi+1 = Cl,1θi+1, . . . , Cl,nlθi+1, Gi,2θi+1, . . . , Gi,ni

θi+1

Si+1 = Si + 〈Gi, l, θi+1〉Je-li Cl faktem, potom Gi+1 = Gi,2θi+1, . . . , Gi,ni

θi+1. Pokud mámenyní Gi+1 = 2, podařilo se odvodit spor a dále pokračujeme bodem3. Jinak pokračujeme bodem 2 v průběžném kroku i + 1.

3. Položme n = i + 1, výstupem je rezoluční zásobník Sn.

Pokud algoritmus skončí neúspěchem, je odpověď na uživatelský do-taz NE. V opačném případě máme výsledný rezoluční zásobník Sn =〈〈Gn1 , Rn1 , θn1〉, . . . , 〈Gnk

, Rnk, θnk

〉〉, pak výslednou substituci θ získáme slože-ním, tj. θ = θn1 · · · θnk

. Odpověď na uživatelský dotaz je tedy ANO a zároveňse vypíší termy, které jsou substituovány (substitucí θ) za proměnné uvedené vuživatelském dotazu. Nevýhodou tohoto algoritmu je situace, že se výpočet do-stane do nekonečné větve, pak teoreticky nikdy neskončí, prakticky ovšem skončípřetečením zásobníku.

1.5. Základy jazyka Prolog

Jak už bylo zmíněno Prolog je nejznámějším logickým programovacím jazy-kem. Prolog je sám o sobě hodně komplexním jazykem, zde však bude uvedenjen základ, který nám postačí. Nyní si nadefinujeme pojmy, které nám pozdějipomohou zjistit jak se zapisují fakty a pravidla, ze kterých se skládá logickýprogram:

• atom — složen s písmen, číslic a symbolu ” ”, vždy začíná malým písmenem

• proměnná — složena s písmen, číslic a symbolu ” ”, vždy začíná velkýmpísmenem

4

• řetězec — text ohraničený apostrofy

• seznam — má tvar [prvek1, prvek2, . . . , prvekn], zápis [H|T] vyjadřuje: Hjako 1.prvek seznamu, T jako zbytek seznamu (bez 1.prvku).

Nyní můžeme říci, že argumenty v Prologu mohou být atomy, proměnné, řetězce,seznamy a číselné konstanty. Atomy se navíc používají jako jména atomickýchformulí, které nám tvoří základní kameny Prologu. Tedy atomická formule sezapisuje takto:

• atom(arg1, . . . , argn) — pro argumenty arg1, . . . , argn

• atom — pokud nejsou žádné argumenty

Pak už je jen krůček k faktům, které se zapisují jako:

• atomicka formule.

Pak už stačí definovat pojem formule, kde formule je:

• atomická formule

• přiřazení — (X1 is X+1), operátory ve výrazech jsou standardní, jen celo-číselné dělení se dělá pomocí operátoru //

• porovnání — (X==Y), operátory porovnání jsou standardní, až na =<(menší rovno) a = \ = (nerovno)

• speciální formule

– true — vždy pravdivá

– fail — vždy nepravdivá

– write(arg1, . . . argn) — vypíše argumenty vždy, když se při výpočtuuživatelského dotazu na tuto formuli narazí

– nl — odřádkování

• konjunkce — formule,formule

• disjunkce — formule;formule

• negace — not(atomicka formule)

• jediné řešení — once(atomicka formule), toto znamená, že jako platné sebere pouze první řešení

Nyní není problém zapsat pravidlo:

• atomicka formule :- formule.

5

V tuto chvíli už víme jak napsat jednoduchý program v Prologu, který se skládá sfaktů a pravidel. Tento program se dá načíst v prostředí Prologu a pak je Prologschopen odpovídat na uživatelské dotazy tvaru:

• formule.

6

2. Lineární logika

2.1. Úvod a historie

Lineární logika je poměrně mladý vědní obor, který byl poprvé představen vroce 1987 J.Y. Girardem2. Postupem času v ní informatici nalezli silný nástroj,protože je dobře použitelná ke kódování výpočetních modelů jako například Pe-triho sítě, Turingovy stroje a mnoho dalších. Lineární logika je tedy využívaná iv logickém programování, což je i tématem této diplomové práce.

2.2. Základní myšlenky lineární logiky

Lineární logika bývá popisována jako ”logika zdrojů”. Na rozdíl od klasickématematické logiky, kde logické fakty jsou neměnné (vždy pravdivé), v lineárnílogice ovšem jsou fakty použitelné zpravidla pouze jednou. Jinými slovy řečeno,že na začátku výpočtu máme nějaké zdroje (lineární fakty), které v průběhuvýpočtu spotřebováváme.V klasické logice platí následující tautologie (ověření je zřejmé):

ϕ ⇒ ϕ ∧ ϕ

ϕ ∧ ψ ⇒ ϕ

Intuitivně nás mohou napadnout otázky ”Odkud se vzalo další ϕ ?” nebo ”Kamse ztratilo ψ ?”. V lineární logice tyto tautologie neplatí, jelikož máme omezenémnožství zdrojů (lineárních faktů). Uveďme si následující příklad: máme jednu20Kč minci (ozn. ji C), automat na nápoje, ve kterém stojí nápoj 20Kč (ozn.nápoj jako N), dále máme automat na bagety, ve kterém stojí bageta rovněž20Kč (ozn. bagetu jako B). Formálně zapsáno:

C ⇒ N

C ⇒ B

Při použití klasické logiky obdržíme následující tvrzení:

C ⇒ (N ∧B)

A to ještě není všechno. Při použití formule ϕ ⇒ ϕ ∧ ϕ a tranzitivity implikacedostaneme:

C ⇒ (N ∧B) ∧ (N ∧B) ∧ . . .

Jinými slovy při použití klasické logiky si můžeme za jedinou minci pořídit nápojůa baget kolik hrdlo ráčí a nejen to. Intuitivně poznáme, že není něco v pořádku,výsledek neodpovídá realitě. Lineární logika na rozdíl od klasické logiky dokážepopsat to, co se ve skutečnosti stane, hodíme-li minci do automatu.

2Jean Yves Girard (*1947) - francouzský matematik a informatik

7

2.3. Operátory lineární logiky

V lineární logice definujeme následující operátory:

implikace — A ( B vyjadřuje, zda B je odvoditelné použitím právě jednohoA.

negace — A⊥ vyjadřuje spotřebu zdroje.

multiplikativní konjunkce — A⊗B znamená použití obou zdrojů najednou.

additivní konjunkce — A&B vyjadřuje právo volby mezi zdroji A a B (musíbýt oba zdroje nespotřebované).

additivní disjunkce — A ⊕ B vyjadřuje volbu mezi A a B (musí být aspoňjeden zdroj nespotřebovaný).

mutliplikativní disjunkce — A℘B znamená, pokud není A, pak B.

exponenciál ! — !A převádí lineární fakt A na logický (nespotřebovatelný) fakt.

exponenciál ? — ?A duální operátor k !.

Dále definujeme následující konstanty:

1 — neutrální prvek pro operaci ⊗> — neutrální prvek pro operaci &

⊥ — neutrální prvek pro operaci ℘

0 — neutrální prvek pro operaci ⊕A nyní několik základních vztahů mezi operacemi (podobně jako v klasické logicejsou i zde využívány De Morganovy zákony):

1⊥ = ⊥⊥⊥ = 1

>⊥ = 0

0⊥ = >(A⊥)⊥ = A

(A⊗B)⊥ = A⊥℘B⊥

(A℘B)⊥ = A⊥ ⊗B⊥

(A&B)⊥ = A⊥ ⊕B⊥

(A⊕B)⊥ = A⊥&B⊥

(!A)⊥ = ?A⊥

(?A)⊥ = !A⊥

A ( B = A⊥℘B

!A ( B = A ⇒ B

8

Ještě pro úplnost upřesníme, že operátory (,⊗, ℘ s příslušnými neutrálnímiprvky 1,⊥ nazýváme multiplikativní. Operátory &,⊕ s příslušnými neutrálnímiprvky >, 0 nazýváme additivní. A operátory !,? nazýváme exponenciály. Celýkalkul lineární logiky nalezneme v [4].

2.4. Teorie lineární logiky

Definice 2.1: Oslabením (v angl. literatuře se setkáme s pojmem Weakening)rozumíme následující pravidlo:

∆ ` Σ∆, A ` Σ

Definice 2.2: Kontrakcí (v angl. literatuře se setkáme s pojmem Contraction)rozumíme následující pravidlo:

∆, A, A ` Σ∆, A ` Σ

Věta 2.3: Použijeme-li pravidlo oslabení v lineární logice, pak operace ⊗ je sil-nější než operace &.

Důkaz:∆ ` ∆

∆, B ` ∆B ` B

∆, B ` B

∆, B ` ∆&B∆⊗B ` ∆&B

Věta 2.4: Použijeme-li pravidlo kontrakce v lineární logice, pak operace & jesilnější než operace ⊗.

Důkaz:∆ ` ∆

∆&B ` ∆B ` B

∆&B ` B

∆&B, ∆&B ` ∆⊗B∆&B ` ∆⊗B

Poznámka 2.5: Věta 2.3 nám vlastně říká, že spotřebování obou zdrojů je sil-nější, než spotřebování zdroje jednoho (podle toho který si zvolíme). Jinýmislovy řečeno, použití vlastnosti oslabení v lineární logice způsobuje ztrácenízdrojů. Věta 2.4 nám na oplátku sděluje, že spotřebování jednoho zdroje jesilnější než spotřebování obou zdrojů. Jinými slovy se dá říci, že vlastnostkontrakce nám zase zdroje přidává. Proto použití vlastností oslabení a kon-trakce v lineární logice je nepovolené. Vyjímku tvoří použití exponenciálů(!,?), které tvoří jakýsi most mezi lineární a klasickou logikou (připomeňmevztah !A ( B = A ⇒ B), který nám umožňuje využití vlastností oslabenía kontrakce.

9

Definice 2.6: Výrokovou lineární logikou nazveme lineární logiku obsahujícímultiplikativní a additivní operace, exponenciály a konstanty 1,⊥,>, 0.

Věta 2.7: Výroková lineární logika je nerozhodnutelná.

Důkaz: Jen idea. Problém rozhodnutelnosti lineární logiky zredukujeme na pro-blém zastavení ACM (and-branching two-counter machine). KonfiguraceACM je trojice 〈Qi, A, B〉, kde Qi je stav a A a B jsou přirozená čísla (tzv.čítače). ACM obsahuje konečnou množinu stavů a instrukce: zvyš A, zvyšB, sniž A, sniž B, rozvětvi. Při redukci jednotlivým operacím lineární logikypřiřazujeme operace ACM (např. additivní konjunkci & odpovídá operacerozvětvi). Odtud se dostaneme k tvrzení, že pokud by byla výroková line-ární logika rozhodnutelná, bude řešitelný i problém zastavení ACM. Dá sevšak dokázat, že problém zastavení ACM je neřešitelný.

Věta 2.8: Problém lineární logiky s multiplikativními a additivními operacemi(bez exponenciálů) je PSPACE-úplný.

Důkaz: Jen idea. Důkaz provedeme pomocí redukce známého PSPACE-úplnéhoproblému splnitelnosti kvantifikovaných formulí na náš problém lineárnílogiky bez exponenciálů. Pro upřesnění je třeba uvést, že bez možnostipoužití exponenciálů se vždy daný zdroj spotřebuje. Při redukci využijemenásledujících vztahů:

∀x = (x&x⊥)

∃x = (x⊕ x⊥)

Tyto vztahy nám sice nezajistí správné kódování pořadí kvantifikátorů,nicméně se dá získat použitím multiplikativních operací.

Věta 2.9: Problém lineární logiky s multiplikativními operacemi (bez additiv-ních operací a exponenciálů) je NP-úplný.

Důkaz: Jen idea. NP-úplnost tohoto problému dokážeme pomocí redukce z pro-blému 3-Partition, který je rovněž NP-úplný. 3-Partition problém spočívá vtom, že na počátku máme množinu přirozených čísel, kterou rozdělíme do3 disjunktních podmnožin a součet čísel jednotlivých podmnožin je shodný.Výhoda tohoto řešení spočívá v tom, že 3-Partition problém se poměrněvýhodně kóduje pomocí multiplikativních operací lineární logiky.

Poznámka 2.10: Ideje důkazů posledních 3 vět jsou k nalezení v [3], kde jsou iodkazy na literaturu obsahující celé důkazy těchto vět.

10

2.5. Využití lineární logiky v informatice

Jak již bylo výše uvedeno, lineární logika je poměrně dobrý nástroj proinformatiky, který dobře slouží k modelování některých problémů. Následujícípříklad ukáže jak se pomocí lineární logiky modelují Petriho sítě:

Přechod T1. . . !((a⊗ c) ( b)

Přechod T2. . . !((b⊗ d⊗ d) ( (c⊗ d))

Počáteční značení. . . a, c, d, d

Je poměrně zřejmě vidět jak se tvoří formule popisující přechody (multiplikativníkonjunkce symbolů vstupních míst implikuje multiplikativní konjunkci symbolůvýstupních míst). Počáteční značení je dáno počtem volných příslušných lineár-ních faktů. Problém dosažitelnosti značení Petriho sítě může být pomocí lineárnílogiky interpretován následovně:

!((a⊗ c) ( b), !((b⊗ d⊗ d) ( (c⊗ d)), a, c, d, d ` c, d

Lineární logika bývá využívaná i při různých optimalizacích a podobně. Její jedi-nečnost spočívá v umění popsat spotřebovávání omezených zdrojů, což vystihujepoměrně velké množství příkladů z reálného světa.

2.6. Lineární logické programování

Tak jako je klasické logické programování postaveno na predikátové logice,tak lineární logické programování je postaveno na logice lineární. I u lineárníhologického programování máme program složen s faktů a pravidel a uživatelskýmdotazem spustíme výpočet, který nám odpoví na otázku, zda daný dotaz vy-plývá z programu (a za jakých podmínek), či nikoli. Rozdíl je v tom, že faktya někdy také pravidla v lineárním logickém programování jsou použitelné pouzejednou, což vychází z teorie lineární logiky. Programovací jazyky zabývající selineárním logickým programování mají zpravidla obdobnou syntaxi jako klasickélogické programovací jazyky (jako např. Prolog). Bývá tak učiněno proto, jeli-kož jazyky používající Hornovské klauzule mají rychlejší výpočet uživatelskéhodotazu, než jazyky, které Hornovských klauzulí nevyužívají. Lineární logika je

11

často spojována s klasickou logikou (v teorii se to řešilo použitím exponenciálu’ !’), tedy v lineárním logickém programu nalezneme jak lineární tak i klasickéfakty, či pravidla. V praxi bývají využívány operace multiplikativní konjunkcea additivní disjunkce. Ostatní operace nemají přílišnou praktickou využitelnost,proto nebývají v některých lineárních logických jazycích implementovány.Lineární programovací jazyky bývají implementovány jako:

Překladače do Prologu — Výhodou tohoto řešení je menší náročnost na vý-voj, ovšem nevýhodou je dlouhá doba výpočtů uživatelských dotazů. Taktoimplementovány jsou např: Lygon, Lolli aj.

Interprety — Výhodou tohoto řešení je poměrně rychlý výpočet uživatelskýchdotazů, ovšem vývoj těchto interpretů je dost složitý. Takto implemento-vány jsou např: LLP, LTL3 aj.

Překladače do Prologu mají práci usnadněnou v tom, že syntaxe jejich jazykabývá podobná té Prologovské. Nevýhodou je, že Prolog nepodporuje lineární lo-giku a tudíž je zde nutné nějakým způsobem lineární logiku emulovat. Dost častobývají využity seznamy lineárních faktů, které jsou mezi jednotlivými pravidlypředávány. Ovšem tento způsob je značně neefektivní. Na rozdíl od toho jsouinterprety o dost efektivnější. Dost často napodobují Prologovský algoritmus hle-dání odpovědi na dotaz (pomocí rezolučního zásobníku) s tím rozdílem, že tentoalgoritmus navíc podporuje lineární logiku. Například práce s lineárními faktyspočívá v tom, že při použití faktu se u něj nastaví příznak na použitý a tentofakt se již nesmí použít znovu. Při návratech se pak příznak faktu může nastavitna volný, navracíme-li se do situace, kdy ještě nebyl použit.Ještě je dobré podotknout, že lineární logické programovací jazyky se nezabývajíjen lineární a klasickou logikou, ale dost často i temporální logikou. Dá se říci,že vývoj logických programovacích jazyků spěje k takovým, které v sobě budouzahrnovat podporu veškerých dosud známých logik.

3Vyvinut zde na UP RNDr. Arnoštem Večerkou

12

3. Jazyk SLLL

3.1. Úvod

Programovací jazyk SLLL (Simple Linear Logic Language) byl navržen jakojazyk podporující lineární logiku a je nedílnou součástí této diplomové práce.Programovací jazyk SLLL je implementován jako překladač do Prologu a protos ním úzce spolupracuje, konkrétně s SWI-Prologem verze 5. Následující dia-gram popisuje činnost programovacího jazyka SLLL a jeho spolupráci s Prologem:

Sám programovací jazyk SLLL je jak již diagram napovídá rozdělen do 2 části:

• Uživatelské prostředí, které slouží uživateli k napsání programu, jeho ulo-žení, případně načtení s disku a vypisují se zde chyby, které nastaly přianalýze programu.

• Jádro, které slouží k analýze a překladu programu do jazyka Prolog.

Programovací jazyk je vytvořen v jazyce C++, ve vývojovém prostředí VisualStudia .NET 2003, ale nebylo zde využito NET Frameworku. Jádro je zkompilo-vané jako dynamická knihovna (dll) bez podpory WinAPI a s podporou knihovnyATL.Uživatelské prostředí je zkompilováno jako spustitelný soubor (exe) s pod-porou knihovny MFC. Programovací jazyk SLLL se tedy dá spustit na jakékoliWindows platformě verze 95 a vyšší (testován je na verzi Windows XP SP2). Přitvorbě jádra bylo využito lexikálního analyzátoru Flex a syntaktického analyzá-toru Bison (viz. dále).

13

3.2. Teoretické základy překladačů

V této podkapitole se budeme zabývat základními poznatky z teorie překla-dačů, které byly využity při tvorbě programovacího jazyka SLLL. Následujícídiagram popisuje posloupnost akcí, které musí překladač vykonat (uvedenybudou jen základní operace):

3.2.1. Lexikální analýza

Lexikální analýza slouží ke zpracování zdrojového kódu do 1. interní formy.Úkoly lexikálního analyzátoru:

• Rozpoznat atomy programovacího jazyka (konstanty, identifikátory, operá-tory, oddělovače a omezovače) a převést je do 1. interní formy.

• Vynechat vše, co není k překladu zapotřebí (mezery, komentáře aj.)

Pro popis atomů programovacího jazyka stačí regulární gramatika (pro popisprogramovacího jazyka jako celku je zapotřebí bezkontextové gramatiky, proto seanalýza dělí na lexikální a syntaktickou). V praxi se ovšem regulární gramatikynepoužívají, místo toho se používají tzv. regulární výrazy, protože práce s nimije jednodušší. Regulární výrazy definujeme následovně:

14

• znak je regulární výraz

• ε je regulární výraz

• jsou-li α a β regulární výrazy, pak jsou regulární výrazy také:

– αβ. . . konkatenance

– α | β. . . α nebo β

– α+. . . pozitivní uzávěr

– (α). . . uzávorkování

• Regulární výraz vzniká konečným počtem výše uvedených kroků

1. interní forma obsahuje posloupnost symbolů, kde typy atomů bývají repre-zentovány celočíselnými konstantami a navíc hodnotou atomu (např. jméno pro-měnné). Chyby rozpoznané lexikálním analyzátorem bývají nejčastěji:

• Neznámý znak

• Chybně zapsaná konstanta

• Konstanta mimo rozsah

3.2.2. Syntaktická analýza

Syntaktická analýza analyzuje program jako celek, k jeho analýze je zapo-třebí bezkontextové gramatiky. Z teorie formálních jazyků vyplývají následující2 možnosti jak bezkontextovou gramatiku analyzovat:

Shora-dolů: Analýze shora dolů přísluší třída gramatik LL(k), v praxi se všakvyužívá pouze LL(1). Konkrétní implementace (tzv. metoda rekurzivníhosestupu) vypadá následovně:

• Každému neterminálnímu symbolu odpovídá funkce na jeho zpraco-vání

• Ke každému pravidlu A→ α vypočítáme množinu terminálních sym-bolů First(αFollow(A))={t1, . . . ,tn} a pro každý terminální symbol ztéto množiny, který byl předtím předán lexikálním analyzátorem, vlo-žíme patřičné instrukce do funkce odpovídající neterminálu A, kterézpracují pravidlo A→ α.

Problém tohoto řešení spočívá v tom, že gramatika LL(1) není natolikobecná, aby vyhověla všem syntaxím. Možné řešení je transformovat gra-matiku do LL(1), ale to nemusí být vždy možné, navíc transformace bývákomplikovaná.

15

Zdola-nahoru: Analýza zdola nahoru je obecnější než analýza shora dolů. Ana-lýze zdola nahoru odpovídá třída gramatik LR(1), která je ovšem dostobecná a konstrukce automatu LR(1) je příliš komplikovaná, proto se vpraxi využívá méně obecnější, ale dostačující gramatika LALR(1). Činnostautomatu LALR(1) se skládá z přesunů a redukcí. Při přesunu se načte novýlexikální symbol a při redukci se zpracovává dané pravidlo. Ovšem i přikonstrukci automatu LALR(1), může dojít ke konfliktům (přesun-redukce,přesun-přesun), pak tedy gramatika není ani LALR(1). Tento problém na-stane vždy, když je derivační strom gramatiky nejednoznačný. V praxi setento problém řeší tak, že se vybere akce, která se vykoná (přesun neboredukce), zpravidla se vybírá podle priority operátorů apod.

2. interní forma může mít tvar abstraktního syntaktického stromu, uspořádanýchčtveřic (operace, 1.operand, 2.operand, výsledek), nebo i jinak. Tvar 2. interníformy závisí na cílovém jazyce překladu nebo na jazyce v němž je programovanýinterpret.Chyb v syntaktické analýze bývá velké množství a bývají často i těžce roze-znatelné. Chybě syntaktické analýzy odpovídá vždy prázdné políčko v tabulceautomatu. Nejčastější chyby syntaktického analyzátoru jsou následující:

• špatné uzávorkování výrazu

• špatné použití (nebo vynechání) klíčového slova

• přiřazení hodnoty do konstanty (např. 5=2*3)

• a mnoho dalších

3.2.3. Generování kódu

Každý překladač musí umět generovat kód cílového jazyka z 2.interní formy.Implementace generátoru kódu závisí na cílovém jazyku a tvaru 2. interní formya proto se různé implementace generátorů kódu mohou výrazně lišit.

3.3. Nástroje pro analýzu kódu

Abychom nemuseli ručně psát analyzátor kódu, existují nástroje, které tutopráci udělají za nás. V následujících podkapitolách se blíže seznámíme s těmianalyzátory, které byly použity pro tvorbu SLLL překladače.

3.3.1. Flex

Flex je nástroj na tvorbu lexikálního analyzátoru. Nejprve musíme vytvořitsoubor následující struktury:

16

%{Vložení knihoven, deklarace proměnných a funkcí

%}definice regulárních výrazů%%pravidla pro dané regulární výrazy%%uživatelský kód

Pak zavoláme program Flex s parametrem, kterým bude jméno souboru s výšeuvedenou strukturou, čímž se nám vygeneruje kód lexikálního analyzátoru vjazyce C. Následující vzory (jen ty nejdůležitější) odpovídají zápisu regulárníchvýrazů:

x odpovídá znaku x. odpovídá libovolnému znaku, kromě znaku pro odřádkování[xyz] tzv. třída znaků, v tomto případě vzor odpovídá budznaku x nebo y nebo z[a-z] třída znaků, odpovídající malému písmenu anglické abecedy[ˆ0-9] negace třídy znaků, tj. odpovídající znak je libovolný znak kromě číslicr* uzávěr, kde r je regulární výrazr+ pozitivní uzávěr, kde r je regulární výraz\x2a odpovídá znaku o hexadecimální hodnotě 2axyz odpovídá slovu xyz{Jméno} použití definice ”Jméno” (viz. níže)

Definice regulárních výrazů vypadá následovně:Jméno regulární výraz

Pravidlo pro regulární výrazy má tvar:Regulární výraz {zpracování daného regulárního výrazu}

Dále tu máme speciální datové typy, proměnné a funkce, se kterými Flex pracuje:

• union YYSTYPE — struktura, která v sobě nese proměnné různých dato-vých typů, do kterých se ukládají hodnoty atomů (tuto strukturu uživateldefinuje sám)

• char yytext[ ] — v této proměnné se nachází hodnota atomu

• FILE *yyin — soubor, který se má analyzovat (nutno otevřít pomocí funkcefopen)

• int yylex() — vrátí celočíselnou konstantu odpovídající právě načtenémuatomu

17

3.3.2. Bison

Bison je nástroj na tvorbu syntaktického analyzátoru. Nejprve musímevytvořit soubor následující struktury:

%{Vložení knihoven, deklarace proměnných a funkcí

%}deklarace terminálních i neterminálních symbolů%%pravidla gramatiky a jejich zpracování%%uživatelský kód

Pak zavoláme program Bison s parametrem, kterým bude jméno souboru s výšeuvedenou strukturou, čímž se nám vygeneruje kód syntaktického analyzátoru vjazyce C. Deklarace terminálních symbolů (atomů, které rozpoznává lexikálníanalyzátor) a neterminálních symbolů vypadá následovně:

%token term1, term2,...%token <s> term3, term4,...%type <x> neterm1, neterm2,...

Pro doplnění, x a s jsou proměnné deklarované ve struktuře YYSTYPE (viz.předchozí podkapitola). V proměnné s jsou uloženy hodnoty atomů, do proměnnéx se uloží výsledek zpracování pravidla, odpovídající danému neterminálu. Prořešení konfliktů (hlavně u operátorů) máme další deklarace:

%right ’=’%left ’+’ ’-’%left ’*’ ’/’

A konečně deklarace startovacího symbolu:%start startsymbol

Dále máme neméně důležitou část, kde uvádíme jednotlivá pravidla gramatiky ak nim kód jejich zpracování. Tato část vypadá následovně:

neterm1: term1 neterm2 {zpracování pravidla}| term2 {zpracování pravidla};

Při psaní kódu pro zpracování pravidel se uplatňují následující symboly:

18

• $$ — Tento symbol označuje proměnnou, která odpovídá neterminálu nalevé straně daného pravidla.

• $i i∈{1,. . . ,n} — Tento symbol označuje proměnnou, která odpovídá ter-minálu nebo netrerminálu na pravé straně daného pravidla.

Dále tu máme funkce, se kterými Bison pracuje:

• int yyparse() — Spustí se syntaktická analýza, po jejím úspěšném provedeníje návratová hodnota funkce 0.

• void yyerror(char* errmsg) — Funkce, která slouží pro obsloužení syntak-tické chyby.

3.4. Implementace

Při implementaci programovacího jazyka bylo využito programu pro genero-vání lexikálního analyzátoru Flex a programu pro generování syntaktického ana-lyzátoru Bison. Spolupráce těchto analyzátorů je plně automatická, není nutnotedy implementovat nějakou vazbu mezi nimi. Pro uložení a zpracování 2. interníformy jsem nadefinoval následující struktury:

• struktura YYSTYPE obsahující datové typy, které jsou zapotřebí pro prácianalyzátorů, má tvar:

union YYSTYPE {char s[1024];atom *a;arg *x;arglist *xl;CAtlArray<arg*> *xa;formula *f;clause *c;

};

• struktura arg popisující jednotlivý argument má tvar:

struct arg {int type;CString x;

};

• struktura arglist popisující seznam argumentů má tvar:

19

struct arglist {arglist *next;arg *a;

};

• struktura atom popisující atomickou formuli má tvar:

struct atom {bool lin;bool lin2;bool parsed;CString name;CAtlArray<arg*> args;

};

• struktura formula popisující formuli má tvar:

struct formula {int op;int type;int lnum;atom *a;CString num;CString var;formula *left;formula *right;

};

• struktura clause popisující klauzuli (pravidlo) má tvar:

struct clause {formula *f;atom *a;

};

• struktura err popisující chybu má tvar:

struct err {CString s;

20

int l;};

Následují globální proměnné, které slouží k uložení 2. interní formy, ty jsou defi-novány následovně:

• Proměnná pro uchování seznamu faktů.

CAtlArray<atom*> g_decl;

• Proměnná pro uchování seznamu klauzulí (pravidel).

CAtlArray<clause*> g_clause;

• Proměnná pro uchování seznamu chyb.

CAtlArray<err*> g_err;

• Proměnná pro uchování uživatelského dotazu.

formula *goal;

3.4.1. Lexikální analyzátor

Lexikální analyzátor je vytvořen pomocí nástroje Flex. Následující symbolyjsou rozpoznávány lexikálním analyzátorem:

[\n] nový řádek, čítač počtu řádků se inkrementuje[ \t] mezera, tabulátor, vynechá se”%%”[ˆ\n]∗ poznámka, vynechá se”[”[ˆ]\n]∗”]” seznam, hodnota se načte do proměnné typu řetězec”\””[ˆ”\n]∗”\”” řetězec, hodnota se načte do řetězce”:-” oddělovač mezi levou a pravou částí pravidla”+” sčítání a disjunkce”-” odčítání”∗” násobení a konjunkce”/” celočíselné dělení”(” levá závorka”)” pravá závorka

21

”<=” menší nebo rovno”>=” větší nebo rovno”==” rovno”!=” nerovno”<” menší”>” větší”=” přiřazení”neg” negace”once” jediné řešení”.” symbol pro ukončení faktu, nebo pravidla”,” oddělovač” ” symbol označující jakoukoli proměnnou, hodnota se načte do pro-

měnné typu řetězec”:” oddělovač mezí u pole”succ” atomická formule, vždy se vyhodnotí úspěšně”fail” atomická formule, vždy se vyhodnotí neúspěšně”one” atomická formule, vyhodnotí se úspěšně, právě když neexistuje ne-

spotřebovaný lineární fakt”goal” klíčové slovo označující uživatelský dotaz”lin” klíčové slovo označující lineární fakt[0-9]∗ celé číslo, hodnota se načte do proměnné typu řetězec[a-z][a-zA-Z0-9]∗ atom jazyka, hodnota se načte do proměnné typu řetězec[A-Z][a-zA-Z0-9]∗ proměnná, hodnota se načte do proměnné typu řetězec. neznámý znak, vygeneruje se chybové hlášení

3.4.2. Syntaktický analyzátor

Syntaktický analyzátor je vytvořen pomocí nástroje Bison. Terminálnímsymbolům gramatiky budou odpovídat symboly získané při lexikální analýze,jen pro upřesnění uvedu některá označení terminálních symbolů, která nemusíbýt na první pohled zřejmá:

• var — označuje proměnnou (včetně symbolu ” ”)

• list — označuje seznam

• string — označuje řetězec

• int — označuje celé číslo

• atom — označuje atomickou formuli

Následující gramatika popisuje jazyk SLLL jako celek, startovací symbol jeprogram. U každého pravidla je slovně popsáno jeho zpracování.

22

program → comm goal formula . do proměnné goal přiřadí, výslednou cílovou for-muli a ukončí analýzu uspěchem

comm → decl comm přidá fakt do seznamu g decl→ decl přidá fakt do seznamu g decl→ clause comm přidá klauzuli do seznamu g clause→ clause přidá klauzuli do seznamu g clause

decl → lin atom args1 . vrátí lineární fakt→ atom args1 . vrátí nelineární fakt

args1 → ( arg1 ) vrátí seznam argumentů→ ε vrátí prázdný seznam argumentů

arg1 → arg11 vytvoří seznam argumentů→ arg1 , arg1 spojí 2 seznamy argumentů

arg11 → var vrátí argument typu proměnná→ int vrátí argument typu číslo→ -int vrátí argument typu záporné číslo→ atom vrátí argument typu atom, který není atomickou

formulí, nýbrž má stejnou syntaxi→ string vrátí argument typu řetězec→ int : int vrátí argument typu pole→ list vrátí argument typu seznam

clause → atom args1 :- formula . vrátí klauzuli (pravidlo)args2 → ( arg2 ) vrátí seznam argumentů

→ ε vrátí prázdný seznam argumentůarg2 → arg21 vytvoří seznam argumentů

→ arg2 , arg2 spojí 2 seznamy argumentůarg21 → var vrátí argument typu proměnná

→ int vrátí argument typu číslo→ -int vrátí argument typu záporné číslo→ atom vrátí argument typu atom, který není atomickou

formulí, nýbrž má stejnou syntaxi→ string vrátí argument typu řetězec→ list vrátí argument typu seznam

23

formula → formula ∗ formula vrátí formuli typu konjunkce→ formula + formula vrátí formuli typu disjunkce→ neg formula1 vrátí formuli typu negace→ once formula1 vrátí formuli typu jediné řešení→ ( formula ) vrátí formuli→ formula1 vrátí formuli

formula1 → atom args2 vrátí atomickou formuli→ succ vrátí speciální formuli, která se vždy vyhodnotí

úspěšně→ fail vrátí speciální formuli, která se vždy vyhodnotí ne-

úspěšně→ one vrátí speciální formuli, která se vyhodnotí úspěšně,

právě když neexistuje nespotřebovaný lineární fakt→ ( let ) vrátí formuli typu přiřazení→ ( comp ) vrátí formuli typu porovnání

let → var = expr sestaví formuli typu přiřazenícomp → expr == expr vrátí porovnání rovnosti

→ expr != expr vrátí porovnání nerovnosti→ expr > expr vrátí porovnání větší než→ expr < expr vrátí porovnání menší než→ expr <= expr vrátí porovnání menší nebo rovno→ expr >= expr vrátí porovnání větší nebo rovno

expr → expr + expr vrátí výraz sčítání→ expr - expr vrátí výraz odčítání→ expr ∗ expr vrátí výraz násobení→ expr / expr vrátí výraz celočíselné dělení→ ( expr ) vrátí výraz→ var vrátí proměnnou→ +var vrátí proměnnou→ -var vrátí zápornou hodnotu proměnné→ int vrátí číslo→ +int vrátí číslo→ -int vrátí zápornou hodnotu čísla

Mechanismus rozpoznávání syntaktických chyb je založen na tom, že do stávajícígramatiky, přidáme další pravidla, která nám budou rozpoznávat chyby. Dálejsou uvedena pravidla, která slouží k detekci některých chyb:

24

program → comm chybí uživatelský dotaz→ ε prázdný program

args1 → ( arg1 chybí pravá závorkaargs2 → ( arg2 chybí pravá závorkaformula → ( formula chybí pravá závorkaformula1 → ( let chybí pravá závorka

→ ( comp chybí pravá závorkalet → int = expr levý operand nesmí být čísloexpr → ( expr chybí pravá závorka

Ostatní chyby jsou označeny jako syntaktické chyby bez udání bližších podrob-ností.

3.4.3. Úprava 2. interní formy

Protože Prolog neumí pracovat s lineárními fakty, musíme tuto činnostnasimulovat. Využít můžeme Prologovských seznamů do niž vložíme všechnylineární fakty a při použití je odstraníme. Abychom tyto seznamy udrželikonzistentní, je potřeba rozšířit pravidla o další proměnné: vstupní a výstupníseznam. Následující algoritmus byl vytvořen proto, abychom zjistili, kterápravidla pracují s lineárními fakty, nebo s pravidly, která využívají lineární fakty.Navíc díky stromové struktuře uložení formulí můžeme zjistit rozložení těchtopravidel, či lineárních faktů, což nám pomůže při generování kódu.

Algoritmus pro zjištění pravidel pracujících s lineárními fakty:VSTUP: 2. interní forma, ve které jsou uloženy fakty, pravidla i uživatelský dotaz.Všechna pravidla mají příznaky lin, lin2,parsed položeny jako nepravdivé a číslolnum=0VÝSTUP: upravená 2. interní forma o příznaky a rozložení lineárních faktů apravidel využívajících lineárních faktů

1. Pro formuli uživatelského dotazu a prázdný atom provedeme krok 2

2. Pro atom a a formuli f budeme provádět následující činnost:

• pokud a není prázdný, pak nastavíme příznak parsed jako pravdivý

• je-li typ f logická operace pak pro levý a pravý (je-li k dispozici) ope-rand a atom a provedeme krok 2, dále pro jednotlivé operace upravímečíslo lnum (označující rozložení lineárních faktů) následovně:

konjunkce — lnum = lnumleft + lnumright

disjunkce — lnum = max(lnumleft + lnumright)

negace — lnum = lnumleft

25

jediné řešení — lnum = lnumleft

Pak pokračujeme krokem 3

• je-li typ f atomická formule, pak prohledáme fakty a nalezneme-li ta-kový lineární fakt, který má stejné jméno a shodný počet argumentůjako tato atomická formule, pak u této formule nastavíme příznaky lin,lin2 na pravdivé a číslo lnum inkrementujeme a pokud není a prázdný,pak jeho příznak lin2 položíme jako pravdivý. Neexistuje-li lineárnífakt odpovídající výše uvedeným vlastnostem, pak nalezneme všechnapravidla, kde levá strana má stejné jméno a stejný počet proměnnýchjako atomická formule. Pak pro všechna tato pravidla provedeme:

– má-li atom (levá strana pravidla) příznak parsed jako nepravdivý,pak provedeme krok 2, kde atom bude levá strana pravidla a for-mule pravá strana pravidla

– pokud má atom (levá strana pravidla) pravdivý příznak lin2, pakzměníme příznak lin2 u atomické formule na pravdivý a inkre-mentujeme číslo lnum a je-li a neprázdný, pak jeho příznak lin2položíme rovněž jako pravdivý. Tyto změny lze provést nejvýšejednou, pro danou atomickou formuli

– není-li splněna předchozí podmínka, pak zkoumáme zda má ato-mická formule stejné jméno a počet argumentů jako a, pak polo-žíme u ní příznak lin2 jako pravdivý a číslo lnum položíme rovno1. Tyto změny lze provést nejvýše jednou, pro danou atomickouformuli a je-li a neprázdný

Pak pokračujeme krokem 3

• pro speciální formuli one, položíme číslo lnum rovno 0 a pokud je aneprázdný, položíme jeho příznak lin2 na pravdivý. Pak pokračujemekrokem 3

3. Nakonec pro každý nelineární fakt budeme hledat pravidlo, jehož levá stranamá stejné jméno a shodný počet argumentů a navíc pravdivý příznak lin2nastavíme příznak lin2 u tohoto faktu rovněž na pravdivý.

3.4.4. Generování kódu

Na začátek je potřeba vložit do přeloženého programu speciální fakty a pravi-dla, pomocí kterých budeme emulovat lineární logiku v Prologu. Nejprve potřebu-jeme nějak definovat lineární fakt. Předpokládejme, že máme seznam lineárníchfaktů (jeho tvorba viz. níže) a potřebujeme v souladu s lineární logikou zařídit to,aby při použití tohoto faktu byl tento fakt odstraněn ze seznamu, pokud tam jižnení, pak použití tohoto faktu skončí neúspěšně. Abychom tohoto dosáhli stačídefinovat (použití viz. níže):

26

linear(V,[V|L],L).linear(V,[H|L],[H|NL]) :- linear(V,L,NL).

Dále potřebujeme definovat fakt, který nám přesune jeden seznam do druhého(použití viz. níže):

same(X,X).

A nakonec definujeme fakt na test prázdnoty seznamu (použití viz. níže):

empty([]).

Jelikož máme agrumenty uložené v seznamu, je zapotřebí abychom je dostalido řetězce, který podporuje syntaxi Prologu. K tomu je zapotřebí následujícíhoalgoritmu:

Algoritmus pro generování řetězce argumentůVSTUP: Seznam argumentů, příznak t, čísla l1, l2VÝSTUP: Řetězec argumentů

• Pokud je seznam argumentů prázdný vrátí prázdný řetězec

• Projde se seznam argumentů, narazí-li se na typ argumentu pole, pak seprovede následující činnost:

– zjistíme meze, které jsou uloženy v řetězci označujícím hodnotu tohotoargumentu (meze označíme lo a hi)

– změníme typ tohoto argumentu na typ číslo

– vyprázdníme řetězec s

– pak provedeme cyklus pro i od lo do hi, kde v každém kroku pozmě-níme hodnotu tohoto argumentu na hodnotu i (číslo převedeme nařetězec, jelikož se v něm ukládá hodnota číselného argumentu) a re-kurzivně zavoláme algoritmus pro generování řetězce argumentů, pronáš pozměněný seznam argumentů a příznak t a čísla l1,l2 (příznaki čísla jsou shodné s těmi, co do algoritmu původně vstupovaly). Vý-stupní řetězec po provedení rekurzivně volaného algoritmu připojímek řetězci s, dále k řetězci s připojíme znak pro ukončení řádku.

– nakonec změněný argument dáme zpět do původní podoby (typ polea hodnota, kterou měl před změnou) a vrátíme řetězec s

• řetězec s nastavíme na hodnotu ”(”

• pro každý argument ze seznamu, připojíme do řetězce s hodnotu argumentua znak ”,”

27

• Pokud je příznak t roven:

– 0 — nahradíme poslední znak v řetězci s znakem ”)”

– 1 — připojíme k řetězci s řetězec ”LIN l1,LIN l2 )”

– 2 — připojíme k řetězci s řetězec ”LIN 0,LIN 0)”

• vrátíme řetězec s

Pro generování formulí (pravých stran pravidel a uživatelského dotazu) budezapotřebí algoritmu, který převede stromovou strukturu uložení formule (viz.struktura formule) na řetězec a navíc využije výsledek algoritmu pro zjišťovánípravidel pracujících s lineárními fakty tak, aby rozpoznal použití lineárního faktua zajistil správné předávání seznamu lineárních faktů při zpracovávání formule.Nutno podotknout, že struktura formule dokáže popsat nejen logické operacemezi formulemi, ale i atomické formule, speciální formule, přiřazení, porovnání avýrazy (včetně proměnných a číselných konstant). Nyní už zmíněný algoritmus:

Algoritmus pro generování formule v řetězciVSTUP: Formule f, čísla begin,add, příznak lVÝSTUP: Řetězec s vyjadřující formuli

• Nechť f je aktuální uzel struktury formule, pak pokud je jeho typ roven:

– proměnné nebo číslu, pak do s přiřadíme hodnotu čísla, nebo proměnné

– přiřazení, pak rekurzivně zavoláme tento algoritmus pro levý a pravýpodstrom uzlu f, kde ostatní vstupní parametry budou shodné s těmi,co vstupovaly do stávajícího algoritmu. Pak řetězec s vznikne zřetěze-ním výsledku volání algoritmu pro levý podstrom, klíčového slova ”is”a výsledku volání algoritmu pro pravý podstrom.

– výraz, nebo porovnání, pak obdobně jako u přiřazení rekurzivně zavo-láme tento algoritmus pro levý a pravý podstrom uzlu f, kde ostatnívstupní parametry budou shodné s těmi, co vstupovaly do stávajícíhoalgoritmu. Pak řetězec s vznikne zřetězením výsledku volání algoritmupro levý podstrom, příslušného operátoru v jazyce Prolog a výsledkuvolání algoritmu pro pravý podstrom.

– speciální formule, pak je-li hodnota speciální formule rovna:

∗ succ — do s přiřadíme hodnotu ”true”

∗ fail — do s přiřadíme hodnotu ”fail”

∗ one — do s přiřadíme hodnotu ”empty(LIN begin)”

28

– atomická formule, pokud je příznak lin u této atomické formule prav-divý, pak zavoláme algoritmus pro generování řetězce argumentů sparametry: seznam argumentů dané atomické formule, příznak t ro-ven 0 a čísla l1,l2 rovněž rovna 0. Pak do řetězce s přiřadíme”linear(jméno formule argumenty, LIN begin, LIN begin+1 )”. Jinak,pokud je příznak lin u této atomické formule nepravdivý, pak zavolámealgoritmus pro generování řetězce argumentů s parametry: seznam ar-gumentů dané atomické formule, příznak t roven 1 pro pravdivé hod-noty příznaků ll a lin2 (u této atomické formule), jinak 0, číslo l1rovno begin, číslo l2 rovno begin+add+1. Pak řetězec s vznikne spoje-ním jména atomické formule a řetězce argumentů.

– logická operace, pak je-li operace:

∗ jediné řešení, pak rekurzivně zavoláme tento algoritmus pro levýpodstrom uzlu f, kde ostatní vstupní parametry budou shodné stěmi, co vstupovaly do stávajícího algoritmu. Do řetězce s přiřa-díme ”once(levá formule)”.

∗ negace, pak rekurzivně zavoláme tento algoritmus pro levý pod-strom uzlu f, kde ostatní vstupní parametry budou shodné s těmi,co vstupovaly do stávajícího algoritmu. Do řetězce s přiřadíme”not(levá formule)”. Je-li ovšem levá podformule atomická a zá-roveň její příznak lin2 je pravdivý, pak k řetězci s připojíme”,same(LIN begin, LIN begin+add+1 )”.

∗ konjunkce, pak rekurzivně zavoláme tento algoritmus pro levýpodstrom uzlu f, kde ostatní vstupní parametry budou shodnés těmi, co vstupovaly do stávajícího algoritmu. Pro pravý pod-strom zavoláme rovněž tento algoritmus, akorát parametr beginbude roven součtu současného begin a add a také čísla lnum u le-vého podstromu a parametr add bude roven 0. Řetězec s vzniknezřetězením výsledku volání algoritmu pro levý podstrom, symbolu”,” a výsledku volání algoritmu pro pravý podstrom.

∗ disjunkce, pak rekurzivně zavoláme tento algoritmus pro levýpodstrom uzlu f, kde vstupní parametr begin bude shodný sevstupním parametrem begin, parametr add bude roven rozdílučísel lnum pravého a levého podstromu nebo nulový, pokud bytento rozdíl byl záporný. Je-li lnum levého podstromu nulové alnum pravého podstromu kladné, pak k výsledku rekurzivníhovolání algoritmu připojíme ”,same(LIN begin, LIN begin+right->lnum)”. Pro pravý podstrom zavoláme rovněž tento algorit-mus, akorát parametr add bude roven rozdílu čísel lnum levéhoa pravého podstromu, nebo nulový pokud by tento rozdíl bylzáporný. Je-li lnum pravého podstromu nulové a lnum levéhopodstromu kladné, pak k výsledku rekurzivního volání algoritmu

29

připojíme ”,same(LIN begin, LIN begin+left->lnum)”. Řetězec svznikne zřetězením výsledku volání algoritmu pro levý podstrom,symbolu ”;” a výsledku volání algoritmu pro pravý podstrom.

• Vrátíme s

A teď již k vlastnímu generování kódu, se kterým bude pracovat Prolog.Algoritmus je následující:

Algoritmus pro generování kóduVSTUP: 2. interní forma upravená algoritmem pro zjištění pravidel pracujících slineárními faktyVÝSTUP: vygenerovaný Prologovský kód a řetězec obsahující uživatelský dotaz

1. Řetězec llist nastavíme jako prázdný. Do souboru uložíme fakty a pravidla,umožňující emulaci lineární logiky v Prologu:

linear(V,[V|L],L).linear(V,[H|L],[H|NL]) :- linear(V,L,NL).same(X,X).empty([]).

2. Pro každý fakt v seznamu g decl budeme provádět následující činnost:

• pokud je fakt nelineární (tj. příznak lin je nepravdivý), pak zavolámealgoritmus pro generování řetězce argumentů, kde jako parametry uve-deme: seznam argumentů daného faktu, příznak t roven 2, pokud pří-znak lin2 je pravdivý, 0 pokud ne, čísla l1,l2 rovna 0. Je-li výstuptohoto algoritmu jednořádkový (tj. mezi argumenty nebylo pole), pakdo souboru zapíšeme jméno faktu, řetězec argumentů a symbol ”.”.Je-li výstup tohoto algoritmu víceřádkový (tj. mezi argumenty bylopole), pak pro každý řádek zapíšeme do souboru: jméno faktu, danýřádek řetězce argumentů, symbol ”.”.

• pokud je fakt lineární (tj. příznak lin je pravdivý), pak zavoláme al-goritmus pro generování řetězce argumentů, kde jako parametry uve-deme: seznam argumentů daného faktu, příznak t roven 0, čísla l1,l2také rovna 0. Je-li výstup tohoto algoritmu jednořádkový (tj. meziargumenty nebylo pole), pak k řetězci llist připojíme jméno faktu,řetězec argumentů a symbol ”,”. Je-li výstup tohoto algoritmu více-řádkový (tj. mezi argumenty bylo pole), pak do řetězce llist připojímejméno faktu, onen výstupní řetězec argumentů, kde budou oddělovačeřádků nahrazeny symbolem ”,” a jménem faktu. Nakonec z řetězce

30

llist odstraníme poslední výskyt jména faktu (ten přebývá a nemá zasebou řetězec argumentů).

3. pro každou klauzuli (pravidlo) ze seznamu g clause budeme provádět ná-sledující činnost.

• Pokud je příznak lin2 nepravdivý u levé strany dané klauzule, pakprohledáme jednotlivé klauzule se stejnou levou stanou, neexistuje-litaková, kde příznak lin2 u levé strany vyhledané klauzule bude prav-divý, pak zavoláme algoritmus pro generování řetězce argumentů, kdejako parametry uvedeme: seznam argumentů dané levé strany klau-zule, příznak t roven 2, číslo l1 rovno 0 , číslo l2 rovno číslu lnum upravé strany dané klauzule.

• Jinak opět zavoláme algoritmus pro generování řetězce argumentů, kdejako parametry uvedeme: seznam argumentů dané levé strany klauzule,příznak t roven 1, je-li příznak lin2 u levé strany klauzule pravdivý,jinak 0, číslo l1 rovno 0 , číslo l2 rovno číslu lnum u pravé strany danéklauzule.

Pak zavoláme algoritmus pro generování formule v řetězci, kde jako para-metry uvedeme: pravá strana klauzule, čísla begin, add rovna 0, příznak llroven příznaku lin2 u levé strany klauzule. Je-li výstup algoritmu pro gene-rování argumentů jednořádkový, pak do souboru zapíšeme jméno levé stranyklauzule, řetězec argumentů, pak řetězec ”:-”, pak řetězec pravé strany pra-vidla (formule) a nakonec symbol ”.”. Je-li výstup algoritmu pro generováníargumentů víceřádkový, pak pro každý řádek zapíšeme do souboru jménolevé strany klauzule, řetězec argumentů na daném řádku, pak řetězec ”:-”,pak řetězec pravé strany pravidla (formule) a nakonec symbol ”.”. danémřádku

4. Nakonec do souboru zapíšeme seznam lineárních faktů: ”linlist([llist ]).”.

5. Řetězec pro uživatelský dotaz vznikne zřetězením ”linlist(LIN 0),” a vý-sledkem volání algoritmu pro generování formule v řetězci pro parametry:formule goal, čísla begin,add rovna 0, příznak ll pravdivý. Nakonec ještěpřidáme symbol ”.”.

Následující příklad nám ještě lépe osvětlí, jak překladač funguje. Nejprve mámeprogram v jazyce SLLL:

lin a(1:2).r(0).r(X) :- (X1=X-1)*a(X1).goal r(2).

31

Po vykonání lexikální a syntaktické analýzy obdržíme seznamy g decl a g clausea formuli goal, které včetně důležitých příznaků vypadají následovně:

• g decl — dvouprvkový seznam faktů

• g clause — jednoprvkový seznam pravidel

• goal — formule uživatelského dotazu

32

Následuje použití algoritmu pro zjištění pravidel pracujících s lineárními fakty.Tento algoritmus aplikujeme na uživatelský dotaz, který má v tomto případě tvarr(2). Jelikož jde o atomickou formuli, pak v prvé řadě zkoumáme, zda neexistujelineární fakt stejného jména a počtu argumentů. Ten v tomto případě neexistuje,tak pokračujeme prohledáváním pravidel, jehož levá strana má stejné jméno apočet argumentů. Takové pravidlo existuje r(X) :- (X1=X-1)*a(X1). a nebyloještě algoritmem prohledáváno, pak nastavíme příznak parsed na pravdivý a zna-mená to tedy, že se algoritmem začne prohledávat pravá strana tohoto pravidla.Nyní prohledáváme aktuální uzel obsahující symbol konjunkce, znamená to tedyprohledat levý a pravý podstrom a sečíst čísla lnum těchto podstromů. Levýpodstrom obsahuje přiřazení X1=X-1, což není lineární fakt a tudíž se dál nepro-hledává. Pravý podstrom obsahuje atomickou formuli a(X1). Aplikováním algo-ritmu na tuto atomickou formuli zjistíme, že existuje lineární fakt mající stejnéjméno a stejný počet argumentů a(1:2) a tudíž příznaky lin a lin2 nastavímejako pravdivé a číslo lnum inkrementujeme. Pak u levé strany pravidla nastavímepříznak lin2 jako pravdivý. Vrátíme se tedy k prohledávání uživatelského dotazutvaru r(2). Jelikož jsme zjistili, že pravidlo r(X) :- (X1=X-1)*a(X1). pracuje slineárními fakty, pak nastavíme příznak lin2 jako pravdivý. Nakonec prohledámevšechny nelineární fakty. Nalezneme pouze jediný tvaru r(0). Pak prohledámepravidla, ve kterých má levá strana shodné jméno a počet argumentů. V tomtopřípadě nalezneme jediné takové pravidlo r(X) :- (X1=X-1)*a(X1). Toto pra-vidlo pracuje s lineárními fakty, proto příznak lin2 u faktu r(0). nastavíme jakopravdivý. Nyní uvidíme v grafické podobě jak se změnila 2.interní forma použi-tím algoritmu pro zjištění pravidel pracujících s lineárními fakty (čísla lnum jsouuvedena nad uzlem):

• g decl

• g clause

33

• goal

Nyní už můžeme přistoupit ke generování kódu v jazyce Prolog. Nejprve vygene-rujeme kód, který se používá k práci s lineárními fakty. A ten má tvar:

linear(V,[V|L],L).linear(V,[H|L],[H|NL]) :- linear(V,L,NL).same(X,X).empty([]).

Pak můžeme přistoupit ke generování faktů. Fakt a(1:2) je lineární, tudíž povygenerování řetězců argumentů tvaru:

(1)(2)

34

přidáme do prozatím prázdného řetězce llist řetězec: "a(1),a(2),", kterývznikne zřetězením jména faktu a a řetězce argumentů, kde odřádkování na-hradíme řetězcem ",a" a poslední výskyt jména faktu a odstraníme. Fakt r(0)není lineární, ovšem příznak lin2 je pravdivý, tak při použití algoritmu pro ge-nerování řetězce argumentů použijeme příznak t roven 2. Pak tento fakt budemít v Prologu ekvivalent: r(0,LIN 0,LIN 0). Pak už nám zbývá přeložit jenpravidlo r(X) :- (X1=X-1)*a(X1). Nejprve vygenerujeme pravou část pravi-dla, k čemuž slouží algoritmus pro generování formule v řetězci. Ten zavolámepro čísla begin a add rovna 0 a příznak ll pravdivý. Nejprve narazíme na uzelobsahující konjunkci, což znamená, že se algoritmus rozvětví pro levý a pravýpodstrom. Levý podstrom obsahuje přiřazení a číslo lnum je u něj rovno 0, protopro pravý podstrom zavoláme algoritmus pro generování formule v řetězci s číslybegin a add rovna 0. Pravý podstrom obsahuje atomickou formuli, kde podlepravdivého příznaku lin poznáme, že se jedná o lineární fakt. Pak tedy algo-ritmus vygeneruje řetězec: linear(a(X1),LIN 0,LIN 1). Celá pravá strana pakvypadá: X1 is X-1,linear(a(X1),LIN 0,LIN 1). Levá strana pravidla pak do-stane podobu r(X,LIN 0,LIN 1), protože příznak lin2 je pravdivý a číslo lnum upravé strany pravidla je rovno 1. Celé pravidlo tedy bude mít v Prologu ekvi-valent: r(X,LIN 0,LIN 1) :- X1 is X-1,linear(a(X1),LIN 0,LIN 1). Nynízbývá do programu vložit seznam lineárních faktů: linlist([a(1),a(2)]). Pře-ložený program do Prologu má tvar:

linear(V,[V|L],L).linear(V,[H|L],[H|NL]) :- linear(V,L,NL).same(X,X). empty([]).

r(0,LIN_0,LIN_0).

r(X,LIN_0,LIN_1) :- X1 is (X-1),linear(a(X1),LIN_0,LIN_1).

linlist([a(1),a(2)]).

Nyní zbývá už jen vygenerovat řetězec uživatelského dotazu. Opět použijeme al-goritmus pro generování formule v řetězci a z něho dostaneme r(2,LIN 0,LIN 1),protože příznak lin2 je pravdivý a čísla begin a add nulová. Celý uživatelský dotazmá tvar: linlist(LIN 0),r(2,LIN 0,LIN 1). Atomická formule linlist se dávána začátek proto, abychom do výpočtu dostali správný seznam lineárních faktůa nemuseli celý tento seznam uvádět přímo v uživatelském dotazu.

3.5. Uživatelské prostředí

Aplikace je vytvořena pro prostředí Windows, tudíž se spustí v okně. Oknose rozděluje na dvě části:

35

• horní část — slouží k psaní programu v jazyce SLLL

• dolní část — slouží k výpisům chyb při překladu, či uživatelského dotazu,proběhl-li překlad správně

Menu aplikace obsahuje tyto funkce:

• File

– New — založí nový dokument

– Open — otevře soubor

– Save — uloží soubor

– Save As — uloží soubor jako. . .

– Exit — zavře aplikaci

• Edit

– Undo — krok zpět

– Cut — odstraní označený text a přesune ho do schránky

– Copy — zkopíruje označený text do schránky

– Paste — vloží text ze schránky na pozici kurzoru

• Compile

– Set PROLOG Path — nastaví cestu k Prologu

– Compile and Run — přeloží program do Prologu a spustí Prolog auživatelský dotaz zkopíruje do schránky

• Help

– Help — zobrazí nápovědu

– About — zobrazí dialog o aplikaci

Ještě pro připomenutí. Po překladu programu z jazyka SLLL do Prologu se zko-píruje uživatelský dotaz do schránky. Po spuštění Prologu tedy stačí na příkazovýřádek vložit uživatelský dotaz ze schránky.

3.5.1. Soubor slll.ini

Tento soubor slouží k uložení nastavení aplikace. V tomto souboru je uloženacesta k Prologu.

36

3.6. Příklady

V této podkapitole si ukážeme příklady, které se dají řešit pomocí jazykaSLLL. Ovšem jazyk SLLL funguje jako překladač do Prologu, ve kterém pouzeemulujeme práci s lineárními fakty, což se projeví na nižší efektivitě při výpočtuodpovědi na uživatelský dotaz.

3.6.1. Eulerův tah

Eulerův tah, je takový tah, který pokryje celý graf a každá hrana je v němobsažena právě jednou. Máme dán následující graf:

Na tomto grafu budeme hledat Eulerův tah, k tomu nám pomůže následujícíprogram v jazyce SLLL.

lin r(1,2). lin r(1,3). lin r(1,4). lin r(2,3). lin r(2,4). linr(3,4). lin r(3,5). lin r(4,5).

%%outputw([]).w([I|X]) :- w(X)*write(I)*write(",").

%%main programtah(X,L) :- one*w([X|L]).tah(X,L) :- (r(X,N)+r(N,X))*tah(N,[X|L]).

goal tah(2,[]).

Lineární fakty r nám označují hrany grafu. Pravidla tah nám zase vyjadřují hle-dání Eulerova tahu, respektive jeho nalezení a pravidlo w nám zajišťuje výpis.

37

Uživatelský dotaz nám říká, že hledáme Eulerův tah z počátkem v uzlu 2. Násle-dující obrázek nám ukáže jedno z možných řešení:

3.6.2. Hamiltonova kružnice

Hamiltonova kružnice je taková kružnice, která pokrývá celý graf. Máme dánnásledující graf:

Na tomto grafu budeme hledat Hamiltonovu kružnici, k čemuž nám pomůže ná-sledující program v jazyce SLLL:

lin u(1:4).

h(1,2:4). h(2,3). h(3,4).

%%outputw([]).w([I|X]) :- w(X)*write(I)*write(",").

38

%%main programham(X,F,L) :- one*(h(X,F)+h(F,X))*w([F|L]).ham(X,F,L) :- (h(X,Y)+h(Y,X))*u(Y)*ham(Y,F,[Y|L]).

hamilton :- u(F)*ham(F,F,[F]).

goal hamilton.

Lineární fakty u nám vyjadřují uzly grafu. Nelineární fakty h vyjadřují jednotlivéhrany grafu. Pravidlo w zajišťuje výpis seznamu uzlů, pravidla ham nám sloužík vyhledávání dalšího nenavštíveného uzlu, nebo pokud už jsou všechny uzlynavštívené, spustíme výpis, existuje-li hrana do prvně navštíveného uzlu. Pravidlohamilton nám spustí výpočet pro první uzel a uživatelský dotaz nám říká, žechceme najít Hamiltonovu kružnici a nezáleží na počátku. Následující obrázeknám ukáže řešení daného problému:

3.6.3. Vodní nádoby

Problém vodních nádob spočívá v tom, že máme 2 různě veliké nádoby a ob-jem, kterého máme dosáhnout (nezáleží na tom v jaké nádobě), přičemž můžemenádoby plnit (vždy do maximálního objemu), vylévat a přelévat. Přelévat mů-žeme jen tak, že přelijeme buď celý objem, nebo jen část objemu v případě, žedruhá nádoba se při přelévání naplní. Tento problém se dá řešit pomocí progra-movacího jazyka SLLL následovně:

lin v(0:5,0:3).

%%outputw([]).w([I,J|X]) :- w(X)*print(I)*write(",")*print(J)*nl.

%%main programj(_,1,X,X) :- w(X).j(1,_,X,X) :- w(X).

39

k(X,Y,L,R) :- (X+Y>0)*v(X,Y)* j(X,Y,[X,Y|L],R).

j(_,Y,L,R) :- k(5,Y,L,R)+k(0,Y,L,R).j(X,_,L,R) :- k(X,3,L,R)+k(X,0,L,R).

j(X,Y,L,R) :- (X1=X+Y)*((X1<=5)*k(X1,0,L,R)+(X1>5)*(Y1=X1-5)*k(5,Y1,L,R)).

j(X,Y,L,R) :- (Y1=X+Y)*((Y1<=3)*k(0,Y1,L,R)+(Y1>3)*(X1=Y1-3)*k(X1,3,L,R)).

goal j(0,0,[],_).

Lineární fakty v nám slouží k tomu, abychom se při hledání řešení nedostalido situace, ve které jsme v historii výpočtu už byli. Pravidlo k se nám staráo to, abychom se neopakovali a stará se i o pořízení záznamu výpočtu, tj.stavy v jednotlivých nádobách. Pravidlo w se nám stará o výpis. První dvěpravidla j nám vyjadřují, že dostaneme-li se na požadovaný objem, pak můžemeukončit výpočet a vypsat řešení. Druhá dvě pravidla j nám vyjadřují, naplnění,či vyprázdnění nádob. Poslední 2 pravidla nám vyjadřují přelévání nádob.Uživatelský dotaz nám říká, že výpočet máme spustit pro obě nádoby prázdné.Následující tabulka nám popisuje možné řešení tohoto problému, pro nádobyvelikosti 3l a 5l a požadovaný objem 1l:

nádoba 5l nádoba 3l5 05 30 33 03 35 1

3.6.4. Tah jezdce

V tomto příkladě máme jezdce na šachovnici a s tím jezdcem máme projítšachovnici tak, aby každé pole navštívil právě jednou. Následující obrázek námukazuje jak šachový jezdec může táhnout:

40

I tento problém lze vyřešit pomocí programu v jazyce SLLL. Program vypadánásledovně:

lin b(1:5,1:5).

%%outputw([]).w([I,J|X]) :- w(X)*print(I)*write(",")*print(J)*nl.

%%main programtour(_,_,[I,J|L]) :- one*w(L).tour(I,J,L) :- b(I,J)*(((I1=I+2)*((J1=J+1)+(J1=J-1)))

+((I1=I-2)*((J1=J+1)+(J1=J-1)))+((I1=I+1)*((J1=J+2)+(J1=J-2)))+((I1=I-1)*((J1=J+2)+(J1=J-2))))*tour(I1,J1,[I1,J1|L]).

goal tour(1,1,[1,1]).

Lineární fakty b nám vyjadřují šachovnici. Pravidlo w nám slouží pro výpis pozic,které jezdec navštívil. Pravidla tour se nám starají o výpočet následujícího tahua zjištění, zda políčko už nebylo navštívené. Výpočet končí v době, kdy všechnapolíčka byla navštívená a vypíše se seznam. Uživatelský dotaz nám říká, odkudjezdec potáhne. Řešení tohoto problému vypadá následovně:

41

3.6.5. Královny

Tento problém spočívá v tom rozestavit na šachovnici n královen tak, aby senavzájem neohrožovaly. Tento problém se řeší pomocí jazyka SLLL následovně:

lin b(1:8,1:8).

%%outputw([]).w([I,J|X]) :- w(X)*print(I)*write(",")*print(J)*nl.

%%main programqueen(0,L) :- w(L).queen(N,L) :- b(I,J)*

once d1(I,J)*once d2(I,J)*once d3(I,J)*once d4(I,J)*once d5(I,J)*once d6(I,J)*once d7(I,J)*once d8(I,J)*(N1=N-1)*queen(N1,[I,J|L]).

d1(9,_). d2(0,_). d3(_,9). d4(_,0). d5(9,_). d5(_,9). d6(9,_).d6(_,0). d7(0,_). d7(_,9). d8(0,_). d8(_,0).

d1(I,J) :- ((I1=I+1)*rem(I1,J)*d1(I1,J)).d2(I,J) :- ((I1=I-1)*rem(I1,J)*d2(I1,J)).d3(I,J) :- ((J1=J+1)*rem(I,J1)*d3(I,J1)).

42

d4(I,J) :- ((J1=J-1)*rem(I,J1)*d4(I,J1)).d5(I,J) :- ((I1=I+1)*(J1=J+1)*rem(I1,J1)*d5(I1,J1)).d6(I,J) :- ((I1=I+1)*(J1=J-1)*rem(I1,J1)*d6(I1,J1)).d7(I,J) :- ((I1=I-1)*(J1=J+1)*rem(I1,J1)*d7(I1,J1)).d8(I,J) :- ((I1=I-1)*(J1=J-1)*rem(I1,J1)*d8(I1,J1)).

rem(I,J) :- b(I,J)+(neg b(I,J)).

goal queen(8,[]).

Lineární fakty b představují políčka šachovnice. Pravidlo w slouží pro výpis po-zic královen. Pravidla queen se starají o umístění královny na šachovnici nebopokud už není co umístit, pak o zavolání výpisu. Pravidla d1-d8 vyjadřují různésměry útoku královen. Pravidlo rem nám slouží k odstranění políčka, nebylo-lijiž odstraněno. Uživatelský dotaz nám říká, že chceme umístit 8 královen. Řešenívypadá následovně:

43

4. Závěr

V této diplomové práci jsem navrhl a implementoval lineární logický progra-movací jazyk SLLL, který funguje jako překladač do Prologu a právě Prolog sestará o interpretaci. Jazyk SLLL podporuje práci s lineárními i nelineárními fakty,pravidla jsou vždy nelineární. Operátory lineární logiky byly použity: multiplika-tivní konjunkce, additivní disjunkce. Ostatní operátory nebyly použity z důvodumalé praktické využitelnosti a poměrně složité implementace.

44

Resumé

This diploma work is about linear logic programming. In this diploma work Ideveloped linear logic programming language SLLL, which is implemented as acompiler to Prolog. SLLL language is designed for Windows platform and canbe executed without .NET Framework. With this language we are able to solveexamples such: Knight tour, Queens, Hamilton circle etc.

45

Reference

[1] Radim Bělohlávek, Matematická logika - poznámky k přednáškám, PřFUPOL, 2003

[2] http://www.inf.upol.cz/vecerka/

[3] Patrick Lincoln, Linear Logic, SRI and Stanford University, 1992

[4] Jean-Yves Girard, Linear Logic: Its Syntax and Semantics, Laboratoire deMathématiques Discretes, Marseille

[5] Jan Wielemaker, SWI-Prolog 5.0 Reference Manual, 2002

[6] http://www.cs.rmit.edu.au/lygon/

[7] Mutsunori Banbara, Design and Implementation of Linear Logic Program-ming Languages, Doctoral Dissertation, University Kobe, 2002

[8] Vilém Vychodil, Příklady Činnosti Interpretu Prologu

[9] Flex, version 2.5 Manual, 1995

[10] Bison Manual, 1995

46