程序设计语言的形式语义

2 - Lambda Calculus

2019-09-29 10:00 CST
2019-12-20 11:35 CST
CC BY-NC 4.0

Introduction

What is $\lambda$-calculus?

  • Programming language
  • Model for computation

Why learn $\lambda$-calculus?

  • Foundations of functional programming
  • Offen used as a core language to study language theories

$\lambda$-calculus as a language

PL = syntax (语法) + semantics (语义)

  • Syntax: How to write a program?
  • Semantics: How to describe the executions of a program?
  • Others: Type system, model theory, …

Syntax

$\lambda$-terms or $\lambda$-expressions:

(Terms) $M, N ::= x \vert \lambda x.M \vert MN$

$M ::= x \vert n \vert \lambda x.M \vert MN \vert M+N$

  • Lambda abstraction ($\lambda x.M$): anonymous functions
    • int f(int x){return x;} $\Rightarrow \lambda x.\ x$
  • Lambda application ($MN$)
    • f(3) $\Rightarrow (\lambda x.\ x)\ 3$

Conventions

  • Body of $\lambda$ extends as far to the right as possible
    • $\lambda x.\ \ M\ N$ means $\lambda x.\ (M\ N)$, not $\sout{(\lambda x.\ M)\ N}$
    • $\lambda x.\ \lambda f.\ f\ x = \lambda x.\ (\lambda f.\ (f\ x))$
  • Function applications are left-associative
    • $MNP$ means $(MN)P$, not $\sout{M(NP)}$
    • $(\lambda x.\ \lambda y.\ x - y)\ 5\ 3 = ((\lambda x.\ \lambda y.\ x - y)\ 5)\ 3 = 5-3$

Higher-order Functions

  • Functions can be returned as return values
    • $\lambda x.\ \lambda y.\ x - y$ is a function that takes $x$, returns a function $\lambda y.\ x - y$.
  • Functions can be passed as arguments
    • $(\lambda f.\ \lambda x.\ f\ x) (\lambda x.\ x + 1) \ 2$ passes a function.

Example. Given function $f$, return function $f \circ f$: $$\lambda f.\ \lambda x.\ f\ (f\ x)$$

$$\begin{aligned} & (\lambda f.\ \lambda x.\ f\ (f\ x)) (\lambda y.\ y+1)\ 5 \\ &= (\lambda x. \ (\lambda y.\ y+1) ((\lambda y.\ y+1)\ x))\ 5 \\ &= (\lambda y.\ y+1)\ 6 = 7.\end{aligned}$$

Curried Functions

Notice difference between

  • $\lambda x.\ \lambda y.\ x - y$: returns a function f(y)
  • int f(int x, int y){return x-y;}: returns a value

$\lambda$ abstraction is a function of $1$ parameter.

But computationally they are the same. They can be transformed by currying: transform $\lambda (x, y)$ to $\lambda x, \lambda y$.

Free and Bound Variables

$\lambda x. x + y$

  • $x$: bound variable (can be renamed, “placeholder”)
  • $y$: free variable
  • $(x+y)$ is the scope (作用域) of the binding $\lambda x$

$(\lambda x. x + y)(x+1)$: $x$ has both a free and a bound occurrence, the same as

int x = 114, y = 514;
int foo(int x) {
  return x + y;
}
add(x+1);

Formal definition about free and bound variables? $\Rightarrow$ 《数理逻辑》

  • $\text{fv}(x) = \{x\}$,
  • $\text{fv}(\lambda x.M) = \text{fv}(M) \setminus \{x\}$,
  • $\text{fv}(MN) = \text{fv}(M) \cup \text{fv}(N)$.

$\alpha$-equivalence: $\lambda x.M = \lambda y. M\left[\dfrac{y}{x}\right]$, where $y$ fresh

Semantics

Reduction

$\beta$-reduction: $(\lambda x.M)N \rightarrow M\left[\frac{N}{x}\right]$

Repeatedly apply $\beta$-reduction rule to any sub-term.

Substitution

$M\left[\frac{N}{x}\right]$: replace $x$ by $N$ in $M$.

  • $x[N/x] = N$
  • $y[N/x] = y$
  • $(MP)[N/x] = (M[N/x])(P[N/x])$
  • $(\lambda x.M)[N/x] = M$ ($x$ is a bound variable)
  • $(\lambda y.M)[N/x] = \lambda y. (M[N/x])$ if $y \notin \text{fv}(N)$
  • $(\lambda y.M)[N/x] = \lambda z. (M[z/y][N/x])$ if $y \in \text{fv}(N)$ and $z$ fresh

Reduction Rules

$${\over (\lambda x.M)N \rightarrow M[N/x]} (\beta)$$

Repeatedly apply $(\beta)$ to any sub-term:

