Discussion :

[NINEON]

comment on écrit une fonction en Caml qui réduit les CL-termes de la lambda calcul (la forme normale)

[gorgonite]

comment on écrit une fonction en Caml qui réduit les CL-termes de la lambda calcul (la forme normale)

ce sera certainement plus long qu'une simple fonction, il faut déjà te fixer une représentation de ton lambda terme, et une stratégie de réduction, puis un "simple" pattern matching devrait faire l'affaire

[NINEON]

si par exemple on a le terme (SXYZ) ,on le représente par une liste ensuite on le rends sous forme normale(réduction).
ALORS comment on implément ça en Caml?(merci)

[alex_pi]

ce sera certainement plus long qu'une simple fonction, il faut déjà te fixer une représentation de ton lambda terme, et une stratégie de réduction, puis un "simple" pattern matching devrait faire l'affaire

Le gros du boulot, c'est l'alpha-conversion quand même ! C'est là qu'il a toutes les chances de se planter :-D

[alex_pi]

si par exemple on a le terme (SXYZ) ,on le représente par une liste ensuite on le rends sous forme normale(réduction).
ALORS comment on implément ça en Caml?(merci)

Alors enfait, il parraitrait que ce serait un forum d'entraide, c'est à dire qu'on serait des volontaire, et qu'on ne serait pas payé pour faire ton boulot. Donc tu prends un bouquin de lambda calcul, un tutoriel OCaml, tu tentes d'implémenter les stratégies de réduction, et quand tu as un problème spécifique, tu reviens, et tu poses ta question, et là on t'aideras.

Bonne chance

[NINEON]

Est ce que je peux avoir une petite idée comment débuter ce programme ou un site,franchement je suis bloqué.

[gorgonite]

Est ce que je peux avoir une petite idée comment débuter ce programme ou un site,franchement je suis bloqué.

ben je dirais

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

type LambaTerme = Var of string | Lambda of string * LambdaTerme | App of LambdaTerme * LambdaTerme

ensuite, réflechis aux règles de réduction



EDIT : en cherchant sur ce forum, tu pourras t'inspirer de ceci :
http://www.developpez.net/forums/sho...ghlight=lambda

[NINEON]

merci,est ce que vous ne connaissez pas un site qui peux m'aider.

[gorgonite]

merci,est ce que vous ne connaissez pas un site qui peux m'aider.

y a tout plein de liens dans le post que j'ai cité au-dessus

[NINEON]

j'ai déja vue c'est en anglais j'aimerais bien l'avoir en français.

[gorgonite]

j'ai déja vue c'est en anglais j'aimerais bien l'avoir en français.

faut chercher parmi les cours de profs d'université...
http://www.eleves.ens.fr/home/saurin...din_poly.ps.gz

[NINEON]

j'ai lue votre document mais je n'ai pas trouver comment on fait pour réduire les terme de lambda calcul en Caml?Est ce vous voulez m'aidez?

[SpiceGuid]

Pour éviter l'alpha-conversion (trop casse gueule et ultra-inefficace à l'exécution) une seule solution: le passage en notation de Bruiijn.

Une fois en notation de Bruijn, le code qui suit fait l'affaire.
Le type des lambda-expressions et celui des lambda-valeurs:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
type lambda_expr =
  (* pure lambda_expr *)
  | Var of int
  | Abs of lambda_expr
  | App of lambda_expr * lambda_expr
  (* more lambda_expr *)
  | Let of lambda_expr * lambda_expr
  | Letrec1 of lambda_expr * lambda_expr
  | Letrec2 of lambda_expr * lambda_expr * lambda_expr
  (* more lambda_expr *)
  | Int of int
  | True_expr | False_expr
  | Const of (lambda_val -> lambda_val) 
  | Cond  of lambda_expr * lambda_expr * lambda_expr
and lambda_val =
  (* pure lambda_val *)
  | Fun of (lambda_val -> lambda_val)
  (* more lambda_val *)
  | Val of int
  | True_val | False_val
;;

Deux fonctions utilitaires:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
let unary f =
  ( function
  | Val n -> (f n: lambda_val)
  | _ -> invalid_arg "Integer expected"
  )
and binary f =
  ( function
  | Val n -> Fun (unary (f n)) 
  | _ -> invalid_arg "Integer expected"
  );;

