Fonctions récursives primitives pour programmeurs praticiens

• Les discussions du type « si ce n’est pas Turing-complet, c’est sûr » s’écartent du sens mathématique : la non-Turing-complétude est largement indépendante de propriétés pratiques comme la terminaison, le déterminisme ou le sandboxing
• Un calcul de machine de Turing dont le temps d’exécution est borné par une fonction récursive primitive de l’entrée peut lui aussi être réécrit sous forme de fonction récursive primitive
• Les fonctions récursives primitives terminent toujours, mais elles peuvent aussi produire des fonctions à croissance très rapide comme 2^(2^N) ; la garantie de terminaison ne signifie donc pas un temps d’exécution pratique
• Dans la pratique, un programme qui ne s’arrête jamais et un programme qui s’arrête dans des milliards d’années posent des problèmes similaires ; même un langage Turing-complet peut être interrompu de force avec un compteur d’étapes
• La qualité d’un langage de configuration dépend davantage du déterminisme, d’une sémantique claire, de la pureté, de la sécurité et du sandboxing, du contrôle du temps d’exécution et de la simplicité que de son caractère Turing-complet ou non

---

Le malentendu central dans les discussions sur la Turing-complétude

• Sur Internet, les programmeurs présentent souvent le fait de « ne pas être Turing-complet » comme un avantage ou une exigence dans certains domaines
• Mais la Turing-completeness est un terme précis venu des mathématiques ; l’utiliser comme substitut à diverses propriétés recherchées en pratique en brouille le sens
• Les propriétés réellement nécessaires sont par exemple la garantie de terminaison, l’exécution rapide, le comportement déterministe, le sandboxing ou un langage de configuration simple ; elles sont pour la plupart orthogonales à la Turing-completeness
• Pour comprendre cette différence, il faut un résultat théorique simple sur les fonctions récursives primitives (Primitive Recursive Functions, PRF)

Une machine de Turing suffisamment rapide peut être convertie en PRF

• Même pour un programme écrit dans un langage Turing-complet, si l’on sait que son temps d’exécution est plus rapide que O(2^(2^N)), on peut implémenter le même algorithme dans un langage non Turing-complet
• La plupart des problèmes pratiques se situent dans un domaine où ils se terminent plus vite que 2^(2^N)
• Ainsi, un langage non Turing-complet ne limite pas significativement la capacité de calcul pratique, et ne confère pas automatiquement de capacité particulière à contrôler le calcul
• Du point de vue pratique, les deux programmes suivants posent en fait le même problème
  • Un programme qui ne termine pas
  • Un programme qui ne termine qu’après un nombre d’étapes égal à un milliard de fois un milliard, par exemple
• Même un langage Turing-complet peut simplement empêcher le problème de non-terminaison au niveau de l’implémentation en comptant le nombre d’étapes et en arrêtant avec une erreur au-delà d’une certaine limite

FSM : termine toujours, mais avec une expressivité limitée

• Une Finite State Machine (FSM) est un reconnaisseur qui prend une chaîne en entrée et renvoie « yes » ou « no »
• Une FSM est composée d’un ensemble fini d’états, d’un état initial, d’un ensemble d’états yes et d’une fonction de transition
• Après avoir appliqué de façon répétée la fonction de transition à chaque symbole de l’entrée, le résultat est déterminé par le fait que l’état final soit ou non un état yes
• L’expressivité des FSM est équivalente à celle des expressions régulières (regular expressions)
• Une FSM fonctionne en temps linéaire par rapport à la longueur de l’entrée et termine toujours, mais elle ne peut pas reconnaître tous les ensembles de chaînes
  • Par exemple, l’ensemble des chaînes où le même nombre de 0 apparaît de chaque côté de 1, comme 1, 010, 00100, 0001000, ne peut pas être reconnu par une FSM
  • Sur une entrée suffisamment longue, des états finissent par se répéter et forment un cycle ; si l’on duplique le segment correspondant à ce cycle, la FSM atteint toujours un état yes, mais la condition sur la chaîne est rompue

Machine de Turing : un modèle qui ajoute une bande modifiable à une FSM

