5.2   Règles d'évaluation

• Var
  E(x) = vE|- x Þ v
  Une variable vaut sa valeur dans son environnement de calcul. Si la variable n'était pas liée, le vérificateur n'aurait pas pu typer l'expression.
• (Pair)
  E|- e₁ Þ v₁ E|- e₂ Þ v₂ E|- (e₁,e₂) Þ (v₁,v₂)
  
  
• (List)
  E|- e₁ Þ v₁ E|- e₂ Þ v₂ E|- e₁::e₂ Þ v₁::v₂
• (If1)
  E|- e₁ : true E|- e₂ : v₂ E|- (if e₁ then e₂ else e₃) Þ v₂
  
  On évalue d'abord la condition. Selon sa valeur la branche gauche (If1) ou droite (If2) est évaluée.
  
  
• (If2)
  E|- e₁ : false E|- e₃ : v₃ E|- (if e₁ then e₂ else e₃) Þ v₃
  
  
• (Abs)
  E|- (function x -> e) Þ <E,(function x -> e)>
  Une abstraction crée une fermeture (couple environnement E, expression fonctionnelle). Ainsi toutes les variables libres du corps de la fonction sont liées à l'environnement E.
  
  
• (App)
  E|- e₁ Þ <E₁,(function x -> e)> E|- e₂ Þ v₂ (x:v₂)::E₁|- e Þ v E|- (e₁ e₂) Þ v
  
  L'évaluation du corps d'une fermeture s'effectue toujours dans l'environnement de la fermeture.
  
  
• (Let)
  E|- e₁ Þ v₁ (x:v₁)::E|- e₂ Þ v₂ E|- let x = e₁ in e₂ Þ v₂
  Une déclaration locale augmente l'environnement de calcul du corps de l'expression.
  
  
• (LetRec)
  E₁=(f:<E₁,(function x -> e)>)::E|- e₂ Þ v₂ E|- let rec f = e₁ in e₂ Þ v₂
  
  Il y a une difficulté pour construire l'environnement E₁ de la fermeture f. En effet cet environnement doit contenir f dans la liste des variables car f peut apparaitre dans son corps.