EECS 762

Programming Language Foundation I

Index
Blog

EECS 762 Blog

Homework Update

I got a question on Homework question 5. You do not need to deal with any language additions other than wildcards. Also, if is not officially part of the simply typed calculus, so you needn’t include it in your proofs. Shouldn’t be too difficult if you choose to add it.


Homework Formatting

I managed to fix the formatting for Homework 3. Turned out to be a difference betwee Obsidian math formatting and mathjax formatting that I forgot about.


Notes

Links to my class notes as of 3/23 suitable for viewing in Obsidian.

preamble.sty defines some LaTeX macros that you will need. Either use the preamble directly or add its definitions to your preamble.


Class Notes

[\newcommand{\typing}[3][\Gamma]{#1 \vdash #2 : #3} \newcommand{\llbracket}{\textlbrackdbl} \newcommand{\rrbracket}{\textrbrackdbl} \newcommand{\oxford}[1]{\llbracket #1\rrbracket} \newcommand{\denotes}[2][v]{\oxford{#2}#1} \newcommand{\compile}[1]{\lfloor #1\rfloor} \newcommand{\lift}[1]{\lceil #1\rceil} \newcommand{\encrypt}[2]{{#1}{#2}} \newcommand{\sign}[2]{{!|#1|!}{#2}} \newcommand{\hash}[1]{|#1|} \newcommand{\evalop}{\rightarrow} \newcommand{\evalopm}{\rightarrow^*} \newcommand{\eval}{\;\evalop\;} \newcommand{\evals}[2]{#1\evalop #2} \newcommand{\evalm}[2]{#1\evalopm #2} \newcommand{\succ}{\mathsf{succ}\;} \newcommand{\pred}{\mathsf{pred}\;} \newcommand{\iszero}{\mathsf{isZero}\;} \newcommand{\ifte}[3]{(\mathsf{if}\ #1\ #2\ #3)} \newcommand{\tru}{\mathsf{true}} \newcommand{\fls}{\mathsf{false}} \newcommand{\RLS}[1]{\RL{\quad\textsf{#1}}}]

Happy, Happy, Joy, Joy

EECS 762 - Programming Language Foundation I

Why Should We Learn This Stuff?

Things are getting too complex and dangerous for ad hoc methods

Fundamentals

Defining Syntax as Sets

Our first (very broken) language of untyped arithmetic expressions

Each of these definitions defines the same set of terms:

Traditional Grammar

\(t = \tru \mid \fls \mid \ifte{t}{t}{t} \mid 0 \mid \succ t \mid \pred t \mid \iszero t\) You should have seen this definition in your computation theory class

Inductive Definition

\(\begin{array}{rcl} \{\tru,\fls,0\} & \subseteq & T \\ \forall t:T \cdot \{\succ t,\pred t,\iszero t\} & \subseteq & T \\ \forall t_c,t_t,t_e:T \cdot \ifte{t_c}{t_t}{t_e} & \in & T \\ \end{array}\)

Why do we call this inductive?

Inference Rules

\(\begin{prooftree} \AxiomC{} \UnaryInfC{$\tru\in T$} \end{prooftree} ~ \begin{prooftree} \AxiomC{} \UnaryInfC{$\fls\in T$} \end{prooftree} ~ \begin{prooftree} \AxiomC{} \UnaryInfC{$0\in T$} \end{prooftree}\) \(\begin{prooftree} \AxiomC{$t\in T$} \UnaryInfC{$\succ t\in T$} \end{prooftree} ~ \begin{prooftree} \AxiomC{$t\in T$} \UnaryInfC{$\pred t\in T$} \end{prooftree} ~ \begin{prooftree} \AxiomC{$t\in T$} \UnaryInfC{$\iszero t\in T$} \end{prooftree}\)

\(\begin{prooftree} \AxiomC{$t_c\in T$} \AxiomC{$t_t\in T$} \AxiomC{$t_e\in T$} \TrinaryInfC{$\ifte{t_c}{t_t}{t_e}\in T$} \end{prooftree}\) ~~This is inductive too!

\(\begin{prooftree} \AxiomC{$A$} \AxiomC{$C$} \BinaryInfC{$D$} \end{prooftree}\) ~~says that if $A$ and $C$ are true, the $D$ follows immediately and is true

Fixed Point

\(\begin{array}{rcl} S_0 & = & \emptyset \\ S_{n+1} & = & \{\tru,\fls,0\} \\ & & \cup\ \{\succ t,\pred t,\iszero t\mid t\in S_n \} \\ & & \cup\ \{\ifte{t_c}{t_t}{t_e}\mid t_c,t_t,t_e\in S_n\} \\ \\ T & = & \bigcup_i S_i \end{array}\)

Thoughts

Equational Reasoning

Defining Terms

Define $\textsf{consts}$, a function that finds the set of unique constants in a term from $T$.

\(\begin{array}{rcl} \mathsf{consts}\ \tru & = & \{\tru\} \\ \mathsf{consts}\ \fls & = & \{\fls\} \\ \mathsf{consts}\ 0 & = & \{0\} \\ \mathsf{consts}\ \succ t & = & \mathsf{consts}\ t \\ \mathsf{consts}\ \pred t & = & \mathsf{consts}\ t \\ \mathsf{consts}\ \iszero t & = & \mathsf{consts}\ t \\ \mathsf{consts}\ \ifte{t_c}{t_t}{t_e} & = & \mathsf{consts}\ t_c \cup \mathsf{consts}\ t_t \cup \mathsf{consts}\ t_e \\ \end{array}\)

Evaluating Terms

If \(A=B\) then we can replace \(A\) with \(B\) wherever \(A\) occurs (Leibniz Equality)

consts (if true then (succ 0) else (pred 0))
= (consts true) U (consts (succ 0)) U (consts (pred 0)) - Definition of consts if
= {true} U (consts 0) U (consts 0)                  - Definition of consts true, succ & pred
= {true} U {0} U {0}                                - Definition of consts 0
= {true,0}                                          - Definition of union

How do we know this definition is complete?

How do we know this definition is a function?

What if we skip a case?

Example: \(\mathsf{terms}\)

Define \(\mathsf{terms}\), a function that calculates the number of subterms in a term

terms true = 1
terms false = 1
terms 0 = 1
terms succ t = 1 + terms t
terms pred t = 1 + terms t
terms isZero t = 1 + term t
terms (if c t e) = 1 + terms c + terms t + terms e
terms (if true (succ 0) (pred (succ 0)))
= 1 + terms true + terms succ 0 + terms pred (succ 0)
= 1 + 1 + (1 + terms 0) + (1 + terms (succ 0))
= 2 + (1+1) + (1 + (1 + terms 0))
= 4 + (1 + (1 + 1))
= 7

Thoughts

Structural Induction and Friends

Math Induction

If \(P(0)\) holds and \(\forall n\cdot P(n)\Rightarrow P(n+1)\) then \(P\) holds for every \(n\).

How does this work?

Can we take advantage of that structure?

A First Example

Let’s prove the number of constants in a term is always less than the number of subterms.

First, should this actually be true??

[\forall t . \mathsf{consts}\ t \leq \mathsf{terms}\ t]

Why these cases?

Induction Schemes

Depth Induction

If for each term \(t\)

Size Induction

If for each term \(t\)

Structural Induction

Structural Induction is an alternative to math induction that is well-suited for proofs over abstract syntax.

If for each term \(t\)

For our language:

This is what we did above with $$P(t)= \textsf{consts}\ t \leq\textsf{terms}\ t$$

Small-Step Operational Semantics

The definitions of consts and terms define the semantics of those functions by defining functions from terms to sets and numbers respectively.

Small-step operational semantics define the semantics of evaluation.

Basic Principles

A single step evaluation relation defines when one term evaluates to another in one step. Usually written using the notation: \(t\rightarrow t'\) and is read “$t$ evaluates to $t’$ in one step.”

\(t\rightarrow t'\) is a homogeneous relation:

Examples we might write for our arithmetic language include

How do we choose and where do we start?

What do \(\tru\), \(\fls\), and \(0\) evaluate to? $$ \begin{prooftree} \AxiomC{} \UnaryInfC{$\tru\eval ??$} \end{prooftree}

\begin{prooftree}
	\AxiomC{}
	\UnaryInfC{$\fls\eval ??$}
\end{prooftree}

\begin{prooftree} \AxiomC{} \UnaryInfC{$0\eval ??$} \end{prooftree} \(How about\)\succ 0\(,\)\pred 0\(?\) \begin{prooftree} \AxiomC{} \UnaryInfC{$\succ 0\eval ??$} \end{prooftree}

\begin{prooftree}
	\AxiomC{}
	\UnaryInfC{$\pred 0\eval ??$}
\end{prooftree}
$$
**Rule 1**: Do not write rules for things that do not evaluate:

How about $$\pred (\succ 0)$$?
$$
\begin{prooftree}
	\AxiomC{}
	\UnaryInfC{$\pred(\succ 0)\eval 0$}
\end{prooftree}
$$

But we can be more general:
$$
\begin{prooftree}
	\AxiomC{}
	\UnaryInfC{$\forall t\cdot\pred(\succ t)\eval t$}
\end{prooftree}
$$

What about this one:

$$
\begin{prooftree}
	\AxiomC{}
	\UnaryInfC{$\forall t\cdot\pred(\succ(\pred(\succ t)))\eval t$}
\end{prooftree}
$$

**Rule 2**: Each rule should capture exactly one step in the evaluation process

How do we capture nested computations?

$$
\begin{prooftree}
	\AxiomC{$t\eval t'$}
	\UnaryInfC{$\succ t\eval\succ t'$}
\end{prooftree}

\begin{prooftree} \AxiomC{$t\eval t’$} \UnaryInfC{$\pred t\eval\pred t’$} \end{prooftree}

\begin{prooftree}
	\AxiomC{$t\eval t'$}
	\UnaryInfC{$\iszero t\eval\iszero t'$}
\end{prooftree}
$$

**Rule 3:** Evaluate subterms before terms

$$
\begin{prooftree}
	\AxiomC{}
	\UnaryInfC{$\ifte{\tru}{t_t}{t_e}\eval t_t$}
\end{prooftree}

\begin{prooftree} \AxiomC{} \UnaryInfC{$\ifte{\fls}{t_t}{t_e}\eval t_e$} \end{prooftree} ~~~ \begin{prooftree} \AxiomC{$t_c\eval t_c’$} \UnaryInfC{$\ifte{t_c}{t_t}{t_e}\eval\ifte{t’_c}{t_t}{t_e} $} \end{prooftree} $$

I want to evaluate \(\pred(\succ(\pred(\succ t)))\). Which rule is best? \(\begin{prooftree} \AxiomC{} \UnaryInfC{$\forall t\cdot\pred(\succ t)\eval t$} \end{prooftree}\)\(\begin{prooftree} \AxiomC{} \UnaryInfC{$\forall t\cdot\pred(\succ(\pred(\succ t)))\eval t$} \end{prooftree}\) Rule 4: Each term should match exactly one rule

To summarize:

Rules of Thumb:

  1. Do not define evaluation rules for things that do not evaluate
  2. Each rule should capture exactly one step in the evaluation process
  3. Evaluate subterms before their terms
  4. No term should have more than one matching inference rule

Definitions:

Properties

When defining a language in the “Pierce Style,” specify Syntax and rules for evaluation:

Syntax t ::= true | false | (if t t t) v ::= true | false

Evaluation \(\begin{prooftree}\AXC{}\RLS{IfTrue}\UIC{\(\ifte{\tru}{t}{e} \eval t\)}\end{prooftree}\)

[\begin{prooftree}\AXC{}\RLS{IfFalse}\UIC{(\ifte{\fls}{t}{e} \eval e)}\end{prooftree}]

[\begin{prooftree}\AXC{(c\eval c’)}\RLS{If}\UIC{(\ifte{c}{t}{e}\eval\ifte{c’}{t}{e})}\end{prooftree}]

We will do this for the remainder of the course. Lots of times!

Theorem: Determinicity of one step evaluation

If \(t\eval t'\) and \(t\eval t''\) then \(t'=t''\)

Proof by induction on \(t\)

More Definitions

Theorem: Values are normal forms

Proof by cases on t:

Theorem: Normal Forms are Values

Multistep Evaluation

Definition The multi-step evaluation relation (\(r\rightarrow^* r'\)) is the reflexive, transitive closure of the single step relation (\(r\rightarrow r'\)):

  1. if \(t\rightarrow t'\) then \(t\rightarrow^* t'\)
  2. \(t\rightarrow^* t\) for all \(t\)
  3. if \(t\rightarrow^* t'\) and \(t'\rightarrow t''\) then \(t\rightarrow^*t''\)

Can we define these things with inference rules? \(\begin{prooftree}\AXC{}\RLS{ERefl}\UIC{\(t\rightarrow^* t\)}\end{prooftree}\)

[\begin{prooftree}\AXC{(t\rightarrow t’)}\RLS{EStep}\UIC{(t\rightarrow^* t’)}\end{prooftree}]

[\begin{prooftree}\AXC{(t\rightarrow^* t’)}\AXC{(t’\rightarrow t’’)}\RLS{ETrans}\BIC{(t\rightarrow^* t’’)}\end{prooftree}]

A couple of theorems will help us along.

Theorem (Uniqueness of Normal Forms) if \(\evalm{t}{u}\) and \(\evalm{t}{u'}\) then \(u=u'\)

Theorem (Termination of Evaluation) For every term \(t\) there is a normal form \(u\) such that \(\evalm{t}{u}\).

Proofs and Derivations

A derivation or proof is a collection of inference rules used in sequence.

Example 1

\(\begin{prooftree} \AXC{} \UIC{$\evals{\ifte{\tru}{\fls}{\tru}}{\fls}$} \end{prooftree}\) What is the proof here?

\(\begin{prooftree} \AXC{}\RLS{EIfTrue} \UIC{$\evals{\ifte{\tru}{\fls}{\tru}}{\fls}$} \end{prooftree}\) We use $\mathsf{EIfTrue}$ one time and get from nothing to the thing we would like to prove. A trivial one-step proof. This is not interesting.

Example 2

[\begin{prooftree} \AXC{} \UIC{$\evals{\ifte{\ifte{\tru}{\fls}{\fls}}{\tru}{\fls}}{\ifte{\fls}{\tru}{\fls}}$} \end{prooftree}]

Here we use $\mathsf{EIf}$, but this rule has an antecedent that we must prove. That proof is done using $\mathsf{EIfTrue}$ \(\begin{prooftree} \AXC{}\RLS{EIfTrue} \UIC{$\evals{\ifte{\tru}{\fls}{\fls}}{\fls}$}\RLS{EIf} \UIC{$\evals{\ifte{\ifte{\tru}{\fls}{\fls}}{\tru}{\fls}}{\ifte{\fls}{\tru}{\fls}}$} \end{prooftree}\)

Back to our arithmetic language, but let’s try to be systematic about the definition.

Example 3

Now let’s do the proof we really want to do by evaluating an $\mathsf{if}$ expression to a value: \(\begin{prooftree} \AXC{} \UIC{$\evals{\ifte{\ifte{\fls}{\tru}{\ifte{\tru}{\fls}{\tru}}}{\tru}{\fls}}{\fls}$} \end{prooftree}\) This one is a different than the first because we have two nested evaluations, one in the else branch of an if. If we were in math class we would do a simple transformation of the left side. How do we do this with inference rules?

Let’s take one step using $\textsf{EIf}$ \(\begin{prooftree} \AXC{} \UIC{$\evals{\ifte{\fls}{\tru}{\ifte{\tru}{\fls}{\tru}}}{\ifte{\tru}{\fls}{\tru}}$}\RLS{EIf} \UIC{$\evals{\ifte{\ifte{\fls}{\tru}{\ifte{\tru}{\fls}{\tru}}}{\tru}{\fls}}{\ifte{\ifte{\tru}{\fls}{\tru}}{\tru}{\fls}}$} \end{prooftree}\) Now we’re stuck until we remember $\evalm{t}{t’}$. If we can show the right hand side of the goal evaluates to something, then then left hand side will too. Let’s us $\textsf{EIf}$ again to take the next step: \(\begin{prooftree} \AXC{$\evals{\ifte{\tru}{\fls}{\tru}}{\fls}$}\RLS{EIf} \UIC{$\evals{\ifte{\ifte{\tru}{\fls}{\tru}}{\tru}{\fls}}{\ifte{\fls}{\tru}{\fls}}$} \end{prooftree}\) Now we can plug the two steps together using the transitive rule. To use it we need to show

[\begin{prooftree} \AXC{$\evals{\ifte{\ifte{\tru}{\fls}{\ifte{\tru}{\fls}{\tru}}}{\tru}{\fls}}{\ifte{\ifte{\tru}{\fls}{\tru}}{\tru}{\fls}}$}\RLS{EStep} \UIC{$\evalm{\ifte{\ifte{\tru}{\fls}{\ifte{\tru}{\fls}{\tru}}}{\tru}{\fls}}{\ifte{\ifte{\tru}{\fls}{\tru}}{\tru}{\fls}}$} \end{prooftree}]

Using the transitive rule we now know that: \(\begin{prooftree} \AXC{$\evalm{\ifte{\ifte{\tru}{\fls}{\ifte{\tru}{\fls}{\tru}}}{\tru}{\fls}}{\ifte{\ifte{\tru}{\fls}{\tru}}{\tru}{\fls}}$} \noLine \UIC{$\evals{\ifte{\ifte{\tru}{\fls}{\tru}}{\tru}{\fls}}{\ifte{\fls}{\tru}{\fls}}$}\RLS{ETrans} \UIC{$\evalm{\ifte{\ifte{\tru}{\fls}{\ifte{\tru}{\fls}{\tru}}}{\tru}{\fls}}{\ifte{\fls}{\tru}{\fls}}$} \end{prooftree}\)

Note the switch from $\evalop$ to $\evalop^*$.

One more time will do the trick. We know:

[\begin{prooftree} \AXC{}\RLS{EIfFalse} \UIC{$\evals{\ifte{\fls}{\tru}{\fls}}{\fls}$} \end{prooftree}]

Transitivity again gives us what we want:

[\begin{prooftree} \AXC{$\evalm{\ifte{\ifte{\tru}{\fls}{\tru}}{\tru}{\fls}}{\ifte{\fls}{\tru}{\fls}}$} \AXC{$\evals{\ifte{\fls}{\tru}{\fls}}{\fls}$}\RLS{ETrans} \BIC{$\evalm{\ifte{\ifte{\tru}{\fls}{\ifte{\tru}{\fls}{\tru}}}{\tru}{\fls}}{\fls}$} \end{prooftree}]

Bingo!

There is a pattern working here:

  1. Do a proof of the first step $\evals{t_0}{t_1}$
  2. Lift into the multistep relation to get $\evalm{t_0}{t_1}$
  3. Do a proof of the second step $\evals{t_1}{t_2}$
  4. Use the transitive rule with $\evalm{t_0}{t_1}$ and $\evals{t_1}{t_2}$ to get $\evalm{t_0}{t_2}$
  5. Do a proof of the third step $\evals{t_2}{t_3}$
  6. Use the transitive rule again to get $\evalm{t_0}{t_3}$
  7. Repeat until you get where you’re going

This is a nifty pattern for both proof and evaluation.

Arithmetic Language Redux

Let’s rebuild our arithmetic language. Carefully this time.

Syntax

t ::= true | false | 0 | (if t t t) | succ t | pred t | isZero t v ::= true | false | nv nv ::= 0 | succ nv

Evaluation ($\evals{t}{t’}$)

$\succ t$

$\begin{prooftree}\AXC{(t_1\eval t_1’)}\RLS{ESucc}\UIC{(\evals{\succ t_1}{\succ t_1’})}\end{prooftree}$

$\pred t$

$\begin{prooftree}\AXC{}\RLS{EPredZero}\UIC{(\evals{\pred 0}{0})}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{EPredSucc}\UIC{(\evals{\pred(\succ nv_1)}{nv_1})}\end{prooftree}$

$\begin{prooftree}\AXC{(t_1\eval t_1’)}\RLS{EPred}\UIC{(\evals{\pred t_1}{\pred t_1’})}\end{prooftree}$

$\iszero t$

$\begin{prooftree}\AXC{}\RLS{EIsZeroZero}\UIC{(\evals{\iszero 0}{\tru})}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{EIsZeroSucc}\UIC{(\evals{\iszero \succ nv}{\fls})}\end{prooftree}$

$\begin{prooftree}\AXC{(t_1\eval t_1’)}\RLS{EIsZero}\UIC{(\evals{\iszero t_1}{\iszero t_1’})}\end{prooftree}$

$\ifte{t}{t}{t}$

$\begin{prooftree}\AXC{}\RLS{EIfTrue}\UIC{(\ifte{\tru}{t_2}{t_3} \eval t_2)}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{EIfFalse}\UIC{(\ifte{\fls}{t_2}{t_3} \eval t_3)}\end{prooftree}$

$\begin{prooftree}\AXC{(t_1\eval t_1’)}\RLS{EIf}\UIC{(\ifte{t_1}{t_2}{t_3}\eval\ifte{t_1’}{t_2}{t_3})}\end{prooftree}$

What happens if we add this rule to our evaluation relation:

$\begin{prooftree}\AXC{(t_2\rightarrow t_2’)}\UIC{(\ifte{t_1}{t_2}{t_3}\rightarrow \ifte{t_1}{t_2’}{t_3})}\end{prooftree}$

Do we lose any of our nice properties?

What about this one:

$\begin{prooftree}\AXC{}\UIC{(\ifte{\tru}{t_2}{t_3}\rightarrow t_3)}\end{prooftree}$

Any properties go away?

Untyped Lambda Calculus

You are already doing lambda calculus in a kind of informal way

(define fact
  (lambda (x)
    (if (= x 0) 1 (* x (fact (- x 1))))))
fact x = if x==0 then 1 else x*(fact x-1)
== fact = \x -> if x==0 then 1 else x*(fact x-1)

The concept of a lambda comes directly from lambda calculus.

There are three forms in Lambda Calculus to think about:

Formally:

Syntax $t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$

An abstraction is a parameter defined in the scope of a term:

$\lambda x . t$

defines a variable $x$ over a term $t$ where $t$ is the scope of $x$ and $x$ may be used in $t$.

What do these things do?

  1. Binding Instance is where a variable is declared
  2. Bound Instance is a variable used in its scope
  3. Free Instance is a variable used outside its scope

$\lambda x.\lambda y. x\ z$

  1. A combinator is a lambda with no free variables
  2. A redux is a lambda expression that can be reduced

Pure Beta Reduction

Syntax

$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$

Evaluation

$\begin{prooftree}\AXC{}\RLS{Beta}\UIC{((\lambda x.t_{12}\ t_2)\rightarrow [x\mapsto t_2]t_{12})}\end{prooftree}$

where $[x\mapsto t_2]t_{12}$ is “replace free instances of $x$ with $t_2$ in $t_{12}$.” The canonical substitution operator.

Example $(\lambda w . w\ \lambda x.x)((\lambda y.y)(\lambda z. z))$

Outer $\lambda$ Inner $\lambda$
$(\lambda w . w\ \lambda x.x)((\lambda y.y)(\lambda z. z))$ $(\lambda w . w\ \lambda x.x)((\lambda y.y)(\lambda z. z))$
$\rightarrow(\lambda x.x)((\lambda y.y)(\lambda z. z))$ $\rightarrow(\lambda w . w\ \lambda x.x)(\lambda z. z)$
$\rightarrow((\lambda y.y)(\lambda z. z))$ $\rightarrow(\lambda x.x)(\lambda z. z)$
$\rightarrow(\lambda z. z)$ $\rightarrow(\lambda z. z)$

This is pure beta reduction with no restrictions.

Call By Value

Syntax

$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$

Evaluation

$\begin{prooftree}\AXC{(t_1\rightarrow t_1’)}\RLS{LambdaT1}\UIC{(t_1\ t_2\rightarrow t_1’\ t_2)}\end{prooftree}$

$\begin{prooftree}\AXC{(t_2\rightarrow t_2’)}\RLS{LambdaT2}\UIC{(v_1\ t_2\rightarrow v_1\ t_2’)}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{Beta}\UIC{((\lambda x.t_{12}\ v_2)\rightarrow [x\mapsto v_2]t_{12})}\end{prooftree}$

Why is this call-by-value?

Call By Name

Syntax

$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$

Evaluation

$\begin{prooftree}\AXC{(t_1\rightarrow t_1’)}\UIC{(t_1\ t_2\rightarrow t_1’\ t_2)}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{Beta}\UIC{((\lambda x.t_{12}\ v_2)\rightarrow [x\mapsto v_2]t_{12})}\end{prooftree}$

How do we code in this language?

$\lambda x . x\ \lambda y . y$

$\rightarrow [x\mapsto \lambda y . y]x$ $= \lambda y . y$

We will usually combine lambda elimination and substitution:

$\lambda x . x\ \lambda y . y$

$\rightarrow \lambda y . y$

$\lambda x . x\ x\ \lambda y . y$

$\rightarrow (\lambda y . y)(\lambda y . y)$ $\rightarrow\lambda y . y$

$((\lambda x. (\lambda y . x\ y))(\lambda z.z\ z))(\lambda w . w)$

$\rightarrow (\lambda y.(\lambda z. z\ z)\ y)(\lambda w.w)$ $\rightarrow (\lambda z. z\ z)(\lambda w . w)$ $\rightarrow (\lambda w . w)(\lambda w . w)$ $\rightarrow (\lambda w . w)$

This technique is called currying or curried function semantics. It is useful for defining multi-argument functions using single argument beta reduction.

Should have been called Schoenfinkling, but let’s not go there.

Let’s look at this function:

$(\lambda x . x\ x)(\lambda x . x\ x)$

$\rightarrow x\mapsto (\lambda x.x\ x)$ $=(\lambda x . x\ x)(\lambda x . x\ x)$

Church Encodings

Church (and many others) used lambda calculus to represent common programming idioms and structures.

Church Booleans

$\tru = \lambda x. \lambda y. x$ $\fls = \lambda x. \lambda y. y$

These are not derived, but designed to behave the way we want them to.

$\mathsf{and} = \lambda x . \lambda y . x\ y\ x$ $\mathsf{or} = \lambda x . \lambda y . x\ x\ y$ $\mathsf{not} = \lambda x . x\ \fls\ \tru$

Church Pairs

$\mathsf{cons} = \lambda l . \lambda r . \lambda c . c\ l\ r$

$((\mathsf{cons}\ v_l)\ v_r) = \lambda l . \lambda r . \lambda c . c\ l\ r$ $\rightarrow\lambda r.\lambda c. c\ v_l\ r$ $\rightarrow\lambda c. c\ v_l\ v_r$

$\mathsf{left} = \lambda p . p\ \tru$ $\mathsf{right} = \lambda p . p\ \fls$

Church Numbers

0 S(0) S(S(0)) S(S(S(0))) …

Inductive nat :=
| 0 : nat
| S : nat -> nat.

How do we construct such things in lambda calculus?

It’s not hard at all:

$0$ $S\ 0$ $S\ (S \ 0)$ $S (S (S\ 0))$

Just a bunch of apps of $S$ to 0 and other numbers.

Where do S and 0 come from?

Easy enough to fix:

$0 = \lambda S . \lambda Z . Z$ $1 = \lambda S . \lambda Z . S\ Z$ $2 = \lambda S . \lambda Z . S\ (S \ Z)$ $3 = \lambda S.\lambda Z. S (S (S\ Z))$

Just add $\lambda$!

Is it that simple? $S$ and $Z$ have no binding instances. They are defined, but have no values.

That’s exactly what we want. $S$ and $Z$ are constructors in Coq or Haskell and are not evaluated. They are values. By not giving them definitions and allowing them to exist, $S$ and $Z$ are exactly that.

Really? Is $\lambda S.\lambda Z. (S(S\ Z))$ a value?

It certainly is!

What about operations. How do we add and multiply?

We add by counting. If I want to calculate $2+3$, I will start and $3$ and count $2$ more. In the lambda calculus:

The value of $2$ is $S(S\ Z)$ - Two successors of $Z$ Adding $3$ is $S(S(S\ 2))$ - Three successors of 2

$\textsf{plus} = \lambda m . \lambda n . \lambda S . \lambda Z . (m\ S\ (n\ S)\ Z)$

$(\lambda s. \lambda z. (s (s (s\ z))))(\lambda s.\lambda z. (s (s\ z)))$ $\rightarrow\lambda s.\lambda z. ((\lambda z. (s (s\ z))))((((s ( s (s\ z))))s)s)$ $\rightarrow\lambda s.\lambda z. ((\lambda z. (s (s\ z)))(((s ( s (s\ z))))$ $\rightarrow\lambda s.\lambda z. (s(s(s(s(s\ z)))))$

Here the constructors are instantiated. Specifically

$\textsf{times} = \lambda m . \lambda n . \lambda s . \lambda z . m\ (n\ s\ z)\ z$

let

We cheated a bit earlier when we did this:

$\tru = (\lambda a.\lambda b. a)$

The $=$ does not exist as a term in $\lambda$-calculus. Are we stuck writing things out by hand?

Remember that let is defined in terms of $\lambda$. We can use this form to define a prelude:

$(\lambda cons.\lambda left.\lambda right.\lambda l . \mathsf{body}) (\lambda r . \lambda c . c\ l\ r)(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)$

Example using cons and left:

$(\lambda cons.\lambda left.\lambda right.\lambda l . \mathsf{(left(cons\ left\ left))}) (\lambda r . \lambda c . c\ l\ r)(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)$

We can make this pretty by not printing the outer $\lambda$s that define a prelude.

Why not just add the = ?

Denotation

Among the most common uses of $\lambda$-calculus is denotational semantics where we denote language constructss to $\lambda$ constructs:

$[![\textsf{true}]!]=\lambda a.\lambda b.a$ $[![\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3]!]=(([![t_1]!]\ [![t_2]!])\ [![t_3]!])$ $[![\textsf{a+b}]!]=\lambda S . \lambda Z . ([![\textsf{a}]!]\ S\ ([![\textsf{b}]!]\ S)\ Z)$

Recursion

$f = \lambda x. if\ x=0\ then\ 1\ else\ x*(f (x-1))$

No. Remember, no equals

$\lambda f.\lambda x. if\ x=0\ then\ 1\ else\ x*(f (x-1))$

$f$ is a problem. First where it is defined and second what it is defined as.

The $\Omega$-combinator had no problem with this. Why?

   
$(\lambda x . x\ x)(\lambda x . x\ x)$ Where is the recursion?
$\rightarrow x\mapsto (\lambda x.x\ x)$ Why does the computation diverge?
$=(\lambda x . x\ x)(\lambda x . x\ x)$  

$\Omega$ is not a function. It is an application. Thus, it is not the $\Omega$-function, but the $\Omega$-combinator.

The argument to $\lambda x.x\ x$ is the function it will call and the argument it is called on. The call is always made. Maybe we can not make it.

Whither the lazy Y:

$\lambda f.(\lambda x.(f(x\ x)))(\lambda x.(f(x\ x)))$

We’ve seen this part before and it diverges:

$(\lambda x.(…(x\ x)))(\lambda x.(…(x\ x)))$

Introducing $f$ gives us a way of: (i) doing work; and (ii) exiting.

$(\lambda f.\ …(f\ …)…(f\ …))$

We can instantiate $f$ from the outside and get:

$(\lambda f.\ …(f\ …)…(f\ …))F$ $\rightarrow f\mapsto F](f\ …)$ = $(F\ …)(F\ …)$

Same $F$. Both places and it appears before $(x\ x)$ where magic happens. If $F$ is some kind of conditional, it can turn the recursion off. See factorial above.

Now the worker…

$f$ consumes the $(x\ x)$ result. If it returns a value, $f$ can calculate with it. | | | |—|—| |$(\lambda f.(\lambda x.(f(x\ x)))(\lambda x.(f(x\ x)))F)$| | | $\rightarrow f\mapsto F(\lambda x.(f(x\ x))$ | Push the worker function into the combinator | | $= (\lambda x.(F(x\ x)))(\lambda x.(F(x\ x)))$| Y-Combinator with our custom work function | |$\rightarrow [x\mapsto (\lambda x.(F(x\ x)))](\lambda x.(F(x\ x))$| Apply the $\Omega$ trick passing in recursive call | |$= (F(\lambda x.(F(x\ x)))(\lambda x.(F(x\ x))))$| Now $F$ is applied to the recursive call | | … | The argument to $F$ is the combinator we started with | |$= (F(F(\lambda x.(F(x\ x)))(\lambda x.(F(x\ x)))))$| Now $F$ is applied to the recursive call | | … | The argument to $F$ is the combinator we started with | |$= (F(F(F(\lambda x.(F(x\ x)))(\lambda x.(F(x\ x))))))$| Now $F$ is applied to the recursive call | | … | The argument to $F$ is the combinator we started with |

We just need to define and $F$ that does our work for us and turns off when it supposed to.

$F= \lambda x. if\ x=0\ then\ 1\ else\ x*(f (x-1))$

This is fine of course, but $f$ is still undefined just like it was before. We need to feed the function through.

What about this:

$F= \lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z*(g (z-1))$ $Y=(\lambda f.(\lambda x. (f\ (x\ x)))(\lambda x.(f\ (x\ x))))$

What is this?

$((Y\ F)\ 3)$

Let’s find out by evaluating the term using call-by-name evaluation semantics.

$((Y\ F)\ 3) = ((\lambda f. (\lambda x. (f\ (x\ x)))(\lambda x.(f\ (x\ x)))) F) 3)$ $\rightarrow (\lambda x. (F(x\ x)))(\lambda x.(F (x\ x))) 3$ $= (\lambda x. (\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(x\ x)))$ $\ \ \ \ (\lambda x.(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1)) (x\ x))) 3$ $=(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(\lambda x.F(x\ x)\ \lambda x.F(x\ x)))) 3$ $=(\lambda z. if\ z=0\ then\ 1\ else\ z((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (z-1))) 3$ $=if\ 3=0\ then\ 1\ else\ 3((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (3-1)))$ $=3(\lambda x.(F(x\ x))\ \lambda x.(F(x\ x)))\ 2$

$= 3(\lambda x. (\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(x\ x)))$ $\ \ \ \ (\lambda x.(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1)) (x\ x))) 2$ $=3(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(\lambda x.F(x\ x)\ \lambda x.F(x\ x)))) 2$ $=3(\lambda z. if\ z=0\ then\ 1\ else\ z((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (z-1))) 2$ $=3if\ 2=0\ then\ 1\ else\ 2((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (2-1)))$ $=32*(\lambda x.(F(x\ x))\ \lambda x.(F(x\ x)))\ 1$

$= 32(\lambda x. (\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(x\ x)))$ $\ \ \ \ (\lambda x.(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1)) (x\ x))) 1$ $=32(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(\lambda x.F(x\ x)\ \lambda x.F(x\ x)))) 1$ $=32(\lambda z. if\ z=0\ then\ 1\ else\ z((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (z-1))) 1$ $=32if\ 1=0\ then\ 1\ else\ 1((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (1-1)))$ $=321(\lambda x.(F(x\ x))\ \lambda x.(F(x\ x)))\ 0$

$= 321(\lambda x. (\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(x\ x)))$ $\ \ \ \ (\lambda x.(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1)) (x\ x))) 0$ $=321(\lambda g.\lambda z. if\ z=0\ then\ 1\ else\ z(g (z-1))(\lambda x.F(x\ x)\ \lambda x.F(x\ x)))) 0$ $=321(\lambda z. if\ 0=0\ then\ 1\ else\ 0((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (0-1)))$ $=321if\ 0=0\ then\ 1\ else\ 3((\lambda x.F(x\ x)\ \lambda x.F(x\ x))) (2-1)))$ $=3211$ $= 6$

Wow. Pretty cool. We can now write recursive functions using $Y$ in a systematic way:

  1. Start with the definition $F=\lambda x.\ \ldots$ where $F$ names the recursive function.
  2. Add a function variable to the front $\lambda F.\lambda x.\ \ldots$ and drop the $F=\ldots$
  3. Call The new $F$ with $Y$ on some input term $(Y\ F)\ t$

There you have it. Build the $Y$ once and don’t think about it again.

$\rightarrow$ (untyped)

And here we have the untyped, call-by-value $\lambda$-calculus:

Syntax

$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$

Evaluation

$\begin{prooftree}\AXC{(t_1\rightarrow t_1’)}\RLS{LambdaT1}\UIC{(t_1\ t_2\rightarrow t_1’\ t_2)}\end{prooftree}$

$\begin{prooftree}\AXC{(t_2\rightarrow t_2’)}\RLS{LambdaT2}\UIC{(v_1\ t_2\rightarrow v_1\ t_2’)}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{Beta}\UIC{((\lambda x.t_{12}\ v_2)\rightarrow [x\mapsto v_2]t_{12})}\end{prooftree}$

This is our first language building block.

Typed Arithmetic Expressions

We saw earlier that if we evaluate expressions in our arithmetic language:

Syntax t ::= $\tru$ | $\fls$ | $\ifte{t}{t}{t}$ | $\succ t$ | $\pred t$ | $\iszero t$

We will either get a value:

$v$ ::= $\tru$ $\fls$ $nv$
$nv$ ::= 0 $\succ nv$  

or we get stuck. We proved this. What did we prove again?

We “fixed” stuckness by defining a standard value that we can return like the $\textsf{Maybe}$ type.

What we would really like to know if we will get stuck before we execute code.

Our tool will be static typing

What do these things mean?

int x;
f::nat -> nat
A:Type.

Each notation states that a structure in a language is constrained to be “of a type” or “in a type”.  We will use a classical notation for types:

$t:T$ - Term $t$ is of type $T$.

where “:” is a relation between language terms and types called the typing relation.

We could just as easily say:

$t\in T$

but sets are not our only option for modeling types. (See the sorts literature.)

Typing Relation

Lets define a typing relation from syntax to type. Syntax is easy:

Syntax $t$ ::= $\tru$ | $\fls$ | $\ifte{t}{t}{t}$ | $\succ t$ | $\pred t$ | $\iszero t$ $v$ ::= $\tru$ | $\fls$ | $nv$ $nv$ ::= 0 | $\succ nv$

What are the set of types?

$T$ ::= $Bool$ $Nat$

This is syntax. Types are in our language, but are they true terms?

Let’s define a typing relation. When all you have is a hammer…

Constant Types

Constants have types like they have values. There is no work to do. $\begin{prooftree}\AXC{}\UIC{(0:Nat)}\end{prooftree}$ $\begin{prooftree}\AXC{}\UIC{(\tru:Bool)}\end{prooftree}$ $\begin{prooftree}\AXC{}\UIC{(\fls:Bool)}\end{prooftree}$

Unary Operations

What is the type of successor? $\begin{prooftree}\AXC{}\UIC{(\succ t:??)}\end{prooftree}$

We know that $t$ is a $Nat$ or a $Bool$. There are no other options.

$\begin{prooftree}\AXC{(t:Nat)}\UIC{(\succ t:Nat)}\end{prooftree}$

$\begin{prooftree}\AXC{(t:Bool)}\UIC{(\succ t:???)}\end{prooftree}$

if $t : Bool$ we know that $t$ is $\tru$ or $\fls$ and $\succ t$ makes no sense.

We know this without evaluating succ t. That is key. We are detecting stuckness before runtime. Better yet, we are proving that $\succ t$ will or will not get stuck.

Our type rules now consist of:

Type Rules (t:T) $\begin{prooftree}\AXC{}\RLS{TZero}\UIC{(0:Nat)}\end{prooftree}$ $\begin{prooftree}\AXC{}\RLS{TTrue}\UIC{(\tru:Bool)}\end{prooftree}$ $\begin{prooftree}\AXC{}\RLS{TFalse}\UIC{(\fls:Bool)}\end{prooftree}$

$\begin{prooftree}\AXC{(t:Nat)}\RLS{TSucc}\UIC{(\succ t:Nat)}\end{prooftree}$

The typing relation like the evaluation relation is the smallest relation that satisfies typing rules.

$\begin{prooftree}\AXC{(t:Nat)}\RLS{TPred}\UIC{(\pred t:Nat)}\end{prooftree}$

$\begin{prooftree}\AXC{(t:Nat)}\RLS{TIsZero}\UIC{(\iszero t:Bool)}\end{prooftree}$

if

One more to go $\ifte{t}{t}{t}$

$\begin{prooftree}\AXC{}\AXC{}\AXC{}\TIC{(\ifte{t_1}{t_2}{t_3}:T)}\end{prooftree}$

Do we know what type the if should be? Everything else has a type that we know based on the term. Does $\mathsf{if}$ work the same way?

$\begin{prooftree}\AXC{(t_1:Bool)}\AXC{}\AXC{}\TIC{(\ifte{t_1}{t_2}{t_3}:T)}\end{prooftree}$

The condition should be $Bool$ for sure. What about $t_1$ and $t_2$?

$\begin{prooftree}\AXC{(t_1:Bool)}\AXC{(t_2:T_2)}\AXC{(t_3:T_3)}\TIC{(\ifte{t_1}{t_2}{t_3}:T)}\end{prooftree}$

What is $T$ given $t_2:T_2$ and $t_3:T_3$?

If $t_1=\tru$ then $T_2$ else $T_3$. Just like evaluation. Right?

What do we do with this? What type is it?

$\ifte{x=3}{5}{\fls}$

If it can be both types the expressing it is embedded to must consume both types. That can’t happen. So we make a conservative approximation:

$\begin{prooftree}\AXC{(t_1:Bool)}\AXC{(t_2:T)}\AXC{(t_3:T)}\RLS{TIf}\TIC{(\ifte{t_1}{t_2}{t_3}:T)}\end{prooftree}$

How does this work?

Properties of Typing Relations

Well-Typed

If $t:T$ for some type $T$ then $t$ is well typed.

Type Inversion

Type Inversion Lemma

Immediate from the definition of the typing relation. Really? How is that?

Well-typed Sub-terms

Every sub-term of a well-type term is well-typed. How do we go about this?

Type Uniqueness

Type Uniqueness - Every term $t$ has at most 1 type. How do we prove this? Have we seen it before somewhere?

Progress + Preservation = Safety

Type Safety means that a program cannot go wrong. Literally.

Progress and Preservation Two define type safety (sometimes called soundness):

Progress

A well-typed term is either a value or it can be evaluated

$\exists t’ . t\rightarrow t’$ or $t$ is a value

Preservation

If a well-typed term can be evaluated, its type is invariant

$t:T\rightarrow t’:T$

How do we prove safety?

Preservation is often called the subject-reduction theorem. The intuition is we are reducing the subject of the term.

Canonical Forms Lemma

  1. if $v:Bool$ then $v=\tru$ or $v=\fls$
  2. if $v:Nat$ then then $v\in nv$ from our grammar definition

    Proof

  3. $\tru:Bool$ and $\fls : Bool$ are both consistent with the typing relation. $nv:Bool$ is violates the type inversion lemma.
  4. $nv:Nat$ is consistent with the typing relation. $\tru : Nat$ and $\fls : Nat$ violate the type inversion lemma $\square$

Some things to remember:

  1. We have proven that values are normal forms and normal forms are values
  2. The induction hypothesis is your friend
  3. Not all induction is over terms

Proof of Progress

A well-typed term is not stuck. Well-typed term is $t:T$. Not stuck is: (i) $t$ is a value; or (ii) $t\rightarrow t’$

If $t:T$ there must be a derivation of $t:T$ that uses our type inference rules. That type inference must end implying there is a “last” rule. Let’s look at those last rules:

$0:Nat$, $\tru : Bool$, $\fls : Bool$ - if any of these rules is last we have a value and we’re done.

$\begin{prooftree}\AXC{(t:Nat)}\RLS{TSucc}\UIC{(\succ t:Nat)}\end{prooftree}$ $t$ is a value or it is not a value. Canonical forms says that if $t$ is a value then $t\in nv$. If that is true, then $\succ t\in nv$ and $\succ t$ is a value. If $t$ is not a value then there is some rule such that $t\rightarrow t’$ and the $\mathsf{ESucc}$ rule applies allowing evaluation to take a step.

The $\pred t$ and $\iszero t$ cases are identical.

$\begin{prooftree}\AXC{(t_1:Bool)}\AXC{(t_2:T)}\AXC{(t_3:T)}\RLS{TIf}\TIC{(\ifte{t_1}{t_2}{t_3}:T)}\end{prooftree}$ $t_1$ is a value or is not a value. Canonical forms says if $t_1$ is a value then $t_1\in {\tru,\fls}$. In these cases either $\mathsf{EIfTrue}$ or $\mathsf{EIfFalse}$ applies and the expression takes a step. If $t_1$ is not a value then $t_1\rightarrow t_1’$ and $\textsf{EIf}$ applies.

Proof of Preservation

If a well-typed term can be evaluated then the result is well-typed:

$t:T\rightarrow t’$

and the result should be well-typed:

$t:T\rightarrow t’:T$

$0:Nat$, $\tru:Bool$, $\fls:Bool$ - these cases cannot be evaluated and thus the conjecture is vacuously true

$\begin{prooftree}\AXC{(t:Nat)}\RLS{TSucc}\UIC{(\succ t:Nat)}\end{prooftree}$- $t$ is either a value or is not a value. Canonical forms says that if $t$ is a value then $t\in nv$. If that is true, then $\succ t\in nv$ and $\succ t$ is also a value making the theorem vacuously true. If $t$ is not a value then there is some rule such that $t\rightarrow t’$. The induction hypothesis tells us that $t:Nat\rightarrow t’:Nat$. Applying $\mathsf{TSucc}$ to $t’$ gives us $\succ t’:Nat$.

$\begin{prooftree}\AXC{(t_1:Bool)}\AXC{(t_2:T)}\AXC{(t_3:T)}\RLS{TIf}\TIC{(\ifte{t_1}{t_2}{t_3}:T)}\end{prooftree}$ - $t_1$ is either a value or is not a value. Canonical forms says that if $t_1$ is a value, then $t_1=\tru$ or $t_1 = \fls$. If that is true, then either $\mathsf{EIfTrue}$ or $\mathsf{EIfFalse}$ apply. In the first case evaluation results in $t_2:T$ and in the second $t_3:T$. Buy the induction hypothesis $t_2$ and $t_3$ are well-typed. If $t_1$ is not a value then some $t_1\rightarrow t_1’$ and $\ifte{t_1}{t_2}{t_3}\rightarrow\ifte{t_1’}{t_2}{t_3}$ By the induction hypothesis, preservation holds for $t_1$ and $t_1’:T$. By $\mathsf{TIf}$ we know $\ifte{t_1’}{t_2}{t_3}:T$ and preservation holds.

Eventual Homework Questions

  1. The evaluation rule $\mathsf{EPredZero}$ (Figure 3-2) is a bit counterintuitive: we might feel that it makes more sense for the predecessor of zero to be undefined, rather than being defined to be zero. Can we achieve this simply by removing the rule from the definition of single-step evaluation?
  2. Having seen the subject reduction property, it is reasonable to wonder whether the opposite property—subject expansion—also holds. Is it always the case that, if $t\rightarrow t’$ and $t’:T$ then $t:T$ ? If so, prove it. If not, give a counterexample.
  3. Suppose our evaluation relation is augmented with rules for reducing nonsensical terms to an explicit wrong state, as in Exercise 3.5.16. Now how should type safety be formalized?

Simply-Typed Lambda Calculus

Let’s add types to the untyped lambda calculus. We’ll define types and a typing relation, then prove the cool properties that we looked at for arithmetic expressions.  That’s the plan at least…

Recall the Untyped Lambda Calculus:

Syntax

$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$

Evaluation

$\begin{prooftree}\AXC{(t_1\rightarrow t_1’)}\RLS{LambdaT1}\UIC{(t_1\ t_2\rightarrow t_1’\ t_2)}\end{prooftree}$

$\begin{prooftree}\AXC{(t_2\rightarrow t_2’)}\RLS{LambdaT2}\UIC{(v_1\ t_2\rightarrow v_1\ t_2’)}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{Beta}\UIC{((\lambda x.t_{12}\ v_2)\rightarrow [x\mapsto v_2]t_{12})}\end{prooftree}$

What needs to have a type?

Let’s start where Pierce starts with this:

$\lambda x . t : \rightarrow$

We’ve defined a new type called $\rightarrow$ and said that all lambdas are of that type.

$T::=\rightarrow$

Good or bad?

$(\lambda x . x\ x):T$ $(\lambda x . x) : T$ $(\lambda x . x . \lambda y . x\ y):T$

What are the values of $T$?

If these are well typed terms then $T$ must be $\rightarrow$

Do we get any goodness from this? Can we predict anything useful.

In a word, no.

Let’s add some precision to our lambda type by talking about what goes in and what comes out:

$T::= T\rightarrow T$

We will call the left and right types the domain and range of the of the type. The $\rightarrow$ is a type constructor as it creates new types from old types. $\rightarrow$ is right-associative.

$T_1\rightarrow T_2\rightarrow T_3 = T_1\rightarrow (T_2\rightarrow T_3)$

This is the opposite of functions and operations.

Now what is the type of $\lambda x.x$?

$\lambda x.x:T\rightarrow T$

That seems to work. This function will return the same type thing in accepts. An now a type rule:

$\begin{prooftree}\AXC{}\UIC{(\lambda x.x:T\rightarrow T)}\end{prooftree}$

Now this:

$\lambda x.x\ x :T\rightarrow T$

This seems to have problems. $x$ has to be a lambda, but the result of applying $x$ to $x$ is not necessarily the same type as $x$. We’re stuck.

Base Types

Let’s write a type. Not a type meta-variable like $T$, but an actual type. Our only type definition so far is:

$T::=T\rightarrow T$

Notice anything?

There are no concrete types. The only thing we can instantiate $T$ with is $T\rightarrow T$.

A base type is a concrete type or a base type. In earlier languages, $Nat$ and $Bool$ are both base types. They do not take arguments.

Base types allow things like $Bool\rightarrow Bool$ which is the type of a function from boolean values to boolean values.

Let’s add $Bool$ to our type system:

$T ::= T \rightarrow T \mid Bool$

Now I can write this:

$(\lambda x:Bool. x):Bool\rightarrow Bool$

We can also write this:

$(((\lambda x: Bool.x):Bool\rightarrow Bool)\ \tru):Bool$

Maybe a type rule for app?

$\begin{prooftree}\AXC{(z:T)}\AXC{(\lambda x:T.t:T\rightarrow R)}\BIC{(((\lambda x.T.t)\ z):R)}\end{prooftree}$

Hmm. Let’s not get ahead of ourselves, but this seems to be something worth thinking about…

Type Ascription

What is the type of $\lambda x . x$? We need the type of $x$ to determine range type which is the type of $x$.

What is the type of this? What is the type of $x$? It’s domain should be $Bool$, but what else?

$\lambda x. (x\ \tru)$

In general, we cannot figure out a $\lambda$’s input type from its output type. Function application “removes” information.

The solution is type ascription where we give a type to a lambda’s parameter and infer the type of evaluation. Provide a domain type and infer a range type.

$\lambda x:Bool.x:D\rightarrow R$

We know the domain type:

$\lambda x:Bool.x:Bool \rightarrow R$

Given the range type, we can infer the function’s body type:

$x:Bool\vdash x:Bool$

Which is $R$ and the function type is:

$\lambda x:Bool.x:Bool \rightarrow Bool$

How about this one:

$((\lambda x:Bool. x)\ \tru):Bool$

Type type of the lambda is $Bool\rightarrow Bool$ which can be interpreted as “if you give me a $Bool$ I will give you back a $Bool$”

How about these:

Type Rules

The rule for application is not too hard to think through:

$\begin{prooftree}\AXC{(t_1:T_1\rightarrow T_2)}\AXC{(t_2:T_1)}\RLS{TApp}\BIC{((t_1\ t_2):T_2)}\end{prooftree}$

The rule for lambda is a little trickier. How did we learn the the type of $(\lambda x:Bool.x)$ to be $Bool\rightarrow Bool$ ?

Because we know the type of $x$ we can infer the type of the function’s return value:

$x:T\vdash x:T$

A more interesting example:

$\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y)$