• Une Turing Machine (TM) possède, comme une FSM, des états et une fonction de transition, mais elle fonctionne sur une bande modifiable plutôt que sur une entrée immuable
• À chaque étape, la TM lit le symbole courant de la bande et effectue les opérations suivantes
  • Elle remplace le symbole courant par un nouveau symbole
  • Elle change son état interne
  • Elle déplace la tête d’une case vers la gauche ou vers la droite
• Quand la TM atteint un état halt, elle s’arrête, et le contenu de la bande à cet instant constitue le résultat
• Alors qu’une FSM est un reconnaisseur binaire, une TM est un dispositif qui calcule des fonctions
• Une TM ne s’arrête pas nécessairement ; elle peut parcourir la bande, changer d’état, et ne jamais atteindre d’état final

Universal Turing Machine et capacité de calcul

• Le programme d’une TM n’est pas du code fourni comme entrée utilisateur, mais il est codé en dur dans la fonction de transition elle-même
• On peut toutefois encoder une TM arbitraire et son entrée sous forme de fichier texte, puis construire une TM « interpréteur » qui les interprète
• Une telle TM est une Universal Turing Machine, et elle simule une autre TM fournie en entrée
• Comme on peut écrire un interpréteur de TM en Python, et inversement implémenter un interpréteur Python sous forme de TM, les deux peuvent être considérés comme équivalents en capacité de calcul
• Une FSM est plus faible qu’une TM
  • Une TM peut simuler une FSM
  • Une TM peut décider, par manipulation de la bande, si une chaîne contient le même nombre de 0 des deux côtés d’un 1 central
  • Une FSM ne peut pas résoudre le même problème

La bande peut être vue comme deux piles

• La bande d’une TM est une abstraction difficile à implémenter directement dans un langage de programmation généraliste
• La bande et la position de la tête peuvent être représentées par deux piles
  • Le contenu à gauche de la tête est la pile de gauche
  • Le contenu à droite de la tête est la pile de droite, dans l’ordre inversé
• Déplacer la tête vers la gauche ou vers la droite devient une opération de pop sur une pile et de push sur l’autre
• Ainsi, une TM a une capacité de calcul équivalente à une « FSM dotée de deux piles »
• Si les symboles de la pile ne sont que 0 et 1, la pile elle-même peut être représentée par un seul entier naturel
  • Consulter le sommet : stack % 2
  • Pop : stack / 2
  • Push de x : stack * 2 + x

Les limites des machines de Turing : Halting Problem et résultats de type Rice

• Comme toutes les TM peuvent être encodées sous forme de texte, on peut énumérer les TM possibles dans une liste infinie
• À l’aide d’un argument diagonal, on peut montrer qu’il existe des fonctions qui ne sont pas calculables par une TM
• Un exemple plus concret est le Halting Problem
  • Il s’agit du problème consistant à déterminer, étant donné le code source d’une TM et son entrée, si cette TM finira un jour par s’arrêter
• Si l’on suppose que halts(program, input) termine toujours correctement, une contradiction apparaît avec le programme weird, qui reçoit son propre code source en entrée
  • Si halts décide qu’il s’arrête, weird entre dans une boucle infinie et ne s’arrête pas
  • Si halts décide qu’il ne s’arrête pas, weird termine immédiatement
• Donc halts doit soit se tromper dans certains cas, soit ne pas terminer dans certains cas
• Plus généralement, aucune propriété non triviale du comportement d’une TM arbitraire, dès lors qu’elle préserve le comportement, ne peut être décidée par algorithme
  • Les propriétés syntaxiques sont vérifiables, mais les propriétés comportementales qui restent valides après refactoring ne sont généralement pas décidables

Fonctions récursives primitives : un dispositif de calcul qui termine toujours

• Une fonction récursive primitive (PRF) est définie comme une fonction qui prend un tuple d’entiers naturels et renvoie un seul entier naturel
• Les fonctions de base sont zero et succ
  • zero = 0
  • succ(x) = x + 1
• La composition de fonctions permet de créer des constantes
  • succ(zero) = 1
  • succ(succ(zero)) = 2
• La récursion générale n’est pas autorisée, mais une boucle limitée LOOP(init, f, n), dont le nombre d’itérations est fixé à l’avance, l’est
  • LOOP(init, f, 0) = init
  • LOOP(init, f, 1) = f(init)
  • LOOP(init, f, 2) = f(f(init))
