A Dialectica-Like Interpretation of a Linear MSO on Infinite Words

Monadic Second-Order Logic (\(\mathsf {MSO}\)) over \(\omega \)-words is a simple yet expressive language for reasoning on non-terminating systems which subsumes non-trivial logics used in verification such as \(\mathsf {LTL}\) (see e.g. [2, 30]). \(\mathsf {MSO}\) on \(\omega \)-words is decidable by Büchi’s Theorem [6] (see e.g. [24, 29]), and can be completely axiomatized as a subsystem of second-order Peano’s arithmetic [28]. While \(\mathsf {MSO}\) admits an effective translation to finite-state (Büchi) automata, it is a non-constructive logic, in the sense that it has true (i.e.provable) \(\forall \exists \)-statements which can be witnessed by no continuous stream function.

On the other hand, Church’s synthesis [8] can be seen as a decision problem for a strong form of constructivity in \(\mathsf {MSO}\). More precisely (see e.g. [12, 32]), Church’s synthesis takes as input a \(\forall \exists \)-formula of \(\mathsf {MSO}\) and asks whether it can be realized by a finite-state causal stream transducer. Church’s synthesis is known to be decidable since Büchi-Landweber Theorem [7], which gives an effective solution to \(\omega \)-regular games on finite graphs generated by \(\forall \exists \)-formulae. In traditional (theoretical) solutions to Church’s synthesis, the game graphs are induced from deterministic (say parity) automata obtained by McNaughton’s Theorem [19]. Despite its long history, Church’s synthesis has not yet been amenable to tractable solutions for the full language of \(\mathsf {MSO}\) (see e.g. [12]).

In recent works [25, 26], the authors suggested a Curry-Howard approach to Church’s synthesis based on intuitionistic and linear variants of \(\mathsf {MSO}\). In particular, [26] proposed a system based on (intuitionistic) linear logic [13], in which via a translation , the provable -statements exactly correspond to the realizable instances of Church’s synthesis. Realizer extraction for is done via an external realizability model based on alternating automata, which amounts to see every formula \(\varphi (a)\) as a formula of the form \((\exists u)(\forall x)\varphi _{\mathcal {D}}(u,x,a)\), where \(\varphi _{\mathcal {D}}\) represents a deterministic automaton.

In this paper, we use a variant of Gödel’s “Dialectica” functional interpretation as a syntactic formulation of the automata-based realizability model of [26]. Dialectica associates to \(\varphi (a)\) a formula \({\varphi ^D}(a)\) of the form \((\exists u)(\forall x){{\varphi }_D}(u,x,a)\). In usual versions formulated in higher-types arithmetic (see e.g. [1, 16]), the formula \({{\varphi }_D}\) is quantifier-free, so that \({\varphi ^D}\) is a prenex form of \(\varphi \). This prenex form is constructive, and a constructive proof of \(\varphi \) can be turned to a proof of \({\varphi ^D}\) with an explicit witness for \(\exists u\). Even if Dialectica originally interprets intuitionistic arithmetic, it is structurally linear, and linear versions of Dialectica were formulated at the very beginning of linear logic [21‐23] (see also [14, 27]).

We show that the automata-based realizability model of [26] can be obtained by a suitable modification of the usual linear Dialectica interpretation, in which the formula \({{\varphi }_D}\) essentially represents a deterministic automaton on \(\omega \)-words and is in general not quantifier-free, and whose realizers are exactly the finite-state accepting strategies in the model of [26]. In addition to provide a syntactic extraction procedure with internalized and automata-free correctness proof, this reformulation has a striking consequence, namely that there exists an extension \(\mathsf {LMSO}(\mathfrak C)\) of which is complete in the sense that for each closed formula \(\varphi \), it either proves \(\varphi \) or its linear negation \(\varphi \multimap \bot \). Since \(\mathsf {LMSO}(\mathfrak C)\) has realizers for all provable -statements, its completeness contrasts with the classical setting, in which due to provable non-constructive statements, one can not decide Church’s synthesis by only looking for proofs of \(\forall \exists \)-statements or their negations. Besides, \(\mathsf {LMSO}(\mathfrak C)\) has a linear choice axiom which is realizable in the sense of both \({(-)^D}\) and [26], but whose naive \(\mathsf {MSO}\) counterpart is false.

