TD 9 : Lemme de Dickson, PDA et logique MSO
EX 1 : Lemme de Dickson et PDA
1.
Montrons l’équivalence entre
-
Pour tout $V$, $\min V$ est un ensemble fini
-
Pour tout $V$, il existe une suite strictement croissante $i_0 < i_1 < ⋯ $ telle que $v_{i_j}≤v_{i_{j+1}}$ pour tout $j≥0$
(1) ⟹ (2)
Supposons que $\min V ≝ \lbrace u_1, ⋯, u_n\rbrace$
On pose
\[U_i ≝ \lbrace j > i \mid v_j ≥ u_i \rbrace\]Par le principe des tiroirs, l’un des $U_i$ est infini, disons $U_{i_0}$.
On recommence avec $U_{i_0}$, en exploitant le fait que
\[\min U_{i_0} \text{ est fini}\]et ainsi de suite.
(2) ⟹ (1)
Montrons la contraposée : s’il existe un
\[V ≝ \lbrace v_{i_j} \rbrace_{j∈ℕ}\]tel que $\min V$ est infini, alors toute suite dont deux éléments de $\min V$ appartiennent à l’image ne peut pas être croissante : il existe donc une telle suite.
2.
Pour $k=1$ :
$\vert \min V \vert = 1$, donc on utilise $(1)⟹(2)$
Pour $k>1$ :
On utilise l’hypothèse de récurrence sur les $k$ premières coordonnées, ce qui nous fournit une suite extraite croissante, puis on en extrait une suite croissante avec le raisonnement de l’intialisation sur la $k+1$-ème coordonnée.
3.
Mq
\[p, z ⟶^𝜔\]ssi $∃q, a∈ Q × 𝛤;$
- $p,z ⟶^\ast q, ua$ pour un $u$ quelconque.
- $q, a ⟶^+ q, va$ pour un $v$ quelconque.
$⟸$
clair
$⟹$
Soit $(p_i, z_i)$ avec $p_i, z_i ⟶𝒜 p{i+1}, z_{i+1}$ et $p, z= p_0, z_0$ une exécution infinie de $𝒜$.
On regarde $(\vert z_i \vert)_{i≥0}$.
On extrait
\[i_0 < i_1 < ⋯\]tq $i_0$ est un indice en lequel le min est atteint et $\vert z_{i_j} \vert ≤ \vert z_{i_{j+1}} \vert$ pour tout $j≥0$, et pour tout $i_j < k < i_{j+1}$,
\[\vert z_k \vert ≥ \vert z_{i_j} \vert\]Soit $z_i = z’_i a_i$ pour $a_i∈𝛤$.
Du coup, on a pour tout $j≥0$ :
\[p_{i_j} z'_{i_j} a_{i_j} ⟶^+ p_{i_{j+1}} z'_{i_{j+1}} a_{i_{j+1}}\]sans toucher à $z’_{i_j}$, donc
\[p_{i_j} a_{i_j} ⟶^+ p_{i_{j+1}} z''_{i_{j+1}} a_{i_{j+1}}\]avec \(z'_{i_{j+1}} = z'_{i_{j}} z''_{i_{j+1}}\)
Par le principe des tiroirs, comme $Q×𝛤$ est fini, il y a une paire $q, a$ tq $q, a$ apparaît deux fois (même infiniment souvent) dans $(p_{i_j}, a_{i_j})_{j≥0}$.
Soient $i_{j_1} < i_{j_2}$ les deux premières occurrences alors on choisit
- $u = z’{i{j_1}}$
- $v = z’‘{i{j_1+1}} ⋯ z’‘{i{j_2}}$
4.
On a vu dans le TD précédent que si un langage de configurations est régulier, il en est de même du langage des prédécesseurs et des successeurs.
Pour toute paire $(q, a)∈Q×𝛤$ on teste s’il existe $v∈𝛤^\ast$ tq
\[q, a ⟶^+ q, va\]⟶ calculer $C(q, a)$ intersecté avec $q, 𝛤^\ast a$
Soit $R$ l’ensemble des $q, a$ qui vérifient cette propriété.
On calcule
\[\overline{C}\Big(\bigcup\limits_{q,a∈R} q, 𝛤^\ast a\Big)\]EX 2. Logique MSO
1.
\[first(x) = ¬ (∃y. \, y < x)\]1.
\[first(x) = ¬ (∃y. \, y < x)\]2.
\[last(x) = ¬ (∃y. \, x < y)\]3.
\[entre(x, z, y) = x<z ∧ z<y\]4.
\[next(x, y) = x<y ∧ ¬(∃z. entre(x, z, y))\]5.
\[x≠y = x<y ∧ y<z\]6.
\[x≠y = x<y ∧ y<z\]5.
\[sing(X) = ∃x. \Big(x∈X ∧ (∀y. y∈X ⟶ x=y) \Big)\]6.
\[X∪Y=pos(w) = ¬∃z. (z∉X ∧ z∉Y)\]7.
\[paires(X) = ∃Y. \; X∪Y = pos(w) ∧ ¬∃z.(z∈X ∧ z∈Y)\\ ∧ ∃y∈Y. \; first(y) \\ ∧ ∀x∈X. \; ∀y. \; next(x,y)⟶y∈Y \\ ∧ ∀x∈X. \; ∀y. \; next(y,x)⟶x∈X\]8.
\[pair(X) = ∀x. x∉X ∨ ∃Y, Z. \Bigg(\; ∀x. (x∈X ⟺ x∈Y \oplus x∈Z) \\ ∧ ∃y∈Y. ∀z∈X. y <z \\ ∧ ∀y∈Y. ∃z∈Z. ∀y'∈Y. y < y' ⟶ entre(y, z, y') \\ ∧ ∃z∈Z. ∀y∈Y. y<z \\ ∧ ∀z∈Z. ∃y∈Y. ∀z'∈Z. z' < z ⟶ entre(z', y, z) \Bigg)\]EX 3.
1.
\[L_1 ≝ (ab)^\ast\] \[∃X; \, paires(X) \\ ∧ ∀x∈X. \, P_a(x) \\ ∧ ∀y∉X. \, P_b(y)\]2.
\[L_2 ≝ \lbrace w \mid \vert w \vert_a \text{ est pair} \rbrace\] \[∃X; P_a(x) ⟺ x∈X \\ ∧ pair(X)\]3.
\[L_3 ≝ 𝛴^\ast \backslash \lbrace w a b w' \mid w, w' ∈𝛴^\ast \rbrace\] \[∀x, y. (P_a(x) ∧ P_b(y)) ⟶ ¬ next(x,y)\]EX 4.
1.
- $M = (ℤ/2ℤ, +)$
- $𝜑(b) = 0$ si $b≠a$
- $𝜑(a)=1$
2.
| x*y | $𝜀$ | $a$ | $b$ | $ba$ | $\bot$ |
|---|---|---|---|---|---|
| $𝜀$ | $𝜀$ | $a$ | $b$ | $ba$ | $\bot$ |
| $a$ | $a$ | $a$ | $\bot$ | $\bot$ | $\bot$ |
| $b$ | $b$ | $ba$ | $b$ | $ba$ | $\bot$ |
| $ba$ | $ba$ | $ba$ | $\bot$ | $\bot$ | $\bot$ |
| $\bot$ | $\bot$ | $\bot$ | $\bot$ | $\bot$ | $\bot$ |
Leave a comment