15 (((add-1 zero) inc) 0)
17 (((add-1 zero) inc) 1)
20 ;; the above examples should be read as follows:
21 ;; (add-1 zero) returns the function which represents 1.
22 ;; i.e. You apply inc once to 0 and that yields 1.
23 ;; in the second example, we apply inc once to 1, and
24 ;; that yields 2. This is just to convert Churl numeral
25 ;; definition to roman numeral definition.
27 ;; as said in the hint, using substitution to evaluate (add-1 zero)
28 ;; tells us that (add-1 zero) == one has one composition of (f x)
29 ;; and (add-1 (add-1 zero)) == 1 is (f (f x)), so here is their formal
31 (def one (fn [f] (fn [x] (f x))))
33 (def two (fn [f] (fn [x] (f (f x)))))
43 ;; (add-1 one) => two. Apply inc twice on 1 => 3
44 ;; similarly the other examples.
46 ;; Definition of an add operator
47 ;; To do m + n, we should have a function which is applied f, n+m times.
51 ;; (m f) = takes a function f and composes a new function which composes
52 ;; f, m times and applies this new function to x.
54 ;; (lambda (f) (lambda (x) ((m f) ((n f) x)))) will create this new
55 ;; function which compose a given function n+m times and hence is equiv
56 ;; to addition of m+n. Some simple repl experiments seem to verify the
63 (((add one two) inc) 1)
67 ;; another definition of add is this:
68 ;; m + n == (m + [1 + 1 + 1 + ... ]
72 ;; continueing the same logic, (add one two) => three
73 ;; and inc applied three times to 1 is 4. This proves
74 ;; that our definition of add is correct.
76 ;; I used the wikipedia article to study Church Numerals:
77 ;; <http://en.wikipedia.org/wiki/Church_encoding#Computation_with_Church_numerals>
81 (defn church-to-numeral [chfn]
84 (deftest test-church-to-numeral
86 (church-to-numeral one) 1
87 (church-to-numeral two) 2))
89 ;; church to roman: func to integer
90 (defn church-to-roman [f]
91 ((f (fn [x] (+ x 1))) 0))
94 (defn roman-to-church [n]
95 (fn [f] (fn [x] (first (drop n (take (inc n) (iterate f x)))))))
98 (loop [n n cf (fn [f] (fn [x] x))]
101 (recur (- n 1) (fn [f] (fn [x]
105 ((f (fn [x] (+ x 1))) 0))