Puis eval la fonction d'évaluation:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
 
let rec eval expr env =
  match expr with
  (* pure lambda_expr *)
  | Var n       -> List.nth env n
  | Abs body    -> Fun (fun x -> eval body (x::env))
  | App (f,arg) ->
      ( match eval f env with
      | Fun f -> f (eval arg env)
      | _ -> invalid_arg "Can't apply, not a function")
  (* more lambda_expr *)
  | Let (e,body) -> eval body (eval e env::env)
  | Letrec1 (e1,body)    ->
      let rec f = Fun (fun x -> eval e1 (x::f::env)) in eval body (f::env) 
  | Letrec2 (e1,e2,body) ->
      let rec f1 = Fun (fun x -> eval e1 (x::env2))
      and     f2 = Fun (fun x -> eval e2 (x::env2))
      and   env2 = f2::f1::env
      in    eval body env2
  (* more lambda_expr *)
  | Int n -> Val n
  | True_expr  -> True_val
  | False_expr -> False_val
  | Const f -> Fun f
  | Cond (e1,e2,e3)->
      ( match eval e1 env with
      | True_val  -> eval e2 env
      | False_val -> eval e3 env
      | _ -> invalid_arg "Boolean expected"
      )
;;

Enfin, il y a un certain temps de cela, gorgonite m'avait fait remarquer combien ce code est inutile, pas d'addition, pas de soustraction, pas de comparaison, bref on ne peut rien calculer avec cet évaluateur.
L'explication c'est que ces opérations sont des constantes, elles ne font pas partie du langage, elles ne sont pas prédéfinies, en effet on les défini ainsi:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
let fun_pred = Const (unary (fun n -> Val (pred n)))
and fun_succ = Const (unary (fun n -> Val (succ n)))
and fun_null = Const (unary (fun n -> if n = 0 then True_val else False_val))
and fun_add  = Const (binary (fun a b -> Val (a + b)))
and fun_mul  = Const (binary (fun a b -> Val (a * b)))
and fun_less = Const (binary (fun a b -> if a < b then True_val else False_val))
;;
 
let app_pred e = App (fun_pred,e)
and app_succ e = App (fun_succ,e)
and app_null e = App (fun_null,e)
and app_add  e1 e2 = App (App (fun_add,e1),e2)
and app_mul  e1 e2 = App (App (fun_mul,e1),e2)
and app_less e1 e2 = App (App (fun_less,e1),e2)
;;

[NINEON]

