Toward Curry-Howard Approaches to MSO and Automata on Infinite Words and Trees
Colin Riba · HAL (Le Centre pour la Communication Scientifique Directe) · 2019
We present works aiming at proposing a Curry-Howard approach to Monadic Second-Order Logic (MSO) on infinite trees and ω-words.Rabin’s Tree Theorem, the decidability of MSO over infinite trees, is a powerfull tool, which provided decidability proofs for many logics and mathematical theories. While the result dates back to the late 60’s, there have been since then considerable work on its proof, culminating in streamlined arguments based on a triangular correspondence between logics, automata, and infinite games.The goal of the works presented here is to revisit this correspondence from the perspective of the Curry-Howard proofs-as-programs correspondence. We propose a realizability model for (alternating) tree automata, based on usual categories of simple games, and following the slogan “automata as types, strategies as programs”. Within this model, we observe that natural oper- ations on automata used in the translations of MSO-formulae to automata underlying Rabin’s Tree Theorem correspond to connectives of intuitionistic (predicate) linear logic (ILL). In other words, the language of ILL reflects operations on alternating automata which are finer grained than the connectives of MSO. As a consequence, ILL can be used as an intermediate language between MSO and tree automata.When we restrict this model to the case of MSO over ω-words, one recovers the usual equiv- alence between determinisitc, non-deterministic, universal and alternating automata. Building on Siefkes’s complete axiomatization of MSO over ω-words as a subsystem of Second-Order Peano Arithmetic (PA2), we obtain, thanks to a variant of Gödel’s functional “Dialectica” inter- pretation, a complete, non-standard, linear logic LMSO(C), which, via a polarization policy, is sound and complete w.r.t. Church’s synthesis: there is a class of extractible ∀∃-statements whose provability exactly corresponds to the solvable instances of Church’s synthesis. We also briefely discuss questions related to the axiomatization of MSO on infinite trees, seen as a subsystem of PA2. By contrast, we see our results in this direction as being more preliminary.