spracherkennungs-und anfrage-aequivalenz von mso, monadischem datalog, und automaten. thomas...
TRANSCRIPT
![Page 1: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/1.jpg)
Spracherkennungs-und Anfrage-
Aequivalenz von MSO, monadischem Datalog, und Automaten.
Thomas Kloecker
Betreuer: Tim Priesnitz
Seminar Logische Aspekte von XML,Gerd Smolka, PS Lab, Uni Saarland, SS 2003
![Page 2: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/2.jpg)
Uebersicht
0. Datalog vs. SQL; monadischer Datalog1. Automaten monadischer Datalog2. Monadischer Datalog MSO3. MSO Automaten
Universum AutomatentypenA. StringsB. Ranked TreesC. Unranked Trees
• 'algebraisch' vs.
bottom-up vs.top-down.
• deterministisch?
![Page 3: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/3.jpg)
Uebersicht
0. Datalog vs. SQL; monadischer Datalog1. Automaten monadischer Datalog2. Monadischer Datalog MSO3. MSO Automaten
Universum AutomatentypenA. StringsB. Ranked TreesC. Unranked Trees
• 'algebraisch' vs.
bottom-up vs.top-down.
• deterministisch?
![Page 4: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/4.jpg)
Uebersicht
0. Datalog vs. SQL; monadischer Datalog1. Automaten monadischer Datalog2. Monadischer Datalog MSO3. MSO Automaten
Universum Automatentypen
Aufgabe
A. StringsB. RankedC. Unranked
'normal' vs.two -way deterministisch
• Sprach-erkennung
• Query-Berechnung
![Page 5: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/5.jpg)
Automaten, monadischer Datalog & MSO
Datalog
![Page 6: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/6.jpg)
Datalog - Beispiel
11
6
5
c
b
a
}3,1,0{
}2,1{
}2,0{
c
b
a
N
N
N
q0 q1
1
1
0
1
0
1
0
0
0
0
1
1
1
0
0
1
1
1
0
1
0
0
0
1
q2
Endlicher Automat für Addition
Presburger Arithmetik
1 0 1 0 0 ...
0 1 1 0 0 ...
1 1 0 1 0 ...
q0 q0 q0 q1 q0 q2
![Page 7: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/7.jpg)
Datalog - Beispiel nocar(0).
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_000(Pos). % 0+0+0 = 0+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_011(Pos). % 0+0+1 = 1+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_101(Pos). % 0+1+0 = 1+0
nocar(NextPos) :- s(Pos, NextPos), carry(Pos), in_001(Pos). % 1+0+0 = 1+0
% c+x+y = z+c'
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_010(Pos). % 1+0+1 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_100(Pos). % 1+1+0 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_111(Pos). % 1+1+1 = 1+1
carry(NextPos) :- s(Pos, NextPos), nocar(Pos), in_110(Pos). % 0+1+1 = 0+1
endOfFile(NextPos) :- s(Pos, NextPos), in_BotBotBot(Pos).
accept :- endOfFile(_).
in_101(0).
in_011(1).
in_110(2).
in_001(3).
in_BotBotBot(4).
s(0,1).
s(1,2).
s(2,3).
s(3,4).
s(4,5).
![Page 8: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/8.jpg)
Datalog Beispiel Presburger Arithmetik
nocar(0).
nocar(NextPos) :- s(Pos,
nocar(NextPos) :- s(Pos,
nocar(NextPos) :- s(Pos,
nocar(NextPos) :- s(Pos,
% c+x+y = z+c'
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_010(Pos). % 1+0+1 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_100(Pos). % 1+1+0 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_111(Pos). % 1+1+1 = 1+1
carry(NextPos) :- s(Pos, NextPos), nocar(Pos), in_110(Pos). % 0+1+1 = 0+1
endOfFile(NextPos) :- s(Pos, NextPos), in_BotBotBot(Pos).
accept :- endOfFile(_).
in_101(0).
in_011(1).
in_110(2).
in_001(3).
in_BotBotBot(4).
s(0,1).
s(1,2).
s(2,3).
s(3,4).
s(4,5).
1 0 1 0 0 ...
0 1 1 0 0 ...
1 1 0 1 0 ...
![Page 9: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/9.jpg)
Datalog Beispiel Presburger Arithmetik nocar(0).
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_000(Pos). % 0+0+0 = 0+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_011(Pos). % 0+0+1 = 1+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_101(Pos). % 0+1+0 = 1+0
nocar(NextPos) :- s(Pos, NextPos), carry(Pos), in_001(Pos). % 1+0+0 = 1+0
% c+x+y = z+c'
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_010(Pos). % 1+0+1 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_100(Pos). % 1+1+0 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_111(Pos). % 1+1+1 = 1+1
carry(NextPos) :- s(Pos, NextPos), nocar(Pos), in_110(Pos). % 0+1+1 = 0+1
endOfFile(NextPos) :- s(Pos, NextPos), in_BotBotBot(Pos).
accept :- endOfFile(_).
in_101(0).
in_011(1).
in_110(2).
in_001(3).
in_BotBotBot(4).
s(0,1).
s(1,2).
s(2,3).
s(3,4).
s(4,5).
![Page 10: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/10.jpg)
nocar(0).nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_000(Pos). % 0+0+0 = 0+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_011(Pos). % 0+0+1 = 1+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_101(Pos). % 0+1+0 = 1+0
nocar(NextPos) :- s(Pos, NextPos), carry(Pos), in_001(Pos). % 1+0+0 = 1+0
% c+x+y = z+c'
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_010(Pos). % 1+0+1 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_100(Pos). % 1+1+0 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_111(Pos). % 1+1+1 = 1+1
carry(NextPos) :- s(Pos, NextPos), nocar(Pos), in_110(Pos). % 0+1+1 = 0+1
endOfFile(NextPos) :- s(Pos, NextPos), in_BotBotBot(Pos).
accept :- endOfFile(_).
in_101(0).
in_011(1).
in_110(2).
in_001(3).
in_BotBotBot(4).
s(0,1).
s(1,2).
s(2,3).
s(3,4).
s(4,5).
Datalog Beispiel Presburger Arithmetik
![Page 11: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/11.jpg)
Datalog Beispiel Presburger Arithmetik
nocar(0).nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_000(Pos). % 0+0+0 = 0+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_011(Pos). % 0+0+1 = 1+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_101(Pos). % 0+1+0 = 1+0
nocar(NextPos) :- s(Pos, NextPos), carry(Pos), in_001(Pos). % 1+0+0 = 1+0
% c+x+y = z+c'
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_010(Pos). % 1+0+1 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_100(Pos). % 1+1+0 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_111(Pos). % 1+1+1 = 1+1
carry(NextPos) :- s(Pos, NextPos), nocar(Pos), in_110(Pos).
endOfFile(NextPos) :- s(Pos, NextPos), in_BotBotBot(Pos).
accept :- endOfFile(_).
in_101(0).
in_011(1).
in_110(2).
in_001(3).
in_BotBotBot(4).
s(0,1).
s(1,2).
s(2,3).
s(3,4).
s(4,5).
nocar carry
1
1
0
1
0
1
0
0
0
0
1
1
1
0
0
1
1
1
0
1
0
0
0
1
endOfFile
![Page 12: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/12.jpg)
Datalog nocar(0).
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_000(Pos). % 0+0+0 = 0+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_011(Pos). % 0+0+1 = 1+0
nocar(NextPos) :- s(Pos, NextPos), nocar(Pos), in_101(Pos). % 0+1+0 = 1+0
nocar(NextPos) :- s(Pos, NextPos), carry(Pos), in_001(Pos). % 1+0+0 = 1+0
% c+x+y = z+c'
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_010(Pos). % 1+0+1 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_100(Pos). % 1+1+0 = 0+1
carry(NextPos) :- s(Pos, NextPos), carry(Pos), in_111(Pos). % 1+1+1 = 1+1
carry(NextPos) :- s(Pos, NextPos), nocar(Pos), in_110(Pos).
endOfFile(NextPos) :- s(Pos, NextPos), in_BotBotBot(Pos).
accept :- endOfFile(_).
in_101(0).
in_011(1).
in_110(2).
in_001(3).
in_BotBotBot(4).
s(0,1).
s(1,2).
s(2,3).
s(3,4).
s(4,5).
nocar carry
1
1
0
1
0
1
0
0
0
0
1
1
1
0
0
1
1
1
0
1
0
0
0
1
endOfFile
![Page 13: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/13.jpg)
Datalog - Grundlegende Konzepte
• Extensionaler und intensionaler Programmteil• kurzer Vergleich mit SQL • formale Definition • Dialekte
• basic vs. stratified • monadisch / voll
• Prolog• Semantik
![Page 14: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/14.jpg)
Datalog vs SQLSQL Datalog
Typen Schema = Menge von Namen von Relationen und Attributen
Signatur = Namen und Aritaeten der extensionalen Praedikate
Modellierung von
gespeichert vs berechnet
Tables vs Views
Extensionale Datenbank (EDB) vs IntensionaleDatenbank (IDB)
Expressivitaet
Transitiver Abschluss nicht modellierbar
Turing complete.
![Page 15: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/15.jpg)
Datalog vs SQLSQL - tablesGetraenke(gid, name, preis)
Kunden(tid, tname, schuhgroesse)
Konsum(gid, tid, menge, datum)------------------------------------------------------------------------------------------------------------
SQL - viewsKunde2(tid, kontonummer)
Konsum2(name, preis, menge, datum, schuhgroesse)
SELECT blahblah-----------------------------------------------------------------------------------------------------------
Datalog- Signatur(getraenk, kunde, konsum)
-----------------------------------------------------------------------------------------------------------
kunde(17, hans, 46).kunde(18, maria, 40).mensch(sokrates).mensch(hans).
Datalog- RegelnAlle Menschen sind sterblich.sterblich(X) :- mensch(X).-------------------------------------------------------------------------------------------------------
Wenn Hans 2 Paar Schuhe hat, verkauft er das teurere Paar.verkauft(hans, X) :- hat(hans,X), hat(hans,Y),schuh(X), schuh(Y), X\==Y, teurerAls(X,Y).
![Page 16: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/16.jpg)
Datalog - Interaktion / Anfragen
1 ?- sterblich(sokrates).
yes.
![Page 17: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/17.jpg)
Datalog - Interaktion / Anfragen
1 ?- sterblich(sokrates).
yes.
2 ?- sterblich(X).
X = sokrates;
![Page 18: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/18.jpg)
Datalog - Interaktion / Anfragen
1 ?- sterblich(sokrates).
yes.
2 ?- sterblich(X).
X = sokrates;X = hans;
![Page 19: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/19.jpg)
Datalog - Interaktion / Anfragen
1 ?- sterblich(sokrates).
yes.
2 ?- sterblich(X).
X = sokrates;X = hans;no.
![Page 20: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/20.jpg)
Datalog - Interaktion / Anfragen1 ?- sterblich(sokrates).yes.
2 ?- sterblich(X).
X = sokrates;X = hans;no.
3 ?- sterblich(_).yes.
![Page 21: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/21.jpg)
Datalog - formale Definition
• Signatur = dasselbe wie ranked Alphabet (Datalog - Sprechweise)
• Sei eine Signatur gegeben. Ein einfaches Datalog Programm (ueber )
mit intensionalen Praedikaten PI ist eine Menge von Regeln der Form
H :- B1, …, Bn.
(wobei die linke Seite H Head, und die rechte Seite B1, …, Bn Body,genannt werden), wenn gilt:
1) Alle Heads sind in Atome Ru1,.., un mit R in PI .
2) Alle Bj , 1 <= j <= n, sind entweder Atome Ru1,.., un mit R in PI ,
oder Literale (¬)Ru1,.., un mit R in ,
3) PI =
![Page 22: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/22.jpg)
Datalog - formale Definition• Die Elemente von heissen auch extensionale Praedikate oder Input Praedikate. Das einfache Datalog Program selbst heisst auch intensionale Datenbank, oder IDB.• Eine Regel wie die obige, jedoch mit leerem Body, und als Head ein
Atom Ru1,.., un mit R aus , heisst auch ein Fakt. Mengen von Fakten
heissen auch extensionale Datenbank, oder EDB.• Die Semantik des Programms (d.h. der IDB) ist eine Abbildung
EDB Zuweisung von Wahrheitswerten an die intensionalen Praedikate.• Ein stratifiziertes Datalog Programm ist eine geordnete Folge von einfachen Datalog Programmen, Strata genannt. Jedes Stratum wird als EDB (d.h. Input) des naechsthoeheren Stratums interpretiert.
![Page 23: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/23.jpg)
Datalog - formale Definition• Ein Datalog Programm heisst monadisch, wenn alle intensionalen Praedikate Aritaet 1 haben. • Die Signatur fuer monadischen Datalog auf ranked trees gemaess Gottlob/Koch ist: ( root, leaf, (childk)k <= maxAritaet, (labela) a , )
• Die Signatur fuer monadischen Datalog auf unranked trees gemaess Gottlob/Koch ist: ( root, leaf, (labela) a ) firstChild, lastChild, nextSibling)
![Page 24: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/24.jpg)
Datalog - Semantik
EDB mensch(sokrates).
IDB sterblich(X) :- mensch(X).
InteractiveToplevel
1 ?- sterblich(sokrates).yes.
2 ?- sterblich(thomas).no.
![Page 25: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/25.jpg)
Datalog - Semantik
shaves(barber, X) :- ¬shaves(X, X).
1 ? - shaves(cartman, cartman).no.2 ? - shaves(barber, cartman).yes.3 ? - shaves(barber, barber).ERROR: out of local stack
![Page 26: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/26.jpg)
Datalog - Semantik
• Erste Wahl: Kleinster Fixpunkt (Perfect Model)• Existiert fuer einfaches Datalog• Im stratified Fall Semantik hierarchisch / schrittweise; kleinster Fixpunkt existiert nicht.
![Page 27: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/27.jpg)
Datalog - stratified%% search.pl -- Section 2.16 of Prolog Tutorial
solve(P) :- start(Start), search(Start,[Start],Q), reverse(Q,P).
search(S,P,P) :- goal(S). /* done */search(S,Visited,P) :- next_state(S,Nxt), /* generate next state */ safe_state(Nxt), /* check safety */ no_loop(Nxt,Visited), /* check for loop */ search(Nxt,[Nxt|Visited],P). /* continue searching... */
no_loop(Nxt,Visited) :- \+member(Nxt,Visited).
start([]).goal(S) :- length(S,8).
next_state(S,[C|S]) :- member(C,[1,2,3,4,5,6,7,8]), \+member(C,S).
safe_state([C|S]) :- length(S,L), Sum is C+L+1, Diff is C-L-1, safe_state(S,Sum,Diff).
safe_state([],_,_) :- !.safe_state([F|R],Sm,Df) :- length(R,L), X is F+L+1, X \= Sm, Y is F-L-1, Y \= Df, safe_state(R,Sm,Df).
![Page 28: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/28.jpg)
Automaten monadischer Datalog
• ranked trees: Beispiel: d(neg(0), or(0, 1))
Signatur: ( root, leaf, (childk)k <= maxAritaet, (labela) a , )
lblAND(root).lblNOT(root-1).lblFALSE(root-1-1).lblOR(root-2).lblTRUE(root-2-2).lblFALSE(root-2-1).
root(root).child_1(root, root-1).child_2(root, root-2).child_1(root-1, root-1-1).child_1(root-2, root-2-1).child_2(root-2, root-2-2).
![Page 29: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/29.jpg)
Automaten monadischer Datalogaccept :- truth(root).
false(Pos) :- lblFALSE(Pos).truth(Pos) :- lblTRUE(Pos).
false(Pos) :- lblAND(Pos), child_1(Pos, ChildPos), false(ChildPos).false(Pos) :- lblAND(Pos), child_2(Pos, ChildPos), false(ChildPos).truth(Pos) :- lblAND(Pos), child_1(Pos, ChildPos_1), child_2(Pos,
ChildPos_2), truth(ChildPos_1), truth(ChildPos_2).
truth(Pos) :- lblOR(Pos), child_1(Pos, ChildPos), truth(ChildPos).truth(Pos) :- lblOR(Pos), child_2(Pos, ChildPos), truth(ChildPos).false(Pos) :- lblOR(Pos), child_1(Pos, ChildPos_1), child_2(Pos,
ChildPos_2), false(Pos-1), false(Pos-2).
truth(Pos) :- lblNOT(Pos), child_1(Pos, ChildPos), false(ChildPos).false(Pos) :- lblNOT(Pos), child_1(Pos, ChildPos), truth(ChildPos).
![Page 30: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/30.jpg)
Automaten monadischer DatalogDefinition:
Gegeben ein monadisches Datalog-Programm P ueber ranked trees mit ausgezeichnetem Praedikat accept,
und mit LEERER EDB. Fuer einen Sigma-gelabelten Baum T definiereedb(T) := Uebersetzung von T in TauRanked(Sigma) Schreibweise,P(T) := das Datalog Programm mit IDB P und EDB edb(T), undM(P(T)) := das eindeutig bestimmte minimale Modell von P(T)dann ist die von P erkannte Sprache L(P) (N* -> Sigma)r-Baum definiert
durch
T in L(P) <==> M(P(T)) |= accept.( In der Praxis: T in L(P) <==> Prolog (oder sonstige Implementierung) antwortet "yes" auf die
Frage "accept." )
Gegeben ein deterministischer Baumautomat A ueber Sigma, mit Zustandsmenge Q,
und Uebergangsfunktionen Delta(Sigma) in Q^n -> Q fuer sigma in Sigma und ar(sigma) = n.
Satz (Gottlob) es ex ein monadisches Datalog-Programm P, derart dass L(P) = L(A)
![Page 31: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/31.jpg)
Automaten monadischer Datalog
Beweis / Konstruktion:
* Fuer jedes q in Q intensionales Praedikat, ebenfalls q genannt.
* Fuer sigma in Sigma, ar(sigma) = n, q-bar = (q1,...,qn) in Q^n, sei die Regel R(sigma, Q-bar) wie folgt definiert ( wobei
delta(sigma)(q-bar) = q )
q(Pos) :- label_sigma(Pos), child(Pos, ChildPos1), q1(ChildPos1),.......
* Fuer Endzustaende q definiere die Regel R_fin(q) durch
accept :- q(root).
Fuer jede Regel deltaaccept :- truth(root).
![Page 32: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/32.jpg)
Automaten monadischer DatalogGegeben ein deterministischer Baumautomat A ueber Sigma, mit Zustandsmenge Q,
und Uebergangsfunktionen Delta(Sigma) in Q^n -> Q fuer sigma in Sigma und ar(sigma) = n.
Satz (Gottlob) es ex ein monadisches Datalog-Programm P, derart dass L(P) = L(A)
Beweis / Konstruktion:
* Fuer jedes q in Q intensionales Praedikat, ebenfalls q genannt.
* Fuer sigma in Sigma, ar(sigma) = n, q-bar = (q1,...,qn) in Q^n, sei die Regel R(sigma, Q-bar) wie folgt definiert ( wobei delta(sigma)(q-bar) = q )
q(Pos) :- label_sigma(Pos), q1(Pos-1),...,qn(Pos-n). ( verkuertzt Schreibweise )
q(Pos) :- label_sigma(Pos), child(Pos, ChildPos1), q1(ChildPos1),....... ( geschwaetzige Schreibweise )
* Fuer Endzustaende q definiere die Regel R_fin(q) durch
accept :- q(root).Fuer jede Regel deltaaccept :- truth(root).
false(Pos) :- lblFALSE(Pos).truth(Pos) :- lblTRUE(Pos).
false(Pos) :- lblAND(Pos), child_1(Pos, ChildPos), false(ChildPos).false(Pos) :- lblAND(Pos), child_2(Pos, ChildPos), false(ChildPos).truth(Pos) :- lblAND(Pos), child_1(Pos, ChildPos_1), child_2(Pos, ChildPos_2), truth(ChildPos_1), truth(ChildPos_2).
truth(Pos) :- lblOR(Pos), child_1(Pos, ChildPos), truth(ChildPos).truth(Pos) :- lblOR(Pos), child_2(Pos, ChildPos), truth(ChildPos).false(Pos) :- lblOR(Pos), child_1(Pos, ChildPos_1), child_2(Pos, ChildPos_2), false(Pos-1), false(Pos-2).
truth(Pos) :- lblNOT(Pos), child_1(Pos, ChildPos), false(ChildPos).false(Pos) :- lblNOT(Pos), child_1(Pos, ChildPos), truth(ChildPos).
![Page 33: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/33.jpg)
Contribution
• theorem: satisfiability of structural subtyping
constraints for recursive types is DEXPTIME complete.
• new relationship to modal logics
• extension of Wand & Tiuryn´s appoach
![Page 34: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/34.jpg)
Sprache Baeume Anfrage Baeume ( ( Knoten ) )
Korrespondenz Automaten <--> MSO hochheben auf
• Anfragen• unranked caseconclusion
Spracherkennung vs. Anfragen
![Page 35: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/35.jpg)
![Page 36: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/36.jpg)
Position
1 2 3 4 5 6 7 8
U A A B A A C A A
V A A C A A B A A
![Page 37: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/37.jpg)
Position
1 2 3 4 5 6 7 8
U A A B A A C A A
V A A C A A B A A
![Page 38: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/38.jpg)
Position
1 2 3 4 5 6 7 8
U A A B A A C A A
V A A C A A B A A
![Page 39: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/39.jpg)
![Page 40: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/40.jpg)
![Page 41: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/41.jpg)
forth(4)
back(7)
![Page 42: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/42.jpg)
Related Work
• subtype constraints for programming languages
[Mitchell 91]
• logical problems: satisfiability, [Fuh, Mishra 90, Amadio, Cardelli 93, Eifrig, Smith, Trifonow 95 ...]
entailment, and
[Pottier 98, Rehof, Henglein 97, Niehren, Priesnitz]
first-order validity [Aiken, Zu, Niehren, Priesnitz, Treinen,
Kuncak]
• satisfiability checking for type reconstruction
![Page 43: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/43.jpg)
forth(4)
back(7)
![Page 44: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/44.jpg)
Contribution
• theorem: satisfiability of structural subtyping
constraints for recursive types is DEXPTIME complete.
• new relationship to modal logics
• extension of Wand & Tiuryn´s appoach
![Page 45: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/45.jpg)
Types
• basic types int, real
• function types
• pair types
• polymorphic types x. xx [Milner]
pair int
int int
![Page 46: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/46.jpg)
Types are Trees
signature of function symbols a,b,f
f
a f
a f
a
f
a f
a b
a
.
.
.
constants only finite trees (ground terms) infinite trees
f ( a , f(a,b) )
![Page 47: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/47.jpg)
Subtyping
• subtypes (substitution) int ≤ real [Mitchell 91]
• ordering is lifted to ground terms
Example: a ≤ b f(a,a) ≤ f(a,b)
t1 ≤ s1 t2 ≤ s2
f(t1, t2) ≤ f(s1, s2)
![Page 48: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/48.jpg)
Structural versus Non-Structural
f
b f
a b
f
a f
a b
≤
f
f
f
f
≤
≤ τ ≤ τ
for every tree τ
![Page 49: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/49.jpg)
Constraint Languages
• terms t over basic types, smallest/greatest
types ?, function (pair) types, and type variables
• subtype constraints are conjunctions of inequations t1 ≤ t2
![Page 50: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/50.jpg)
Open Questions
• Is entailment of non-structural subtyping decidable?
- structural case solved [Rehof, Henglein 97,98]
- many approaches [Niehren, Priesnitz, Aiken, Zu, Treinen]
• satisfiability of subtyping with constant ordering
- complexity for structural subtyping with recursive types [Wand, Tiuryn: between PSPACE and DEXPTIME] - decidability for non-structural subtyping
![Page 51: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/51.jpg)
Structural Subtyping with Constants
• constant ordering is lattice: O(n ) [Kozen, Palsberg, Schwartzbach 94, Palsberg, Wand, O’Keefe 97] • arbitrary ordering
3
constants only NP-hard in NP
finite trees PSPACE-hard in PSPACE
infinite trees DEXPTIME-hard in DEXPTIME
new! Tiuryn, Wand 93
Tiuryn, Wand 93 Frey 2002
Pratt, Tiuryn 93,96 easy
lower bound upper bound
![Page 52: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/52.jpg)
Example: NP-hardness
signature with 4 constantsc < a, c < b, d < a, d < b
a b
c d
consider constraint c ≤ x ≤ a d ≤ y ≤ b y’ ≤ x ≤ x’ y’ ≤ y ≤ x’
a x’ b
x y
c y’ d
which has exactly 2 solutions:
a=x=x’ b
c y’=y=d
a x=x’=b
c=y’=y d
![Page 53: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/53.jpg)
Negation Gate
has exactly 2 solutions:a=z3=z2, b=z4=z1, c=x=z5,
d=y=z6
a=x=z1, b=y=z2, c=z4=z6,
d=z3=z5
a z1 z2 b
x z3 z4 y
c z5 z6 d
true z1 z2 b
x z3 z4 y
false z5 z6 d
b z7 true
y z
d z8 false
plug it together
negation gate: x = z
![Page 54: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/54.jpg)
Negation Gate for Vectorsf
f truef false
.
f true.
.
f
f falsef false
.
f true.
.
f
f falsef false
.
f true.
.
true
false
true.
.
.
false
false
.
.
.
true
false
false
.
.
.
true
*constants are unary
*
![Page 55: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/55.jpg)
Negation Gate: Implementation
• new variables: a∞ a∞ = a ( a∞ )
• x is boolsche: false∞ ≤ x ≤ true∞
• same idea to implement only negate at position π negate all positions at π1*
a
. . .
a a
π
π*
![Page 56: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/56.jpg)
Example: 1-Bit-Counter
given signature with 4 unary symbols true a
false b
true∞ ≤ x ≤ false∞ true∞ ≤ y ≤ false∞ x= y x=true(y)
define counter by
x
true
false
true
false
false
true
false
true
y
![Page 57: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/57.jpg)
Regular Tree Constraints: Models
1
1
1
2
2
2
Complete Infinite Tree.
x y
x y
x y
x y
x y
x y
x y x y x y
alternative: v {true,false} for π in (1∪2)*
π
![Page 58: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/58.jpg)
Regular Tree Constraintsgiven signature with constant ordering, alphabet A of letters i, regular expressions r over A, regular tree constraints are conjunctions of 4 types• ( x ≤ y )
• ( x ≤ y )
• ( x ≤ c )
• ( c ≤ x )
π πi π in r
πi π π in r
π π in r
π π in r
![Page 59: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/59.jpg)
Tiuryn & Wand’s ApproachSatisfiability of structural subtype constraintsover infinite trees is O(n)-reducible toregular tree constraints.
Tiuryn, Wand 93
![Page 60: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/60.jpg)
Propositional Dynamic Logic (PDL)
• Pratt’s dynamic logic
• logic for program verification
• propositional fragment by Fischer, Ladner
![Page 61: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/61.jpg)
PDL Models
models are rooted directed labeled graphs
1
1,2
2
2
2
x y
x y
x y
x y
x y
x y
x y
2
![Page 62: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/62.jpg)
PDL Language
• alphabet A = { 1,2,...n }
• regular expressions r over A
• PDL Syntax: φ ::= P φ φ φ’ [r] φ
• modal operator [r] φ
for all r-sucessors holds φ
2
1P Q
P Q
[1∪2] (PQ)
![Page 63: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/63.jpg)
Example: 1-Bit-Counter
[1*] (P ∨ [1] P) P has one solutionin the class of unary infinite deterministic trees
+
1
1
1
1
P
P
P
P
![Page 64: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/64.jpg)
Tree PDL
theorem: satisfiability of Tree PDL is DEXPTIME-complete
proof: reduction to deterministic PDL: models are restricted to be functional
1
1
1
2
2
2
2
2
forbidden
1,2
Satisfiability of Deterministic PDL is DEXPTIME-complete.
Ben-Ari, Halpern, Pnueli 82 & Parikh 78
![Page 65: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/65.jpg)
Regular Tree Constraints Tree PDL
theorem: regular tree constraints are a fragment of tree DPL example signature
x ≤ y Px Py
• ( x ≤ y ) [r] (Px [i]Py)
• ( x ≤ false ) [r] (Px false)
π πi π in r
π π in r
true
false
ε ε
![Page 66: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/66.jpg)
Core Tree PDL
Core Tree PDL is defined by a restricted syntax:
φ ::= [r1]ψ1 … [rn]ψn where r is ε or (1∪2)*
ψ ::= P ψ ψ ψ [r] ψ where r is 1 or 2
![Page 67: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/67.jpg)
Satisfiability of Core Tree PDL
theorem: satisfiability of Core Tree PDL is DEXPTIME-complete
possibilities for the hardness-proof: encode• Halting-Problem of alternating linear-space bounded Turing machine.• Exists a winning strategy in a two person tiling game? Maarten de Rijke:
PDL
• Emptiness of the intersection of some tree automta. Helmut Seidl: haskell
overloading
![Page 68: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/68.jpg)
Sat. of Core Tree PDL is DEXPTIME-hardregard n tree automata (Q, Σ, δ, q ) with Σ = { f, a, b }
Pf
Pa
Pb
P# P# P# P#
a
b
f
init
except one nonempty infinite tree[(1∪2)*] ( Pf ∨ Pa ∨ Pb ∨ P#)[(1∪2)*] (Pa ∨ Pb ∨ P#) [1∪2] P# [ε] P#
+ + +
except one nonempty finite treemark with counterall exponential deep nodes
[(1∪2)*] Pdeep P#
Pf
Pa
Pb
Pdeep PdeepPdeep Pdeep
![Page 69: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/69.jpg)
Sat. of Core Tree PDL is DEXPTIME-hard
Pqinit
Pq2
Pq2
Pq1 Pq1 Pq1 Pq1
init
every tree automata accepts a tree
[ε] Pq
[(1∪2)*] (Pf ∧ [1] Pq ∧ [2] Pq’ ) Pq’’ if f(q,q’) q’’ in δ[(1∪2)*] Pa Pq if a q in δ
init
![Page 70: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/70.jpg)
Core Tree PDL Subtype Constraints
main theorem: sat. of core tree PDL is O(n)-reducible to sat. of structural subtype constraints over infinite trees.
reduce example: [(1∪2)*] (P [i]P’)
[*] P2= (P P1= ( [i] P’ ) ) [*] P2 = (P P1 = ( [i] P’ )
)
false∞ ≤ { P2, P, P1, P’ } ≤ true∞
P1=true( P‘) P2 = P P1
P2=true ∞
* * * * *i
*
![Page 71: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/71.jpg)
Conclusion
• modal logic approach to subtyping constraints
• non-structural case still open
• can we extend our approach?
• what about entailment?
![Page 72: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/72.jpg)
thank you
![Page 73: Spracherkennungs-und Anfrage-Aequivalenz von MSO, monadischem Datalog, und Automaten. Thomas Kloecker Betreuer: Tim Priesnitz Seminar Logische Aspekte](https://reader036.vdokument.com/reader036/viewer/2022062512/55204d6449795902118ba7bc/html5/thumbnails/73.jpg)
Result Pratt, Tiuryn 96
Satisfiability of Structural Subtype Constraints is NP-complete in the Model of single Leafs. (Signature contains only Constants)