Nous présentons des travaux ayant pour objectif de proposer une approche Curry-Howard à la Logique Monadique du Second-Ordre (MSO) sur les arbres infinis et les ω-mots.
Le Théorème de l’Arbre de Rabin, à savoir la décidabilité de MSO sur les arbres infinis, est un outil puissant, qui a fourni des arguments de décidabilité pour de nombreuses logiques et théories mathématiques. Alors que ce résultat date de la fin des années 60, il y a eu depuis un travail considérable sur sa preuve, aboutissant à des arguments basés sur une correspondance triangulaire entre logiques, automates et jeux infinis.
L’objectif des travaux présentés ici est de revisiter cette correspondance selon la perspective de la correspondance peuves-programmes de Curry-Howard. Nous proposons un modèle de réalisabilité pour des automates d’arbres alternants, dans lequel les automates sont assimilés à des types et les stratégies d’acceptation sont vues comme des programmes. Nous observons, à travers ce modèle, que les opérations naturelles sur les automates utilisées dans les traductions de formules MSO en automates sous-jacentes au théorème de Rabin correspondent à des connecteurs de la logique (des prédicats) linéaire intuitionniste (ILL). En d’autres termes, le langage de ILL reflète des opérations sur les automates alternants ayant un grain plus fin que les connecteurs de MSO. Ainsi, ILL peut-être utilisé comme un langage intermédiaire entre MSO et les automates d’arbres.
Lorsque l’on restreint ce modèle au cas des ω-mots, on retrouve les équivalences usuelles entre automates déterministes, non-déterministes, universels et alternants. En s’appuyant sur l’axiomatisation complète par Siefkes de MSO sur les ω-mots en un sous-système de l’arithmétique de Peano du second-ordre (PA2), nous obtenons, grâce à une variante de l’interprétation fonctionnelle « Dialectica » de Gödel, une logique linéaire LMSO(C) complète et non-standard, qui, via un système de polarités, est correcte et complète pour la synthèse de Church : il existe une classe syntaxique d’énoncés ∀∃, extractibles et dont la prouvabilité correspond exactement aux instances résolubles de la synthèse de
Church. Nous discutons aussi brièvement des questions reliées à l’axiomatisation de MSO sur les arbres infinis. Nos résultats dans cette directions nous semblent en revanche plus préliminaires.
Gratuit
Disciplines