Implémentations informatiques du lambda calcul

Congru

Bonjour, je propose ici des implémentations du lambda calcul en caml light.

Quiconque a d'autres implémentations ou suggestions est libre de rajouter les siennes.

Congru

Tout d'abord, j'aimerais remercier @Médiat_Suprème pour m'avoir orienté vers le manuscrit de Mr Krivine sur le lambda calcul, aussi j'aimerais remercier @Heuristique de m'avoir donné quelques tuyaux sur le lambda calcul et de m'avoir orienté vers un manuscrit sur le sujet, et aussi je remercie @Foys pour m'avoir conseillé d'aller voir les indices de Brujin.

Voyons quelques implémentations de $\lambda -calcul$

Congru

1) Définition du type $\lambda -terme$

type lambda_terme = V of int | S of lambda_terme*lambda_terme | K of int*lambda_terme ;;

2) Fonction "substitution-simultanée":

let rec sub (a,b,c) =  match a with
                        | d when b = [||] -> d
                        | V(i) -> if b.(0) = i
                                     then c.(0)
                                     else let R = ref a in
                                            let l = vect_length b in
                                            let r = ref 0 in
                                            while ( (not (b.(!r) = i) ) && !r <l-1)
                                            do r:= (!r)+1;
                                                 if b.(!r) = i
                                                 then R := c.(!r)
                                                 else ()
                                            done;
                                           !R
                        |K(i,u) ->       let l = vect_length b in
                                             let bb = make_vect (l-1) 0 in
                                             let cc = make_vect (l-1) (V(0)) in
                                             let d = ref 0 in
                                             let r = ref 0 in
                                             if b.(0) = i
                                             then   (
                                                for z = 0 to l-2
                                                do (bb.(z) <- b.(z+1); cc.(z) <- c.(z+1))
                                                done;
                                                K(i, sub(u,bb,cc))
                                                        )
                                             else (
                                                 while( (not(b.(!r)=i)) && (!r)<l-1)
                                                 do  r:= (!r)+1;
                                                      if b.(!r) = i
                                                      then d := 1
                                                      else ()
                                                 done;
                                                 if !d =1
                                                 then (
                                                    for z = 0 to (!r)-1
                                                    do (bb.(z) <- b.(z); cc.(z) <- c.(z))
                                                    done;
                                                    for z = (!r) to (l-2)
                                                    do (bb.(z) <- b.(z+1); cc.(z) <- c.(z+1))
                                                    done;
                                                    K(i, sub(u,bb,cc))
                                                          )
                                                   else K(i, sub(u,b,c))
                                                         )
              
                        | S(u,v) ->    S( sub(u,b,c) , sub(v,b,c))
;;

Remarque : dans la fonction $sub$, l'argument est un triplet $(a,b,c)$ tel que $a$ est un lambda terme, $b$ est une vecteur d'entiers naturels (l'entier $i$ évoque la variable $ V(i)$) et $c$ est un vecteur de lambda termes qui a même longueur que $b$. Grosso modo, il faut remplacer la variable $V(b.(i))$ par le lambda terme $c.(i)$ dans $a$.

Congru

3) l'appartenance à une liste

let rec belonging a b = match b with
                        | [] -> 0
                        | c when (a = hd c) -> 1
            | d -> belonging a (tl d)
;;

Remarque: donne $1$ si $a\in b$ et zéro sinon.

4) éliminer les répétitions dans une liste

let rec elimrep a = match a with
           | [] -> []
           | c::d when (belonging c d)=1 -> elimrep d
           | c::d when not (belonging c d)=1  -> c::(elimrep d)
;;

5) enlever un élément à une liste

let rec enlv a b = match b with
                  | [] -> []
                  | c::d when (a = c) -> enlv a d
                  | c::d when not (a = c) -> c::(enlv a d)
;;

Remarque: cette fonction enlève $a$ à la liste $b$

Congru

6) fonction variables libres

let rec fv a = match a with
           | V(i) -> [i]
           | S(u,v)  -> elimrep ((fv u)@(fv v))
           | K(i,u)  -> enlv i (fv u)
;;

Remarque: cette fonction associe à tout lambda-terme $a$ une liste $l$ d'entiers telle que l'ensemble des variables libres de $a$ est $\{V(i)\vert i\in l\}$

7) fonction variables liées

let rec bv a = match a with
           | V(i) -> []
           | S(u,v)  -> elimrep ((bv u)@(bv v))
           | K(i,u)  -> elimrep (i::(bv u))
;;

Remarque: cette fonction associe à tout lambda-terme $a$ une liste $l$  d'entiers telle que l'ensemble des variables liées de $a$ est $\{V(i)\vert i\in l\}$

Congru

8) maximum

let maximum (a,b) = if a>b

                                 then a
                                 else b ;;

9) minimum

let minimum (a,b) = if a<b

                                 then a
                                 else b ;;

10) profondeur d'un lambda-terme

let rec profondeur a = match a with

                                    | V(i) -> 1
                                    | S(u,v)  ->  1+(maximum (profondeur u, profondeur v))
                                    | K(i,u)  ->  1+(profondeur u)

