Fourth Interlude: Church predecessor function with sunflowers
To have at least one predecessor function not on the https://en.wikipedia.org/wiki/Lambda_calculus page, here's a derivation using a chain of function and argument pairs. We start with the basic zero and succ from >>172 >>185 >>193.
(define (zero state-transformer initial-state) initial-state)
(define empty "")
(define (addsunflower string) (string-append string "🌻"))
(define (succ n) (lambda (state-transformer initial-state) (state-transformer (n state-transformer initial-state))))
((succ (succ (succ zero))) addsunflower empty)
=> "🌻🌻🌻"We also use the pairs from >>172 >>193 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 a function and its argument.
(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 we keep the successor function in the first component of a pair and its current argument in the second component. We are using [fun, arg] --> [fun, fun(arg)] as the state tranformer and starting off the chain with [succ, 0]. After n rounds the initial 0 is wrapped in n applications of succ.
(define (apply-fun-value pair) (make-pair (first pair) ((first pair) (second pair))))
(define (same-but-with-fun-value n) (second (n apply-fun-value (make-pair succ zero))))
((same-but-with-fun-value (succ (succ (succ zero)))) addsunflower empty)
=> "🌻🌻🌻"This is not particularly useful yet because we are simulating n by using the n we already have in hand, but if we manage to elide one round of succ application while keeping the rest, we will be left with n-1 applications of succ on our initial 0, which is what we want from our predecessor function. To elide one round we resort to the usual device of a special initial state and a state tranformer that can handle it. In the new state tranformer, instead of always applying and propagating the function we find in the first component of the current pair, we apply the function we find but then overwrite it with succ. We use [fun, arg] --> [succ, fun(arg)]. This allows us to start off the chain with [identity, 0] as the new initial state. On the first round identity is applied to 0 and is then replaced with succ: [identity, 0] --> [succ, 0]. The remaining n-1 rounds wrap 0 in n-1 applications of the successor function.
(define (apply-and-switch-to-succ pair) (make-pair succ ((first pair) (second pair))))
(define (identity a) a)
(define (pred n) (second (n apply-and-switch-to-succ (make-pair identity zero))))
((pred zero) addsunflower empty)
=> ""
((pred (succ zero)) addsunflower empty)
=> ""
((pred (succ (succ zero))) addsunflower empty)
=> "🌻"
((pred (succ (succ (succ zero)))) addsunflower empty)
=> "🌻🌻"
((pred (succ (succ (succ (succ zero))))) addsunflower empty)
=> "🌻🌻🌻"
((pred (succ (succ (succ (succ (succ zero)))))) addsunflower empty)
=> "🌻🌻🌻🌻"
((pred (pred (succ (succ (succ (succ (succ zero))))))) addsunflower empty)
=> "🌻🌻🌻"
((pred (pred (pred (succ (succ (succ (succ (succ zero)))))))) addsunflower empty)
=> "🌻🌻"The chain of function and argument pairs with the succ overwrite and identity bootstrap suffices for this derivation of the Church predecessor function.
This technique of rebuilding n and then arranging for one of the rounds to be elided can be used as a general method for obtaining various forms of the predecessor function.