Simplifying division of church-numbers with church-fractions.
A church number n can be understood as the act of applying a function to a value n times. That is:
(λ f x . (f (f (f x))))
Can be understood as the church number 3, since it is an action that applies a function, f, to a value, x, 3 times. Here, I will be using "number" as a synonym for "church number" and, thus, a "natural number". Implementing addition, multiplication and exponentiation on church numbers is straightforward. Division is more awkward. Wikipedia, for instance, uses a recursive definition that doesn't have a normal form and is, thus, unsuited for strongly normalizing evaluators. This version is total, but has a huge normal form and works for integers, not naturals. There is a simpler way to define it, extending the same intuition to build a concept of church fractions:
A church fraction n/m can be understood as the act of homogeneously distributing the application of a function f to m values n times. For example, the church fraction 6/2 can be encoded as:
(λ f g a b . (g (f (f (f a))) (f (f (f b)))))
Which is a function that applies f to 2 values, a and b, 3 times each (since 6/2=3). Since the lambda calculus doesn't allow for multiple return values, we use an additional parameter, g, to serve as a "callback" that holds (and, possibly, decides how to combine) the m results.
A function that converts between church numbers and church fractions can, then, be defined as:
frac = (λ n m f . (n (m (λ t nt v . (t (λ a . (nt a v)))) id (λ a b . (b (f a))))))
So, for example:
frac 6 2 -> (λ f g a b . (g (f (f (f a))) (f (f (f b)))))
We can, also, define a "floor" function which maps back from fractions to numbers:
floor = (λ m frac f x . (repeat m x (frac f (lastOf m))))
Notice floor is indexed by the divisor of the fraction. Here, repeat applies a function to a number n of x's, and lastOf returns the last of its n arguments:
repeat = (λ n x f . (n (λ t . (t x)) f))
lastOf = (λ n . (n true id id))
In other words, floor just gets the last "bucket" of a fraction and adjusts its variables to denote a church number. With that, we can easily define division by:
div = (λ n m . (floor m (frac n m)))
So, for example:
(div 12 3) -> 4
As expected. Since it doesn't use any form of recursion, the div combinator has a normal form:
(λ a b c d . (b (λ e . (e d)) (a (b (λ e f g . (e (λ h . (f h g)))) (λ a . a) (λ e f . (f (c e)))) (b (λ a b . a) (λ a . a) (λ a . a)))))
And, thus, can be used by strongly normalizing evaluators.