;;

11) Union d'une liste de listes

let rec list_union a = match a with
                                 | [] -> []
                                 | b::c -> b@(list_union c)
;;

12) maximum d'une liste d'entiers

let rec big_cup a = match a with
                               |[] -> 0
                               |c::d -> maximum (c,big_cup d)
;;

13) fonction caractéristique de l'alpha équivalence

let rec v_alpha a b = match (a,b) with
                                 |((V i),c) -> if c=(V i) 

                                                   then 1
                                                   else 0
                                 | (K(i,c),K(j,d)) -> let h = [fv(c);bv(c);fv(d);bv(d);[i;j]] in
                                                            let g = 1+(big_cup (list_union(h))) in
                                                            v_alpha (sub(c,[|i|],[|V(g)|])) (sub(d,[|j|],[|V(g)|]))
                                 | (S(u,v),S(u',v')) ->  minimum (v_alpha u u',v_alpha v v')
                                 | (c,d) ->  0
;;

Remarque: cette fonction est d'arité deux. "v_alpha a b" retourne $1$ si les deux lambda termes a et b sont alpha-équivalent, "v_alpha a b" retourne $0$ dans le cas contraire. Si quelqu'un a d'autres implémentations de la fonction caractéristique de l'alpha-équivalence, ce serait gentil de les partager ici.

Congru

14) $\alpha$-renomage

let rec alpha_renaming a j = match a with
                            | V i -> V i
                            | K(i,u) when 1 = (belonging i j) -> let l = list_union [j;fv u; bv u] in
                                                                                   let g = 1+(big_cup l) in
                                                                                   K(g, alpha_renaming (sub (u,[|i|],[|V g|])) j)
                            | K(i,u) when 0 = (belonging i j) -> K(i, alpha_renaming u j)
                            | S(u,v)                                        -> S(alpha_renaming u j, alpha_renaming v j)
;;

Remarque: dans "alpha_renaming a j", $a$ est un lambda terme et $j$ est une liste d'netiers, "alpha_renaming a j ;; " retourne un lambda-terme $\alpha$-équivalent à $a$ qui n'a aucun élément de $\{V(i)\vert i\in j \}$ comme variable liée.

15)
let vectfvlist a = if a =[||]
                          then []
                          else let l= vect_length a and m= ref [] in
                                 for i=0 to l-1
                                 do m:= (fv(a.(i))) ::(!m)
                                 done;
                                 !m
;;

Remarque: dans "vectfvlist a", $a$ est un vect de $\lambda$-termes et "vectfvlist a ;;" retourne une liste qui correspond à la l'ensemble des ensembles des variables libres des éléments de a.

16) substitution sur  $L/\equiv$

($L$ étant la structure des $\lambda$-termes et $\equiv$ étant la relation d'$\alpha$-équivalence)

let sub2 (a,u,v) = let w = vectfvlist v in
                            let g = list_union w in
                            let b = alpha_renaming a g in
                            sub (b,u,v)
;;

Remarque : dans $sub2 (a,u,v)$, $a$ est un $\lambda$-terme et $u$ est une liste d'entiers naturels et "v" est une liste de $\lambda$-termes. 

Ce programme renomme les variables liées de $a$ pour obtenir un $\lambda$-terme $b$ tel qu'aucune variable libre d'un élément de $v$ n'est liée dans $b$ et tel que $b \equiv a$, ensuite le programme calcule "sub(b,u,v) ;;"

Merci aux modérateurs pour leur patience.

Foys

Bonjour,

Tu devrais chercher le "poplmark challenge" pour voir comment la problématique de l'alpha-renommage est abordée par les informaticiens.

Congru

Merci @Foys, je vais regarder cela.

Congru

Remarquez que la fonction sub2 est une fonction qui fait la substitution sans capture.

J'ai une autre fonction qui fait aussi une substitution sans capture:

17) change un tableau en liste

let image a = if a =[||]
              then []
              else let l= vect_length a and m= ref [] in
                   for i=0 to l-1
                   do m:= (a.(i))::(!m)
                   done;
                   !m
;;

18) substitution sans capture (construite par récursion transfinie)

let rec sub_capture (a,u,v) = match a with
                            | V i -> if i= u.(0)
                                     then v.(0)
                                     else let l = vect_length u and b = ref 0 and c= ref 0 in
                                          while ((!b<l-1) && not (i= u.(!b)))
                                          do b:=(!b)+1;
                                             if i= u.(!b)
                                             then c:= 1
                                             else ()
                                          done;
                                          if !c =0
                                          then V i
                                          else v.(!b)
                            | K(i,w)  -> let l = list_union [list_union(vectfvlist v);image u; fv a] in
                                         let g = 1+(big_cup l) in
                                         let x = sub_capture (w,[|i|],[|V g|]) in
                                         K(g, sub_capture(x,u,v))
                            | S(b,c)  -> S(sub_capture(b,u,v),sub_capture(c,u,v))
;;

Remarque: $a$ est un lambda-terme, $u$ est un tableau d'entiers et $v$ est un tableau de lambda-termes de la même taille que $u$