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

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 fini : on a alors à la suite une opération 4, qui a une opération 1 associée.
Si le calcul de la condition est infini :

S'il n'y a qu'un nombre fini d'opérations dans ce cas alors cela n'a pas d'influence sur la proportion.
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 :

"recurse $F c → if c 1b 0b", dans cet exemple on voit que l'on a lors du calcul une imbrication infinie de if, mais pour chaque niveau il est nécessaire de calculer plusieurs distribute. Remarquons qu'imbriquer plusieurs if comme ceci "recurse $F c → if (if c 1b 0b) 1b 0b" ne change rien car cela augmente le nombre de distribute nécessaires.

Le raisonnement général est le suivant :

Soit n (respectivement m) la taille maximale des fils d'imbrications de if dans "distribute x y z" (respectivement "(x z) (y z)").
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 toute la formule alors (y z) est le dernier argument du if et z l'avant dernier et donc x contient en condition un fil de taille m-1.
- Si le plus grand fil est dans x z ou y z : on raisonne comme ci-dessus.

Donc m = n ou m = n + 1.

revenir au calcul d'un if après le calcul de la condition

Puisque le cacul global est infini, cela implique que le résultat du calcul de la condition est 0b ou 1b et que l'on applique une opération 1 (calculer un if avec en condition 1b ou 0b).

empiler un argument (quand il y a trop d'arguments)

- Si l'argument est dépilé plus tard :

alors il est associé à l'opération 6 qui est elle-même associé au final à un calcul élémentaire (voir le cas 6 ci-dessous).

- Si l'argument n'est jamais dépilé mais que lors du calcul seuls un nombre fini d'arguments ne sont jamais dépilés :

alors comme on a un nombre fini d'opérations cela n'a pas d'influence sur les proportions puisque le calcul est infini.

- Si il existe une infinité d'arguments jamais dépilés :

Cela implique que les résultats intermédiaires du calcul grossissent indéfiniment. Nous pouvons faire pour ce cas un raisonnement similaire à celui portant sur les imbrications de if, mais ici nous comptons le nombre maximal d'arguments des sous-formule (d'un même fil d'arguments). Nous voyons que l'on a n ≤ m ≤ n + 2 (deux arguments sont ajoutés à x dans "(x z) (y z)").

dépiler un argument (quand on manque d'argument)

L'opération suite à un dépilement est forcément 1, 2 ou 3. Si c'est 1 ou 2 on a alors une opération correspondant à un calcul élémentaire associée. Si c'est 3 alors nous avons vu qu'il est associé à une opération correspondant à un calcul élémentaire.

Recherche d'une preuve

Recherche d'un contre-exemple

Soit f = if 1b f x₁ x₂ ... x_n, est-ce que l'exécution lazy de f n'est pas en O(1) ?

Si on néglige la partie récursive c'est le cas. Regardons en détail la partie récursive :
f = recurse $F f → if 1b f x₁ x₂ ... x_n
L'interprétation de la partie "recurse" est constante, ce qu'il faut voir est la partie "distribute" :

$F f → if 1b f x₁ x₂ ... x_n = distribute ($F f → if 1b f x₁ x₂ ... x_n-1; constF x_n)

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)

passer au calcul de la condition d'un if

Si le calcul de la condition est fini : on a alors à la suite une opération 4, qui a une opération 1 associée.
Si le calcul de la condition est infini :

Le raisonnement général est le suivant :

Donc m = n ou m = n + 1.

revenir au calcul d'un if après le calcul de la condition

Puisque le cacul global est infini, cela implique que le résultat du calcul de la condition est 0b ou 1b et que l'on applique une opération 1 (calculer un if avec en condition 1b ou 0b).

empiler un argument (quand il y a trop d'arguments)

- Si l'argument est dépilé plus tard :

alors il est associé à l'opération 6 qui est elle-même associé au final à un calcul élémentaire (voir le cas 6 ci-dessous).

- Si l'argument n'est jamais dépilé mais que lors du calcul seuls un nombre fini d'arguments ne sont jamais dépilés :

alors comme on a un nombre fini d'opérations cela n'a pas d'influence sur les proportions puisque le calcul est infini.

- Si il existe une infinité d'arguments jamais dépilés :

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)

Résumé du raisonnement :

Seul duplicate peut augmenter le nombre d'applications de la formule et un duplicate ne peut engendrer par lui-même que deux opérations sans calcul élémentaire. Donc mis à part la formule de départ, qui ne peut engendrer qu'un nombre fini d'opération sans calcul élémentaire, on a un ratio maximum de deux opérations sans calcul élémentaire pour un calcul élémentaire.

Soit l'hypothèse de récurrence H(n) :

Soient :

- cud un calcul univocal détaillé de longueur n sur une formule f
- 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

Alors 2 × nce + apf ≥ nno

Prouvons H(1) :

Comme nno ≤ 1 et apf ≥ 1 et nce ≥ 0, on a 2 × nce + apf ≥ 1 ≥ nno, donc on a H(1).

Supposons que pour toute longueur de cud n < N on ait H(n), montrons alors que l'on a H(N) :

Raisonnons suivant la première opération de cud :

1) calculer un if avec en condition 1b ou 0b

