LOCALLY FINITE LANGUAGES

Olivier Finkel Equipe de Logique Mathématique CNRS URA 753 et Université Paris 7

U.F.R. deMathématiques, 2 Place Jussieu 75251 Paris cedex 05, France. E Mail: finkel@logique.jussieu.fr

Abstract

We investigate properties of locally finite languages introduced by J-P. Ressayre in [Res88]. These languages are defined by locally finite sentences and generalize languages recognized by automata or defined by monadic second order sentences. We give many examples, showing that numerous context free languages are locally finite. Then we study closure properties of the family LOC of locally finite languages, and show that most undecidability results that hold for context free languages may be extended to locally finite languages. In a second part, we consider an extension of these languages to infinite and transfinite length words. We prove that each α-language which is recognized by a Büchi automaton ( where α is an ordinal and ω ≤ α < ω^{ω} ) is defined by a locally finite sentence. This result, combined with a preceding one of [FR96], provides a generalization of Büchi’s result about decidability of monadic second order theory of the structure (α, <).

1 Introduction

In the sixties J.R. Büchi established some ties between monadic second order logic and finite automata, [Büc60]. When a word over a finite alphabet is considered as a structure in a natural manner, a finitary language is recognized by a finite automaton if and only if it is the class of finite models of a monadic second order sentence. And the distinction between first order and second order sentences is here very significant: first order sentences define the important class of star free languages, [Pin96] [Par83].

In 1974 R. Fagin proved that the class NP is characterized by existential second order formulas, [Fag93]. Since then, many complexity classes like P, PSPACE, LogSPACE, NLogSPACE, have been proved to be characterized by different versions of second order logic with the use of, for example, fixed point operators or transitive closure operators [Tho96]. This led to the now called descriptive complexity theory, (see [Tho96], [Fag93], [Imm87],

[EF95] for more results and references). A logical characterization of context free languages has been recently found by C. Lauteman, T. Schwentick and D. Therien, involving second order quantifications over some special binary relations called matchings, [LST94]. A logical characterization for Petri Net languages had been found by M. Parigot and E. Pelz, [PP85].

To prove the decidability of the monadic second order theory of one successor over the integers, and further over the structure (α, <), for α a countable ordinal, J.R. Büchi and D. Siefkes studied ω-languages ( and α-languages ) which are recognized by finite automata reading infinite ( and transfinite ) length words. An α-language is shown to be accepted by a finite automaton iff it is defined by a monadic second order formula, [Büc62] ,[BS73]. Since then the expressive power of other logics, such as temporal logics, over infinite words has been studied, and many results have been stated. See [Tho90], [Tho96], [Pin96], [PP98], [Sta97], [LT94] for more results and references.

The case of transfinite length word languages appear in the theory of traces for the modelization of concurrency [DR95] and in the work about timed automata when one consider that an infinite number of actions may happen during a finite period of time [AD94], [BP97]. The languages of transfinite length words which are recognized by finite automata have been recently studied by N. Bedon in [Bed96], [Bed98] where the extension of the equivalence between first order sentences and star free languages is shown.

To extend these results, J-P. Ressayre, in order to apply ideas and machinery of model theory to the study of formal languages, introduced in [Res88] the locally finite sentences and the locally finite and free locally finite languages. He showed that these latter languages may be seen as a class of finite structures satisfying a strong finitary analogue to the properties of a universal and complete class of first order structures equipped with elementary embeddings.

Locally finite sentences are first order, but they define locally finite languages, via existential quantifications over relations and functions which appear in the locally finite sentence. And these second order quantifications are much more general than the monadic ones as the following results show:

• Each rational language is locally finite, [Res88].

• Each quasirational language is locally finite, Theorem 2.21 below.

• Each ω-language which is accepted by a Büchi automaton is a locally finite ω-language, [Fin89] and Theorem 5.7 below.

• And there exist much more locally finite (ω-)languages, see section 2 below and [Fin89],[Fin99].

But syntaxic and semantic restrictions (a locally finite sentence is equivalent to a universal one and its models satisfy simple structural properties) make locally finite ω-languages keep important properties of rational ω-languages. The pumping lemma of [Res88] is an analogue for each locally finite ωlanguage of the property : ” A rational ω-language is non empty if and only if it contains an ultimately periodic word ”. And this lemma implies in a similar manner the decidability of the emptiness problem for locally finite ω-languages. And similar results exist for α-languages, where α is an ordinal < ω^{ω}, [FR96]. And other pumping lemmas based on the existence of indiscernables in a model imply decidability of problems like: is a finitary locally finite language infinite?

We study here first the finitary locally finite languages. In section 2, we give many examples. The question to know whether every context free language is locally finite remains open contrary to that is asserted in [Res88]. But Dyck languages and quasirational languages as many other context free languages are locally finite. We then study two hierarchies which are located between context free and context sensitive languages: there are locally finite languages at each level of these hierarchies.

In section 3, classical closure properties are investigated. Locally finite languages are closed under union, concatenation product and star operation [Res88]. We show that the class LOC of locally finite languages is closed under substitution, morphism, alphabetic inverse morphism, but not under intersection, complementation, intersection with a rational language, inverse morphism. These latest results are obtained by the use of the notion of rational cone.

In section 4, numerous undecidable problems for context free languages are shown to remain undecidable when locally finite languages are considered. In particular, given an alphabet Σ containing more than two letters, it is undecidable to determine, for arbitrary given locally finite languages L(φ) and L(ψ) over Σ, whether L(φ) ∩ L(ψ) is empty, infinite, rational, context free or locally finite, whether L(φ) ⊆ L(ψ), whether

L(φ) = L(ψ), whether L(φ) is rational, whether ^{c}L(φ), the complement of L(φ), is empty, infinite, rational, or locally finite.

In section 5 and 6, we consider an extension of locally finite languages to infinite and transfinite length words. We show that every α-language which is recognized by a Büchi finite automata, (with ω ≤ α < ω^{ω}), is a locally finite α-language. This gives a new decision algorithm for the emptiness problem for Büchi α-languages. And this permits us to consider other new decidability results based on the use of indiscernables in a model. This shows also that the expressive power of the formulas ∃R_{1}...R_{k}φ(R_{1}...R_{k}), where φ(R_{1}...R_{k}) is locally finite in the signature {<, R_{1}, ..., R_{k}}, is stronger than that of the monadic second order formulas while keeping decidability properties for the structure (α, <), ω ≤ α < ω^{ω}. Hence this provides a generalization of Büchi’s result.

2 Examples of locally finite languages

2.1 First definitions

We briefly indicates now some basic facts about first order logic and model theory. More information may be found in textbooks, like [CK73] or [Sch67].

We consider here formulas of first order logic. The language of first order logic contains (first order) variables x, y, z, ... ranging over elements of a structure, logical symbols: the connectives ∧ (and), ∨ (or), → (implication), ¬ (negation), and the quantifiers ∀ (for all), and ∃ (there exists), and also the binary predicate symbol of identity =. A signature is a set of constant, relation ( different from = ) and function symbols. we will consider here only finite signatures.

Let Sig a finite signature. We define first the set of terms in the signature Sig which is built inductively as follows:

1. A variable is a term.

2. A constant symbol is a term.

3. If F is a m-ary function symbol and t_{1}, t_{2}, ..., t_{m} are terms, then F (t_{1}, ..., t_{m}) is a term.

We then define the set of atomic formulas which are in the form given below:

1. If t_{1} and t_{2} are terms, then t_{1} = t_{2} is an atomic formula.

2. If t_{1}, t_{2}, ..., t_{m} are terms and R is a m-ary relation symbol, then R(t_{1}, ..., t_{m}) is an atomic formula.

Finally the set of formulas is built inductively from atomic formulas as follows:

1. An atomic formula is a formula.

2. If φ and ψ are formulas, then φ∧ψ, φ∨ψ, φ → ψ and ¬φ are formulas.

3. If x is a variable and φ is a formula, then ∀xφ and ∃xφ are formulas.

An open formula is a formula with no quantifier. We assume the reader to know the notion of free and bound occurrences of a variable in a formula. Then a sentence is a formula with no free variable. A sentence in prenex normal form is in the form φ = Q_{1}x_{1}...Q_{n}x_{n}φ_{0}(x_{1}, ..., x_{n}), where each Q_{i} is either the quantifier ∀ or the quantifier ∃ and the formula φ_{0} is an open formula. It is well known that every sentence is equivalent to a sentence written

in prenex normal form. A sentence is said to be universal if it is in prenex normal form and each quantifier is the universal quantifier ∀.

We then recall the notion of a structure in a signature Sig: A structure is in the form:

M = (|M|, (a^{M})_{a∈Sig})

Where |M| is a set called the universe of the structure, and for a ∈ Sig, a^{M} is the interpretation of a in M: If f is a m-ary function symbol in Sig, then f^{M} is a function: M^{m} → M. If R is a m-ary relation symbol in Sig, then R^{M} is a relation: R^{M} ⊆ M^{m}. If a is a constant symbol in Sig, then a^{M} is a distinguished element in M.

When M is a structure and φ is a sentence in the same signature Sig, we write M ⊧ φ for ” M is a model of φ ”, which means that φ is satisfied in the structure M. More details about these notions may be found in [CK73] or [Sch67].

When M is a structure in the signature Sig and Sig_{1} is another signature such that Sig_{1} ⊆ Sig, then the reduction of M to the signature Sig_{1} is denoted M|Sig_{1}. It is a structure in the signature Sig_{1} which has same universe |M| as M, and the same interpretations for symbols in Sig_{1}. Conversely an expansion of a structure M in the signature Sig_{1} to a structure in the signature Sig has same universe as M and same interpretations for symbols in Sig_{1}.

When M is a structure in a signature Sig and X ⊆ |M|, we define: cl^{1}(X, M) = X ∪ ⋃_{{f n−ary function of Sig }} f^{M}(X^{n}) ∪ ⋃_{{a constant of Sig }} a^{M} cl^{n+1}(X, M) = cl^{1}(cl^{n}(X, M), M) for an integer n ≥ 1 and cl(X, M) = ⋃_{n≥1} cl^{n}(X, M) is the closure of X in M.

Let us now define locally finite sentences:

Definition 2.1 A first order sentence φ ( in the signature S(φ)= non logic symbols appearing in φ ) is locally finite if and only if (iff):

a) M ⊧ φ and X ⊆ |M| imply cl(X, M) ⊧ φ

b) ∃n ∈ ℕ such that ∀M, if M ⊧ φ and X ⊆ |M|, then cl(X, M) = cl^{n}(X, M), where cl(X, M) is the closure of X in M and cl^{n}(X, M) is the subset obtained from X applying at most n times the functions of S(φ). (closure in models of φ takes less than n steps).

Notation. For a locally finite sentence φ, let n_{φ} be the smallest integer n ≥ 1 verifying b) of the above definition.

Remark 2.2 Because of a) of Definition 2.1, a locally finite sentence φ is always equivalent to a universal sentence, So we may assume that we are still in that case.

Let us now introduce basic notations for words. Let Σ be a finite alphabet whose elements are called letters. A finite word over Σ is a finite sequence of letters: x = a_{0}...a_{n} where ∀i ∈ [0; n] a_{i} ∈ Σ. We’ ll denote x(i) = a_{i} the i + 1^{th} letter of x. The length of x is |x| = n + 1. The empty word will be denoted by λ and has 0 letter. Its length is 0. The set of finite words over Σ is denoted Σ^{⋆}. Σ^{+} = Σ^{⋆} − {λ} is the set of non empty words over Σ. A (finitary) language L over Σ is a subset of Σ^{⋆}. Its complement ( in Σ^{⋆} ) is ^{c}L = Σ^{⋆} − L. When x = a_{0}...a_{n} is a word over Σ and the a_{i} are letters, we denote x^{R} = a_{n}...a_{0} the word obtained from x by the reverse operation. The usual concatenation product of u and v will be denoted by u.v or uv. ℕ will be the set of non negative integers. For V ⊆ Σ^{⋆}, we denote V^{⋆} = {v_{1}...v_{n}/n ∈ ℕ and v_{i} ∈ V ∀i ∈ [1; n]}.

A word over Σ may be considered as a structure in the following usual manner:

Let Σ be a finite alphabet. We denote P_{a} a unary predicate for each letter a ∈ Σ and Λ_{Σ} the signature {<, (P_{a})_{a∈Σ}}. Let σ be a word over the alphabet Σ, |σ| is the length of the word σ. We may write that |σ| = {0, 1, ...., |σ|−1}. σ is identified to the structure (|σ|, <^{σ}, (P_{a}^{σ})_{a∈Σ}) of signature Λ_{Σ} where P_{a}^{σ} = {i < |σ|/ the i + 1^{th} letter of σ is an a }.

Definition 2.3 Let Σ be a finite alphabet and L be a language of finite words over the alphabet Σ, L ⊆ Σ^{⋆}. Then L is a locally finite language ⟷ there exists a locally finite sentence φ in a signature Λ ⊇ Λ_{Σ} such that σ ∈ L iff ∃M, M ⊧ φ and M|Λ_{Σ} = σ. ( where M|Λ_{Σ} is the reduction of M to the signature Λ_{Σ}). We then denote L = L^{Σ}(φ) , and to simplify, when there is no ambiguity, L = L(φ) the locally finite language defined by φ. The class of locally finite languages will be denoted LOC.

The empty word λ has 0 letter. It is represented by the empty structure.

Remark 2.4 The most natural convention concerning the possibility for a structure to have an empty domain is that an empty structure of signature Λ exists if Λ does not contain any constant symbol. A sentence of Λ is then true in the empty structure if under prenex form it begins by ∀ and false if it begins by ∃. Let then L(φ) be a locally finite language. If λ ∈ L(φ), let d ∉ S(φ) and φ′ = φ ∧ (d = d), then φ′ is locally finite, S(φ′) = S(φ) ∪ {d} where d is a new constant symbol. And it holds that L(φ′) = L(φ) − {λ}. Conversely assume that λ ∉ L(φ). We then replace each constant symbol c of φ by a unary function symbol c(u), each occurrence of c in φ by c(u) for each constant c, we place ∀u in front of φ and we add to φ the sentence ∀uv ⋀_{c} c(u) = c(v). The resulting sentence φ′ is locally finite and verifies L(φ′) = L(φ) ∪ {λ}.

Remark 2.5 We call locally finite sentences the above defined sentences by analogy with the notion of a locally finite group. Each finite subset of a locally finite group generates a finite subgroup. Here each finite subset of a model of a locally finite sentence generates a finite submodel and moreover with a uniform upper bound over the iteration number which is necessary to obtain the generated submodel.

The notion of locally finite language seemingly looses its initial signification because a subword of a finite word always generates a finite word. Nevertheless, there is moreover a uniform bound, and we may also consider words of infinite and even transfinite length of which each finite subword generates a finite subword. We’ ll then keep the notion of language defined by a locally finite sentence. The notion of locally finite language is very different of the usual notion of local language which represents a subclass of the class of rational languages. But whenever the things are well defined and precised, in a precise context and when there will be no ambiguity, we’ll always call local languages the locally finite languages. So in the course of this paper.

2.2 First properties

Proposition 2.6 a) The set of local sentences is recursively enumerable.

b) It is undecidable to determine whether an arbitrary sentence φ is a local one.

Proof of a). Let T_{n}(φ) be the set of terms obtained by applying at most n times the functions of S(φ) and T (φ) = ∪_{n≥1}T_{n}(φ). We express by a first order formula the statement ” T_{n}(φ) generate T (φ) ” :

⋀_{{ffunction∈S(φ),t_{1},...,t_{k}∈T_{n}(φ)}} ∀ū ⋁_{t∈T_{n}(φ)} ∃(sequence v̄ of points of ū)f(t_{1}(ū)...t_{k}(ū)) = t(v̄)

Then we enumerate all the proofs, checking whether they prove that:

φ ⊢ [T_{n}(φ) generate T (φ)], for some n ∈ ℕ

. If φ is local we obtain such a proof for some n ≥ n_{φ}.

