Egzamin 2011/2012 | Informatyka MIMUW

Zadanie 1 (15 punktów)

Napisać formułę $\varphi(x,y)$ w języku arytmetyki taką, że $(\mathfrak{N},x:r,y:k)\models \varphi$ wtw w ćwierćkole $\{(x,y)\in \mathbb{R}^2~:~x,y\geq 0,~x^2+y^2\leq r\}$ na płaszczyźnie euklidesowej jest dokładnie $k$ punktów kratowych (tzn. punktów o obu współrzędnych całkowitych).

Rozwiązanie

Wykorzystamy formułę $\chi$ , definiującą funkcję $\beta$ Goedla, aby powiedzieć, że istnieje ciąg $y$ parami różnych par liczb naturalnych $(u,v)$ spełniających $u^2+v^2\leq x$ i że każda para liczb spełniająca ten warunek w tym ciągu występuje.

$\exists t\exists p [\forall i(i\le y-1\to(\exists u\exists v\chi(t,p,2*i,u)\land\chi(t,p,2*1+1,v)\land u*u+v*v\leq x)\land$
$(\forall u\forall u(u*u+v*v\leq x\to\exists! i(i\le y-1\land \chi(t,p,2*i,u)\land\chi(t,p,2*1+1,v))]$ .

Zadanie 2 (15 punktów)

W pewnej bazie danych znajduje się dwukolumnowa tabela $R$ , zawierająca w sobie relację liniowego porządku na wszystkich elementach dziedziny aktywnej tej bazy danych. Dane jest także wyrażenie $E$ algebry relacji

$R\setminus (\pi_{1,4}(\sigma_{2=3}(R\times R)\setminus(\sigma_{1=2}(R\times R)\cup\sigma_{3=4}(R\times R)))).$

Zaprojektować algorytm obliczający $[\![E]\!]$ , którego złożoność czasowa wynosi $O(n)$ , gdzie $n=|R|.$ Można korzystać z tablicy haszującej dla elementów dziedziny aktywnej, o dostępie w czasie jednostkowym i zapewniającej brak kolizji.

Rozwiązanie

Wyrażenie

$E$ opisuje sumę relacji bezpośredniego następnika na dziedzinie aktywnej i relacji identycznościowej na dziedzinie aktywnej, zgodnie z porządkiem zadanym przez

$R$ . Obliczenie relacji identycznościowej jest banalne, problemem jest tylko następnik.

Jeśli $|R|=n$ , to rozmiar dziedziny aktywnej wynosi $m=O(\sqrt{n})$ .

W celu obliczenia następnika można użyć tablicy haszującej $T$ , używając ją do zliczania ile razy każdy z elementów dziedziny aktywnej występuje po lewej stronie par w relacji $R$ . Wymaga to liniowego przejścia $R$ w czasie $O(n)$ . Po zakończeniu tego procesu można $T$ posortować po wartościach zliczeń w czasie $O(m\log m)=O(n)$ i wypisać pary kolejnych elementów, albo wykorzystać $T$ do rozstrzygania w czasie stałym o porządku par poszczególnych elementów (przez porównanie ich zliczeń w $T$ ), co pozwala po prostu posortować dziedzinę aktywną.

Zadanie 3 (15 punktów)

Rozważamy logikę LTL nad skończonymi strukturami-słowami.
Jak wiadomo z tw. Gabbaya, każde zdanie $\varphi$ logiki LTL można wyrazić równoważnie w postaci zdania będącego boolowską kombinacją zdań czasu przyszłego i zdań czasu przeszłego.

Podać przykład zdania $\varphi$ logiki LTL którego nie można wyrazić równoważnie w postaci koniunkcji jednego zdania czasu przyszłego i jednego zdania czasu przeszłego.

Rozwiązanie

Roważmy zdanie

$\varphi=Yp\lor Xp$ .

Przypuśćmy, że $\varphi$ jest równoważne formule $\alpha\land\beta$ , gdzie $\alpha$ jest czasu przeszłego a $\beta$ jest czasu przyszłego. Rozważmy teraz dwa modele o trzech stanach, zapisane jako ciągi prawdziwości $p$ w kolejnych stanach. Te modele to $100$ i $001$ . W obu stan środkowy oznaczmy $*$ .

Mamy zatem $(100,*)\models\varphi$ i $(001,*)\models\varphi$ .

Ponieważ $varphi$ jest równoważne $\alpha\land\beta$ , to $(100,*)\models\beta$ i $(001,*)\models\alpha$ .

Zatem $(000,*)\models\beta$ bo $\beta$ jest czasu przyszłego a $000$ różni się od $100$ tylko w przeszłości względem $*$
oraz $(000,*)\models\alpha$ bo $\alpha$ jest czasu przeszłego a $000$ różni się od $001$ tylko w przyszłości względem $*$ .

Stąd $(000,*)\models\alpha\land\beta$ wbrew założeniu, że ta formuła jest równoważna $Yp\lor Xp$ .

Zadanie 4 (15 punktów: 5 za podpunkt 1 i 10 za podpunkt 2)

Zajmujemy się skończonymi grafami nieskierowanymi. W obu podpunktach należy napisać zdanie $\varphi$ logiki drugiego rzędu takie, że dla każdego grafu $\mathfrak{G}$ zachodzi

$\mathfrak{G}\models\varphi$ wtw $\mathfrak{G}$ jest spójny}.

$\varphi$ ma mieć postać $\forall R\varphi',$ gdzie $\varphi'$ jest formułą pierwszego rzędu.
$\varphi$ ma mieć postać $\exists R\varphi',$ gdzie $\varphi'$ jest formułą pierwszego rzędu.

Rozwiązanie

Niech $E$ to relacja krawędzi.

Wyrażamy Dla każdego podziału $\mathfrak{G}$ na dwa niepuste podzbiory, istnieje krawędź łacząca wierzchołek w jednej z tych części z wierzchołkiem w drugiej części.
$\forall R((\exists x\exists y R(x)\land\lnot R(y)) \to(\exists x\exists y R(x)\land\lnot R(y)\land E(x,y)))$
Najpierw napiszemy zdanie postaci $\forall x\forall y \exists R\varphi$ wyrażające spójność. Będzie ono formalizowało
$\forall x\forall y$ istnieje ścieżka od $x$ do $y$ .
Ma ono postać

$\forall x\forall y \exists R(x=y\lor$ " $R$ jest liniowym porządkiem, $x$ jest pierwszy w tym porządku, między każdymi dwoma kolejnymi wierchołkami $z,t$ położonymi pomiędzy $x$ i $y$ jest krawędź").

$\forall x\forall y \exists R\varphi(x=y\lor$
$((\forall u R(u,u))\land(\forall u\forall v R(u,v)\lor R(v,u))\land(\forall u\forall v (R(u,v)\land R(v,u))\to u=v)\land(\forall u \forall v\forall w (R(u,v)\land R(v,w))\to R(u,w)))\land$
$(\forall z R(x,z))\land$
$\forall z\forall t [[R(z,y)\land R(t,y)\land(\forall u ((R(z,u)\land R(u,t)))\to(u=z\lor u=t))]\to E(z,t)]$

Teraz mając zdanie $\forall x\forall y \exists R\varphi$ przerabiamy je na żądaną postać przez zamianę $R$ z dwuargumentowego na czteroargumentowy:

$\exists R\forall x\forall y \varphi[R(x,y,*,*)/R(*,*)]$ , co ma ten efekt, że nowa relacja $R$ dla każdego wyboru $x,y$ ma w sobie zapisany odpowiedni porządek, opisujący ścieżkę od $x$ do $y$ .

TEST

1. Niech dla zdania $\varphi$ logiki pierwszego rzędu

${spec}(\varphi)=\{n\in\mathbb{N}_+$ istnieje $\mathfrak{A}$ o mocy $n$ takie, że $\mathfrak{A}\models\varphi\}.$

Czy następujący problem jest rozstrzygalny:
Dane: Dwa zdania $\varphi,\psi$ logiki pierwszego rzędu.
Pytanie: Czy $spec(\varphi)=spec(\psi)$ ?

Odpowiedź

NIE, bo gdyby był, to można by sprawdzać czy dane zdanie

$\varphi$ ma skończony model pytając czy

$spec(\varphi)=spec(\bot)$ . Tymczasem jest to niemożliwe na mocy tw. Trachtenbrota.

2. Czy następująca formuła logiki drugiego rzędu SO jest jest tautologią?

$[\forall R \exists Q_1 \exists Q_2 \forall x \forall y (R(x,y) \leftrightarrow (Q_1(x) \land Q_2(y)))]$

$\to$

$[\exists Q_1 \exists Q_2 \forall R \forall x \forall y ((R(x,y) \leftrightarrow Q_1(x,y)) \lor (R(x,y) \leftrightarrow Q_2(x,y)))]$

Odpowiedź

TAK.

Zdanie w pierwszej linijce orzeka, że każda relacja dwuargumentowa (czyli zbiór par elementów) jest produktem kartezjańskim dwóch zbiorów elementów. Jest to możliwe wtedy i tylko wtedy gdy uniwersum modelu ma dokładnie jeden element.

W takim model z kolei istnieją dwie relacje dwuragumentowe (a konkretnie pusta i pełna) takie, że każda relacja relacja dwuargumentowa jest jedną z nich (bo innych na uniwersum jednoelementowym nie ma).

3. Czy gracz II ma strategię wygrywającą w grze Ehrenfeuchta-Fra\"{\i}ss\'ego o 4 rundach $G_4(\mathfrak{A},\mathfrak{B}),$ gdzie $\mathfrak{A}$ i $\mathfrak{B}$ są poniższymi grafami nieskierowanymi ( $\mathfrak{A}$ po lewej, $\mathfrak{B}$ po prawej):

   *      *      *      *                        *      *      *    
   |      |      |      |                        |      |      |    
 *-*-*  *-*-*  *-*-*  *-*-*                    *-*-*  *-*-*  *-*-*  
   |      |      |      |                        |      |      |    
   *      *      *      *                        *      *      *

Odpowiedź

NIE. Oto strategia dla gracza I: w trzech ruchach kolejno zaznacza centra krzyży po prawej stronie, po czym w czwartym zaznacza dowolny element tego krzyża po lewej, w którym gracz II nie zaznaczył dotąd żadnego elementu.

4. Ustalamy alfabet $A_k$ i rozpatrujemy modele-słowa postaci $\mathfrak{A}(w)$ dla słów $w\in A_k^+.$ Niech dla zdania $\varphi$ logiki monadycznej drugiego rzędu MSO
$\bar{spec}(\varphi)=\{n\in\mathbb{N}_+ :$ istnieje $w\in A_k^n$ takie, że $\mathfrak{A}(w)\models\varphi\}.$

Czy dla każdego zdania $\varphi$ w MSO istnieje zdanie $\psi$ w MSO takie, że $\mathbb{N}_+\setminus\bar{spec}(\varphi)=\bar{spec}(\psi)$ ?

Odpowiedź

TAK. Wystarczy wziąć zdanie

$\lnot \exists X_1\ldots\exists X_k\varphi$ , gdzie

$X_1\ldots X_k$ to wszystkie relacje unarne w sygnaturze

$\varphi$ .

5. Czy w logice LTL da się wyrazić formułą następującą własność modelu-słowa $\mathfrak{A}(w)$ :
jest dokładnie tyle samo stanów w których zmienna zdaniowa $p$ jest prawdziwa i stanów w których zmienna zdaniowa $p$ jest fałszywa.

Odpowiedź

NIE. Opisana własnośc nie jest regularna, więc nie da się jej wyrazić nawet w logice MSO (tw. Buchi-Elgota), a tym bardziej w FO, która jest równoważna LTL (tw. Kampa).