Böhm trees and Taylor expansion
Apparaît dans la collection : Differential $\lambda$-Calculus and Differential Linear Logic, 20 Years Later / $ \lambda $-calcul différentiel et logique linéaire différentielle, 20 ans après
We revise the classical theory of program approximation based on Scott-continuity and Böhm trees. We then present the more recent theory proposed by Ehrhard&Regnier, based on Taylor expansion. We first introduce the resource calculus and its properties, and then the Taylor expansion associating each term with a power series of resource terms. Finally, we show how to apply this technique to prove results in lambda calculus in an easier way.
