tweak ml code/instructions
authorJim Pryor <profjim@jimpryor.net>
Mon, 20 Sep 2010 16:16:44 +0000 (12:16 -0400)
committerJim Pryor <profjim@jimpryor.net>
Mon, 20 Sep 2010 16:16:44 +0000 (12:16 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
code/lambda.ml
using_the_programming_languages.mdwn

index 3f1435d..146c9eb 100644 (file)
@@ -372,3 +372,5 @@ let pp, pn, pi = string_of_lambda, normal_string_of_lambda, int_of_lambda
 let pnv,piv= (fun expr -> string_of_lambda (cbv expr)), (fun expr -> to_int (cbv expr))
 let db, db_equal, db_contains = db, db_equal, db_contains
 
 let pnv,piv= (fun expr -> string_of_lambda (cbv expr)), (fun expr -> to_int (cbv expr))
 let db, db_equal, db_contains = db, db_equal, db_contains
 
+let alpha_eq x f = db_equal (db x) (db y)
+
index deef2ee..1fab79f 100644 (file)
@@ -44,7 +44,16 @@ know much OCaml yet to use it. Using it looks like this:
                (* or *)
                let add = << fun m n -> fun s z -> m s (n s z) >>;;
 
                (* or *)
                let add = << fun m n -> fun s z -> m s (n s z) >>;;
 
-               church_to_int << $add$ $one$ $two$ >>;;
+               (* now use:
+                       pp FORMULA                              to print a formula, unreduced
+                       pn FORMULA                              to print the normal form of a formula (when possible)
+                       pi FORMULA                              to print the integer which FORMULA is a Church numeral for (when possible)
+
+                       alpha_eq FORM1 FORM2    are FORM1 and FORM2 syntactically equivalent (up to alpha-conversion)?
+                                                                       this does not do reductions on the formulae
+               *)
+
+               pi << $add$ $one$ $two$ >>;;
                - : int = 3
 
        To install this package, here's what you need to do. I've tried to explain it in basic terms, but you do need some familiarity with your operating system: for instance, how to open a Terminal window, how to figure out what directory the Terminal is open to (use `pwd`); how to change directories (use `cd`); and so on.
                - : int = 3
 
        To install this package, here's what you need to do. I've tried to explain it in basic terms, but you do need some familiarity with your operating system: for instance, how to open a Terminal window, how to figure out what directory the Terminal is open to (use `pwd`); how to change directories (use `cd`); and so on.