Pierre Pradic
email: pierre.pradic@ens-lyon.fr

Colin Riba
email: colin.riba@ens-lyon.fr

A Curry-Howard Approach to Church's Synthesis *

Keywords: 1998 ACM Subject Classification F.4.1 Mathematical Logic Keywords and phrases Intuitionistic Arithmetic, Realizability, Monadic Second-Order Logic on Infinite Words. Digital Object Identifier 10.4230/LIPIcs.FSCD.2017.29

Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, a non-classical subsystem of MSO, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model.

Introduction

Church's synthesis [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis[END_REF] consists in the automatic extraction of stream transducers (or Mealy machines) from input-output specifications, typically written in some subsystem of Monadic Second-Order Logic (MSO) over ω-words. MSO over ω-words is a decidable logic by Büchi's Theorem [START_REF] Büchi | On a Decision Methond in Restricted Second-Order Arithmetic[END_REF]. It subsumes non-trivial logics used in verification such as LTL (see e.g. [START_REF] Thomas | Languages, Automata, and Logic[END_REF][START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]).

Traditional approaches to synthesis (see e.g. [START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF]) are based, via McNaughton's Theorem [START_REF] Mcnaughton | Testing and generating infinite sequences by a finite automaton[END_REF], on the translation of MSO-formulae to deterministic automata on ω-words (such as Muller or parity automata) 1 . Such automata are then turned into game graphs, in which the Opponent O (∀bélard) plays input characters to which the Proponent P (∃loïse) replies with output characters. Solutions to Church's synthesis are then given by the Büchi-Landweber Theorem [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF], which says that in such games, either P or O has finite-state winning strategy.

Fully automatic approaches to synthesis suffer from prohibitively high computational costs, essentially for the following two reasons. First, the translation of MSO-formulae to automata is non-elementary, and McNaughton Theorem involves a non-trivial powerset construction (such as Safra construction, see e.g. [START_REF] Thomas | Languages, Automata, and Logic[END_REF][START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]). Second, similarly as with other automatic verification techniques based on Model Checking, the solution of parity games ultimately relies on exhaustive state exploration. While they have had (and still have) considerable success for verifying concurrency properties, such techniques hardly managed up to now to give practical algorithms for synthesis (even for fragments of LTL, see e.g. [START_REF] Bloem | Synthesis of reactive (1) designs[END_REF]). B ∈ 2 ω from input streams A ∈ 2 ω , the behavior (from [START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF]) expressed by

Φ(A, B) def. ⇐⇒    ∀n(A(n) = 1 =⇒ B(n) = 1) and ∀n(B(n) = 0 =⇒ B(n + 1) = 1) and (∃ ∞ n A(n) = 0) =⇒ (∃ ∞ n B(n) = 0) (1)
In words, the relation Φ(A, B) imposes B(n) ∈ 2 to be 1 whenever A(n) ∈ 2 is 1, B not to be 0 in two consecutive positions, and moreover B to be infinitely often 0 whenever A is infinitely often 0. We are interested in the realization of such specifications by finite-state stream transducers or Mealy machines.

Definition 2.1 (Mealy Machine).

A Mealy machine M with input alphabet Σ and output alphabet Γ (notation M : Σ → Γ) is given by a finite set of states Q with a distinguished initial state q ı ∈ Q, and a transition function

∂ : Q × Σ → Q × Γ.
We often write ∂ o for π 2 • ∂ : Q × Σ → Γ and ∂ * for the map Σ * → Q obtained by iterating ∂ from the initial state: ∂ * (ε) := q ı and ∂ * (a.a) := π 1 (∂(∂ * (a), a)).

A Mealy machine M : Σ → Γ induces a function F : Σ ω → Γ ω obtained by iterating ∂ o along the input:

F (B)(n) = ∂ o (∂ * (B n), B(n)).
Hence F can produce a length-n prefix of its output from a length-n prefix of its input. These functions are called synchronous.

Definition 2.2 (Synchronous Function).

A function F : Σ ω → Γ ω is synchronous if for all n ∈ N and all A, B ∈ Σ ω we have F (A) n = F (B) n whenever A n = B n. We say that a synchronous function F is finite-state if it is induced by a Mealy machine. such that F (B)(n + 1) = 1 iff B(n) = 1. (c) The Mealy machine depicted on Fig. 1 (right), taken from [START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF], induces a synchronous function which realizes the specification (1). (d) Synchronous functions are obviously continuous (taking the product topology on Σ ω and Γ ω , with Σ, Γ discrete), but there are continuous functions which are not synchronous, for instance the function P :

2 ω → 2 ω such that P (A)(n) = 1 iff A(n + 1) = 1.
For the definition and adequacy of our realizability interpretation, it turns out to be convenient to work with a category of finite-state synchronous functions.

Definition 2.4. Let M be the category whose objects are alphabets and whose maps from Σ to Γ are finite-state synchronous functions F : Σ ω → Γ ω .

Note that functions f : Σ → Γ induce M-maps [f] : Σ → M Γ. Also, M has finite products. Proposition 2.5. The category M has finite products. The product of Σ 1 , . . . , Σ n (for n ≥ 0) is given by the Set-product Σ 1 × • • • × Σ n (so that 1 is terminal in M).

::= x . = y | x ≤ y | S(x, y) | Z(x) | x ∈ X | | ⊥ Deterministic formulae: δ, δ ::= α | δ ∧ δ | ¬ϕ MSO formulae: ϕ, ψ ::= δ | ϕ ∧ ψ | ∃x ϕ | ∃X ϕ Figure 2
The Formulae of MSO.

Monadic Second-Order Logic (MSO) on Infinite Words. We consider a formulation of MSO based on a purely relational two-sorted language, with a specific choice of atomic formulae. There is a sort of individuals, with variables x, y, z, etc, and a sort of (monadic) predicates, with variables X, Y, Z, etc. Our formulae for MSO, denoted ϕ, ψ, etc are given on Fig. 2. They are defined by mutual induction with the deterministic formulae (denoted δ, δ , etc) from atomic formulae ranged over by α. MSO formulae are interpreted in the standard model N of ω-words as usual. Individual variables range over natural numbers n, m, . . . ∈ N and predicate variables range over sets of natural numbers A, B, . . . ∈ P(N) 2 ω . The atomic predicates are interpreted as expected: . = is equality, ∈ is membership, ≤ is the relation ≤ on N, S is the successor relation, and Z holds on n iff n = 0. We often write X(x) or even Xx for x ∈ X. As usual we let:

ϕ → ψ := ¬(ϕ ∧ ¬ψ) ϕ ∨ ψ := ¬(¬ϕ ∧ ¬ψ) ∀(-) ϕ := ¬∃(-) ¬ϕ
MSO on ω-words is known to be decidable by Büchi's Theorem [START_REF] Büchi | On a Decision Methond in Restricted Second-Order Arithmetic[END_REF].

Theorem 2.6 (Büchi [3]). MSO over N is decidable.

Following [START_REF] Büchi | On a Decision Methond in Restricted Second-Order Arithmetic[END_REF] (but see also e.g. [START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]), the (non-deterministic) automata method for deciding MSO proceeds by a recursive translation of MSO-formulae to Büchi automata. A Büchi automaton is a non-deterministic finite state automaton running on ω-words. Büchi automata are equipped with a set of final states, and a run on an ω-word is accepting if it has infinitely many occurrences of final states. The crux of Büchi's Theorem is the effective closure of Büchi automata under complement. Let us recall a few known facts (see e.g. [START_REF] Thomas | Languages, Automata, and Logic[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF]). First, the translation of MSO-formulae to automata is non-elementary. Second, its is known that deterministic Büchi automata are strictly less expressive than non-deterministic ones. Finally, it is known that complementation of Büchi automata is algorithmically hard: there is a family of languages (L n ) n>0 such that each L n can be recognized by a Büchi automaton with n + 2 states, but such that the complement of L n can not be recognized by a Büchi automaton with less than n! states.

Church's Synthesis for MSO. Church's synthesis problem for MSO is the following. Given as input an MSO formula ϕ(X; Y ) (where X = X 1 , . . . , X q and Y = Y 1 , . . . , Y p ), (1) decide whether there exist finite-state synchronous functions F = F 1 , . . . , F p : 2 q → M 2 such that N |= ϕ(A; F (A)) for all A ∈ (2 ω ) q (2 q ) ω , and (2), construct such F whenever they exist.

