Colin Riba
LIP, ÉNS Lyon
http://perso.ens-lyon.fr/colin.riba/
Date(s) : 15/12/2022 iCal
11 h 00 min - 12 h 30 min
(j.w.w. P. Pradic)
We present LMSO, a linear logic-based variant of MSO over omega-words. LMSO can be seen as a logical syntax for a Curry-Howard-Lambek-like approach to automata, in which the latter are seen as objects and their runs (turned into appropriate simulation games) are morphisms. The specific design of these morphisms is motivated by two properties: (1) the extraction of existential witnesses in the positive (i.e. non-deterministic) case, and (2) a closed structure (i.e., given automata A and B, there is an automaton A -o B whose runs are exactly the morphisms from A to B). The resulting setting has inherent linearity constraints, which are reflected in the language and deduction rules of LMSO. Furthermore, we can give a syntactic characterization of those forall-exists sentences of LMSO which admit causal realizers (in the sense of Church’s synthesis). This relies on a form linear-causal choice which, via a complete axiomatization of MSO on omega-words, makes LMSO a complete linear logic with quantifiers. This theory is non-standard (i.e classically wrong) but consistent and with a meaningful computational interpretation.
Emplacement
Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)
Catégories