Third Interlude: Church predecessor function with cherry blossoms
Recall from SICP 1.2.2 Tree Recursion https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/6515/sicp.zip/full-text/book/book-Z-H-11.html#%_sec_1.2.2 that to go from a tree-recursive procedure for computing Fibonacci numbers to an iterative procedure, we used the technique of keeping two consecutive values from the Fibonacci sequence and moving them at each step to the next position in the sequence. Here is a version without the superfluous round performed in SICP:
(define (fib-iter a b n) (if (= n 1) b (fib-iter b (+ a b) (- n 1))))
(define (fib n) (if (<= n 0) 0 (fib-iter 0 1 n)))
(fib 10)
=> 55We can use the same technique of keeping two consecutive values from a sequence on Church numerals. We start with the basic zero and succ from >>172 >>185.
(define (zero state-transformer initial-state) initial-state)
(define empty "")
(define (addcherry string) (string-append string "🌸"))
(define (succ n) (lambda (state-transformer initial-state) (state-transformer (n state-transformer initial-state))))
((succ (succ (succ zero))) addcherry empty)
=> "🌸🌸🌸"We also use the pairs from >>172 SICP exercise 2.4 https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/6515/sicp.zip/full-text/book/book-Z-H-14.html#%_thm_2.4 to package the two consecutive values.
(define (make-pair a b) (lambda (receiver) (receiver a b)))
(define (first-projection a b) a)
(define (second-projection a b) b)
(define (first pair) (pair first-projection))
(define (second pair) (pair second-projection))
(first (make-pair "🌸" "🦋"))
=> "🌸"
(second (make-pair "🌸" "🦋"))
=> "🦋"We can rebuild the Church numeral n by starting with 0 and applying the successor function n times, but in the spirit of the iterative Fibonacci technique we also keep around the previous value in our sequence, the one to which we apply the successor function. Our state transformation is [a, b] --> [b, b+1]. Starting with [0, 0] this yields the chain [0, 0] --> [0, 1] --> [1, 2] --> [2, 3] and so on. After n rounds the second component of our pair is n.
(define (keep-one-behind pair) (make-pair (second pair) (succ (second pair))))
(define (same-but-with-one-behind n) (second (n keep-one-behind (make-pair zero zero))))
((same-but-with-one-behind (succ (succ (succ zero)))) addcherry empty)
=> "🌸🌸🌸"This is not particularly useful yet because we are simulating n by using the n we already have in hand, but we can easily change this into a predecessor function by extracting the first component of the final pair instead of the second component. At this point it becomes important that the first component of our initial pair is 0. In same-but-with-one-behind the first component of our initial pair could be any value because that value will never be used. But here it must be 0 so that we get the correct predecessor even when the state transformer is not applied at all because n happens to be 0.
(define (pred n) (first (n keep-one-behind (make-pair zero zero))))
((pred zero) addcherry empty)
=> ""
((pred (succ zero)) addcherry empty)
=> ""
((pred (succ (succ zero))) addcherry empty)
=> "🌸"
((pred (succ (succ (succ zero)))) addcherry empty)
=> "🌸🌸"
((pred (succ (succ (succ (succ zero))))) addcherry empty)
=> "🌸🌸🌸"
((pred (succ (succ (succ (succ (succ zero)))))) addcherry empty)
=> "🌸🌸🌸🌸"
((pred (pred (succ (succ (succ (succ (succ zero))))))) addcherry empty)
=> "🌸🌸🌸"
((pred (pred (pred (succ (succ (succ (succ (succ zero)))))))) addcherry empty)
=> "🌸🌸"The successor sequence that keeps around two consecutive values suffices for this derivation of the Church predecessor function.
In this case the third PRED formula from the https://en.wikipedia.org/wiki/Lambda_calculus page is effectively in the clear, with Φ being our keep-one-behind function.
Φ := λx.PAIR (SECOND x) (SUCC (SECOND x))
PRED := λn.FIRST (n Φ (PAIR 0 0))