For an exact definition of a proof, see for example [CK73].

Proof of b). By Church’s Theorem, it is undecidable to determine whether an arbitrary sentence φ is consistent, (recalling that a first order sentence is said to be consistent if it has at least one model, otherwise the sentence is said to be inconsistent). From this result we can deduce b): Indeed otherwise, admitting that a non consistent sentence is local, two cases may happen: First case: φ is not local, then φ is consistent. Second case: φ is local. As in the proof of a), we can find an integer n ≥ n_{φ} and therefore, if there exists a model of φ, we find one such model which cardinal is finite and bounded by an integer m obtained from n. Otherwise φ is not consistent.

In each case the algorithm determines whether φ is consistent, But ” φ is consistent ” is undecidable, then a contradiction would appear.

This negative result does not depend on the convention we have chosen: ” a non consistent sentence is local ”. Indeed:

Proposition 2.7 There does not exist any algorithm A which, for every sentence ψ, decide whether ψ is local and consistent.

Proof. Otherwise let p be a propositional variable an let ψ_{0} be a consistent local sentence . Using A, here is an algorithm which, for every sentence ψ, decide whether ψ is consistant. We put (¬p ∧ ψ) ∨ (ψ_{0} ∧ p) = θ as entry for A.

–If A answers that θ is local and consistent, we find n ≥ n_{θ} as in the preceding proof, then we look for a model of ψ which cardinal is bounded by a bound depending on n. If we find such a model, then ψ is consistent, otherwise ψ is not.

– If A answers that θ is not ” local and consistent ”, then ψ is consistent (because θ being consistent as ψ_{0} is, the answer of A means that ψ is not local, then ψ is consistent).

In a similar manner, we obtain:

Proposition 2.8 There does not exist any algorithm A which, for every consistent sentence ψ, decide whether ψ is local.

Per contra to these negative results, there exists a ”recursive presentation” up to logical equivalence of all local sentences ( two sentences φ and ψ in the same signature are said to be equivalent iff they have the same models, we then write φ ≡ ψ ):

Theorem 2.9 There exists a recursive set L of local sentences and a recursive function F such that:

1) ψ local ⟷ ∃ψ′ ∈ L such that ψ ≡ ψ′.

2) ψ′ ∈ L ⟶ n_{ψ′} = F (ψ′).

Proof. The elements of L are the ψ ∧ C_{n}, where ψ run over the universal formulas and C_{n} run over the universal formulas in the signature S(ψ) which express that closure in a model takes at most n steps. ψ ∧ C_{n} is local and n_{ψ∧C_{n}} ≤ n. Then we can compute n_{ψ∧C_{n}}, considering only finite models of cardinal ≤ m, where m is an integer depending on n. And each local sentence ψ is equivalent to a universal formula θ, hence ψ ≡ θ ∧ C_{n_{ψ}}.

These results are due to J-P. Ressayre.

From now on, in the sequel of this paper, we’ ll assume that the local sentences, whenever they are not explicit, belong to this recursive set L.

2.3 Examples of locally finite languages

Remark that in the following examples, to prove that a language is local, we sometimes use the closure properties of the class LOC which will be shown in the next section.

Example 2.10 Rational languages. Recall that every rational language is a local language. This result is proved in [Res88] by induction on the complexity of a regular expression defining a rational language. It is clear that each language containing only one word of length 1, a ∈ Σ, is defined by the local sentence ∀x[x = A∧P_{a}(A)] in the signature {<, P_{a}, A}, where A is a constant symbol. Then each rational language is local because LOC is closed under union, concatenation product and star operation ( see Theorem 3.1 below ).

Example 2.11 Dyck and Antidyck Languages.

Recall the following:

Definition 2.12 The Antidyck language over two sorts of parentheses is the following language: Q_{2}^{′⋆} = {v ∈ (Y ∪ Ȳ)^{⋆}/v →^{⋆} λ}, where Y = {y_{1}, y_{2}}, Ȳ = {ȳ_{1}, ȳ_{2}} and →^{⋆} is the transitive closure of → defined in (Y ∪ Ȳ)^{⋆} by ∀y ∈ Y, yv_{1}ȳv_{2} → v_{1}v_{2} if and only if (iff) v_{1} ∈ Y^{⋆}.

Remark 2.13 This language may be seen as constituted by words with two sorts of parentheses, such that: ” the first parenthesis to be opened is the first to be closed”

Definition 2.14 The Dyck language D_{2}^{′⋆} is defined in a similar manner but with v_{1}yȳv_{2} → v_{1}v_{2}, ∀v_{1}, v_{2} ∈ (Y ∪ Ȳ)^{⋆}.

Remark 2.15 This time we have: ” the first opened parenthesis is the last to be closed”.

These definitions are generalized to Dyck and Antidyck languages D_{n}^{′⋆} and Q_{n}^{′⋆} with n sorts of parentheses , n ≥ 1. Then we show the:

Proposition 2.16 These languages D_{n}^{′⋆} and Q_{n}^{′⋆} are local.

Proof. Let us show that D_{n}^{′⋆} is a local language. D_{n}^{′⋆} is a language over the alphabet Σ = {y_{1}, ..., y_{n}, ȳ_{1}, ..., ȳ_{n}}. The letters y_{i}

represent here the open parentheses, and the letters ȳ_{i} represent the closed parentheses corresponding to the y_{i}. We give a sentence φ_{n} in the signature S(φ_{n}) = {(P_{a})_{a∈Σ}, <, s}, where s is a unary function symbol. φ_{n} is the conjunction of the following sentences:

• ∀xyz[(x ≤ y ∨ y ≤ x) ∧ (x ≤ y ∧ y ≤ x ↔ x = y) ∧ (x ≤ y ∧ y ≤ z → x ≤ z)] (this means: “ < is a linear order ”),

• ∀x[(⋁_{a∈Σ} P_{a}(x)) ∧ (⋀_{(a,a′)∈Σ^{2},a≠a′} ¬(P_{a}(x) ∧ P_{a′}(x)))] ( this means: (P_{a})_{a∈Σ} form a partition ),

• ∀x[P_{y_{i}}(x) → x < s(x)], for each i ∈ [1, n],

• ∀xz[(P_{y_{i}}(x) ∧ P_{y_{j}}(z) ∧ x < z) → s(z) < s(x)], for all i, j ∈ [1, n],

• ∀x[P_{y_{i}}(x) ↔ Pȳ_{i}(s(x))], for each i ∈ [1, n],

• ∀x[s(s(x)) = x].

φ_{n} is equivalent to a universal formula and closure in its models takes only one step because ∀x[s(s(x)) = x]. Then φ_{n} is a local sentence and we easily verify that L(φ_{n}) = D_{n}^{′⋆}.

Remark 2.17 In the sequel, (< is a linear order) and ((P_{a})_{a∈Σ} form a partition) are abreviations for the corresponding first order sentences written above.

Example 2.18 L = {a^{n_{1}}ba^{n_{2}}b...a^{n_{p}}ba^{n_{p+1}}c...a^{n_{2p}}c/n_{i} ≥ 0, p ≥ 1} is local.

Proof. This context free language is given by the local sentence φ which is the conjunction of:

• (< is a linear order ),

• (P_{a}, P_{b}, P_{c}, form a partition ),

• ∀xy[(P_{b}(x) ∧ P_{c}(y)) → x < y],

• ∀x[P_{c}(x) ↔ P_{b}(s(x))],

• ∀x[s(s(x)) = x].

• ∀x[P_{a}(x) → s(x) = x],

• ∀x[x ≤ d ∧ P_{c}(d)]. φ is given in the signature S(φ) = {<, P_{a}, P_{b}, P_{c}, s, d}, where s is unary function symbol and d is a constant symbol. φ is equivalent to a universal formula and closure in its models takes only two steps because it suffices to add the element which interprets d and then to take the closure by s in one step to obtain the closure in a model of φ. Example 2.19 The language L = {0^{n}1^{p}/0 ≤ n, p ≤ 2^{n}} is local over the alphabet Σ = {0, 1}, while its complement ^{c}L = {u10v/u, v ∈ Σ^{⋆}}∪{0^{n}1^{p}/0 ≤ n, p > 2^{n}} is not local. The language L is local: let φ be the following sentence which signature is {<, P_{0}, P_{1}, ∈ f}, where f is a binary function symbol and ∈ is a binary relation symbol. φ is the the conjunction of:

• (< is a linear order ),

• (P_{0}, P_{1}, form a partition ),

• ∀xy[(P_{0}(x) ∧ P_{1}(y)) → x < y],

• ∀xy[(x ∈ y) → (P_{0}(x) ∧ P_{1}(y))],

• ∀x[f(xx) ∈ x ↔ P_{1}(x)],

• ∀xy[(x ≠ y ∧ P_{1}(x) ∧ P_{1}(y)) → ((f(xy) ∈ x ∧ f(xy) ∉ y) ∨ (f(xy) ∈ y ∧ f(xy) ∉ x))],

• ∀xy[P_{0}(x) ∨ P_{0}(y) → f(xy) = min(xy)].

A model M of φ is formed by two successive and disjoint segments P_{0}^{M} and P_{1}^{M}. One may consider that P_{1}^{M} is a subset of the set of nonempty subsets of P_{0}^{M}. In fact, there is an injection j : P_{1}^{M} → 2^{P_{0}^{M}} − { emptyset }, defined by j(x) = {z ∈ M/z ∈^{M} x}. This property in particular implies that card(P_{1}^{M})≤ 2^{card(P_{0}^{M})}. The function f^{M} defined by φ is then a choice function which permits to see that j is injective. φ is equivalent to a universal formula and closure in its models takes only one step. And we easily see that L = L(φ) ∪ L(φ).1 and so L is a local language. But if ^{c}L was local, for sufficiently large integer n, the word 0^{n}1^{2^{n}+1} of ^{c}L would have a strict subword containing 0^{n} and also being in ^{c}L (because the closure of 0^{n} in 0^{n}1^{2^{n}+1} would take at most n_{φ} steps, where n_{φ} does not depend on n). This example is due to J-P. Ressayre.

Example 2.20 Quasirational languages.

The quasirational languages, also called non expansive, finite index, superlinear, have given rise to a great interest. With its two subfamilies of ultralinear and bounded languages, the family of quasirational languages has been more or less the subject of a large part of the work done about context free languages. The main advantage of these languages is the richness of their algebraic structures. Their various characterizations, using some very diverse concepts, like automata, grammars, closure under operators, algebraic expressions, provide efficacious investigation tools which generally fail in language theory. More, quasirational languages take a fundamental place into the context free languages general theory. The family of quasirational languages is the closure under substitution of the cone of linear languages. It is also the family of languages which are generated by finite index context free grammars [Cre73]. Then we shall prove the following:

Theorem 2.21 Every quasirational language is local.

Proof. First state a lemma:

Lemma 2.22 Every linear context free language is local.

Proof. Let L(G) be a linear context free language, over a finite alphabet Σ, which is generated by the linear grammar G of which production rules are: A_{i} → u_{i}B_{i}v_{i} for 1 ≤ i ≤ n, and C_{i} → w_{i} for 1 ≤ i ≤ k, where ∀i, u_{i}, v_{i}, w_{i} ∈ Σ^{⋆}. The variables A_{i}, B_{i}, C_{i} not necessarily are distinct, but are variables taken in a finite set given by G. Let us now associate to L(G) another linear language over the alphabet Γ = {c_{1}, ...c_{n}, d_{1}, ..., d_{n}, e_{1}, ..., e_{k}}. This new language is generated by the grammar G′ of which the production rules are: A_{i} → c_{i}B_{i}d_{i} for 1 ≤ i ≤ n, and C_{i} → e_{i} for 1 ≤ i ≤ k. This language L(G′) is the set of words in the form c_{i_{1}}...c_{i_{j}}e_{i}d_{i_{j}}...d_{i_{1}} , where 1 ≤ i ≤ k and i_{1}, ..., i_{j} are integers in [1, n], n ≥ 1. The set {c_{i_{1}}...c_{i_{j}}e_{i}/c_{i_{1}}...c_{i_{j}}e_{i}d_{i_{j}}...d_{i_{1}} ∈ L(G′)} is a rational language, generated by the grammar of which production rules are A_{i} → c_{i}B_{i} , 1 ≤ i ≤ n, and C_{i} → e_{i} , 1 ≤ i ≤ k. Therefore this language is local, defined by a local sentence φ. It is now easy to see that L(G′) is defined by a local sentence ψ, associating a word of L(ψ) with each word of L(φ):

Let S(ψ) = {P, a, s} ∪ S(φ) ∪ {P_{d_{i}}/1 ≤ i ≤ n} , where P is a unary predicate symbol, a is a constant symbol and s is a unary function symbol. Then ψ is the conjunction of the following sentences:

• (< is a linear order ),

• ((P_{c_{i}})_{1≤i≤n}, (P_{d_{i}})_{1≤i≤n}, (P_{e_{i}})_{1≤i≤k}) form a partition,

• ∀xy[P (x) ∧ ¬P (y) → x < y],

• ∀x_{1}...x_{j} ∈ P [φ_{0}(x_{1}, ..., x_{j})], where φ = ∀x_{1}...x_{j}φ_{0}(x_{1}, ..., x_{j}) with φ_{0} an open formula,

• ∀x_{1}...x_{m} ∈ P [f(x_{1}, ..., x_{m}) ∈ P], for each m-ary function f of S(φ),

• ∀x_{1}...x_{m}[⋁_{1≤i≤m} ¬P (x_{i}) → f(x_{1}, ..., x_{m}) = min(x_{1}, ..., x_{m})], for each m-ary function f of S(φ),

• P (c), for each constant c of S(φ),

• P (a) ∧ ∀x(P (x) → x ≤ a),

• s(a) = a,

• ∀x ∈ P [x ≠ a → ¬P (s(x))],

• ∀xy[P (x) ∧ P (y) ∧ x < y → s(y) < s(x)],

• ∀x[s(s(x)) = x],

• ∀x[P (x) ∧ P_{c_{i}}(x) ↔ P_{d_{i}}(s(x))], for each integer i ∈ [1, n]. ψ is equivalent to a universal formula and closure in its models takes at most n_{φ} + 2 steps: one takes closure under s then by the functions of S(φ), and then again by s. One can check that L(ψ) = L(G′) holds by construction. Let now the morphism h : Γ^{⋆} → Σ^{⋆} defined by h(c_{i}) = u_{i}, h(d_{i}) = v_{i}, for 1 ≤ i ≤ n, and h(e_{i}) = w_{i} for 1 ≤ i ≤ k. Then h(L(G′)) = L(G) hence L(G) is the image of the local language L(ψ) by the morphism h and, using the fact that LOC is closed under morphism (proved in next section), we can infer that L(G) is local. Then each linear context free language is local.

To end the proof of the Theorem, recall that the family of quasirational languages is the closure under substitution of the family of linear languages. LOC being closed under substitution, ( result proved in next section ), the preceding lemma implies that quasirational languages are local.

Remark that context free languages L such that each word in L is in the form xca^{|x|}, where a ∈ Σ, c ∉ Σ, Σ is a finite alphabet and x ∈ Σ^{⋆}, are important languages for the syntax of many programming languages. The set {x/xca^{|x|} ∈ L} is in that case rational hence local, and this permits to easily prove that L is local. In a similar manner, the context free languages of which each word is in the form xcx^{R}, important for programming, are local.

Example 2.23 Denote CF the class of context free languages, and OC the class of one counter languages. Then RAT ⊊ OC ⊊ CF [Ber79]. RAT ⊆ LOC. {a^{n}b^{n}/n ≥ 1} is in LOC and in OC − RAT. The Dyck language with two sorts of parentheses is in CF −OC and in LOC.

Then many context free languages are in LOC, but it is an open question to know whether every context free language is local.

