Théorème de l'évaluation lazy en O(1)
Contexte
Pour l'étude d'un postulat simplifié on a besoin de montrer qu'en moyenne l'évaluation d'un calcul élémentaire au cours d'une interprétation lazy est en O(1) par rapport au nombre de calculs élémentaires de l'interpréteur. On peut résumer ce théorème par "la virtualisation est peu coûteuse". C'est important car la virtualisation permet l'inovation par l'introduction de nouvelles fonctionalités. Il est important que l'innovation soit rentable car sans elle le calcul brut l'emporterait ce qui nuirait à la structuration des choses.
Énoncé
Variables
f
Conditions
f est une 1-formule lazy dont le calcul est infini.
Conclusion
Soit e une fonction lazi d'évaluation paresseuse (c'est à dire de calcul univocal) de 1-formules.
Le ratio entre le nombre de calculs élémentaires de e calculant f et le nombre de calculs élémentaires effectués sur f par e est en O(1).
Preuve
On décompose un calcul univocal en les opérations suivante :
- calculer un if avec en condition 1b ou 0b
- calculer un distribute
- passer au calcul de la condition d'un if
- revenir au calcul d'un if après le calcul de la condition
- empiler un argument (quand il y a trop d'arguments)
- dépiler un argument (quand on manque d'argument)
On peut représenter un calcul univocal par une liste des opérations décrites ci-dessus. Comme on a déjà une représentation d'un calcul univocal, appelons celle-ci un calcul univocal détaillé. Pour montrer que le nombre de calcul élémentaire nécessaires pour effectuer un calcul univocal est en moyenne en O(1) par rapport au nombre de calcul élémentaires effectués dans le calcul, il nous suffit de montrer que la longueur de la liste représentant le calcul univocal détaillé est en moyenne en O(1) par rapport au nombre de calcul élémentaires dans le calcul. En effet, chaque opération élémentaire du calcul univocal détaillé nécessite un nombre constant de calculs élémentaires pour être effectuée.
Seules les opérations 1 et 2 de la liste ci-dessus correspondent à des calculs élémentaires sur la formule à calculer. Donc il faut qu'en moyenne la proportion de ces deux opérations soient en O(1) par rapport à l'ensemble des opérations.
Pour chaque opérations sans calul élémentaire (de 3 à 6), nous allons montrer qu'il existe un calcul élémentaire associé qui n'est associé qu'à un maximum de deux opérations sans calul élémentaire. Ainsi cela impliquera une proportion minimale fixée entre les opérations sans calcul élémentaire et celles avec :
- passer au calcul de la condition d'un if
Si le calcul de la condition est infini :
S'il y a un nombre infini d'opérations dans ce cas alors la formule résultant du calcul partiel grossit indéfiniment avec des if imbriqués par la condition. Lsors d'un calcul distribute est la seule opération faisant grossir une formule. Il nous suffit donc de montrer que distribute ne peut augmenter que de 1 le nombre d'imbrication de if par la condition.
Voici un exemple illustrant ce cas :
Dans distribute x y z les fils d'imbrication sont inclus dans l'un des 3 arguments.
Dans "(x z) (y z)" :
- Si le plus grand fil est dans x z ou y z : on raisonne comme ci-dessus.
- revenir au calcul d'un if après le calcul de la condition
- empiler un argument (quand il y a trop d'arguments)
- dépiler un argument (quand on manque d'argument)
Recherche d'une preuve
Recherche d'un contre-exemple
Soit f = if 1b f x1 x2 ... xn, est-ce que l'exécution lazy de f n'est pas en O(1) ?
f = recurse $F f → if 1b f x1 x2 ... xn
L'interprétation de la partie "recurse" est constante, ce qu'il faut voir est la partie "distribute" :
Essai de preuve 4 (validé)
On décompose un calcul univocal en les opérations suivante :
- calculer un if avec en condition 1b ou 0b
- calculer un distribute
- passer au calcul de la condition d'un if
- revenir au calcul d'un if après le calcul de la condition
- empiler un argument (quand il y a trop d'arguments)
- dépiler un argument (quand on manque d'argument)
On peut représenter un calcul univocal par une liste des opérations décrites ci-dessus. Comme on a déjà une représentation d'un calcul univocal, appelons celle-ci un calcul univocal détaillé. Pour montrer que le nombre de calcul élémentaire nécessaires pour effectuer un calcul univocal est en moyenne en O(1) par rapport au nombre de calcul élémentaires effectués dans le calcul, il nous suffit de montrer que la longueur de la liste représentant le calcul univocal détaillé est en moyenne en O(1) par rapport au nombre de calcul élémentaires dans le calcul. En effet, chaque opération élémentaire du calcul univocal détaillé nécessite un nombre constant de calculs élémentaires pour être effectuée.
Seules les opérations 1 et 2 de la liste ci-dessus correspondent à des calculs élémentaires sur la formule à calculer. Donc il faut qu'en moyenne la proportion de ces deux opérations soient en O(1) par rapport à l'ensemble des opérations.
Pour chaque opérations sans calul élémentaire (de 3 à 6), nous allons montrer qu'il existe un calcul élémentaire associé qui n'est associé qu'à un maximum de deux opérations sans calul élémentaire. Ainsi cela impliquera une proportion minimale fixée entre les opérations sans calcul élémentaire et celles avec :
- passer au calcul de la condition d'un if
Si le calcul de la condition est infini :
S'il y a un nombre infini d'opérations dans ce cas alors la formule résultant du calcul partiel grossit indéfiniment avec des if imbriqués par la condition. Lsors d'un calcul distribute est la seule opération faisant grossir une formule. Il nous suffit donc de montrer que distribute ne peut augmenter que de 1 le nombre d'imbrication de if par la condition.
Voici un exemple illustrant ce cas :
Dans distribute x y z les fils d'imbrication sont inclus dans l'un des 3 arguments.
Dans "(x z) (y z)" :
- Si le plus grand fil est dans x z ou y z : on raisonne comme ci-dessus.
- revenir au calcul d'un if après le calcul de la condition
- empiler un argument (quand il y a trop d'arguments)
- dépiler un argument (quand on manque d'argument)
Essai de preuve 3
On décompose un calcul univocal en les opérations suivante :
- calculer un if avec en condition 1b ou 0b
- calculer un distribute
- passer au calcul de la condition d'un if
- revenir au calcul d'un if après le calcul de la condition
- empiler un argument (quand il y a trop d'arguments)
- dépiler un argument (quand on manque d'argument)
On peut représenter un calcul univocal par une liste des opérations décrites ci-dessus. Comme on a déjà une représentation d'un calcul univocal, appelons celle-ci un calcul univocal détaillé. Pour montrer que le nombre de calcul élémentaire nécessaires pour effectuer un calcul univocal est en moyenne en O(1) par rapport au nombre de calcul élémentaires effectués dans le calcul, il nous suffit de montrer que la longueur de la liste représentant le calcul univocal détaillé est en moyenne en O(1) par rapport au nombre de calcul élémentaires dans le calcul. En effet, chaque opération élémentaire du calcul univocal détaillé nécessite un nombre constant de calculs élémentaires pour être effectuée.
Seules les opérations 1 et 2 de la liste ci-dessus correspondent à des calculs élémentaires sur la formule à calculer. Donc il faut qu'en moyenne la proportion de ces deux opérations soient en O(1) par rapport à l'ensemble des opérations.
Résumé du raisonnement :
Soit l'hypothèse de récurrence H(n) :
- nce le nombre de calculs élémentaires de cud (opérations 1 et 2)
- nno le nombre d'opérations de cud qui ne sont pas des calculs élémentaires (opérations 3 à 6)
- apf le nombre d'applications de f
Prouvons H(1) :
Supposons que pour toute longueur de cud n < N on ait H(n), montrons alors que l'on a H(N) :
- Si c'est un empilement : à finir
b) empilement + calcul de la partie fonction + dépilement + calcul
Par hypothèse de récurrence on a 2 × nce1 + apf1 ≥ nno1 et 2 × nce2 + apf2 ≥ nno2.
Le problème est que apf2 peut être énorme car c'est le résultat du calcul de la fonction.
Changement d'idée : un dépilement correspond forcément à un calcul élémentaire, voir l'essai 4.
Essai de preuve 2
On décompose l'évaluation en les opérations suivante :
- passer au calcul de la condition d'un if
- calculer un if avec en condition 1b ou 0b
- calculer un duplicate
- empiler un argument (quand il y a trop d'arguments)
- dépiler un argument (quand on manque d'argument)
Raisonnons sur le nombre d'applications de la sous-formule évaluée :
- Il diminue quand on enlève un argument et quand on applique un if.
- Il diminue quand on passe au calcul de la condition d'un if.
- Quand on ajoute un argument, il augmente.
- Quand on applique un duplicate, il reste constant (ssi z est un mot) ou augmente strictement.
Le nombre d'application de la formule globale calculée ne peut augmenter que par le calcul d'un duplicate. L'évaluation du résultat (x z) (y z)peut amener à deux empilements (y z et z) avant d'arriver au calcul de x.
Hypothèse de récurrence :
- e le nombre d'empilements dans ca
- c le nombre de calculs élémentaires
- ap le nombre d'applications
Raisonnons par récurrence sur ap.
Si ap ≤ 3 alors c = 0 ou c = 1 et e = 0, donc l'inégalité est vérifiée.
Supposons que l'hypothèse de récurrence soit vraie dans tous les cas où ap ≤ aph, et prouvons le pour ap = aph + 1.
Soit caf la partie du calcul avant le dépilement (où jusqu'à la fin s'il n'y a pas de dépilement de l'argument). Soit ef et cf respectivement le nombre d'empilement et de calculs élémentaires dans caf. Par récurrence on a 2 × cf + apf ≥ ef.
S'il n'y a pas de dépilement du premier argument :
Problème
Le problème est que l'on ne peut pas appliquer la récurrence car le calcul peut passer par des formules ayant plus d'application.
Il semblerait meilleur de faire la récurrence sur les instructions utilisées par l'évaluation.
Essai de preuve 1
Lors d'un calcul lazy, ce qui peut rendre le calcul non O(1) est quand on se restreint à la partie fonction d'une application, car il peut y avoir un nombre quelconque d'application.
Quand on se restreint on diminue la profondeur de la sous-formule que l'on veut calculer (faux). On ne peut le faire qu'un nombre de fois limité, sauf quand on cré de la profondeur par "distribute x y z →c[univocal] (x z) (y z)", où l'on passe de la profondeur (pr est la fonction mesurant la profondeur d'une formule)
1 + max (pr(z), 1 + max(pr(y), 1 + pr(x)))
à
1 + max( 1 + max( pr(x),pr(z) ) ; 1 + max( pr(y),pr(z) ) )
La profondeur peut augmenter de 1 si pr(z) ≥ 2 + pr(x) ∧ pr(z) ≥ 1 + pr(y)
Il ne peut y avoir une augmentation >1.
En conclusion chaque augmentation de la profondeur est de 1 au maximum et correspond à un calcul élémentaire.
Les démantèlements d'applications correspondent à une diminution de la profondeur de la partie examinée. Comme la diminution de profondeur de la partie examinée est limité par la profondeur de départ, et que l'augmentation ne peut se faire que par incrémentation correspondant à une calcul élémentaire, on en déduit que le nombre de démantèlement est en O(1) par rapport au calcul élémentaire.
Abandonné (voir le "faux" surligné)