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.
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.
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.
[\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}}}]
Things are getting too complex and dangerous for ad hoc methods
Our first (very broken) language of untyped arithmetic expressions
Each of these definitions defines the same set of terms:
\(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
\(\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?
\(\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
\(\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}\)
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}\)
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
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
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?
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] |
Case true : $$ |
\mathsf{consts}\ \tru | \leq \mathsf{terms}\ \tru$$ |
Case false : $$ |
\mathsf{consts}\ \fls | \leq \mathsf{terms}\ \tru$$ |
Case succ : $$\forall t \cdot |
\mathsf{consts}\ t | \leq\mathsf{terms}\ t\Rightarrow | \mathsf{consts}\ \succ t | \leq\mathsf{terms}\ \succ t$$ |
Case pred : $$\forall t . |
\mathsf{consts}\ t | \leq\mathsf{terms}\ t\Rightarrow | \mathsf{consts}\ \pred t | \leq\mathsf{terms}\ \pred t$$ |
Case isTrue : $$\forall t \cdot |
\mathsf{consts}\ t | \leq\mathsf{terms}\ t\Rightarrow | \mathsf{consts}\ \iszero t | \leq\mathsf{terms}\ \iszero t$$ |
Case if : $$\forall t_c,t_t,t_e \cdot |
\mathsf{consts}\ t_c | \leq\mathsf{terms}\ t_c\wedge | \mathsf{consts}\ t_c | \leq\mathsf{terms}\ t_c\wedge | \mathsf{consts}\ t_c | \leq\mathsf{terms}\ t_c\Rightarrow | \mathsf{consts}\ \ifte{t_c}{t_t}{t_e} | \leq\mathsf{terms}\ \ifte{t_c}{t_t}{t_e}$$ |
Why these cases?
If for each term \(t\)
If for each term \(t\)
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$$ |
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.
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:
Definitions:
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!
If \(t\eval t'\) and \(t\eval t''\) then \(t'=t''\)
Proof by induction on \(t\)
More Definitions
Proof by cases on t:
Definition The multi-step evaluation relation (\(r\rightarrow^* r'\)) is the reflexive, transitive closure of the single step relation (\(r\rightarrow r'\)):
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}\).
A derivation or proof is a collection of inference rules used in sequence.
\(\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.
[\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.
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:
This is a nifty pattern for both proof and evaluation.
Let’s rebuild our arithmetic language. Carefully this time.
t ::= true | false | 0 | (if t t t) | succ t | pred t | isZero t v ::= true | false | nv nv ::= 0 | succ nv
$\begin{prooftree}\AXC{(t_1\eval t_1’)}\RLS{ESucc}\UIC{(\evals{\succ t_1}{\succ t_1’})}\end{prooftree}$
$\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}$
$\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}$
$\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?
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?
$\lambda x.\lambda y. x\ z$
$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$
$\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.
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.
$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$
$\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?
$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$
$\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?
$\rightarrow [x\mapsto \lambda y . y]x$ $= \lambda y . y$
We will usually combine lambda elimination and substitution:
$\rightarrow \lambda y . y$
$\rightarrow (\lambda y . y)(\lambda y . y)$ $\rightarrow\lambda y . y$
$\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:
$\rightarrow x\mapsto (\lambda x.x\ x)$ $=(\lambda x . x\ x)(\lambda x . x\ x)$
Church (and many others) used lambda calculus to represent common programming idioms and structures.
$\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$
$\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$
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$
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 = ?
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)$
$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:
There you have it. Build the $Y$ once and don’t think about it again.
And here we have the untyped, call-by-value $\lambda$-calculus:
$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$
$\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.
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.)
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…
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}$
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}$
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?
If $t:T$ for some type $T$ then $t$ is well typed.
Type Inversion Lemma
Immediate from the definition of the typing relation. Really? How is that?
Every sub-term of a well-type term is well-typed. How do we go about this?
Type Uniqueness - Every term $t$ has at most 1 type. How do we prove this? Have we seen it before somewhere?
Type Safety means that a program cannot go wrong. Literally.
Progress and Preservation Two define type safety (sometimes called soundness):
A well-typed term is either a value or it can be evaluated
$\exists t’ . t\rightarrow t’$ or $t$ is a value
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.
Some things to remember:
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.
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.
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:
$t$ ::= $\lambda x.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x . t$
$\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.
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…
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:
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.
And here we have the simply-typed, call-by-value $\lambda$-calculus:
$t$ ::= $\lambda x:T.t$ | $(t\ t)$ | $x$ $v$ ::= $\lambda x:T . t$ $T$ ::= $T\rightarrow T$ $\Gamma$ ::= $\emptyset\mid (x\mapsto T),\Gamma$
$\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}$
$\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.
Immediate from the definition of the typing relation. $\square$
What is the proof for this? Pierce says it is “so direct there is almost nothing to say”
Pierce says this proof is “straightforward”
if $\typing{t}{T}$ then $t$ is a value or $t\rightarrow t’$ for some $t’$
This one is more work. We’re going to need some lemmas.
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?
Induction over type rules:
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
Induction over type rules (again)
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.
Induction over type rules
Now we put the bits together for preservation over $\rightarrow T$
What we know about simply-typed lambda calculus:
Are we seeing a pattern here?
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 |
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.
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]
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 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.