Effectivité du calcul
Contexte
Dans le cadre des principes fondateurs et de la sub-physique, il faut représenter ce qui existe par des calculs. Il parait logique que pour exister il faut que le calcul soit réalisé (voir ci-dessous "Réaliser le calcul ?"). Mais du fait que l'interprétation est paresseuse, si on retourne par exemple une paire, alors les deux valeurs contenues ne sont pas calculées.
Question
Comment faire en sorte pour que les calculs soit effectifs ?
Étude
Réaliser le calcul ?
Si le calcul n'a pas besoin d'être réalisé alors le temps de calcul n'a plus d'importance. On peut alors avoir à l'intérieur d'une étape d'un calcul une formule qui génère une infinité de calculs. On ne peut alors plus raisonner sur les densités des choses dans les calculs car on a partout des infinités. Et donc la notion de calcul pour représenter le réel n'a plus de sens puisque très tôt on a toute les choses possibles.
Exemple de calcul non effectif
On veut calculer la liste infinie des entiers naturels, on définit :
$Def f = $F n → $T[ n , f \ n + 1 ]
et le calcul des entiers naturels est fait par f 0.
Le problème est que si on calcul f 0 alors le calcul s'arrête à $T[ 0 , f \ 0 + 1 ].
Des blocages incontournables
Si on veut retourner une structure infinie où chaque nœud demande un calcul, alors la fonction ne peut pas la retourner car cela demanderait un temps infini.
S'assurer de l'effectivité du calcul par le calcul de la condition des if
On ne peut pas retourner une structure demandant une infinité de calculs effectifs. Il faut donc renoncer à récupérer le résultat.
Par contre on peut faire en sorte que le calcul soit effectif en faisant calculer la donnée dans la condition d'un if. Même si le résultat n'est jamais retourné puisqu'il y a une infinité de calculs.
Par exemple pour l'énumération des entiers naturels :
$Def f = $F n → if ( isEmptyList n ∨b 1b ; $T[ n, f \ n + 1 ] ; 0b)
Mais dans ce cas on ne fait exister l'entier naturel que tout seul et par intermitence dans le calcul.
Si la structure infinie n'est pas retournée, comment existe-t-elle ?
Elle peut exister soit :
- tout au long du calcul
- par intermitence
La solution par intermitence consiste à faire exécuter le calcul dans la condition d'un "if". Cette solution me gêne pour plusieurs raisons :
- elle est artificielle car le if ne sert qu'à ça
- le calcul doit être refait depuis le début à chaque fois
- la partie du calcul où la chose existe devient de plus en plus petite par rapport au reste du calcul
C'est pourquoi je choisis que l'existence doit reposer sur une donnée existant en permanence dans le calcul. Par contre l'endroit où se trouve cette donnée peut changer (car quand le calcul évolue les endroits changent).
Changer de postulat ?
essai 7
Idée
Pour calculer une formule, on définit une "étape de calcul sur une formule" , cela prend en argument une formule et retourne une liste de formules où chacunne est la formule précédente avec un calcul élémentaire en plus. L'algorithme d'une "étape de calcul sur une formule" est le suivant :
- On éxécute une étape de calcul sur la partie argument
- La dernière formule de la liste est utilisée (ou si elle est vide la formule de départ) pour éxécuter une étape de calcul sur la partie fonction
- La dernière formule de la liste est utilisée pour éxécuter un calcul élémentaire sur la formule entière (ou si elle est vide la formule de départ)
Pour calculer l'ensemble des formules on utilise un système qui équilibre le nombre de calcul élémentaires entre les formules de départ. Pour cela, pour chaque formule à calculer, on a deux couples : la liste des formules où chacune subit un calcul élémentaire par rapport à la précédente, la formule active. Quand on a utilisé toute la liste des formules, on reprovisionne la liste à partir de la formule active.
Si le calcul d'une formule est fini alors on élimine le calcul.
essai 6
Idée
À la place d'interpréter d'une certaine manière, guidé par un marquage (que ce soit le mot clé "compute" ou autre), on exécute les calculs de toutes les manières possibles. Donc on produit à chaque fois, pour une seule formule et un seul pas de calcul, une multitude de formules résultantes (une par possibilité de calcul sur n'importe quelle partie de la formule).
Implémentation
On ne peut plus représenter un calcul par une liste car il y a différentes possibilité. Il faut donc un arbre de la forme $T[ f, l ] où f est la formule à calculer et l est la liste des calculs possibles ayant pour la partie formule une formule g tq f →c[loose]1 g.
Problème
Cela cré une multitude de calculs parallèles, ce qui en soit n'est pas gênant. Mais alors on a deux problèmes :
Équilibrer les quantités de calculs entre les formules :
Équilibrer les calculs inutils entre les formules :
Solution :
Dans ce mode toutes les sous-formules sont calculées (par un calcul élémentaire). On pourra donc avoir une des sous-formules qui grossit indéfiniment (par exemple l'évaluation du "recurse"). Mais bien que cela fasse grossir indéfiniment la formule, ce n'est pas gênant. On est assuré que toute sous-formule sera entièrement calculée si le calcul n'est pas infini.
essai 5
Idée
On reprend l'idée d'introduire le mot compute, mais à la place de modifier le calcul, on interprète le mot compute partout dans la formule et sur le résultat.
On n'utilise pas de règles supplémentaire.
Problème
Pour modifier la 1-formule retournée et interpréter partout compute, il est nécessaire d'avoir un "compute" comme dans l'essai 4, sinon le calcul s'arrête à la première application.
essai 4
Idée
On calcule les formules différement : quand on est dans le cas "distribute x y \ compute z" (où compute est un nouveau mot clé), alors on commence par calculer z.
compute vs cdistribute
On pourrait aussi définit cdistribute qui fait comme distribute mais avec le calcul du dernier argument avant. Mais compute s'adapte mieux à de futurs notations.
Postulat
- Tout ce qui existe a une cause, qui existe, et qui est un calcul.
- Tous les calculs existent.
Exemples sur les entiers naturels
$Def f = $F l,n → f( compute \ l +le n , compute \ n + 1 )
f est traduite par un distribute, donc le calcul de n + 1 est fait.
Donc le calcul de "f ∅l 0" comporte une liste $L[ 0, ..., n ] à différents endroits dans la formule calculée suivant la phase de la boucle récursive.
Comme le calcul est infini (du fait qu'il est effectif) il ne retourne jamais.
compute vs le partage de valeur
Est-ce que le calcul par partage de valeur est toujours suppérieur au mot clé compute ?
Si on boucle 1000 fois pour ajouter 0b à une liste, le processus normal sera de retourner une formule où le calcul est symbolique (ce qui est plus gros). Ce calcul symbolique ne sert à rien si on utilise vraiment la valeur.
Donc on voit que compute peut parfois être supérieur au partage de valeur : quand on est sûr d'utiliser le résultat et que la version symbolique est plus lourde. La lourdeur de la version symbolique n'est pas évidente car le partage de valeur peut réduire la lourdeur réelle.
Conclusion :
compute et le postulat
Question : pourquoi on a besoin d'un calcul différent pour le postulat ?
Ce qui détermine en temps normal les parties calculées sont les besoins (extérieurs aux calculs) de connaître les valeurs. Ce n'est pas le cas quand le calcul est l'origine de l'existence car il n'y a pas d'extérieur. Il faut alors inclure dans les formules les indications de ce qui doit être calculé.
Permettre "compute" partout ?
Il me parait assé facile d'ajouter le traitement de compute pour tout argument de l'application que l'on veut exécuter, même si ça n'a pas d'intérêt pour le "if".
Pour la règle "distribute x y z = (x z) (y z)", que faire si on veut que y soit calculé ? Comme y est une fonction, ce serait bizarre de vouloir la calculer. Par contre on pourrait vouloir calculer "y z". Dans ce cas on change la fonction pour que le résultat soit (x z) (compute \ y z) , qui sera alors calculer puisque c'est un argument d'une application.
Voir l'étude "nouveau mot clé compute".
essai 3
Idée
On calcule les formules différement : quand on est dans le cas "distribute x y z", on commence par calculer z. C'est très proche de l'évaluation stricte puisque l'argument est calculé en premier.
Le problème des calculs infinis
Si le calcul de z est infini alors on ne passe pas à la suite, alors qu'il est possible que z soit ignoré par la suite.
Est-ce compatible avec la définition de recurse ?
On a
$Def selfx = $F f,x → f \ x x
$Def recurse = $F f → selfx f \ selfx f
Donc
recurse f
→c selfx f \ selfx f
→c f \ selfx f \ selfx f
→c f \ f \ selfx f \ selfx f
→c f \ f \ f \ selfx f \ selfx f
Donc non.
Le problème des calculs inutils
Cette solution est moins bien que de lier les deux formules résultant du dédoublement car avec la liaison on ne calcule qu'une fois et seulement si c'est nécessaire, système utilisé par l'interpréteur lazi "compute". Mais dans le cadre du paradigme cela n'a pas d'importance.
essai 2
Idée
On ajoute un nouveau mot pour que les valeurs soient calculées ? Un mot "compute" qui calcule son argument puis si c'est une paire calcule les deux arguments de la paire. En plaçant judicieusement des "compute" on peut ainsi calculer toute une structure.
Problème:
essai 1
Le postulat
La valeur en entrée d'un calcul est un couple de formules f,d dont l'une est la fonction et l'autre la valeur.
Le calcul est représenté par $T[ f0 d, $T[ f1 d, $T[ f2 d, ...
- Tout ce qui existe a une cause, qui existe, et qui est un calcul.
- Tous les calculs existent.
Equivalence avec le calcul d'une fonction
Soit g une fonction, soit g1 la 1-formule représentant g. Alors le couple $T[compute,g1] produit les étapes du calcul de g. Donc le nouveau paradigme permet de calculer n'importe quelle formule. On peut même interpréter les différentes valeurs pour passer des 1-formules à des 0-formules.
Soit $T[f,d] un couple de formules, soit
$Def g = $F x → $T[ x, g \ f x ]
alors le calcul par l'ancienne définition de g retourne la même chose qu'avec la nouvelle définition sur $T[f,d]
Effectivité des calculs
Chaque valeur de la liste infini est calculée, donc le calcul est effectif.
Reproductivité
Question : est-ce que l'on peut générer d'autres calculs effectifs sur tout un ensemble de couples $T[fonction, donnée] ?
Le problème est que pour chaque valeur calculée, si elle contient une structure alors les valeurs internes ne sont pas calculées. Par exemple si pour deux couples $T[ f1, d1 ], $T[ f2, d2 ] on veut calculer
$T[ $T[ d1, d2 ], $T[ f1 d1, f2 d2 ], , $T[ f1 \ f1 d1, f2 \ f2 d2 ] ]
Conclusion
Ça ne résoud pas le problème car pour chaque nœud du calcul on retombe sur le problème de l'effectivité du calcul.
Réponse
Le calcul ne peut être retourné (car il nécessite une infinité de calcul élémentaires). Il doit donc exister lors du calcul, qui est infini. Avec l'évaluation actuelle il est impossible d'avoir un calcul effectif où les données ne sont pas temporaires et morcelées. Il faut donc changer la forme de calcul, voir l'essai 6 : évaluation loose.