A Dialectica-Like Approach to Tree Automata
Résumé
We propose a fibred monoidal closed category of alternating tree automata. Our notion is based on Dialectica-like categories, suggested by the specific logical form of the transitions of alternating automata. The basic monoidal closed structure gives a realizability interpretation of proofs of a first-order multiplicative linear logic as winning strategies in corresponding acceptance games. Moreover, we show that the usual powerset operation translating an alternating automaton to an equivalent non-deterministic one satisfies the deduction rules of the '!' modality of linear logic. We thus get a deduction system for intuitionistic linear logic, which in particular gives deduction for minimal intuitionistic predicate logic via the Girard translation. We also get a weak form of completeness of our realizers wrt language inclusion, based on the '?' modality.
Origine : Fichiers produits par l'(les) auteur(s)