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 :

Si les calculs entre les différentes formules ne sont pas séparés de manière à équilibrer le nombre des calculs par formules :

Les formules s'agrandissant beaucoup (par exemple en produisant toutes les formules de profondeur < n, ce que l'on peut faire en produisant d'abord des représentations de formules puis en les interprétant) seront alors beaucoup plus calculées que les autres. Il en résulte que cela favorise les formules ayant tendance à produire des formules. Donc les choses produites auront tendance à produire des formules par pression sélective. Ce qui nuit à avoir une pression sélective basée sur l'efficacité du calcul, ce qui nuit à la cohérence. À faire : établir la relation entre l'efficacité et la cohérence.

Solution : faires les calculs à tour de rôle, pour cela préparer la liste des formules ayant subit un calcul élémentaire et équilibrer entre les calculs.

Équilibrer les calculs inutils entre les formules :

Une formule qui a au départ deux fois plus de sous-calculs qu'une autre génèrera deux fois plus de formules. Donc pour la suite il y aura aussi deux fois plus de formules (en supposant que par la suite le nombre de sous-formules à calculer est identique). On voit que l'on a alors un déséquilibre de nombre de calculs élémentaire entre deux formules à cause du nombre de sous-formules que l'on peut calculer.
Solution :

On change de mode de calcul : on exécute un calcul élémentaire pour toute sous-formule, le résultat d'un calcul étant intégré dans la formule pour le calcul suivant. On passe donc du mode parallèle au mode sérialisé.
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 :

Ça peut servir dans certain cas qui, pour l'instant, me paraissent assez rares pour ne pas à avoir à s'en occuper.

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:

Si on calcule en appliquant les compute alors si la structure est infinie la fonction ne retourne rien.

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[ f⁰ d, $T[ f¹ d, $T[ f² 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.