The paper is organized as follows. We present our basic setting in Sect. 2, with a particular emphasis on particularities of (finite-state) causal functions to model strategies and realizers. Our variant of Dialectica and the corresponding linear system are discussed in Sect. 3, while Sect. 4 defines the systems and \(\mathsf {LMSO}(\mathfrak C)\) and shows the completeness of \(\mathsf {LMSO}(\mathfrak C)\).

Alphabets (denoted \(\varSigma ,\varGamma ,\text {etc}\)) are finite non-empty sets of the form \(\mathbf {2}^p\) for some \(p \in \mathbb {N}\). We let . Note that alphabets are closed under Cartesian products and set-theoretic function spaces. It follows that taking , we have an alphabet \(\llbracket \tau \rrbracket \) for each simple type \(\tau \in \mathrm {ST}\), where

We often write \((\tau )\sigma \) for the type \(\sigma \rightarrow \tau \). Given an \(\omega \)-word (or stream) \(B\in \varSigma ^\omega \) and \(n \in \mathbb {N}\), we write \(B\mathord \upharpoonright n\) for the finite word \(B(0).\cdots .B(n-1) \in {\varSigma }^{*}\).

Church’s Synthesis and Causal Functions. Church’s synthesis consists in the automatic extraction of stream functions from input-output specifications (see e.g. [12, 31]). These specifications are in general asked to be \(\omega \)-regular, or equivalently definable in \(\mathsf {MSO}\) over \(\omega \)-words. In practice, proper subsets of \(\mathsf {MSO}\) (and even of \(\mathsf {LTL}\)) are assumed (see e.g. [5, 11, 12]). As an example, the relationwith input \(B\in \mathbf {2}^\omega \) and output \(C\in \mathbf {2}^\omega \) specifies functions \(F : \mathbf {2}^\omega \rightarrow \mathbf {2}^\omega \) such that \(F(B) \in \mathbf {2}^\omega \simeq \mathcal {P}(\mathbb {N})\) is infinite whenever \(B\in \mathbf {2}^\omega \simeq \mathcal {P}(\mathbb {N})\) is infinite (resp. the complement of \(B\) is finite). One may also additionally require to respect the transitions of some automaton. For instance, following [31], in addition to either case of (1) one can ask \(C\subseteq B\) and \(C\) not to contain two consecutive positions:In any case, the realizers must be (finite-state) causal functions. A stream function \(F : \varSigma ^\omega \rightarrow \varGamma ^\omega \) is causal (notation \(F:\varSigma \rightarrow _{\mathbb {S}} \varGamma \)) if it can produce a prefix of length n of its output from a prefix of length n of its input. Hence F is causal if it is induced by a map \(f : \varSigma ^+ \rightarrow \varGamma \) as follows:

The finite-state (f.s.) causal functions are those induced by Mealy machines. A Mealy machine \(\mathcal {M} : \varSigma \rightarrow \varGamma \) is a DFA over input alphabet \(\varSigma \) equipped with an output function \(\lambda : Q_{\mathcal {M}} \times \varSigma \rightarrow \varGamma \) (where \(Q_{\mathcal {M}}\) is the state set of \(\mathcal {M}\)). Writing \({\partial }^{*}: {\varSigma }^{*}\rightarrow Q_{\mathcal {M}}\) for the iteration of the transition function \(\partial \) of \(\mathcal {M}\) from its initial state, \(\mathcal {M}\) induces a causal function via .

