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
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
et ainsi de suite.
(2) ⟹ (1)
Montrons la contraposée : s’il existe un
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
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}$,
Soit $z_i = z’_i a_i$ pour $a_i∈𝛤$.
Du coup, on a pour tout $j≥0$ :
sans toucher à $z’_{i_j}$, donc
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
⟶ calculer $C(q, a)$ intersecté avec $q, 𝛤^\ast a$
Soit $R$ l’ensemble des $q, a$ qui vérifient cette propriété.
On calcule
EX 2. Logique MSO
1.
1.
2.
3.
4.
5.
6.
5.
6.
7.
8.
EX 3.
1.
2.
3.
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