The simply typed lambda-calculus (STLC) is a tiny core calculus embodying the key concept of functional abstraction. This concept shows up in pretty much every real-world programming language in some form (functions, procedures, methods, etc.). We will follow exactly the same pattern as in the previous chapter when formalizing this calculus (syntax, small-step semantics, typing rules) and its main properties (progress and preservation). The new technical challenges arise from the mechanisms of variable binding and substitution. It will take some work to deal with these. The STLC lives in the lower-left front corner of the famous lambda cube (also called the Barendregt Cube), which visualizes three sets of features that can be added to its simple core:
                               Calculus of Constructions
      type operators +--------+
                    /| /|
                   / | / |
     polymorphism +--------+ |
                  | | | |
                  | +-----|--+
                  | / | /
                  |/ |/
                  +--------+ dependent types
                STLC Moving from bottom to top in the cube corresponds to adding polymorphic types like ∀ X, X → X. Adding just polymorphism gives us the famous Girard-Reynolds calculus, System F. Moving from front to back corresponds to adding type operators like list. Moving from left to right corresponds to adding dependent types like ∀ n, array-of-size n. The top right corner on the back, which combines all three features, is called the Calculus of Constructions. First studied by Coquand and Huet, it forms the foundation of Coq's logic.

Overview

The STLC is built on some collection of base types: booleans, numbers, strings, etc. The exact choice of base types doesn't matter much -- the definition of the language as well as its theoretical properties work out the same no matter what we choose -- so for the sake of brevity let's take just Bool for the moment. At the end of the chapter we'll see how to add more base types, and in later chapters we'll enrich the pure STLC with other useful constructs like pairs, records, subtyping, and mutable state. Starting from boolean constants and conditionals, we add three things:

• variables
• function abstractions
• application