Causal and f.s. causal functions form categories with finite products. Let \(\mathbb {S}\) be the category whose objects are alphabets and whose maps from \(\varSigma \) to \(\varGamma \) are causal functions \(F : \varSigma ^\omega \rightarrow \varGamma ^\omega \). Let \(\mathbb {M}\) be the wide subcategory of \(\mathbb {S}\) whose maps are finite-state causal functions.¹

The Logic \({{\mathbf {\mathsf{{MSO}}}}}\mathbf{(M). }\) Our specification language \(\mathsf {MSO}(\mathbf {M})\) is an extension of \(\mathsf {MSO}\) on \(\omega \)-words with one function symbol for each f.s. causal function. More precisely, \(\mathsf {MSO}(\mathbf {M})\) is a many-sorted first-order logic, with one sort for each simple type \(\tau \in \mathrm {ST}\), and with one function symbol of arity \((\sigma _1,\dots ,\sigma _n;\tau )\) for each map . A term \(\mathtt {t}\) of sort \(\tau \) (notation \(\mathtt {t}^\tau \)) with free variables among \(x_1^{\sigma _1},\dots ,x_n^{\sigma _n}\) (we say that \(\mathtt {t}\) is of arity \((\sigma _1,\dots ,\sigma _n;\tau )\)) thus induces a map . Given a valuation for \(i \in \{1,\dots ,n\}\), we then obtain an \(\omega \)-word\(\mathsf {MSO}(\mathbf {M})\) extends \(\mathsf {MSO}\) with \(\exists x^\tau \) and \(\forall x^\tau \) ranging over and with sorted equalities \(\mathtt {t}^\tau \doteq \mathtt {u}^\tau \) interpreted as equality over . Write \(\models \varphi \) when \(\varphi \) holds in this model, called the standard model. The full definition of \(\mathsf {MSO}(\mathbf {M})\) is deferred to Sect. 4.1.

An instance of Church’s synthesis problem is given by a closed formula \((\forall x^\sigma )(\exists u^\tau )\varphi (u,x)\). A positive solution (or realizer) of this instance is a term \(\mathtt {t}(x)\) of arity \((\sigma ;\tau )\) such that \((\forall x^\sigma )\varphi (\mathtt {t}(x),x)\) holds.

Proposition 1 implies that \(\mathsf {MSO}(\mathbf {M})\) proves the following equations:Hence each formula \(\varphi (a_1^{\sigma _1},\dots ,a_n^{\sigma _n})\) can be seen as a formula \(\varphi (a^{\sigma _1 \times \dots \times \sigma _n})\).

Eager Functions. A causal function \(\varSigma \rightarrow _{\mathbb {S}} \varGamma \) is eager if it can produce a prefix of length \(n+1\) of its output from a prefix of length n of its input. More precisely, an eager \(F : \varSigma \rightarrow _{\mathbb {S}} \varGamma \) is induced by a map \(f : {\varSigma }^{*}\rightarrow \varGamma \) asFinite-state eager functions are those induced by eager (Moore) machines (see also [11]). An eager machine \(\mathcal {E} : \varSigma \rightarrow \varGamma \) is a Mealy machine \(\varSigma \rightarrow \varGamma \) whose output function \(\lambda : Q_{\mathcal {E}} \rightarrow \varGamma \) is does not depend on the current input letter. An eager \(\mathcal {E} : \varSigma \rightarrow \varGamma \) induces an eager function via the map .

We write \(F : \varSigma \rightarrow _{\mathbb {E}} \varGamma \) when \(F : \varSigma \rightarrow _{\mathbb {S}} \varGamma \) is eager and \(F : \varSigma \rightarrow _{\mathbb {EM}} \varGamma \) when F is f.s. eager. All functions \(F : \varSigma \rightarrow _{\mathbb {M}} \mathbf {1}\), and more generally, constants functions \(F : \varSigma \rightarrow _{\mathbb {S}} \varGamma \) are eager. Note also that if \(F : \varSigma \rightarrow _{\mathbb {S}} \varGamma \) is eager, then \(F : \varSigma \rightarrow _{\mathbb {EM}} \varGamma \). On the other hand, if \(F : \varSigma \rightarrow _{\mathbb {EM}} \varGamma \) is induced by an eager machine \(\mathcal {E}\) then F is finite-state causal as being induced by the Mealy machine with same states and transitions as \(\mathcal {E}\), but with output function \((q,\mathsf {a}) \mapsto \lambda _{\mathcal {E}}(q)\).

