Hi fellow ocaml coder,


Church numerals is a unary coding and as such is awfully inefficient.
Multiplication typically uses repeated addition.
Division/remainder also typically uses repeated substraction.
Because of the crappy unary coding there is little you can do to improve on that. 

My advice is you could gain much better efficiency via a binary coding.
Here is how you can do the easy part :

type nat =
  | Null           (* 0 *) 
  | Unit           (* 1 *)
  | Zero of nat    (* 0... *)
  | One  of nat    (* 1... *)

let rec even = function
  | Null -> true
  | Unit -> false
  | Zero n | One  n -> even n 

let rec double = function
  | Null -> Zero Null
  | Unit -> One  Null
  | Zero n -> Zero (double n)
  | One  n -> One  (double n)

let succ n = 
  let rec loop = function
    | Null -> Unit,false
    | Unit -> Null,true
    | Zero n -> let m,c = loop n in (if c then One m else Zero m),false  
    | One  n -> let m,c = loop n in (if c then Zero m else One m),c  
  in
  let m,c = loop n in if c then One m else m

let mult a b =
  let rec loop = function 
    | Null -> Null,double b
    | Unit -> b,double b
    | Zero n -> let d,c = loop n in d,double c 
    | One  n -> let d,c = loop n in add d c,double c
  in let n,_ = loop a in n


That is dirty untested code yet i hope you get the idea.
Addition/substraction and division will be somewhat trickier however.

- damien





Damien Guichard
2009-03-21



En réponse au message
de : Su Zhang
du : 2009-03-21 18:36:11
À : caml-list@yquem.inria.fr
CC : 
Sujet : [Caml-list] calculating a remainder of two church number on lambdacalculs with ocaml

Hi OCaml hackers,

I have a question about how can I write a function which can get the remainder of two church numberials in lambda calculus. I know this is a ocaml maillist, but this lambda calculus should use ocaml engine, so is there anybody know how can I write this function? 

Thanks!



-- 
Su Zhang
PHD Student 
Computer Information and Science
Kansas State University