This gives us the following collection of abstract syntax constructors (written out first in informal BNF notation -- we'll formalize it below).
       t ::= x (variable)
           | \x:T,t (abstraction)
           | t t (application)
           | true (constant true)
           | false (constant false)
           | if t then t else t (conditional) The \ symbol in a function abstraction \x:T,t is usually written as a Greek letter "lambda" (hence the name of the calculus). The variable x is called the parameter to the function; the term t is its body. The annotation :T specifies the type of arguments that the function can be applied to. If you've seen lambda-calculus notation elsewhere, you might be wondering why abstraction is written here as \x:T,t instead of the usual "\x:T.t". The reason is that some user interfaces for interacting with Coq use periods to separate a file into "sentences" to be passed separately to the Coq top level. Some examples:

• \x:Bool, x
  The identity function for booleans.
• (\x:Bool, x) true
  The identity function for booleans, applied to the boolean true.
• \x:Bool, if x then false else true
  The boolean "not" function.
• \x:Bool, true
  The constant function that takes every (boolean) argument to true.

• \x:Bool, \y:Bool, x
  A two-argument function that takes two booleans and returns the first one. (As in Coq, a two-argument function in the lambda-calculus is really a one-argument function whose body is also a one-argument function.)
• (\x:Bool, \y:Bool, x) false true
  A two-argument function that takes two booleans and returns the first one, applied to the booleans false and true.
  As in Coq, application associates to the left -- i.e., this expression is parsed as ((\x:Bool, \y:Bool, x) false) true.
• \f:Bool→Bool, f (f true)
  A higher-order function that takes a function f (from booleans to booleans) as an argument, applies f to true, and applies f again to the result.
• (\f:Bool→Bool, f (f true)) (\x:Bool, false)
  The same higher-order function, applied to the constantly false function.

As the last several examples show, the STLC is a language of higher-order functions: we can write down functions that take other functions as arguments and/or return other functions as results. The STLC doesn't provide any primitive syntax for defining named functions: i.e., all functions are "anonymous." We'll see in chapter MoreStlc that it is easy to add named functions -- indeed, the fundamental naming and binding mechanisms are exactly the same. The types of the STLC include Bool, which classifies the boolean constants true and false as well as more complex computations that yield booleans, plus arrow types that classify functions.
      T ::= Bool
          | T → T For example:

• \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

Syntax

We next formalize the syntax of the STLC.

Types

Terms

We need some notation magic to set up the concrete syntax, as we did in the Imp chapter...

Note that an abstraction \x:T,t (formally, tm_abs 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 at all here. Examples...

(We write these as Notations rather than Definitions to make things easier for auto.)

Operational Semantics

To define the small-step semantics of STLC terms, we begin, as always, by defining the set of values. Next, we define the critical notions of free variables and substitution, which are used in the reduction rule for application expressions. And finally we give the small-step relation itself.

Values

To define the values of the STLC, we have a few cases to consider. First, for the boolean part of the language, the situation is clear: true and false are the only values. An if expression is never a value. Second, an application is not a value: it represents a function being invoked on some argument, which clearly still has work left to do. Third, for abstractions, we have a choice:

• We can say that \x:T, t is a value only when t 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, t is always a value, no matter whether t is one or not -- in other words, we can say that reduction stops at abstractions.

Our usual way of evaluating expressions in Gallina makes the first choice -- for example,
         Compute (fun x:bool ⇒ 3 + 4) yields:
         fun x:bool ⇒ 7 But Gallina is rather unusual in this respect. Most real-world functional programming languages make the second choice -- reduction of a function's body only begins when the function is actually applied to an argument. We also make the second choice here.

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 complete program, then, is one that is closed -- that is, that contains no free variables. (Conversely, a term that may contain free variables is often called an open term.) 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.

Substitution

Now we come to the heart of the STLC: the operation of substituting one term for a variable in another term. This operation is used below to define the operational semantics of function application, where we will need to substitute the argument term for the function parameter in the function's body. For example, we reduce
       (\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. In general, we need to be able to substitute some given term s for occurrences of some variable x in another term t. Informally, this is written [x:=s]t and pronounced "substitute s for x in t." Here are some examples:

• [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

The last example is key: substituting x with true in \x:Bool, x does not yield \x:Bool, true! The reason for this is that the x in the body of \x:Bool, x is bound by the abstraction: it is a new, local name that just happens to be spelled the same as some global name x. Here is the definition, informally...
       [x:=s]x = s
       [x:=s]y = y if x ≠ y
       [x:=s](\x:T, t) = \x:T, t
       [x:=s](\y:T, t) = \y:T, [x:=s]t if x ≠ y
       [x:=s](t₁ t₂) = ([x:=s]t₁) ([x:=s]t₂)
       [x:=s]true = true
       [x:=s]false = false
       [x:=s](if t₁ then t₂ else t₃) =
                       if [x:=s]t₁ then [x:=s]t₂ else [x:=s]t₃ ... and formally:

Note on notations: You might be wondering why we need parentheses around the substitution notation in the above definition, and why we need to redefine the substitution notation in the stlc custom grammar. The reason is that reserved notations in definitions have to be defined in the general Coq grammar (and not a custom one like stlc). This restriction only applies to the subst definition -- that is, before the where ... part. From now on, using the substitution notation in the stlc custom grammar doesn't need any curly braces. For example...

Technical note: Substitution also 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. For example, using the definition of substitution above to substitute the open term
      s = \x:Bool, r (where r is a free reference to some global resource) for the free variable z in the term
      t = \r:Bool, z where r is a bound variable, we would get
      \r:Bool, \x:Bool, r where the free reference to r in s has been "captured" by the binder at the beginning of t. Why would this be bad? Because it violates the principle that the names of bound variables do not matter. For example, if we rename the bound variable in t, e.g., let
      t' = \w:Bool, z then [z:=s]t' is
      \w:Bool, \x:Bool, r which does not behave the same as the original substitution into t:
      [z:=s]t = \r:Bool, \x:Bool, r That is, renaming a bound variable in t changes how t behaves under substitution. See, for example, [Aydemir 2008] for further discussion of this issue. Fortunately, since we are only interested here in defining the step relation on closed terms (i.e., terms like \x:Bool, x that include binders for all of the variables they mention), we can sidestep this extra complexity, but it must be dealt with when formalizing richer languages.

Exercise: 3 stars, standard (substi_correct)

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 and prove that the relation you've defined coincides with the function given above.

Reduction

The small-step reduction relation for STLC now follows the same pattern as the ones we have seen before. Intuitively, to reduce a function application, we first reduce its left-hand side (the function) until it becomes an abstraction; then we reduce its right-hand side (the argument) until it is also a value; and finally we substitute the argument for the bound variable in the body of the abstraction. This last rule, written informally as
      (\x:T,t₁₂) v₂ --> [x:=v₂] t₁₂ is traditionally called beta-reduction.

value v2	(ST_AppAbs)
(\x:T2,t1) v2 --> [x:=v2]t1

t1 --> t1'	(ST_App1)
t1 t2 --> t1' t2

value v1
t2 --> t2'	(ST_App2)
v1 t2 --> v1 t2'

... plus the usual rules for conditionals:

	(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)

Formally:

Examples

Example:
      (\x:Bool→Bool, x) (\x:Bool, x) -->* \x:Bool, x i.e.,
      idBB idB -->* idB

Example:
      (\x:Bool→Bool, x) ((\x:Bool→Bool, x) (\x:Bool, x))
            -->* \x:Bool, x i.e.,
      (idBB (idBB idB)) -->* idB.

Example:
      (\x:Bool→Bool, x)
         (\x:Bool, if x then false else true)
         true
            -->* false i.e.,
       (idBB notB) true -->* false.

Example:
      (\x:Bool → Bool, x)
         ((\x:Bool, if x then false else true) true)
            -->* false i.e.,
      idBB (notB true) -->* false. (Note that this term doesn't actually typecheck; even so, we can ask how it reduces.)

We can use the normalize tactic defined in the Smallstep chapter to simplify these proofs.

Exercise: 2 stars, standard (step_example5)

Try to do this one both with and without normalize.

Typing

Next we consider the typing relation of the STLC.

Contexts

Although we are primarily interested in the binary relation |-- t \in T, relating a closed term t to its type T, we need to generalize a bit to make the definitions work. Consider checking that \x:T₁₁,t₁₂ has type T₁₁→T₁₂. Intuitively, we need to check that t₁₂ has type T₁₂. However, we have removed the binder \x, so x may occur free in t₁₂ (that is, t₁₂ may be open). While checking that t₁₂ has type T₁₂, we must remember that x has type T₁₁, in order to deal with these free occurrences of x. Similarly, t₁₂ itself could contain abstractions, and typechecking their bodies could require looking up the declared types of yet more free variables. To keep track of all this, we add a third element to the relation, a typing context Gamma, which records the types of the variables that may occur free in a term -- that is, Gamma is a partial map from variables to types. The new typing judgment is written Gamma |-- t \in T and informally read as "term t has type T, given the types of free variables in t as specified by Gamma". We'll also write x ⊢> T ; Gamma for "update the partial map Gamma so that it maps x to T," following the notation from the Maps chapter. With these refinements, we are ready to give informal and formal specifications of the typing relation. Following the usual notation for partial maps, we write (X ⊢> T, Gamma) for "update the partial function Gamma so that it maps x to T."

Typing Relation

Gamma x = T1	(T_Var)
Gamma |-- x ∈ T1

x ⊢> T2 ; Gamma |-- t1 ∈ T1	(T_Abs)
Gamma |-- \x:T2,t1 ∈ T2->T1

Gamma |-- t1 ∈ T2->T1
Gamma |-- t2 ∈ T2	(T_App)
Gamma |-- t1 t2 ∈ T1

	(T_True)
Gamma |-- true ∈ Bool

	(T_False)
Gamma |-- false ∈ Bool

Gamma |-- t1 ∈ Bool    Gamma |-- t2 ∈ T1    Gamma |-- t3 ∈ T1	(T_If)
Gamma |-- if t1 then t2 else t3 ∈ T1

We can read the three-place relation Gamma |-- t \in T as: "under the assumptions in Gamma, the term t has the type T."

Examples

Note that, since we added the has_type constructors to the hints database, auto can actually solve this one immediately.

More examples:
       empty |-- \x:A, \y:A→A, y (y x)
             \in A → (A→A) → A.

Exercise: 2 stars, standard, optional (typing_example_2_full)

Prove the same result without using auto, eauto, or eapply (or ...).

Exercise: 2 stars, standard (typing_example_3)

Formally prove the following typing derivation holds:
       empty |-- \x:Bool→B, \y:Bool→Bool, \z:Bool,
                   y (x z)
             \in T.

We can also show that some terms are not typable. For example, let's 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 \in T.

Exercise: 3 stars, standard, optional (typing_nonexample_3)

Another nonexample:
    ¬(∃ S T,
          empty |-- \x:S, x x \in T).