Example 2.24 The cone of Greibach languages is the closure under substitution of the family LIN ∪ OC, where LIN is the family of linear languages and OC is the family of one counter languages. We have seen that there are local languages which are generators of the family of context free languages, like the Dyck languages D_{n}^{′⋆}, for n ≥ 2. There are local languages in NGE − GRE, the family of context free languages which are neither generator nor Greibach languages. An example is given by the following language:

Let Ẑ_{n} = {z_{1}, ..., z_{n}, z̄_{1}, ..., z̄_{n}} = Z_{n} ∪ Z̄_{n} Where Z_{n} = {z_{1}, ..., z_{n}} and Z̄_{n} = {z̄_{1}, ..., z̄_{n}}. Let us define the substitution s over Ẑ_{n} by: s(z_{i}) = z_{i} and s(z̄_{i}) = z̄_{i}Z̄_{n}^{⋆} for 1 ≤ i ≤ n.

The image δ_{n} of the Dyck language over the alphabet Ẑ_{n} (with n sorts of parentheses) by the substitution s is then context free and, for n ≥ 2, δ_{n} ∈ NGE − GRE holds. This language is local, because the Dyck languages and the languages z̄_{i}Z̄_{n}^{⋆} are local, and LOC is closed under substitution by the Theorem 3.3 of next section.

The question is open to know whether OC ⊂ LOC, which would imply that GRE ⊂ LOC.

Example 2.25 The Hardest Context Free Language or the non deterministic version of the Dyck language.

This language is defined over the alphabet Σ_{n} = Ẑ_{n} ∪ {[,], +}; A block is a word in the form [u_{1} + u_{2} + ... + u_{p}]; So the set of blocks is the rational language [(Ẑ_{n} ∪ {+})^{⋆}]. A factor u in a block ( maximal factor over Ẑ_{n} ) is called a choice in this block. Then f ∈ H_{n} iff f = f_{1}f_{2}...f_{r} where: each f_{i} is a block and there exists a choice u_{i} in every block f_{i} such that u_{1}u_{2}...u_{r} ∈ D_{n}^{′⋆}.

All these languages H_{n} are context free and, for n ≥ 2, H_{n} is a generator of the rational cone CF. These languages have been studied because they generate the family CF without using direct morphisms. Indeed Shamir-Greibach Theorem states that: A language L is context free iff there exists a morphism h such that: L − {λ} = h^{−1}(H_{2}). Let us show that H_{n} is local. Consider first the sentence ψ_{n} which is the conjunction of:

• (< is a linear order),

• ((P_{a})_{a∈Σ_{n}} form a partition),

• ∀xy(P_{[}(x) → x ≤ y),

• ∀xy(P_{]}(x) → y ≤ x),

• ∀x(P (x) → ⋁_{a∈Ẑ_{n}} P_{a}(x)), • ∀x(P (x) ↔ b_{1} < x < b_{2}),

• P_{[}(b_{1}) ∨ P_{+}(b_{1}),

• P_{[}(a_{1}) ∧ P_{]}(a_{2}),

• P_{]}(b_{2}) ∨ P_{+}(b_{2}),

The signature of ψ_{n} is S(ψ_{n}) = {(P_{a})_{a∈Σ_{n}}, <, P, b_{1}, b_{2}, a_{1}, a_{2}} , where P is a unary predicate symbol and b_{1}, b_{2}, a_{1}, a_{2} are constant symbols. A model M of ψ_{n} provides a block M|Λ_{Σ_{n}} and P^{M}|Λ_{Σ_{n}} gives a choice in this block.

Let then the signature S(φ_{n}) = {(P_{a})_{a∈Σ_{n}}, <, P, I, s, b_{1}, b_{2}, a_{1}, a_{2}}, where P is a unary predicate symbol and I, s, b_{1}, b_{2}, a_{1}, a_{2} are unary function symbols. Let φ = ∀xyzφ_{0}(xyz) a local sentence defining D_{n}^{′⋆} with φ_{0} an open formula, S(φ) = {(P_{a})_{a∈Ẑ_{n}}, < s}, s a unary function. (See Example 2.11 ) Now define :

φ_{n} = ψ_{n}^{⋆} ∧ [∀xyz ∈ P φ_{0}(xyz)] ∧ ∀x(¬P (x) → s(x) = x),

where ψ_{n}^{⋆} is the conjunction of:

• (< is a linear order),

• ((P_{a})_{a∈Σ_{n}} form a partition),

• ∀xy[(I(y) ≤ y) ∧ (y ≤ x → I(y) ≤ I(x)) ∧ (I(y) ≤ x ≤ y → I(x) = I(y))],

• ∀xy[I(x) = I(y) → e(x) = e(y)], for e ∈ {b_{1}, b_{2}, a_{1}, a_{2}},

• ∀xψ_{n}^{x}, where ψ_{n}^{x} is the local sentence ψ_{n} in which the constants b_{1}, b_{2}, a_{1}, a_{2} are replaced by the terms b_{1}(x), b_{2}(x), a_{1}(x), a_{2}(x) and each quantifier is relativized to the set {y/I(y) = I(x)}.

φ_{n} is equivalent to a universal formula and closure in each of its models takes at most two steps: (take first closure under s, then by b_{1}, b_{2}, a_{1}, a_{2} and I. Hence φ_{n} is local and, by construction L^{Σ_{n}}(φ_{n}) = H_{n} holds. We’ll see in next section that LOC is not closed under inverse morphism; Then we cannot use this result in order to prove, by Shamir-Greibach Theorem, that CF ⊂ LOC.

Example 2.26 Languages of bigger complexity than that of context free languages.

Let NEST be the family of languages which are recognized by a non erasing stack automata, ST be the family of languages which are recognized by a stack automata, and CS be the family of context sensitive languages which are generated by a context sensitive grammar. It holds that: CF ⊊ NEST ⊊ ST ⊊ CS. [Ogd69]. There are local languages in each family of this hierarchy.

{a^{n^{2}}b^{n}/n ≥ 1} is in NEST − CF. {b^{n}a^{n^{2}}/n ≥ 1} is in ST − NEST. {a^{n^{2}}b^{n^{2}}c^{n^{2}}/n ≥ 1} is in CS − ST. [Ogd69].

Proof. We shall prove that the language {b^{n}a^{n^{2}}/n ≥ 1} is local; some analogous methods proving that {a^{n^{2}}b^{n}/n ≥ 1} and {a^{n^{2}}b^{n^{2}}c^{n^{2}}/n ≥ 1} are local. Let S(ψ) = {P_{a}, P_{b}, <, d, f, p_{1}, p_{2}} where f is a 2-ary function symbol, p_{1} and p_{2} are unary function symbols and d is a constant symbol. The sentence ψ is the conjunction of:

• (< is a linear order ),

• (P_{a}, P_{b} form a partition ),

• ∀xy[(P_{b}(x) ∧ P_{a}(y)) → x < y],

• ∀xyzt[(P_{b}(x) ∧ P_{b}(y) ∧ P_{b}(z) ∧ P_{b}(t) ∧ (x ≠ z ∨ y ≠ t)) → (f(xy) ≠ f(zt) ∧ P_{a}(f(xy)))],

• ∀xy[(P_{a}(x) ∨ P_{a}(y)) → f(xy) = x],

• ∀x[P_{a}(x) → P_{b}(p_{1}(x)) ∧ P_{b}(p_{2}(x)) ∧ f(p_{1}(x)p_{2}(x)) = x],

• ∀x[P_{b}(x) → p_{1}(x) = p_{2}(x) = x],

• ∀x[x ≤ d].

ψ is equivalent to a universal formula and closure in each of its models takes at most three steps: ( one first takes first closure under d, then under p_{1} and p_{2}, and then under f ). Hence ψ is local and L(ψ) = {b^{n}a^{n^{2}}/n ≥ 1} holds by construction.

Example 2.27 In comparison with Kasai Hierarchy We investigate here another hierarchy of families of languages which are located betweeen CF and CS, introduced by Takumi Kasai, [Kas70].

Many programming languages cannot be represented by context free languages, hence he studied grammars which are more powerful than the context free ones: the state grammars. Making restrictions over these grammars, Kasai obtained an infinity of AF L ( Abstract Family of Languages ), families of state languages which are closed under rational operations ∪, ., +, and under rational transductions.

Definition 2.28 ([Kas70]) A state grammar is a sextuple G = (K, V, Σ, P, p_{0}, σ) where:

(1) K is a non empty finite set (of states).

(2) V is a finite set of symbols and Σ ⊆ V.

(3) σ is an element of V − Σ.

(4) p_{0} is an element of K.

(5) P is a finite subset of K × (V − Σ) × K × V^{+} where V^{+} = ∪_{i=1}^{∞}V^{i}.

An element (p, ξ, q, u) of P is called a production and is usually written (p, ξ) → (q, u). V − Σ is the set of variables and a variable ξ is said to be applicable under a state p if (p, ξ) → (q, u) is in P for some q ∈ K and u in V^{+}. Let G = (K, V, Σ, P, p_{0}, σ) be a state grammar, and let ⇒ be a relation on K × V^{+} defined as follows: Let p ∈ K and w = xξy ∈ V^{+}. If this ξ is the leftmost occurrence of applicable variables in w under p and (p, ξ) → (q, u) is in P, then we write (p, xξy) ⇒ (q, xuy). If this ξ is the j-th variable in w, then we sometimes write ⇒^{j} instead of ⇒. For α and β in K × V^{+} , write α ⇒^{⋆} β if either α = β or there exist α_{0}, ..., α_{r} such that α_{0} = α, α_{r} = β, and α_{i} ⇒ α_{i+1} for each i. The sequence α_{0}, ..., α_{r} is called a derivation (of length r) and is denoted α_{0} ⇒ ... ⇒ α_{r}. The subset of Σ^{+}, L(G) = {w ∈ Σ^{+}/(p_{0}, σ) ⇒^{⋆} (q, w) for some q ∈ K} is called a state language, generated by the grammar G.

Definition 2.29 ([Kas70]) Let G = (K, V, Σ, P, p_{0}, σ) be a state grammar and let n be a positive integer. A n-limited derivation is a derivation:

α_{0} ⇒^{j(1)} α_{1} ⇒^{j(2)} ... ⇒^{j(r)} α_{r} such that j(i) ≤ n for each i.

In this case we sometimes write α_{0} ⇒^{n^{⋆}} α_{r} instead of α_{0} ⇒^{⋆} α_{r}, in order to indicate that it is realized by a n-limited derivation.

Then L(G, n) = {w ∈ Σ^{+}/(p_{0}, σ) ⇒^{n^{⋆}} (q, w) for some q ∈ K}

G is said to be a state grammar of degree n iff L(G) = L(G, n).

A state language is said to be of degree n iff it is generated by a state grammar of degree n. Otherwise this state language is of infinite degree.

L_{1} is the family of context free languages which do not contain the empty word. L_{n} is the family of state languages of degree n. L_{∞} = ∪_{n≥1}L_{n} is the family of state languages of finite degree. L_{ω} is the family of state languages which is equal to the family of context sensitive languages. T. Kasai proved that all the following inclusions are strict: L_{1} ⊊ L_{2} ⊊ ... ⊊ L_{n} ⊊ L_{n+1} ⊊ ... ⊊ L_{∞} ⊊ L_{ω}. Let us cite a property of finite degree state languages: If L ∈ L_{n} for some n ≥ 1, then {|w|/w ∈ L} is an ultimately periodic set of integers. In comparison with local languages, it holds that:

Proposition 2.30 There exist local languages at each level of this hierarchy; more precisely, ∀n ≥ 1, there exists a local language L(φ_{n}) in L_{n+1} − L_{n} and there exists a local language in L_{ω} − L_{∞} i.e. a (context sensitive) state language of infinite degree.

Proof. The language {a_{1}^{k}a_{2}^{k}...a_{4n+2}^{k}/k ≥ 1} over the alphabet Σ_{n} = {a_{1}, ..., a_{4n+2}} is in L_{n+1} − L_{n} , for n ≥ 1. And the language {b^{n}a^{n^{2}}/n ≥ 1} over the alphabet Σ = {a, b} is in L_{ω} but not in L_{∞} ,[Kas70]. Now it is easy to check that these languages are local.

Example 2.31 There exist NP-complete languages in LOC.

This result is stated in [Res88]. For example the NP-complete language CLIQUE is a local language: For a finite graph G and an integer n ≥ 1, (G, n) ∈ CLIQUE iff G contains a clique of cardinal n (i.e. a set C of vertices of cardinal n such that every edge between two vertices of C is in G ).

A graph G = (V, E) is defined by the set V of its vertices and the set E ⊆ V × V of its edges, with ∀(u, v) ∈ V^{2}[(u, v) ∈ E → (v, u) ∈ E] and [(u, u) ∉ E]. We code a word in CLIQUE in the following manner: card(V) zeros followed by an a followed by (cardV)^{2} letters in {0, 1} coding E followed by a b followed by n times the letter 1. If V = {v_{1}, ..., v_{p}}, we obtain the following word:

0^{p}a[v_{1}v_{1}][v_{1}v_{2}]...[v_{1}v_{p}][v_{2}v_{1}][v_{2}v_{2}]...[v_{2}v_{p}]...[v_{p}v_{1}][v_{p}v_{2}]...[v_{p}v_{p}]b1^{n} where [v_{i}v_{j}] = 0 if (v_{i}, v_{j}) ∈ E and [v_{i}v_{j}] = 1 if (v_{i}, v_{j}) ∉ E. Let then φ the following sentence, conjunction of:

• (< is a linear order),

• (P_{0}, P_{1}, P_{a}, P_{b}) form a partition,

• (P, Q, R, P_{a}, P_{b}) form a partition,

• ∀xyz[P (x) ∧ Q(y) ∧ R(z) → x < A < y < B < z],

• P_{a}(A) ∧ ∀x(P_{a}(x) ↔ x = A),

• P_{b}(B) ∧ ∀x(P_{b}(x) ↔ x = B),

• ∀xyz ∈ P [y < z → f(xy) < f(xz)],

• ∀xyzt ∈ P [y < z → f(yt) < f(zx)],

• ∀xy ∈ P [Q(f(xy))],

• p_{1}(A) = p_{2}(A) = A,

• p_{1}(B) = p_{2}(B) = B,

• ∀xy[¬P (x) ∨ ¬P (y) → f(xy) = min(xy)],

• ∀x[P (x) ∨ R(x) → p_{1}(x) = p_{2}(x) = x],

• ∀x[Q(x) → f(p_{1}(x)p_{2}(x)) = x],

• ∀x[Q(x) → P (p_{1}(x)) ∧ P (p_{2}(x))],

• ∀x[P (x) → P_{0}(x)],

• ∀x ∈ Q[P_{0}(x) ∨ P_{1}(x)],

• ∀x ∈ R[P_{1}(x)],

• ∀x[¬R(x) → i(x) = x],

• ∀x[R(x) → P (i(x))],

• ∀xy[R(x) ∧ R(y) ∧ x ≠ y → i(x) ≠ i(y)],

• ∀xy[R(x) ∧ R(y) ∧ x ≠ y → P_{0}(f(i(x)i(y)))], • ∀xy[P (x) ∧ P (y) → (P_{0}(f(xy)) ↔ P_{0}(f(yx)))],

• ∀x ∈ P [P_{1}(f(xx))].

The signature of φ is S(φ) = {<, P_{0}, P_{1}, P_{a}, P_{b}, P, Q, R, f, A, B, i, p_{1}, p_{2}} , where P, Q, R are unary predicate symbols, A, B are constant symbols, f is a binary function symbol and i, p_{1}, p_{2} are unary function symbols. φ is equivalent to a universal formula and closure in each of its models takes at most two steps: one takes the closure under A, B, p_{1}, p_{2}, i and then under f. Hence φ is a local sentence . We then check that L(φ)^{{a,b,0,1}} = CLIQUE.

Another example of NP-complete language: The language which is connected with the problem V C: ” Vertex Cover ”. Let G = (V, E) be a graph and let k be a non negative integer ≤ card(V). (G, k) ∈ V C ↔ ∃V′ ⊆ V such that card(V′) ≤ k and V′ covers the graph, i.e. for each edge (u, v) ∈ E, {u, v} ∩ V′ is not empty.

We code a word of V C in the same manner as for CLIQUE. Let then S(ψ) = {<, P_{0}, P_{1}, P_{a}, P_{b}, P, Q, R, V′, f, A, B, s, p_{1}, p_{2}}, where V′, P, Q, R are unary predicate symbols, A, B are constant symbols, f is a binary function symbol and s, p_{1}, p_{2} are unary function symbols.

Let then ψ the following sentence, conjunction of:

• (< is a linear order),

• (P_{0}, P_{1}, P_{a}, P_{b}) form a partition,

• (P, Q, R, P_{a}, P_{b}) form a partition,

• ∀x[P_{a}(x) ↔ x = A],

• ∀x[P_{b}(x) ↔ x = B],

• ∀xyz[P (x) ∧ Q(y) ∧ R(z) → x < A < y < B < z],

• ∀xyz ∈ P [y < z → f(xy) < f(xz)],

• ∀xyzt ∈ P [y < z → f(yt) < f(zx)],

• ∀xy ∈ P [Q(f(xy))],

• ∀x[Q(x) → f(p_{1}(x)p_{2}(x)) = x], • ∀x[Q(x) → P (p_{1}(x)) ∧ P (p_{2}(x))],

• ∀x[¬Q(x) → p_{1}(x) = p_{2}(x) = x],

• ∀x[P (x) → P_{0}(x)],

• ∀x[Q(x) → P_{0}(x) ∨ P_{1}(x)],

• ∀x[R(x) → P_{1}(x)],

• ∀xy[P (x) ∧ P (y) → (P_{0}(f(xy)) ↔ P_{0}(f(yx)))],

• ∀x ∈ P [P_{1}(f(xx))].

• ∀x[V′(x) → P (x)],

• ∀x[V′(x) → R(s(x)) ∧ s(s(x)) = x],

• ∀x[R(x) → P (s(x))],

• ∀xy[R(x) ∧ R(y) ∧ x ≠ y → s(x) ≠ s(y)],

• ∀x[¬R(x) ∧ ¬V′(x) → s(x) = x],

• ∀xy[P (x) ∧ P (y) ∧ P_{0}(f(xy)) → V′(x) ∨ V′(y)]. ψ is equivalent to a universal formula and closure in each of its models takes at most three steps: one takes the closure under A, B, p_{1}, p_{2} and then under s, then under f. Hence ψ is a local sentence . By construction we can check that in a model M of ψ, V^{′M} represents a subset of P^{M} of cardinal ≤ k ≤ card(P^{M}), k = card(R^{M}), which covers the graph. Then it holds that L(ψ)^{{a,b,0,1}} = V C. Example 2.32 There exists a set of integers in P which is not the spectrum of any local language, as {2^{n}/n ≥ 1}. (Result of J-P. Ressayre) Recall that the spectrum of a first order sentence φ is the subset of ℕ defined by: Sp(φ) = {n ∈ ℕ / ∃M ⊧ φ such that card(M) = n}. Example 2.33 By methods which are similar to those used in example 2.26, we easily show that p(ℕ) is a spectrum of a local language for every polynomial p with coefficients in ℕ. And more generally if A is the spectrum of a local language, then p(A) is the spectrum of a local language, for every polynomial p with coefficients in ℕ.

Let us show that L = {a^{n}/n is a non prime integer ≥ 0} is a local language.

Let S(φ) = {<, P_{a}, P, b, c, f, p_{1}, p_{2}} , where P is a unary predicate symbol, b, c are constant symbols, f is a binary function symbol and p_{1}, p_{2} are unary function symbols.

Let then φ the following sentence, conjunction of:

• (< is a linear order),

• ∀xP_{a}(x),

• ∀xy[P (x) ∧ ¬P (y) → x < y],

• P (b) ∧ P (c) ∧ c < b,

• ∀xy[P (x) ∧ P (y) ∧ y < b → ¬P (f(xy))],

• ∀xyzt[P (x) ∧ P (y) ∧ P (z) ∧ P (t) ∧ y < b ∧ t < b ∧ (x ≠ z ∨ y ≠ t) → f(xy) ≠ f(zt)],

• ∀xy[¬P (x) ∨ b ≤ y → f(xy) = x],

• ∀x[P (x) → p_{1}(x) = p_{2}(x) = x],

• ∀x[¬P (x) → f(p_{1}(x)p_{2}(x)) = x ∧ p_{2}(x) < b ∧ P (p_{1}(x))].

We then check that this sentence φ is local because it is equivalent to a universal formula and closure in each of its models takes at most two steps: one takes the closure under p_{1}, p_{2} and then under f. If M ⊧ φ and card(P^{M}) = m, then card(M) = m + nm with 1 ≤ n < m. Hence card(M) = m(n + 1) with 2 ≤ n + 1 ≤ m. Conversely we check that for every non prime integer in the form m(n + 1) with 2 ≤ n + 1 ≤ m, there exists a model of φ of cardinal m(n + 1). Therefore the spectrum of φ is {n ≥ 4 /n is a non prime integer }. ¿From what we easily deduce that the language L = {a^{n} / n is a non prime integer ≥ 0} = {λ, a} ∪ L(φ) is a local language. So the spectrum {n ∈ ℕ /n is non prime } is the spectrum of a local language. Its complement, {n ∈ ℕ /n is prime } is not the spectrum of a local language, because the spectrum of an infinite local language always contains a set in the form p(ℕ), where p is a polynomial with positive integers as coefficients, [Fin99]. Indeed a result of number theory states that a polynomial with coefficients in ℕ cannot take only prime number values over ℕ.

Remark that the question to know whether the complement of a spectrum is a spectrum is connected with the algorithmic complexity problem NP = co − NP. This problem has a negative answer when it is restricted to spectra of local sentences. See [Fag93] for more results and references about spectra of first order sentences.

3 Closure properties

Recall the following:

Theorem 3.1 ([Res88]) Loc is closed under union, catenation product, and operation ⋆.

Proof. the proof of closure under union and catenation product is easy. To prove closure under star operation, J-P. Ressayre defined a new operation over local sentences: For each local sentence φ, φ^{⋆} is a local sentence in the signature S(φ^{⋆}) which is the signature of φ to which is added a unary function symbol I and in which every constant symbol e is replaced by a unary function symbol e(x).

For a local sentence φ, φ^{⋆} is the sentence defined by the conjunction of:

• ( < is a linear order ),

• ∀yz[I(y) ≤ y and (y ≤ z → I(y) ≤ I(z)) and (I(y) ≤ z ≤ y → I(z) = I(y))],

• ∀xy[I(x) = I(y) → e(x) = e(y)], for each constant e of the signature S(φ) of φ,

• ∀x_{1}...x_{n}[(⋁_{i,j≤n} I(x_{i}) ≠ I(x_{j})) → f(x_{1}...x_{n}) = min(x_{1}...x_{n})] , for each n-ary function f of S(φ),

• ∀x_{1}...x_{n}[(⋀_{i,j≤n} I(x_{i}) = I(x_{j})) → I(f(x_{1}...x_{n})) = I(x_{1})], for each n-ary function f of S(φ),

• ∀xφ^{x}, where φ^{x} is the local sentence φ in which every constant e is replaced by the term e(x) and each quantifier is relativized to the set {y \ I(y) = I(x)}.

Remark 3.2 The models of φ^{⋆} are essentially direct sums of models of φ, and L^{Σ}(φ^{⋆}) = (L^{Σ}(φ))^{⋆}.

We shall prove the following:

Theorem 3.3 The class LOC of local languages is closed under substitution, morphism, inverse alphabetic morphism. LOC is not closed under intersection, intersection with a rational language, complementation, inverse morphism. LOC is neither closed under quotient, nor under quotient by a context free language, but LOC is closed under quotient by a finite language.

Proof.

a) Closure under substitution. Let then Σ = {a_{1}, ..., a_{n}} be a finite alphabet and let f be a substitution: Σ → P (Γ^{⋆}), a_{i} → L_{i} where ∀i ∈ [1; n], L_{i} is a local language defined by the sentence φ_{i}, over the alphabet Γ. More assume that the empty word is not in L_{i}. We may also assume that the signatures of the sentences φ_{i} verify S(φ_{i}) ∩ S(φ_{j}) = {<, (P_{a})_{a∈Γ}} for i ≠ j. Let now L ⊆ Σ^{⋆} be a local language defined by a local sentence φ. We’ll denote by Q_{a_{i}} the unary predicate of S(φ) which indicates the places of the letters a_{i} in a word of L, so as that if a_{i} ∈ Γ∩Σ for an indice i, there will be two distinct predicates Q_{a_{i}} and P_{a_{i}}. We’ ll also assume, possibly differently naming function, constant, and other predicate symbols of S(φ), that ∀i ∈ [1, ..., n], S(φ_{i})∩S(φ) = {<}. Then we now construct a local sentence ψ which defines the language f(L): ψ is the conjunction of the following sentences, which meaning is explained below:

