ARBRES D’ORDRE SUPÉRIEUR

Au Chapitre 6, on a démontré que l’éliminateur de coupures était un modèle de machine abstraite pouvant calculer les fonctions qu’on peut dénoter par des preuves circulaires. Mais quelles sont ces fonctions, exactement ? C’est une ques- tion qui fut soulevée et partiellement répondue, dans le cas des fonctions numé- riques f : Nk ! N, dans (Paré et Román, 1989; Cockett et Santocanale, 2003), où il fut démontré que les fonctions primitives récursives en faisaient partie.On a expliqué, au Chapitre 5, que l’éliminateur de coupures était une sorte d’au- tomate fini avec mémoire qui produit une preuve arborescente. La question peut donc être tournée autrement comme suit : quelle est la complexité des arbres pou- vant être produits par l’éliminateur de coupures ? C’est une question qui englobe la précédente, car n’importe quelle fonction numérique peut être encodée en un arbre étiqueté comme à la Figure 7.1, où les branches successives partant de la tige principale encodent les différentes valeurs de f (n).Cette approche ramène le problème à celui de comparer le fonctionnement de l’éliminateur de coupures au fonctionnement d’autres modèles d’automates finis avec mémoire qui produisent des arbres. Un choix particulièrement intéressant de telles machines est celui des automates à pile d’ordre supérieur (Knapik et al., 2002). La hiérarchie de Caucal (Caucal, 2003) est une classification bien établied’arbres infinis à branchements finis. Le niveau d’un arbre dans cette hiérarchie correspond au niveau de complexité de la structure de mémoire de l’automate d’ordre supérieur qui l’engendre. Ces structures de mémoire sont des piles de piles de . . . de piles. L’idée est donc de situer les arbres produits par l’éliminateur de coupure dans la hiérarchie.

Il se trouve, comme on le démontre dans le présent chapitre, que tous les arbres se trouvant dans la hiérarchie de Caucal peuvent être calculés par l’éliminateur de coupures, qui opère sur une pré-preuve finie. On démontre ce fait par une construction explicite de la pré-preuve en question. Cela ne signifie toutefois pas que les arbres d’ordre supérieur peuvent tous être dénotés par des preuves cir- culaires, car notre construction ne satisfait pas nécessairement la condition de garde (ce qui n’empêche pas l’élimination des coupures d’être productive). On doit donc faire une distinction entre les arbres qui sont circulairement calculables et ceux qui sont circulairement définissables. On démontre aussi que la réciproque est fausse, en exhibant un arbre circulairement définissable qui ne se trouve pas dans la hiérarchie de Caucal.

Algèbre des n-piles

Les automates d’ordre supérieur opèrent sur des piles d’ordre supérieur, qu’on appelle des n-piles. Avant de passer à la définition des automates eux mêmes, il importe d’étudier les piles ainsi que leur structure algébrique.Définition. Fixons un alphabet fini avec un symbole ? 2 . Une 0-pile est un élément de . Pour n 1, une n-pile est une liste finie de (n1)-piles. Une n-pile est dite bien formée si n = 0 ou si elle est une liste non vide de (n 1)-piles bien formées. Le symbole de dessus d’une n-pile bien formée est défini récursivement comme suit :On doit d’abord décrire les n-piles par un système d’équations dirigé, afin de les manipuler par les preuves circulaires. Puisque les n-piles sont des listes finies de (n 1)-piles, la première solution à laquelle on pourrait penser serait d’itérer l’étoile de Kleene, P = X:(1 + P X), qui définit le monoïde libre. On aurait donc la définition récursive suivante de l’ensemble Pn des n-piles :Or, ce système ne conviendra pas à nos besoins, puisque les produits cartésiens se traitent mal du côté gauche des preuves circulaires. En effet, la structure des règles Lj nous oblige à sacrifier la queue d’une telle liste pour pouvoir lire sa tête, et vice-versa.

Soit Ln l’ensemble des mots décrivant un chemin allant de Zn vers Zn+1 (par les transitions du graphe) dans le jeu Jn. Puisque le jeu J0 ne contient que les transitions de Z0 vers Z1 étiquetées par les a 2 , alors L0 = = P0. Pour n 1, clairement, les seuls mots s 2 Ln sont Niln et les mots de la forme Consn u v où u 2 Ln1 et v 2 Ln. On a doncIl est quand même utile d’exhiber la construction de s qui est proposée dans le Théorème 6.4. Rappelons que, selon la représentation du Lemme 7.2, s est identifié à un mot de Ln. Chaque lettre de s correspond à un mouvement dans le jeu correspondant. On peut encoder ces mouvements dans une preuve comme suit :– si s = Niln, alorsNotre prochain objectif est d’exprimer les opérations usuelles de n-piles dans ce modèle. L’objectif est de dégager le fait que ces opérations ne font intervenir rien d’autre que les opérations des catégories -bicomplètes et donc, qu’elles sont définissables par des preuves circulaires, en vertu du Théorème 4.7.

w; u] en mémoire. À l’exception de la règle I sur la feuille, toutes les règles de chaque k sont des règles droites. De plus, ces règles sont les mêmes que celles qui sont utilisées dans la construction de s. Alors les 2(n + 1) premières actions de l’éliminateur de coupures sont des productions droites, qui produisent une copie de r (excepté à la feuille), où r = ConsnConsn1 Cons1 a.Or, puisque % est une exécution, alors (qt; top(st)) = (f; p1 : : : pr) pour certains p1 : : : pr 2 Q. Par le Lemme 7.10, ce(M 0) et tcoïnciden ta umoin sjusqu’ àun ehauteu rd e4 .Pou rl ahauteu rrestante ,o ndoi tvérifie rqu epou r 1 i r ,le smulticoupure s M0L’objectif de cette section est de démontrer que la réciproque du Théorème 7.7, qui dit que tous les arbres circulairement calculables peuvent être situés dans la hiérarchie de Caucal, est fausse. Pour ce faire, on donne un exemple d’un arbre circulairement définissable, donc circulairement calculable par la Proposition 7.1, qui ne se trouve pas dans la hiérarchie.