\( % Latex Preamble definitions here (mostly usepackage) \usepackage% %[dvipsnames] {xcolor} % make sure this is before the loading font packages \newcommand\hmmax{0} \newcommand\bmmax{0} \usepackage{amssymb} \usepackage{amsmath} \usepackage{mathtools} \usepackage %[dvipsnames] {graphicx} \usepackage{float} %\usepackage[numbers]{natbib} \usepackage[document]{ragged2e} % % enumitem doesn't seem to work with beamer %\usepackage[inline]{enumitem} \usepackage{wrapfig} \usepackage{stackrel} % extensible arrows \usepackage{extpfeil} % \usepackage{trfrac} \usepackage{amsthm} \usepackage{tikz} \usepackage{tikz-cd} \usepackage{tikz} \usepackage{tikz-qtree} \usetikzlibrary{automata, positioning, arrows, shapes.geometric} \usepackage{turnstile} \usepackage{comment} %https://tex.stackexchange.com/questions/21334/is-there-a-package-that-has-the-clockwise-gapped-circle-arrow-in-it % \usepackage{mathbx} \usepackage{datetime} \usepackage{datetime2} %% Also See %% http://u.cs.biu.ac.il/~tsaban/Pdf/LaTeXCommonErrs.pdf %% for general tips \usepackage{listings} \usepackage{subfigure} \usepackage{bm} \usepackage{amsfonts} %% - also included by amssymb \usepackage{mathpazo} %% - because the OP uses mathpazo, optional %\usepackage{tufte-latex} \usepackage{comment} \usepackage{mathtools} \usepackage{bussproofs} \usepackage{hyperref} %\usepackage{cleveref} \)
\( %% Your math definitions here % \newcommand{\alphaequiv}{{\underset{\raise 0.7em\alpha}{=}}} \newcommand{\yields}{\Rightarrow} \newcommand{\derives}{\overset{*}{\yields}} \newcommand{\alphaequiv}{=_{\alpha}} \newcommand{\tto}[2]{{\overset{#1}{\underset{#2}{\longrightarrow}}}} \newcommand{\transitsto}[2]{{\overset{#1}{\underset{#2}{\longrightarrow}}}} \newcommand{\xtransitsto}[2]{{\underset{#2}{\xrightarrow{#1}}}} \newcommand{\xtransitsfrom}[2]{{\underset{#2}{\xleftarrow{#1}}}} \newcommand{\xto}[2]{{\xtransitsto{#1}{#2}}} \newcommand{\xfrom}[2]{{\xtransitsfrom{#1}{#2}}} \newcommand{\xreaches}[2]{{\underset{#2}{\xtwoheadrightarrow{#1}}}} \newcommand{\reaches}[2]{{\underset{#2}{\xtwoheadrightarrow{#1}}}} %\newcommand{\reaches}[2]{{\overset{#1}{\underset{#2}{\twoheadrightarrow}}}} %\newcommand{\goesto}[2]{\transitsto{#1}{#2}} %\newcommand{\betareducesto}{{\underset{\beta}{\rightarrow}}} \newcommand{\betareducesto}{\rightarrow_{\beta}} %\newcommand{\etareducesto}{{\underset{\eta}{\rightarrow}}} \newcommand{\etareducesto}{\rightarrow_{\eta}} %\newcommand{\betaetareducesto}{{\underset{\beta\ \eta}{\rightarrow}}} \newcommand{\betaetareducesto}{\rightarrow_{\beta\eta}} \newcommand{\preducesto}{\rhd} \newcommand{\psimplifiesto}{\stackrel{\scriptstyle{*}}{\rhd}} \newcommand{\lreducesto}{\rightsquigarrow} \newcommand{\lsimplifiesto}{\stackrel{\scriptstyle{*}}{\lreducesto}} \newcommand{\rewritesto}{\hookrightarrow} \newcommand{\goesto}[1]{\stackrel{#1}{\rightarrow}} \newcommand{\xgoesto}[1]{\xrightarrow{#1}} \newcommand{\reducesto}{\stackrel{}{\rightarrow}} \newcommand{\simplifiesto}{\stackrel{\scriptstyle{*}}{\rightarrow}} \newcommand{\connected}[1]{\stackrel{#1}{\leftrightarrow}} \newcommand{\joins}{\downarrow} \newcommand{\evaluatesto}{\Longrightarrow} %\newcommand{\lit}[1]{\hbox{\sf{#1}}} \newcommand{\lit}[1]{{\sf{#1}}} \newcommand{\true}{\lit{true}} \newcommand{\false}{\lit{false}} \def\Z{\mbox{${\mathbb Z}$}} \def\N{\mbox{${\mathbb N}$}} \def\P{\mbox{${\mathbb P}$}} \def\R{\mbox{${\mathbb R}$}} \def\T{\mbox{${\mathbb T}$}} \newcommand{\Rp}{{\mathbb{R}}^+} \def\Bool{\mbox{${\mathbb B}$}} \def\Q{\mbox{${\mathbb Q}$}} \def\sA{\mbox{${\cal A}$}} \def\sB{\mbox{${\cal B}$}} \def\sC{\mbox{${\cal C}$}} \def\sD{\mbox{${\cal D}$}} \def\sF{\mbox{${\cal F}$}} \def\sG{\mbox{${\cal G}$}} \def\sL{\mbox{${\cal L}$}} \def\sP{\mbox{${\cal P}$}} \def\sM{\mbox{${\cal M}$}} \def\sN{\mbox{${\cal N}$}} \def\sR{\mbox{${\cal R}$}} \def\sS{\mbox{${\cal S}$}} \def\sO{\mbox{${\cal O}$}} \def\sT{\mbox{${\cal T}$}} \def\sU{\mbox{${\cal U}$}} \def\th{\mbox{$\widetilde{h}$}} \def\tg{\mbox{$\widetilde{g}$}} \def\tP{\mbox{$\widetilde{P}$}} \def\norm{\mbox{$\parallel$}} \def\osum{${{\bigcirc}}\!\!\!\!{\rm s}~$} \def\pf{\noindent {\bf Proof}~~} \def\exec{\mathit{exec}} \def\Act{\mathit{A\!ct}} \def\Traces{\mathit{Traces}} \def\Spec{\mathit{Spec}} \def\uns{\mathit{unless}} \def\ens{\mathit{ensures}} \def\lto{\mathit{leads\!\!-\!\!to}} \def\a{\alpha} \def\b{\beta} \def\c{\gamma} \def\d{\delta} \def\sP{\mbox{${\cal P}$}} \def\sM{\mbox{${\cal M}$}} \def\sA{\mbox{${\cal A}$}} \def\sB{\mbox{${\cal B}$}} \def\sC{\mbox{${\cal C}$}} \def\sI{\mbox{${\cal I}$}} \def\sS{\mbox{${\cal S}$}} \def\sD{\mbox{${\cal D}$}} \def\sF{\mbox{${\cal F}$}} \def\sG{\mbox{${\cal G}$}} \def\sR{\mbox{${\cal R}$}} \def\tg{\mbox{$\widetilde{g}$}} \def\ta{\mbox{$\widetilde{a}$}} \def\tb{\mbox{$\widetilde{b}$}} \def\tc{\mbox{$\widetilde{c}$}} \def\tx{\mbox{$\widetilde{x}$}} \def\ty{\mbox{$\widetilde{y}$}} \def\tz{\mbox{$\widetilde{z}$}} \def\tI{\mbox{$\widetilde{I}$}} \def\norm{\mbox{$\parallel$}} \def\sL{\mbox{${\cal L}$}} \def\sM{\mbox{${\cal M}$}} \def\sN{\mbox{${\cal N}$}} \def\th{\mbox{$\widetilde{h}$}} \def\tg{\mbox{$\widetilde{g}$}} \def\tP{\mbox{$\widetilde{P}$}} \def\norm{\mbox{$\parallel$}} \def\to{\rightarrow} \def\ov{\overline} \def\gets{\leftarrow} \def\too{\longrightarrow} \def\To{\Rightarrow} %\def\points{\mapsto} %\def\yields{\mapsto^{*}} \def\un{\underline} \def\vep{$\varepsilon$} \def\ep{$\epsilon$} \def\tri{$\bigtriangleup$} \def\Fi{$F^{\infty}$} \def\Di{\Delta^{\infty}} \def\ebox\Box \def\emp{\emptyset} \def\leadsto{\rightharpoondown^{*}} \newcommand{\benum}{\begin{enumerate}} \newcommand{\eenum}{\end{enumerate}} \newcommand{\bdes}{\begin{description}} \newcommand{\edes}{\end{description}} \newcommand{\bt}{\begin{theorem}} \newcommand{\et}{\end{theorem}} \newcommand{\bl}{\begin{lemma}} \newcommand{\el}{\end{lemma}} % \newcommand{\bp}{\begin{prop}} % \newcommand{\ep}{\end{prop}} \newcommand{\bd}{\begin{defn}} \newcommand{\ed}{\end{defn}} \newcommand{\brem}{\begin{remark}} \newcommand{\erem}{\end{remark}} \newcommand{\bxr}{\begin{exercise}} \newcommand{\exr}{\end{exercise}} \newcommand{\bxm}{\begin{example}} \newcommand{\exm}{\end{example}} \newcommand{\beqa}{\begin{eqnarray*}} \newcommand{\eeqa}{\end{eqnarray*}} \newcommand{\bc}{\begin{center}} \newcommand{\ec}{\end{center}} \newcommand{\bcent}{\begin{center}} \newcommand{\ecent}{\end{center}} % \newcommand{\la}{\langle} % \newcommand{\ra}{\rangle} \newcommand{\bcor}{\begin{corollary}} \newcommand{\ecor}{\end{corollary}} \newcommand{\bds}{\begin{defns}} \newcommand{\eds}{\end{defns}} \newcommand{\brems}{\begin{remarks}} \newcommand{\erems}{\end{remarks}} \newcommand{\bxrs}{\begin{exercises}} \newcommand{\exrs}{\end{exercises}} \newcommand{\bxms}{\begin{examples}} \newcommand{\exms}{\end{examples}} \newcommand{\bfig}{\begin{figure}} \newcommand{\efig}{\end{figure}} \newcommand{\set}[1]{\{#1\}} \newcommand{\pair}[1]{\langle #1\rangle} \newcommand{\tuple}[1]{\langle #1\rangle} \newcommand{\size}[1]{| #1 |} \newcommand{\union}{\cup} \newcommand{\Union}{\bigcup} \newcommand{\intersection}{\cap} \newcommand{\Intersection}{\bigcap} \newcommand{\B}{\textbf{B}} %\newcommand{\be}[2]{\begin{equation} \label{#1} \tag{#2} \end{equation}} \newcommand{\abs}[1]{{\lvert}#1{\rvert}} \newcommand{\id}[1]{\mathit{#1}} \newcommand{\pfun}{\rightharpoonup} \newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} \newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex} \newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}} \newcommand{\ua}[1]{\bigg\uparrow\raise.5ex\rlap{\scriptstyle#1}} % \newcommand{\lift}[1]{#1_{\bot}} \newcommand{\signal}[1]{\tilde{#1}} \newcommand{\ida}{\stackrel{{\sf def}}{=}} \newcommand{\eqn}{\doteq} \newcommand{\deduce}[1]{\sststile{#1}{}} %% These don't sit very well with MathJax %% so we don't plan to use theorem like environments %% in org documents. %% instead we plan to use headings with %% 1. property drawers with a CLASS property identifying %% the environment %% 2. A tag with the same name as the CLASS property %% In LaTeX export, these turn into (sub)sections. %% See http://u.cs.biu.ac.il/~tsaban/Pdf/LaTeXCommonErrs.pdf %% \newtheorem{prop}[thm]{Proposition} %% \theoremstyle{plain}%default %% \newtheorem{theorem}{Theorem}[section] %% \newtheorem{lemma}{Lemma}[section] %% \newtheorem{corollary}{Corollary}[section] %% \newtheorem{definition}{Definition}[section] %% \newtheorem{remark}{Remark}[section] %% \newtheorem{example}{Example}[section] %% \newtheorem{exercise}{Exercise}[section] \newcommand{\less}[1]{#1_{<}} \newcommand{\pfn}{\rightharpoonup} \newcommand{\ffn}{\stackrel{{\sf fin}}{\rightharpoonup}} \newcommand{\stkout}[1]{\ifmmode\text{\sout{\ensuremath{#1}}}\else\sout{#1}\fi} % Caution: Not supported by MathJax! % ---------------------------------- % \DeclareMathSymbol{\shortminus}{\mathbin}{AMSa}{"39} % \usepackage{amsfonts} %% <- also included by amssymb % \DeclareMathSymbol{\shortminus}{\mathbin}{AMSa}{"39} \usepackage{mathpazo} %% <- because the OP uses mathpazo, optional \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor} \newcommand{\ceil}[1]{\left\lceil #1 \right\rceil} \newcommand{\rel}{\twoheadrightarrow} \newcommand{\map}{\rightarrow} %\newcommand{\fixed}{\boldsymbol{\circlearrowleft}} \newcommand{\terminal}{\not\xto{}{}} \newcommand{\fixed}{\bm\circlearrowleft} \newcommand{\imp}{\rightarrow} \newcommand{\dimp}{\leftrightarrow} % double implication \newcommand{\lequiv}{\Longleftrightarrow} % logical equivalence \newcommand{\limplies}{\Rightarrow} \newcommand{\lxor}{\veebar} \)

Lecture notes on Lambda Calculus Part 2: Church Numerals and Computability

Table of Contents

1 Introduction

The \(\lambda\) calculus, is a minimalist programming language of great theoretical as well as practical importance. While Turing machines may be thought of inspiring models of computer hardware, the \(\lambda\) calculus is model for software, or programs. By the Church-Turing thesis of effective computability, both \(\lambda\) calculus and Turing machines are canonical models of effective computation. The \(\lambda\) calculus is also the basis for the design of many modern day programming languages.

1.1 Syntax

2 Lambda Calculus Syntax

\begin{align*} e ::= & & \scriptstyle{EXP} & \qquad \mbox{Expression}\\ & x & \scriptstyle{Id} & \qquad \mbox{Identifier}\\ & ({\texttt {lambda}}\ (x)\ e) & \scriptstyle{ABS} & \qquad \mbox{Abstraction}\\ & (e\ e) & \scriptstyle{APP} & \qquad \mbox{Application} \end{align*}

At a syntactic level, \(\lambda\) calculus is a system of manipulating expressions. Reduction is a relation on expressions.

At the semantic level, however, the purpose of studying \(\lambda\) expressions is to build a theory of functions to encode both data and computation.

Note that we are dealing with a hierarchy of three different domains. At the top, we have the domain of expressions in the lambda calculus. The meaning of these expressions is given by mathematical functions. These functions in turn, are used are used to encode data, like numbers, booleans.

Functions may be viewed as black boxes. Thus the function \(x\mapsto x+1\) may be seen as a black box. If you input \(5\) as an argument to it will return \(6\).

2.0.1 Notation

We use tt font when we write lambda expressions. We use mathematical italicized font when referring to the meaning of lambda expressions as black box functions. Finally, the data encoded by these black boxes will also be written in the italicized font.

For example, the lambda expression (lambda (x) (lambda (y) x)) denotes the black box function \(\lambda\ x.\ \lambda y.\ x\). This function, in turn, encodes the data element \(\id{true}\), a member of the set \(\id{BOOLEAN}\).

3 An embedding of $λ$-calculus in Scheme

It is this view that we will exploit simulate \(\lambda\) calculus in Scheme. So (closed) \(\lambda\) expressions will evaluate to closures, which are black boxes.

Note that $λ$-calculus is already built into Scheme! However, \(\lambda\) calculus is quite a bit more frugal: functions take exactly one formal parameter, and correspondingly, applications take a single argument. But we know how to create multiple argument functions from functions that take a single argument: currying.

4 Currying

(define :
  (lambda (f x . xs)
      [(null? xs) (f x)]
      [else (apply : (f x) xs)])))

(define-syntax lambda:
  (syntax-rules () 
    [(lambda: (x) body) (lambda (x) body)]
    [(lambda: (x y ...) body)
     (lambda (x) (lambda: (y ...) body))]))
(define-syntax define:
  (syntax-rules ()
    [(define: (f x y ...) body) (define f (lambda: (x y ...) body))]))

5 Modeling data in \(\lambda\) calculus

Computation involves programs manipulating data. If we wish to model computation in the $λ$-calculus, we would need to model, from scratch, things we take for granted in a high level programming languages: numbers, booleans, pairs for data, and conditionals, selectors, function abstraction and application, recursion, etc. .

In order to distinguish the language which we are studying and the meanings of expressions in that language that exist in a ``value'' domain, we will use different fonts to represent expressions and their meanings.

For example, the expression (lambda (x) x) denotes the function \(\lambda x.\ x\).

6 Booleans and Conditional

6.1 True and False

The primordial data elements true and false are defined as the following \(\lambda\) expressions.

(define: (true x y) x)
(define: (false x y) y)

(check-equal? (: true 2 5) 2)
(check-equal? (: false 2 5) 5)
(check-equal? (: true 'love-me 'love-me-not) 'love-me)

(define (show-bool b)
  (: b #t #f))

Notice that true is short hand for (lambda: (x y) x) which itself is a short hand for (lambda (x) (lambda (y) x)). (You may want to appreciate the mileage we are deriving from the compact define: notation.) The meaning of true, however, is the function (a black box) \(\id{TRUE}\) that takes an argument \(x\) and returns a function (another black box) that takes an argument \(y\) and returns \(x\).

One way of thinking about \(\id{TRUE}\) and \(\id{FALSE}\) is that they are selectors: the former selects its first argument, while the latter selects the second argument, whatever those arguments are:

6.2 If-then-else

A conditional takes three arguments (curried of course!). The first is a boolean (either true or false). The result is applying the first argument, a boolean, to the other two.

(define:  (ifte x y z) (: x y z))
(check-equal? (: ifte true 2 5) 2)
(check-equal? (: ifte false 2 5) 5)

6.3 Other boolean operators

and, or, not and xor may follow easily:

(define: (not a)
  (: ifte a false true))
(define: (and a b)
  (: ifte a b false))
(define: (or a b)
  (: ifte a true b))
(define: (xor a b)
  (: ifte a (not b) b))

(check-equal? (: (not true) 3 5) 5)
(check-equal? (: (: and true false) 3 5) 5)
(check-equal? (: (: or true false) 3 5) 3)
(check-equal? (: (: or false false) 3 5) 5)
(check-equal? (: (: xor false true) 3 5) 3)

7 Church Numerals

We next consider an encoding of natural numbers via black boxes:

7.1 Zero

z encodes the number \(0\).

(define: (z f x)  x)

One way thinking about it that \(\id{ZERO}\) is that when supplied arguments \(f\) and \(x\) \(\id{ZERO}\) computes the value \(f^0(x)\).

This suggests that the number \(n\) may be encoded as the blackbox function \(n\) which is \(\lambda\ f.\ \lambda\ x. f^{n}(x)\)

7.2 Successor

(define: (s n f x) 
  (f (: n f x)))

(define zero z)
(define one (s zero))
(define two (s one))
(define three (s two))

(define (show-nat n)
  (: n add1 0))
(check-equal? (show-nat zero) 0)
(check-equal? (show-nat one) 1)
(check-equal? (show-nat two) 2)

(check-equal? (: zero add1 5) 5)
(check-equal? (: one add1 5) 6)
(check-equal? (: two add1 5) 7)
(check-equal? (: three add1 5) 8)
(check-equal? (: ifte true (: two add1 5) (: zero add1 5)) 7)
(check-equal? (: ifte true two zero add1 5) 7)
(check-equal? (: ifte false two zero add1 5) 5)

7.3 zero?

(define: (z? n)
  (: n (lambda (x) false) true))

Note that this denotes the application \(f^n(\id{true})\) where \(f\) is the function \(\lambda\ x.\ \id{false}\). When \(n\) is \(0\), then the result is $\id{true}, otherwise, it is \(\id{false}\).

7.4 Addition

(define: (add m n f x)
  (: m f (: n f x)))
(check-equal? (: add one two add1 5) 8)

7.5 Multiplication

(define: (mul m n f)
  (m (n f)))

(check-equal? (: mul two three add1 5) 11)
(check-equal? (: mul zero three add1 5) 5)
(check-equal? (: mul one three add1 5) 8)

8 Pairs

(define: (pair a b sel)
  (: sel a b))

(define: (fst p)
  (p true))

(define: (snd p)
  (p false))

(check-true (eq? (fst (: pair one two)) one))
(check-true (eq? (snd (: pair one two)) two))

9 Predecessor and Saturated Subtraction

9.1 next

p is a pair of numbers. (next (: pair a b)) returns (: pair (s a) a).

(define:  (next p)
  (: pair (s (fst p)) (fst p)))

(check-equal? (: fst (: next (: pair z z)) add1 4) 5)
(check-equal? (: snd (: next (: pair z z)) add1 4) 4)
(check-equal? (: fst (: next (: pair one two)) add1 4) 6)
(check-equal? (: snd (: next (: pair one two)) add1 4) 5)

9.2 Predecessor

(: pred zero) is defined to be zero. Recall that if n denotes the Church numeral \(n\), and f an arbitrary function \(f\) then (: n f) denotes the function \(f^n\). Also note that \(\id{next}^{n}\pair{0,0}\) denotes the function \(\id{next}^f\pair{0,0}\), which yields \(\pair{n, n-1}\). \(\id{pred}(n) = \id{snd}\pair{n, n-1}\), which equals \(\id{snd}(\id{next}^n\pair{0,0})\).

(define: (pred n)
  (snd (: n next (: pair z z))))
(check-equal? (: pred one add1 5) 5)
(check-equal? (: pred zero add1 5) 5)
(check-equal? (: pred three add1 5) 7)

9.3 Saturated subtraction

Subtracting \(n\) from \(m\) is just taking the predecessor of \(m\) \(n\) times:

(define: (sub m n)
  (: n pred m))

9.4 Relational operators on numbers

(define: (leq m n) ; m <= n
  (: z? (: sub m n)))

(define: (geq m n) ; m >= n
  (: z? (: sub n m)))

(define: (gt m n) ; m > n
  (: not (: leq m n)))

(define: (lt m n) ; m < n
  (: not (: geq m n)))

(define: (eq m n) ; m = n
  (: and (leq m n) (leq n m)))

10 Universality of lambda calculus

Once we have recursion and the basic datatypes, it is not hard to see that we can take a Turing machine, and implement it. A Turing machine has a tape (with a finite segment containing symbols), a head (which is a finite state machine) and a tape counter (the position of the head on the tape).

11 References and online resources

Benjamin Lynn's notes on lambda calculus
Provides excellent notes motivating lambda calculus and presents a one-line universal machine (but without proof of its universality) in the lambda calculus.
Manuel Eberl's notes on Untyped Lambda Calculus
Systematically develops data types in the lambda calculus.
Functional Bits: Lambda Calculus based Algorithmic Information Theory
by John Tromp. A theory of the binary lambda calculus. Shows how to build a universal machine in lambda calculus and combinatory theory. You may also want to see John Tromp's page on Binary Lambda Calculus.
David Evans's slides on the Lambda calculus
Shows how one might convert a Turing Machine into a Lambda calculus machine.
Cornell CS 312 Recitation on Lambda Calculus
A short tutorial introduction to Lambda calculus.
CS329 IIT Bombay: Notes on Lambda Calculus
Notes by Rushikesh Joshi.
Garrigue's notes on Computability and Lambda Calculus
Demonstrates the simulation of a Turing machine by a Lambda Calculus term and vice versa.
Lambda calculus: The other Turing Machine
Harvard CS50 talk by Guy Blelloch and Robert Harper

Author: Venkatesh Choppella

Created: 2023-11-25 Sat 09:15