text:
# Structure automatique
En informatique théorique, une structure automatique est une structure définie à partir d'automates finis. L'intérêt principal de ces structures est de représenter de manière finie des objets infinis, ce qui offre un cadre « naturel » à la décidabilité de problèmes.
En particulier, la vérification de modèles de formules de la logique du premier ordre est décidable sur les structures automatiques.

## Introduction

### Structures
On considère des structures de la forme {\displaystyle \langle A,R_{1}\dots R_{p},f_{1}\dots f_{q}\rangle }où :
- {\displaystyle A} est un ensemble (dénombrable) ;
- {\displaystyle R_{1}\dots R_{p}} sont des prédicats sur {\displaystyle A} d'arités {\displaystyle r_{1}\dots r_{p}} ;
- {\displaystyle f_{1}\dots f_{q}} sont des fonctions (partielles) sur {\displaystyle A} d'arités {\displaystyle r'_{1}\dots r'_{q}}.

Quitte à remplacer les fonctions des prédicats caractérisant leurs graphes, on peut supposer que les structures sont purement relationnelles.

### Structures récursives
Il semble naturel qu'afin de décider des propriétés logiques sur une structure, celle-ci doive posséder une représentation finie.
C'est l'idée que généralisent les structures récursives : l'ensemble de leurs éléments {\displaystyle A} est récursif, et les ensembles de {\displaystyle r}-uplets définis par les relations le sont également. On peut donc représenter de telles structures par une collection finie de machines de Turing.
Néanmoins les nombreux résultats d'indécidabilité sur ces structures très générales montrent qu'il est nécessaire de se restreindre à certaines sous-classes, comme les structures automatiques.

## Définition formelle