Eager functions do not form a category since the identity of \(\mathbb {S}\) is not eager. On the other hand, eager functions are closed under composition with causal functions.

Isolating eager functions allows a proper treatment of strategies in games and realizers w.r.t. the Dialectica interpretation. Since \(\varSigma ^+ \rightarrow \varGamma \simeq {\varSigma }^{*}\rightarrow \varGamma ^\varSigma \), maps \(\varSigma \rightarrow _{\mathbb {E}} \varGamma ^\varSigma \) are in bijection with maps \(\varSigma \rightarrow _{\mathbb {S}} \varGamma \). This easily extends to machines. Given a Mealy machine \(\mathcal {M} : \varSigma \rightarrow \varGamma \), let \(\varvec{\varLambda }(\mathcal {M}) : \varSigma \rightarrow \varGamma ^\varSigma \) be the eager machine defined as \(\mathcal {M}\) but with output map taking \(q \in Q_{\mathcal {M}}\) to \((\mathsf {a} \mapsto \lambda _{\mathcal {M}}(q,\mathsf {a})) \in \varGamma ^\varSigma \).

Eager f.s. functions will often be used with the following notations. First, let \(@\) be the pointwise lift to \(\mathbb {M}\) of the usual application function \(\varGamma ^\varSigma \times \varSigma \rightarrow \varGamma \). We often write (F)G for \(@(F,G)\). Consider a Mealy machine \(\mathcal {M} : \varSigma \rightarrow \varGamma \) and the induced eager machine \(\varvec{\varLambda }(\mathcal {M}) : \varSigma \rightarrow \varGamma ^\varSigma \). We haveGiven \(F : \varGamma \rightarrow _{\mathbb {E}} \varSigma ^\varGamma \), we write \(\varvec{\mathrm {e}}(F)\) for the causal \(@(F(-),-) : \varGamma \rightarrow _{\mathbb {S}} \varSigma \). Given \(F : \varGamma \rightarrow _{\mathbb {S}} \varSigma \), we write \(\varvec{\varLambda }(F)\) for the eager \(\varGamma \rightarrow _{\mathbb {E}} \varSigma ^\varGamma \) such that \(F = \varvec{\mathrm {e}}(\varvec{\varLambda }(F))\). We extend these notations to terms.

Eager functions admit fixpoints similar to those of contractive maps in the topos of tree (see e.g. [4, Thm. 2.4]).

Games. Traditional solutions to Church’s synthesis turn specifications to infinite two-player games with \(\omega \)-regular winning conditions. Consider an \(\mathsf {MSO}(\mathbf {M})\) formula \(\varphi (u^\tau ,x^\sigma )\) with no free variable other than u, x. We see this formula as defining a two-player infinite game \(\mathcal {G}(\varphi )(u^\tau ,x^\sigma )\) between the Proponent \(\mathsf {P}\) (\(\exists \)loïse), playing moves in and the Opponent \(\mathsf {O}\) (\(\forall \)bélard), playing moves in . The Proponent begins, and then the two players alternate, producing an infinite play of the form

