Les programmes bien typés ont tout bon

Resumé

On étudie ici les sytèmes de typage prescriptif (à la Gödel ou Mercury) pour la programmation en logique. Dans de tels systèmes, le typage est statique, mais il garantit une propriété opérationnelle: si un programme est ``bien typé'', alors tous les buts obtenus par dérivation d'un but ``bien typé'' sont eux-même ``bien typés''. Le système est alors dit stable par réduction (``subject reduction''). Nous montrons dans ce papier que cette propriété de stabilité est en fait aussi déclarative. Cette vue déclarative nous conduit à reconsidérer une condition habituellement admise et nécéssaire pour la stabilité par réduction, dite condition de tête (``head condition''). Cette condition stipule que le type des têtes des clauses d'un programme ``bien typé'' doit être une variante (et non une instance quelconque) du type déclaré de son prédicat. Il est alors possible de formuler des conditions plus générales qui rétablissent une certaine symétrie entre les têtes et les atomes du corps, et qui garantissent en fait que dans toutes dérivations les types des termes unifiables sont eux aussi unifiables. On discute enfin les implications possibles d'un tel résultat.