Localisation

Adresses

Aix-Marseille Université
Institut de Mathématiques de Marseille (I2M) - UMR 7373
Site Saint-Charles : 3 place Victor Hugo, Case 19, 13331 Marseille Cedex 3
Site Luminy : Campus de Luminy - Case 907 - 13288 Marseille Cedex 9

Séminaire

A linear monadic second-order logic over omega-words

Colin Riba
LIP, ÉNS Lyon
http://perso.ens-lyon.fr/colin.riba/

Date(s) : 15/12/2022   iCal
11h00 - 12h30

(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
I2M Luminy - Ancienne BU, Salle Séminaire2 (RdC)

Catégories


Secured By miniOrange