• La contrainte essentielle est que le nombre d’itérations n est fixé avant le début de la boucle, et que le corps de la boucle ne peut pas modifier le compteur de boucle

Construire les éléments de programmation de base avec des PRF

• L’addition peut être définie par add(x, y) = LOOP(x, succ, y)
• La multiplication peut être définie par mul(x, y) = LOOP(0, add x, y)
• L’exponentiation peut être définie par pow(x, y) = LOOP(1, mul x, y)
• Cela permet aussi de construire des fonctions à croissance rapide
  • pow_2(n) = pow(2, n)
  • pow_2_2(n) = pow_2(pow_2(n))
• Si l’on ajoute pred aux fonctions de base, on peut construire la soustraction saturée et les opérations booléennes
  • sub(x, y) = LOOP(x, pred, y)
  • and(x, y) = mul(x, y)
  • not(x) = sub(1, x)
  • if(cond, a, b) peut aussi être exprimé par une formule arithmétique
• Les comparaisons, le reste et la division peuvent également être implémentés avec des itérations bornées et des expressions conditionnelles

Structures de données des PRF et simulation de TM

• Une PRF peut prendre plusieurs arguments, mais son résultat est un seul entier naturel ; il faut donc encoder les structures de données sous forme d’entiers naturels
• Une paire (a, b) peut être représentée par 2^a * 3^b
• Pour en extraire les composantes, on cherche l’exposant maximal d’un nombre premier donné
  • fst(p) est l’exposant de la plus grande puissance de 2 qui divise p
  • snd(p) est l’exposant de la plus grande puissance de 3 qui divise p
• De la même manière, trois valeurs (S, stack1, stack2) peuvent être empaquetées dans un seul entier naturel
• Une configuration de TM peut être représentée par les trois éléments suivants
  • L’état courant S
  • La pile de gauche de la bande
  • La pile de droite de la bande
• Les manipulations de piles peuvent être implémentées avec le reste, la multiplication et la division ; on peut donc encoder un pas unique de TM sous forme de PRF
• Avec LOOP(initial_config, single_step, n), on peut simuler une TM pendant exactement n étapes
• Le problème est que l’on ne connaît pas forcément un n suffisant ; mais si le temps d’exécution est borné par une PRF, on peut effectuer autant d’itérations
• En fin de compte, un calcul de TM dont le temps d’exécution est borné par une fonction récursive primitive peut être remplacé par une PRF

Les limites des PRF : même si elles terminent toujours, elles ne sont pas aussi puissantes que les TM

• Les PRF terminent toujours, mais elles ne peuvent pas exprimer toutes les fonctions qui terminent
• Il existe des fonctions calculables par une TM mais non calculables par une PRF
• Pour le montrer, on borne le taux de croissance en fonction de la profondeur de l’arbre syntaxique de la PRF
• Pour toute PRF de profondeur inférieure ou égale à d, on peut fixer une borne afin qu’elle ne croisse pas plus vite qu’une certaine fonction unaire A_d
• A(d, x) est définie comme suit
  • A(1, x) = x + 1
  • A(d + 1, 0) = A(d, A(d, 0))
  • A(d + 1, x) = A(d, A(d + 1, x - 1))
• Dans cette définition, à chaque appel récursif, (d, x) diminue dans l’ordre lexicographique ; calculée par une TM, elle termine donc
• a(x) = A(x, x) croît plus vite que n’importe quelle PRF ; elle est calculable par une TM, mais pas par une PRF

Retour à la pratique : la non-Turing-complétude ne suffit pas

• Une machine de Turing peut ne pas s’arrêter
• Même des dispositifs qui terminent toujours, comme les FSM et les PRF, ne garantissent pas une fin rapide
• Une PRF peut calculer de grandes fonctions comme 2^(2^N) ; la seule garantie de terminaison ne garantit donc pas un temps d’exécution pratique
• De nombreux algorithmes réels ont un temps d’exécution borné par une PRF, et peuvent donc être exprimés même avec un dispositif non Turing-complet
• La méthode générale pour rendre un calcul Turing-complet semblable à une PRF consiste à ajouter un compteur d’itérations et à interrompre de force l’exécution si ce compteur devient trop grand

