La lettre de Caml, numéro 6

Les sources des programmes Caml

décompositions d'un entier ; partitions d'un entier et algorithme RSK ; entrées-sorties des lambda-termes et termes de de Bruijn ; lambda-calcul

Retour à la page générale de La lettre de Caml.

Les décompositions d'un entier :

let rec décompose_1 = function
	| 0 -> []
	| 1 -> [[1]]
	| n ->	let res = ref []
			in
			for k = 1 to n - 1 do
				do_list (function l -> res := (k :: l) :: !res)
						(décompose_1 (n - k))
			done ;
			[n] :: !res ;;

let rec décompose_2 n =
	let rec décompose_rec n accu = function
		| 0 ->	accu
		| k ->	let ll = décompose (n - k)
				in
				décompose_rec n ((map (function l -> k :: l) ll) @ accu) (k - 1)
	in
	match n with
		| 0 -> []
		| 1 -> [ [1] ]
		| n -> décompose_rec n [ [n] ] (n - 1) ;;

let rec décompose n =
	let rec gonfle_accu k ll accu =
		match ll with
			| [] -> accu
			| t :: q -> gonfle_accu k q ((k :: t) :: accu)
	in
	let rec décompose_rec n accu = function
		| 0 ->	accu
		| k ->	let ll = décompose (n - k)
				in
				décompose_rec n (gonfle_accu k ll accu) (k - 1)
	in
	match n with
		| 0 -> []
		| 1 -> [ [1] ]
		| n -> décompose_rec n [ [n] ] (n - 1) ;;

Les partitions d'un entier :

#open "format" ;;