• “ < is a linear order ”,

• ∀xy[(I(y) ≤ y) ∧ (y ≤ x → I(y) ≤ I(x)) ∧ (I(y) ≤ x ≤ y → I(x) = I(y))],

• ∀x[I(x) = x ↔ P (x)],

• P (c), for each constant c of S(φ),

• ∀x_{1}...x_{k}[R(x_{1}...x_{k}) → P (x_{1})∧....∧P (x_{k})], for each predicate R(x_{1}...x_{k}) of S(φ),

• ∀x_{1}...x_{j}[(P (x_{1}) ∧ ... ∧ P (x_{j})) → P (f(x_{1}...x_{j}))], for each j-ary function symbol f of S(φ),

• ∀x_{1}...x_{j}[(⋁_{1≤i≤j} ¬P (x_{i})) → f(x_{1}...x_{j}) = min(x_{1}...x_{j})], for each j-ary function symbol f of S(φ), • ∀x_{1}...x_{m}[(P (x_{1})∧...∧P (x_{m})) → φ_{0}(x_{1}...x_{m})], where φ = ∀x_{1}...x_{m}φ_{0}(x_{1}...x_{m})

with φ_{0} an open formula,

• ∀x_{1}...x_{j}[⋁_{i,k≤j}(I(x_{i}) ≠ I(x_{k})) → f(x_{1}...x_{j}) = min(x_{1}...x_{j})], for every function f of S(φ_{l}) for an integer l ≤ n,

• ∀xy_{1}...y_{j}[(⋀_{1≤l≤j} I(y_{l}) = I(x)) → I(f(y_{1}...y_{j})) = I(x)], for each j-ary function symbol f of S(φ_{i}) for an integer i ≤ n,

Finally, for each i ≤ n:

• ∀xy_{1}...y_{p}[(⋀_{1≤l≤p} I(y_{l}) = I(x) ∧ Q_{a_{i}}(I(x))) → φ_{i}^{0}(y_{1}...y_{p}) ∧ {(e_{j}(y_{1}) = I(x)∧f_{j}(y_{1}...y_{p}) = y_{1}∧¬R_{j}(y_{1}...y_{p})∧⋀_{e_{i}∈S(φ_{i})} e_{i}(y_{1}) = e_{i}(x); where n ≥ j ≠ i, and e_{j}, f_{j}, R_{j} run over the constants, functions, and predicates of S(φ_{j})}],

Above , 1) to each constant e_{l} of S(φ_{l}) is associated a new unary function e_{l}(y) and 2) whenever φ_{i} = ∀y_{1}...y_{p}ψ_{i}(y_{1}...y_{p}) with ψ_{i} an open formula, φ_{i}^{0} is ψ_{i} in which every constant e_{i} has been replaced by the function e_{i}(y).

Construction of ψ : Using the function I which marks the first letters of the subwords, we divide a word into subwords. In every model M of ψ, the set of the ”first letters of subwords” , P^{M}, grows richer in a model of φ ( therefore will constitute a word of L ). Then we ”substitute” : for each letter a_{i} in P^{M}, we substitute a word of L_{i}, using for that the formula φ_{i}. Then if closure takes at most m(φ) (respectively m(φ_{i}) ) steps in every model of φ (respectively of φ_{i}), then closure takes at most [m(φ) + 2sup_{i}(m(φ_{i}))] steps in each model of ψ. Therefore ψ is a local sentence and by construction ψ defines the language f(L).

When the languages L_{i} may contain the empty word λ, consider a substitution f: Σ → P (Γ^{⋆}), a_{i} → L_{i} as above and let c ∉ Σ ∪ Γ. Define f^{c} by: f^{c} : Σ → P ((Γ∪{c})^{⋆}), a_{i} → L_{i} if λ ∉ L_{i} and a_{i} → L_{i}−{λ}∪{c} otherwise. By the preceding proof, the language f^{c}(L) is local. The local sentence defining f^{c}(L) contains the unary predicate P_{c} which marks the places of the letters c in every word. The ”projection” of the models of this sentence on the predicate ¬P_{c} gives the local language f(L). Indeed according to a result of J-P. Ressayre: if L(φ) is a local language over an alphabet Σ and P is a unary predicate of S(φ), then {σ ∈ Σ^{⋆}/∃M ⊧ φ and M|P^{M}|Λ_{Σ} = σ} is a local language.

b) Closure under morphism. This is a particular case of the preceding one.

b) Closure under inverse alphabetic morphism. Let f be an alphabetic morphism: Σ → Γ ∪ {λ}, where Σ and Γ are finite alphabets. Let Σ′ = {a ∈ Σ/f(a) = λ}. Let L(φ) ⊆ Γ^{⋆} be a local language. We first replace in φ the letter predicates (P_{a})_{a∈Γ} by (Q_{a})_{a∈Γ}. Then ψ is the conjunction of the following sentences:

• (< is a linear order),

• ((P_{a})_{a∈Σ} form a partition),

• ∀x_{1}...x_{n} ∈ P [φ_{0}(x_{1}...x_{n}) ∧ ⋀_{a∈Γ}(Q_{a}(x_{1}) ↔ ⋁_{c∈f^{−1}(a)} P_{c}(x_{1}))], where φ = ∀x_{1}...x_{n}φ_{0}(x_{1}...x_{n}) with φ_{0} an open formula,

• ((P_{a})_{a∈Σ′} form a partition of ¬P ),

• ∀x_{1}...x_{j}[(⋁_{1≤i≤j} ¬P (x_{i})) → f(x_{1}...x_{j}) = x_{1}], for each j-ary function symbol f of S(φ),

The sentence ψ is equivalent to a universal sentence, and it is local because in its models closure takes at most n_{ψ} = n_{φ} steps. And L(ψ) = f^{−1}(L(φ)) holds by construction.

d) Closure under inverse morphism, intersection, complementation. The proof uses the notion of rational cone of which we now recall the definition:

Definition 3.4 A rational cone is a class of languages which is closed under morphism, inverse morphism, and intersection with a rational language. (Or, equivalently to these three properties, closed under rational transduction).

Then recall the following:

Proposition 3.5 ([HU69], exercise) A class of languages closed under morphism, inverse morphism, union and concatenation product, is a rational cone.

Now we can state the next Proposition:

Proposition 3.6 The class LOC is not a rational cone.

Proof. It uses the following result:

Proposition 3.7 ([FZV80]) The Antidyck language Q_{2}^{′⋆} is a generator of the rational cone of the recursively enumerable languages.

But we have seen that the Antidyck language Q_{2}^{′⋆} is local, but there exist many recursively enumerable languages which are not local, for example {a^{2^{n}}/n ≥ 1}, or the language ^{c}L of the above example 2.19.

Then from Propositions 3.5 and 3.6, we infer that LOC is not closed under inverse morphism. Now recall the following:

Theorem 3.8 (Nivat [Ber79]) A class of languages which is closed under alphabetic morphism, inverse alphabetic morphism, and intersection with a rational language, is a rational cone.

LOC is a class which is closed under alphabetic morphism, inverse alphabetic morphism but which is not a rational cone, therefore it is not closed under intersection with a rational language, and it is also neither closed under intersection, nor under complementation.

