AUTOMATA, WORDS AND LOGIC

Invited talk

Stephan Foldes, Boolean functions and finite functions
Tampere University of Technology

Recent and on-going research on Boolean functions and more general functions of several discrete variables will be discussed, including in particular results of Ekin, Hammer, Hellerstein, Pippenger, Pogosyan, Zverovich, and of Couceiro and Lehtonen in Tampere, and focusing mainly on the following aspects and topics:

(i) subfunctions (or minors);
(ii) function properties definable by relations and functional equations;
(iii) expressions of functions by formulas, efficiency of syntax;
(iv) closure conditions on function classes, and local character of function properties.

Contributions

Elena Czeizler, Intricacies of Word Equations
Department of Mathematics, University of Turku and Turku Centre for Computer Science, elenac(at)it.utu.fi

Although it is decidable whether or not a word equation is satisfiable, due to Makanin's results, the structure of all solutions in general is difficult to describe. In particular, it was proved by Hmelevskii that the solutions of xyz=zvx cannot be finitely parametrized, contrary to the case of equations in three unknowns. In this presentation we give a simple, necessary, non-sufficient condition for an equation to be nonparametrizable. Then, we give a short, elementary proof of Hmelevkii's result. We also discuss some problems related to systems of equations with three unknowns.

Eugen Czeizler, Jarkko Kari, A tight linear bound on the neighborhood of inverse cellular automata
Department of Mathematics, University of Turku, Finland, and Turku Centre for Computer Science, eugenc(at)cs.utu.fi
Department of Mathematics, University of Turku, and Department of Computer Science, University of Iowa, USA, jjkari(at)cs.uiowa.edu

Reversible cellular automata (RCA) are models of massively parallel computation that preserve information. They consist of an array of identical finite state machines that change their states synchronously according to a local update rule. By selecting the update rule properly the system has been made information preserving, which means that any computation process can be traced back step-by-step using an inverse automaton. We investigate the maximum range in the array that a cell may need to see in order to determine its previous state. We provide a tight upper bound on this inverse neighborhood size in the one-dimensional case: we prove that in a RCA with n states the inverse neighborhood is not wider than n-1, when the neighborhood in the forward direction consists of two consecutive cells. Examples are known where range n-1 is needed, so the bound is tight. If the forward neighborhood consists of m consecutive cells then the same technique provides the upper bound n^m-1-1 for the inverse direction.

Lauri Hella, Games for regular languages
University of Tampere

In this talk we study regular languages from the point of view of Abstract logic : regular expressions are considered as formulas, words as models, and the satisfaction relation |= is defined by the condition

w |= r ⇔ w is in the language denoted by the expression r.

We introduce a game theoretic semantics for this logic of regular languages. Furthermore, we show that there is a game theoretic characterization for the equivalence of words with respect to all expressions containing a fixed number of catenations and Kleene stars.

Jari Kivelä, Equational classes of Boolean functions and frame definability in modal logic
joint work with M.Couceiro and L.Hella at University of Tampere

Let B = {0, 1}. There is a canonical bijection between n-ary vector-valued Boolean functions Bⁿ → Bⁿ and set functions F: P(W) → P(W) where W an n-element set. This connection can be used in the study of a generalization of Kripke semantics for modal logic, so called Scott-Montague semantics. A Scott-Montague frame is a structure F = ⟨W, F⟩ where W is a non-empty set and F is a set function P(W) → P(W). As in Kripke semantics, we get a Scott-Montague model by assigning a valuation function V to a Scott-Montague frame. The truth conditions for modal formulas are defined recursively as in Kripke semantics, except for the modal operator □. Let M = ⟨W, F, V⟩ be a Scott-Montague model. Then

M, w |= □φ ⇔ w ∈ F(||φ||^M),

where ||φ||^M = {v ∈ W | M,v |= φ}.

Equational classes of Boolean functions are those which are definable by functional terms. In particular, Boolean clones (i.e. classes of Boolean functions closed under composition and containing all projections) are equational classes. Based on the connection between vector-valued Boolean functions and set functions, we can define a bijective translation between functional terms and modal formulas of specific form (uniform degree-1 formulas) in a way that the definability of Boolean functions by functional terms corresponds exactly to the frame definability of Scott-Montague frames by uniform degree-1 formulas.

We also show that several classes of Kripke frames correspond to classes of Scott-Montague frames "determined" by some Boolean clones.

Tomi Kärki, Transcendence of numbers with a low complexity expansion
Turku Centre for Computer Science and Department of Mathematics, University of Turku, topeka(at)utu