$x:Bool\rightarrow Bool$, $y:Bool$ $\vdash$ $\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y) : Bool$

By gathering up all the types of variables in scope, we can determine the type of any term. The only way we have of creating variables and scopes is $\lambda$.

Definition The context of a term ($\Gamma$) is a list of all bound variables and their types.

The context of the innermost term above is:

$\Gamma=[(x\mapsto Bool\rightarrow Bool),(y\mapsto Bool)]$

The choice of a list is not just for convenience. We will take advantage of this structure later.

We can now define a type rule for variables:

$\begin{prooftree}\AXC{((x\mapsto T)\in\Gamma)}\RLS{TVar}\UIC{(\Gamma\vdash x:T)}\end{prooftree}$

Note that $(x\mapsto T)\in\Gamma$ finds the first binding of $x$.

This is read “gamma derives $x$ of type $T$”

The notation $(x\mapsto T),\Gamma$ adds a new outermost binding to $\Gamma$. (The operator is the comma.)

Now we can write the type rule for $\lambda$:

$\begin{prooftree}\AXC{(((x\mapsto T_1),\Gamma\vdash t_2:T_2)}\RLS{TLambda}\UIC{(\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2)}\end{prooftree}$

[\begin{prooftree}\AXC{}\UIC{(\emptyset\vdash\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y):(Bool\rightarrow Bool)\rightarrow (Bool\rightarrow Bool))}\end{prooftree}]