Example 2.7. The specification Φ displayed in (1) can be officially written in the language of MSO as the following formula φ(X; Y ) (where

∃ ∞ t ϕ(t) stands for ∀x∃t(t ≥ x ∧ ϕ(t))): φ(X; Y ) := ∀t (Xt → Y t) ∧ ∀t, t (S(t, t ) → ¬Y t → Y t ) ∧ [(∃ ∞ t ¬Xt) → (∃ ∞ t ¬Y t)]
Church's synthesis has been solved by Büchi & Landweber [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF], using automata on ω-words and infinite two-player games (a solution is also possible via tree automata [START_REF] Rabin | Automata on infinite objects and Church's Problem[END_REF]): there is an algorithm which, on input ϕ(X; Y ), (1) decides when a synchronous realizer of ϕ(X; Y ) exists, (2) provides a finite-state Mealy machine implementing it 4 , and (3) moreover provides a synchronous finite-state counter realizer (i.e. a realizer of ψ(Y ; X) := ¬ϕ(X; Y )) when no synchronous realizer of ϕ(X; Y ) exists.

The standard algorithm solving Church's synthesis for MSO (see e.g. [START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF]) proceeds via McNaughton's Theorem ( [START_REF] Mcnaughton | Testing and generating infinite sequences by a finite automaton[END_REF], see also e.g. [START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF][START_REF] Thomas | Languages, Automata, and Logic[END_REF]), which states that Büchi automata can be translated to equivalent deterministic finite state automata, but equipped with stronger acceptance conditions than Büchi automata. There are different variants of such conditions (Muller, Rabin, Streett or parity conditions, see e.g. [START_REF] Thomas | Languages, Automata, and Logic[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF]). All of them allow to specify which states an infinite run must not see infinitely often. For the purpose of this paper, we only need to consider the simplest of them, the Muller conditions. A Muller condition is given by a family of set of states T , and a run is accepting when the set of states occurring infinitely often in it belongs to the family T .

Theorem 2.8 (McNaughton [9]). Each Büchi automaton is equivalent to a deterministic Muller automaton.

There is a lower bound in 2 O(n) for the number of states of a Muller automaton equivalent to a Büchi automaton with n states. The best known constructions for McNaughton's Theorem (such as Safra's construction or its variants) give deterministic Muller automata with 2 O(n log(n)) states from non-deterministic Büchi automata with n states.

The standard solution to Church's synthesis for MSO starts by translating ϕ(X; Y ) to a deterministic Muller automaton, and then turns this deterministic automaton into a twoplayer sequential game, in which the Opponent ∀bélard plays inputs bit sequences in 2 p while the Proponent ∃loïse replies with outputs bit sequences in 2 q . The game is equipped with an ω-regular winning condition (induced by the acceptance condition of the Muller automaton). The solution is then provided by Büchi-Landweber's Theorem, which states that ω-regular games on finite graphs are effectively determined, and moreover that the winner always has a finite state winning strategy.

Example 2.9. Consider the last conjunct φ 2 [X, Y ] := (∃ ∞ t ¬Xt) → (∃ ∞ t ¬Y t) of the formula φ(X; Y ) of Ex. 2.7. When translating φ 2 to a finite state automaton, the positive occurrence of (∃ ∞ t ¬Y t) can be translated to a deterministic Büchi automaton. However, the negative occurrence of (∃ ∞ t ¬Xt) corresponds to (∀ ∞ t Xt) = (∃n ∀t ≥ n Xt) and can not be translated to a deterministic Büchi automaton. Even if a very simple two-state Muller automaton exists for (∀ ∞ t Xt), McNaughton's Theorem 2.8 is in general required for positive occurrences of the form ∀ ∞ t (-).

An Axiomatization of MSO. Our approach to Church's synthesis relies on the fact that the MSO-theory of N can be completely axiomatized as a subsystem of second-order Peano arithmetic [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF] (see also [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF]). We consider a specific set of axioms which consists of the rules depicted on Fig. 3 together with the following comprehension and induction rules

ϕ ϕ[ψ[y]/X] ϕ ∃X ϕ ϕ, Z(z) ϕ[z/x] ϕ, S(y, z), ϕ[y/x] ϕ[z/x] ϕ ϕ (2)
where z and y do not occur free in ϕ, ϕ, and where ϕ[ψ[y]/X] is the usual formula substitution, which commutes over all connectives (avoiding the capture of free variables), and with