Les propriétés réellement nécessaires à un langage de configuration

• Les langages de configuration affichent souvent la « non-Turing-complétude » comme objectif de conception, mais ce qu’il faut réellement est un ensemble de propriétés plus fortes

• Déterminisme

  • Un langage de configuration doit être déterministe
  • Un comportement comme id([]) en Python, qui produit des valeurs différentes à chaque exécution, peut être acceptable en programmation générale, mais ne convient pas à la configuration
  • Les configurations servent souvent de clé pour des builds incrémentaux ou des systèmes de cache ; l’introduction de non-déterminisme perturbe le comportement du cache

• Sémantique claire

  • Le comportement du langage doit être clairement fixé par une référence consultable
  • Même si l’on peut rendre id([]) déterministe en désactivant l’ASLR et en utilisant un allocator particulier, cela ne garantit pas que le résultat soit prévisible ni identique entre implémentations
  • Pour garantir le même comportement entre différentes implémentations ou lors d’un changement de version de Python, la sémantique doit être explicite

• Pureté

  • Si la configuration peut lire des variables d’environnement ou des fichiers sur disque, sa signification dépend de l’environnement d’évaluation
  • Pour que le cache fonctionne correctement, le langage de configuration doit être pur

• Sécurité et sandboxing

  • La pureté et la sécurité peuvent toutes deux être obtenues en n’exposant pas d’IO générales
  • Les objectifs de ces deux propriétés sont différents
  • La pureté vise à empêcher que le résultat devienne non déterministe
  • La sécurité vise à éviter d’exposer à un attaquant des ressources comme des jetons d’accès

• Contrôle du temps d’exécution

  • Même en contrôlant les IO, une configuration malveillante peut encore mener une attaque par déni de service en consommant du CPU
  • Deux approches sont possibles pour garantir le temps d’exécution
  • Restreindre le traitement à une structure clairement linéaire, directement proportionnelle à la taille de l’entrée
  • Utiliser une exécution mesurée (metered execution) qui décrémente un compteur à chaque étape atomique et s’arrête quand ce compteur atteint 0

• Simplicité

  • Un langage de configuration doit inciter les utilisateurs à écrire des programmes simples
  • Interdire la récursion et les boucles infinies peut constituer un ralentisseur utile en faveur de la simplicité
  • Cependant, comme le montre l’exemple des PRF, de telles interdictions n’empêchent pas totalement d’écrire des programmes récursifs arbitraires ; elles obligent seulement à passer par un code plus détourné
  • Un exemple connexe est some roundabout code

Récapitulatif final

• Un algorithme de machine de Turing dont le temps d’exécution par rapport à l’entrée est borné par une fonction récursive primitive peut aussi être implémenté sous forme de fonction récursive primitive
• La non-Turing-complétude peut offrir une garantie de terminaison, mais elle ne garantit pas automatiquement les bornes de temps d’exécution ni la qualité d’un langage de configuration nécessaires en pratique
• Dans la conception d’un langage de configuration, les questions importantes sont moins la Turing-completeness elle-même que le déterminisme, une sémantique claire, la pureté, le sandboxing, la mesure du temps d’exécution et la simplicité

[GN⁺]

Commentaires sur Hacker News

• Auto-promo : https://www.nayuki.io/page/primitive-recursive-functions

  • Bien meilleur que l’article original, mais de nos jours tout le monde semble préférer les explications faciles façon ELI5

