Lambda-calcul et langages fonctionnels

Jean Goubault-Larrecq

Abstract: Ceci est la version 3 de la première partie du cours de lambda-calcul, datant du 28 janvier 2011. La version 2 datait du 04 mars 2009. La première version datait du 02 août 1999. Bizarrement, je n'avais pas remarqué l'erreur présente depuis dix ans dans la démonstration du théorème de standardisation. Merci à Arthur Milchior.
Un langage fonctionnel est juste un langage dans lequel la notion de fonction (procédure, sous-programme) est centrale. Cette définition vague recouvre les langages fonctionnels dits purs, dans lesquels tout calcul est effectué au moyen d'appels de fonctions (Miranda, Haskell, par exemple); et les langages fonctionnels impératifs (Lisp, ML), dans lesquels il est aussi permis d'effectuer des effets de bord (affectations), comme en Pascal ou en C.

Pour prendre un exemple, en OCaml, on peut définir la factorielle par: 
let rec fact n = if n=0 then 1 else n*fact (n-1);;
et calculer la factorielle de 10 en demandant: 
fact 10;;
ce à quoi le système répond 3628800. On a donc défini la fonction fact par une définition proche de la notion mathématique usuelle:
n! =def ⎧
⎨
⎩
1 si n=0
n × (n−1)! sinon
où =def dénote l'égalité par définition.

Les ingrédients de cette définition sont, d'abord, l'absence d'affectation à des variables, contrairement au programme C typique réalisant la même fonction: 
int fact (int n)
{
  int res, i;

  for (res = 1, i = 1; i<=n; i++)
    res *= i;
  return res;
}
ensuite, la définition de fact par une expression utilisant fact elle-même — ce qu'on appelle une définition récursive. On pourrait d'ailleurs faire la même chose en C: 
int fact (int n)
{
  if (n==0)
    return 1;
  return n * fact (n-1);
}
ce qui montre que C est lui-même un langage fonctionnel, selon notre définition.

Le point intéressant dans ces petits exemples, et que nous développerons, est que la notion de fonction est une notion importante en programmation. En fait, elle est tellement fondamentale qu'on peut fonder un langage de programmation universel (au sens où une machine de Turing est universelle) sur la seule notion de fonction: c'est le λ-calcul pur, que nous allons étudier dans ce chapitre. Le λ-calcul est aujourd'hui un outil central en informatique et en logique: en fait, la sémantique des langages de programmation, la formalisation des logiques d'ordre supérieur ou de la déduction naturelle bénéficient directement des concepts inhérents au λ-calcul.

Nous examinons principalement le λ-calcul pur dans ce chapitre. Nous en donnons la définition en section 1, prouvons certaines de ses propriétés les plus importantes en section 2, puis nous dégageons les quelques stratégies de réduction les plus caractéristiques des langages de programmation actuels en section 3. Nous définissons ensuite des modèles mathématiques des programmes du λ-calcul (les λ-termes) en section 4, ce qui nous permettra de raisonner sémantiquement sur les programmes. Finalement, nous introduirons la notion de continuation en section 5, en profiterons pour faire le lien entre sémantiques dénotationnelles en style de passage de continuations et stratégies de réduction.

This document was translated from LATEX by HEVEA.