[\begin{prooftree}\AXC{([x,\mapsto (Bool\rightarrow Bool)]\vdash\lambda y:Bool.(x\ y):Bool\rightarrow Bool)}\UIC{(\emptyset\vdash\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y):(Bool\rightarrow Bool)\rightarrow (Bool\rightarrow Bool))}\end{prooftree}]

\(\begin{prooftree}\AXC{\([y\mapsto Bool,x\mapsto (Bool\rightarrow Bool)]\vdash(x\ y):Bool\)}\UIC{\([x,\mapsto (Bool\rightarrow Bool)]\vdash\lambda y:Bool.(x\ y):Bool\rightarrow Bool\)}\UIC{\(\emptyset\vdash\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y):(Bool\rightarrow Bool)\rightarrow (Bool\rightarrow Bool)\)}\end{prooftree}\) \(\begin{prooftree}\AXC{\(\Gamma\vdash x:Bool\rightarrow Bool\)}\AXC{\(\Gamma\vdash y:Bool\)}\BIC{\([y\mapsto Bool,x\mapsto (Bool\rightarrow Bool)]\vdash(x\ y):Bool\)}\UIC{\([x,\mapsto (Bool\rightarrow Bool)]\vdash\lambda y:Bool.(x\ y):Bool\rightarrow Bool\)}\UIC{\(\emptyset\vdash\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y):(Bool\rightarrow Bool)\rightarrow (Bool\rightarrow Bool)\)}\end{prooftree}\) \(\begin{prooftree} \AXC{\(x\mapsto Bool\rightarrow Bool\in \Gamma\)} \UIC{\(\Gamma\vdash x:Bool\rightarrow Bool\)} \AXC{\(y\mapsto Bool\in \Gamma\)} \UIC{\(\Gamma\vdash y:Bool\)} \BIC{\([y\mapsto Bool,x\mapsto (Bool\rightarrow Bool)]\vdash(x\ y):Bool\)} \UIC{\([x,\mapsto (Bool\rightarrow Bool)]\vdash\lambda y:Bool.(x\ y):Bool\rightarrow Bool\)} \UIC{\(\emptyset\vdash\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y):(Bool\rightarrow Bool)\rightarrow (Bool\rightarrow Bool)\)}\end{prooftree}\)