The play \(\chi \) is winning for \(\mathsf {P}\) if \(\varphi ((\mathsf {u}_k)_k,(\mathsf {x})_k)\) holds. Otherwise \(\chi \) is winning for \(\mathsf {O}\). Strategies for \(\mathsf {P}\) resp. \(\mathsf {O}\) in this game are functionsHence finite-state strategies are represented by f.s. eager functions. In particular, a realizer of \((\forall x^\sigma )(\exists u^\tau )\varphi (u,x)\) in the sense of Church is a f.s. \(\mathsf {P}\)-strategy inMost approaches to Church’s synthesis reduce to Büchi-Landweber Theorem [7], stating that games with \(\omega \)-regular winning conditions are effectively determined, and that the winner always has a finite-state winning strategy. We will use Büchi-Landweber Theorem in following form. Note that an \(\mathsf {O}\)-strategy in the game \(\mathcal {G}(\varphi )(u^\tau ,x^\sigma )\) is a \(\mathsf {P}\)-strategy in the game \(\mathcal {G}\big (\lnot \varphi (u,(x)u) \big )\big ( x^{(\sigma )\tau },u^\tau \big )\).

Curry-Howard Approaches. Following the complete axiomatization of \(\mathsf {MSO}\) on \(\omega \)-words of [28] (see also [26]), one can axiomatize \(\mathsf {MSO}(\mathbf {M})\) with a deduction system based on arithmetic (see Sect. 4.1). Consider an instance of Church’s synthesis \((\forall x^\sigma )(\exists u^\tau )\varphi (u,x)\). Then we get from Theorem 1 the alternativefor an eager term \(\mathtt {u}(x)\) or a causal term \(\mathtt {x}(u)\). By enumerating proofs and machines, one thus gets a (naive) syntactic algorithm for Church’s synthesis. But it seems however unlikely to obtain a complete classical system in which the provable \(\forall \exists \)-statements do correspond to the realizable instances of Church’s synthesis, because \(\mathsf {MSO}(\mathbf {M})\) has true but unrealizable \(\forall \exists \)-statements. Besides, note that

while it is possible both for realizable and unrealizable instances to haveIn previous works [25, 26], the authors devised intuitionistic and linear variants of \(\mathsf {MSO}\) on \(\omega \)-words in which, thanks to automata-based polarity systems, proofs of suitably polarized existential statements correspond exactly to realizers for Church’s synthesis. In particular, [26] proposed a system based on (intuitionistic) linear logic [13], such that via a translation , provable -statements exactly correspond to realizable instances of Church’s synthesis, while (4) exactly corresponds to alternatives of the formThis paper goes further. We show that the automata-based realizability model of [26] can be obtained in a syntactic way, thanks to a (linear) Dialectica-like interpretation of a variant of , which turns a formula \(\varphi \) to a formula \({\varphi ^D}\) of the form \((\exists u)(\forall x){{\varphi }_D}(u,x)\), where \({{\varphi }_D}(u,x)\) essentially represents a deterministic automaton. While the correctness of the extraction procedure of [25, 26] relied on automata-theoretic techniques, we show here that it can be performed syntactically. Second, by extending with realizable axioms, we obtain a system \(\mathsf {LMSO}(\mathfrak C)\) in which, using an adaptation of the usual Characterization Theorem for Dialectica stating that (see e.g. [16]), alternatives of the form (6) imply that for a closed \(\varphi \),where \((-) \multimap \bot \) is a linear negation. We thus get a complete linear system with extraction of suitably polarized \(\forall \exists \)-statements. Such a system can of course not have a standard semantics, and indeed, \(\mathsf {LMSO}(\mathfrak C)\) has a functional choice axiom

which is realizable in the sense of both \({(-)^D}\) and [26], but whose translation to \(\mathsf {MSO}(\mathbf {M})\) (which precludes (5)) is false in the standard model.

Gödel’s “Dialectica” functional interpretation associates to \(\varphi (a)\) a formula \({\varphi ^D}(a)\) of the form \((\exists u^{\tau })(\forall x^{\sigma }){{\varphi }_D}(u,x,a)\). In usual versions formulated in higher-types arithmetic (see e.g. [1, 16]), the formula \({{\varphi }_D}\) is quantifier-free, so that \({\varphi ^D}\) is a prenex form of \(\varphi \). This prenex form is constructive, and a constructive proof of \(\varphi \) can be turned to a proof of \({\varphi ^D}\) with an explicit (closed) witness for \(\exists u\). We call such witnesses realizers of \(\varphi \). Even if Dialectica originally interprets intuitionistic arithmetic, it is structurally linear: in general, realizers of contractiononly exist when the term language can decide \({{\varphi }_D}(u,x,a)\), which is possible in arithmetic but not in all settings. Besides, linear versions of Dialectica were formulated at the very beginning of linear logic [21‐23] (see also [14, 27]).

