Exercises 3: wSkS

EX 1: The power of wSkS

  • Finite automata: Reg ⟺ MSO on words ⟺ wS1S ⟺ Presburger arithmetic: +, =

  • Tree automata: Reg on trees ⟺ ℱ(a(2), b(0)), etc…

  • Hedges: at each stage, one can recognize a regular language

1.

The set $X$ has exactly two elements:

\[∃ \underbrace{x,y∈ X}_{\text{shortcut}}. x ≠ y ∧ (∀z. z∈ X ⟹ z = x ∨ z = y)\]

2.

The set $X$ contains at least one strings beginning with a 1:

\[∃x. x∈ X ∧ 1 ≤ x\]

(or: $∃y, z. y = ε ∧ z = y \cdot 1; z ≤ x$)

3.

$x ≤_{lex} y$ (lexicographic order on $\lbrace 1, ⋯, k \rbrace^\ast$):

\[∃z. \bigwedge_{1 ≤ i < j ≤ k} zi ≤ x ∧ zj ≤ y \\ ∨ x ≤ y\]

Ex: $12345 ≤_{lex} 12445$

4.

\[X ⊨ φ ≝ ∀x. x ∈ X ⟹ φ(x)\]

$φ$ is satisfied by an infinite number of words:

\[∀X. X ⊨ φ ⟹ ∃Y. X ⊊ Y ∧ Y ⊨ φ\]

NB: $X ≝ ∅$ satisfies $φ$

EX 2: The limit of wSkS

Recap:

If $(X, y) ≝ (\lbrace 12, 31 \rbrace, 11)$

  graph {
    rankdir=TB;
    zer1, zer2[label="00"];
    bot1, bot2, bot3, bot4, bot5[label="⊥⊥"];
    zer1 -- zer2, bot1, "0⊥";
  }
\[L = \lbrace (x, y) \mid x = 1y \rbrace\]

Let’s show there exists no wSkS formula recognizing $L$.

Idea: Pumping lemma

$x=1, y=11$

  graph {
    rankdir=TB;
    00 -- 10, ⊥⊥;
    10 -- ⊥1
  }

$x=12, y=2$

EX 3: Let’s try to minimize

  • $\sim_0: \lbrace ⊤ \rbrace, \lbrace q_a, q_b, ⊥, q_g, q_f\rbrace$
  • $\sim_1: \lbrace ⊤ \rbrace, \lbrace q_a, ⊥, q_b \rbrace, \lbrace q_g, q_f \rbrace$
  • $\sim_2: \lbrace ⊤ \rbrace, \lbrace q_a \rbrace, \lbrace q_b \rbrace, \lbrace ⊥ \rbrace, \lbrace q_g, q_f \rbrace$

So $q_f$ and $q_g$ can be merged into the same state.

EX 4: To infinity… and beyond!

Rules of the form: $a(R) ⟶ q_a$

  • $Q ≝ \lbrace q_a, q_b, ⊤ \rbrace$
  • $Q_f = \lbrace q_b, ⊤ \rbrace$

$Δ$:

  • $a(ε) ⟶ q_a$
  • $b(ε) ⟶ q_b$
  • $a(⊤^+) ⟶ ⊤$
  • $b(⊤^+) ⟶ ⊤$
  • $b(Q^\ast q_b Q^\ast) ⟶ q_b$
  • $a(Q^\ast q_b Q^\ast) ⟶ ⊤$
  • $a((q_a + ⊤)^\ast q_a (q_a + ⊤)^\ast) ⟶ q_a$
  • $b((q_a + ⊤)^\ast q_a (q_a + ⊤)^\ast) ⟶ q_a$

$q_a$: I have seen an $a$-labelled leaf

$q_b$: I have seen a $b$-labelled branch

Leave a comment