And there we have it. A proof that $\lambda x:Bool\rightarrow Bool.\lambda y:Bool.(x\ y)$ is well-typed.

$\rightarrow$ (T)

And here we have the simply-typed, call-by-value $\lambda$-calculus:

Syntax

$t$ ::= $\lambda x:T.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x:T . t$ $T$ ::= $T\rightarrow T$ $\Gamma$ ::= $\emptyset\mid (x\mapsto T),\Gamma$

Evaluation (CBV)

$\begin{prooftree}\AXC{(t_1\rightarrow t_1’)}\RLS{LambdaT1}\UIC{(t_1\ t_2\rightarrow t_1’\ t_2)}\end{prooftree}$

$\begin{prooftree}\AXC{(t_2\rightarrow t_2’)}\RLS{LambdaT2}\UIC{(v_1\ t_2\rightarrow v_1\ t_2’)}\end{prooftree}$

$\begin{prooftree}\AXC{}\RLS{Beta}\UIC{((\lambda x:T_{11}.t_{12}\ v_2)\rightarrow [x\mapsto v_2]t_{12})}\end{prooftree}$

Typing

$\begin{prooftree}\AXC{((x\mapsto T)\in\Gamma)}\RLS{TVar}\UIC{(\Gamma\vdash x:T)}\end{prooftree}$