d) Closure under quotient. Recall that the left quotient of L_{1} by L_{2} is L_{2}\L_{1} = {w/yw ∈ L_{1} for an y ∈ L_{2}}. And the right quotient of L_{1} by L_{2} is L_{1}/L_{2} = {w/wy ∈ L_{1} for an y ∈ L_{2}}.

Let then R = a{b^{i}a^{i}/i > 0}^{⋆} and L = {a^{i}b^{2i}/i > 0}^{⋆}. R and L are local and context free languages and it holds that: R\L ∩ b^{+} = {b^{2^{n}}/n > 0} then R\L is not local. Because if R\L = L(φ) was local, the formula φ ∧ ∀xP_{b}(x) would be local and would define R\L ∩ b^{+}, but {b^{2^{n}}/n > 0} cannot be defined by a local sentence . The proof is similar for the right quotient.

e) Closure under quotient by a finite language. whenever the language is finite and contains a single word a of length 1, the language {a}\L(φ) is local, by projection of the models of φ on a predicate. Furthermore we then use the formulas: L_{1}L_{2}\L = L_{2}\(L_{1}\L) and (L_{1} ∪ L_{2})\L = (L_{1}\L) ∪ (L_{2}\L).

4 UNDECIDABLE PROBLEMS

Return to Chapter 4 of [Gin66] about undecidable problems for context free languages . Showing that languages which appear there are local, we can prove the following undecidability results about local languages. Theorem 4.1 Let Σ be an alphabet containing at least two letters. It is undecidable to determine for arbitrary local languages L(φ) and L(ψ) over Σ whether :

1. L(φ) ∩ L(ψ) is empty.

2. L(φ) ∩ L(ψ) is infinite.

3. L(φ) ∩ L(ψ) is rational.

4. L(φ) ∩ L(ψ) is context free.

5. L(φ) ∩ L(ψ) is local: more precisely, there does not exist any algorithm which answers , either L(φ)∩L(ψ) is not local, or L(φ)∩L(ψ) is local, giving θ local and n_{θ} such that L(φ) ∩ L(ψ) = L(θ). (closure taking at most n_{θ} steps in the models of θ).

6. L(φ) ⊆ L(ψ).

7. L(φ) = L(ψ).

8. L(φ) = Σ^{⋆}.

9. L(φ) is rational.

10. ^{c}L(φ), is empty . ( ^{c}L(φ) = Σ^{⋆} − L(φ) being the complement of L(φ) in Σ^{⋆} ).

11. ^{c}L(φ) is rational.

12. ^{c}L(φ) is context free.

13. ^{c}L(φ) is infinite.

14. ^{c}L(φ) is local . ( with the same precision as for 5) ).

15. L(φ) is a linear context free language . ( Σ has here at least three letters ).

16. L(φ) contains an infinite rational language.

For arbitrary local sentence φ and rational language R:

17. L(φ) ⊇ R.

18. L(φ) = R.

Proof. We return to the Post correspondance Theorem :

Theorem 4.2 Let Σ be an alphabet with at least two elements . Then it is undecidable to determine for arbitrary n-tuples (w_{1}, .., w_{n}) and (y_{1}, ....y_{n}) of nonempty words in Σ^{⋆} whether there exists a nonempty sequence of indices i_{1}, ..., i_{k} such that w_{i_{1}}....w_{i_{k}} = y_{i_{1}}...y_{i_{k}}.

Let Σ = {a, b, c}. For all n-tuples x = (x_{1}, ...x_{n}) and y = (y_{1}, ..y_{n}) of nonempty words of {a, b}^{⋆} , let: L(x) = {ba^{i_{k}}...ba^{i_{1}}cx_{i_{1}}...x_{i_{k}}/k ≥ 1, 1 ≤ i_{j} ≤ n} and L(x, y) = L(x)cL(y)^{R}, where for a language L, L^{R} = {u^{R}/u ∈ L} and u^{R} = u_{n}...u_{2}u_{1} whenever u = u_{1}u_{2}...u_{n}, u_{i} being a letter ∀i.

Let Γ = {c, a_{1}, ...a_{n}, c_{1}, ...c_{n}} a new alphabet. And let h be the morphism Γ^{⋆} → Σ^{⋆} defined by : c → c, a_{j} → x_{j}, c_{j} → ba^{j}. And let: L = {c_{i_{k}}...c_{i_{1}}ca_{i_{1}}...a_{i_{k}}/k ≥ 1, 1 ≤ i_{j} ≤ n} . L is a local language defined by the following sentence ψ of signature S(ψ) = {<, (P_{a_{i}})_{1≤i≤n}, P_{c}, (P_{c_{i}})_{1≤i≤n}, d, s}, where P_{a_{i}}, P_{c}, P_{c_{i}} are unary predicate symbols, d is a constant symbol and s is a unary function symbol.

ψ is the conjunction of :

• (< is a linear order)

• (P_{a_{i}}, P_{c}, P_{c_{i}}, 1 ≤ i ≤ n) form a partition,

• ∀x(P (x) ↔ ⋁_{1≤i≤n} P_{c_{i}}(x)),

• ∀x(Q(x) ↔ ⋁_{1≤i≤n} P_{a_{i}}(x)),

• ∀xyz(P (x) ∧ Q(y) ∧ P_{c}(z) → x < z < y),

• ∀xy(P_{c}(x) ∧ P_{c}(y) → x = y),

• ∀x(s(s(x)) = x),

• ∀x(P_{a_{i}}(x) ↔ P_{c_{i}}(s(x))), 1 ≤ i ≤ n, • ∀x(P_{c}(x) → s(x) = x),

• P_{c}(d),

• ∀xy(P (x) ∧ P (y) ∧ x < y → s(y) < s(x)). Then the language L is local, and L(x) = h(L) is also local because the image of a local language by a morphism is local. L(x, y) is a local language: We easily see that A local implies A^{R} local from what we deduce that L(y)^{R} is local and by concatenation product that L(x).c.L(y)^{R} is local Define now L_{s} = {w_{1}cw_{2}cw_{2}^{R}cw_{1}^{R}/w_{1} and w_{2} ∈ {a, b}^{⋆}} , Σ = {a, b, c}. Let us prove that L_{s} is a local language: The language {a, b}^{⋆}c{a, b}^{⋆} is rational then local and it is defined by the sentence τ = [∀x(P_{c}(x) → x = d)] ∧ [P_{c}(d)] ∧ [P_{a}, P_{b}, P_{c} form a partition ] ∧ [< is a linear order ], where d is a constant symbol. The language L_{s} is defined by ψ_{s} which is the conjunction of :

• (< is a linear order),

• (P_{a}, P_{b}, P_{c}, form a partition),

• (P, Q, R, form a partition) ,

• ∀xy(R(x) ∧ R(y) → x = y ∧ P_{c}(x)),

• ∀xyz(P (x) ∧ Q(y) ∧ R(z) → x < z < y),

• P (d),

• ∀x(s(s(x)) = x),

• ∀x(P (x) → Q(s(x))),

• ∀x(R(x) → s(x) = x),

• ∀x ∈ P (P_{c}(x) ↔ x = d),

• ∀xy(P (x) ∧ P (y) ∧ x < y → s(y) < s(x))

• ∀x(P_{a}(x) ↔ P_{a}(s(x))),

• ∀x(P_{b}(x) ↔ P_{b}(s(x))),

• ∀x(P_{c}(x) ↔ P_{c}(s(x))).

With S(ψ_{s}) = S(τ)∪{P, Q, R, s}, where P, Q, R are unary predicate symbols and s is a unary function symbol. ψ_{s} is equivalent to a universal sentence and closure takes at most two steps in every model of it, hence ψ_{s} is local.

L(x, y) ∩ L_{s} consists of all words in the following form: ba^{i_{k}}...ba^{i_{1}}cx_{i_{1}}...x_{i_{k}}cy_{i_{k}}^{R}...y_{i_{1}}^{R}ca^{i_{1}}b...a^{i_{k}}b where: k ≥ 1, 1 ≤ i_{j} ≤ n and x_{i_{1}}...x_{i_{k}} = y_{i_{1}}...y_{i_{k}}

Then L(x, y) ∩ L_{s} is empty if and only if there is not any solution to Post Correspondence Problem for x, y. In the other case L(x, y) ∩ L_{s} is infinite. From this fact we can deduce a), b), and c):

It is undecidable to determine , for arbitrary L(x, y):

a) Whether L(x, y) ∩ L_{s} is empty.

b) Whether L(x, y) ∩ L_{s} is infinite.

c) Whether τ(L(x, y))∩τ(L_{s}) is empty, where τ is the morphism {a, b, c}^{⋆} → {a, b}^{⋆} defined by : a → bab, b → ba^{2}b, c → ba^{3}b.

c) results from the fact that τ(L(x, y)) ∩ τ(L_{s}) is empty iff L(x, y) ∩ L_{s} is empty.

Lemma 4.3 τ(L(x, y)) ∩ τ(L_{s}) doesn’t contain any infinite context free language.

Proof. In [Gin66]

So we can deduce that τ(L(x, y)) ∩ τ(L_{s}) is context free iff it is rational iff it is empty iff it is not infinite. L(x, y) and L_{s} being local languages, and the image of a local language by a morphism being a local language, τ(L(x, y)) and τ(L_{s}) are local languages over the alphabet {a, b}. ¿From this we deduce 1),2), 3), and 4) of our Theorem , because one cannot decide whether τ(L(x, y)) ∩ τ(L_{s}) is empty, infinite, rational or context free.

\underline{Let us show 5)}: Suppose there exists an algorithm which, for any arbitrary given local languages L(φ) and L(ψ) over an alphabet Σ = {a, b}, answers: either L(φ) ∩ L(ψ) is not local , either L(φ) ∩ L(ψ) = L(θ) giving a local sentence θ and n_{θ}.

Then there are two cases:

1. First case. L(φ) ∩ L(ψ) is not local, and then L(φ) ∩ L(ψ) is not empty because the emptyset is a local language.

2. Second case. L(φ) ∩ L(ψ) = L(θ), and then following [Res88] we could decide whether L(θ) is empty so whether L(φ) ∩ L(ψ) is empty. The proof of 1) shows there would be a contradiction, so 5) is proved.

Let us prove 6) –14). First show that {a, b, c}^{⋆} − L(x, y) is a local language. It is the union of six languages M_{i}, 1 ≤ i ≤ 6. Let x = (x_{1}, ..., x_{n}) and y = (y_{1}, ..., y_{n}) and let:

M_{1} = {a, b}^{⋆} ∪ {a, b}^{⋆}c{a, b}^{⋆} ∪ [{a, b}^{⋆}c]^{2}{a, b}^{⋆} ∪ [{a, b}^{⋆}c]^{4}{a, b, c, }^{⋆}

{a, b, c, }^{⋆} − M_{1} consists of all the words of {a, b, c, }^{⋆} with exactly three occurrences of c.

Let M_{2} = {a, c}{a, b, c}^{⋆} ∪ {a, b, c}^{⋆}{a, c} ∪ {a, b, c}^{⋆}c^{2}{a, b, c}^{⋆}.

Then M_{2} consists of all the words beginning by a or c or finishing by a or c or containing c^{2} as a subword.

Let M_{3} = {a, b}^{⋆}b^{2}{a, b}^{⋆}c{a, b, c}^{⋆}∪{a, b, c}^{⋆}c{a, b}^{⋆}b^{2}{a, b}^{⋆}∪{a, b}^{⋆}bc{a, b, c}^{⋆}∪ {a, b, c}^{⋆}cb{a, b}^{⋆}.

M_{3} consists of all the words with either b^{2} before the first c, either b^{2} after the last c , either b immediately on the left of the first c , either immediately on the right of the last c.

Let M_{4} = {a, b}^{⋆}a^{n+1}{a, b}^{⋆}c{a, b, c}^{⋆} ∪ {a, b, c}^{⋆}c{a, b}^{⋆}a^{n+1}{a, b}^{⋆}.

M_{4} consists of all the words with some a^{h}, h ≥ n + 1, either before the first c or after the last c.

Each language M_{i}, 1 ≤ i ≤ 4, is rational, hence local.

Let H = {a, b, c}^{⋆} − ∪_{i=1}^{4}M_{i}. H consists of all the words in the following form: ba^{i_{k}}...ba^{i_{1}}cucvca^{j_{1}}b...a^{j_{m}}b, where u and v are nonempty words of {a, b}^{⋆}, k ≥ 1, m ≥ 1, 1 ≤ i_{r} ≤ n, 1 ≤ j_{s} ≤ n.

{a, b, c}^{⋆} − H = ∪_{i=1}^{4}M_{i} is rational then it is local.

We are going to add two languages M_{5} and M_{6} to {a, b, c}^{⋆} −H in order that the resulting union be {a, b, c}^{⋆} − L(x, y).

Define for every nonempty word w of {a, b}^{⋆}: D(w) = {u ≠ λ/u ∈ {a, b}^{⋆}, |u| < |w|} and J(w) = {u ≠ λ/u ∈ {a, b}^{⋆}, u ≠ w, |u| = |w|} Next for each n-tuple w = (w_{1}, ...w_{n}) of nonempty words w_{i}, we define: M(w) = c{a, b}^{⋆}{a, b} ∪ b{a, b}^{⋆}c ∪ ∪_{1≤i≤n} ∪_{u∈D(w_{i})} (ba^{i}cu ∪ ba^{i}b{a, b}^{⋆}cu) ∪ ∪_{1≤i≤n} ∪_{u∈J(w_{i})} (ba^{i}c{a, b}^{⋆}u ∪ ba^{i}b{a, b}^{⋆}c{a, b}^{⋆}u).

M(x) is a rational language (because for each i, D(w_{i}) and J(w_{i}) are finite sets ), hence local and generated by a grammar G = (V, Σ, P, σ). Let G′ = (V′, Σ, P′, σ′), where σ′ is not in V and P′ = P ∪ {σ′ → σ, σ′ → ba^{i}σ′x_{i}/1 ≤ i ≤ n}.

It holds that M_{5} = L(G′).c.{a, b, c}^{⋆}. Remark that if h is the substitution {a, b, c}^{⋆} → P ({a, b, c}^{⋆}) defined by a → {a}, b → {b}, and c → M(x) then h(L(x)) = L(G′). But L(x) and M(x) being local, and local languages being closed under substitution, we can infer that L(G′) is local and then by concatenation product that M_{5} is a local language.

Each word of L(G′) contains exactly one occurrence of c, L(G′) ∩ L(x) is empty and L(G′) contains the set of words {ba^{i_{k}}...ba^{i_{1}}cw/w ≠ x_{i_{1}}...x_{i_{k}}, w ∈ {a, b}^{⋆}}.

M_{5} ∩ H consists of all the words of H in the form ba^{i_{k}}...ba^{i_{1}}cucvca^{j_{1}}b...a^{j_{m}}b with u ∈ {a, b}^{⋆} and u ≠ x_{i_{1}}...x_{i_{k}}.

In a similar manner , let G_{1} = (V_{1}, Σ, P_{1}, σ_{1}) be a grammar generating M(y)^{R}. Let G_{2} = (V′_{1}, Σ, P′_{1}, σ′_{1}) , where σ′_{1} is a new symbol not in V_{1} and P′_{1} = P_{1} ∪ {σ′_{1} → σ, σ′_{1} → y_{i}^{R}σ′_{1}a^{i}b/1 ≤ i ≤ n}. Then M_{6} = {a, b, c}^{⋆}.c.L(G_{2}).

And if h′ is the substitution {a, b, c}^{⋆} → P ({a, b, c}^{⋆}) defined by a → {a}, b → {b}, and c → M(y)^{R} , then L(G_{2}) = h′(L(y)^{R}).

L(y)^{R} and M(y)^{R} are local languages therefore L(G_{2}) is local by substitution and we deduce by concatenation product that M_{6} is a local language.

