Is Zero

Testing for Zero

Recall how Church numerals work:

• ZERO = λf.λx.x -- applies f zero times, returns x untouched
• ONE = λf.λx.f x -- applies f once
• TWO = λf.λx.f (f x) -- applies f twice

The key observation: ZERO is the only numeral that never applies f. Every numeral $n \geq 1$ applies f at least once.

This gives us a detection strategy. If we choose f and x carefully, we can distinguish "f was never applied" from "f was applied at least once."

ISZERO Definition

To test for zero, we need f and x such that:

• If f is never applied (numeral is ZERO): result is TRUE
• If f is applied at least once (numeral is non-zero): result is FALSE

The solution: use TRUE as the base value x, and use λx.FALSE as f.

ISZERO = λn.n (λx.FALSE) TRUE

The trick is in f = λx.FALSE. This function ignores its argument and always returns FALSE. So:

• ZERO never applies f $\to$ the base TRUE survives untouched
• Any non-zero numeral applies f at least once $\to$ FALSE replaces whatever was there

ISZERO ZERO

ISZERO = λn.n (λx.FALSE) TRUE

Applying ISZERO to ZERO:

ISZERO ZERO = ZERO (λx.FALSE) TRUE

Recall ZERO = λf.λx.x. It ignores f and returns x:

ZERO (λx.FALSE) TRUE = TRUE

The function λx.FALSE is never called. The base value TRUE passes through untouched.

ISZERO ONE

ISZERO = λn.n (λx.FALSE) TRUE

Applying ISZERO to ONE:

ISZERO ONE = ONE (λx.FALSE) TRUE

Recall ONE = λf.λx.f x. It applies f once to x:

ONE (λx.FALSE) TRUE = (λx.FALSE) TRUE = FALSE

The function λx.FALSE is applied once to TRUE. It ignores TRUE and returns FALSE. One application is all it takes.

Why ISZERO Works

ISZERO = λn.n (λx.FALSE) TRUE

The design of ISZERO rests on a single fact about Church numerals:

• ZERO applies f zero times $\to$ base value TRUE survives
• ONE applies f once $\to$ (λx.FALSE) TRUE = FALSE
• TWO applies f twice $\to$ (λx.FALSE) ((λx.FALSE) TRUE) = FALSE
• Any $n \geq 1$ applies f at least once $\to$ result is FALSE

The function λx.FALSE is a constant function -- it ignores its argument and always returns FALSE. Once it fires even once, the result is FALSE no matter how many more times it is applied. FALSE fed into λx.FALSE still gives FALSE.

This is why the test is binary: zero applications vs one-or-more.

ISZERO Any Non-Zero

ISZERO = λn.n (λx.FALSE) TRUE

We have seen that ISZERO ZERO = TRUE and ISZERO ONE = FALSE. The pattern holds for every non-zero numeral:

• ISZERO TWO = TWO (λx.FALSE) TRUE = (λx.FALSE) ((λx.FALSE) TRUE) = (λx.FALSE) FALSE = FALSE
• ISZERO THREE applies (λx.FALSE) three times $\to$ still FALSE

No matter how large the numeral, (λx.FALSE) fires at least once and the result is FALSE. ISZERO returns a Church boolean: TRUE for zero, FALSE for everything else.