• La conclusion de l’article propose d’assez bons critères concernant les langages de configuration, et je me demande s’il existe aujourd’hui des langages qui en satisfont tout ou la plupart

  • Parmi les exemples qui satisfont ces critères, on trouve Dhall [1] et Cue [2], mais ce ne sont pas des exemples très intéressants dans un certain sens
    Dhall est intentionnellement un langage à fonctions totales, donc il choisit délibérément de ne pas être « Turing-complet », et Cue n’a pas de fonctions, donc rien à faire récursivement
    RCL [3] me semble satisfaire ces critères. Il est déterministe et pur, fournit une exécution mesurée, et sandboxe l’accès au système de fichiers. Si la politique de sandbox l’autorise, il peut lire des fichiers, mais ces fichiers sont alors considérés comme faisant partie du code source et se comportent comme des imports
    Dans RCL, on n’a pas voulu aller vers le « non Turing-complet » pour les raisons mentionnées par l’auteur. Le fait qu’un programme termine toujours n’est pas une propriété très utile en pratique, et inversement, même dans un langage à fonctions totales comme Agda, on peut écrire des programmes très complexes, donc le fait de ne pas être Turing-complet ne garantit pas des programmes ou des configurations simples
    Toutes les boucles de RCL sont bornées, mais comme il y a des fonctions, la récursion reste possible. Il n’y a pas d’appel terminal, donc au départ une limite de profondeur de récursion a été ajoutée pour éviter les stack overflows natifs, mais un fuzzer a trouvé une fonction qui s’arrête tout en s’exécutant avec un espace de pile constant, et je ne la comprends toujours pas complètement : let f = g => g(g(h => k => g(g(h)))); f(f)
    Au final, le fait de pouvoir exprimer ce genre de fonctions pathologiques ne pose pas vraiment de problème en pratique. Il suffit de limiter le nombre d’étapes d’exécution, c’est-à-dire avec une « limite de gas » ou l’« exécution mesurée » mentionnée par l’auteur. Pour garder un code simple, le fait que les structures de boucle intégrées soient bornées et que la récursion soit peu pratique est un bon garde-fou, mais au bout du compte les outils les plus précieux restent la revue de code et le bon jugement
    [1]: https://dhall-lang.org/
    [2]: https://cuelang.org/
    [3]: https://rcl-lang.org/
  • Ce n’est pas impératif et ce n’est pas non plus « pur », mais même C a été conçu dans une direction où il serait possible de connaître une borne supérieure du nombre d’itérations avant d’entrer dans chaque boucle, et il est donc primitif récursif
    Les recherches de Dennis Ritchie au MIT portaient sur ce qu’il appelait la programmation par boucles
    The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
    https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
    La programmation structurée, que presque tous les programmeurs modernes suivent par défaut, est en réalité un paradigme qui pousse fortement vers les fonctions primitives récursives. Comme la programmation structurée a été acceptée presque universellement par rapport à deux autres catégories comme le spaghetti code et le fonctionnel, on semble mal comprendre l’article de Dijkstra « goto considered harmful »
    Les fonctions primitives récursives n’incluent pas l’ensemble des fonctions calculables, mais elles couvrent presque toutes les fonctions intuitives dont on peut garantir la terminaison. Bien sûr, il existe des cas où des boucles dont on ne connaît pas le nombre d’itérations à l’entrée sont réellement nécessaires, mais c’est un piège à éviter sauf quand c’est indispensable
    Même COBOL s’est modernisé en déplaçant les goto illimités vers l’instruction ALTER. Je ne vois pas de langage moderne et utile qui n’autorise pas les fonctions PR
    Même en C, si on évite while et qu’on évite explicitement le fall through, on peut presque toujours écrire du code à fonctions totales qui termine forcément
    Il existe des cas pathologiques, comme l’inférence de types en ML. Le coût réel y est bien plus faible que ce que suggère la classe de complexité, donc cela vaut la peine de l’accepter même si le langage a du mal à restreindre ce type d’usage sans devenir un langage à fonctions totales
    En pratique, tous les langages fournissent par défaut quelque chose qui prend en charge la plupart de ces critères, mais des contraintes imposées pour les faire respecter limiteraient gravement l’utilité du langage. Même les frameworks SOLID et Clean, souvent critiqués, poussent selon moi dans cette direction
    La programmation structurée est devenue si universelle qu’il est facile d’oublier ce point, voire de ne plus savoir l’enseigner. En vieux barbu, je me souviens avoir appris les dangers de WHILE et consorts
  • Il suffirait probablement de prendre Dhall et de voir à quels critères il échoue. C’est celui qui paraît le plus proche

• Dire que ça s’exécute plus vite que O(2^(2^N)) est sans doute une simplification, mais la partie sur les « très grands nombres » fait un peu baisser la crédibilité
  Plus précisément, il faudrait sans doute parler de « fonction à croissance très rapide ». Ou alors cela semble vouloir dire que le programme se termine en moins de O(2^(2^N)) étapes

