prog

frontpage - thread list - new thread - preferences - ?

The Forced Indentation Of Code

186 2022-09-08 10:45

[2/2] This is not particularly useful yet because we are simulating n by using the n we already have in hand, but we'll tweak this a bit. If we somehow manage to elide one of the applications of next-adder but keep the rest, we will obtain an adder with an increment of n-1, from which it is easy to extract the numeral by passing in 0. The route we will take here is to use conditionals. One representation of booleans in lambda calculus is to use the first projection as true and the second projection as false. To make a conditional we pass the consequent and the alternate to the boolean test result, and the boolean will choose which branch to return.

(define (true a b) a)
(define (false a b) b)
(true "yes" "no")
=> "yes"
(false "yes" "no")
=> "no"

Scheme is an applicative-order language https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/6515/sicp.zip/full-text/book/book-Z-H-10.html#%_sec_Temp_22 so this representation of conditionals is not appropriate for the general case because both the consequent and the alternate are always evaluated, but in our case both branches will construct lambdas so these conditionals will suffice. If we have a Church numeral we can determine whether it is zero by using true as the initial state and using a state transformer that switches the state to false. If the numeral is zero the state transformer is never applied and the state remains true. If the state transformer is applied even once because the numeral is non-zero, the state becomes false.

(define (iszero n) (n (lambda (ignored) false) true))
((iszero zero) "yes" "no")
=> "yes"
((iszero (succ zero)) "yes" "no")
=> "no"

To tweak same-but-with-adders and elide one of the applications of next-adder but keep the rest, we will use the following strategy. We replace the initial add-zero with a fake adder with two properties: it should function correctly in case it is also the final adder because the state transformer is never applied, and it should be easy to check for in the state transformer. The state transformer is switched from next-adder to a wrapped version of next-adder that first checks whether it is dealing with the fake adder. If so it discards the fake adder and returns add-zero, otherwise it delegates to next-adder. The net result is that the first round of the state transformer is used up for changing the state of the computation from the fake adder to add-zero, while from the second round the next-adder chain proceeds as normal as it did from the first round in same-but-with-adders, but now we only have n-1 rounds left. The final adder will therefore use an increment of n-1. A simple fake adder with the desired properties is one that ignores its argument and always returns 0. To detect it in the state transformer we check whether it returns 0 when invoked on 1. This works because no normal adder returns a result that is less than the argument it is given.

(define (fake-adder ignored) zero)
(define one (succ zero))
(define (next-state adder) ((iszero (adder one)) add-zero (next-adder adder)))
(define (pred n) ((n next-state fake-adder) zero))

To see it in action:

((pred zero) addtulip empty)
=> ""
((pred (succ zero)) addtulip empty)
=> ""
((pred (succ (succ zero))) addtulip empty)
=> "🌷"
((pred (succ (succ (succ zero)))) addtulip empty)
=> "🌷🌷"
((pred (succ (succ (succ (succ zero))))) addtulip empty)
=> "🌷🌷🌷"
((pred (succ (succ (succ (succ (succ zero)))))) addtulip empty)
=> "🌷🌷🌷🌷"
((pred (pred (succ (succ (succ (succ (succ zero))))))) addtulip empty)
=> "🌷🌷🌷"
((pred (pred (pred (succ (succ (succ (succ (succ zero)))))))) addtulip empty)
=> "🌷🌷"

The conditional adder increment chain and the fake adder suffice for this derivation of the Church predecessor function.

As a bonus we can take our definition of pred, inline its entire dependency tree except iszero, obfuscate all the parameter names and almost arrive at the second PRED formula currently on the https://en.wikipedia.org/wiki/Lambda_calculus page.

PRED := λn.n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0

There are two differences. One is the gratuitous use of (PLUS arg 1) instead of (SUCC arg). There is no need to make PLUS a dependency of PRED when all you're going to add is 1, that's what the successor function is for. The other is more curious. The test of ISZERO does not depend on k, yet it is placed inside λk. The result is that the same test, which k has no influence on, is wastefully recomputed each time λk is invoked. Instead, the test can be evaluated as soon as all the information necessary to perform the test is available, inside λg. This way instead of one lambda with a test that does not use the lambda argument, and two branches as the body, we can have one test with two unconditional lambdas as branches:

PRED := λn.n (λg.ISZERO (g 1) (λk.k) (λk.PLUS (g k) 1)) (λv.0) 0

The final 0 is the extraction of the increment from the final adder. The preceding (λv.0) is our fake adder which ignores its argument. The g parameter is the current adder of next-state. The (λk.k) branch is add-zero. The PLUS branch is the body of next-adder. Translation:

PRED := λn.n (λg         .ISZERO (g          1) (λk.k)   (λk.PLUS (g k) 1)) (λv.0) 0
PRED := λn.n (λcurrent   .ISZERO (current    1) add-zero     (succ (g k))   fake   extract
               adder of           adder of               body of next-adder adder  final
               next-state         next-state                                       increment

However, 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 conditional adder increment chain and the fake adder.

267