"Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :"
On dirait que la principale raison du coté indécidable est la récursion. C'est pour cela que je parle de graphe acyclique. Il suffit de traiter les références différemment des définitions, cela permet de transformer la plus part des codes/données en graphes acycliques.
Selon le système de types (sa « puissance » expressive) l'existence d'une preuve d'une assertion peut devenir indécidable
Oui, d'où la recherche d'un sous-ensemble dans lequel il est possible de prouver quelques choses d'utile, et ne surtout pas regarder le cas général.
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
On dirait que la principale raison du coté indécidable est la récursion. C'est pour cela que je parle de graphe acyclique. Il suffit de traiter les références différemment des définitions, cela permet de transformer la plus part des codes/données en graphes acycliques.
Oui, d'où la recherche d'un sous-ensemble dans lequel il est possible de prouver quelques choses d'utile, et ne surtout pas regarder le cas général.
"La première sécurité est la liberté"