$${M \rightarrow M' \over MN \rightarrow M’N}$$

$${N \rightarrow N' \over MN \rightarrow MN'}$$

$${M \rightarrow M' \over \lambda x.M \rightarrow \lambda x.M'}$$

Normal Form

  • $\beta$-redex: a term of the form $(\lambda x.M) N$
  • $\beta$-normal form: aterm containing no $\beta$-redex
    • Stopping point: cannot further apply $\beta$-reduction rules

Confluence (Church-Rosser Property): terms can be evaluated in any order. Final result (if there is one) is uniquely determined.

Corollary of confluence theorem: with $\alpha$-equivalence, every term has at most one normal form. Some reduction methods may not come out with a normal form.

Reduction Strategies

  • Normal-order reduction: choose the left-most, outer-most redex first.
  • Applicative-order reduction: choose the left-most, inner-most redex first.

Theorem: normal-order reduction will find normal form if exists.

Examples:

  • Normal-order: $$\begin{aligned} &(\lambda x.\ x\ x) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow ((\lambda y.\ y) (\lambda z.\ z)) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow (\lambda z.\ z) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow \lambda z.\ z \end{aligned}$$
  • Applicative-order: $$\begin{aligned}&(\lambda x.\ x\ x) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow (\lambda x.\ x\ x) (\lambda z.\ z) \\ &\rightarrow (\lambda z.\ z) (\lambda z.\ z) \\ &\rightarrow \lambda z.\ z \end{aligned}$$

Evaluation Strategies

  • Only evaluate closed terms (i.e., no free variables)
  • May not reduce all the way to a normal form.

Evaluation don’t reduce under lambda (terminates after first canonical form (i.e., lambda abstraction, or $\lambda x. M$)).

  • Call-by-name (like normal-order): ALGOL 60
  • Call-by-need (memorized call-by-name, lazy evaluation): Haskell, R, …
  • Call-by-value(like applicative-order, eager evaluation): C, …

Normal Order Evaluation Rules

$${\over \lambda x. M \Rightarrow \lambda x. M}(\text{Term})$$

$${M \Rightarrow \lambda x. M' \ \ \ \ \ M'[N/x] \Rightarrow P \over MN \Rightarrow P}(\beta)$$

Eager Evaluation Rules

$${\over \lambda x. M \Rightarrow_E \lambda x. M}(\text{Term})$$

$${M \Rightarrow_E \lambda x. M' \ \ \ \ N \Rightarrow_E N' \ \ \ \ M'[N'/x] \Rightarrow_E P \over MN \Rightarrow_E P}(\beta)$$

Programming in $\lambda$-calculus

Encoding Boolean Values and Operators

  • True: $\lambda x.\ \lambda y.\ x$
  • False: $\lambda x.\ \lambda y.\ y$
  • Not: $\lambda b. \texttt{ False True}$, or $\lambda b.\ \lambda x.\ \lambda y.\ b\ y\ x$
  • And: $\lambda b.\ \lambda b'.\ b\ b'\ \texttt{False}$
  • Or: $\lambda b.\ \lambda b'.\ b\ \texttt{True}\ b'$
  • If $b$ then $M$ else $N$: $b M N$

Church Numerals

  • 0: $\lambda f.\ \lambda x.\ x$
  • 1: $\lambda f.\ \lambda x.\ f\ x$
  • n: $\lambda f.\ \lambda x.\ f^n\ x$
  • succ: $\lambda n.\ \lambda f.\ \lambda x.\ f\ (n\ f\ x)$
  • iszero: $\lambda n.\ \lambda x.\ \lambda y.\ n\ (\lambda z.\ y)\ x$
  • add: $\lambda n.\ \lambda m.\ \lambda f.\ \lambda x.\ n\ f\ (m\ f\ x)$
  • mult: $\lambda n.\ \lambda m.\ \lambda f.\ \lambda x.\ n\ (m\ f\ x)$

Pairs and Tuples

  • $(M, N): \lambda f.\ f\ M\ N$
  • $\pi_0: \lambda p.\ p\ (\lambda x.\ \lambda y.\ x)$
  • $\pi_1: \lambda p.\ p\ (\lambda x.\ \lambda y.\ y)$

$\pi_i = \lambda p.\ p\ (\lambda x_1. \ \cdots \lambda x_n.\ x_i)$

Fixpoint in Arithmetics

$x$ is a fixpoint of $f$ if $f(x) = x$.

In $\lambda$-calculus, every term has a fixpoint.

Fixpoint combinator is a higher-order function $h$ satisfying that for all $f$, $(h\ f)$ gives a fixpoint of $f$, i.e. $h\ f = f(h\ f)$.

  • Turing’s fixpoint combinator $\Theta$: $$A = \lambda x.\ \lambda y.\ y\ (x\ x\ y), \Theta = A\ A$$
  • Church’s fixpoint combinator $\textbf{Y}$: $$\textbf{Y} = \lambda f.\ (\lambda x.\ f\ (x\ x)) (\lambda x.\ f\ (x\ x))$$

Let $F = \lambda f.\ \lambda n.\ \texttt{if } iszero(n) \texttt{ then } 1 \texttt{ else } n * f(n-1)$, the factorial function $fact$ is a fixpoint of $F$, i.e. $fact = \Theta F$. The right-hand side is a closed lambda term that represents the factorial function.