Information Technology Reference
In-Depth Information
x
·
Universal quantifiers and other Boolean connectives are defined naturally:
ˆ
≡¬∃
x
·¬
ˆ ,
X
·
ˆ
≡¬∃
X
·¬
ˆ , ˆ 1
ˆ 2 ≡¬
( ˆ 1
ˆ 2 )and ˆ 1
ˆ 2 ≡¬
ˆ 1
ˆ 2 .We
≡∀
x
·
( L a ( x )
∨¬
L a ( x )) and
↥≡¬
also define the formulas true and false:
.
We do not define the semantics of MSO formulas, neither the standard notion of
free and bound variables, but rather give examples and refer the reader to [19]
or [40] for formal definitions.
GivenanMSOformula ˆ ,wewrite ˆ ( x 1 ,...,x n ,X 1 ,...,X m ) to emphasise
the fact that the free first-order variables of ˆ are exactly x 1 ,...,x n , and its free
second-order variables are X 1 ,...,X m . Given a
S ʣ -structure M andanMSO
sentence ˆ ,wewrite M
|
= ˆ when M satisfies ˆ .Let i 1 ,...,i n
dom( M ),
I 1 ,...,I m
=
ˆ ( i 1 ,...,i n ,I 1 ,...,I m ) to denote the fact that M together with the interpreta-
tion of x j by i j , j =1 ,...,n and X j by I j , j =1 ,...,m ,satisfy ˆ .
Given an MSO sentence ˆ ,wewrite
dom( M ). For a formula ˆ ( x 1 ,...,x n ,X 1 ,...,X m ), we write M
|
ˆ
the set of words that satisfy ˆ , i.e.
ʣ |
ʣ , if there exists an MSO
ˆ
=
{
w
w
|
= ˆ
}
. Given a language L
sentence ˆ such that
ˆ
= L ,wesaythat L is MSO-definable, and that ˆ
defines L .
First-order logic First-order (FO) formulas over
S ʣ are MSO formulas in which
no second-order variable occurs.
Example 2. Let ʣ =
{
a, b
}
. The formula
x
·
defines the set of non-empty
words. The formula
L a ( x ) define the set of words over ʣ that contain at
least one position labelled a , i.e. the language ʣ .
The formula S ( x, y )
x
·
x
y
x
= y
∧∀
z
·
( x
z
y
( x = z
y = z ) defines
the successor relation.
The formula
L b ( y )) defines the set of words such
that any occurrence of the letter a is followed by the letter b . The formulas
x
y
·
( L a ( x )
S ( x, y )
first( x )
≡¬∃
y
·
S ( y,x )
and
last( x )
≡¬∃
y
·
S ( x, y )
ʣ + and i
are such that for all w
dom( w ), w
|
=first( i )iff i =1,and
w
|
=last( i )iff i =
.
The language a b is definable by the following formula:
|
w
|
L a ( y ))
More generally, it is known that the class of MSO-definable languages is the
class of regular languages [41]. The MSO formula
x
y
·
( L a ( x )
S ( y,x )
n
part( X 1 ,...,X n )
(
x
·
x
X i )
∧∀
x
·
( x
X i
x
X j )
i =1
i = j
holds true whenever X 1 ,...,X n defines a partition of the domain. Finally, one
can define the set of words of even length in MSO, but one needs second-order
variables X o and X e to capture, respectively, odd and even positions of the word,
as defined by the formula
ˆ o/e ( X o ,X e )
part( X o ,X e )
∧∀
x
·
(first( x )
x
X o )
∧∀
x
y
·
S ( x, y )
( x
X o
y
X e )
( x
X e
y
X o )
 
Search WWH ::




Custom Search