# Simply Typed Lambda Calculus

In this chapter, we look at how inductively defined types can be used to represent both raw data, inductively defined relations, and proofs relating the two.

By way of illustration, we develop a case study in the simply typed lambda calculus (STLC), a very simple programming language which is often studied in introductory courses on the semantics of programming languages. Its syntax, type system, and runtime behavior can be described in just a few lines. The main result we’re interested in proving is the soundness of the type system, i.e., that if a program type checks then it can be executed safely without a certain class of runtime errors.

If you haven’t seen the STLC before, there are several good resources for it available on the web, including the Software Foundations book, though we’ll try to keep the presentation here as self-contained as possible. Thanks to Simon Forest, Catalin Hritcu, and Simon Schaffer for contributing parts of this case study.

## Syntax

The syntax of programs \(e\) is defined by the context-free grammar shown below.

This can be read as follows: a program \(e\) is either

the unit value \(()\);

a variable \(x\);

a lambda term \(\lambda x:t. e_0\) associating a variable \(x\) to a type \(t\) and a some sub-program \(e_0\);

or, the application of the sub-program \(e_0\) to another sub-program \(e_1\).

The syntax of the type annotation \(t\) is also very simple:

A type \(t\) is either

the \(\mathsf{unit}\) type constant;

or, arrow type \(t_0 \rightarrow t_1\) formed from two smaller types \(t_0\) and \(t_1\)

This language is very minimalistic, but it can be easily extended with some other forms, e.g., one could add a type of integers, integer constants, and operators like addition and subtraction. We’ll look at that as part of some exercises.

We’ll define the syntax of types and programs formally in F* as a pair
of simple inductive datatypes `typ`

(for types) and `exp`

(for
programs or expressions) with a constructor for each of the cases
above.

The main subtlety is in the representation of variables. For example,
ignoring the type annotations, in the term
\(\lambda x. (\lambda x. x)\) the inner lambda binds *a different*
\(x\) than the outer one, i.e., the term is equivalent to
\(\lambda x. (\lambda y. y)\) and our representation of programs
must respect this this convention. We’ll use a technique called de
Bruijn indices, where the names of the variables are no longer
significant and instead each variable is represented by a natural
number describing the number of \(\lambda\) binders that one must
cross when traversing a term from the occurrence of the variable to
that variable’s \(\lambda\) binder.