Let k ≥ 2 be an integer. We consider expansions of numbers in base k as infinite words and examine the relations between the subword complexity of the expansion and the trancendence of the corresponding number. It is conjectured that irrational algebraic number is normal in the sense that its expansion u contains every block of digits of length n with a frequency asymptotic to 1/kⁿ. Hence, the complexity function p_u(n) i.e. the number of factors of length n occurring in the word u is kⁿ. For rational numbers the expansion u in any base k is ultimately periodic, which is equivalent to the existence of a positive integer n such that p_u(n) ≤ n. Thus, between these extreme behaviours of complexity we ought to find "simple" non-ultimately periodic expansions corresponding to transcendental numbers.

In 1997 Ferenczi and Mauduit proved that numbers with an expansion u in base k of complexity p_u(n)=n+l-1, where 2 ≤ l ≤ k, are transcendental. Such expansions are called Sturmian words. The proof method of Ferenczi and Mauduit was based on the combinatorial translation of a number theoretical result of Ridout concerning rational approximations. With this criterion they were also able to prove the transcendence of numbers with Arnoux-Rauzy expansions, which form a subclass of sequences with complexity p_u(n)=2n+1. In 2004 the author extended their result to some other classes of complexity 2n+1. Recently, Adamczewski et al. obtained a new criterion for transcendence, which is based on the Schmidt Subspace Theorem. This powerful criterion implies many new transcendence results for expansions in base k as well as for continued fraction expansions. For example, Adamczewski et al. proved that all irrational numbers with an expansion in base k generated by a finite automaton are transcendental.

Andrea Meinander, A solution of the uniform word problem for ortholattices
University of Helsinki

Petri Salmela, Commutation of Languages and the Fixed Point Approach
Turku Centre for Computer Science and Department of Mathematics, University of Turku

The commutation equation uv=vu for two words is well known and has very clear and easy solution. Both words are powers of a common word. Commutation equation for two languages is however much more complicated. We focus on the maximal solution of the equation XY=YX, with fixed rational language X, and call this solution the centralizer of X. The centralizer can also be defined as the maximal fixed point of a certain language operator. In most cases the centralizer of given language is reached by iterating this operation. However, an infinite number of iterations might be needed. Even for finite languages.

Ryan Siders, Quantifier-rank levels in the theories of Linear Order and Wellorder
University of Helsinki

To each linear order L, there is a hierarchy of semi-models s(k,L), each of which is a finite ordered set whose domain has k nested subsets (one within the other). We say s |=^s.m. φ if φ holds, when any free variable of φ must be chosen from the innermost of the nested subsets of s; and any other variable, appearing within the scope of l-many quantifiers, must be chosen from the innermost l subsets of s. Ehrenfeucht proved that for any sentence φ of first order logic and of quantifier depth k, L |= φ iff s(k,L) |=^s.m. φ, i.e., the semi-models provide points and gaps which witness, in the sense of |=^s.m., the truth or falsehood of all k-quantifier sentences about the linear order. However, the decidability of Th(LO) was published by different authors, and the proof proceded by different means.

We define the word "left" in the sentence "φ talks about the left end of L." We prove equivalence between "φ(x) only describes the right end of L left of x and the left end of L right of x" and "φ describes x locally" in the sense in which locality for first-order logic has been widely studied. We construct semi-models s(k,L) for all linear orders L and to all depths k. We obtain previously unknown results about the first-order theory of linear orders, particularly: we construct piecewise-dense linear orders which form so dense a subset of Th(LO) that any sentence φ in Th(LO) is modeled by a piecewise-dense linear order, which is axiomatizable by an extension of φ using only one quantifier more than appears in φ. Previously, tower-of-exponential bounds have been discussed for the difference in quantifier depth between an arbitrary φ and its minimal complete extension. This bears heavily, of course, on the effectivity of the decision procedure for Th(LO).

To keep the talk interesting and brief, we will describe these results by comparing the differences between the k-quantifier theories of Wellorder and of Linear Order. Whereas a profluence of local types forces there to exist 2^{2^{2^...}} (in which the exponent 2 should be imagined to appear k-many times)-many ≢_k linear orders, the complete lack of interesting local types, other than those which can only appear on the ``right", leaves only 2^k²/4-many (ignoring the linear term in the exponent) ≢_k wellorders.

Anssi Yli-Jyrä, Some connections between theoretical computer science and linguistics
University of Helsinki

Finite automata are being applied extensively in natural language processing to produce efficient and simple algorithms. Sometimes these applications present challenges that are related to deep questions in formal language theory, as well as algorithmics.