• Si l’on ne regarde que la première partie, sur le fait qu’un langage restreint serait meilleur pour certaines applications, j’ai l’impression que l’avantage est qu’on peut calculer statiquement une borne supérieure du nombre d’étapes nécessaires
  On pourrait alors rejeter tout calcul qui violerait cette limite pour n’importe quelle entrée, et renvoyer une erreur utile
  À l’inverse, quand on impose une limite d’exécution à un langage Turing-complet, on risque de fixer une limite trop basse pour certaines entrées qui nous intéressent. On ne le sait pas avant d’exécuter et de voir que la limite est atteinte. J’ai déjà vu ça de temps en temps avec la récursion de templates C++
  Il est possible que je sois complètement à côté de la plaque, donc j’aimerais bien qu’une personne qui maîtrise mieux le sujet l’explique

  • Un ancien collègue avait fixé un plafond proche de 3x, puis quelques années plus tard la charge réelle l’a effectivement atteint ; depuis, j’utilise une limite à 10x d’un volume de calcul raisonnable
    Même si un mauvais workflow met plusieurs fois plus longtemps à échouer, ça reste de l’ordre de la milliseconde, donc je n’y vois pas de gros dommage
    En général, on rencontre ce problème quand quelqu’un a traité le domaine du problème comme un graphe orienté acyclique, sans pouvoir imposer réellement la partie « acyclique ». Modéliser un problème comme un graphe orienté acyclique, c’est comme Dark Galadriel réfléchissant à accepter l’Anneau de Frodon. « Tous m’aimeront et désespéreront. » Les gens qui construisent ce genre de chose sont toujours bien plus fiers d’eux-mêmes qu’ils n’ont de raisons de l’être
    Au bout du compte, les clients attirés vers une solution coûteuse et complexe finissent à court d’argent, et leur propre problème commence à paraître bien plus petit. Il ne reste alors, littéralement, qu’une application incapable de réduire suffisamment le coût par tâche pour maintenir l’activité du client
  • Prédire exactement la consommation de carburant d’un calcul blockchain peut sembler intéressant à d’autres, mais pas à moi
    Ce qui m’intéresse davantage, c’est d’utiliser cela comme un marteau de plus dans la boîte à outils pour attraper des bugs qui ont échappé aux marteaux précédents, comme la vérification statique des types, l’absence de null et l’absence de mutation
    Le fait de terminer en temps fini ne prouve pas la correction, mais si je déclare que mon code se termine en temps fini et que le compilateur n’est pas d’accord, je considérerai que le code est faux
  • Une borne déterminée statiquement peut fortement surestimer la complexité réelle à l’exécution dans les cas courants. En effet, on ne peut généralement pas prédire comment seront évaluées les conditions qui provoquent une sortie anticipée dans une récursion
    Pour qu’une sortie anticipée influe sur le temps d’exécution, il faut supposer une évaluation paresseuse ou des conditions en court-circuit, mais un langage pratique disposera généralement de ce genre de mécanismes
  • Que fait-on si cette borne est extrêmement lâche ? Par exemple, le tri rapide déterministe est généralement en n log n, mais a une borne quadratique en fonction de la taille de l’entrée
    Faut-il alors rejeter un calcul de tri rapide ? Plus extrême encore, l’algorithme de Hindley–Milner a une borne exponentielle, alors qu’en pratique il tourne souvent en temps linéaire
  • Je ne sais pas si on peut parler de calcul « statique », mais à mes yeux le seul avantage d’une forte restriction des capacités du langage est qu’on peut imposer des limites de calcul qui ne dépendent pas des données
    Cela dit, j’ai du mal à imaginer ne serait-ce qu’une seule situation où ce serait vraiment une exigence forte. Combien de systèmes ne peuvent pas renvoyer une erreur du type « la requête a pris trop de temps » ?

