StlcThe Simply Typed Lambda-Calculus
The Simply Typed Lambda-Calculus
Overview
- variables
- function abstractions
- application
t ::= x variable
| \x:T1.t2 abstraction
| t1 t2 application
| true constant true
| false constant false
| if t1 then t2 else t3 conditional
| \x:T1.t2 abstraction
| t1 t2 application
| true constant true
| false constant false
| if t1 then t2 else t3 conditional
- \x:Bool. x
- (\x:Bool. x) true
- \x:Bool. if x then false else true
- \x:Bool. true
- \x:Bool. \y:Bool. x
- (\x:Bool. \y:Bool. x) false true
- \f:Bool→Bool. f (f true)
- (\f:Bool→Bool. f (f true)) (\x:Bool. false)
T ::= Bool
| T1 → T2
For example:
| T1 → T2
- \x:Bool. false has type Bool→Bool
- \x:Bool. x has type Bool→Bool
- (\x:Bool. x) true has type Bool
- \x:Bool. \y:Bool. x has type Bool→Bool→Bool (i.e. Bool → (Bool→Bool))
- (\x:Bool. \y:Bool. x) false has type Bool→Bool
- (\x:Bool. \y:Bool. x) false true has type Bool
Inductive tm : Type :=
| tvar : id → tm
| tapp : tm → tm → tm
| tabs : id → ty → tm → tm
| ttrue : tm
| tfalse : tm
| tif : tm → tm → tm → tm.
Note that an abstraction \x:T.t (formally, tabs x T t) is
always annotated with the type T of its parameter, in contrast
to Coq (and other functional languages like ML, Haskell, etc.),
which use type inference to fill in missing annotations. We're
not considering type inference here, to keep things simple.
Some examples...
idB = \x:Bool. x
idBB = \x:Bool→Bool. x
idBBBB = \x:(Bool→Bool) → (Bool→Bool). x
k = \x:Bool. \y:Bool. x
notB = \x:Bool. if x then false else true
(We write these as Notations rather than Definitions to make
things easier for auto.)
Operational Semantics
Values
- We can say that \x:T.t1 is a value only when t1 is a
value — i.e., only if the function's body has been
reduced (as much as it can be without knowing what argument it
is going to be applied to).
- Or we can say that \x:T.t1 is always a value, no matter whether t1 is one or not — in other words, we can say that reduction stops at abstractions.
Compute (fun x:bool ⇒ 3 + 4)
yields fun x:bool ⇒ 7.
Inductive value : tm → Prop :=
| v_abs : ∀x T t,
value (tabs x T t)
| v_true :
value ttrue
| v_false :
value tfalse.
Hint Constructors value.
Finally, we must consider what constitutes a complete program.
Intuitively, a "complete" program must not refer to any undefined
variables. We'll see shortly how to define the "free" variables
in a STLC term. A program is "closed", that is, it contains no
free variables.
Having made the choice not to reduce under abstractions,
we don't need to worry about whether variables are values, since
we'll always be reducing programs "from the outside in," and that
means the step relation will always be working with closed
terms (ones with no free variables).
Substitution
(\x:Bool. if x then true else x) false
to
if false then true else false
by substituting false for the parameter x in the body of the
function.
- [x:=true] (if x then x else false) yields if true then true else false
- [x:=true] x yields true
- [x:=true] (if x then x else y) yields if true then true else y
- [x:=true] y yields y
- [x:=true] false yields false (vacuous substitution)
- [x:=true] (\y:Bool. if y then x else false) yields \y:Bool. if y then true else false
- [x:=true] (\y:Bool. x) yields \y:Bool. true
- [x:=true] (\y:Bool. y) yields \y:Bool. y
- [x:=true] (\x:Bool. x) yields \x:Bool. x
[x:=s]x = s
[x:=s]y = y if x ≠ y
[x:=s](\x:T11.t12) = \x:T11. t12
[x:=s](\y:T11.t12) = \y:T11. [x:=s]t12 if x ≠ y
[x:=s](t1 t2) = ([x:=s]t1) ([x:=s]t2)
[x:=s]true = true
[x:=s]false = false
[x:=s](if t1 then t2 else t3) =
if [x:=s]t1 then [x:=s]t2 else [x:=s]t3
[x:=s]y = y if x ≠ y
[x:=s](\x:T11.t12) = \x:T11. t12
[x:=s](\y:T11.t12) = \y:T11. [x:=s]t12 if x ≠ y
[x:=s](t1 t2) = ([x:=s]t1) ([x:=s]t2)
[x:=s]true = true
[x:=s]false = false
[x:=s](if t1 then t2 else t3) =
if [x:=s]t1 then [x:=s]t2 else [x:=s]t3
Reserved Notation "'[' x ':=' s ']' t" (at level 20).
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tvar x' ⇒
if beq_id x x' then s else t
| tabs x' T t1 ⇒
tabs x' T (if beq_id x x' then t1 else ([x:=s] t1))
| tapp t1 t2 ⇒
tapp ([x:=s] t1) ([x:=s] t2)
| ttrue ⇒
ttrue
| tfalse ⇒
tfalse
| tif t1 t2 t3 ⇒
tif ([x:=s] t1) ([x:=s] t2) ([x:=s] t3)
end
where "'[' x ':=' s ']' t" := (subst x s t).
Technical note: Substitution becomes trickier to define if we
consider the case where s, the term being substituted for a
variable in some other term, may itself contain free variables.
Since we are only interested here in defining the step relation
on closed terms (i.e., terms like \x:Bool. x, that do not mention
variables are not bound by some enclosing lambda), we can skip
this extra complexity here, but it must be dealt with when
formalizing richer languages.
The definition that we gave above uses Coq's Fixpoint facility
to define substitution as a function. Suppose, instead, we
wanted to define substitution as an inductive relation substi.
We've begun the definition by providing the Inductive header and
one of the constructors; your job is to fill in the rest of the
constructors.
Exercise: 3 stars (substi)
Inductive substi (s:tm) (x:id) : tm → tm → Prop :=
| s_var1 :
substi s x (tvar x) s
(* FILL IN HERE *)
.
Hint Constructors substi.
Theorem substi_correct : ∀s x t t',
[x:=s]t = t' ↔ substi s x t t'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Reduction
(\x:T.t12) v2 ⇒ [x:=v2]t12
is traditionally called "beta-reduction".
value v2 | (ST_AppAbs) |
(\x:T.t12) v2 ⇒ [x:=v2]t12 |
t1 ⇒ t1' | (ST_App1) |
t1 t2 ⇒ t1' t2 |
value v1 | |
t2 ⇒ t2' | (ST_App2) |
v1 t2 ⇒ v1 t2' |
(ST_IfTrue) | |
(if true then t1 else t2) ⇒ t1 |
(ST_IfFalse) | |
(if false then t1 else t2) ⇒ t2 |
t1 ⇒ t1' | (ST_If) |
(if t1 then t2 else t3) ⇒ (if t1' then t2 else t3) |
Reserved Notation "t1 '⇒' t2" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀x T t12 v2,
value v2 →
(tapp (tabs x T t12) v2) ⇒ [x:=v2]t12
| ST_App1 : ∀t1 t1' t2,
t1 ⇒ t1' →
tapp t1 t2 ⇒ tapp t1' t2
| ST_App2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
tapp v1 t2 ⇒ tapp v1 t2'
| ST_IfTrue : ∀t1 t2,
(tif ttrue t1 t2) ⇒ t1
| ST_IfFalse : ∀t1 t2,
(tif tfalse t1 t2) ⇒ t2
| ST_If : ∀t1 t1' t2 t3,
t1 ⇒ t1' →
(tif t1 t2 t3) ⇒ (tif t1' t2 t3)
where "t1 '⇒' t2" := (step t1 t2).
Hint Constructors step.
Notation multistep := (multi step).
Notation "t1 '⇒*' t2" := (multistep t1 t2) (at level 40).
Lemma step_example1 :
(tapp idBB idB) ⇒* idB.
Proof.
eapply multi_step.
apply ST_AppAbs.
apply v_abs.
simpl.
apply multi_refl. Qed.
Example:
((\x:Bool→Bool. x) ((\x:Bool→Bool. x) (\x:Bool. x)))
⇒* (\x:Bool. x)
i.e.
⇒* (\x:Bool. x)
(idBB (idBB idB)) ⇒* idB.
Lemma step_example2 :
(tapp idBB (tapp idBB idB)) ⇒* idB.
Proof.
eapply multi_step.
apply ST_App2. auto.
apply ST_AppAbs. auto.
eapply multi_step.
apply ST_AppAbs. simpl. auto.
simpl. apply multi_refl. Qed.
Example:
((\x:Bool→Bool. x) (\x:Bool. if x then false
else true)) true)
⇒* false
i.e.
else true)) true)
⇒* false
((idBB notB) ttrue) ⇒* tfalse.
Lemma step_example3 :
tapp (tapp idBB notB) ttrue ⇒* tfalse.
Proof.
eapply multi_step.
apply ST_App1. apply ST_AppAbs. auto. simpl.
eapply multi_step.
apply ST_AppAbs. auto. simpl.
eapply multi_step.
apply ST_IfTrue. apply multi_refl. Qed.
Example:
((\x:Bool → Bool. x) ((\x:Bool. if x then false
else true) true))
⇒* false
i.e.
else true) true))
⇒* false
(idBB (notB ttrue)) ⇒* tfalse.
Lemma step_example4 :
tapp idBB (tapp notB ttrue) ⇒* tfalse.
Proof.
eapply multi_step.
apply ST_App2. auto.
apply ST_AppAbs. auto. simpl.
eapply multi_step.
apply ST_App2. auto.
apply ST_IfTrue.
eapply multi_step.
apply ST_AppAbs. auto. simpl.
apply multi_refl. Qed.
A more automatic proof
Again, we can use the normalize tactic from above to simplify
the proof.
Lemma step_example2' :
(tapp idBB (tapp idBB idB)) ⇒* idB.
Proof.
normalize.
Qed.
Lemma step_example3' :
tapp (tapp idBB notB) ttrue ⇒* tfalse.
Proof. normalize. Qed.
Lemma step_example4' :
tapp idBB (tapp notB ttrue) ⇒* tfalse.
Proof. normalize. Qed.
Lemma step_example5 :
(tapp (tapp idBBBB idBB) idB)
⇒* idB.
Proof.
(* FILL IN HERE *) Admitted.
(* FILL IN HERE *)
☐
Contexts
Typing Relation
Γ x = T | (T_Var) |
Γ ⊢ x ∈ T |
Γ , x:T11 ⊢ t12 ∈ T12 | (T_Abs) |
Γ ⊢ \x:T11.t12 ∈ T11->T12 |
Γ ⊢ t1 ∈ T11->T12 | |
Γ ⊢ t2 ∈ T11 | (T_App) |
Γ ⊢ t1 t2 ∈ T12 |
(T_True) | |
Γ ⊢ true ∈ Bool |
(T_False) | |
Γ ⊢ false ∈ Bool |
Γ ⊢ t1 ∈ Bool Γ ⊢ t2 ∈ T Γ ⊢ t3 ∈ T | (T_If) |
Γ ⊢ if t1 then t2 else t3 ∈ T |
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
| T_Var : ∀Γ x T,
Γ x = Some T →
Γ ⊢ tvar x ∈ T
| T_Abs : ∀Γ x T11 T12 t12,
update Γ x T11 ⊢ t12 ∈ T12 →
Γ ⊢ tabs x T11 t12 ∈ TArrow T11 T12
| T_App : ∀T11 T12 Γ t1 t2,
Γ ⊢ t1 ∈ TArrow T11 T12 →
Γ ⊢ t2 ∈ T11 →
Γ ⊢ tapp t1 t2 ∈ T12
| T_True : ∀Γ,
Γ ⊢ ttrue ∈ TBool
| T_False : ∀Γ,
Γ ⊢ tfalse ∈ TBool
| T_If : ∀t1 t2 t3 T Γ,
Γ ⊢ t1 ∈ TBool →
Γ ⊢ t2 ∈ T →
Γ ⊢ t3 ∈ T →
Γ ⊢ tif t1 t2 t3 ∈ T
where "Gamma '⊢' t '∈' T" := (has_type Γ t T).
Hint Constructors has_type.
Example typing_example_1 :
empty ⊢ tabs x TBool (tvar x) ∈ TArrow TBool TBool.
Proof.
apply T_Abs. apply T_Var. reflexivity. Qed.
Note that since we added the has_type constructors to the hints
database, auto can actually solve this one immediately.
Another example:
empty ⊢ \x:A. λy:A→A. y (y x))
∈ A → (A→A) → A.
∈ A → (A→A) → A.
Example typing_example_2 :
empty ⊢
(tabs x TBool
(tabs y (TArrow TBool TBool)
(tapp (tvar y) (tapp (tvar y) (tvar x))))) ∈
(TArrow TBool (TArrow (TArrow TBool TBool) TBool)).
Proof with auto using update_eq.
apply T_Abs.
apply T_Abs.
eapply T_App. apply T_Var...
eapply T_App. apply T_Var...
apply T_Var...
Qed.
empty ⊢
(tabs x TBool
(tabs y (TArrow TBool TBool)
(tapp (tvar y) (tapp (tvar y) (tvar x))))) ∈
(TArrow TBool (TArrow (TArrow TBool TBool) TBool)).
Proof with auto using update_eq.
apply T_Abs.
apply T_Abs.
eapply T_App. apply T_Var...
eapply T_App. apply T_Var...
apply T_Var...
Qed.
Exercise: 2 stars, optional (typing_example_2_full)
Prove the same result without using auto, eauto, or eapply.Example typing_example_2_full :
empty ⊢
(tabs x TBool
(tabs y (TArrow TBool TBool)
(tapp (tvar y) (tapp (tvar y) (tvar x))))) ∈
(TArrow TBool (TArrow (TArrow TBool TBool) TBool)).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars (typing_example_3)
Formally prove the following typing derivation holds:
empty ⊢ \x:Bool→B. λy:Bool→Bool. λz:Bool.
y (x z)
∈ T.
y (x z)
∈ T.
Example typing_example_3 :
∃T,
empty ⊢
(tabs x (TArrow TBool TBool)
(tabs y (TArrow TBool TBool)
(tabs z TBool
(tapp (tvar y) (tapp (tvar x) (tvar z)))))) ∈
T.
Proof with auto.
(* FILL IN HERE *) Admitted.
☐
We can also show that terms are not typable. For example, let's
formally check that there is no typing derivation assigning a type
to the term \x:Bool. \y:Bool, x y — i.e.,
¬ ∃T,
empty ⊢ \x:Bool. λy:Bool, x y : T.
empty ⊢ \x:Bool. λy:Bool, x y : T.
Example typing_nonexample_1 :
¬ ∃T,
empty ⊢
(tabs x TBool
(tabs y TBool
(tapp (tvar x) (tvar y)))) ∈
T.
Proof.
intros Hc. inversion Hc.
(* The clear tactic is useful here for tidying away bits of
the context that we're not going to need again. *)
inversion H. subst. clear H.
inversion H5. subst. clear H5.
inversion H4. subst. clear H4.
inversion H2. subst. clear H2.
inversion H5. subst. clear H5.
inversion H1. Qed.
¬ ∃T,
empty ⊢
(tabs x TBool
(tabs y TBool
(tapp (tvar x) (tvar y)))) ∈
T.
Proof.
intros Hc. inversion Hc.
(* The clear tactic is useful here for tidying away bits of
the context that we're not going to need again. *)
inversion H. subst. clear H.
inversion H5. subst. clear H5.
inversion H4. subst. clear H4.
inversion H2. subst. clear H2.
inversion H5. subst. clear H5.
inversion H1. Qed.
Exercise: 3 stars, optional (typing_nonexample_3)
Another nonexample:
¬ (∃S, ∃T,
empty ⊢ \x:S. x x : T).
empty ⊢ \x:S. x x : T).
Example typing_nonexample_3 :
¬ (∃S, ∃T,
empty ⊢
(tabs x S
(tapp (tvar x) (tvar x))) ∈
T).
Proof.
(* FILL IN HERE *) Admitted.
☐