Soit apf2 le nombre d'applications de la formule résultant du calcul du if, on a apf2 ≤ apf - 2 (à cause des 2 applications provenant du if). Par récurrence on a 2 × ( nce -1) + apf2 ≥ nno, donc 2 × nce + (apf2 + 2) - 4 ≥ nno, donc 2 × nce + apf - 4 ≥ nno, donc 2 × nce + apf ≥ nno.

2) calculer un duplicate

Nous allons différencier suivant l'opération suivante :

- S'il n'y a pas d'opération suivante on a alors nno = 0, donc l'inégalité est évidente.
- Si c'est un empilement : à finir

5) empiler un argument (quand il y a trop d'arguments)

Alors on peut décomposer le calcul cud en 2 ou 4 partie :

a) empilement + calcul de la partie fonction
b) empilement + calcul de la partie fonction + dépilement + calcul

Soit cud1 et cud2 les calcul univocal détaillés de respectivment la partie fonction et du résultat du calcul de la partie fonction avec l'argument. Soit les variables correspondantes nce1, nce2 etc.
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 :

Soient :

- ca un calcul univocal sur une formule f
- e le nombre d'empilements dans ca
- c le nombre de calculs élémentaires
- ap le nombre d'applications

Alors 2 × c + ap ≥ e

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.

Si l'évaluation commence par un if :

On peut alors diviser le caclul en deux étapes : calculer la condition puis le résultat du if. Ces deux étapes sont indépendantes et c, ap ou e sont l'addition de ces deux étapes. Comme l'inégalité est linéaire, l'hypothèse de récurrence appliquées aux deux partie reste vraie pour la totalité.

Si l'évaluation commence par un empilement :

Soit apa le nombre d'application de l'argument et apf le nombre d'application de la formule. On a apa + apf + 1 = ap.
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 :

On a alors e = ef + 1, c = cf, apf + 1 ≤ ap, donc 2 × c + apf ≥ e - 1 et 2 × c + ap ≥ 2 × c + apf + 1, d'où 2 × c + ap -1 ≥ e - 1 et donc 2 × c + ap ≥ e

S'il y a dépilement du premier argument :

Si l'évaluation commence par un distribute :

On passe donc d'une formule distribute x y z à (x z) (y z). S'il suit un dépilement, comme "x z" a un nombre inférieur d'application on peut utiliser l'hypothèse de récurrence. Il en est de même s'il suit une évaluation d'un "if" car les différentes parties (la condition et les deux valeurs) ont un nombre d'application ≤ aph.

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é)