(* l'impression sous forme de tableau *)
let print_partition p =
    let rec make_bullets = function
        | 0 -> ""
        | n -> "· " ^ (make_bullets (n - 1))
    in
    let print_n_stars n =
        ( print_string (make_bullets n) ; print_break(0,0) )
    in
    open_vbox 0 ;
    do_list print_n_stars p ;
    close_box () ;;

install_printer "print_partition" ;;

(* la partition 3.2.2.1  |-  8                    *)
(* est représentée par la liste [ 3 ; 2 ; 2 ; 1 ] *)

let somme = it_list (prefix +) 0 ;;

let transpose p =
    let nb_de_plus_grands k liste =
            it_list (fun n x -> if x >= k then n + 1 else n) 0 liste
    in
    let rec intervalle i j =
        if i > j then []
        else i :: (intervalle (i+1) j)
    in
    map (function x -> nb_de_plus_grands x p) (intervalle 1 (hd p)) ;;

let exemple = [ 3 ; 2 ; 2 ; 1 ] ;;
exemple ;; (transpose exemple) ;; (transpose (transpose exemple)) ;;

(* une décomposition de n est une liste de somme n, tout simplement *)

let partition_de_décomposition = sort__sort (prefix >=) ;;

(* je représente -- basiquement -- une permutation de n objets *)
(* par un vecteur des n éléments 0, 1, ..., n-1  *)

let applique_permutation sigma k = sigma.(k) (* calcule sigma(k) *)
and inverse_permutation sigma =
    let n = vect_length sigma
    in
    let res = make_vect n 0
    in
    for i = 0 to n-1 do res.(sigma.(i)) <- i done ;
    res
and compose_permutations s1 s2 = (* calcule évidemment s1 o s2 *)
    let n = vect_length s1
    in
    let res = make_vect n 0
    in
    for i = 0 to n-1 do res.(i) <- s1.(s2.(i)) done ;
    res ;;

let partition_de_permutation sigma =
    let n = vect_length sigma
    and partition = ref []
    in
    let coches = make_vect n false
    in
    for i = 0 to n-1 do if not coches.(i) then
        let j = ref i and longueur = ref 0
        in
        while not coches.(!j) do
            coches.(!j) <- true ;
            incr longueur ;
            j := sigma.(!j)
        done ;
        partition := !longueur :: !partition
    done ;
    partition_de_décomposition !partition ;;

(* --------- génération des partitions ------------- *)

let rec intervalle i j =
    if i > j then []
    else i :: (intervalle (i+1) j) ;;

let partitions n =
    let cons a b = a :: b
    in
    let rec aux n k =
        if k > n then aux n n
        else if k = 0 && n = 0 then [[]]    (* fin normale de récursion *)
        else if k = 0 then []               (* pas de solution ici !    *)
        else it_list (fun l j -> map (cons j) (aux (n-j) j) @ l)
                     []
                     (intervalle 1 k)
    in
    aux n n ;;
    
let partitions_sans_répétition n =
    let cons a b = a :: b
    in
    let rec aux n k =
        if k > n then aux n n
        else if k = 0 && n = 0 then [[]]
        else if k = 0 then []
        else it_list (fun l j -> map (cons j) (aux (n-j) (j-1)) @ l)
                     []
                     (intervalle 1 k)
    in
    aux n n ;;

(* ----- manipulation des partitions sans répétition ---- *)

let rec last = function
    | [] -> failwith "last"
    | [a] -> a
    | t :: q -> last q ;;

let taille_base = last ;;

let rec taille_flanc = function
    | [] -> 0
    | a :: b :: q when a = b + 1 -> 1 + (taille_flanc (b :: q))
    | _ -> 1 ;;

let intersection_BF l = (taille_flanc l) = (list_length l) ;;

type manipulation = BF | FB | NOP ;;

let que_faire l =
    let tf = taille_flanc l
    and tb = taille_base l
    and n  = list_length l
    in
    if (n = tf) && ( (tb = tf) || (tb = 1 + tf)) then NOP
    else if tf >= tb then BF
    else FB ;;

let rec équeute = function (* détruit le dernier élément d'une liste *)
    | [] -> failwith "équeute"
    | [a] -> []
    | t :: q -> t :: (équeute q) ;;

let rec map_borné f k = function
    | [] -> []
    | t :: q when k > 0 -> (f t) :: (map_borné f (k - 1) q)
    | l -> l ;;

let manipule l = match que_faire l with
    | NOP -> l
    | BF -> équeute (map_borné succ (taille_base l) l)
    | FB -> (map_borné pred (taille_flanc l) l) @ [ taille_flanc l ] ;;

exception Stop ;;

let even n = (n mod 2) = 0
and odd  n = (n mod 2) = 1 ;;

let rec nb_de_partitions_naïf n =
    if n < 0 then 0
    else if n < 2 then 1
    else    let résultat = ref 0
            and k = ref 1
            in
            try
            while true do
                let k1 = (!k * (3 * !k - 1)) / 2
                and k2 = (!k * (3 * !k + 1)) / 2
                in
                if k1 > n then raise Stop ;
                if even(!k) then
                    résultat := !résultat
                        - (nb_de_partitions_naïf (n - k1))
                        - (nb_de_partitions_naïf (n - k2))
                else
                    résultat := !résultat
                        + (nb_de_partitions_naïf (n - k1))
                        + (nb_de_partitions_naïf (n - k2)) ;
                incr k
            done ; 0
            with Stop -> !résultat ;;

let nb_de_partitions =
    let mémoire = ref [ (0,1) ; (1,1) ; (2,2) ]
    in
    let rec f n =
        if n < 0 then 0
        else try assoc n !mémoire with Not_found
                ->  let résultat = ref 0
                    and k = ref 1
                    in
                    try
                    while true do
                        let k1 = !k * (3 * !k - 1) / 2
                        and k2 = !k * (3 * !k + 1) / 2
                        in
                        if k1 > n then raise Stop ;
                        if even(!k) then
                            résultat := !résultat - (f (n - k1)) - (f (n - k2))
                        else
                            résultat := !résultat + (f (n - k1)) + (f (n - k2)) ;
                        incr k
                    done ; 0
                    with Stop
                        ->  (   mémoire := (n,!résultat) :: !mémoire ;
                                !résultat   )
    in f ;;

let iota n =
    let rec aux a b k =
        if k = n then a
        else aux b (b + (k + 1)*a) (k + 1)
    in
    aux 1 1 0 ;;

(* ----- algorithme RSK direct ------ *)

let RSK_direct sigma =
    let n = vect_length sigma
    in
    let rec substitue k a dl el = match dl,el with
        | [],[] -> [a],[k],None
        | (td::qd),(te::qe) when td < a
            ->  let qd',qe',suite = substitue k a qd qe
                in
                (td::qd'),(te::qe'),suite
        | (td::qd),_ -> (a::qd),el,Some(td)
        | _ -> failwith "bug"
    in
    let rec insertion k a_k (d,e) =
        match d,e with
            | [],[] -> ([[a_k]],[[k]])
            | (dl :: dq),(el :: eq)
                -> ( match substitue k a_k dl el with
                        | dl',el',None -> (dl'::dq),(el'::eq)
                        | dl',el',Some(a)
                            ->  let dq',eq' = insertion k a (dq,eq)
                                in
                                (dl'::dq'),(el'::eq') )
            | _ ->  failwith "bug"
    in
    it_list (fun (d,e) k -> insertion k sigma.(k) (d,e))
            ([],[])
            (intervalle 0 (n-1)) ;;

(* ----- algorithme RSK inverse ------ *)

let RSK_inverse (d,e) =
	let dv = vect_of_list d
	and ev = vect_of_list e
	and n = it_list (fun x l -> x + (list_length l)) 0 d
    in
    let sigma = make_vect n 0
    in
    let cherche k =
    	let rec aux i =
    		if last ev.(i) = k then
    			let a = last dv.(i)
    			in
    			dv.(i) <- équeute dv.(i) ; ev.(i) <- équeute ev.(i) ;
    			(i,a)
    		else aux (i+1)
    	in
    	aux 0
    in
    let rec substitue l a = match l with
    	| [ x ] -> [a],x
    	| x :: y :: q when y > a -> (a::y::q),x
    	| x :: q -> let q',a = substitue q a in (x::q'),a
    	| _ -> failwith "bug"
    in
    let rec remonte i a = match i,(substitue dv.(i) a) with
    	| 0,(l,a) -> dv.(i) <- l ; a
    	| _,(l,a) -> dv.(i) <- l ; remonte (i-1) a
    in
    let calcule k = match cherche k with
    	| 0,a -> sigma.(k) <- a
    	| i,a -> sigma.(k) <- remonte (i-1) a
    in
    for k = n-1 downto 0 do calcule k done ;
    sigma ;;

Les entrées-sorties des lambda-termes et des termes de de Bruijn :

type lambda_terme =
    | Variable of string
    | Application of lambda_terme * lambda_terme
    | Abstraction of string * lambda_terme ;;

type lexème = ParG | ParD | Flèche | Identificateur of string ;;

let string_of_char_list l =
    let s = make_string (list_length l) `.`
    in
    let rec construit i = function
        | [] -> s
        | t :: q -> s.[i] <- t ; construit (i+1) q
    in
    construit 0 l;;

let mange flot c =
    let rec accumule () =
        try let c,_ = stream_get flot
            in
            if c == ` ` || c == `)` then []
            else ( stream_next flot ; c :: (accumule ()) )
        with Parse_failure -> []
    in
    string_of_char_list (c :: accumule ()) ;;
    
let rec fin_ligne flot = match flot with
    | [< '`\n` >] -> [< flot >]
    | [< 'c >] -> fin_ligne flot ;;
    
let rec lexeur flot = match flot with
    | [< '(` ` | `\r` | `\n`) >] -> lexeur flot
    | [< '`%` >] -> lexeur (fin_ligne flot)
    | [< '`(` >] -> ParG :: (lexeur flot)
    | [< '`)` >] -> ParD :: (lexeur flot)
    | [< '`-` >]
        ->  (   match flot with
                    | [< '`>` >] -> Flèche :: (lexeur flot)
                    | [< >] -> let u = Identificateur(mange flot `-`)
                               in
                               u :: (lexeur flot)  )
    | [< 'c >] -> let u = Identificateur(mange flot c)
                  in
                  u :: (lexeur flot)
    | [< >] -> [] ;;

let rec parse_terme lex_list = let r,_ = parse_T lex_list in r  
and parse_T lex_list = match lex_list with
    | (Identificateur v) :: Flèche :: q
        -> let t,q = parse_T q in Abstraction(v,t),q
    | _ -> parse_E lex_list
and parse_E lex_list =
    let f,q = parse_F lex_list in parse_E' f q
and parse_E' f = function
    | (ParD :: _) as lex_list -> f,lex_list
    | [] -> f,[]
    | lex_list -> let f',q = parse_F lex_list in parse_E' (Application(f,f')) q
and parse_F = function
    | (Identificateur v) :: q -> Variable(v),q
    | ParG :: q -> let t,q = parse_T q in match q with
                                            | ParD :: q -> t,q
                                            | _ -> failwith "Erreur de syntaxe" ;;

let parseur chaîne = parse_terme (lexeur (stream_of_string chaîne)) ;;

#open "format" ;;

let print_lambda_terme e =
    let ps = print_string
    and pc = print_char
    and space = print_space
    and open() = open_hovbox 3
    and close = close_box
    in
    let rec print e p =
        open() ;
        if p then pc `(` ;
        ( match e with
            | Variable(v) -> ps v
            | Abstraction(x,u)
                -> ps x ; space() ; ps "->" ; space() ; print u false
            | Application(g,d)
                ->  let pg,pd = match g,d with
                        | Variable(_),Abstraction(_) -> false,true
                        | Variable(_),_ -> false,false
                        | Application(_),Variable(_) -> false,false
                        | Abstraction(_),Variable(_) -> true,false
                        | _ -> true,true
                    in
                    print g pg ; space() ; print d pd
        ) ;
        if p then pc `)` ;
        close()
    in
    print e false ; print_newline () ;;
    
install_printer "print_lambda_terme" ;;

type terme_de_de_Bruijn =
    | Index of int
    | Appl of terme_de_de_Bruijn * terme_de_de_Bruijn
    | Lambda of terme_de_de_Bruijn ;;

let print_terme_de_de_Bruijn e =
    let ps = print_string
    and pi = print_int
    and pc = print_char
    and space = print_space
    and open() = open_hovbox 3
    and close = close_box
    in
    let rec print e =
        open() ;
        ( match e with
            | Index(i) -> pi i
            | Lambda(u)
                -> ps "(\\" ; space() ; print u ; pc `)`
            | Appl(g,d)
                ->  pc `(` ; print g ; space() ; print d ; pc `)`
        ) ;
        close()
    in
    print e ;;

install_printer "print_terme_de_de_Bruijn" ;;

Lambda-calcul :

include "parseur" ;;

(* définit entre autre :

type lambda_terme =
    | Variable of string
    | Application of lambda_terme * lambda_terme
    | Abstraction of string * lambda_terme ;;

type terme_de_de_Bruijn =
    | Index of int
    | Appl of terme_de_de_Bruijn * terme_de_de_Bruijn
    | Lambda of terme_de_de_Bruijn ;;

*)

(*************************************** AUXILIAIRES ********************************************)

let rec intervalle i j = if i > j then [] else i :: (intervalle (i+1) j) ;;

let variables =
    let v = make_vect 26 ""
    in
    for i = 0 to 25 do v.(i) <- make_string 1 (char_of_int (int_of_char `a` + i)) done ;
    v ;;

let vect_index v a =
    let i = ref 0
    in
    try
        while v.(!i) <> a do incr i done ;
        !i
    with _ -> raise Not_found ;;

let var_index a = vect_index variables a ;;
let index_var = var_index ;;

let index l a =
    let rec aux i = function
        | [] -> raise Not_found
        | t :: _ when t = a -> i
        | _ :: q -> aux (i+1) q
    in
    aux 0 l ;;
    
let rec nth k l = match k,l with
    | _,[] -> raise Not_found
    | 0,t::_ -> t
    | _,_::q -> nth (k - 1) q ;;

let cons a b = a :: b ;;

(************************** Gestion des lambda-termes *******************************************

    lt_occurrences : string -> lambda_terme -> int list list * int list list
        
        prend en arguments le nom d'une variable et un lambda-terme
        et renvoie le couple constitué des occurrences libres et liées
        de cette variable dans ce terme
        
    lt_libres : lambda_terme -> (int list * string) list
    
        prend en argument un lambda-terme
        et renvoie la liste des couples constitués d'une occurrence de variable
        libre et de cette variable
        
************************************************************************************************)

let lt_occurrences x t =
    let ajoute c = map (cons c)
    in
    let rec aux est_liée = function
        | Variable(a) when a = x -> if est_liée then [[]],[] else [],[[]]
        | Variable(_) -> [],[]
        | Application(t1,t2)
            ->  let free1,bound1 = aux est_liée t1
                and free2,bound2 = aux est_liée t2
                in
                (ajoute 1 free1) @ (ajoute 2 free2) ,
                (ajoute 1 bound1) @ (ajoute 2 bound2)
        | Abstraction(a,t)
            ->  let free,bound = aux (est_liée || x = a) t
                in
                (ajoute 1 free),(ajoute 1 bound)
    in
    aux false t ;;

let lt_libres t =
    let ajoute c = map (function (o,v) -> (c::o,v))
    in
    let rec aux liées = function
        | Variable(a) -> if mem a liées then [] else [[],a]
        | Application(t1,t2) -> (ajoute 1 (aux liées t1)) @ (ajoute 2 (aux liées t2))
        | Abstraction(x,t) -> ajoute 1 (aux (x :: liées) t)
    in
    aux [] t ;;

(************************** Gestion des termes de de Bruijn **************************************

    db_occurrences : string -> terme_de_de_Bruijn -> int list list
        
        prend en arguments le nom d'une variable et un terme de de Bruijn
        et renvoie la liste des occurrences libres de cette variable dans ce terme
        
    db_libres : terme_de_de_Bruijn -> (int list * string) list
    
        prend en argument un 
        et renvoie la liste des couples constitués d'une occurrence de variable
        libre et de cette variable
        
    la variable globale `variables' contient la liste de toutes les variables du monde,
    la partie auxiliaire l'initialise avec [ "a" ; "b" ; ... ; "z" ]
        
************************************************************************************************)

let db_occurrences x t =
    let ajoute c = map (cons c)
    in
    let rec aux p = function
        | Index(i) when i < p -> []
        | Index(i) -> if variables.(i-p) = x then [[]] else []
        | Appl(t1,t2) -> (ajoute 1 (aux p t1)) @ (ajoute 2 (aux p t2))
        | Lambda(t) -> ajoute 1 (aux (p + 1) t)
    in
    aux 0 t ;;

let db_libres t =
    let ajoute c = map (function (o,v) -> (c::o,v))
    in
    let rec aux p = function
        | Index(i) -> if i < p then [] else [[],variables.(i-p)]
        | Appl(t1,t2) -> (ajoute 1 (aux p t1)) @ (ajoute 2 (aux p t2))
        | Lambda(t) -> ajoute 1 (aux (p + 1) t)
    in
    aux 0 t ;;

(****************** Conversion lambda-termes <--> termes de de Bruijn ****************************

    db_of_lt : lambda_terme -> terme_de_de_Bruijn
    
    lt_of_db : terme_de_de_Bruijn -> lambda_terme
        
************************************************************************************************)

let db_of_lt t =
    let rec aux liées = function
        | Variable(x) -> Index( try index liées x
                                with Not_found -> (list_length liées) + (var_index x)   )
        | Application(t1,t2) -> Appl(aux liées t1 , aux liées t2)
        | Abstraction (x,t) -> Lambda(aux (x :: liées) t)
    in
    aux [] t ;;

let lt_of_db t =
    let libres = map snd (db_libres t)
    in
    let rec aux p liées k = function
        | Index(i) when i < p -> Variable(nth i liées)
        | Index(i) -> Variable(variables.(i - p))
        | Appl(t1,t2) -> Application(aux p liées k t1 , aux p liées k t2)
        | Lambda(t)
            ->  if mem variables.(k) libres then aux p liées (k + 1) (Lambda t)
                else
                    let x = variables.(k)
                    in
                    Abstraction(x,aux (p + 1) (x :: liées) (k + 1) t)
    in
    aux 0 [] 0 t ;;


(**************************** Quelques exemples simples *****************************************)

let identité =  parseur "x -> x" ;;
let omega =     parseur "(x -> (x x)) (x -> (x x))" ;;
let exemple1 =  parseur "(x -> (w -> ((y -> y) w) x))"
and exemple2 =  parseur "(x -> (y -> ((x -> x) y) x))"
and exemple3 =  parseur "x -> y -> x x y"
and exemple4 =  parseur "x -> y -> z x y"
and exemple5 =  parseur "x -> (z (z -> x z))" ;;

let à_réduire = parseur "(x -> x x)((y -> x y) a)" ;;


let identité' = db_of_lt identité
and omega' =    db_of_lt omega
and exemple1' = db_of_lt exemple1
and exemple2' = db_of_lt exemple2
and exemple3' = db_of_lt exemple3
and exemple4' = db_of_lt exemple4
and exemple5' = db_of_lt exemple5 ;;

let à_réduire' = db_of_lt à_réduire ;;

(********************************** Alpha-équivalence ********************************************

    db_alpha_équivalence : terme_de_de_Bruijn -> terme_de_de_Bruijn -> bool
        est l'égalité stricte, tout simplement !
    
    lt_alpha_équivalence : lambda_terme -> lambda_terme -> bool
        
************************************************************************************************)

let rec db_alpha_équivalence t1 t2 = match t1,t2 with
    | Index(i1),Index(i2) -> i1 = i2
    | Appl(t11,t12),Appl(t21,t22) -> (db_alpha_équivalence t11 t21)
                                        && (db_alpha_équivalence t12 t22)
    | Lambda(t1),Lambda(t2) -> db_alpha_équivalence t1 t2
    | _ -> false ;;

let lt_alpha_équivalence t1 t2 =
    db_alpha_équivalence (db_of_lt t1) (db_of_lt t2) ;;

(********************************** Bêta-réduction ***********************************************

    bêta : terme_de_de_Bruijn -> terme_de_de_Bruijn -> terme_de_de_Bruijn
        bêta a t réalise la bêta-réduction supposant que a est un Lambda(u)
    
    bêta_un : terme_de_de_Bruijn -> terme_de_de_Bruijn
        réalise la première bêta-réduction à gauche possible ou déclenche Stop
        si aucune bêta-réduction n'est possible
    
    bêta_réduction : terme_de_de_Bruijn -> terme_de_de_Bruijn
        itère tant que possible bêta_un
        peut donc boucler ... (sur les termes non normalisables)
        
    db_bêta_réduction : terme_de_de_Bruijn -> terme_de_de_Bruijn
        est un synonyme de bêta_réduction
        
    lt_bêta_réduction : lambda_terme -> lambda_terme
        opère sur les lambda-termes
        
************************************************************************************************)

let bêta (Lambda u) t =
    let décalage d t =
        let rec aux_décale p = function
            | Appl(t1,t2) -> Appl(aux_décale p t1,aux_décale p t2)
            | Lambda(t) -> Lambda(aux_décale (p + 1) t)
            | Index(i) when i < p -> Index(i)
            | Index(i) -> Index(i + d)
        in
        aux_décale 0 t
    in
    let rec aux p = function
        | Appl(u1,u2) -> Appl(aux p u1,aux p u2)
        | Lambda(v) -> Lambda(aux (p + 1) v)
        | Index(i) when i = p -> décalage p t
        | Index(i) when i < p -> Index(i)
        | Index(i) -> Index(i - 1)
    in
    aux 0 u ;;

exception Stop ;;

let rec bêta_un = function
    | Index(_) -> raise Stop
    | Lambda(t) -> Lambda(bêta_un t)
    | Appl(Lambda(u),t) -> bêta (Lambda u) t
    | Appl(t1,t2) -> try Appl(bêta_un t1,t2) with Stop -> Appl(t1,bêta_un t2) ;;

let rec bêta_réduction t =
    try bêta_réduction (bêta_un t)
    with Stop -> t ;;

let db_bêta_réduction = bêta_réduction
and lt_bêta_réduction t = lt_of_db (bêta_réduction (db_of_lt t)) ;;

Retour à la page générale de La lettre de Caml.