(x ∈ X)[ψ[y]/X] = ψ[x/y]. ϕ t . = t ϕ ϕ[t/z] ϕ t . = u ϕ ϕ[u/z] ϕ x ≤ y ϕ y ≤ x ϕ x . = y ϕ x ≤ x ϕ S(x, y) ϕ x ≤ y ϕ x ≤ y ϕ y ≤ z ϕ x ≤ z ϕ, S(x,

A Synchronous Intuitionistic Restriction of MSO

We now introduce SMSO, an intuitionistic restriction of MSO. As expected, SMSO contains MSO via negative translation. But thanks to its vocabulary without primitive universals, SMSO actually admits a Glivenko Theorem, so that SMSO proves ¬¬ϕ whenever MSO ϕ. Moreover, SMSO is equipped with an extraction procedure which is sound and complete w.r.t. Church's synthesis: proofs of existential statements can be translated to finite state synchronous realizers, and such proofs exist for all solvable instances of Church's synthesis.

As it is common with intuitionistic versions of classical systems, SMSO has the same language as MSO, and its deduction rules are based on intuitionistic predicate calculus. Moreover, since (monadic) predicate variables are computational objects in our realizability interpretation, similarly as with higher-type Heyting arithmetic (see e.g. [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and their Use in Mathematics[END_REF]), SMSO has a comprehension scheme which corresponds to the negative translation of the full comprehension scheme of MSO5 . On the other hand, for the extraction of synchronous realizers from proofs, SMSO has a restricted induction scheme corresponding to the negative translation of the induction scheme of MSO. As a consequence, and in contrast with usual versions of intuitionistic (Heyting) arithmetic, this restricted induction scheme is not able to prove the elimination of double negation on atomic formulae. Fortunately, all atomic formulae of MSO can be interpreted by deterministic Büchi automata, and have a trivial computational content. This more generally leads to the notion of deterministic formulae (see Fig. 2), which contain negative formulae and atomic formulae. Deterministic formulae will be interpreted by deterministic (not nec. Büchi) automata, and have trivial realizers. We can therefore have as axiom the elimination of double negation for deterministic formulae, which are thus the SMSO counterpart of the formulae of Heyting arithmetic admitting elimination of double negation (see e.g. [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and their Use in Mathematics[END_REF]).

Furthermore, SMSO is equipped with a positive synchronous restriction of comprehension, which allows to have realizers for all solvable instances of Church's synthesis. The 29:7 synchronous restriction of comprehension asks the comprehension formula to be uniformly bounded in the following sense.

ϕ, ϕ ϕ ϕ ψ ϕ, ψ ϕ ϕ ϕ ϕ, ¬¬δ δ ϕ ϕ ϕ ¬ϕ ϕ ⊥ ϕ ⊥ ϕ ϕ ϕ ϕ ϕ ψ ϕ ϕ ∧ ψ ϕ ϕ ∧ ψ ϕ ϕ ϕ ϕ ∧ ψ ϕ ψ ϕ ϕ[y/x] ϕ ∃x ϕ ϕ ϕ[Y /X] ϕ ∃X ϕ ϕ, ϕ ψ ϕ ∃x ϕ ϕ ψ (x not free in ϕ, ψ) ϕ, ϕ ψ ϕ ∃X ϕ ϕ ψ (X not free in ϕ, ψ)
Definition 3.1. (i) Given MSO-formulae ϕ and θ and a variable y, the relativization of

ϕ to θ[y] (notation ϕ θ[y]
), is defined by induction on ϕ as usual:

α θ[y] := α (ϕ ∧ ψ) θ[y] := ϕ θ[y] ∧ ψ θ[y] (¬ϕ) θ[y] := ¬ϕ θ[y] (∃X ϕ) θ[y] := ∃X ϕ θ[y] (∃x ϕ) θ[y] := ∃x (θ[x/y] ∧ ϕ θ[y])
where, in the clauses for ∃, the variables x and X are assumed not to occur free in θ. Note that y does not occur free in

ϕ θ[y]. (ii) An MSO-formula φ is bounded by x if it is of the form ψ (y ≤ x)[y] (notation ψ [-≤ x]).
It is uniformly bounded if moreover x is the only free individual variable of φ.

As we shall see in §4.3, bounded formulae are exactly those definable in MSO over finite words. We are now ready to define the system SMSO.

Definition 3.2 (SMSO).

The logic SMSO has the same language as MSO. Its deduction rules are those given in Fig. 4 together with the rules of Fig. 3 and with the following rules of resp. negative comprehension, deterministic induction (where x and y do not occur free in ϕ, δ) and synchronous comprehension in which φ is uniformly bounded by y:

ϕ ψ[ϕ[y]/X] ϕ ¬¬∃X ψ ϕ, Z(z) δ[z/x] ϕ, S(y, z), δ[y/x] δ[z/x] ϕ δ ϕ ψ[ φ[y]/X] ϕ ∃X ψ
Remark. The axiom ϕ, ¬¬δ δ of double negation elimination for deterministic formulae would already be derivable in a version of SMSO where this axiom is weakened to double negation elimination for atomic formulae. We take ϕ, ¬¬δ δ as an axiom because it admits trivial realizers. Similarly, the cut rule is admissible, but we include it since we have a direct composition of realizers.

A Glivenko Theorem for SMSO. Thanks to its limited vocabulary, SMSO satisfies a Glivenko theorem, and thus a very simple negative translation from MSO. Glivenko's theorem is usually stated only for propositional logic, but can be extended to formulae containing existentials; the impossible case is the universal quantification. In particular, should one extend the logical constructs with universal quantification by freely adjoining them to SMSO, this would no longer hold. This would actually not be such a severe consequence since our results would also hold with a usual recursive negative translation instead of ¬¬(-). The Main Result. We are now ready to state the main result of this paper, which says that SMSO is correct and complete (w.r.t. its provable existentials) for Church's synthesis.

Theorem 3.4 (Main Theorem). Consider an MSO-formula ϕ(X; Y ).

(i) From a proof of ∃Y ¬¬ϕ(X; Y ) in SMSO, one can extract a finite-state synchronous realizer of ϕ(X; Y ). (ii) If ϕ(X; Y ) admits a (finite-state) synchronous realizer, then SMSO ∃Y ¬¬ϕ(X; Y ).

The correctness part (i) of Thm. 3.4 will be proved in §5 using a notion of realizability for SMSO based on automata and synchronous finite-state functions. The completeness part (ii) will be proved in §4.1, relying the completeness of the axiomatization of MSO (Thm. 2.10) together with the correctness of the negative translation ¬¬(-) (Thm. 3.3).

On the Representation of Mealy Machines in MSO

This section gathers several (possibly known) results related to the representation of Mealy machines in MSO. We begin in §4.1 with the completeness part of Thm. 3.4, which follows usual representations of automata in MSO (see e.g. [16, §5.3]). We then recall from [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF][START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF] the Recursion Theorem, which is a convenient tool to reason on runs of deterministic automata in MSO ( §4.2). In §4. We work with the following notion of representation.

Definition 4.1. Let ϕ be a formula with free variables among z, x 1 , . . . , x p , X 1 , . . . , X q . We say that ϕ z-represents F : 2 p × 2 q -→ M 2 if for all n ∈ N, all A ∈ (2 ω ) q , and all k ∈ (2 ω ) p such that k i ≤ n for all i ≤ p, we have

F (k, A)(n) = 1 iff N |= ϕ[n/z, k/x, A/X] (3)

Internalizing Mealy Machines in MSO

The completeness part (ii) of Thm. 3.4 relies on the following simple fact.

Proposition 4.2. For every finite-state synchronous F : 2 p -→ M 2, one can build a deterministic uniformly bounded formula δ[X, x] which x-represents F .

Proof. The proof is a simple adaptation of the usual pattern (see e.g. [16, §5.3]). Let F : 2 p → M 2 be induced by a Mealy machine M. W.l.o.g. we can assume the state set of M to be of the form 2 q . Then F is represented by a formula of the form

δ[X, x] := ∀Q, Y ∀t ≤ x(Z(t) → I[Q(t)]) ∧ ∀t, t ≤ x (S(t, t ) → H[Q(t), X(t), Y (t), Q(t )]) -→ Y (x) (4)
where X = X 1 , . . . , X p codes sequences of inputs, Y codes sequences of outputs, and where

Q = Q 1 , . . . , Q q codes runs.
Remark. In the proof of Prop. 4.2, since M is deterministic, we can assume the formula

I[Q(t)] to be of the form 1≤i≤q [Q i (t) ↔ B i ] with B i ∈ { , ⊥}, and, for some propositional formulae O[-, -], D[-, -], the formula H[Q(t), X(t), Y (t), Q(t )] to be of the form Y (t) ←→ O[Q(t), X(t)] ∧ 1≤i≤q Q i (t ) ←→ D i [Q(t), X(t)] ( 5
O[Q(t), X(t)] = D[Q(t), X(t)] = (¬Q(t) ∨ [Q(t) ∧ X(t)]) (6)
The completeness of our approach to Church's synthesis is obtained as follows.

Proof of Thm. 3.4.(ii). Assume that ϕ(X; Y ) admits a realizer C : 2 q -→ M 2 p . Using the Cartesian structure of M (Prop. 2.5), we assume

C = C = C 1 , . . . , C p with C i : 2 q → M 2. We thus have N |= ϕ[B/X, C(B)/Y ] for all B ∈ (2 ω ) q (2 q ) ω .
; Y ) = φ 0 [X, Y ] ∧ φ 1 [X, Y ] ∧ φ 2 [X, Y ] where φ 0 [X, Y ] := ∀t (Xt → Y t) φ 1 [X, Y ] := ∀t, t (S(t, t ) ∧ ¬Y t → Y t ) φ 2 [X, Y ] := (∃ ∞ t ¬Xt) → (∃ ∞ t ¬Y t)
Note that φ 0 and φ 1 are monotonic in Y , while φ 2 is anti-monotonic in Y . The formula φ 0 is trivially realized by the identity function 2 → M 2 (see Ex. 2.3.(a)), which is itself represented by the deterministic uniformly bounded formula δ 0 [X, x] := (x ∈ X). For φ 1 (which asks Y not to have two consecutive occurrences of 0), consider

δ 1 [X, x] := δ 0 [X, x] ∨ ∃t ≤ x[S(t, x) ∧ ¬X(t)] We have MSO φ 0 [X, δ 1 [x]/Y ] since δ 0 MSO δ 1 and moreover MSO φ 1 [X, δ 1 [x]/Y ] since S(t, t ) , ¬Xt , ¬∃u(S(u, t) ∧ ¬Xu) MSO Xt ∨ ∃t (S(t , t ) ∧ ¬Xt )
The case of φ 2 in Ex. 4.4 is more complex. The point is that φ 2 [δ 1 [x]/Y ] does not hold because if ∀ ∞ t ¬Xt (that is if X remains constantly 0 from some time on), then δ 1 will output no 1's. On the other hand, the machine of Ex. 2.3.(c) involves an internal state, and can be represented using a fixpoint formula of the form (4). Reasoning on such formulae is easier with more advanced tools on MSO, that we provide in §4.2.

The Recursion Theorem

Theorem 3.4.(ii) ensures that SMSO is able to handle all solvable instances of Church's synthesis, but it gives no hint on how to actually produce proofs. When reasoning on fixpoint formulae as those representing Mealy machines in Prop. 4.2, a crucial role is played by the Recursion Theorem for MSO [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF] (see also [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF]). The Recursion Theorem says that MSO allows to define predicates by well-founded induction w.r.t. the relation < defined as (x < y) := (x ≤ y ∧ ¬(x . = y)). Given a formula ψ and variables X and x, we say that ψ is x-recursive in X when the following formula Rec x X (ψ) holds:

Rec x X (ψ) := ∀z ∀Z, Z (∀y < z [Zy ←→ Z y] -→ [ψ[Z/X, z/x] ←→ ψ[Z /X, z/x]])
(where z, Z, Z do not occur free in ψ). For ψ[X, x] x-recursive in X, the Recursion Theorem says that, provably in MSO, the equation ∀x(Xx ←→ ψ[X, x]) has a unique solution.

F S C D 2 0 1 7

29:10

A Curry-Howard Approach to Church's Synthesis Theorem 4.5 (Recursion Theorem [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF]).

If MSO Rec x X (ψ) then ∀z Zz ←→ ∀X ∀x ≤ z(Xx ↔ ψ) -→ Xz MSO ∀x (Zx ←→ ψ[Z/X]) and ∀x(Zx ←→ ψ[Z/X]) , ∀x(Z x ←→ ψ[Z /X]) MSO ∀x (Zx ←→ Z x) Example 4.6. (a) W.r.t. the representation used in Prop. 4.2, let θ[X, Q, Y, x] be ∀t ≤ x(Z(t) -→ I[Q(t)]) ∧ ∀t, t ≤ x (S(t, t ) -→ H[Q(t), X(t), Y (t), Q(t )]) so that δ[X, x] = ∀Q, Y θ[X, Q, Y, x] → Y (x)
. The Recursion Theorem 4.5 implies that, provably in MSO, for all X there are unique predicates

Q, Y s.t. ∀x.θ[X, Q, Y, x].
Indeed, assuming I and H are as in [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis[END_REF] we have that θ

[X, Q, Y, x] is equivalent to θ o [Q, X, Y, x] ∧ 1≤i≤q θ i [Q, X, Y, x],
where

θ o [X, Q, Y, x] := ∀t ≤ x (Y i (t) ←→ O i [Q(t), X(t)]) θ i [X, Q, Y, x] := ∀t ≤ x (Q i (t) ←→ θi [Q, X, t]) with θi [X, Q, t] := (Z(t) ∧ B i ) ∨ ∃u ≤ t S(u, t) ∧ D i [Q(u), X(u)]
Now, apply Thm. 4. t) which itself can be derived using induction.

5 to O[Q(t), X(t)] (resp. θi ), which is t-recursive in Y (resp. in Q i ). (b)
δ 2 [X, x] := ∀Q, Y (θ[X, Q, Y, x] -→ Y (x)) It is not difficult to derive MSO φ 0 [δ 2 [x]/Y ]∧φ 1 [δ 2 [x]/Y ]. In order to show φ 2 [δ 2 [y]/Y ], one has to prove ∃ ∞ t (¬Xt) MSO ∃ ∞ t ∃Q, Y (θ[X, Q, Y, t] ∧ ¬Y t). Thanks to Thm. 4.5, this follows from ∀x.θ[X, Q, Y, x] , ∃ ∞ t (¬Xt) MSO ∃ ∞ t (¬Y

From Bounded Formulae to Mealy Machines

We now turn to a useful fact for part (i) of Thm. 3.4, namely, for synchronous comprehension, the extraction of finite-state synchronous functions from bounded formulae. This relies on the standard translation of MSO-formulae over finite words to DFA's (see e.g. [16, §3.1]). Lemma 4.7. Let φ be a formula with free variables among z, x 1 , . . . , x p , X 1 , . . . , X q , and which is bounded by z. Then φ z-represents a finite-state synchronous C : 2 p × 2 q → M 2 induced by a Mealy machine computable from φ.

Remark. Given

C : 2 p × 2 q → M 2 z-represented by ψ [-≤ z] (with z not free in ψ), for all n ∈ N, all A ∈ (2 ω ) q and all k ∈ (2 ω ) p with k i ≤ n, we have C(k, A)(n) = 1 if and only if k, A (n + 1) |= ψ (in the sense of MSO over finite words). It follows that if C is induced by a Mealy machine M = (Q, q ı , ∂), then with the DFA A := (Q × 2 + {q ı }, q ı , ∂ A , Q × {1}) where ∂ A (q ı , a) := ∂(q ı , a) and ∂ A ((q, b), a) := ∂(q, a), we have C(k, A)(n) = 1 iff

Internally Bounded Formulae

The synchronous comprehension scheme of MSO is motivated by Lem. 4.7, which tells that uniformly bounded formulae induce Mealy machines. However, being uniformly bounded may seem to be a strict syntactic requirement, and one may wish to relax synchronous comprehension to formulae which behave as bounded formulae, that is to formulae ψ[X, x] such that the following formula B x X (ψ[X, x]) holds (where z, Z, Z do not occur free in ψ):

B x X (ψ[X, x]) := ∀z∀ZZ (∀y ≤ z[Zz ←→ Z z] -→ [ψ[Z/X, z/x] ←→ ψ[Z /X, z/x]]) Theorem 4.9. If MSO B x X (ψ[X, x]
) and the free variables of ψ are among x, X, then there is a uniformly bounded formula φ[X, x] which is effectively computable from ψ and such that

MSO ∀X ∀x (ψ[X, x] ←→ φ[X, x]).
Remark. Theorem 4.9 relies on the decidability of MSO. Note that Thm. 4.9 in part. applies

if SMSO B x X (ψ[X, x]). Moreover, if ψ[X, x] is recursive (in the sense of §4.2), then B x X (ψ[X, x]
) holds, but not conversely.

The Realizability Interpretation of SMSO

This Section presents our realizability model for SMSO, and uses it to prove Thm. 3.4.(i).

Our approach to Church's synthesis via realizability uses automata in two different ways. First, from a proof D in SMSO of an existential formula ∃Y ϕ(X; Y ), one can compute a finite-state synchronous realizer F of ϕ(X; Y ). Second, the adequacy of realizability (and in particular the correctness of F w.r.t. ϕ(X; Y )) is proved using automata for ϕ(X; Y ) obtained by McNaughton's Theorem, but these automata do not have to be built concretely.

Uniform Automata

The adequacy of realizability will be proved using the notion of uniform automata (adapted from [START_REF] Riba | A Dialectica-Like Approach to Tree Automata[END_REF]). In our context, uniform automata are essentially usual non-deterministic automata, but in which non-determinism is expressed via an explicitly given set of moves. This allows a simple inheritance of the Cartesian structure of synchronous functions (Prop. 2.5), and thus to interpret the positive existentials of SMSO similarly as usual (weak) sums of type theory. In particular, the set of moves M (A) of an automaton A interpreting a formula ϕ will exhibit the strictly positive existentials of ϕ as M (A) = M (ϕ) where

M (α) M (¬ϕ) 1 M (ϕ ∧ ψ) M (ϕ) × M (ψ) M (∃(-) ϕ) 2 × M (ϕ) (7)

Definition 5.1 ((Non-Deterministic) Uniform Automata). A (non-deterministic) uniform automaton A over Σ (notation A : Σ) has the form

A = (Q A , q ı A , M (A) , ∂ A , Ω A ) (8)
where Q A is the finite set of states, q ı A ∈ Q A is the initial state, M (A) is the finite non-empty set of moves, the acceptance condition Ω A is an ω-regular subset of Q ω A , and the transition function ∂ A has the form

∂ A : Q A × Σ -→ M (A) -→ Q A A run of A on an ω-word B ∈ Σ ω is an ω-word R ∈ M (A) ω . We say that R is accepting (notation R A(B)) if (q k ) k∈N ∈ Ω A
for the sequence of states (q k ) k∈N defined as q 0 := q ı A and q k+1 := ∂ A (q k , B(k), R(k)). We say that A accepts B if there exists an accepting run of A on B, and we let L(A) be the set of ω-words accepted by A.

F S C D 2 0 1 7

Following the usual terminology, an automaton A as in ( 8) is deterministic if M (A) 1.

Let us now sketch how uniform automata will be used in our realizability interpretation of SMSO. First, by adapting to our context usual constructions on automata ( §5.2), to each MSO-formula ϕ with free variables among (say) X = X 1 , . . . , X q , we associate a uniform automaton ϕ over 2 q (Fig. 5). Then, from an SMSO-derivation D of a sequent (say) ϕ ψ (with free variables among X as above), we will extract a finite-state synchronous function

F D : 2 q × M ( ϕ ) -→ M M ( ψ ), such that F D (B, R)
ψ (B) whenever R ϕ (B). In the case of ∃Y φ(X; Y ), the finite-state realizer F D will be of the form C, G with C and G finite-state synchronous functions C : 2 q -→ M 2 and G : 2 q -→ M M (φ) such that G(B) φ (B, C(B)) for all B. This motivates the following notion.

Definition 5.2 (The Category Aut Σ ). For each alphabet Σ, the category Aut Σ , has automata A : Σ as objects. Morphisms F from A to B (notation A F : B) are finite-state synchronous maps

F : Σ × M (A) -→ M M (B) such that F (B, R) B(B) whenever R A(B).
Remark. (a) Note that if B F : A for some F , then L(B) ⊆ L(A). (b) One could also consider the category AUT Σ defined as Aut Σ , but with maps not required to be finite-state. All statements of this Section hold for AUT Σ , but for Cor. 5.10, which would lead to non necessarily finite-state realizers and would not give Thm. 3.4.(i). (c) Uniform automata are a variation of usual automata on ω-words, which is convenient for our purposes, namely the adequacy of our realizability interpretation. Hence, while it would have been possible to define uniform automata with any of the usual acceptance condition (see e.g. [START_REF] Thomas | Languages, Automata, and Logic[END_REF]), we lose nothing by assuming their acceptance condition to be given by arbitrary ω-regular sets.

Constructions on Automata

We gather here constructions on uniform automata that we will need to interpret MSO formulae. First, automata are closed under the following operation of finite substitution.

Proposition 5.3. Given A : Σ and a function f : Γ → Σ, let A[f] : Γ be the automaton identical to A, but with ∂

A[f] (q, b, u) := ∂ A (q, f(b), u). Then B ∈ L(A[f]) iff f • B ∈ L(A).
A × B := (Q A × Q B , (q ı A , q ı B ) , M (A) × M (B) , ∂ , Ω) where ∂((q A , q B ), a, (u, v)) := (∂ A (q A , a, u) , ∂ B (q B , a, v))
and where

(q n , q n ) n ∈ Ω iff ((q n ) n ∈ Ω A and (q n ) n ∈ Ω B )
. Note that Ω is ω-regular since Ω A and Ω B are ω-regular (see e.g. [START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]Ex. I.11.3.7]). Moreover,

L(I) = Σ ω and L(A × B) = L(A) ∩ L(B).
Uniform automata are equipped with the obvious adaptation of the usual projection on non-deterministic automata, which interprets existentials. Given a uniform automaton A : Σ × Γ, its projection on Σ is the automaton

(∃ Γ A : Σ) := (Q A , q ı A , Γ × M (A) , ∂ , Ω A ) where ∂(q, a, (b, u)) := ∂ A (q, (a, b), u) α x,X := A α [π] ¬ψ x,X := ∼ ψ x,X ∃X ψ x,X := ∃ 2 ( ψ x,X,X ) ψ 1 ∧ ψ 2 x,X := ψ 1 x,X × ψ 2 x,X ∃x ψ x,X := ∃ 2 (Sing[π] × ψ x,x,X [π ])

The Realizability Interpretation

Consider a formula ϕ with free variables among x = x 1 , . . . , x p and X = X 1 , . . . , X q . Its interpretation ϕ x,X is the uniform automaton over 2 p × 2 q defined by induction over ϕ in Fig. 5, where A α is a deterministic uniform automaton for the atomic formula α, Sing : 2 is a deterministic uniform automaton accepting the B ∈ 2 ω P(N) such that B is a singleton, and π, π are suitable projections. We write ϕ when x, X are irrelevant or understood from the context. Note that the set of moves M (ϕ) of ϕ indeed satisfies [START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF], so in particular δ is deterministic for a deterministic δ. Moreover, as expected we get:

Proposition 5.8. Given an MSO-formula ϕ with free variables among x = x 1 , . . . , x p and X = X 1 , . . . , X q , for all k ∈ (2 ω ) p (2 p ) ω and all B ∈ (2 ω ) q (2 q ) ω , we have

(k, B) ∈ L( ϕ x,X ) iff N |= ϕ[k/x, B/X].
Let ϕ 1 , . . . , ϕ n , ϕ be MSO-formulae with free variables among x = x 1 , . . . , x p and X = X 1 , . . . , X q . Then we say that a synchronous function

F : 2 p × 2 q × M (ϕ 1 ) × • • • × M (ϕ n ) -→ M M (ϕ) realizes the sequent ϕ 1 , . . . , ϕ n ϕ (notation ϕ 1 , . . . , ϕ n F : ϕ or ϕ F : ϕ) if ϕ 1 x,X × • • • × ϕ n x,X F : ϕ x,X
Theorem 5.9 (Adequacy). Let ϕ, ϕ be MSO-formulae with variables among x, X. From an SMSO-derivation D of ϕ ϕ, one can compute an M-morphism

F D s.t. ϕ x,X F D : ϕ.
Proof. The proof is by induction on derivations. Note that if ϕ SMSO ϕ, then ϕ |= N ϕ. In part., for all rules whose conclusion is of the form ϕ δ with δ deterministic, it follows from Prop. 5.8 and ( 7) that the unique M-map with codomain M (δ) 1 (and with appropriate domain) is a realizer. A similar argument applies to the Ex Falso rule (elimination of ⊥), but in this case the realizer of ϕ ϕ is not canonical, and elimination of equality is direct from Prop. 5.8. Adequacy for synchronous comprehension is deferred to §5.3.1. As for the rules of Fig. 4, the first two rules follow from the fact that M is a category with finite limits (Prop. 2.5), and the rules for conjunction (resp. existentials) follow from Prop. 5.5 (resp. Prop. 5.6). It remains the rules ϕ ∃y Z(y) and ϕ ∃y S(x, y) of Fig. 3. For the latter, we use the Mealy machine depicted on Fig. 1

(i)). Given a derivation D in SMSO of ∃Y ϕ(X; Y ) with X = X 1 , . . . , X q and Y = Y 1 , . . . , Y p , we have F D = C, G where C = C 1 , . . . , C p with C i : 2 q -→ M 2 and N |= ϕ(B, C(B)) for all B ∈ (2 ω ) q (2 q ) ω .

Realization of Synchronous Comprehension

We now turn to the adequacy of the synchronous comprehension rule. It directly follows from the existence of finite-state characteristic functions for bounded formulae (Lem. 4.7) and from the following semantic substitution lemma, which allows, given a synchronous function C φ y-represented by φ, to lift a realizer of ψ[ φ[y]/Y ] into a realizer of ∃Y ψ. Lemma 5.11. Let x = x 1 , . . . , x p and X = X 1 , . . . , X q . Let φ be a formula with free variables among y, X, and assume that φ y-represents C φ : 2 q -→ M 2. Then for every MSO-formula ψ with free variables among x, X, there is a finite-state synchronous function

H ψ : M (ψ[ φ[y]/Y ]) -→ M M (ψ) such that for all k ∈ (2 ω ) p , all A ∈ (2 ω ) q and all R ∈ M (ψ) ω , we have R ψ[ φ[y]/Y ] x,X (k, A) =⇒ H ψ (R) ψ x,X,Y (k, A, C φ(A)) (9)
Adequacy of synchronous comprehension then directly follows.

Lemma 5.12. Let ψ with free variables among x, X, Y and let φ be a formula with free variables among y, X and which is uniformly bounded by y. Then there is a finite-state realizer ψ[ φ[y]/Y ] x,X F : ∃Y ψ, effectively computable from ψ and ϕ.

Proof. Let C φ satisfying (3) be given by Lem. 4.7, and let H ψ satisfying (9) be given by Lem. 5.11. It then directly follows from Prop. 5.6 and Len. 5.

11 that ψ[ φ[y]/Y ] x,X C φ • [π], H ψ • [π ] : ∃Y ψ,
where π, π are suitable projections.

Conclusion

In this paper, we revisited Church's synthesis via an automata-based realizability interpretation of an intuitionistic proof system SMSO for MSO on ω-words, and we demonstrated that our approach is sound and complete, in the sense of Thm. 3.4. As it stands, this approach must still pay the price of the non-elementary lower-bound for the translation of MSO formulae over finite words to DFA's (see the Remark after Lem. 4.7, §4.3) and the system SMSO is limited by its set of connectives and its restricted induction scheme.

Further Works. First, following the approach of [START_REF] Riba | A Dialectica-Like Approach to Tree Automata[END_REF], SMSO could be extended with primitive universal quantifications and implications as soon as one goes to a linear deduction system. In particular, primitive universals and implications would allow to extend the logic with atomic formulae for Mealy machines with defining axioms of the form (4). We expect this to give better lower bounds w.r.t. completeness (for each solvable instance of Church's synthesis, to provide proofs with realizers of a reasonable complexity). Among other outcomes of going to a linear deduction system, following [START_REF] Riba | A Dialectica-Like Approach to Tree Automata[END_REF] we expect similar proof-theoretical properties as with the usual Dialectica interpretation (see e.g. [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and their Use in Mathematics[END_REF]), such as realizers of linear Markov rules and choices schemes. On the other hand, we do not know yet if effective computations of modulus of uniform continuity could be pertinent for Church's synthesis (e.g.

for a non-linear Markov rule). Moreover, we expect that a linear variant of MSO on finite words could help (for some classes of formulae) to mitigate the Remark of §4.3. The case of induction is more complex. One possibility to have finite-state realizers for a more general induction rule would be to rely on saturation techniques for regular languages. Another possibility, which may be of practical interest, is to follow the usual Curry-Howard approach and allow possibly infinite-state realizers.

Another direction of future work is to incorporate specific reasoning principles on Mealy machines. For instance, a translation from (a subsystem of) [START_REF] Bonsangue | Coalgebraic logic and synthesis of Mealy machines[END_REF] could be interesting.

A Proofs of §2 (Church's Synthesis and MSO on Infinite Words)

Theorem 1.1 (Thm. 2.10). The theory of MSO over N is completely axiomatized by deduction in classical two-sorted predicate logic with the axioms of Fig. 3 and the folllowing comprehension and induction rules (where z and y do not occur free in ϕ, ϕ):

ϕ ϕ[ψ[y]/X] ϕ ∃X ϕ ϕ, Z(z) ϕ[z/x] ϕ, S(y, z), ϕ[y/x] ϕ[z/x] ϕ ϕ
where ϕ[ψ[y]/X] is the usual formula substitution, which commutes over all connectives (avoiding variable capture), and with

(x ∈ X)[ψ[y]/X] = ψ[x/y].
The difference between [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF] and the present system is that the axiomatization of [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF] is expressed in terms of the < relation and that comprehension is formulated in the usual way with the following axiom scheme (where X is not free in ϕ):

∃X∀x (X(x) ←→ ϕ[x/y]) (10)
We thus proceed to show that we can bridge these gaps.

Let us first recapitulate the non-logical axioms of MSO (omitting equality):

(i) ≤ is a partial order:

ϕ x ≤ x ϕ x ≤ y ϕ y ≤ z ϕ x ≤ z ϕ x ≤ y ϕ y ≤ x ϕ x . = y (ii) Basic
∀x (ϕ[x/y] ←→ ϕ[x/y]) = ∀x (X(x) ←→ ϕ[x/y]) [ϕ[y]/X]
we have

∀x (ϕ[x/y] ←→ ϕ[x/y]) ∃X∀x (X(x) ←→ ϕ[x/y])
Arithmetic axioms. Concerning the arithmetic axioms of [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF], let

(x < y) := x ≤ y ∧ ¬(x . = y)
We have to check that S(-, -) is indeed a successor in the sense of [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF], that is ∀x, y [S(x, y) ←→ (x < y ∧ ¬∃z(x < z < y))]

Moreover, we have to show the linear order axioms

¬(x < x) (x < y < z → x < z) (x < y ∨ x . = y ∨ y < x)
as well as the predecessor and unboundeness axioms ∀x [∃y(y < x) → ∃yS(y, x)] ∀x∃y(x < y)

and the axiom of <-induction

∀X [∀x(∀y(y < x → X(y)) → X(x)) → ∀x X(x)]
We now proceed to derive a list of basic theorems following from our axiomatization (where refers to provability in this setting), from which the axioms of [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF] follow. Proof. The basic and arithmetic axioms above ensure that every x has a successor y, and that the successor satisfies x ≤ y. Thus, in combination with (c), we get that x < y. The base case Z[x] φ[x] follows from (f). For the induction step, we have to show

S(x, x ), φ[x] ∀y(x < y ∨ x . = y ∨ y < x )
By induction on y we show S(x, x ), φ[x] ψ [y, x ] where

ψ[y, x ] := x < y ∨ x . = y ∨ y < x
The base case follows again from (f). For the induction step, we have to show

S(x, x ), S(y, y ), φ[x], ψ[y, x ] ∀y(x < y ∨ x . = y ∨ y < x )
and we are done since (j) gives ∀x, x , y, y (x < y → S(x, x ) → S(y, y ) → x < y )

F S C D 2 0 1 7 (m) ∀x, y [S(x, y) ←→ (x < y ∧ ¬∃z(x < z < y))]
Proof. For the left-to-right direction, thanks to (c) we are left to show S(x, y), x < z, z < y ⊥ Assume that y is the successor of x and an intermediate z such that x < z < y (in particular, we have x < y by (b)). By (j), y ≤ z. But then it means that z = y by z ≤ y by antisymmetry, which is contradictory. Conversely, assume that x < y without any intermediate z. Assume ¬S(x, y) towards a contradiction. But there exists some z such that S(x, z). Clearly, x < z by (c). But we also have z ≤ y by (i) and ¬y . = z by assumption, so z < y. This contradicts our assumption of non-existence of intermediate z.

The linear order axioms ((a), (b), (l)), the successor axiom (m), the unboundedness (d) and predecessor (k) axioms are thus proved in our axiomatic. Finally, we have to prove that induction w.r.t. < (also called strong induction) is derivable:

∀X [∀x(∀y(y < x → X(y)) → X(x)) → ∀x X(x)]
The proof holds no surprise.

Proof. We have to show

∀x(∀y(y < x → X(y)) → X(x)) ∀x X(x) By induction on x we show ∀x(∀y(y < x → X(y)) → X(x)) φ[x]
where φ[x] := ∀y(y ≤ x → X(y))

The base case

∀x(∀y(y < x → X(y)) → X(x)), Z(x) φ[x]
is trivial since by (f),

Z(x) ¬∃y(y < x)

For the induction step, we have to show

∀x(∀y(y < x → X(y)) → X(x)), S(x, x ), φ[x], z ≤ x X(z)
Notice that φ[x] is equivalent to φ [x ] := ∀y(y < x → X(y)) using (k). Using trichotomy (l), we have three subcase according to:

z < x ∨ z . = x ∨ x < z
The first case enables to use φ [x ] directly, and the second requires to use the hypothesis of <-induction ∀x(∀y(y < x → X(y)) → X(x) together with φ [x ]. The last one leads to a contradiction using antisymmetry of ≤ together with z < x = z ≤ x ∧ ¬z . = x .

B Proofs of §3 (A Synchronous Intuitionistic Restriction of MSO)

Theorem 2.1 (Thm. 3.3). If MSO ϕ then SMSO ¬¬ϕ.

Proof. Induction over a derivation ϕ ϕ in MSO will prove ϕ ¬¬ϕ (which is equivalent to ¬¬ϕ ¬¬ϕ).

The cases of propositional connectives are standard (usual Glivenko's theorem). The cases of existential quantifications are explicited on Fig. 6 (top and middle). The comprehesion rule of MSO (which behaves as an extended rule of ∃-introduction) requires a bit reworking of the rule for the introduction of existentials with the double-negated version of comprehension of SMSO. It is detailed on Fig. 6 (bottom).

We now turn to the rules of Fig. 3. Most of these rules only involve sequents of the form ϕ δ where δ is deterministic. Such rules are handled using the rule ϕ, ¬¬δ δ of SMSO. The other rules on Fig. 3 are

ϕ ϕ[t/z] ϕ t . = u ϕ ϕ[u/z] ϕ ∃y Z(y) ϕ ∃y S(x, y)
Their cases follow from the fact that ϕ, ϕ SMSO ¬¬ϕ and the fact that ϕ SMSO δ whenever ϕ SMSO ¬¬δ.

Finally, the induction rule of MSO follows from the fact that ¬¬ϕ is deterministic.

C Proofs of §4 (On the Representation of Mealy Machines in MSO)

C.1 From Bounded Formulae to Mealy Machines Lemma 3.1 (Lem. 4.7). Let φ be a formula with free variables among z, x 1 , . . . , x p , X 1 , . . . , X q , and which is bounded by z. Then φ z-represents a finite-state synchronous function C : 2 p × 2 q -→ M 2 induced by a Mealy machine computable from φ.

Proof. First, given an MSO-formula φ with free variables among z, x 1 , . . . , x p , X 1 , . . . , X q , if φ is bounded by z then φ is of the form ψ [-≤ z], where the free variables of ψ are among z, x 1 , . . . , x p , X 1 , . . . , X q . But note that ψ

[-≤ z] is equivalent to the formula (∃t(last[t] ∧ ψ[t/z])) [-≤ z],
where last[t] := ∀x(t ≤ x → t . = x) and where t does not occur free in ψ. We can therefore assume that φ is of the form ψ [-≤ z] where ψ has free variables among x 1 , . . . , x p , X 1 , . . . , X q .

Then, for all n ∈ N, all A ∈ (2 ω ) q and all k ∈ (2 ω ) p with k i ≤ n, we have N |= ψ[k/x, A/X] [-≤ n] if and only if the formula ψ holds (in the sense of MSO over finite words) in the finite word k, A (n + 1) . Let A = (Q, q ı , ∂, F ) be a DFA recognizing the language of finite words satisfying ψ [START_REF] Thomas | Languages, Automata, and Logic[END_REF]Thm. 3.1]. Consider the Mealy machine M = (Q, q ı , ∂ M ) with ∂ M (q, a) = (q , b) where q = ∂(q, a) and (b = 1 iff q ∈ F ), and let C : 2 p × 2 q -→ M 2 be the function induced by M. We then have

D.3 Automata for Atomic Fomulae

We give below the automaton Sing (of §5.3) and automata for the atomic formulae of MSO. These automata are presented as deterministic Büchi automata (with accepting states circled). As uniform automata, each of them has set of moves 1. Note that automata for atomic formulae involving individual variables do not detect if the corresponding inputs actually represent natural numbers. This is harmless, since all statments of §5 actually assume streams representing natural numbers to be singletons, and since in Fig. 5

Figure 1

 1 Figure 1 Examples of Mealy Machines (where a transition a|b outputs b from input a).

Example 2 . 3 .

 23 (a) The identity function Σ ω → Σ ω is induced by the Mealy machine with state set 1 = {•} and identity transition function ∂ : (•, a) -→ (•, a). (b) The Mealy machine depicted on Fig. 1 (left) induces a synchronous function F : 2 ω → 2 ω

F

Figure 4

 4 Figure 4 Logical Rules of SMSO (where δ is deterministic).

Theorem 3 . 3 .F

 33 If MSO ϕ, then SMSO ¬¬ϕ.

) 29: 9 Example 4 . 3 .

 943 The function induced by the Mealy machine of Ex. 2.3.(c) (depicted on Fig. 1, right), is represented by a formula of the form (4), where Q = Q (since the machine has state set 2), X = X, where I[-] := [(-) ↔ ⊥] (since state 0 is initial) and

  A accepts the finite word k, A (n + 1) . Hence M must pay the price of the non-elementary lowerbound for translating MSO-formulae over finite words to DFAs (see e.g.[START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF] Chap. 13]).

Example 4 . 8 .

 48 Recall the continuous but not synchronous function P of Ex. 2.3.(d). The function P can be used to realize a predecessor function, and thus is represented (in the sense of (3)) by a formula ϕ[X, Y, x] such that N |= ϕ[A, B, n] iff A = {k + 1} and B = {k} for some k ≤ n. But ϕ is not equivalent to a bounded formula, since by Lem. 4.7 bounded formulae represent synchronous functions.

Example 5 . 4 .Proposition 5 . 5 .

 5455 Assume A interprets a formula ϕ with free variables among X, so thatB ∈ L(A) iff N |= ϕ[B/X].Then ϕ is also a formula with free variables among X, Y , and we haveBB ∈ L(A[π]) iff N |= ϕ[B/X/B /Y ], where π : X × Y → X is a projection.The Cartesian structure of M lifts to Aut Σ . This gives the interpretation of conjunctions. For each Σ, the category Aut Σ has finite products. Its terminal object is the automaton I = (1, •, 1, ∂ I , 1 ω ), where ∂ I (-, -, -) = •. Binary products are given by

Figure 5 Proposition 5 . 6 . 8 . 5 . 7 .

 556857 Figure 5 Interpretation of MSO-Formulae as Uniform Automata.

F 14 A

 14 (left) (Ex. 2.3.(b)) together with the fact that S(-, -) is deterministic. The case of the former is similar and simpler. Curry-Howard Approach to Church's Synthesis Adequacy of realizability, together with Prop. 5.6, directly gives Thm. 3.4.(i). Corollary 5.10 (Thm. 3.4.

  Z and S axioms (total injective relations): ϕ ∃y Z(y) ϕ ∃y S(x, y) ϕ, S(y, x), S(z, x) y . = z ϕ, Z(x), Z(y) x . = y ϕ, S(x, y), S(x, z) y . = z (iii) Arithmetic axioms: ϕ, S(x, y), Z(y) ⊥ ϕ S(x, y) ϕ x ≤ y ϕ, S(y, y ), x ≤ y , ¬(x . = y ) x ≤ y Comprehension. The comprehension scheme of the present version of MSO directly implies (10); indeed, using

  (a) ¬(x < x) Proof. From reflexivity of equality. (b) x < y, y < z < z Proof. We have x < y, y < z x ≤ z and x < y, y < z, x . = z ⊥ by the partial order axioms for ≤. (c) S(x, y), x . = y ⊥ Proof. By induction on y, we show φ[y] := ∀x(S(x, y) → ¬(x . = y)) We have Z(y) φ[y] by the first arithmetic axiom. We now show φ[y], S(y, y ) φ[y ], that is φ[y], S(y, y ), S(x, y ), x . = y ⊥ Note that S(y, y ), S(x, y ), x . = y x . = y ∧ y . = y ∧ S(x, y) From which follows that φ[y], S(y, y ), S(x, y ), x . = y ⊥ (d) ∀x∃y x < y.

F

  (e) S(y, y ), x ≤ y, x . = y ⊥ y ), x ≤ y, x . = y y ≤ y and by the partial order axioms for ≤ together with the second arithmetic axiom, we have S(y, y ), x ≤ y, x . = y y . = y and we conclude by (c).(f) Z(x) x ≤ y Proof. By induction on y.(g) x ≤ y, Z(y) Z(x)Proof. By (f), we have Z(y) y ≤ x and we conclude by the partial order axioms for ≤.(h) ∀y(x ≤ y) Z(x)Proof. We have∀y(x ≤ y), Z(z) x ≤ zHence by (g) we get∀y(x ≤ y), Z(z) Z(x)and we conclude by the basic axioms for Z.(i) x < y, S(x, x ) x ≤ y Proof. By induction on y, we showφ[y] := ∀x, x x < y → S(x, x ) → x ≤ yFirst, the base case Z(y) φ[y] follows from the fact that Z(y), x < y ⊥ by (g). For the induction step, we showS(y, y ), φ[y], x < y , S(x, x ) x ≤ yWe use the excluded middle on x . = y, and we are left to showS(y, y ), φ[y], x < y , ¬(x . = y), S(x, x ) x ≤ yBut by the arithmetic axioms, S(y, y ), x < y x ≤ y, so thatS(y, y ), φ[y], x < y , ¬(x . = y), S(x, x ) x < y But φ[y], x < y, S(x, x ) x ≤ yand we are done. (j) x ≤ y, S(x, x ), S(y, y ) x ≤ y Proof. By induction on z we show φ[z] := ∀x, x , y x ≤ y → S(x, x ) → S(y, z) → x ≤ z We trivially have Z(z) φ[z]. We now show S(z, z ), φ[z] φ[z ], that is S(z, z ), φ[z], x ≤ y, S(x, x ), S(y, z ) x ≤ z By the basic Z and S axioms, this amounts to show φ[z], x ≤ z, S(x, x ), S(z, z ) x ≤ z Now, using the excluded middle on x . = z, we are left with showing φ[z], S(x, x ), S(z, z ), x < z x ≤ z But by (i) we have x < z, S(x, x ) x ≤ z and we are done. (k) ∀x∀y y < x ←→ ∃z(y ≤ z ∧ S(z, x)) Proof. The right-to-left direction follows from (c). For the left-to-right direction, by induction on x, we show φ[x] := ∀y y < x → ∃z(y ≤ z ∧ S(z, x)) For the base case Z(x) φ[x], by (g) we have Z(x), y ≤ x Z(y) and we conclude by the basic Z-axioms. For the induction step, we have to show S(x, x ), φ[x], y < x ∃z(y ≤ z ∧ S(z, x )) By the last arithmetic axiom, S(x, x ), y < x y ≤ x and we are done. (l) x < y ∨ x . = y ∨ y < x Proof. By induction on x, we show φ[x] := ∀y (x < y ∨ x . = y ∨ y < x)

1 FFigure 6 1 ) 4 . 4 (

 16144 Figure 6The cases of existential quantifications of Glivenko (Proof of Thm. 2.1)

6 4 11 5 6 14 A 16 B

 61161416 , MSOquantifications over individuals are relativized to Sing. On the Representation of Mealy Machines in MSO 8 4.1 Internalizing Mealy Machines in MSO . . . . . . . . . . . . . . . . . . . . . . 8 4.2 The Recursion Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3 From Bounded Formulae to Mealy Machines . . . . . . . . . . . . . . . . . . . 10 4.4 Internally Bounded Formulae . . . . . . . . . . . . . . . . . . . . . . . . . . . The Realizability Interpretation of SMSO 11 5.1 Uniform Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 5.2 Constructions on Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 5.3 The Realizability Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.3.1 Realization of Synchronous Comprehension . . . . . . . . . . . . . . . 14 Conclusion Proofs of §2 (Church's Synthesis and MSO on Infinite Words) Proofs of §3 (A Synchronous Intuitionistic Restriction of MSO) 21 C Proofs of §4 (On the Representation of Mealy Machines in MSO) 21 C.1 From Bounded Formulae to Mealy Machines . . . . . . . . . . . . . . . . . . . 21 C.2 Internally Bounded Formulae . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 D Proofs of §5 (The Realizability Interpretation of SMSO) 25 D.1 Uniform Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 D.2 Constructions on Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 D.3 Automata for Atomic Fomulae . . . . . . . . . . . . . . . . . . . . . . . . . . 26 D.4 The Realizability Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . 27 D.4.1 Realization of Synchronous Comprehension . . . . . . . . . . . . . . . 27 F S C D 2 0 1 7

  Now, by Prop. 4.2 there are uniformly bounded (deterministic) formulae δ = δ 1 , . . . , δ p , with free variables among X, x, and such that (3) holds for all i = 1, . . . , p. It thus follows that N |= ∀Xϕ[δ[x]/Y ]. Then, by completeness (Thm. 2.10) we know that ϕ[δ[x]/Y ] is provable in MSO, and by negative translation (Thm. 3.3) we get SMSO ¬¬ϕ[δ[x]/Y ]. We can then apply (p times) the synchronous comprehension scheme of SMSO and obtain SMSO ∃Y ¬¬ϕ(X; Y ). Recall the specification (1) from [17], represented in MSO by the formula φ(X; Y ) of Ex. 2.7. Write φ(X

	Example 4.4.

  The machine of Ex. 2.3.(c) is represented as in (a) with O and D given by (6) (see Ex. 4.3, recalling that the machine as only two states). Hence MSO proves that for all X there are unique Q, Y such that ∀x.θ[X, Q, Y, x]. Continuing now Ex. 4.4, let

We thank the anonymous referee who urged us to state this explicitly.

We use the word realizer with two historically distinct meanings. In the context of Church's synthesis, a realizer of a ∀∃-formula is a transducer which witnesses the ∀∃ by computing an instantiation of the existential variables while reading input values for the universal variables (see e.g.[START_REF] Bloem | Synthesis of reactive (1) designs[END_REF]). In (constructive) proof theory, realizability is a relation between programs (the realizers) and formulae, usually defined by induction on formulae (see e.g.[START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and their Use in Mathematics[END_REF]). A realizer of a ∀∃-formula consists of a function witnessing the ∀∃, together with a realizer witnessing the correctness of that function.

It follows from the finite-state determinacy of ω-regular games that a finite-state synchronous realizer exists whenever a synchronous realizer exists (see e.g.[START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF]).F S C D 2 0 1 7

In contrast with Girard's System F[START_REF] Girard | Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d[END_REF], in which second-order variables have no computational content.

Acknowledgements. We thank the anonymous referees for helpful comments.

* This work was partially supported by the ANR-14-CE25-0007 -RAPIDO and the ANR-BLANC-SIMI-2-2011 -RECRÉ. † UMR 5668 CNRS ENS Lyon UCBL INRIA 1 A solution is also possible via tree automata [11].

C.2 Internally Bounded Formulae

We work in the standard model N of MSO. Our goal is to show Thm. 4.9, that if a formula ψ[X, x] can be proven to behave as a bounded formula (in the sense of B x X (ψ[X, x])) then ψ[X, x] is actually equivalent to a uniformly bounded formula.

In the following, we consider MSO-formulae over the vocabulary of [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF], that is MSOformulae given by the grammar

Following §A, defining the atomic formulae . =, S(-, -), ≤ and Z(-) as

x .

= y := ∀X (x ∈ X → y ∈ X) S(x, y) := (x < y ∧ ¬∃z(x < z < y)) x ≤ y := (x < y) ∨ (x . = y) Z(x) := ∀y (x ≤ y)

we obtain for each formula in the sense of Fig. 2 an equivalent formula in Λ. Moreover, we write FV ι (ϕ) for the set of free individual variables of the formula ϕ.

We shall make use of the following usual transfer property (see e.g. [START_REF] Riba | A model theoretic proof of completeness of an axiomatization of monadic secondorder logic on infinite words[END_REF]).

Lemma 3.2 (Transfer). Let ϕ ∈ Λ be a formula with free variables among x = x 1 , . . . , x p and X = X 1 , . . . , X q . Furthermore, let A ∈ 2 ω P(N) be non-empty. Then for all a 1 , . . . , a n ∈ A and all B ∈ (2 ω ) q we have

Lemma 3.3 (Splitting). Let ψ ∈ Λ be an MSO-formula and z be an individual variables. For every V ⊆ FV ι (ψ) with z ∈ V , one can produce natural number N ψ and two matching sequences of length N ψ of left formulae (L V (ψ) j ) j<N ψ and right formulae (R V (ψ) j ) j<N ψ sucht that the following holds:

If FV ι (ψ) = {x, z, y} with V = {x, z}, then for all n ∈ N, all a ≤ n and all b > n, we have

Proof. The proof proceeds by induction on ψ.

If ψ = x < y, then N ψ := 1. We define suitable left and right formulae according to V :

One of the produced formula is ψ and the other is according to whether x ∈ V or not. If ψ = ϕ ∨ φ, then it is clear that taking the concatenation of the sequences of formulae given by the induction hypothesis will be enough If ψ = ∃x.φ, using our induction hypothesis, we have N φ ∈ N and sequences of formulae

The disjunction is equivalent to ∃x.φ by making a case analysis over whether x ≤ n is true.

If ψ = ∃X.ϕ, then it directly follows from ( 11) that we can take L V (ψ

If ψ = ¬φ, using our induction hypothesis, we have a natural number N φ and two sequences of formulae

. Hence all we need to do is to add the negation, push it through the disjunction and convert the obtained CNF into a DNF. More explicitely (leaving the parameters implicit), we ¬φ ←→

Remark. Note that there is a combinatorial explosion in the case of ψ = ¬φ in Lem. 3.3 since N ¬φ = 2 N φ . It follows that the size of the formulae produced in Lem. 3.3 is nonelementary in the size of ψ.

We can now prove Thm. 4.9. Recall that

) then there is a uniformly bounded formula φ[X, x] which is effectivelly computable from ψ and such that

writting L j as a shorthand for L {x} (ψ(x, X)) j (and similarly for R j ). Then

Again using Lem. 3.2, we know that, for every j, R j (X(-)

where we set R j := R j (⊥). Lemma 3.2 moreover implies (since R j is a sentence and since

P. Pradic and C. Riba

29:25

But now, since R j is closed, it follows from the decidabiltiy of MSO (Thm. 2.6) that we can decide whether N |= R j or N |= ¬R j . It follows that our initial ψ is equivalent to the following formula, which is effectively computable from ψ:

where each R j is either or ⊥ according N |= R j or N |= ¬R j .

D Proofs of §5 (The Realizability Interpretation of SMSO)

D.1 Uniform Automata

We note the follwing simple fact, recorded in the Remark after Def. 5.2. Proof. Assume B F : A and B ∈ L(B) so that R (B) for some R ∈ M (B) ω . Then by definition of B F : A, we have F (B, R) A(B), so that B ∈ L(A).

D.2 Constructions on Automata

and where (q n , q n ) n ∈ Ω iff ((q n ) n ∈ Ω A and (q n ) n ∈ Ω B ). Note that Ω is ω-regular since Ω A and Ω B are ω-regular (see e.g. [START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]Ex. I.11.3.7]). Moreover, L(I) = Σ ω and L(A × B) = L(A) ∩ L(B).

Proof. The Cartesian structure is directly inherited from M and is omitted. Moreover, we obviously have

. The inclusion (⊆) follows from Lem. 4.1 applied to the projection maps A 1 × A 2 i : A i induced by the Catesian structure. For the converse inclusion (⊇), note that if

Proof. Consider a realizer B F : ∃ Γ A, for some B : Σ with set of moves V . Then F is a synchronous function from Σ ω × V ω to (Γ × U ) ω Γ ω × U ω , and is therefore given by a pair C, G of synchronous functions

Conversely, given C and G as in [START_REF] Riba | A Dialectica-Like Approach to Tree Automata[END_REF], if G(B, R) A( B,C(B,R) ) for all B ∈ A ω and all R B(B), then we have B C, G : ∃ Γ A. Proof. The proof is as usual by induction on derivations. Note that if ϕ SMSO ϕ, then ϕ |= N ϕ. So in particular, for all rules whose conclusion is of the form ϕ δ with δ deterministic, it follows from Prop. 5.8 and (7) that the unique M-map with codomain M (δ) 1 (and with appropriate domain) is a realizer. A similar argument also shows the adequacy of the Ex Falso rule (elimination of ⊥), but in this case the realizer of ϕ ϕ is not canonical. Adequacy for synchronous comprehension is defered to §5.3.1. Concerning the rules of Fig. 4, the first two rules follow from the fact that M is a category with finite limits (Prop. 2.5), and the rules for conjunction (resp. existentials) follow from Prop. 5.5 (resp. Prop. 5.6). It remains to deal with the rules ϕ ∃y Z(y) and ϕ ∃y S(x, y) of Fig. 3. For the latter, we use the Mealy machine depicted on Fig. 1 (left) (Ex. 2.3.(b)) together with the fact that S(-, -) is deterministic. The case of the former is similar and simpler.

D.4.1 Realization of Synchronous Comprehension

Lemma 4. 6 (Lem. 5.11). Let x = x 1 , . . . , x p and X = X 1 , . . . , X q . Let φ be a formula with free variables among y, X, and assume that φ y-represents C φ : 2 q -→ M 2. Then for all MSO-formula ψ with free variables among x, X, there is a finite-state synchronous function

Proof. By induction on ψ, we show [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF] and that for all k ∈ (2 ω ) p , and all A ∈ (2 ω ) q , we have

If ψ is an atomic formula not of the form (x ∈ Y ), then ψ[ φ[y]/Y ] = ψ. So we take the identity for H ψ and ( 14) and ( 15) are obvious.

If

Then by ( 3), for all k ∈ (2 ω ) p , and all A ∈ (2 ω ) q , we have

and it then follows from Prop. 5.8 that

from which we also get [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF].

If ψ is of the form ϕ 1 ∧ ϕ 2 (resp. ∃X ϕ, ∃x ϕ) then we conclude by induction hypothesis and Prop. 5.5 (resp. Prop. 5.6).

If ψ = ¬ϕ, then we have M (ψ) = M (ψ[ φ[y]/Y ]) = 1, and H ψ is the identity. Moreover, property [START_REF] Coq | The Coq Proof Assistant Reference Manual[END_REF] follows from the induction hypothesis and Prop. 5.7, and we thus also get [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF].

Lemma 4.7 (Lem. 5.12). Let ψ with free variables among x, X, Y and let φ be a formula with free variables among y, X and which is uniformly bounded by y. Then there is a finitestate realizer ψ[ φ[y]/Y ] x,X F : ∃Y ψ, effectivelly computable from ψ and ϕ.

Proof. Let C φ satisfying (3) be given by Lem. 4.7, and let H ψ satisfying (14) be given by Lem.