Notes on MSO Transducers

Credibility

This article references information generated by AI. It is a memo for research and learning. Please verify accuracy and factuality yourself. In particular, I cannot judge whether terms actually exist or are used in Japanese, so I use the LLM-generated terms as-is.

##Introduction

I touched MSO Transducers briefly as an undergraduate, but never gained intuition for them. Now that LLMs lower the learning barrier, I thought I might understand them better, so I'm revisiting the topic and taking notes within what I can understand.

##First-Order Logic (FOL)

In first-order logic, we treat elements of a set as variables and can quantify over them. Here, variables and quantifiers mean:

• First-order variables: written as lowercase letters like $x, y, z, \dots$, representing individual elements of a set
• Quantifiers: universal/existential quantifiers using $\forall$ and $\exists$ meaning "for all" and "there exists"

For example, the following predicate says: "for every $x$, there exists a $y$ such that $y = x + 1".

$$\forall x \exists y (y = x + 1)$$

So far, this is straightforward.

##Monadic Second-Order Logic (MSO)

In second-order logic (SOL), we can quantify over relations or functions of elements. In MSO, we restrict quantification to unary relations (monadic relations), i.e., sets. We can also use structure-specific predicates called atomic formulas.

For example, a graph being 2-colorable can be expressed by:

$$\exists R \exists B (\forall v (v \in R \lor v \in B)) \land \forall u \forall v ((u, v) \in E \to \lnot ((u \in R \land v \in R) \lor (u \in B \land v \in B)))$$

Here $R$ (red) and $B$ (blue) are sets of vertices, and $E$ is the edge set.

It suddenly looks complex, so let's break it down:

• $\exists R \exists B$:
  • There exist vertex sets $R$ and $B$
• $\forall (v \in R \lor v \in B)$:
  • For every vertex $v$, it is in $R$ or $B$
• $\forall u \forall v ((u, v) \in E \to \dots)$:
  • For all vertices $u, v$, if $(u, v)$ is an edge, then ...
• $\lnot ((u \in R \land v \in R) \lor (u \in B \land v \in B))$:
  • $u \in R \land v \in R$: both $u$ and $v$ are in $R$
  • $u \in B \land v \in B$: both $u$ and $v$ are in $B$

With this breakdown it's understandable. Indeed, graphs satisfying this predicate are 2-colorable.

So the set of all 2-colorable graphs is definable in MSO.

I remember learning how to describe graphs with predicates in graph theory lectures, but I had forgotten. Even when researching MSO, I didn't connect it with graph theory. In class, it was presented as "graphs can be expressed with predicates," but I didn't think about the logical class involved.

##Büchi–Elgot–Trakhtenbrot theorem

The Büchi–Elgot–Trakhtenbrot theorem shows that MSO over strings and regular languages have equivalent expressive power. It was proved in a paper from 1960, so it has been known for a long time.

It was an important result bridging logic and automata theory. I haven't studied automata theory comprehensively, so I didn't know it. Maybe I should read Elements of Automata Theory after all.

As an undergraduate, I read [1706.01668] One-way definability of two-way word transducers where MSO Transducers appear, but I didn't even know that regular languages are MSO-definable. So if I reread it now, I might understand more.

##Courcelle's Theorem

Courcelle's Theorem states that for graphs of bounded treewidth, any property definable in MSO can be decided in linear time.

This seems related to tree automata. According to Gemini Deep Research, as with strings, the class of trees definable by regular tree languages and MSO coincide. I want to verify that later.

It's amazing that you can wait 20 minutes and have the web automatically researched for you. I wish I had that as a student.

I will leave the HTML version of the DeepResarch results here (accuracy unknown).

The rapid explosion in complexity from $k = 4$ or $k = 5$ reminds me of my undergraduate thesis results.

##MSO Transducers

###Example: String transformation

Consider transforming a string over alphabet ${a, b, c}$ by replacing $a$ with $b$, $b$ with $c$, and $c$ with $a$. This can be expressed by:

• $L_b'(p') \iff L_a(p)$
• $L_c'(p') \iff L_b(p)$
• $L_a'(p') \iff L_c(p)$

Here $L_a$, $L_b$, $L_c$ are predicates true at position $p$ in the input string when the character is $a$, $b$, $c$. $L_a'$, $L_b'$, $L_c'$ are similar predicates for position $p'$ in the output string. $p$ and $p'$ indicate the same position in input and output.

This is a fairly casual definition, but it is enough to capture what MSO can do. I'll try a more rigorous definition later.

###Example: Complement graph generation

Consider transforming a graph $G = (V, E)$ into its complement $\overline{G} = (V, \overline{E})$. The complement graph has the same vertex set and edges between vertices that are not connected in the original graph.

For MSO transformation, input and output are:

• Input: graph $G = (V, E)$
• Output: complement graph $\overline{G} = (V, \overline{E})$

Transformation rules

1. Define output vertex set:
   • $\forall (v \in V_{\mathrm out} \iff v \in V_{\mathit in})$
   • The output vertex set is identical to the input vertex set.
