src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
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.
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\]