• J’aimerais essayer un langage de programmation backend web fondé sur le principe non divergence / borné
  L’idée serait que chaque fonction doive prouver au compilateur, pour un état et des arguments donnés, que son exécution est bornée, et qu’elle puisse montrer que X est une borne inférieure et Y une borne supérieure. Cette information remonterait jusqu’aux points d’entrée
  Je suis d’accord avec l’auteur quand il dit qu’il faut une sémantique plus forte, et c’est pour cela que j’ai imaginé ce langage. On veut souvent des garanties sur le temps d’exécution d’un programme
  Le cœur serait basé sur les fonctions récursives primitives, mais en pratique il pourrait être Turing-complet. De la même manière que Rust rejette les emprunts invalides tout en fournissant unsafe pour les pointeurs bruts, ce langage pourrait calculer des bornes à partir de primitives itératives simples, ou bien utiliser un opérateur unsafe et fournir une formule alternative pour les bornes

• Je ne comprends pas bien la courte partie de plainte / motivation dans l’article
  Je parle du passage : « En général, dans certains domaines, le fait de ne pas être Turing-complet est célébré comme un avantage ou une exigence. Je pense que la plupart de ces discussions reposent sur une mauvaise compréhension — être non Turing-complet ne signifie pas ce que les gens s’imaginent. »
  Pourquoi ces discussions seraient-elles erronées ? La plupart des outils d’analyse formelle, par exemple Coq, Isabelle et Agda, exigent en général une preuve que les fonctions terminent. Cela revient à prouver que la fonction est totale ; cela ne signifie-t-il pas alors qu’elle est récursive primitive ?

  • Je ne l’ai pas lu jusqu’au bout, mais cet article semble partir du fait que certains langages de configuration mettent en avant le fait de « ne pas être Turing-complets » comme argument de vente. La fonctionnalité qu’ils veulent réellement promouvoir, ce serait plutôt un temps d’exécution raisonnablement borné
    C’est aussi ressorti dans les discussions récentes autour de CEL :
    https://news.ycombinator.com/item?id=40954652
  • Si l’on parle de preuve formelle, alors démontrer qu’une fonction est totale dans le cas général — et non via un contre-exemple scientifique comme dans la programmation moderne — est un problème de recherche exhaustive NP-complet
    Si je me souviens bien, c’est équivalent à NP avec un oracle co-NP, autrement dit au deuxième niveau de la hiérarchie polynomiale. Même si c’est faisable sur de petits problèmes, c’est coûteux
    Ces outils fonctionnent le mieux quand on structure le programme de façon à ce que les fonctions soient totales. Parmi ces structures, l’une des plus courantes consiste à n’utiliser que FOR en programmation structurée, ou seulement des WHILE / récursions dont le nombre d’itérations est borné
    Même si cela ne concerne que SAT, les formes faciles traitées dans le théorème de dichotomie de Schaefer sont la grille de lecture la plus accessible qui me vienne à l’esprit
  • Comme le montre l’article, il existe des fonctions qui terminent mais ne sont pas récursives primitives, donc une preuve de totalité d’une fonction n’implique pas qu’elle soit récursive primitive
    Agda, et probablement d’autres outils aussi, peut prouver la terminaison de certaines fonctions non récursives primitives qui terminent. Évidemment, c’est impossible de le faire pour toutes
    Le malentendu que critique l’article ressemble plus ou moins à ceci : « La complétude de Turing signifie qu’on peut calculer ; l’absence de complétude de Turing signifie qu’on ne peut pas calculer, et qu’on obtient de bonnes propriétés de langage de configuration. »
    L’idée de l’article est que même sans être Turing-complet, on peut encore faire beaucoup de calculs coûteux ou délicats, et qu’un langage de configuration a besoin de restrictions bien plus fortes que la simple non-complétude de Turing
  • Il peut y avoir d’autres manières de ne pas être Turing-complet que d’être une classe proprement totale de fonctions qui terminent élégamment. Par exemple, une boucle infinie n’est ni capable de calcul universel, ni terminante

• Je suis développeur CUE. CUE est primitivement récursif et répond aussi aux critères qu’on attend d’un « bon » langage de configuration

  • Pour le plaisir, voici un exemple qui simule avec CUE un nombre arbitraire mais fini d’étapes de la Rule 110 : https://cuelang.org/play/?id=Ityqia88Mvq#w=function&i=cue&f=...
    [0] https://en.wikipedia.org/wiki/Rule_110