M_{6} ∩ H consists of all the words of H in the form ba^{i_{k}}...ba^{i_{1}}cucvca^{j_{1}}b...a^{j_{m}}b with v^{R} ≠ y_{j_{1}}...y_{j_{m}}.

Therefore [{a, b, c}^{⋆} − H] ∪ M_{5} ∪ M_{6} = ∪_{i=1}^{6}M_{i} = {a, b, c}^{⋆} − L(x, y) is a local language.

Then considering the previous morphism τ, τ[{a, b, c}^{⋆} − L(x, y)] is a local language, which is equal to τ[{a, b, c}^{⋆}] − τ[L(x, y)]. The language {a, b}^{⋆} − τ[{a, b, c}^{⋆}] is a rational language hence it is also a local one. But local languages are closed under union, then {a, b}^{⋆}−τ[L(x, y)] is also a local language. And if Σ contains at least two elements, then Σ^{⋆} − [L(x, y)] is a local language.

Let us show now that {a, b}^{⋆} − τ[L_{s}] is a local language:

{a, b, c}^{⋆} − L_{s} = M′_{1} ∪ M′_{2} ∪ M′_{4}, Where:

M′_{1} is the set words of {a, b, c}^{⋆} with less than three or more than three occurrences of c. M′_{1} is rational then local.

M′_{2} is the set of words w_{1}cw_{2}cw_{3}cw_{4} where each w_{i} ∈ {a, b}^{⋆} and where w_{4} ≠ w_{1}^{R}. This language is the union of the following languages :

• M_{2,1} = {w_{1}cw_{2}cw_{3}cw_{4}/w_{i} ∈ {a, b}^{⋆} and |w_{1}| < |w_{4}|},

• M_{2,2} = {w_{1}cw_{2}cw_{3}cw_{4}/w_{i} ∈ {a, b}^{⋆} and |w_{4}| < |w_{1}|},

• M_{2,3} = {w_{1}cw_{2}cw_{3}cw_{4}/w_{i} ∈ {a, b}^{⋆} and |w_{1}| = |w_{4}| and w_{4} ≠ w_{1}^{R}}.

M_{2,1} is defined by the following local sentence ψ_{2,1}, conjunction of:

• (< is a linear order)

• (P_{a}, P_{b}, P_{c}, form a partition),

• (P, Q, R, form a partition) ,

• ∀xyz(P (x) ∧ Q(y) ∧ R(z) → x < z < y),

• ∀x(P (x) → P_{a}(x) ∨ P_{b}(x)), • ∀x(Q(x) → P_{a}(x) ∨ P_{b}(x)),

• ∀x(R(x) → c_{1} ≤ x ≤ c_{3}),

• R(c_{1}) ∧ R(c_{2}) ∧ R(c_{3}) ∧ c_{1} ≠ c_{2} ∧ c_{1} ≠ c_{3} ∧ c_{2} ≠ c_{3},

• ∀x(P_{c}(x) ↔ x = c_{1} ∨ x = c_{2} ∨ x = c_{3}),

• ∀xy((P (x) ∧ P (y) ∧ x ≠ y) → i(x) ≠ i(y)),

• ∀x(P (x) → Q(i(x))),

• ∀x(R(x) ∨ Q(x) → i(x) = x),

• Q(d) ∧ ∀x(P (x) → i(x) ≠ d). This sentence is equivalent to a universal sentence, its signature is

S(ψ_{2,1}) = {<, P_{a}, P_{b}, P_{c}, P, Q, R, i, c_{1}, c_{2}, c_{3}, d} where P, Q, R, are unary predicate symbols, i is a unary function symbol, and c_{1}, c_{2}, c_{3}, d , are constant symbols. And if M ⊧ ψ_{2,1} and X ⊆ |M| then cl(X, M) = cl^{1}(X, M).Therefore ψ_{2,1} is local and the language L(ψ_{2,1}) = M_{2,1} is local. In a similar manner, M_{2,2} = M_{2,1}^{R} is a local language. M_{2,3} is defined by the following local sentence ψ_{2,3}, conjunction of:

• (< is a linear order),

• (P_{a}, P_{b}, P_{c}, form a partition),

• (P, Q, R, form a partition ),

• ∀xyz(P (x) ∧ Q(y) ∧ R(z) → x < z < y),

• ∀x(P (x) → P_{a}(x) ∨ P_{b}(x)),

• ∀x(Q(x) → P_{a}(x) ∨ P_{b}(x)),

• ∀x(R(x) → c_{1} ≤ x ≤ c_{3}),

• R(c_{1}) ∧ R(c_{2}) ∧ R(c_{3}) ∧ c_{1} ≠ c_{2} ∧ c_{1} ≠ c_{3} ∧ c_{2} ≠ c_{3},

• ∀x(P_{c}(x) ↔ x = c_{1} ∨ x = c_{2} ∨ x = c_{3}),

• ∀x(i(i(x)) = x),

• ∀x(P (x) ↔ Q(i(x))), • ∀x(R(x) → i(x) = x),

• ∀xy(P (x) ∧ P (y) ∧ x < y → i(y) < i(x)),

• P_{a}(d) ∧ P_{b}(i(d)).

the signature of ψ_{2,3} is the same as S(ψ_{2,1}). ψ_{2,3} is equivalent to a universal sentence and closure takes at most two steps in each of its models. So this sentence is local and the language L(ψ_{2,3}) = M_{2,3} is local.

Then by union the language M′_{2} is local.

Then M′_{4} = {a, b}^{⋆}.c.M′_{3}.c.{a, b}^{⋆}, where M′_{3} is the set of words w_{2}cw_{3} , where w_{2} and w_{3} ∈ {a, b}^{⋆} and w_{3} ≠ w_{2}^{R}. By analogous methods as in the case of M′_{2}, We show that M′_{3} is local , then by concatenation we can deduce that M′_{4} is local.

Therefore, as the union of the local languages M′_{1}, M′_{2} and M′_{4}, the language {a, b, c}^{⋆} − L_{s} is local. Then by an analogous reasoning as in the case of {a, b}^{⋆} −τ[L(x, y)], we show that {a, b}^{⋆} −τ[L_{s}] is a local language, Where τ is the above morphism.

Now , For Σ an alphabet containing at least two elements a and b, let: M_{1}(x, y) = Σ^{⋆} − (τ[L(x, y)] ∩ τ[L_{s}]) = (Σ^{⋆} − τ[L(x, y)]) ∪ (Σ^{⋆} − τ[L_{s}]).

M_{1}(x, y) is a local language as the union of two local languages, and Σ^{⋆} − M_{1}(x, y) = τ[L(x, y)] ∩ τ[L_{s}]

Then from our proof of 1), 2), 3), and 4), we can deduce 8), 10), 11), 12) and 13) because τ[L(x, y)] ∩ τ[L_{s}] is context free iff it is rational iff it is empty iff it is not infinite, and this is undecidable.

And M_{1}(x, y) is a rational language iff Σ^{⋆} − M_{1}(x, y) is a rational language because the class of rational languages is closed under complementation, and this implies 9).

For 14) we reason as for 5).

8) implies 7) which implies 6).

8) implies also 17) and 18).

\underline{To prove 15)} we follow [Gin66, exercise 16, p.128]. Let Σ containing at least three elements and let c ∈ Σ. For an arbitrary context free language L ⊆ (Σ − {c})^{⋆}, LcL is a linear language iff L is rational. Then when M_{1}(x, y) = {a, b}^{⋆} − (τ[L(x, y)] ∩ τ[L_{s}]) it is undecidable to determine whether the local language M_{1}(x, y)cM_{1}(x, y) is a linear language.

\underline{To prove 16)} let us utilize Lemma 4.3.4. of [Gin66] : For some n-tuples of nonempty words of {a, b}^{⋆} : y = (y_{1}, ..., y_{n}) and z = (z_{1}, ..., z_{n}), consider the language M(y, z) = ∪_{1≤r<∞}[dL(y)]^{r}[dL(z)]^{r}. It is undecidable to determine whether the language M(y, z), ( over an alphabet containing at least four elements a, b, c, d) , contains an infinite rational language. Then by Lemma 4.3.4. of [Gin66] , if τ′ is the morphism {a, b, c, d}^{⋆} → {a, b}^{⋆} defined by τ′(a) = bab , τ′(b) = ba^{2}b, τ′(c) = ba^{3}b, τ′(d) = ba^{4}b , it is undecidable to determine whether the language τ′[M(y, z)] over {a, b} contains an infinite rational language. Then it suffices to show that τ′[M(y, z)] is a local language and, because the image of a local language by a morphism is local, that M(y, z) is local. The language L = {e^{n}f^{n}/1 ≤ n} is local . And if k is the substitution {e, f}^{⋆} → P ({a, b, c, d}^{⋆}) defined by e → dL(y) and f → dL(z) , then k(L) = M(y, z). Therefore M(y, z) is local because L is local and local languages are closed under substitution.

5 Definitions and review of transfinite length word languages

5.1 words of infinite and transfinite length

We shall assume the reader to be familiar with the elementary theory of countable ordinals, which may be found in [Sie65]. Let Σ be a finite alphabet, and α be an ordinal. A word of length α (an α-word) over the alphabet Σ is an α-sequence (or sequence of length α) of letters in Σ. In a similar manner as in the case of finite words, we’ ll identify a word σ of length α over Σ with the structure (α, <^{σ}, (P_{a}^{σ})_{a∈Σ}) which signature is Λ_{Σ} = {<, (P_{a})_{a∈Σ}} where the unary predicate P_{a} is interpreted by P_{a}^{σ} = {i < α such that the i + 1^{th} letter of σ is an a}. Let then α be an ordinal ≥ ω. We’ ll denote Σ^{α} the set of α-words over the alphabet Σ. And we define an α-language over Σ as a subset of Σ^{α}. We can now set the following definition:

Definition 5.1 Let L be an α-language over the alphabet Σ. L is a locally finite α-language iff there exists a local sentence φ in a signature Λ ⊇ Λ_{Σ} such that: (σ ∈ L) ⟷ (∃M, M ⊧ φ, M of order type α and M|Λ_{Σ} = σ). (where M|Λ_{Σ} is the reduction of M to the signature Λ_{Σ}).

Notation. Let us denote L_{α}^{Σ}(φ) ( or L_{α}(φ) if there is no ambiguity about the alphabet Σ ) the α-language defined by the local sentence φ. And we’ ll note L_{≥α}(φ) = ∪_{β≥α}L_{β}(φ) and L_{>α}(φ) = ∪_{β>α}L_{β}(φ).

5.2 Automata over words of length ω

Recall first the notion of Büchi automaton reading words of length ω, [Eil74], [Tho90], [PP98]. Intuitively a Büchi automaton is a finite automaton which reads infinite words, the acceptation condition for an ω-word being that during its reading ( or during one of its readings, in the non deterministic case ), one of the “final” states appears infinitely often.

Definition 5.2 A Büchi automaton over the alphabet Σ is of the form Aut = (Q, q_{0}, Δ, F) where Q is a finite set of states, q_{0} is the initial state ∈ Q , Δ is the transition relation ( Δ ⊆ Q × Σ × Q ) and F is a subset of Q called the set of final states. A run of Aut reading an ω-word σ = σ(0)σ(1)...σ(n)... of Σ^{ω} is an ω-sequence α = α(0)α(1)...α(n)... such that α(0) = q_{0} and (α(i), σ(i), α(i + 1)) ∈ Δ for i ≥ 0. The run is called successful if Inf(α) ∩ F ≠ ∅ ,where Inf(α) is the set of elements of Q which appear infinitely often in the ω-sequence α. The automaton Aut accepts the ω-word σ if there exists a successful run of Aut over σ.We denote L_{ω}(Aut) = {σ ∈ Σ^{ω} \ Aut accepts σ} the ω-language recognized by Aut. If L = L_{ω}(Aut) for a Büchi automaton Aut, L is called a Büchi ω-language .

Recall now some of the essential results about Büchi ω-languages:

Theorem 5.3 The class of Büchi ω-languages is the omega-Kleene closure of the set of rational languages , i.e. the class of languages in the form ∪_{i=1}^{n}U_{i}.V_{i}^{ω} ,where n is a non negative integer, and for each i∈[1,n], U_{i} and V_{i} are rational languages.

Theorem 5.4 ([Tho90]) The emptiness problem for Büchi ω-languages is decidable. (this means that: “For an arbitrary Büchi automaton Aut, is L_{ω}(Aut) empty? “ is a decidable problem. )

Remark 5.5 Muller defined another class of automata reading words of length ω. the difference between Büchi and Müller automata is the notion of acceptation of an ω-word . A Muller automata is in the form Aut = (Q, q_{0}, Δ, F) where Q, q_{0}, Δ are defined in a similar manner as in the Büchi case and where F ⊆ P (Q), (F is a subset of the power set of Q). A run of the automata is defined as above but a run α of Aut over σ is successful if Inf(α) ∈ F.

Theorem 5.6 (Mac Naughton). An ω-language over the alphabet Σ is Muller recognizable iff it is Büchi recognizable.

The advantage of Muller automata is that the deterministic version has the same expressive power as the non deterministic version, while this is false for Büchi automata.

5.3 Büchi ω-languages are local ω-languages

We shall show the following result:

Theorem 5.7 Every Büchi ω-language is a local ω-language and, if B is a Büchi ω-language, there exists a local sentence φ such that L_{ω}(φ) = B and L_{>ω}(φ) = ∅.

Proof. We shall use the characterization of Büchi ω-languages by ω-regular expresssions. Let B be a Büchi ω-language over the alphabet Σ. Then there exist some rational languages (U_{i}) and (V_{i}) over Σ, where 1 ≤ i ≤ n, such that B = ∪_{i=1}^{n}U_{i}.V_{i}^{ω}. Recall that for V ⊆ Σ^{⋆}, we denote V^{ω} = {α ∈ Σ^{ω} \α = α_{1}α_{2}α_{3}...α_{n}..... with α_{i} ∈ V, ∀i ≥ 1}.

Recall The following Lemma [Fin89]: If U is a rational language over Σ, Then there exists a local sentence φ such that U = L^{Σ}(φ) and L_{α}^{Σ}(φ) = ∅ for α ordinal ≥ ω. This is proved by induction on the complexity of a regular expression defining a rational language.

Let then some local sentences φ_{i} and ψ_{i}, 1 ≤ i ≤ n, such that ∀i ∈ [1, n], L(φ_{i}) = U_{i}, L(ψ_{i}) = V_{i} and L_{≥ω}(φ_{i}) = ∅ and L_{≥ω}(ψ_{i}) = ∅.

Recall also that for two local sentences φ_{1} and φ_{2} defining local languages L(φ_{1}) and L(φ_{2}), we can easily define the local sentences φ_{1}.φ_{2} and φ_{1} ∪ φ_{2} such that L(φ_{1}.φ_{2}) = L(φ_{1}).L(φ_{2}) and L(φ_{1} ∪ φ_{2}) = L(φ_{1}) ∪ L(φ_{2}).

Remark that for words of transfinite length, we get:

L_{α}(φ_{1}.φ_{2}) = ∪_{(β_{1}+β_{2}=α)}L_{β_{1}}(φ_{1}).L_{β_{2}}(φ_{2})
L_{α}(φ_{1} ∪ φ_{2}) = L_{α}(φ_{1}) ∪ L_{α}(φ_{2}).

Recall also (see proof of Theorem 3.1) that for any local sentence φ,

φ^{⋆} is defined in the signature S(φ^{⋆}) which is the signature of φ to which is added a unary function symbol I and in which every constant symbol e is replaced by a unary function symbol.

φ^{⋆} is the sentence defined by the conjunction of:

• (< is a linear order),

• ∀yz[I(y) ≤ y and (y ≤ z → I(y) ≤ I(z)) and (I(y) ≤ z ≤ y → I(z) = I(y))],

• ∀xy[I(x) = I(y) → e(x) = e(y)], for each constant e of the signature S(φ) of φ,

