Lazi

Calcul avec contexte

Contexte

La méthode consistant à appliquer les règles de calculs totales ne peut pas être optimale du fait que le calcul par étapes indépendantes (sans contexte) pénalise l'efficacité, par exemple quand on en est au calcul d'une sous-formule profonde, il faut à chaque étape réanalyser la formule pour retrouver la sous-formule, puis reconstruire la formule globale. Il y a donc une forte pénalité à découper en calculs élémentaires.

Question

Comment à la fois :

  • voir les calculs comme des déductions
  • avoir la notion de calcul élémentaire
  • permetre d'optimiser le calcul
?

Étude

On peut utiliser un entier pour paramétrer la déduction de calcul sur le nombre de déductions élémentaires à effectuer, ainsi on peut avoir un contexte et éviter les calculs infinis.

Donc on a une règle de calcul par déduction prenant un argument supplémentaire qui est le nombre de calculs élémentaires maximums. Et qui se traduit en preuve composée de calculs élémentaires.

Quand on sait que le calcul est fini, on peut utiliser une règle de calcul qui va jusqu'au bout du calcul. Cette déduction par calcul peut avoir une fonction "domain" qui ne retourne rien si le calcul est infini.

Réponse

Quand on est sûr que le calcul est fini on peut utiliser une règle de calcul finale qui fait tout le calcul. Sinon on peut paramétrer une règle de calcul par le nombre de calculs élémentaires à effectuer.