merci beaucoup, je n'oublierais pas ce jeste.est ce qu'on peut le faire avec des caractéres et sans des caractéres.(vous pouvez me proposer un site ou je pourais trouver un cours en français, j'ai envie de comprendre).MERCI je ne t'oublerais jamais.

[SpiceGuid]

Pour les plus courageux, le code qui précèdent est encore inefficace car toutes les fonctions sont curryfiées et donc l'évaluation construit n fermetures pour tout appel d'une fonction à n arguments.

L'optimisation principale consiste alors à ne créer qu'une seule fermeture par appel de fonctions, quelque soit le nombre d'arguments. Pour cela, après le passage en notation de Bruijn il faut faire une passe supplémentaire de transformation dite Johnsson-Lambda-Lifting, en français lissage des lambdas. À la fin de cette transformation on a plus que des super-combinateurs c'est-à-dire des fonctions à plusieurs arguments qui ne contiennent que des variables liées et aucune variable libre.

L'évaluateur devient alors plus traditionnel puisque l'environnement sera stocké dans une pile d'exécution. L'allocation d'une fermeture ne se fera plus que dans le cas (statistiquement plus rare) d'une évaluation partielle, dans l'attente des arguments manquants.

Mon type pour les expressions et les valeurs:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
type combine_expr =
  (* pure combine_expr *)
  | Var   of int
  | Combinator of int * combine_expr
  | Apply of combine_expr * (combine_expr list)
  (* more combine_expr *)
  | Local of combine_expr list * combine_expr
  (* more combine_expr *)
  | Int of int
  | True_expr | False_expr
  | Const of (unit -> combine_val) 
  | Cond  of combine_expr * combine_expr * combine_expr
and combine_val =
  (* pure combine_val *)
  | Function of int * combine_expr
  | Closure  of int * combine_expr * (combine_val list)
  (* more combine_val *)
  | Val of int
  | True_val | False_val
;;

L'évaluateur prend un argument supplémentaire (la taille maximale de la pile).
Le code de mon évaluateur:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
let evaluator smax =
  let top   = ref 0
  and stack = Array.make smax False_val
  in let unary f =
    ( match stack.(pred !top) with
    | Val n -> f n
    | _ -> invalid_arg "Integer expected"
    )
  and binary f =
    ( match stack.(!top-2), stack.(!top-1) with
    | Val n, Val m -> f n m
    | _ , _ -> invalid_arg "Integer expected"
    )
  in let rec eval expr =
    match expr with
    (* pure combine_expr *)
    | Var b ->
        stack.(!top - b)
    | Combinator(arity,body) ->
        Function (arity,body) 
    | Apply(f,arg_list) ->
        ( match eval f with
        | Function (arity,body) ->
            let arg_length = List.length arg_list in
            if arg_length = arity then begin
              List.iter (fun e -> stack.(!top) <- eval e; incr top) arg_list;
              let result = eval body
              in  top := !top - arity; result
            end else begin
              Closure(arity - arg_length, body, List.map eval arg_list)
            end
        | Closure (arity,body,args) ->
            let arg_length = List.length arg_list in
            if arg_length < arity then
              Closure(arity - arg_length, body, List.map eval arg_list @ args)
            else begin
              let base = !top in
              List.iter (fun e -> stack.(!top) <- eval e; incr top) arg_list;
              List.iter (fun e -> stack.(!top) <- e; incr top) args;
              let result = eval body
              in  top := base; result
            end
        | _ -> invalid_arg "Can't apply, not a function" )
    (* more combine_expr *)
    | Local(expr_list,body) ->
        let base = !top in
        List.iter (fun e -> stack.(!top) <- eval e; incr top) expr_list;
        let result = eval body
        in  top := base; result
    (* more combine_expr *)
    | Int n -> Val n
    | True_expr  -> True_val
    | False_expr -> False_val
    | Const body -> body ()  
    | Cond (e1,e2,e3)->
        ( match eval e1 with
        | True_val  -> eval e2
        | False_val -> eval e3
        | _ -> invalid_arg "Boolean expected"
        )
  in eval;;

EDIT:

Pardon, il existe un article en français qui décrit très bien le passage en notation de Bruijn et qui lit et imprime les expressions, par contre, contrairement à mon code il ne gère rien (pas d'opérations et pas de récursion, rien que du lambda-calcul pur). De plus il est écrit en Caml-Light et pas en Objective-Caml.
Cet article est dans La lettre de Caml, l'imprimé n°6.

[gorgonite]

vous pouvez me proposer un site ou je pourais trouver un cours en français, j'ai envie de comprendre

et ce cours-ci te conviendrait ?
http://quincy.inria.fr/data/courses/itlp/


perso, je l'ai suivi et je pense qu'il est excellent pour les débutants... ça amène des bases de parseurs, lambda-calcul, machine virtuelle, etc

[NINEON]

je m'éxcuse je vous trop embeter avec mes questio,merci beaucoup.
Je ne connais pas cette méthode ,la seul méthode que je connais c'est alpha et béta réduction.
Est ce qu'on peut écrire une fonction (pas un programme) qui prend en argument une liste de termes et renvoie la liste sous forme normale.

[NINEON]

Un grand merci à Spiceguid gorgonite.
Est ce qu'on peut écrire une fonction (pas un programme) qui prend en argument une liste de termes et renvoie la liste sous forme normale.

[gorgonite]

Est ce qu'on peut écrire une fonction (pas un programme) qui prend en argument une liste de termes et renvoie la liste sous forme normale.

il faut voir qu'une fonction va appliquer une stratégie bien précise, qui va progresser dans la réduction... rien ne dit que le lambda terme ne va pas exploser

connais-tu ce terme ?

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

( ((lambda x) ((x) (x)))  ((lambda x) ((x) (x))) )

[NINEON]

oui,je penses quand ne peut pas le réduire ,il n'est pas sous une forme normale,mais comment on écrit une fonction (pas un programme) qui prend en argument une liste de termes et renvoie la liste sous forme normale.