Alors que SupGen approche, je publierai du contenu technique qui fera un flop car il ne s'agit pas de contenu sur l'IA décérébrée, mais je veux le faire quand même. Voici quelques réflexions sur la totalité et la cessation. En Agda (et en Lean ?), la terminaison est assurée par une « récursivité structurelle », ce qui signifie que les arguments peuvent décroître selon l'« ordre lexicographique ». Vous comprenez ? Moi non plus, je ne comprenais pas. Mais en fait, c'est assez simple. Prenons une proposition comme : foo : Nat → Nat foo (S a) (S b) (S c) (S d) = foo (S a) (S b) c (S (S (S d))) foo x = x Est-ce que ça se termine ? Est-ce que ça ne se termine pas ? Comment le savoir ? En Agda, cela se passe ainsi : Étape n° 0 : - argument 0 à gauche : (S a) - argument 0 du membre de droite : (S a) - c'est *identique*, donc, vérifiez l'argument suivant (Remarque : LHS/RHS signifie côté gauche/côté droit de l'équation) Étape n° 1 : - argument 1 à gauche : (S b) - argument 1 du membre de droite : (S b) - c'est *identique*, donc, vérifiez l'argument suivant Étape n° 2 : - argument 2 à gauche : (S c) - argument 2 du membre de droite : c - ceci est *plus petit*, donc, cette clause se termine ! Et voilà, c'est terminé. En résumé, à chaque fois qu'il y a un appel récursif du côté droit, il suffit de comparer ses arguments avec les modèles correspondants du côté gauche, un par un, jusqu'à ce que l'un soit plus petit. Simple, n'est-ce pas ? (J'aurais aimé qu'ils puissent l'expliquer comme ça...) Considérons maintenant : foo : Paire -> Paire foo (Paire (S a) (S b)) = foo (P a (S (S (S b)))) foo x = x Cette fonction est-elle en train de se terminer ? Eh bien, selon Agda… non ! Pourtant, c’est clairement le cas, pour la même raison : puisque le premier composant est plus petit, le fait que le second soit plus grand n’a aucune importance. Il semblerait que le vérificateur d’Agda soit programmé pour segmenter les arguments. Par conséquent, cette clause, telle qu’elle est écrite, ne passera pas le test, même si elle se termine. Pourquoi est-ce que je parle de ça ? J'ai donc examiné le générateur de récursivité de SupGen et je me suis rendu compte qu'il pourrait être plus propre *et* plus rapide avec quelques modifications. Mais ces modifications sont-elles pertinentes ? J'ai fait des tests et, à ma grande surprise, SupGen générait des programmes non terminaux… selon Agda. J'ai d'abord pensé que mon approche était erronée, mais il s'avère que c'était Agda qui l'était. Vous avez maintenant de nouvelles connaissances. Je suis sûr que cela vous sera utile un jour !
Le nouvel algorithme utilisé par SupGen pour générer des appels récursifs terminaux est beaucoup plus simple *et* plus général !
