calculating a remainder of two church number on lambda calculs with ocaml

Su Zhang
 Damien Guichard
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20090321 (19:06) 
From:  Damien Guichard <alphablock@o...> 
Subject:  Re: [Camllist] calculating a remainder of two church number on lambdacalculs with ocaml 
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 20090321 En réponse au message de : Su Zhang du : 20090321 18:36:11 À : camllist@yquem.inria.fr CC : Sujet : [Camllist] 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