• ∀x_{1}...x_{n}[(⋁_{i,j≤n} I(x_{i}) ≠ I(x_{j})) → f(x_{1}...x_{n}) = min(x_{1}...x_{n})] , for each n-ary function f of S(φ),

• ∀x_{1}...x_{n}[(⋀_{i,j≤n} I(x_{i}) = I(x_{j})) → I(f(x_{1}...x_{n})) = I(x_{1})], for each n-ary function f of S(φ),

• ∀xφ^{x}, where φ^{x} is the local sentence φ in which every constant e is replaced by the term e(x) and each quantifier is relativized to the set {y \ I(y) = I(x)}.

Remark 5.8 The models of φ^{⋆} are essentially direct sums of models of φ , and L^{Σ}(φ^{⋆}) = (L^{Σ}(φ))^{⋆}.

Remark 5.9 These three operations over local sentences : φ, ψ → φ.ψ then φ, ψ → φ∪ψ and φ → φ^{⋆}, already permit us to construct a sentence defining the Büchi language B.

We have B = ∪_{i=1}^{n}U_{i}.V_{i}^{ω} and U_{i} = L(φ_{i}), V_{i} = L(ψ_{i}) for 1 ≤ i ≤ n. Let then the local sentence ∪_{i=1}^{n}φ_{i}.(ψ_{i}^{⋆}) = φ. We easily verify that L_{ω}(φ) = ∪_{i=1}^{n}L(φ_{i}).L_{ω}(ψ_{i}^{⋆}), i.e. L_{ω}(φ) = ∪_{i=1}^{n}L(φ_{i}).L(ψ_{i})^{ω} = ∪_{i=1}^{n}U_{i}.V_{i}^{ω} = B.

Remark 5.10 The hypothesis L_{≥ω}(φ_{i}) = ∅ and L_{≥ω}(ψ_{i}) = ∅ was necessary to state that L_{ω}(ψ_{i}^{⋆}) = L(ψ_{i})^{ω} and that L_{ω}(φ) = ∪_{i=1}^{n}L(φ_{i}).L_{ω}(ψ_{i}^{⋆}).

Remark 5.11 Every Büchi ω-language is then a local ω-language. For the continuation, we’ll show that we can obtain φ such that L_{ω}(φ) = B and L_{>ω}(φ) = ∅. for that, let us define a new operation over local sentences.

Definition 5.12 Let φ and ψ local sentences such that S(φ^{⋆})∩S(ψ) = {<}. We define the sentence φ^{(⋆ψ)} in the signature S(φ^{⋆}) ∪ S(ψ) ∪ {P }, where P is a new unary predicate symbol . φ^{(⋆ψ)} is the conjunction of :

• φ^{⋆},

• ∀x[P (x) ↔ I(x) = x],

• ∀x_{1}...x_{n}[(⋀_{i=1}^{n} P (x_{i})) → ψ_{1}(x_{1}...x_{n})], where ψ = ∀x_{1}...x_{n}ψ_{1}(x_{1}...x_{n}) and ψ_{1} is an open formula,

• ∀x_{1}...x_{k}[(⋀_{i=1}^{k} P (x_{i})) → P (t(x_{1}...x_{k}))], for each k-ary function t of S(ψ),

• ∀x_{1}...x_{k}[Q(x_{1}...x_{k}) → P (x_{1}) ∧ ... ∧ P (x_{k})], for each k-ary predicate symbol Q of S(ψ)

• P (a), for each constant a of S(ψ),

• ∀x_{1}...x_{n}[(⋁_{i=1}^{n} ¬P (x_{i})) → t(x_{1}...x_{n}) = min(x_{1}...x_{n})], for each n-ary function t in S(ψ).

Remark 5.13 The models of φ^{(⋆ψ)} essentially are direct sums of models of φ , these models being ordered by the order type of a model of ψ.

Recall now the following result:

Lemma 5.14 ([FR96]) There exists a local sentence φ_{ω}, with <∈ S(φ_{ω}), which has a model of order type ω (for <) and no model of order type an ordinal α > ω.

We can then modify the expression of φ we are looking for: Let φ = ∪_{i=1}^{n}φ_{i}.ψ_{i}^{(⋆φ_{ω})}. We have then L_{ω}(φ) = ∪_{i=1}^{n}U_{i}.V_{i}^{ω} = B , and this time φ has not any model of order type > ω.

Remark 5.15 The same proof shows that every ω-language in the form

∪_{i=1}^{n}U_{i}.V_{i}^{ω} where U_{i} and V_{i} are local languages , is a local ω-language. then the ω-Kleene closure of the set of local languages is included in the set of local ω-languages. We have shown that local languages extend far beyond rational languages , that many context free languages are local, and many non context free also. So the above proof implies that local ω-languages extend far beyond Büchi ω-languages [Fin89] [Fin99].

6 Automata over words of transfinite length

So as an automata to be able to read words of length ≥ ω, we must add to the automaton a transition relation for limit steps: after the reading of a word which length is a limit ordinal, the state of the automaton will depend on the set of states which cofinally appeared during the run of the automaton [BS73], [Hem92], [Bed96].

6.1 First definitions

Definition 6.1 A generalized Büchi automaton is a sextuple (Σ, Q, q_{0}, Δ, γ, F) where: Σ is a finite alphabet , Q is a finite set of states, q_{0} is a state in Q called initial state, Δ ⊂ Q × Σ × Q, is the transition relation, γ ⊂ P (Q) × Q.

Σ, Q, q_{0}, Δ and F keep the same signification as before, the signification of γ is given by the :

Definition 6.2 A run of the generalized Büchi automaton Aut = (Σ, Q, q_{0}, Δ, γ, F) reading the word σ of length α, is an (α+1)-sequence of states x defined by : x(0) = q_{0} and for i < α , (x(i), σ(i), x(i+1)) ∈ Δ and for i a limit ordinal, (Inf(x, i), x(i)) ∈ γ, where Inf(x, i) = {q ∈ Q \ ∀μ < i, ∃ν < i such that μ < ν and x(ν) = q}. Inf(x, i) is the set of states which cofinally appear during the reading of the i first letters of σ. A run x of the automaton Aut over the word σ of length α is called successful if x(α) ∈ F. A word σ of length α is accepted by Aut if there exists a successful run of Aut over σ. We denote L_{α}(Aut) the set of words of length α which are accepted by Aut. An α-language L is a (generalized) Büchi α-language if there exists a generalized Büchi automaton A such that L = L_{α}(A).

Remark 6.3 When we consider only finite words, the language accepted by a generalized Büchi automaton is a rational language. And the notion of ω-language accepted by generalized Büchi automaton corresponds to that of ω-language accepted by Muller automaton and then also by Büchi automaton.

6.2 ω^{2}-languages accepted by generalized Büchi automata are local ω^{2}-languages

Let Aut = (Σ, Q, q_{0}, Δ, γ, F) be a generalized Büchi automaton, and let L_{ω^{2}}(Aut) be the ω^{2}-language recognized by Aut. We shall decompose the reading of an ω^{2}-word by Aut into blocks of length ω. Let σ be an ω^{2}-word. Aut reads the word σ: after the reading of the first ω letters, Aut is in state x(ω), after the reading of ω.2 letters, Aut is in state x(ω.2) and so on... Define now the following ω-languages : For q_{i} ∈ Q, q_{j} ∈ Q and E ⊆ Q, L(q_{i}, q_{j}, E) is the ω-language of words u such that there exists a reading of u by Aut such that Aut reads the word u, beginning in state q_{i}, it is in state q_{j} after the reading of u and the set of states in which the automaton has been (q_{i} and q_{j} comprised) is the set E. We easily see that these ω-languages are recognized by Muller automata therefore also by Büchi automata.

Consider now a new alphabet: Γ = {(q_{i}, q_{j}, E) \ q_{i} ∈ Q, q_{j} ∈ Q, E ⊆ Q} = Q×Q×P (Q) and consider the ω-language over Γ of the ω-words such that: The first letter is in the form (q_{0}, q, E) and each letter (q_{i}, q_{j}, E) is followed by a letter (q_{j}, q, G) with q ∈ Q, G ⊆ Q. And such that X = {q ∈ Q\ there exists a letter (q_{i}, q_{j}, G) which appears infinitely often with q ∈ G} satisfies (X, q_{f}) ∈ γ for a q_{f} ∈ F. This ω-language over Γ is a Büchi ω-language. Denote it by L_{Aut}^{Γ}. Remark that if we substitute in L_{Aut}^{Γ} the ω-language L(q_{i}, q_{j}, E) for each letter (q_{i}, q_{j}, E) , we obtain the ω^{2}-language recognized by Aut, i.e. L_{ω^{2}}(Aut). From the preceding results, there exists a local sentence φ^{Γ} such that L_{ω}^{Γ}(φ^{Γ}) = L_{Aut}^{Γ} and L_{>ω}(φ^{Γ}) = ∅. In the same way there exist local sentences φ_{(q_{i},q_{j},E)} such that L_{ω}^{Σ}(φ_{(q_{i},q_{j},E)}) = L(q_{i}, q_{j}, E) and L_{>ω}(φ_{(q_{i},q_{j},E)}) = ∅. We then use the substitution method established in the above section :” closure properties of local languages ”. We’ll now assume that the signatures of the sentences φ_{(q_{i},q_{j},E)} satisfy: S(φ_{(q_{i},q_{j},E)}) ∩ S(φ_{(q′_{i},q′_{j},E′)}) = {<, (P_{a})_{a∈Σ}} for (q_{i}, q_{j}, E) ≠ (q′_{i}, q′_{j}, E′).

Let Q_{a} be the unary predicate in S(φ^{Γ}), which indicates the place of the letter a ∈ Γ. We also assume, possibly differently naming the function, constant and other predicate symbols of S(φ^{Γ}) that S(φ_{(q_{i},q_{j},E)}) ∩ S(φ^{Γ}) = {<} for every (q_{i}, q_{j}, E) ∈ Q × Q × P (Q).

Let us now construct a local sentence defining the language L_{ω^{2}}(Aut): ψ is the conjunction of the following sentences ( the meaning of which is explained below):

• (< is a linear order),

• ∀xy[(I(y) ≤ y) ∧ (y ≤ x → I(y) ≤ I(x)) ∧ (I(y) ≤ x ≤ y → I(x) = I(y))],

• ∀x[I(x) = x ↔ P (x)],

• P (c), for each constant c of S(φ^{Γ}),

• ∀x_{1}...x_{k}[R(x_{1}...x_{k}) → P (x_{1})∧....∧P (x_{k})], for each predicate R(x_{1}...x_{k}) of S(φ^{Γ}),

• ∀x_{1}...x_{j}[(P (x_{1}) ∧ ... ∧ P (x_{j})) → P (f(x_{1}...x_{j}))], for each j-ary function symbol f of S(φ^{Γ}),

• ∀x_{1}...x_{j}[(⋁_{1≤i≤j} ¬P (x_{i})) → f(x_{1}...x_{j}) = min(x_{1}...x_{j})], for each j-ary function symbol f of S(φ^{Γ}),

• ∀x_{1}...x_{m}[(P (x_{1})∧...∧P (x_{m})) → φ_{0}^{Γ}(x_{1}...x_{m})], where φ^{Γ} = ∀x_{1}...x_{m}φ_{0}^{Γ}(x_{1}...x_{m}) with φ_{0}^{Γ} an open formula,

• ∀x_{1}...x_{j}[⋁_{i,k≤j}(I(x_{i}) ≠ I(x_{k})) → f(x_{1}...x_{j}) = min(x_{1}...x_{j})], for every function f of S(φ_{(q_{i},q_{j},E)}) for (q_{i}, q_{j}, E) ∈ Q × Q × P (Q),

• ∀xy_{1}...y_{j}[(⋀_{1≤l≤j} I(y_{l}) = I(x)) → I(f(y_{1}...y_{j})) = I(x)], for each j-ary function symbol f of S(φ_{(q_{i},q_{j},E)}) for (q_{i}, q_{j}, E) ∈ Γ,

• Finally, for each letter (q_{i}, q_{j}, E) and the associated sentence φ_{a} = φ_{(q_{i},q_{j},E)}:

• ∀xy_{1}...y_{p}[(⋀_{1≤l≤p} I(y_{l}) = I(x) ∧ Q_{a}(I(x))) → φ_{a}^{0}(y_{1}...y_{p}) ∧ {(e_{b}(y_{1}) = I(x) ∧ f_{b}(y_{1}...y_{p}) = y_{1} ∧ ¬R_{b}(y_{1}...y_{p}) ∧ ⋀_{e_{a}∈S(φ_{a})} e_{a}(y_{1}) = e_{a}(x); where b ≠ a, and e_{b}, f_{b}, R_{b} run over the constants, functions, and predicates of S(φ_{b})}], Above , 1) to each constant e_{a} of S(φ_{a}) is associated a new unary function e_{a}(y) and 2) whenever φ_{a} = ∀y_{1}...y_{p}ψ_{a}(y_{1}...y_{p}) with ψ_{a} open, φ_{a}^{0} is ψ_{a} in which every constant e_{a} has been replaced by the function e_{a}. At last we have the following conjunctions:

• ∀xy[(P (x) ∧ P (y) ∧ x < y) → (x < h(xy) < y ∧ ¬P (h(xy)))],

• ∀xyz ∈ P [x < y < z → x < h(xy) < h(xz) < y],

• ∀xy[(¬P (x) ∨ ¬P (y)) → h(xy) = x],

• ∀xy[(P (x) ∧ P (y) ∧ ¬(x < y)) → h(xy) = x].

Above h is a new binary function, P a unary predicate, I a unary function added to S(ψ).

Construction of ψ : Using the function I which marks the first letters of the subwords, we divide a word into subwords. In every model M of ψ, the set of the ”first letters of subwords” , P^{M}, grows richer in a model of φ^{Γ} ( therefore will constitute a word of L_{Aut}^{Γ}). Then we ”substitute” : for each letter (q_{i}, q_{j}, E) in P^{M}, we substitute a word of the associated language L(q_{i}, q_{j}, E), using for that the formula φ_{(q_{i},q_{j},E)}. The last four conjunctions imply that in a model M of ψ of order type ω^{2}, (P^{M} being of order type ω because the φ_{(q_{i},q_{j},E)} have not any model of order type > ω ), every subword is of order type ω, and therefore is a word of the associated Büchi language L(q_{i}, q_{j}, E). Then it really holds that L_{ω^{2}}(ψ) = L_{ω^{2}}(Aut).

Remark 6.4 This sentence is local because it is equivalent to a universal one, and closure takes a finite number of steps in a model of ψ: one takes the closure by I, then by the functions of S(φ^{Γ}), then by h, afterwards by the functions of the S(φ_{(q_{i},q_{j},E)}).

Remark 6.5 By construction, the sentence ψ has not any well ordered model of order type > ω^{2}, because φ^{Γ} and the φ_{(q_{i},q_{j},E)} have no well ordered model of order type > ω.

6.3 ω^{n}-languages recognized by generalized Büchi automata are local ω^{n}-languages

We shall prove the following result:

Theorem 6.6 Whenever n is an integer ≥ 1, every ω^{n}-language which is recognized by a generalized Büchi automaton is defined by a local sentence which has not any well ordered model of order type > ω^{n}.

Proof. We reason by induction over n. The cases n = 1 and n = 2 were solved in preceding paragraphs. Suppose the result be established for the integer n − 1. Let then a generalized Büchi automata Aut = (Σ, Q, q_{0}, Δ, γ, F) reading words of length ω^{n} with n ≥ 2. We now use a method which is analogous to that one used in the preceding case: We can divide a word of length ω^{n} into ω subwords of length ω^{n−1}. Let as above the new alphabet Γ = Q × Q × P (Q) and the ω-language over Γ: L_{Aut}^{Γ} = L_{ω}(φ^{Γ}). And let L^{n−1}(q_{i}, q_{j}, E), the ω^{n−1}-language of the ω^{n−1}-words u such that if Aut reads the word u beginning the reading in state q_{i} , it finishes the reading in state q_{j} and the set of states entered by Aut during the run is E, (q_{i} and q_{j} comprised in E ). We easily see that the languages L^{n−1}(q_{i}, q_{j}, E) are ω^{n−1}-languages recognized by generalized Büchi automata. Then remark that if one substitute in the language L_{Aut}^{Γ} the

