[ prog / sol / mona ]

prog


The Forced Indentation Of Code

185 2022-09-08 10:38

Second Interlude: Church predecessor function with tulips [1/2]

We can make an adder function that adds some fixed value to its argument.

(define (add-two augend) (+ augend 2))
(add-two 3)
=> 5

If we have an adder function but don't know what fixed value it uses as its increment, we can obtain it by passing in 0.

(add-two 0)
=> 2

We can create a factory that makes adder functions for a given increment.

(define (make-adder addend) (lambda (augend) (+ augend addend)))
((make-adder 2) 3)
=> 5

If we have an adder function in hand, one way to create the adder function that uses an increment that is 1 higher is to add 1 to its output.

(define (next-adder adder) (lambda (augend) (+ (adder augend) 1)))
((next-adder (make-adder 2)) 4)
=> 7

We can play the same adder game with Church numerals. We start with the basic zero and succ from >>172.

(define (zero state-transformer initial-state) initial-state)
(define empty "")
(define (addtulip string) (string-append string "🌷"))
(define (succ n) (lambda (state-transformer initial-state) (state-transformer (n state-transformer initial-state))))
(zero addtulip empty)
=> ""
((succ zero) addtulip empty)
=> "🌷"
((succ (succ zero)) addtulip empty)
=> "🌷🌷"
((succ (succ (succ zero))) addtulip empty)
=> "🌷🌷🌷"

The adder with a 0 increment returns its argument unmodified, so it is simply the identity function. The adder with an increment of 1 is the successor function. To make an adder that uses an increment that is 1 higher we wrap the output of the current adder in succ.

(define (identity x) x)
(define add-zero identity)
(define add-one succ)
(define (next-adder adder) (lambda (augend) (succ (adder augend))))
(((next-adder (next-adder (next-adder add-zero))) zero) addtulip empty)
=> "🌷🌷🌷"

We can simulate the behavior of the Church numeral n by using adders as the state of the computation. We start with the zero adder as the initial state, and on each application of the state transformer we create an adder 1 higher than the current one. After n rounds we obtain an adder with an increment of n, but this is still an adder rather than a numeral. To extract its increment we simply pass in 0.

(define (same-but-with-adders n) ((n next-adder add-zero) zero))
((same-but-with-adders (succ (succ (succ zero)))) addtulip empty)
=> "🌷🌷🌷"
267


VIP:

do not edit these