Prédicats morphiques
et applications à la décidabilité
de théories arithmétiques

Arnaud Maes

Résumé

A. L. Semenov a déterminé les prédicats unaires P sur N (l'ensemble des nombres naturels) pour lesquels la structure <N,S,P,<,0> admet l'élimination des quantificateurs. Il s'agit des prédicats presque-périodiques.

Lorsque le prédicat P est morphique, c'est-à-dire est obtenu comme projection du point fixe d'un morphisme de mots, nous donnons un algorithme permettant de tester s'il est presque-périodique.

De plus, nous montrons que la structure <N,S,P,<,0> est décidable pour tout prédicat unaire morphique P (qu'il soit presque-périodique ou non).

Dans le cas des prédicats n-aires, nous étendons la notion de presque-périodicité afin d'obtenir une condition suffisante d'élimination des quantificateurs dans ce cadre plus général.

Enfin, nous introduisons une notion de morphisme de mots à n dimensions (ou tableaux) et montrons que la structure <N,S,P,<,0> est décidable pour tout prédicat n-aire P obtenu comme projection d'un tableau morphique satisfaisant une certaine condition de symétrie.