[2/2] Next, we note that in the repacking chain we have n applications of the state transformer, which provide the behavior of the Church numeral n, so if we manage to elide one of the applications but keep the rest, we will obtain the behavior of the Church numeral n-1. We also have the repacker produce every box after the initial one, but the initial box is special in that it is created outside of the repacker's control. The natural idea is to try to exploit the common all-but-one nature of these two situations. To this end we create a fake box that works by ignoring the receiver function and directly returning the content of the box.
(define (make-fake-box a) (lambda (receiver) a))
(extract (make-fake-box "馃尮"))
=> "馃尮"Note that the fake box works correctly with the extractor, because the only thing the fake box is capable of returning, the content of the box, is the correct return for the extractor. If we use the fake box as the initial box, the first attempt to apply the state transformer will be ignored by the fake box, because the fake box ignores the receiver function, but every subsequent box will be a regular box created by the repacker, so all remaining attempts to apply the state transformer will be carried out. This results in n-1 applications of the state transformer, which is the behavior of the Church numeral n-1. This is why we changed the repacker to give the box control over the application of the state transformer, because if we had kept the explicit application of the state transformer in the repacker then using a fake box would have made no difference to the number of applications of the state transformer.
(define (pred n) (lambda (state-transformer initial-state) (extract (n (make-merged-repacker state-transformer) (make-fake-box initial-state)))))
((pred zero) addrose empty)
= ""
((pred (succ zero)) addrose empty)
= ""
((pred (succ (succ zero))) addrose empty)
= "馃尮"
((pred (succ (succ (succ zero)))) addrose empty)
= "馃尮馃尮"
((pred (succ (succ (succ (succ zero))))) addrose empty)
= "馃尮馃尮馃尮"
((pred (succ (succ (succ (succ (succ zero)))))) addrose empty)
= "馃尮馃尮馃尮馃尮"
((pred (pred (succ (succ (succ (succ (succ zero))))))) addrose empty)
= "馃尮馃尮馃尮"
((pred (pred (pred (succ (succ (succ (succ (succ zero)))))))) addrose empty)
= "馃尮馃尮"Recall that in the context of Church numerals the predecessor of zero is zero itself. The merged repacker and the fake box suffice for this derivation of the Church predecessor function.
As a bonus we can take our definition of pred, inline its entire dependency tree, obfuscate all the parameter names and arrive at the first PRED formula currently on the https://en.wikipedia.org/wiki/Lambda_calculus page.
PRED := 位n.位f.位x.n (位g.位h.h (g f)) (位u.x) (位u.u)The final (位u.u) is the identity function that the extractor passes to the final box to extract its content. The preceding (位u.x), which uses a different u__, is the inlined fake box which ignores the receiver function, __u, and returns the content of the box, which is x__, the initial state. The box parameter from the repacker's definition is renamed to __g, while the receiver function from make-box is renamed to h__. The initial state is __x and the state transformer is f. Translation:
PRED := 位n.位f .位x .n (位g .位h .h (g f )) (位u .x ) (位u.u)
PRED := 位n.位state .位initial.n (位current .位make .make (current state )) (位make .initial) identity
transformer state box of box box box of transformer fake box state function
repacker receiver receiver repacker receiver of extractHowever, because the current version of that page was written by dodo birds, they'd rather offer induction than explain a derivation of the formula, such as the one with the repacker chain and the fake box.