L'objectif est de faire le lien entre deux avatars de la réduction optimale. L'un concerne la réduction faible du λ-calcul, l'autre la récriture du premier ordre, et tous deux se démarquent de la théorie générale par une même agréable propriété : on peut les implémenter simplement avec des graphes acycliques.

Je commencerai par présenter les principes de la réduction optimale tels qu'introduits par Lévy, en insistant sur leurs liens avec les notions d'événement et de causalité.

On interprétera ensuite dans ce cadre le λ-lifting, un procédé de compilation classique assurant le passage du λ-calcul à la récriture du premier ordre. On verra que cette transformation peut être vue comme un événement “silencieux”, causalement transparent, et respectueux de l'optimalité, et on en profitera pour réaliser quelques transferts de propriétés.