language L^{n−1}(q_{i}, q_{j}, E) for the letter (q_{i}, q_{j}, E), we obtain the ω^{n}-language L_{ω^{n}}(Aut). By induction assumption, each language L^{n−1}(q_{i}, q_{j}, E) is defined by a local sentence φ_{(q_{i},q_{j},E)}^{n−1}: we have L^{n−1}(q_{i}, q_{j}, E) = L_{ω^{n−1}}^{Σ}(φ_{(q_{i},q_{j},E)}^{n−1}). We then use the substitution method as above: we obtain the sentence ψ of preceding paragraph, where we replaced the sentences φ_{(q_{i},q_{j},E)} by the sentences φ_{(q_{i},q_{j},E)}^{n−1} and the four last conjunctions by the conjunction of the following sentences (where h is a n-ary function symbol ).

• ∀x_{1}...x_{n}[(⋁_{1≤i≤n} ¬P (x_{i})) → h(x_{1}...x_{n}) = x_{1}],

• ∀x_{1}...x_{n}[(⋁_{2≤i≤n} ¬(x_{1} < x_{i})) → h(x_{1}...x_{n}) = x_{1}].

• ∀x_{1}...x_{n}[(⋀_{1≤i≤n} P (x_{i}) ∧ ⋀_{2≤i≤n}(x_{1} < x_{i})) → ¬P (h(x_{1}...x_{n}))], • ∀x_{1}...x_{n}[(⋀_{1≤i≤n} P (x_{i}) ∧ ⋀_{2≤i≤n}(x_{1} < x_{i}) ∧ P (y) ∧ x_{1} < y) → x_{1} <

h(x_{1}x_{2}...x_{n}) < y],

• ∀x_{1}...x_{n}∀y_{1}...y_{n}[(⋀_{1≤i≤n} P (x_{i})∧⋀_{1≤i≤n} P (y_{i})∧⋀_{2≤i≤n} x_{1} < x_{i}∧⋀_{2≤i≤n} x_{1} < y_{i} ∧ ⋀_{1≤i≤j} x_{i} = y_{i} ∧ x_{j+1} < y_{j+1}) → h(x_{1}...x_{n}) < h(y_{1}...y_{n})], for each integer j such that 1 ≤ j < n.

The principle is the same as before: if M is a model of order type ω^{n} of ψ, P^{M} is of order type ω because every sentence φ_{(q_{i},q_{j},E)}^{n−1} has no well ordered model of order type > ω^{n−1} , and then the function h ensures that every subword is of length ω^{n−1}. M|Λ_{Σ} is then a word of L_{ω^{n}}(Aut) and the converse is true: every word of L_{ω^{n}}(Aut) grows richer in a model of ψ. Then it really holds that: L_{ω^{n}}^{Σ}(ψ) = L_{ω^{n}}(Aut). More, by construction, ψ has no well ordered model of order type > ω^{n}. This achieves the proof by induction.

Remark 6.7 The construction of the sentence ψ may be done in an effective manner from the automaton Aut.

6.4 α-languages (ω ≤ α < ω^{ω}) recognized by generalized Büchi automata are local α-languages

We shall prove the following

Theorem 6.8 Let α be an ordinal such that ω ≤ α < ω^{ω}. Then every αlanguage recognized by a generalized Büchi automaton is a local α-language.

Proof. Let α be an ordinal such that ω ≤ α < ω^{ω}. The ordinal α admits a decomposition into the Cantor normal form [?]:

α = ω^{p_{k}}.n_{k} + ω^{p_{k−1}}.n_{k−1} + .... + ω^{p_{1}}.n_{1} + n_{0} where p_{i}, n_{i}, k are integers such that p_{k} > p_{k−1} > .... > p_{1} ≥ 1 and n_{0} ≥ 0, n_{i} ≥ 1 for 1 ≤ i ≤ k, and k ≥ 1. let Aut = (Σ, Q, q_{0}, Δ, γ, F) be a generalized Büchi automaton reading αwords over Σ. We reason as above, dividing this time an α-word into n_{k} subwords of length ω^{p_{k}}, then n_{k−1} subwords of length ω^{p_{k−1}} and so on ... up to n_{1} subwords of length ω^{p_{1}} and a finite subword of length n_{0}. Assume n_{0} > 0, the case n_{0} = 0 being treated in a similar manner. Let then L^{n}(q_{i}, q_{j}) be the ω^{n}-language of the ω^{n}-words σ over Σ such that there exists a run of the automaton Aut reading the word σ where Aut begins the reading of σ in state q_{i} and finishes it in state q_{j} (where q_{i} ∈ Q, q_{j} ∈ Q). And let R_{q} the rational language of finite words σ such that if Aut begins to read σ in state q, it finishes the reading in a final state of F. Let then the (finite) language L of finite words, of length n_{k} +n_{k−1} +...n_{1} +1 over the alphabet A = {L^{p_{l}}(q_{i}, q_{j}) \ q_{i} ∈ Q, q_{j} ∈ Q, 1 ≤ l ≤ k} ∪ {R_{q} \ q ∈ Q}. L is constituted of the words which begin with a letter in the form L^{p_{k}}(q_{0}, q_{i}), such that the n_{k} first letters are among the L^{p_{k}}(q_{i}, q_{l}) and such that a letter L^{p_{k}}(q_{i}, q_{l}) is followed by a letter L^{p_{k}}(q_{l}, q_{m}). The following n_{k−1} letters are among the letters L^{p_{k−1}}(q_{i}, q_{l}) then the n_{k−2} following letters are among the L^{p_{k−2}}(q_{i}, q_{l}), until the n_{1} letters among the L^{p_{1}}(q_{i}, q_{j}) followed by a letter among the R_{q}, q ∈ Q. And always a letter L^{p_{m}}(q_{i}, q_{l}) is followed by a letter L^{p_{m}}(q_{l}, q_{j}) or by a letter L^{p_{m−1}}(q_{l}, q_{j}), and the latest letter of the word being R_{q} if the last but one letter is in the form L^{p_{1}}(q_{i}, q). By construction, if one substitute in the language L for each letter L^{p_{m}}(q_{i}, q_{j}) or R_{q} the associated language (over Σ ), we obtain the α-language L_{α}(Aut). The language L is finite then it is local and it is defined by a local sentence φ which has no model of cardinal > n_{k} + n_{k−1} + ....n_{1} + 1. Each language L^{p_{j}}(q_{i}, q_{m}) is recognized by a generalized Büchi automaton therefore (from preceding paragraph) it is defined by a local sentence φ_{p_{j}}(q_{i}, q_{m}) such that L_{>ω^{p_{j}}} (φ_{p_{j}}(q_{i}, q_{m})) = ∅. For q ∈ Q, the language R_{q} is rational then it is defined by a local sentence ψ_{q} such that L_{≥ω}(ψ_{q}) = ∅. Again with the “ substitution method ”, we obtain a local sentence ψ_{α} such that L_{α}^{Σ}(ψ_{α}) = L_{α}(Aut).

6.5 Conclusion

We have proved in [FR96] the following:

Theorem 6.9 let φ be a local sentence with a symbol < in S(φ), and α be an ordinal such that ω ≤ α < ω^{ω}, has φ a well ordered model (for < ) of order type α? is a decidable problem.

The proof relies upon the existence of indiscernables in a model which reduces the existence of a model of order type α to the existence of a finite model of another local sentence which is effectively obtained from φ. The preceding method, which associates a local sentence to a Büchi αlanguage then allows to decide the emptiness problem for a Büchi α-language. The α-languages which are recognized by finite automata were first studied by Büchi in order to obtain a decision algorithm for the monadic theory of (α, <). The preceding result ( Theorem 6.9 ) allows to obtain a decision algorithm for the sentences in the form ∃R_{1}....∃R_{k}φ, where φ is local in the signature S(φ) = {<, R_{1}, ...R_{k}}, where R_{1}, ...R_{k} are relation or n-ary function symbols with n ≥ 1. Theorem 6.8 shows that this is actually an extension (for α < ω^{ω}) of Büchi’s result. In fact local α-languages extend far beyond Büchi α-languages: all Büchi ω-languages are, considering topological complexity, boolean combination of G_{δ}-sets, then Δ_{3}^{0}-sets, when there are local ω-languages in each Borel class Σ_{β}^{0}, for β an ordinal < ω^{2} and there are even some Σ_{1}^{1}-complete analytic local ω-languages, [Fin99]. Transfinite length word languages occur in the field of concurrency modelisation with the trace languages [DR95] and also in the work about timed automata where one consider that infinitely many actions may happen during a finite period [BP97] [AD94]. Beyond the decidability of the emptiness problem, we may hope to obtain other decidability results about Büchi α-languages, using results of model theory of local sentences, particularly some stretching theorems based upon the notion of indiscernables in a model [FR96].

In a second paper, we focus on local ω-languages, [Fin99]. We show that:

• Local ω-languages are neither closed under intersection nor under

complementation.

• Most undecidability results that hold for locally finite languages may be extended to locally finite ω-languages, in particular the inclusion, the equivalence problems are undecidable, as the problem of the rationality of a local ω-language is.

We then study topological properties of these languages, showing:

• There are local ω-languages in each Borel class of finite rank and even in Borel classes of infinite rank < ω^{2}.

• For any Borel class G, it is undecidable to determine whether a local ω-language is in the class G.

• There exist local ω-languages which are analytic but not Borel sets.

• One cannot decide whether a local ω-language is a Borel set.

Acknowledgments.

Thanks to the anonymous referee and to M. Nivat for useful comments on the preliminary version of this paper.

References

[ABB96] J-M. Autebert, J. Berstel and L. Boasson, Context Free Languages and Pushdown Automata, in Handbook of Formal Languages, Vol 1, Springer Verlag 1996.

[AD94] R. Alur and D. L. Dill, A Theory of Timed Automata, T.C.S. 126, p. 183-235, 1994.

[Bed96] N. Bedon, Finite Automata and Ordinals, T.C.S. 156, p. 119-144, 1996.

[Bed98] N. Bedon, Langages Reconnaissables de Mots Indexés par des ordinaux, Ph.d Thesis, Université de Marne la Vallée, January 1998.

[Ber79] J. Berstel, Transductions and Context Free Languages, Teubner Studienbücher Informatik, 1979.

[BP97] B. Bérard and C. Picarony, Accepting Zeno Words without Making Time Stand Still, Technical Report, L.S.V., CNRS URA 2236, ENS de Cachan, 1997.

[Büc60] J.R. Büchi, Weak Second Order Arithmetic and Finite Automata, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 6 (1960), pp 66-92.

[Büc62] J.R. Büchi, On a Decision Method in Restricted Second Order Arithmetic, Logic Methodology and Philosophy of Science, ( Proc. 1960 Int. Congr. ). Stanford University Press, 1962, 1-11.

[BS73] J.R. Büchi, D. Siefkes, The Monadic Second Order Theory of All Countable ordinals, Decidable Theories 2, 1973, S.L.N.M. , number 328.

[CK73] C.C. Chang and H.J. Keisler, Model Theory, American Elsevier Publishing Company, Inc, New York, 1973. ( North Holland, Amsterdam, 3rd ed., 1990).

[Cre73] J-P. Crestin, Langages Quasirationnels, In Langages Algébriques, Actes des premières journées d’informatique théorique Bonascre 1973, Ecole Nationale Supérieure de Techniques Avancées, Mars 1978.

[DR95] V. Diekert and G. Rozenberg, Editors. The Book of Traces, World Scientific, Singapore, 1995.

[EF95] H. D. Ebbinghaus and J. Flum, Finite Model Theory, Springer Verlag, New York, 1995.

[Eil74] S. Eilenberg, Automata, Languages and Machines, Vol. A, Academic Press, New York, 1974.

[Fag93] R. Fagin, Finite-Model Theory , A Personal Perspective, T.C.S. 116 (1993) p. 3-31.

[Fin89] O.Finkel, Langages de Büchi et ω-langages Locaux, C.R.A.S. Paris, t.309, Série 1, p. 991-994, 1989.

[Fin93] O.Finkel, Théorie des Modèles des Formules Locales et Etude des Langages Formels qu’ elles Definissent, Ph. D Thesis, University Paris 7, May 1993.

[Fin94] O.Finkel, Closure Properties of Locally Finite Omega Languages, preprint, 1994.

[Fin99] O. Finkel, Locally Finite Omega Languages, submitted to T.C.S., september 1999.

[FR96] O. Finkel and J-P. Ressayre, Stretchings, Journal of Symbolic Logic, Volume 61, number 2, Juin 1996, p. 563-585.

[FZV80] P. Franchi-Zanettacci and B. Vauquelin, Automates à Files, T.C.S. 11 (1980), p.221-225.

[Gin66] S. Ginsburg, The Mathematical Theory Of Context Free Languages, Mc Graw-Hill Book Company, New York, 1966.

[Hac98] Y. Hachaichi, Logic For Unambiguous Context Free Languages, submitted to C.S.L. 99.

[Hem92] J. C. Hemmer, Automates sur Mots de Longueur Supérieure à ω, Mémoire de Licence, Université de Liège, 1992.

[HU69] J.E. Hopcroft and J.D. Ullman, Formal Languages and their Relation to Automata, Addison-Wesley Publishing Company, Reading, Massachussetts, 1969.

[Imm87] N. Immerman, Languages That Capture Complexity Classes, SIAM J. of Computing 16:4 (1987), p. 347-354.

[Kas70] T. Kasai, An Hierarchy Between Context Free and Context Sensitive Languages, Journal of Computer and System Sciences, Vol 4, 1970, p.492-508.

[LT94] H. Lescow and W. Thomas, Logical specifications of infinite computations, In:”A Decade of Concurrency” (J. W. de Bakker et al., eds), Springer LNCS 803 (1994), 583-621.

[LST94] C. Lauteman, T. Schwentick and D. Therien, Logics for Context Free Languages, in C.S.L. 94, p. 205-216.

[Ogd69] W.F. Ogden, Intercalation Theorems for Pushdown Store and Stack Languages, Proceeding of the first ACM Symposium on Theory of Computing, 1969, p. 31-42.

[Par83] M. Parigot, Automates, Réseaux, Formules, in : Séminaire Général de Logique, 1983-1984, Publications Mathématiques de l’Université Paris 7.

[PP85] M. Parigot and E. Pelz, A Logical Approach of Petri Net Languages, T.C.S. 39 (1985) p. 155-169.

[PP98] D. Perrin and J.-E. Pin, Mots Infinis, Book in preparation, available from http://www.liafa.jussieu.fr/∼jep/synthese.html

[Pin96] J-E. Pin, Logic, Semigroups and Automata on Words, Annals of Mathematics and Artificial Intelligence 16 (1996), p. 343-384.

[Res88] J-P. Ressayre, Formal Languages defined by the Underlying Structure of their Words, Journal of Symbolic Logic, 53, number 4, December 1988, p. 1009-1026.

[Sch67] J.R. Schoenfield, Mathematical Logic, Addison-Wesley, Reading, MA, 1967.

[Sie65] W. Sierpinski, Cardinal and Ordinal Numbers, Polish Scientific Publisher, Varsovie, 1965.

[Sta97] L. Staiger, ω-languages, Chapter of the Handbbok of Formal languages, Vol 3, edited by G. Rozenberg and A. Salomaa, Springer-Verlag, Berlin.

[Tho90] W. Thomas, Automata on Infinite Objects, in: J. Van Leeuwen, ed., Handbook of Theorical Computer Science, Vol. B ( Elsevier, Amsterdam, 1990 ), p. 133-191.

[Tho96] W. Thomas, Languages, Automata and Logic, in Handbook of Formal Languages Theory, Vol 3, Edited by G. Rozenberg and A. Salomaa, Springer Verlag, 1996.