For example, the terms \(\lambda x. (\lambda x. x)\) and \(\lambda x. (\lambda y. y)\) are both represented as \(\lambda _. (\lambda _. 0)\), since the inner occurrence of \(x\) is associated with the inner \(\lambda\); while \(\lambda x. (\lambda y. (\lambda z. x))\) is represented as \(\lambda _. (\lambda _. (\lambda _. 2)\), since from the inner occurrence of \(x\) one must skip past \(2\) \(\lambda\)lambda` associated with \(x\). Note, the variable names are no longer significant in de Bruijn’s notation.

### Representing types

The inductive type `typ`

defined below is our representation of
types.

```
type typ =
| TUnit : typ
| TArr : typ -> typ -> typ
```

This is entirely straightforward: a constructor for each case in our type grammar, as described above.

### Representing programs

The representation of program expressions is shown below:

```
let var = nat
type exp =
| EUnit : exp
| EVar : var -> exp
| ELam : typ -> exp -> exp
| EApp : exp -> exp -> exp
```

This too is straightforward: a constructor for each case in our
program grammar, as described above. We use a `nat`

to represent
variables `var`

and `ELam`

represents an annotated lambda term of
the form \(\lambda _:t. e\), where the name of the binder is
omitted, since we’re using de Bruijn’s representation.

## Runtime semantics

STLC has just one main computation rule to execute a program—the function application rule or a \(\beta\) reduction, as shown below:

This says that when a \(\lambda\) literal is applied to an
argument \(e_1\) the program takes a single step of computation to
the body of the lambda literal \(e_0\) with every occurrence of
the bound variable \(x\) replaced by the argument \(e_1\). The
substituion has to be careful to avoid “name capture”, i.e.,
substituting a term in a context that re-binds its free variables. For
example, when substituting \(y \mapsto x\) in
\(\lambda x. y\), one must make sure that the resulting term is
**not** \(\lambda x. x\). Using de Bruijn notation will help us
make precise and avoid name capture.

The other computation rules in the language are inductively defined, e.g., \(e_0~e_1\) can take a step to \(e_0'~e_1\) if \(e_0 \longrightarrow e_0'\), and similarly for \(e_1\).

By choosing these other rules in different ways one obtains different
reduction strategies, e.g., call-by-value or call-by-name etc. We’ll
leave the choice of reduction strategy non-deterministic and represent
the computation rules of the STLC as an indexed inductive type, ```
step
e e'
```

encoding one or more steps of computation.

### Formalizing an Operational Semantics

The inductive type `step`

below describes a single step of
computation in what is known as a “small-step operational
semantics”. The type `step e e'`

is a relation between an initial
program `e`

and a program `e'`

that results after taking one step
of computation on some sub-term of `e`

.

```
type step : exp -> exp -> Type =
| Beta :
t:typ ->
e1:exp ->
e2:exp ->
step (EApp (ELam t e1) e2) (subst (sub_beta e2) e1)
| AppLeft :
#e1:exp ->
e2:exp ->
#e1':exp ->
hst:step e1 e1' ->
step (EApp e1 e2) (EApp e1' e2)
| AppRight :
e1:exp ->
#e2:exp ->
#e2':exp ->
hst:step e2 e2' ->
step (EApp e1 e2) (EApp e1 e2')
```

The constructor

`Beta`

represents the rule for \(\beta\) reduction. The most subtle part of the development is defining`subst`

and`sub_beta`

—we’ll return to that in detail shortly.

`AppLeft`

and`AppRight`

allow reducing either the left- or right-subterm of`EApp e1 e2`

.

#### Exercise

Define an inductive relation `steps : exp -> exp -> Type`

for the
transitive closure of `step`

, representing multiple steps of
computation.

Use this exercise file for all the exercises that follow.

**Answer**

```
type steps : exp -> exp -> Type =
| Single : #e0:exp ->
#e1:exp ->
step e0 e1 ->
steps e0 e1
| Many : #e0:exp ->
#e1:exp ->
#e2:exp ->
step e0 e1 ->
steps e1 e2 ->
steps e0 e2
```

### Substitution: Failed Attempt

Defining substitution is the trickiest part of the system. Our first attempt will convey the main intuitions, but F* will refuse to accept it as well-founded. We’ll then enrich our definitions to prove that substitution terminates.

We’ll define a substitution as a total function from variables `var`

to expressions `exp`

.

```
let sub0 = var -> exp
```

These kind of substituions are sometimes called “parallel substitutions”—the each variable is substituted independently of the others.

When doing a \(\beta\) reduction, we want to substitute the
variable associated with de Bruijn index `0`

in the body of the
function with the argument `e`

and then remove the \(\lambda\)
binder—`sub_beta0`

does just that, replacing variable `0`

with
`e`

and shifting other variables down by `1`

, since the
\(\lambda\) binder of the function is removed.

```
let sub_beta0 (e:exp)
: sub0
= fun (y:var) ->
if y = 0 then e (* substitute *)
else EVar (y-1) (* shift -1 *)
```

The function `subst s e`

applies the substitution `s`

to `e`

:

```
let sub_inc0 : sub0 = fun y -> EVar (y+1)
[@@expect_failure [19;19]]
let rec subst0 (s:sub0)
(e:exp)
: exp
= match e with
| EUnit -> EUnit
| EVar x -> s x
| EApp e1 e2 -> EApp (subst0 s e1) (subst0 s e2)
| ELam t e1 -> ELam t (subst0 (sub_elam0 s) e1)
and sub_elam0 (s:sub0)
: sub0
= fun y ->
if y=0
then EVar y
else subst0 sub_inc0 (s (y - 1))
```

The

`EUnit`

case is trivial—there are no variables to substitute.In the variable case

`subst0 s (EVar x)`

just applies`s`

to`x`

.In the

`EApp`

case, we apply the substitution to each sub-term.The

`ELam`

case is the most interesting. To apply the substitution`s`

to the body`e1`

, we have to traverse a binder. The mutally recursive function`sub_elam0 s`

adjusts`s`

to account for this new binder, which has de Bruijn index`0`

in the body`e1`

(at least until another binder is encountered).In

`sub_elam0`

, if we are applying`s`

to the newly bound variable at index`0`

, then we leave that variable unchanged, since`s`

cannot affect it.Otherwise, we have a variable with index at least

`1`

, referencing a binder that is bound in an outer scope; so, we shift it down and apply`s`

to it, and then increment all the variables in the resulting term (using`sub_inc0`

) to avoid capture.

This definition of substitution is correct, but F* refuses to accept
it since we have not convinced the typechecker that `subst0`

and
`sub_elam0`

actually terminate. In fact, F* complains in two
locations about a failed termination check.

Note

This definition is expected to fail, so the ```
[@@expect_failure
[19;19]]
```

attribute on the definition asks F* to check that the
definition raises Error 19 twice. We’ll look in detail as to why it
fails, next.

### Substitution, Proven Total

Informally, let’s try to convince ourselves why `subst0`

and
`sub_elam0`

actually terminate.

The recursive calls in the

`EApp`

case are applied to strictly smaller sub-terms (`e0`

and`e1`

) of the original term`e`

.In the

`ELam`

case, we apply`subst0`

to a smaller sub-term`e1`

, but we make a mutally recursive call to`sub_elam0 s`

first—so we need to check that that call terminates. This is the first place where F* complains.When calling

`sub_elam0`

, it calls back to`subst0`

on a completely unrelated term`s (y - 1)`

, and F* complains that this may not terminate. But, thankfully, this call makes use only of the`sub_inc0`

substitution, which is just a renaming substitution and which does not make any further recursive calls. Somehow, we have to convince F* that a recursive call with a renaming substitution is fine.

To distinguish renamings from general substitutions, we’ll use an
indexed type `sub r`

, shown below.

```
let sub (renaming:bool) =
f:(var -> exp){ renaming <==> (forall x. EVar? (f x)) }
```

`sub true`

is the type of renamings, substitutions that map variables to variables.`sub false`

are substitutions that map at least one variable to a non-variable.

It’s easy to prove that `sub_inc`

is a renaming:

```
let sub_inc
: sub true
= fun y -> EVar (y+1)
```

The function `sub_beta`

shown below is the analog of `sub_beta0`

,
but with a type that tracks whether it is a renaming or not.

```
let sub_beta (e:exp)
: sub (EVar? e)
= let f =
fun (y:var) ->
if y = 0 then e (* substitute *)
else (EVar (y-1)) (* shift -1 *)
in
if not (EVar? e)
then introduce exists (x:var). ~(EVar? (f x))
with 0 and ();
f
```

The type says that

`sub_beta e`

is a renaming if and only if`e`

is itself a variable.Proving this type, particularly in the case where

`e`

is not a variable requires proving an existentially quantified formula, i.e.,`exists x. ~(EVar (subst_beta e) x)`

. As mentioned previously, the SMT solver cannot always automatically instantiate existential quantifiers in the goal. So, we introduce the existential quantifier explicitly, providing the witness`0`

, and then the SMT solver can easily prove`~(EVar (subst_beta e) 0)`

.

Finally, we show the definitions of `subst`

and `sub_elam`

below—identical to `subst0`

and `sub_elam0`

, but enriched with
types that allow expressing a termination argument to F* using a
4-ary lexicographic ordering.

```
let bool_order (b:bool) = if b then 0 else 1
let is_var (e:exp) : int = if EVar? e then 0 else 1
let rec subst (#r:bool)
(s:sub r)
(e:exp)
: Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
(decreases %[bool_order (EVar? e);
bool_order r;
1;
e])
= match e with
| EUnit -> EUnit
| EVar x -> s x
| EApp e1 e2 -> EApp (subst s e1) (subst s e2)
| ELam t e1 -> ELam t (subst (sub_elam s) e1)
and sub_elam (#r:bool) (s:sub r)
: Tot (sub r)
(decreases %[1;
bool_order r;
0;
EVar 0])
= let f : var -> exp =
fun y ->
if y=0
then EVar y
else subst sub_inc (s (y - 1))
in
assert (not r ==> (forall x. ~(EVar? (s x)) ==> ~(EVar? (f (x + 1)))));
f
```

Let’s analyze the recursive calls of `subst`

and `subst_elam`

to
see why this order works.

Cases of

`subst`

:The

`EUnit`

and`EVar`

cases are trivial, as before.In

`EApp`

,`e`

is definitely not a variable, so`bool_order (EVar? e)`

is`1`

. if`e1`

(respectively`e2`

) are variables, then this recursive call terminates, the lexicographic tuple`(0, _, _, _) << (1, _, _, _)`

, regardles of the other values. Otherwise, the last component of the tuple decreases (since`e1`

and`e2`

are proper sub-terms of`e`

), while none of the other components of the tuple change.The call to

`sub_elam s`

in`ELam`

terminates because the third component of the tuple decreases from`1`

to`0`

, while the first two do not change.The final recursive call to

`subst`

terminates for similar reasons to the recursive calls in the`EApp`

case, since the type of`sub_elam`

guarantees that`sub_elam s`

is renaming if an only of`s`

is (so the`r`

bit does not change).

Cases of

`sub_elam`

, in the recursive call to`subst sub_inc (s (y - 1))`

, we have already proven that`sub_inc`

is a renaming. So, we have two cases to consider:If

`s (y - 1)`

is a variable, then`bool_order (EVar? e)`

, the first component of the decreases clause of`subst`

is`0`

, which clearly precedes`1`

, the first component of the decreases clause of`subst_elam`

.Otherwwise,

`s (y - 1)`

is not a variable, so`s`

is definitely not a renaming while`sub_inc`

is. So, the second second component of the decreases clause decreases while the first component is unchanged.

Finally, we need to prove that `sub_elam s`

is a renaming if and
only if `s`

is. For this, we need two things:

First, strengthen the type of

`subst s`

to show that it maps variables to variables if and only if`r`

is a renaming,Second, we need to instantiate an exisential quantifier in

`sub_elam`

, to show that if`s`

is not a renaming, then it must map some`x`

to a non-variable and, hence,`sub_elam s (x + 1)`

is a non-variable too. One way to do this is by asserting this fact, which is a sufficient hint to the SMT solver to find the instantiation needed. Another way is to explicitly introduce the existential, as in the exercise below.

In summary, using indexed types combined with well-founded recursion on lexicographic orderings, we were able to prove our definitions total. That said, coming up with such orderings is non-trivial and requires some ingenuity, but once you do, it allows for relatively compact definitions that handle both substiutions and renamings.

#### Exercise

Remove the first component of the decreases clause of both definitions and revise the definitions to make F* accept it.

Your solution should have signature

```
let rec subst1 (#r:bool)
(s:sub r)
(e:exp)
: Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
(decreases %[bool_order r;
1;
e])
...
and sub_elam1 (#r:bool) (s:sub r)
: Tot (sub r)
(decreases %[bool_order r;
0;
EVar 0])
```

**Hint**

Inline a case of `subst`

in `subst_elam`

.
The answer is included with the next problem below.

Replace the assertion in `subst_elam`

with a proof that explicitly
introduces the existential quantifier.

**Answer**

```
let rec subst1 (#r:bool)
(s:sub r)
(e:exp)
: Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
(decreases %[bool_order r;
1;
e])
= match e with
| EVar x -> s x
| ELam t e1 -> ELam t (subst1 (sub_elam1 s) e1)
| EApp e1 e2 -> EApp (subst1 s e1) (subst1 s e2)
| EUnit -> EUnit
and sub_elam1 (#r:bool) (s:sub r)
: Tot (sub r)
(decreases %[bool_order r;
0;
EVar 0])
= let f : var -> exp =
fun y ->
if y=0
then EVar y
else match s (y - 1) with
| EVar x -> sub_inc x
| e -> subst1 sub_inc e
in
introduce not r ==> (exists x. ~ (EVar? (f x)))
with not_r.
eliminate exists y. ~ (EVar? (s y))
returns _
with not_evar_sy.
introduce exists x. ~(EVar? (f x))
with (y + 1)
and ()
;
f
```

## Type system

If when running a program, if one ends up with an term like \(()~e\) (i.e., some non-function term like \(()\) being used as if it were a function) then a runtime error has occurred and the program crashes. A type system for the simply-typed lambda calculus is designed to prevent this kind of runtime error.

The type system is an inductively defined relation `typing g e t`

between a

typing environment

`g:env`

, a partial map from variable indexes in a particular scope to their annotated types;a program expression

`e:exp`

;and its type

`t:typ`

.

### Environments

The code below shows our representation of typing environments
`env`

, a total function from variable indexes `var`

to `Some t`

or `None`

.

```
let env = var -> option typ
let empty : env = fun _ -> None
let extend (t:typ) (g:env)
: env
= fun y -> if y = 0 then Some t
else g (y-1)
```

The

`empty`

environment maps all variables to`None`

.Extending an an environment

`g`

associating a type`t`

with a new variable at index`0`

involves shifting up the indexes of all other variables in`g`

by`1`

.

### Typing Relation

The type system of STLC is defined by the inductively defined relation
`typing g e t`

shown below. A value of `typing g e t`

is a
derivation, or a proof, that `e`

has type `t`

in the environment
`g`

.

```
noeq
type typing : env -> exp -> typ -> Type =
| TyUnit :
#g:env ->
typing g EUnit TUnit
| TyVar :
#g:env ->
x:var{Some? (g x)} ->
typing g (EVar x) (Some?.v (g x))
| TyLam :
#g :env ->
t:typ ->
#e1:exp ->
#t':typ ->
hbody:typing (extend t g) e1 t' ->
typing g (ELam t e1) (TArr t t')
| TyApp :
#g:env ->
#e1:exp ->
#e2:exp ->
#t11:typ ->
#t12:typ ->
h1:typing g e1 (TArr t11 t12) ->
h2:typing g e2 t11 ->
typing g (EApp e1 e2) t12
```

The type does not support decidable equality, since all its constructors contain a field

`g:env`

, a function-typed value without decidable equality. So, we mark the inductive with the`noeq`

qualifier, as described previously.`TyUnit`

says that the unit value`EUnit`

has type`TUnit`

in all environments.`TyVar`

says that a variable`x`

is well-typed only in an environment`g`

that binds its type to`Some t`

, in which case, the program`EVar x`

has type`t`

. This rule ensures that no out-of-scope variables can be used.`TyLam`

says that a function literal`ELam t e1`

has type`TArr t t'`

in environment`g`

, when the body of the function`e1`

has type`t'`

in an environment that extends`g`

with a binding for the new variable at type`t`

(while shifting and retaining all other ariables).Finally,

`TyApp`

allows applying`e1`

to`e2`

only when`e1`

has an arrow type and the argument`e2`

has the type of the formal parameter of`e1`

—the entire term has the return type of`e1`

.

## Progress

It’s relatively easy to prove that a well-typed non-unit or lambda
term with no free variables can take a single step of
computation. This property is known as *progress*.

### Exercise

State and prove progress.

**Answer**

```
let is_value (e:exp) : bool = ELam? e || EUnit? e
let rec progress (#e:exp {~ (is_value e) })
(#t:typ)
(h:typing empty e t)
: (e':exp & step e e')
= let TyApp #g #e1 #e2 #t11 #t12 h1 h2 = h in
match e1 with
| ELam t e1' -> (| subst (sub_beta e2) e1', Beta t e1' e2 |)
| _ -> let (| e1', h1' |) = progress h1 in
(| EApp e1' e2, AppLeft e2 h1'|)
```

## Preservation

Given a well-typed term satisfying `typing g e t`

and `steps e e'`

,
we would like to prove that `e'`

has the same type as `e`

, i.e.,
`typing g e' t`

. This property is known as *preservation* (or
sometimes *subject reduction*). When taken in combination with
*progress*, this allows us to show that a well-typed term can keep
taking a step until it reaches a value.

The proof below establishes preservation for a single step.

```
let rec preservation_step #e #e' #g #t (ht:typing g e t) (hs:step e e')
: typing g e' t
= let TyApp h1 h2 = ht in
match hs with
| Beta tx e1' e2' -> substitution_beta h2 (TyLam?.hbody h1)
| AppLeft e2' hs1 -> TyApp (preservation_step h1 hs1) h2
| AppRight e1' hs2 -> TyApp h1 (preservation_step h2 hs2)
```

Since we know the computation takes a step, the typing derivation

`ht`

must be an instance of`TyApp`

.In the

`AppLeft`

and`AppRight`

case, we can easily use the induction hypothesis depending on which side actually stepped.The

`Beta`

case is the most interesting and requires a lemma about substitutions preserving typing.

The substitution lemma follows:

```
let subst_typing #r (s:sub r) (g1:env) (g2:env) =
x:var{Some? (g1 x)} -> typing g2 (s x) (Some?.v (g1 x))
let rec substitution (#g1:env)
(#e:exp)
(#t:typ)
(#r:bool)
(s:sub r)
(#g2:env)
(h1:typing g1 e t)
(hs:subst_typing s g1 g2)
: Tot (typing g2 (subst s e) t)
(decreases %[bool_order (EVar? e); bool_order r; e])
= match h1 with
| TyUnit -> TyUnit
| TyVar x -> hs x
| TyApp hfun harg -> TyApp (substitution s hfun hs) (substitution s harg hs)
| TyLam tlam hbody ->
let hs'' : subst_typing (sub_inc) g2 (extend tlam g2) =
fun x -> TyVar (x+1)
in
let hs' : subst_typing (sub_elam s) (extend tlam g1) (extend tlam g2) =
fun y -> if y = 0 then TyVar y
else substitution sub_inc (hs (y - 1)) hs''
in
TyLam tlam (substitution (sub_elam s) hbody hs')
```

It starts with a notion of typability of substitutions, ```
subst_typing
s g1 g2
```

, which that if a variable `x`

has type `g1 x`

, then ```
s
x
```

must have that same type in `g2`

.

The substitution lemma lifts this notion to expressions, stating that
applying a well-typed substitution `subst_typing s g1 g2`

to a term
well-typed in `g1`

produces a term well-typed in `g2`

with the
same type.

### Exercise

Use the substitution lemma to state and prove the
`substitution_beta`

lemma used in the proof of preservation.

**Answer**

```
let substitution_beta #e #v #t_x #t #g
(h1:typing g v t_x)
(h2:typing (extend t_x g) e t)
: typing g (subst (sub_beta v) e) t
= let hs : subst_typing (sub_beta v) (extend t_x g) g =
fun y -> if y = 0 then h1 else TyVar (y-1) in
substitution (sub_beta v) h2 hs
```

### Exercise

Prove a preservation lemma for multiple steps.

**Answer**

```
let rec preservation #e #e' #g #t (ht:typing g e t) (hs:steps e e')
: Tot (typing g e' t)
(decreases hs)
= match hs with
| Single s ->
preservation_step ht s
| Many s0 s1 ->
let ht' = preservation_step ht s0 in
preservation ht' s1
```

## Exercise

Prove a type soundness lemma with the following statement:

```
let soundness #e #e' #t
(ht:typing empty e t)
: either (squash (is_value e))
(e':exp & steps e e' & typing empty e' t)
```

**Answer**

```
= if is_value e then Inl ()
else let (| e', s |) = progress ht in
let ht' = preservation_step ht s in
Inr (| e', Single s, ht' |)
```

## Exercise

Add a step for reduction underneath a binder and prove the system sound.

**Answer**

```
(*
Copyright 2014-2015
Simon Forest - Inria and ENS Paris
Catalin Hritcu - Inria
Nikhil Swamy - Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Part2.STLC.Strong
open FStar.Classical.Sugar
(* Constructive-style progress and preservation proof for STLC with
strong reduction, using deBruijn indices and parallel substitution. *)
type typ =
| TUnit : typ
| TArr : typ -> typ -> typ
let var = nat
type exp =
| EUnit : exp
| EVar : var -> exp
| ELam : typ -> exp -> exp
| EApp : exp -> exp -> exp
(* Parallel substitution operation `subst` *)
let sub (renaming:bool) =
f:(var -> exp){ renaming <==> (forall x. EVar? (f x)) }
let bool_order (b:bool) = if b then 0 else 1
let sub_inc
: sub true
= fun y -> EVar (y+1)
let is_var (e:exp) : int = if EVar? e then 0 else 1
let rec subst (#r:bool)
(s:sub r)
(e:exp)
: Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
(decreases %[bool_order (EVar? e);
bool_order r;
1;
e])
= match e with
| EVar x -> s x
| ELam t e1 -> ELam t (subst (sub_elam s) e1)
| EApp e1 e2 -> EApp (subst s e1) (subst s e2)
| EUnit -> EUnit
and sub_elam (#r:bool) (s:sub r)
: Tot (sub r)
(decreases %[1;
bool_order r;
0;
EVar 0])
= let f : var -> exp =
fun y ->
if y=0
then EVar y
else subst sub_inc (s (y - 1))
in
introduce not r ==> (exists x. ~ (EVar? (f x)))
with not_r.
eliminate exists y. ~ (EVar? (s y))
returns _
with not_evar_sy.
introduce exists x. ~(EVar? (f x))
with (y + 1)
and ()
;
f
let sub_beta (e:exp)
: sub (EVar? e)
= let f =
fun (y:var) ->
if y = 0 then e (* substitute *)
else (EVar (y-1)) (* shift -1 *)
in
if not (EVar? e)
then introduce exists (x:var). ~(EVar? (f x))
with 0 and ();
f
(* Small-step operational semantics; strong / full-beta reduction is
non-deterministic, so necessarily as inductive relation *)
type step : exp -> exp -> Type =
| SBeta : t:typ ->
e1:exp ->
e2:exp ->
step (EApp (ELam t e1) e2) (subst (sub_beta e2) e1)
| SApp1 : #e1:exp ->
e2:exp ->
#e1':exp ->
hst:step e1 e1' ->
step (EApp e1 e2) (EApp e1' e2)
| SApp2 : e1:exp ->
#e2:exp ->
#e2':exp ->
hst:step e2 e2' ->
step (EApp e1 e2) (EApp e1 e2')
| STrans : #e0:exp ->
#e1:exp ->
#e2:exp ->
step e0 e1 ->
step e1 e2 ->
step e0 e2
| SStrong : t:typ ->
e:exp ->
e':exp ->
step e e' ->
step (ELam t e) (ELam t e')
(* Type system; as inductive relation (not strictly necessary for STLC) *)
type env = var -> option typ
let empty : env = fun _ -> None
(* we only need extend at 0 *)
let extend (t:typ) (g:env)
: env
= fun y -> if y = 0 then Some t
else g (y-1)
noeq
type typing : env -> exp -> typ -> Type =
| TyUnit : #g:env ->
typing g EUnit TUnit
| TyVar : #g:env ->
x:var{Some? (g x)} ->
typing g (EVar x) (Some?.v (g x))
| TyLam : #g :env ->
t:typ ->
#e1:exp ->
#t':typ ->
hbody:typing (extend t g) e1 t' ->
typing g (ELam t e1) (TArr t t')
| TyApp : #g:env ->
#e1:exp ->
#e2:exp ->
#t11:typ ->
#t12:typ ->
h1:typing g e1 (TArr t11 t12) ->
h2:typing g e2 t11 ->
typing g (EApp e1 e2) t12
(* Progress *)
let is_value (e:exp) : bool = ELam? e || EUnit? e
let rec progress (#e:exp {~ (is_value e) })
(#t:typ)
(h:typing empty e t)
: (e':exp & step e e')
= let TyApp #g #e1 #e2 #t11 #t12 h1 h2 = h in
match e1 with
| ELam t e1' -> (| subst (sub_beta e2) e1', SBeta t e1' e2 |)
| _ -> let (| e1', h1' |) = progress h1 in
(| EApp e1' e2, SApp1 e2 h1'|)
(* Typing of substitutions (very easy, actually) *)
let subst_typing #r (s:sub r) (g1:env) (g2:env) =
x:var{Some? (g1 x)} -> typing g2 (s x) (Some?.v (g1 x))
(* Substitution preserves typing
Strongest possible statement; suggested by Steven Schäfer *)
let rec substitution (#g1:env)
(#e:exp)
(#t:typ)
(#r:bool)
(s:sub r)
(#g2:env)
(h1:typing g1 e t)
(hs:subst_typing s g1 g2)
: Tot (typing g2 (subst s e) t)
(decreases %[bool_order (EVar? e); bool_order r; e])
= match h1 with
| TyVar x -> hs x
| TyApp hfun harg -> TyApp (substitution s hfun hs) (substitution s harg hs)
| TyLam tlam hbody ->
let hs'' : subst_typing (sub_inc) g2 (extend tlam g2) =
fun x -> TyVar (x+1) in
let hs' : subst_typing (sub_elam s) (extend tlam g1) (extend tlam g2) =
fun y -> if y = 0 then TyVar y
else substitution sub_inc (hs (y - 1)) hs''
in TyLam tlam (substitution (sub_elam s) hbody hs')
| TyUnit -> TyUnit
(* Substitution for beta reduction
Now just a special case of substitution lemma *)
let substitution_beta #e #v #t_x #t #g
(h1:typing g v t_x)
(h2:typing (extend t_x g) e t)
: typing g (subst (sub_beta v) e) t
= let hs : subst_typing (sub_beta v) (extend t_x g) g =
fun y -> if y = 0 then h1 else TyVar (y-1) in
substitution (sub_beta v) h2 hs
(* Type preservation *)
let rec preservation #e #e' #g #t (ht:typing g e t) (hs:step e e')
: Tot (typing g e' t)
(decreases hs)
= match hs with
| STrans s0 s1 ->
let ht' = preservation ht s0 in
preservation ht' s1
| _ ->
match ht with
| TyApp h1 h2 -> (
match hs with
| SBeta tx e1' e2' -> substitution_beta h2 (TyLam?.hbody h1)
| SApp1 e2' hs1 -> TyApp (preservation h1 hs1) h2
| SApp2 e1' hs2 -> TyApp h1 (preservation h2 hs2)
)
| TyLam t hb ->
let SStrong t e e' hs' = hs in
let hb' = preservation hb hs' in
TyLam t hb'
```