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$