Terminaison

Terminaison

Mathématique	Caml-Light
Ensemble inductif	type récursif
fonction récursive	fonction récursive

type arbre_bin = 
  | Feuille of int
  | Noeud of (arbre_bin * arbre_bin) ;;

let rec it_arbre = fun op -> function arbre -> 
  match arbre with
    | Feuille n -> n
    | Noeud (fg,fd) -> 
      op (it_arbre op fg) (it_arbre op fd) ;;

On n'explicite pas les environnements, les expressions, les valeurs !

On identifie les fermetures et leurs noms, les paramètres et leurs valeurs

Par induction on a deux cas :

l'arbre est une feuille et
it_arbre(F, Feuillen) vaut n
on suppose que A₁ et A₂ sont des arbre_bin tels que :
- it_arbre(F , A₁) = a₁
- it_arbre(F,A₂) = a₂
La valeur de it_arbre(F,Noeud(A₁,A₂)) est alors F(a₁,a₂).