D’un côté, il y a le calcul : des termes et des opérations algébriques, avec peut-être une stratégie pour appliquer ces opérations, pas à pas. De l’autre, il y a l’ordinateur qui effectue des calculs à grands pas. Et entre les deux, il y a un langage de programmation pour exprimer les calculs à effectuer.
C’est une belle image. Par exemple, on aime bien dire que le lambda-calcul (qui est un calcul, avec des termes, des opérations, et des stratégies) est la fondation des langages fonctionnels. A l’occasion, on exhibe un calcul des objets pour fonder les langages à objets. Mais dans l’implantation des langages de programmation, force est de reconnaitre que le calcul a disparu. Par exemple, pour les langages fonctionnels, la beta-réduction du lambda-calcul n’est plus qu’une métaphore.

Le but de cet exposé est de montrer comment le calcul mathématique se métamorphose en calcul informatique.  En partant d’une représentation du calcul mathématique basée sur la réduction (« reduction-based evaluation »), nous nous libérerons méthodiquement de cette représentation pour aboutir à une représentation du calcul informatique basée sur l’évaluation (« reduction-free evaluation »).