Conditions, Booleans and Integers

Keywords

ver. 1.0.0

This chapter introduces untyped lambda calculus encodings for conditional expressions, boolean logic operations, natural numbers, and syntactic conveniences.

Chapter 3 explores building higher-level functional programming abstractions from the pure $\lambda$-calculus. It demonstrates how to encode conditional expressions (cond), truth values (true, false), and boolean operations (not, and, or). Additionally, it constructs natural numbers via Church/pair-based encodings with zero, succ, iszero, and pred, while introducing syntactic simplifications like curried definitions and if...then...else notation.

Full summary

3. Conditions, Booleans and Integers

This chapter constructs functional abstractions on top of the untyped $\lambda$-calculus:

Truth Values and Conditional Expressions:
- true is defined as select_first ($\lambda \text{first}.\lambda \text{second}.\text{first}$).
- false is defined as select_second ($\lambda \text{first}.\lambda \text{second}.\text{second}$).
- cond is defined as $\lambda e1.\lambda e2.\lambda c.((c\ e1)\ e2)$, taking the condition $c$ as its last argument.
Boolean Operations:
- NOT: Defined via conditional selection as $\lambda x.((x\ \text{false})\ \text{true})$ or simply def not x = x false true.
- AND: Defined as $\lambda x.\lambda y.((x\ y)\ \text{false})$ or def and x y = x y false.
- OR: Defined as $\lambda x.\lambda y.((x\ \text{true})\ y)$ or def or x y = x true y.
Natural Numbers:
- Numbers are represented as successor chains of zero:
  - zero = identity ($\lambda x.x$)
  - succ = $\lambda n.\lambda s.((s\ \text{false})\ n)$ (constructing pairs with false and the previous number)
- Operations include:
  - iszero = $\lambda n.(n\ \text{select\_first})$
  - pred = $\lambda n.((( \text{iszero}\ n)\ \text{zero})\ (n\ \text{select\_second}))$, handling the edge case for zero by returning zero.
Simplified Notations:
- Omitting nested parentheses using left-associative function application rules.
- Dropping $\lambda$ and . in definitions (e.g., def and x y = x y false).
- Introducing the syntactic form if <condition> then <true choice> else <false choice> mapping to cond <true choice> <false choice> <condition>.
Exercises:
- Deriving implementations and truth tables for implies and equiv.
- Proving De Morgan’s laws and equivalence identities via functional reduction.

Materials

Lecture notesThe unit written out, to read at your own paceOpen → SlidesThe deck to present fromOpen →

Source document

An Introduction To Functional Programming Through Lambda Calculus, Greg Michaelson, Dover Publications, 1989, 2011 — Page 39-50

← Elements of Lambda Calculus Recursion and Arithmetic →

--- title: "Conditions, Booleans and Integers" keywords: - ver. 1.0.0 format: html: toc: false --- **This chapter introduces untyped lambda calculus encodings for conditional expressions, boolean logic operations, natural numbers, and syntactic conveniences.** > Chapter 3 explores building higher-level functional programming abstractions from the pure $\lambda$-calculus. It demonstrates how to encode conditional expressions (`cond`), truth values (`true`, `false`), and boolean operations (`not`, `and`, `or`). Additionally, it constructs natural numbers via Church/pair-based encodings with `zero`, `succ`, `iszero`, and `pred`, while introducing syntactic simplifications like curried definitions and `if...then...else` notation. ::: {.callout-note collapse="true" title="Full summary"} ### 3. Conditions, Booleans and Integers This chapter constructs functional abstractions on top of the untyped $\lambda$-calculus: 1. **Truth Values and Conditional Expressions**: - `true` is defined as `select_first` ($\lambda \text{first}.\lambda \text{second}.\text{first}$). - `false` is defined as `select_second` ($\lambda \text{first}.\lambda \text{second}.\text{second}$). - `cond` is defined as $\lambda e1.\lambda e2.\lambda c.((c\ e1)\ e2)$, taking the condition $c$ as its last argument. 2. **Boolean Operations**: - **NOT**: Defined via conditional selection as $\lambda x.((x\ \text{false})\ \text{true})$ or simply `def not x = x false true`. - **AND**: Defined as $\lambda x.\lambda y.((x\ y)\ \text{false})$ or `def and x y = x y false`. - **OR**: Defined as $\lambda x.\lambda y.((x\ \text{true})\ y)$ or `def or x y = x true y`. 3. **Natural Numbers**: - Numbers are represented as successor chains of zero: - `zero` = `identity` ($\lambda x.x$) - `succ` = $\lambda n.\lambda s.((s\ \text{false})\ n)$ (constructing pairs with `false` and the previous number) - Operations include: - `iszero` = $\lambda n.(n\ \text{select\_first})$ - `pred` = $\lambda n.((( \text{iszero}\ n)\ \text{zero})\ (n\ \text{select\_second}))$, handling the edge case for zero by returning `zero`. 4. **Simplified Notations**: - Omitting nested parentheses using left-associative function application rules. - Dropping $\lambda$ and `.` in definitions (e.g., `def and x y = x y false`). - Introducing the syntactic form `if <condition> then <true choice> else <false choice>` mapping to `cond <true choice> <false choice> <condition>`. 5. **Exercises**: - Deriving implementations and truth tables for `implies` and `equiv`. - Proving De Morgan's laws and equivalence identities via functional reduction. ::: ## Materials ::: {.hg-deck} <a class="hg-card" href="notes.qmd">Lecture notesThe unit written out, to read at your own paceOpen →</a> <a class="hg-card" href="slides.qmd">SlidesThe deck to present fromOpen →</a> ::: ## Source document - An Introduction To Functional Programming Through Lambda Calculus, _Greg Michaelson_, Dover Publications, 1989, 2011 — Page 39-50 ::: {.hg-nav} [← Elements of Lambda Calculus](../2_lambda_calculus/index.qmd){.hg-prev} [Recursion and Arithmetic →](../4_recursion_and_arithmetic/index.qmd){.hg-next} :::