Lazi

Définition de la cause d'un calcul

Contexte

La notion de calcul est bien défini, mais pas celle de cause. Une définition informelle est :

Le calcul c est la cause du calcul d ssi c comporte le calcul de d.

Un calcul est constitué :

  • d'une règle de calcul R
  • d'une formule f
  • d'une liste (finie ou non) de premier élément f et où l'élément suivant est le résultat par R du précédant.

Question

Quelle définition formelle peut-on donner à la notion de cause d'un calcul ?

Étude

Bestiaire

Complexité

La cause d'un calcul peut être dans un univers à particule, un ordinateur virtualise un ordinateur qui réalise un calcul.

La triche

Si on définit "x est cause de y" par le fait qu'il existe une fonction f qui calcule y à partir des éléments isols de x, alors il suffit que f reprère un compteur dans les éléments de x pour calculer y simplement à partir du compteur.

Le flou

On peut avoir une mathématique où pour représenter un bit on utilise un ensemble de bit et l'on compte le pourcentage de 0 et de 1 pour déterminer si c'est un 0b ou un 1b.

Cela montre que la traduction d'un binaire de lazi.1 peut se traduire en quelque chose que l'on ne pas intrinsèquement pas ramener à un binaire. Il y a donc une possible complexité irréductible dans la reconnaissance des calculs.

Différenciation des données

Si on ne différencie pas les données, alors la cause d'un calcul doit être la "virtualisation" dans un calcul plus grand de ce calcul, c'est à dire que la moindre variation de la manière de calculer fait que le calcul n'est pas reconnu. Cela serait trop restrictif car la manière dont le calcul est fait n'a pas de conséquences sur les données, il serait donc illogique de chercher une forme particulière alors que la manière de calculer n'a pas d'incidence. On doit donc définir la notion de donnée d'un calcul.
Mais alors autant abandonner, dans la définition actuelle du calcul, la notion d'égalité (de règle de calcul), et considérer qu'un calcul est une liste (finie ou non).

Si on définit que x est la cause de y par le fait qu'il existe une fonction f qui transforme certains éléments de x en éléments de y, dans le même ordre, il faut ajouter une condition pour éviter le cas "triche", c'est à dire pour éviter que ce soit f qui soit en fait la cause du calcul. Pour cela on peut ajouter la condition que f a un temps de calcul en o(1) par rapport à la quantité taille des formules de x. Mais alors on limite la définition aux calculs infinis.

Quel sens pour la notion de cause pour les calculs finis ?

Avec la définition ci-dessus, quasiment tout calcul assez long comportant un timer est la cause d'un calcul fini.

Isolation

Il faut que l'on puisse isoler un calcul à l'intérieur du calcul.
Par exemple dans notre univers, si une personne éxécute un calcul sur une calculatrice, il n'y a pas de sous-formule de notre univers qui soit un calcul indépendant et qui représente ce calcul. Cela est dû au fait qu'il n'y a pas de réelle isolation dans notre univers. Donc on ne peut pas voir le calcul éxécuté par la calculatrice comme un calcul au sens Lazi ayant pour cause notre univers.

Déterminer des sous-parties

Pour définir un sous-calcul d'un calcul il faut déterminer une sous-partie de la formule calculée. Cela ne va pas de soi car on peut avoir affaire à des extensions de formules. Il faut un système de chemin pour indiquer la zone de la formule, car on ne peut pas se contenter du fait qu'une sous-formule existe quelque part.

Sauter des étapes

Le calcul principal peut avancer plus lentement que le sous-calcul que l'on veut définir. Il faut donc quelque part "sauter des étapes". On ne peut juste fournir un chemin pour déterminer le sous-calcul, car on ne peut pas éliminer les sous-formules qui ont la même valeur que la précédante (car un calcul peut converger vers une valeur constante).

Triche de la fonction définissant le sous-calcul ?

Dans un calcul assez gros, on peut toujours attendre et trouver quelque part certaines valeurs pour trouver les formules souhaitées et définir le sous-calcul.

Pour éviter cela, il faudrait une notion de continuité de manière à ne pas avoir de saut dans les endroits où sont pris les formules du sous-calcul.
Mais comme les formules changent de position lors des calculs, il faudrait une notion de traçage de ces endroits. Même si le système est complexe, tant qu'il y a copie d'information le seul mécanisme est distribute, donc on peut tracer les copies. Par contre il faut que la mathématique définisse comment réaliser ce traçage.

Avec un système de traçage plutôt que de désignation par chemin, il me parait possible de seulement indiquer le chemin de la sous-formule au départ :

Quand il y a duplication, on vérifie dans les deux exemplaires si le calcul continue.
Quand le calcul n'avance pas, on attend qu'il avance.

Essai 1

Définition de : le calcul C est une cause du calcul D

Soit C un calcul de chemin mathématique Cm et de formule de départ f.
Soit D un calcul de chemin mathématique Dm.
On dit que D est un sous calcul de C ssi :

  • Dm est une extension de Cm
  • Il existe g une sous-formule de f tq :
    • g est une formule de Dm
    • la trace de g dans le calcul C contient le calcul de g par D.

Définition de : la trace de g dans le calcul C

Soit C un calcul de formule de départ f0. Soit la suite fn la suite des formules pour le calcul de la formule f0.
Soit g tel qu'il existe k∈ℕ tq g soit une sous-formule de fk.
La trace de g

Réponse

@todo