TD 9 : Lemme de Dickson, PDA et logique MSO

Énoncé

EX 1 : Lemme de Dickson et PDA

1.

Montrons l’équivalence entre

  1. Pour tout $V$, $\min V$ est un ensemble fini

  2. 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$
\[L_2 = 𝜑^{-1}(𝜑(L_2))\]

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