taylor.ml

   1: (*****************************************************************************
   2:  * Calcul de l'expansion de Taylor d'un lambda-terme par la machine de Krivine
   3:  *****************************************************************************)
   4: 
   5: open List;;
   6: open Lambda;;
   7: open Diff;;
   8: 
   9: type lambda_closure = Clos  of lambda_term * lambda_env
  10:                     | Free  of int
  11: and    diff_closure = Dclos of       bunch * diff_env
  12: 
  13: and      lambda_env = lambda_closure list
  14: and        diff_env =   diff_closure list
  15: 
  16: and    lambda_stack = lambda_closure list
  17: and      diff_stack =   diff_closure list
  18: 
  19: and    lambda_state = (lambda_term * lambda_env * lambda_stack)
  20: and      diff_state = (  diff_term *   diff_env *   diff_stack)
  21: ;;
  22: 
  23: 
  24: let rec diff_env_make : diff_closure -> int -> diff_env =
  25:   fun c ->
  26:     function
  27:         0 -> [c]
  28:       | n -> Dclos([], [])::(diff_env_make c (n-1))
  29: 
  30: and diff_env_contract : diff_env -> diff_env -> diff_env =
  31:   fun e1 e2 ->
  32:     match (e1, e2) with
  33:         (e, []) | ([], e) -> e
  34:       | (Dclos(b1, e'1)::e''1, Dclos(b2, e'2)::e''2) ->
  35:           (Dclos(bunch_mult b1 b2, diff_env_contract e'1 e'2))::
  36:             (diff_env_contract e''1 e''2)
  37: 
  38: and diff_env_power : diff_env -> int -> diff_env =
  39:   fun e n ->
  40:     match e with
  41:         [] -> []
  42:       | Dclos(b, e')::e'' ->
  43:           (Dclos(bunch_power b n, diff_env_power e' n))::(diff_env_power e'' n)
  44: ;;
  45: 
  46: (* Prend en argument un terme clos t et un terme avec ressources simple et
  47:    normal t0 approximant la forme normale de t. Retourne le terme avec resource
  48:    simple du développement de Taylor de t qui se réduit en t0. *)
  49: 
  50: let diff_of_term : lambda_term -> diff_term -> diff_term = fun t t0 ->
  51:   let rec kam : int -> int -> diff_term -> lambda_state -> diff_state =
  52:     (* Les deux premiers arguments depth et lambdas sont respectivement
  53:        le nombre d'appels récursifs, et le nombre de lambdas sous-lesquels la
  54:        machine est entrée. *)
  55:     fun depth lambdas t0 ->
  56:       if depth > max_depth_limit then failwith "Max recursion depth exceeded"
  57:       else
  58:         function
  59:           (App(u, v), e, s) -> (
  60:             let (u_d, e_d, s'_d) =
  61:               kam (depth + 1) lambdas t0 (u, e, Clos(v, e)::s)
  62:             in
  63:               match s'_d with 
  64:                   Dclos(b, e'_d)::s_d ->
  65:                     (DiffApp(u_d, b), diff_env_contract e_d e'_d, s_d)
  66:                 | _ -> failwith "kam failure (App case)"
  67:           )
  68: 
  69:         | (Abs(x, u), e, c::s) -> (
  70:             let (u_d, e'_d, s_d) = kam (depth + 1) lambdas t0 (u, c::e, s)
  71:             in 
  72:               match e'_d
  73:               with
  74:                   [] -> (DiffAbs(x, 0, u_d), [], Dclos([], [])::s_d)
  75:                 | (Dclos(b, _) as c_d)::e_d ->
  76:                     (DiffAbs(x, bunch_length b, u_d), e_d, c_d::s_d)
  77:           )
  78: 
  79:         | (Abs(x, u), e, []) -> (
  80:             match t0 with
  81:                 DiffAbs(_, d, u0) ->
  82:                   let (u_d, e_d, s_d) =
  83:                     kam (depth + 1) (lambdas + 1) u0
  84:                       (u, Free(lambdas + 1)::e, [])
  85:                   in (match (e_d, s_d)
  86:                       with
  87:                           ([], []) -> (DiffAbs(x, d, u_d), [], [])
  88:                         | (Dclos([], [])::e'_d, []) ->
  89:                             (DiffAbs(x, d, u_d), e'_d, [])
  90:                         | _ -> failwith "kam failure (Abs case)"
  91:                      )
  92:               | _ -> failwith "lambda mismatch"
  93:           )
  94: 
  95:         | (Var(n, x), e, s) -> (
  96:             try
  97:               match nth e n
  98:               with
  99:                   Clos(vn, en) ->
 100:                     let (vn_d, en_d, s_d) =
 101:                       kam (depth + 1) lambdas t0 (vn, en, s)
 102:                     in (DiffVar(n, x),
 103:                         diff_env_make (Dclos([(vn_d, 1)], en_d)) n,
 104:                         s_d)
 105: 
 106:                 | Free(lambda_index) ->
 107:                     let s_d = kam_args depth lambdas
 108:                       (lambdas - lambda_index) (rev s, t0)
 109:                     in (DiffVar(n, x), [], rev s_d)
 110: 
 111:             with Failure("nth") -> failwith "kam failure (Var case)"
 112:           )
 113: 
 114:         |  (Star, _, []) -> (
 115:              match t0
 116:              with
 117:                  DiffStar -> (DiffStar, [], [])
 118:                | _ -> failwith "star mismatch"
 119:            )
 120: 
 121:         | (Star, _, _::_) -> failwith "star constant violation"
 122: 
 123:   and kam_args : int -> int -> int -> (lambda_stack * diff_term) -> diff_env =
 124:     fun depth lambdas var_index ->
 125:       function
 126:           ([], DiffVar(n, _)) ->
 127:             if n = var_index then []
 128:             else failwith "variable mismatch"
 129: 
 130:         | (c::s, DiffApp(u0, b0)) ->
 131:             let c_d = kam_bunch depth lambdas c b0
 132:             and s_d = kam_args depth lambdas var_index (s, u0)
 133:             in c_d::s_d
 134: 
 135:         | _ -> failwith "application mismatch"
 136: 
 137:   and kam_bunch : int -> int -> lambda_closure -> bunch -> diff_closure =
 138:     fun depth lambdas c b0 ->
 139:       match c
 140:       with
 141:           Clos(t, e) -> (
 142:             match b0
 143:             with
 144:                 [] -> Dclos([], [])
 145:               | (t0, n)::b0' ->
 146:                   let (t_d, e_d, _)   = kam (depth + 1) lambdas t0 (t, e, [])
 147:                   and Dclos(b', e'_d) = kam_bunch depth lambdas c b0'
 148:                   in let e_d         = diff_env_power e_d n
 149:                   in Dclos(monomial_bunch_mult (t_d, n) b',
 150:                            diff_env_contract e_d e'_d)
 151:           )
 152:         | _ -> failwith "kam failure (bunch case)"
 153: 
 154:   in
 155:     match kam 0 0 t0 (t, [], [])
 156:     with
 157:         (t_d, [], []) -> t_d
 158:       |        _      -> failwith "kam failure (toplevel)"
 159: ;;
 160: 
 161: (* synthèse *)
 162: let linearize (t: string) (t0: string) : string =
 163:   string_of_diff (diff_of_term (lambda_of_string t) (diff_of_string t0));;
 164: 

This document was generated using caml2html