2. Define output edge set:
   • $\forall u \forall v ((u, v) \in E_{\mathit out} \iff u \neq v \land \lnot ((u, v) \in E_{\mathit in}))$
   • "There is an edge between $u, v$ in the output graph iff $u \neq v$ and there is no edge between them in the input graph."

These definitions are in MSO, so complement graph generation is an MSO transformation.

##A more formal definition

The earlier examples were too informal, so let's define MSO transformations more formally.

###Formal definition of string structures

A $\Sigma$-string structure is defined as a tuple $S = \langle D, <, (P_c)_{c \in \Sigma} \rangle$ where:

• $D$: Domain, a finite set of positions.
• $<$: a total order on $D$.
• $(P_c)_{c \in \Sigma}$: a set of labels. For each $c \in \Sigma$, $P_c$ is a subset of $D$ representing positions where character $c$ occurs.
  • $P_a(p)$ means "the character at position $p$ is $a".

###Formal definition of MSO transformations

An MSO transformation $T$ is defined as a relation from input structure $S_{\mathit in}$ to output structure $S_{\mathit out}$. The relation is specified by a single MSO formula $\varphi_T$.

The formula $\varphi_T$ is written over the input structure $(D_{\mathit in}, <_{\mathit in}, P_c)$ and output structure $(D_{\mathit out}, <_{\mathit out}, P_c')$.

A pair $(S_{\mathit in}, S_{\mathit out})$ belongs to $T$ iff it satisfies $\varphi_T$:

$$(S_{\mathit in}, S_{\mathit out}) \in T \iff (S_{\mathit in}, S_{\mathit out}) \vDash \varphi_T$$

###Example

Let's revisit the transformation that maps $a \to b$, $b \to c$, $c \to a$, now with a formal definition.

First define input and output structures:

• Input: $S_{\mathit in} = \langle D_{\mathit in}, <_{\mathit in}, P_a, P_b, P_c \rangle$
• Output: $S_{\mathit out} = \langle D_{\mathit out}, <_{\mathit out}, P_a', P_b', P_c' \rangle$

Next define a formula expressing that the input and output structures are isomorphic when labels are ignored:

$$\varphi_{\mathit iso} \equiv (D_{\mathit in} = D_{\mathit out}) \land (\forall x \forall y (x <_{\mathit in} y \leftrightarrow x <_{\mathit out} y))$$

This says the domains are equal (same string length) and the order of positions is the same.

Define the relabeling rules:

$$\varphi_{\mathit relabel} \equiv \forall x \in D_{\mathit in} \left( \begin{align*} (P_a(x) \leftrightarrow P_b'(x)) \land \\ (P_b(x) \leftrightarrow P_c'(x)) \land \\ (P_c(x) \leftrightarrow P_a'(x)) \end{align*} \right)$$

This refers to the labels at the same position.

Finally, the overall transformation formula is:

$$\varphi_T \equiv \varphi_{\mathit iso} \land \varphi_{\mathit relabel}$$

Thus the transformation is expressible in MSO logic.

Execution example

Let's check the behavior for input $abac$.

1. Input structure $S_{\mathit in}$
   • $D_{\mathit in} = \{1, 2, 3, 4\}$
   • $<_{\mathit in} = \{(1, 2), (1, 3), (1, 4), (2, 3), (2, 4), (3, 4)\}$
   • $P_a = \{1, 3\}$, $P_b = \{2\}$, $P_c = \{4\}$
2. Output structure $S_{\mathit out}$
   • $D_{\mathit out} = \{1, 2, 3, 4\}$
   • $<_{\mathit out} = <_{\mathit in}$
   • Output labels from relabeling rules:
     • $P_a \leftrightarrow P_b'$: $P_a = \{1, 3\}$ so $P_b' = \{1, 3\}$
     • $P_b \leftrightarrow P_c'$: $P_b = \{2\}$ so $P_c' = \{2\}$
     • $P_c \leftrightarrow P_a'$: $P_c = \{4\}$ so $P_a' = \{4\}$

Interpreting $S_{\mathit out}$ as a string yields $bcba$.

Personally, it feels a bit strange that you can define a transformation this way, but it reminds me of writing programs in Prolog.

##MSO has variants

It seems MSO has multiple variants. By adding predicates to the logic, the class of definable transformations changes.

For graphs: $\mathrm{MSO}_1$ can use adjacency $\mathit{adj}(u, v)$, $\mathrm{MSO}_2$ can use incidence $\mathit{inc}(v, e)$, $\mathrm{CMSO}$ can use $\mathit{card}_{p,q}(X)$ to check cardinality modulo $q$ and $p$, and there are extensions like $\mathrm{EMSO}$ / $\mathrm{LinEMSOL}$ that add predicates for minimal/maximal size of sets satisfying an MSO property.

##Conclusion

I reviewed MSO Transducers with examples. When thinking about structures or transformations, I naturally imagine constructive definitions, so defining a structure and then expressing transformations via logic over that structure still doesn't feel natural. This is probably part of proofs, but I feel it's hard to define a transformation purely in logical form unless you have practiced converting constructive definitions into logical ones. Properties like 2-colorability or complement graphs are clear enough that logical definitions come naturally, but arbitrary transformations are harder.

Next, I want to look into proofs of the theorems mentioned here and related theory.