In this paper, we use a variant of Dialectica as a syntactic formulation of the automata-based realizability model of [26]. The formula \({{\varphi }_D}\) essentially represents a deterministic automaton on \(\omega \)-words and is in general not quantifier-free. Moreover, we extract f.s. causal functions, while the category \(\mathbb {M}\) is not closed. As a result, a realizer of \(\varphi \) is an open (eager) term \(\mathtt {u}(x)\) of arity \((\sigma ;\tau )\) satisfying \({{\varphi }_D}(\mathtt {u}(x),x)\). While it is possible to exhibit realizers for contraction on closed \(\varphi \) thanks to the Büchi-Landweber Theorem, this is generally not the case for open \(\varphi (a)\). We therefore resort to working in a linear system, in which we obtain witnesses for -statements (and thus for realizable instances of Church’s synthesis), but not for all \(\forall \exists \)-statements.

Fix a set of atomic formulae \(\mathrm {At}\) containing all \((\mathtt {t}^\tau \doteq \mathtt {u}^\tau )\), and a standard interpretation extending Sect. 2 for each \(\alpha \in \mathrm {At}\).

In Sect. 3 we devised a Dialectica-like \({(-)^D}\) providing a syntactic extraction procedure for -statements. In this Section, building on an axiomatic treatment of \(\mathsf {MSO}(\mathbf {M})\), we show that , an arithmetic extension of \(\mathsf {FS}+(\mathsf {LSIP})+(\mathsf {DEXP})+(\mathsf {PEXP})\) adapted from [26], is correct and complete w.r.t. Church’s synthesis, in the sense that the provable -statements are exactly the realizable ones. We then turn to the main result of this paper, namely the completeness of . We fix the set of atomic formulae

We provided a linear Dialectica-like interpretation of \(\mathsf {LMSO}(\mathfrak C)\), a linear variant of \(\mathsf {MSO}\) on \(\omega \)-words based on [26]. Our interpretation is correct and complete w.r.t. Church’s synthesis, in the sense that it proves exactly the realizable -statements. We thus obtain a syntactic extraction procedure with correctness proof internalized in \(\mathsf {LMSO}(\mathfrak C)\). The system \(\mathsf {LMSO}(\mathfrak C)\) is moreover complete in the sense that for every closed formula \(\varphi \), it proves either \(\varphi \) or its linear negation. While completeness for a linear logic necessarily collapse some linear structure, the corresponding axioms \((\mathsf {DEXP})\) and \((\mathsf {PEXP})\) do respect the structural constraints allowing for realizer extraction from proofs. The completeness of \(\mathsf {LMSO}(\mathfrak C)\) contrasts with that of the classical system \(\mathsf {MSO}(\mathbf {M})\), since the latter has provable unrealizable \(\forall \exists \)-statements. In particular, proof search in \(\mathsf {LMSO}(\mathfrak C)\) for -formulae and their negation is correct and complete w.r.t. Church’s synthesis. The design of the Dialectica interpretation also clarified the linear structure of , as it allowed us to decompose it starting from a system based on usual full intuitionistic linear logic (see e.g. [3] for recent references on the subject).

An outcome of witness extraction for \(\mathsf {LMSO}(\mathfrak C)\) is the realization of a simple version of the fan rule (in the usual sense of e.g. [16]). We plan to investigate monotone variants of Dialectica for our setting. Thanks to the compactness of \(\varSigma ^\omega \), we expect this to allow extraction of uniform bounds, possibly with translations to stronger constructive logics than .