$\begin{prooftree}\AXC{(((x\mapsto T_1),\Gamma\vdash t_t:T)}\RLS{TLambda}\UIC{(\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2)}\end{prooftree}$

$\begin{prooftree}\AXC{(t_1:T_1\rightarrow T_2)}\AXC{(t_2:T_1)}\RLS{TApp}\BIC{((t_1\ t_2):T_2)}\end{prooftree}$

Adding $Bool$ or $Nat$ would enrich the calculus to include base types and actually allow us to write programs.

Properties

Type Inversion Lemma

Immediate from the definition of the typing relation. $\square$

Uniqueness of Types

What is the proof for this? Pierce says it is “so direct there is almost nothing to say”

Canonical Forms

Pierce says this proof is “straightforward”

Progress

if $\typing{t}{T}$ then $t$ is a value or $t\rightarrow t’$ for some $t’$

What is the proof here

Preservation

This one is more work. We’re going to need some lemmas.

Permutation

If $\typing{t}{T}$ and $\Delta$ is a permutation of $\Gamma$, then $\typing[\Delta]{t}{T}$

Typing is invariant with respect to the ordering of variable bindings in the context.

Is this true in general?

the proof

Induction over type rules:

Weakening

If $\typing{t}{T}$ and $x\notin dom(\Gamma)$ then $\typing[(x\mapsto S),\Gamma]{t}{T}$

Typing is invariant with respect to the addition of unique variables to the context

The Proof

Induction over type rules (again)

Preservation of Types Under Substitution

If $\typing[(x\mapsto S),\Gamma]{t}{T}$ and $\typing{s}{S}$ then $\typing{[x\mapsto s]t}{T}$

Typing is invariant with respect to replacing a well-typed variable with a well-typed term of the same type.

The Proof

Induction over type rules

Preservation

Now we put the bits together for preservation over $\rightarrow T$

The Proof

What we know about simply-typed lambda calculus:

  1. Type preservation
  2. Progress
  3. Termination

Proof Tools

Are we seeing a pattern here?

  1. Induction over type derivations (looking at each type rule)
  2. Canonical forms (type tells us values)
  3. Type inversion (whole implies the parts)
  4. Unique types (only one type per term)
  5. Induction hypothesis (parts imply the whole)
         
    Evaluation + Induction Hyp    
  $t_1:T_1, t_2:T_2,\ldots$ $\longrightarrow$ $t_1’:T_1, t_2’:T_2,\ldots$  
Type Inversion $\uparrow$   $\downarrow$ Type Rule
  $t:T$ $\longrightarrow$ $t’:T$  
    Evaluation    

Type Erasure

The erasure of a simply typed term $t$ is defined as:

$erase\ x = x$ $erase\ \lambda x:T_1.t_2 = \lambda x.erase\ t_2$ $erase\ (t_1\ t_2)=(erase\ t_1\ erase t_2)$

Provable by induction on evaluation derivations.

Church vs Curry Style Semantics

Curry Howard

Types are theorems and values are proofs

The type constructor $T\rightarrow T$ has introduction and elimination rules just like other logical constructions.

Look what’s happening to the types not the values.

Propositions Types
$P\Rightarrow Q$ $P\rightarrow Q$
$P\wedge Q$ $P\times Q$
Proof of $P$ $t:P$
$P$ is provable Type $P$ is inhabited

If $P\rightarrow Q$ is a theorem, what theorem is it?

Why is $f:P\rightarrow Q$ a proof of a theorem

$P\vee Q$ is not in the list. What is $r:P\vee Q$ and why is it a proof?As promised, here are links to the markdown and style files from Obsidian that I use for class notes.

[\Delta]


Notes Issues

I promised to have my notes posted online. Unfortunately, the Obsidian export tool chokes generating some of my equations. That’s the most important thing to export. I will continue working to find a solution. Sorry!


Welcome

Welcome to the EECS 762 blog. I will post information about projects, homework and lectures here. Please check here often when homework and projects are due as I will post late-breaking information including hints and corrections.