home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Source Code / C / Applications / SML⁄NJ 93+ / Documentation / examples / textbooks / working / Lambda.ML < prev    next >
Encoding:
Text File  |  1995-12-30  |  9.0 KB  |  293 lines  |  [TEXT/R*ch]
  1. (**** ML Programs from the book
  2.  
  3.   ML for the Working Programmer
  4.   by Lawrence C. Paulson, Computer Laboratory, University of Cambridge.
  5.   (Cambridge University Press, 1991)
  6.  
  7. Copyright (C) 1991 by Cambridge University Press.
  8. Permission to copy without fee is granted provided that this copyright
  9. notice and the DISCLAIMER OF WARRANTY are included in any copy.
  10.  
  11. DISCLAIMER OF WARRANTY.  These programs are provided `as is' without
  12. warranty of any kind.  We make no warranties, express or implied, that the
  13. programs are free of error, or are consistent with any particular standard
  14. of merchantability, or that they will meet your requirements for any
  15. particular application.  They should not be relied upon for solving a
  16. problem whose incorrect solution could result in injury to a person or loss
  17. of property.  If you do use the programs or functions in such a manner, it
  18. is at your own risk.  The author and publisher disclaim all liability for
  19. direct, incidental or consequential damages resulting from your use of
  20. these programs or functions.
  21. ****)
  22.  
  23.  
  24. (**** Chapter 9.  WRITING INTERPRETERS FOR THE LAMBDA-CALCULUS ****)
  25.  
  26. use"ParsePrint.ML";           (*Read library, parser, and pretty printer*)
  27.  
  28. (*** Lambda-terms ***)
  29.  
  30. signature LAMBDA_NAMELESS =
  31.   sig
  32.   datatype term = Free  of string
  33.         | Bound of int
  34.         | Abs   of string*term
  35.         | Apply of term*term
  36.   val abstract: int -> string -> term -> term
  37.   val subst: int -> term -> term -> term
  38.   val inst: (string * term) list -> term -> term
  39.   end;
  40.   
  41.  
  42. functor LambdaFUN(Basic: BASIC) : LAMBDA_NAMELESS =
  43.   struct
  44.   local open Basic in
  45.   datatype term = Free  of string
  46.         | Bound of int
  47.         | Abs   of string*term
  48.         | Apply of term*term;
  49.  
  50.   (*Convert occurrences of b to bound index i in a term*)
  51.   fun abstract i b (Free a) = if a=b then  Bound i  else  Free a
  52.     | abstract i b (Bound j) = Bound j
  53.     | abstract i b (Abs(a,t)) = Abs(a, abstract (i+1) b t)
  54.     | abstract i b (Apply(t,u)) = Apply(abstract i b t, abstract i b u);
  55.  
  56.   (*Shift by i a term's non-local indexes; d is the depth of abstractions*)
  57.   fun shift 0 d u = u
  58.     | shift i d (Free a) = Free a
  59.     | shift i d (Bound j) = if j>=d then Bound(j+i) else Bound j 
  60.     | shift i d (Abs(a,t)) = Abs(a, shift i (d+1) t)
  61.     | shift i d (Apply(t,u)) = Apply(shift i d t, shift i d u);
  62.  
  63.   (*Substitute u for bound variable i in a term t*)
  64.   fun subst i u (Free a)  = Free a
  65.     | subst i u (Bound j) =
  66.     if j<i then      Bound j       (*locally bound*)
  67.     else if j=i then shift i 0 u
  68.     else (*j>i*)    Bound(j-1)    (*non-local to t*)
  69.     | subst i u (Abs(a,t)) = Abs(a, subst (i+1) u t)
  70.     | subst i u (Apply(t1,t2)) = Apply(subst i u t1, subst i u t2);
  71.  
  72.   (*Substitution for free variables*)
  73.   fun inst env (Free a) = (inst env (lookup(env,a)) 
  74.                    handle Lookup => Free a)
  75.     | inst env (Bound i) = Bound i
  76.     | inst env (Abs(a,t)) = Abs(a, inst env t)
  77.     | inst env (Apply(t1,t2)) = Apply(inst env t1, inst env t2);
  78.   end
  79.   end;
  80.  
  81.  
  82. (*** Parsing of lambda terms ***)
  83. signature PARSELAM = 
  84.   sig
  85.   type term
  86.   val abslist: string list * term -> term
  87.   val applylist: term * term list -> term
  88.   val read: string -> term
  89.   end;
  90.  
  91. functor ParseLamFUN (structure Parse: PARSE 
  92.              and       Lambda: LAMBDA_NAMELESS) : PARSELAM =
  93.   struct
  94.   local open Parse  open Lambda  in
  95.   type term = term;
  96.  
  97.   (*Abstraction over several free variables*)
  98.   fun abslist([],    t) = t
  99.     | abslist(b::bs, t) = Abs(b, abstract 0 b (abslist(bs, t)));
  100.  
  101.   (*Application of t to several terms*)
  102.   fun applylist(t, []) = t
  103.     | applylist(t, u::us) = applylist(Apply(t,u), us);
  104.  
  105.   fun makelambda ((((_,b),bs),_),t) = abslist(b::bs,t)
  106.  
  107.   (*term/atom distinction prevents left recursion; grammar is ambiguous*)
  108.   fun term toks =
  109.    (   $"%" -- id -- repeat id -- $"." -- term    >> makelambda
  110.      || atom -- repeat atom            >> applylist
  111.     ) toks
  112.   and atom toks =
  113.     (   id                    >> Free
  114.      || $"(" -- term -- $")"            >> (#2 o #1)
  115.     ) toks;
  116.   val read = reader term;
  117.   end
  118.   end;
  119.  
  120.  
  121. (*** Pretty Printing of lambda terms ***)
  122.  
  123. signature DISPLAM = 
  124.   sig
  125.   type term
  126.   val rename: string list * string -> string
  127.   val stripabs: term -> string list * term
  128.   val pr: term -> unit
  129.   end;
  130.  
  131. functor DispLamFUN (structure Basic: BASIC 
  132.             and       Pretty: PRETTY
  133.             and       Lambda: LAMBDA_NAMELESS) : DISPLAM =
  134.   struct
  135.   local open Basic  open Pretty  open Lambda  in
  136.   type term = Lambda.term;
  137.  
  138.   (*Free variable in a term -- simple & slow version using append*)
  139.   fun vars (Free a) = [a]
  140.     | vars (Bound i) = []
  141.     | vars (Abs(a,t)) = vars t
  142.     | vars (Apply(t1,t2)) = vars t1 @ vars t2;
  143.  
  144.   (*rename variable "a" to avoid clashes with the strings bs. *)
  145.   fun rename (bs,a) =
  146.       if  a mem bs  then  rename (bs, a ^ "'")  else  a;
  147.  
  148.   (*Remove leading lambdas; return bound variable names*)
  149.   fun strip (bs, Abs(a,t)) = 
  150.         let val b = rename (vars t, a)
  151.     in  strip (b::bs, subst 0 (Free b) t)  end
  152.     | strip (bs, u) = (rev bs, u);
  153.  
  154.   fun stripabs t = strip ([],t);
  155.  
  156.   fun spacejoin (a,b) = a ^ " " ^ b;
  157.  
  158.   fun term (Free a) = str a 
  159.     | term (Bound i) = str "??UNMATCHED INDEX??"
  160.     | term (t as Abs _) =
  161.       let val (b::bs,u) = stripabs t
  162.           val binder = foldleft spacejoin ("%" ^ b, bs) ^ ". "
  163.       in  blo(0, [str binder, term u])  end
  164.     | term t = blo(0, applic t)
  165.   and applic (Apply(t,u)) = applic t @ [brk 1, atom u]
  166.     | applic t        = [ atom t ]
  167.   and atom (Free a) = str a 
  168.     | atom t = blo(1, [str"(", term t, str")"]);
  169.  
  170.   fun pr t = Pretty.pr (std_out, term t, 50);
  171.   end
  172.   end;
  173.  
  174.  
  175. (*** Evaluation of lambda terms ***)
  176.  
  177. signature REDUCE = 
  178.   sig
  179.   type term
  180.   val eval : term -> term
  181.   val byvalue : term -> term
  182.   val headnf : term -> term
  183.   val byname : term -> term
  184.   end;
  185.  
  186.  
  187. functor ReduceFUN (Lambda: LAMBDA_NAMELESS) : REDUCE =
  188.   struct
  189.   local open Lambda  in
  190.   type term = term;
  191.  
  192.   (*evaluation, not affecting function bodies*)
  193.   fun eval (Apply(t1,t2)) = 
  194.         (case eval t1 of
  195.          Abs(a,u) => eval(subst 0 (eval t2) u)
  196.        | u1 => Apply(u1, eval t2))
  197.     | eval t = t;
  198.  
  199.   (*normalization using call-by-value*)
  200.   fun byvalue t = normbodies (eval t)
  201.   and normbodies (Abs(a,t)) = Abs(a, byvalue t)
  202.     | normbodies (Apply(t1,t2)) = Apply(normbodies t1, normbodies t2)
  203.     | normbodies t = t;
  204.  
  205.   (*head normal form*)
  206.   fun headnf (Abs(a,t)) = Abs(a, headnf t)
  207.     | headnf (Apply(t1,t2)) = 
  208.         (case headnf t1 of
  209.          Abs(a,t) => headnf(subst 0 t2 t)
  210.        | u1 => Apply(u1, t2))
  211.     | headnf t = t;
  212.  
  213.   (*normalization using call-by-name*)
  214.   fun byname t = normargs (headnf t)
  215.   and normargs (Abs(a,t)) = Abs(a, normargs t)
  216.     | normargs (Apply(t1,t2)) = Apply(normargs t1, byname t2)
  217.     | normargs t = t;
  218.   end
  219.   end;
  220.  
  221.  
  222. (******** SHORT DEMONSTRATIONS ********)
  223.  
  224. structure Basic = BasicFUN();
  225. structure LamKey = 
  226.     struct val alphas = []
  227.            and symbols = ["(", ")", "'", "->"]
  228.     end;
  229. structure LamLex = LexicalFUN (structure Basic=Basic and Keyword=LamKey);
  230. structure Parse = ParseFUN(LamLex);
  231. structure Pretty = PrettyFUN();
  232.  
  233. structure Lambda = LambdaFUN(Basic);
  234. structure ParseLam = ParseLamFUN (structure Parse=Parse and Lambda=Lambda);
  235. structure DispLam = DispLamFUN 
  236.     (structure Basic=Basic and Pretty=Pretty and Lambda=Lambda);
  237. structure Reduce = ReduceFUN(Lambda);
  238.  
  239. open Basic;  open Lambda; 
  240.  
  241. val stdenv = map  (fn (a,b) => (a, ParseLam.read b))
  242. [    (*booleans*)
  243.  ("true", "%x y.x"),           ("false",  "%x y.y"), 
  244.  ("if", "%p x y. p x y"),
  245.      (*ordered pairs*)
  246.  ("pair", "%x y f.f x y"),  
  247.  ("fst", "%p.p true"),         ("snd", "%p.p false"),
  248.      (*natural numbers*)
  249.  ("suc", "%n f x. n f (f x)"),
  250.  ("iszero", "%n. n (%x.false) true"),
  251.  ("0", "%f x. x"),             ("1", "suc 0"),
  252.  ("2", "suc 1"),               ("3", "suc 2"),
  253.  ("4", "suc 3"),               ("5", "suc 4"),
  254.  ("6", "suc 5"),               ("7", "suc 6"),
  255.  ("8", "suc 7"),               ("9", "suc 8"),
  256.  ("add",  "%m n f x. m f (n f x)"),
  257.  ("mult", "%m n f. m (n f)"),
  258.  ("expt", "%m n f x. n m f x"),
  259.  ("prefn", "%f p. pair (f (fst p)) (fst p)"),
  260.  ("pre",  "%n f x. snd (n (prefn f) (pair x x))"),
  261.  ("sub",  "%m n. n pre m"),
  262.       (*lists*)
  263.  ("nil",  "%z.z"),
  264.  ("cons", "%x y. pair false (pair x y)"),
  265.  ("null", "fst"),
  266.  ("hd", "%z. fst(snd z)"),     ("tl", "%z. snd(snd z)"),
  267.     (*recursion for call-by-name*)
  268.  ("Y", "%f. (%x.f(x x))(%x.f(x x))"),
  269.  ("fact", "Y (%g n. if (iszero n) 1 (mult n (g (pre n))))"),
  270.  ("append", "Y (%g z w. if (null z) w (cons (hd z) (g (tl z) w)))"),
  271.  ("inflist", "Y (%z. cons MORE z)"),
  272.      (*recursion for call-by-value*)
  273.  ("YV", "%f. (%x.f(%y.x x y)) (%x.f(%y.x x y))"),
  274.  ("factV", "YV (%g n. (if (iszero n) (%y.1) (%y.mult n (g (pre n))))y)") ];
  275.  
  276.  
  277. (** first example: parsing/displaying of types **)
  278. structure Type = TypeFUN (structure Parse=Parse and Pretty=Pretty);
  279. Type.read"('a->'b)->('c->'d)";
  280. Type.pr it;
  281.  
  282. (** lambda reduction examples **)
  283. fun stdread a = inst stdenv (ParseLam.read a);
  284. fun try evfn = DispLam.pr o evfn o stdread;
  285. try Reduce.byvalue "expt 2 3";       (*call-by-value*)
  286. try Reduce.byvalue "sub 9 6";
  287. try Reduce.byvalue "factV 3";
  288. try Reduce.byname "mult 2 3";       (*call-by-name*)
  289. try Reduce.byname "(%x.hello)(Y Y)";   (*diverges under call-by-value*)
  290. try Reduce.byname "hd (tl (Y (%z. append (cons MORE (cons AND nil)) z)))";
  291.  
  292.  
  293.