### Structures automatiques
Une structure relationnelle {\displaystyle {\mathcal {U}}=\langle A,R_{1}\dots R_{p}\rangle }est dite automatique s'il existe un alphabet fini {\displaystyle \Sigma }, un langage {\displaystyle L_{\delta }} et une fonction de décodage surjective {\displaystyle \nu :L_{\delta }\mapsto A} tels que :
- {\displaystyle L_{\delta }}, le domaine de {\displaystyle \nu }, est un langage régulier de {\displaystyle \Sigma ^{*}};
- {\displaystyle L_{\varepsilon }:=\{(w,w')~|~\nu (w)=\nu (w')\}}(qui caractérise les défauts d'injectivité) est reconnu par un transducteur synchrone (sans {\displaystyle \varepsilon }-règles) ;
- Pour tout prédicat {\displaystyle R_{i}} d'arité {\displaystyle r_{i}}, le langage {\displaystyle L_{i}:=\{(w_{1}\dots w_{r_{i}})~|~R_{1}(\nu (w_{1})\dots \nu (w_{r_{i}}))\}} est reconnu par un transducteur synchrone.

### Représentations automatiques
Toute structure automatique {\displaystyle {\mathcal {U}}=\langle A,R_{1}\dots R_{p}\rangle } possède une représentation automatique sous la forme {\displaystyle \langle \nu ,M_{\delta },T_{\varepsilon },T_{1}\dots T_{p}\rangle }où :
- {\displaystyle M_{\delta }} est un automate fini sur {\displaystyle \Sigma } qui reconnaît {\displaystyle L_{\delta }} ;
- {\displaystyle T_{\varepsilon }} est un transducteur synchrone qui reconnaît {\displaystyle L_{\varepsilon }} ;
- Chaque {\displaystyle T_{i}} est un transducteur synchrone qui reconnaît {\displaystyle L_{i}}.

C'est à partir de cette représentation que l'on va décider certaines propriétés de la structure.

## Exemples
1. Les structures finies sont automatiques.
2. L'ensemble des entiers naturels muni de l'addition {\displaystyle \langle \mathbb {N} ,+\rangle } est automatique. On code les entiers en base 2 avec le bit de poids fort à droite et l'addition est représentée avec un transducteur synchrone.
3. On peut étendre la structure précédente avec une relation de divisibilité restreinte : {\displaystyle x|_{p}y} si {\displaystyle x} est une puissance de {\displaystyle p} qui divise {\displaystyle y}. Pour tout {\displaystyle p\geq 2}, la structure {\displaystyle {\mathfrak {N}}_{p}=\langle \mathbb {N} ,+,|_{p}\rangle } est automatique.
4. Les groupes automatiques sont des cas particuliers de structures automatiques qui sont des groupes.

### Représentation automatique deNp=⟨N,+,|p⟩{\displaystyle {\mathfrak {N}}_{p}=\langle \mathbb {N} ,+,|_{p}\rangle }
Le langage {\displaystyle L_{\delta }} est l'ensemble des mots finis sur l'alphabet {0, 1}. La fonction de décodage associe à tout mot fini m l'entier dont la représentation binaire avec le bit de poids fort à droite est m. Par exemple, le mot 00101 se décode en 4+16 = 20. L'addition est représentée par l'automate à deux états donnée dans la figure de droite.

## Décidabilité de la vérification de modèles
Étant donné une représentation d'une structure automatique, la vérification de modèles d'une formule logique du premier ordre sur le langage des prédicats de la structure est décidable.
En particulier, étant donné une formule {\displaystyle \varphi ({\overline {x}})} de variables libres {\displaystyle {\overline {x}}=(x_{1}\dots x_{n})} sur ce langage, il est possible de construire un transducteur synchrone reconnaissant l'ensemble des codages d'éléments vérifiant la formule :{\displaystyle \{(w_{1}\dots w_{n}~|~{\mathcal {U}},[x_{1}\mapsto \nu (w_{1})\dots x_{n}\mapsto \nu (w_{n})]\models \varphi ({\overline {x}})\}}.
Il est possible d'étendre la logique du premier ordre avec un quantificateur {\displaystyle \exists ^{\omega }}dont la sémantique est définie comme « il existe une infinité ». Grâce au lemme de l'étoile, on peut montrer que la vérification de modèles de cette logique étendue reste décidable sur les structures automatiques.

## Propriétés remarquables

### Injectivité de la représentation
À partir d'une représentation automatique d'une structure, il est possible d'en construire une représentation injective.
Une telle représentation vérifie que la fonction de décodage {\displaystyle \nu } est injective, ou de manière équivalente, que {\displaystyle L_{\varepsilon }=\{(w,w)~|~w\in L_{\delta }\}}.

### Clôture
La classe des structures automatiques est closes par :
- mise à une puissance finie ;
- quotient par une relation définissable au premier ordre ;
- ajout d'un prédicat définissable au premier ordre ;
- restriction à une sous-structure dont le domaine est définissable au premier ordre.

## Extensions
Par définition, les structures automatiques sont finies ou dénombrables. Il est possible d'étendre la définition à des ensembles ayant la puissance du continu via un encodage par des mots infinis, on parle alors de structure {\displaystyle \omega }-automatique.

title: Structure automatique

wikitext:
En [[informatique théorique]], une '''structure automatique'''<ref>{{Article|prénom1=Achim|nom1=Blumensath|prénom2=Erich|nom2=Grädel|titre=Automatic Structures|périodique=Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science|série=LICS '00|éditeur=IEEE Computer Society|date=2000-01-01|isbn=0769507255|lire en ligne=http://dl.acm.org/citation.cfm?id=788022.789015|consulté le=11 juin 2016|pages=51–}}.</ref> est une [[Structure (logique mathématique)|structure]] définie à partir d'[[Automate fini|automates finis]]. L'intérêt principal de ces structures est de représenter de manière finie des objets infinis, ce qui offre un cadre « naturel » à la décidabilité de problèmes.

En particulier, la [[vérification de modèles]] de formules de la [[logique du premier ordre]] est [[décidable]] sur les structures automatiques.

== Introduction ==

=== Structures ===
On considère des [[Structure (logique mathématique)|structures]] de la forme <math>\langle A, R_1 \dots R_p, f_1 \dots f_q \rangle</math>où :
* <math>A</math> est un ensemble (dénombrable) ;
* <math>R_1 \dots R_p</math> sont des prédicats sur <math>A</math> d'arités <math>r_1 \dots r_p</math> ;
* <math>f_1 \dots f_q</math> sont des fonctions (partielles) sur <math>A</math> d'arités <math>r'_1 \dots r'_q</math>.
Quitte à remplacer les fonctions des prédicats caractérisant leurs [[Graphe d'une fonction|graphes]], on peut supposer que les structures sont purement relationnelles.

=== Structures récursives ===
Il semble naturel qu'afin de décider des propriétés logiques sur une structure, celle-ci doive posséder une représentation finie.

C'est l'idée que généralisent les '''structures récursives'''<ref name=":0">{{Article|langue=anglais|auteur1=T. Hirst and D. Harel.|titre=More about recursive structures: Descriptive complexity and zero-one laws|périodique=Proc. 11th IEEE Symp. on Logic in Computer Science|numéro=|jour=|mois=|année=1996|issn=|lire en ligne=http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.8316&rep=rep1&type=pdf|pages=334-348}}.</ref> : l'ensemble de leurs éléments <math>A</math> est [[Ensemble récursif|récursif]], et les ensembles de <math>r</math>-[[Uplet|uplets]] définis par les relations le sont également. On peut donc représenter de telles structures par une collection finie de [[Machine de Turing|machines de Turing]].

Néanmoins les nombreux résultats d'[[Décidabilité|indécidabilité]]<ref name=":0" /> sur ces structures très générales montrent qu'il est nécessaire de se restreindre à certaines sous-classes, comme les '''structures automatiques'''.

== Définition formelle ==

=== Structures automatiques ===
Une structure relationnelle <math>\mathcal{U} = \langle A, R_1 \dots R_p\rangle</math>est dite '''automatique''' s'il existe un alphabet fini <math>\Sigma</math>, un langage <math>L_\delta</math> et une fonction de décodage surjective <math>\nu : L_\delta \mapsto A</math> tels que :
* <math>L_\delta </math>, le domaine de <math>\nu</math>, est un [[Langage rationnel|langage régulier]] de <math>\Sigma^*</math>;
* <math>L_\varepsilon := \{(w,w')~|~\nu(w) = \nu(w')\} </math>(qui caractérise les défauts d'injectivité) est reconnu par un [[Transducteur fini|transducteur]] synchrone (sans <math>\varepsilon </math>-règles) ;
* Pour tout prédicat <math>R_i </math> d'arité <math>r_i </math>, le langage <math>L_i := \{(w_1 \dots w_{r_i})~|~R_1(\nu(w_1) \dots \nu(w_{r_i}))\} </math> est reconnu par un transducteur synchrone.

=== Représentations automatiques ===
Toute structure automatique <math>\mathcal{U} = \langle A, R_1 \dots R_p\rangle</math> possède une représentation automatique sous la forme <math>\langle \nu, M_\delta, T_\varepsilon, T_1 \dots T_p\rangle</math>où :
* <math>M_\delta</math> est un [[automate fini]] sur <math>\Sigma</math> qui reconnaît <math>L_\delta </math> ;
* <math>T_\varepsilon</math> est un transducteur synchrone qui reconnaît <math>L_\varepsilon </math> ;
* Chaque <math>T_i</math> est un transducteur synchrone qui reconnaît <math>L_i </math>.
C'est à partir de cette représentation que l'on va décider certaines propriétés de la structure.

== Exemples ==
# Les structures finies sont automatiques.
# L'ensemble des entiers naturels muni de l'addition <math>\langle\mathbb{N}, + \rangle</math> est automatique. On code les entiers en base 2 avec le [[bit de poids fort]] à droite et l'addition est représentée avec un transducteur synchrone.
# On peut étendre la structure précédente avec une relation de divisibilité restreinte : <math>x |_p y</math> si <math>x</math> est une puissance de <math>p</math> qui divise <math>y</math>. Pour tout <math>p \ge 2</math>, la structure <math>\mathfrak{N}_p = \langle\mathbb{N}, +, |_p\rangle</math> est automatique.
# Les [[Groupe automatique|groupes automatiques]] sont des cas particuliers de structures automatiques qui sont des [[Groupe (mathématiques)|groupes]].

=== Représentation automatique de <math>\mathfrak{N}_p = \langle\mathbb{N}, +, |_p\rangle</math> ===
[[Fichier:Automate addition verificateur.svg|vignette|Automate qui vérifie l'addition. Il accepte un mot <math>(x_n y_n z_n)\dots (x_0 y_0 z_0)</math> si le nombre <math>z_0\dots z_n</math> est égal à la somme de <math>x_0\dots x_n</math>et <math>y_0\dots y_n</math>.|489x489px]]
Le langage <math>L_\delta</math> est l'ensemble des mots finis sur l'alphabet {0, 1}. La fonction de décodage associe à tout mot fini m l'entier dont la représentation binaire avec le bit de poids fort à droite est m. Par exemple, le mot 00101 se décode en 4+16 = 20. L'addition est représentée par l'automate à deux états donnée dans la figure de droite.

== Décidabilité de la vérification de modèles ==
Étant donné une représentation d'une structure automatique, la [[vérification de modèles]] d'une [[formule logique]] du [[Logique du premier ordre|premier ordre]] sur le langage des prédicats de la structure est décidable.

En particulier, étant donné une formule <math>\varphi(\overline{x})</math> de variables libres <math>\overline{x} = (x_1 \dots x_n)</math> sur ce langage, il est possible de construire un transducteur synchrone reconnaissant l'ensemble des codages d'éléments vérifiant la formule :<math>\{(w_1 \dots w_n~|~\mathcal{U}, [x_1 \mapsto \nu(w_1) \dots x_n \mapsto \nu(w_n)] \models \varphi(\overline{x})\}</math>.

Il est possible d'étendre la logique du premier ordre avec un quantificateur <math>\exists^\omega</math>dont la sémantique est définie comme « il existe une infinité ». Grâce au [[lemme de l'étoile]], on peut montrer que la vérification de modèles de cette logique étendue reste décidable sur les structures automatiques.

== Propriétés remarquables ==

=== Injectivité de la représentation ===
À partir d'une représentation automatique d'une structure, il est possible d'en construire une représentation injective.

Une telle représentation vérifie que la fonction de décodage <math>\nu</math> est injective, ou de manière équivalente, que <math>L_\varepsilon = \{(w,w)~|~w \in L_\delta\} </math>.

=== Clôture ===
La classe des structures automatiques est closes par :
* mise à une puissance finie ;
* quotient par une relation définissable au premier ordre ;
* ajout d'un prédicat définissable au premier ordre ;
* restriction à une sous-structure dont le domaine est définissable au premier ordre.

== Extensions ==
Par définition, les structures automatiques sont finies ou [[Ensemble dénombrable|dénombrables]]. Il est possible d'étendre la définition à des ensembles ayant la [[puissance du continu]] via un encodage par des mots infinis, on parle alors de [[Structure oméga-automatique|structure <math>\omega</math>-automatique]].

== Notes et références ==
{{Références}}

{{Portail|informatique théorique}}

[[Catégorie:Théorie des modèles]]