static semantics: grammar and typing rules of the language

dynamic semantics: evaluation rules

---

The structure of the rules that we will see: each statement, whether a premise or a conclusion, typically involves a context, a term and a classification.

For example, here is the rule $\to -elim$. Both the premises and the conclusion take the form $\Gamma ⊢M:A$, which we can read "In the context $\Gamma$, $M$ has type $A$."

---

The name "simply typed lambda calculus" is rather unwieldy, so we’ll use the traditional and shorter name ${\lambda }^{\to }$

For uniformity we will present both the grammar of the language and the type rules as inference rules.

The elements of the lambda calculi described here are divided into three "sorts":

• terms
• types, We write $M:A$ to say that the term $M$ has the type $A$.
• kinds, which you can think of as the types of type expressions. We write $T::K$ to say that the type expression $T$ has the kind $K$.

Kinding rules in ${\lambda }^{\to }$

In ${\lambda }^{\to }$, there is a single kind, called $\ast$.

There are two kinding rules, which describe how to form types:

The $\text{ kind- }\mathcal{B}$ rule introduces a base type $\mathcal{B}$ of kind $\ast$. Base types correspond to primitive types available in most programming languages.

The $\text{kind-}\to$ gives us a way of forming function types $A\to B$ from types $A$ and $B$.

For example, the type $(\mathcal{B}\to \mathcal{B})\to \mathcal{B}$ can be derived as follows:

Environment rules in ${\lambda }^{\to }$

Environments associate variables with their classifiers — i.e.

• term variables with types
• and type variables with kinds.

In ${\lambda }^{\to }$ there are two rules for forming environments:

Typing rules in ${\lambda }^{\to }$

The tvar rule shows how to type open terms (i.e. terms with free variables).

The introduction rule $\to \text{ -intro }$ shows how to form a term $\lambda x:A.M$ of type $A\to B$

The elimination rule $\to \text{ -elim }$ shows how to apply terms of function type.

The $\to \text{ -intro }$ and $\to \text{ -elim }$ form the first introduction-elimination pair.

---

Extensions

Adding products

We introduce a new type: product type $A\times B$

Kinding rules for $\times$

There is a new way of forming types, so we need a new kinding rule.

Typing rules for $\times$

There are three new typing rules:

The $\times \text{ -intro }$ rule shows how to build pairs: a pair $⟨M,N⟩$ of type $A\times B$ is built from terms $M$ and $N$ of types $A$ and $B$.

The $\times -\text{elim-1}$ and $\times -\text{elim-2}$ rules show how to deconstruct pairs.

Adding sums

We next extend ${\lambda }^{\to }$ with sum types, which correspond to a simple version of variants.

Kinding rules for $+$

There is a new way of forming types, so we need a new kinding rule.

Typing rules for $+$

There are three new typing rules:

The $+\text{ -intro-1 }$ and $+\text{ -intro-2 }$ rules show how to build values of sum type by injecting with $inl$ or $inr$
In order to maintain the property that each term has a unique type we also require a type argument to $inl$ and $inr$

The $+\text{ -elim }$ rule shows how to deconstruct sums.

---

In the lambda-calculus everything is a function: the arguments accepted by functions are themselves functions and the result returned by a function is another function

When discussing the syntax of programming languages, it is useful to distinguish two levels of structure.

• The concrete syntax of the language refers to the string of characters that programmers directly read and write.
• The abstract syntax is a much simpler internal representation of programs as labeled trees (called abstract syntax trees).

Definition: An occurrence of the variable $x$ is said to be bound when it occurs in the body $t$ of an abstraction $\lambda x.t$. Definition: An occurrence of $x$ is free if it appears in a position where it is not bound by an enclosing abstraction on $x$.

Definition: A term with no free variables is said to be closed; closed terms are also called combinators

Operational Semantics

redex... / beta-reduction...

---

Evaluation Strategies:

• full beta-reduction
• normal order strategy, the left most outer most
• call by name strategy

Recursion

Definition: Terms with no normal form are said to diverge.

• e.g., $\omega =(\lambda x.xx)(\lambda x.xx)$

TODO: p61