`` (ƛ "x" ⇒ ` "x" · (` "x" · `zero)) ``. Instead, we should rename the bound variable to avoid capture: * `` (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · `zero ] `` should yield

`` ƛ "x′" ⇒ ` "x′" · (` "x" · `zero) ``. Here `x′` is a fresh variable distinct from `x`. Formal definition of substitution with suitable renaming is considerably more complex, so we avoid it by restricting to substitution by closed terms, which will be adequate for our purposes. Here is the formal definition of substitution by closed terms in Agda: ```agda infix 9 _[_:=_] _[_:=_] : Term → Id → Term → Term (` x) [ y := V ] with x ≟ y ... | yes _ = V ... | no _ = ` x (ƛ x ⇒ N) [ y := V ] with x ≟ y ... | yes _ = ƛ x ⇒ N ... | no _ = ƛ x ⇒ N [ y := V ] (L · M) [ y := V ] = L [ y := V ] · M [ y := V ] (`zero) [ y := V ] = `zero (`suc M) [ y := V ] = `suc M [ y := V ] (case L [zero⇒ M |suc x ⇒ N ]) [ y := V ] with x ≟ y ... | yes _ = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N ] ... | no _ = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N [ y := V ] ] (μ x ⇒ N) [ y := V ] with x ≟ y ... | yes _ = μ x ⇒ N ... | no _ = μ x ⇒ N [ y := V ] ``` Let's unpack the first three cases: * For variables, we compare `y`, the substituted variable, with `x`, the variable in the term. If they are the same, we yield `V`, otherwise we yield `x` unchanged. * For abstractions, we compare `y`, the substituted variable, with `x`, the variable bound in the abstraction. If they are the same, we yield the abstraction unchanged, otherwise we substitute inside the body. * For application, we recursively substitute in the function and the argument. Case expressions and recursion also have bound variables that are treated similarly to those in lambda abstractions. Otherwise we simply push substitution recursively into the subterms. ### Examples Here is confirmation that the examples above are correct: ```agda _ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") _ = refl _ : (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] ≡ sucᶜ · (sucᶜ · `zero) _ = refl _ : (ƛ "x" ⇒ ` "y") [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero _ = refl _ : (ƛ "x" ⇒ ` "x") [ "x" := `zero ] ≡ ƛ "x" ⇒ ` "x" _ = refl _ : (ƛ "y" ⇒ ` "y") [ "x" := `zero ] ≡ ƛ "y" ⇒ ` "y" _ = refl ``` #### Quiz What is the result of the following substitution? (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ ` "x")) [ "x" := `zero ] 1. `` (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ ` "x")) `` 2. `` (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ `zero)) `` 3. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ ` "x")) `` 4. `` (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ `zero)) `` #### Exercise `_[_:=_]′` (stretch) The definition of substitution above has three clauses (`ƛ`, `case`, and `μ`) that invoke a `with` clause to deal with bound variables. Rewrite the definition to factor the common part of these three clauses into a single function, defined by mutual recursion with substitution. ```agda mutual infix 9 _[_:=_]′ _⇒′_[_:=_]′ _[_:=_]′ : Term → Id → Term → Term (` x) [ y := V ]′ with x ≟ y ... | yes _ = V ... | no _ = ` x (ƛ x ⇒ N) [ y := V ]′ = ƛ x ⇒ (x ⇒′ N [ y := V ]′) (L · M) [ y := V ]′ = L [ y := V ]′ · M [ y := V ]′ (`zero) [ y := V ]′ = `zero (`suc M) [ y := V ]′ = `suc M [ y := V ]′ (case L [zero⇒ M |suc x ⇒ N ]) [ y := V ]′ = case L [ y := V ]′ [zero⇒ M [ y := V ]′ |suc x ⇒ (x ⇒′ N [ y := V ]′) ] (μ x ⇒ N) [ y := V ]′ = μ x ⇒ (x ⇒′ N [ y := V ]′) _⇒′_[_:=_]′ : Id → Term → Id → Term → Term x ⇒′ M [ y := V ]′ with x ≟ y ... | yes _ = M ... | no _ = M [ y := V ]′ ``` ## Reduction We give the reduction rules for call-by-value lambda calculus. To reduce an application, first we reduce the left-hand side until it becomes a value (which must be an abstraction); then we reduce the right-hand side until it becomes a value; and finally we substitute the argument for the variable in the abstraction. In an informal presentation of the operational semantics, the rules for reduction of applications are written as follows: L —→ L′ --------------- ξ-·₁ L · M —→ L′ · M M —→ M′ --------------- ξ-·₂ V · M —→ V · M′ ----------------------------- β-ƛ (ƛ x ⇒ N) · V —→ N [ x := V ] The Agda version of the rules below will be similar, except that universal quantifications are made explicit, and so are the predicates that indicate which terms are values. The rules break into two sorts. Compatibility rules direct us to reduce some part of a term. We give them names starting with the Greek letter `ξ` (_xi_). Once a term is sufficiently reduced, it will consist of a constructor and a deconstructor, in our case `ƛ` and `·`, which reduces directly. We give them names starting with the Greek letter `β` (_beta_) and such rules are traditionally called _beta rules_. A bit of terminology: A term that matches the left-hand side of a reduction rule is called a _redex_. In the redex `(ƛ x ⇒ N) · V`, we may refer to `x` as the _formal parameter_ of the function, and `V` as the _actual parameter_ of the function application. Beta reduction replaces the formal parameter by the actual parameter. If a term is a value, then no reduction applies; conversely, if a reduction applies to a term then it is not a value. We will show in the next chapter that this exhausts the possibilities: every well-typed term either reduces or is a value. For numbers, zero does not reduce and successor reduces the subterm. A case expression reduces its argument to a number, and then chooses the zero or successor branch as appropriate. A fixpoint replaces the bound variable by the entire fixpoint term; this is the one case where we substitute by a term that is not a value. Here are the rules formalised in Agda: ```agda infix 4 _—→_ data _—→_ : Term → Term → Set where ξ-·₁ : ∀ {L L′ M} → L —→ L′ ----------------- → L · M —→ L′ · M ξ-·₂ : ∀ {V M M′} → Value V → M —→ M′ ----------------- → V · M —→ V · M′ β-ƛ : ∀ {x N V} → Value V ------------------------------ → (ƛ x ⇒ N) · V —→ N [ x := V ] ξ-suc : ∀ {M M′} → M —→ M′ ------------------ → `suc M —→ `suc M′ ξ-case : ∀ {x L L′ M N} → L —→ L′ ----------------------------------------------------------------- → case L [zero⇒ M |suc x ⇒ N ] —→ case L′ [zero⇒ M |suc x ⇒ N ] β-zero : ∀ {x M N} ---------------------------------------- → case `zero [zero⇒ M |suc x ⇒ N ] —→ M β-suc : ∀ {x V M N} → Value V --------------------------------------------------- → case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ] β-μ : ∀ {x M} ------------------------------ → μ x ⇒ M —→ M [ x := μ x ⇒ M ] ``` The reduction rules are carefully designed to ensure that subterms of a term are reduced to values before the whole term is reduced. This is referred to as _call-by-value_ reduction. Further, we have arranged that subterms are reduced in a left-to-right order. This means that reduction is _deterministic_: for any term, there is at most one other term to which it reduces. Put another way, our reduction relation `—→` is in fact a function. This style of explaining the meaning of terms is called a _small-step operational semantics_. If `M —→ N`, we say that term `M` _reduces_ to term `N`, or equivalently, term `M` _steps_ to term `N`. Each compatibility rule has another reduction rule in its premise; so a step always consists of a beta rule, possibly adjusted by zero or more compatibility rules. #### Quiz What does the following term step to? (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") —→ ??? 1. `` (ƛ "x" ⇒ ` "x") `` 2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") `` 3. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") `` What does the following term step to? (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") —→ ??? 1. `` (ƛ "x" ⇒ ` "x") `` 2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") `` 3. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") `` What does the following term step to? (Where `twoᶜ` and `sucᶜ` are as defined above.) twoᶜ · sucᶜ · `zero —→ ??? 1. `` sucᶜ · (sucᶜ · `zero) `` 2. `` (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero `` 3. `` `zero `` ## Reflexive and transitive closure A single step is only part of the story. In general, we wish to repeatedly step a closed term until it reduces to a value. We do this by defining the reflexive and transitive closure `—↠` of the step relation `—→`. We define reflexive and transitive closure as a sequence of zero or more steps of the underlying relation, along lines similar to that for reasoning about chains of equalities in Chapter [Equality](/Equality/): ```agda infix 2 _—↠_ infix 1 begin_ infixr 2 _—→⟨_⟩_ infix 3 _∎ data _—↠_ : Term → Term → Set where _∎ : ∀ M --------- → M —↠ M _—→⟨_⟩_ : ∀ L {M N} → L —→ M → M —↠ N --------- → L —↠ N begin_ : ∀ {M N} → M —↠ N ------ → M —↠ N begin M—↠N = M—↠N ``` We can read this as follows: * From term `M`, we can take no steps, giving a step of type `M —↠ M`. It is written `M ∎`. * From term `L` we can take a single step of type `L —→ M` followed by zero or more steps of type `M —↠ N`, giving a step of type `L —↠ N`. It is written `L —→⟨ L—→M ⟩ M—↠N`, where `L—→M` and `M—↠N` are steps of the appropriate type. The notation is chosen to allow us to lay out example reductions in an appealing way, as we will see in the next section. Alternatively, we might define reflexive and transitive closure directly as the smallest relation that includes `—→` and is reflexive and transitive. We do so as follows: ```agda data _—↠′_ : Term → Term → Set where step′ : ∀ {M N} → M —→ N ------- → M —↠′ N refl′ : ∀ {M} ------- → M —↠′ M trans′ : ∀ {L M N} → L —↠′ M → M —↠′ N ------- → L —↠′ N ``` The three constructors specify, respectively, that `—↠′` includes `—→` and is reflexive and transitive. A good exercise is to show that the two definitions are equivalent (indeed, one embeds in the other). #### Exercise `—↠≲—↠′` (practice) Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic? ```agda open import plfa.part1.Isomorphism using (_≲_) open import Relation.Binary.PropositionalEquality using (cong) to' : ∀ {M N} → M —↠ N → M —↠′ N to' (_ ∎) = refl′ to' (_ —→⟨ p ⟩ q) = trans′ (step′ p) (to' q) trans : ∀ {M N P} → M —↠ N → N —↠ P → M —↠ P trans (_ ∎) q = q trans (_ —→⟨ s ⟩ p) q = _ —→⟨ s ⟩ trans p q from' : ∀ {M N} → M —↠′ N → M —↠ N from' (step′ p) = _ —→⟨ p ⟩ _ ∎ from' refl′ = _ ∎ from' (trans′ p q) = trans (from' p) (from' q) from∘to' : ∀ {M N} (p : M —↠ N) → from' (to' p) ≡ p from∘to' (_ ∎) = refl from∘to' (_ —→⟨ x ⟩ p) = cong (λ q → _ —→⟨ x ⟩ q) (from∘to' p) —↠≲—↠′ : ∀ {M N} → (M —↠ N) ≲ (M —↠′ N) —↠≲—↠′ = record { to = to' ; from = from' ; from∘to = from∘to' } -- The other direction (to∘from) does not hold: -- —↠ is modeled as a list of steps, whereas —↠` is modeled as a tree -- of steps. This implies that for each M and N, there are either 0 or 1 terms of type `M —↠ N`, -- whereas there can be also more than 1 term of type `M —↠′ N`. -- -- example: given three proofs: -- p₁ : M –→ N -- p₂ : N –→ P -- p₃ : P –→ Q -- -- there is only one way to combine them to M —↠ N, i.e. -- -- _ –→⟨ p₁ ⟩ _ –→⟨ p₂ ⟩ _ –→⟨ p₃ ⟩ _ ∎ -- -- but there are two ways to combine them to M —↠′ N, i.e. -- -- trans′ p₁ (trans′ p₂ p₃) -- trans′ (trans′ p₁ p₂) p₃ -- -- Converting from M —↠′ N to M —↠ N and back, loses this structure. -- -- This is analogous to the Bin-exercises where arbitrary amounts of -- leading zeros cause multiple bit-string representations of the same -- natural number. ``` ## Confluence One important property a reduction relation might satisfy is to be _confluent_. If term `L` reduces to two other terms, `M` and `N`, then both of these reduce to a common term `P`. It can be illustrated as follows: L / \ / \ / \ M N \ / \ / \ / P Here `L`, `M`, `N` are universally quantified while `P` is existentially quantified. If each line stands for zero or more reduction steps, this is called confluence, while if the top two lines stand for a single reduction step and the bottom two stand for zero or more reduction steps it is called the diamond property. In symbols: ```agda postulate confluence : ∀ {L M N} → ((L —↠ M) × (L —↠ N)) -------------------- → ∃[ P ] ((M —↠ P) × (N —↠ P)) diamond : ∀ {L M N} → ((L —→ M) × (L —→ N)) -------------------- → ∃[ P ] ((M —↠ P) × (N —↠ P)) ``` The reduction system studied in this chapter is deterministic. In symbols: ```agda postulate deterministic : ∀ {L M N} → L —→ M → L —→ N ------ → M ≡ N ``` It is easy to show that every deterministic relation satisfies the diamond and confluence properties. Hence, all the reduction systems studied in this text are trivially confluent. ## Examples We start with a simple example. The Church numeral two applied to the successor function and zero yields the natural number two: ```agda _ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero _ = begin twoᶜ · sucᶜ · `zero —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero —→⟨ β-ƛ V-zero ⟩ sucᶜ · (sucᶜ · `zero) —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩ sucᶜ · `suc `zero —→⟨ β-ƛ (V-suc V-zero) ⟩ `suc (`suc `zero) ∎ ``` Here is a sample reduction demonstrating that two plus two is four: ```agda _ : plus · two · two —↠ `suc `suc `suc `suc `zero _ = begin plus · two · two —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩ (ƛ "m" ⇒ ƛ "n" ⇒ case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · two · two —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩ (ƛ "n" ⇒ case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · two —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩ case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ] —→⟨ β-suc (V-suc V-zero) ⟩ `suc (plus · `suc `zero · two) —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩ `suc ((ƛ "m" ⇒ ƛ "n" ⇒ case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · `suc `zero · two) —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩ `suc ((ƛ "n" ⇒ case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · two) —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩ `suc (case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]) —→⟨ ξ-suc (β-suc V-zero) ⟩ `suc `suc (plus · `zero · two) —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩ `suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒ case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · `zero · two) —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩ `suc `suc ((ƛ "n" ⇒ case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · two) —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩ `suc `suc (case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]) —→⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎ ``` And here is a similar sample reduction for Church numerals: ```agda _ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero _ = begin (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z")) · twoᶜ · twoᶜ · sucᶜ · `zero —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩ (ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (` "n" · ` "s" · ` "z")) · twoᶜ · sucᶜ · `zero —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩ (ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (twoᶜ · ` "s" · ` "z")) · sucᶜ · `zero —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ (ƛ "z" ⇒ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` "z")) · `zero —→⟨ β-ƛ V-zero ⟩ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero) —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩ (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (twoᶜ · sucᶜ · `zero) —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩ (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · ((ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero) —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩ (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (sucᶜ · `zero)) —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩ (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (`suc `zero)) —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩ (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (`suc `suc `zero) —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩ sucᶜ · (sucᶜ · `suc `suc `zero) —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩ sucᶜ · (`suc `suc `suc `zero) —→⟨ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩ `suc (`suc (`suc (`suc `zero))) ∎ ``` In the next chapter, we will see how to compute such reduction sequences. #### Exercise `plus-example` (practice) Write out the reduction sequence demonstrating that one plus one is two. ```agda `one = `suc `zero `two = `suc `one infixr 2 _—→⟨⟩_ _—→⟨⟩_ : ∀ e {e'} → e —↠ e' → e —↠ e' _ —→⟨⟩ e—↠e' = e—↠e' _ : plus · `one · `one —↠ `two _ = begin plus · `one · `one —→⟨⟩ (μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]) · `one · `one —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩ (ƛ "m" ⇒ ƛ "n" ⇒ case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · `one · `one —→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩ (ƛ "n" ⇒ case `one [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · `one —→⟨ β-ƛ (V-suc V-zero) ⟩ case `one [zero⇒ `one |suc "m" ⇒ `suc (plus · ` "m" · `one) ] —→⟨ β-suc V-zero ⟩ `suc (plus · `zero · `one) —→⟨⟩ `suc ((μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]) · `zero · `one) —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩ `suc ((ƛ "m" ⇒ ƛ "n" ⇒ case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · `zero · `one) —→⟨ ξ-suc (ξ-·₁ (β-ƛ V-zero)) ⟩ `suc ((ƛ "n" ⇒ case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ]) · `one) —→⟨ ξ-suc (β-ƛ (V-suc V-zero)) ⟩ `suc (case `zero [zero⇒ `one |suc "m" ⇒ `suc (plus · ` "m" · `one) ]) —→⟨ ξ-suc β-zero ⟩ `suc `one —→⟨⟩ `two ∎ ``` ## Syntax of types We have just two types: * Functions, `A ⇒ B` * Naturals, `` `ℕ `` As before, to avoid overlap we use variants of the names used by Agda. Here is the syntax of types in BNF: A, B, C ::= A ⇒ B | `ℕ And here it is formalised in Agda: ```agda infixr 7 _⇒_ data Type : Set where _⇒_ : Type → Type → Type `ℕ : Type ``` ### Precedence As in Agda, functions of two or more arguments are represented via currying. This is made more convenient by declaring `_⇒_` to associate to the right and `_·_` to associate to the left. Thus: * ``(`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ`` stands for ``((`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ))``. * `plus · two · two` stands for `(plus · two) · two`. ### Quiz * What is the type of the following term? `` ƛ "s" ⇒ ` "s" · (` "s" · `zero) `` 1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) `` 2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ `` 3. `` `ℕ ⇒ (`ℕ ⇒ `ℕ) `` 4. `` `ℕ ⇒ `ℕ ⇒ `ℕ `` 5. `` `ℕ ⇒ `ℕ `` 6. `` `ℕ `` Give more than one answer if appropriate. * What is the type of the following term? `` (ƛ "s" ⇒ ` "s" · (` "s" · `zero)) · sucᶜ `` 1. `` (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ) `` 2. `` (`ℕ ⇒ `ℕ) ⇒ `ℕ `` 3. `` `ℕ ⇒ (`ℕ ⇒ `ℕ) `` 4. `` `ℕ ⇒ `ℕ ⇒ `ℕ `` 5. `` `ℕ ⇒ `ℕ `` 6. `` `ℕ `` Give more than one answer if appropriate. ## Typing ### Contexts While reduction considers only closed terms, typing must consider terms with free variables. To type a term, we must first type its subterms, and in particular in the body of an abstraction its bound variable may appear free. A _context_ associates variables with types. We let `Γ` and `Δ` range over contexts. We write `∅` for the empty context, and `Γ , x ⦂ A` for the context that extends `Γ` by associating variable `x` with type `A`. For example, * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ `` is the context that associates variable `` "s" `` with type `` `ℕ ⇒ `ℕ ``, and variable `` "z" `` with type `` `ℕ ``. Contexts are formalised as follows: ```agda infixl 5 _,_⦂_ data Context : Set where ∅ : Context _,_⦂_ : Context → Id → Type → Context ``` #### Exercise `Context-≃` (practice) Show that `Context` is isomorphic to `List (Id × Type)`. For instance, the isomorphism relates the context ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ to the list [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ] ```agda open import Data.Product using (_×_; _,_) infix 0 _≃_ record _≃_ (A B : Set) : Set where field to : A → B from : B → A from∘to : ∀ (x : A) → from (to x) ≡ x to∘from : ∀ (y : B) → to (from y) ≡ y open _≃_ Context-to-List : Context → List (Id × Type) Context-to-List ∅ = [] Context-to-List (Γ , x ⦂ t) = (x , t) ∷ Context-to-List Γ Context-from-List : List (Id × Type) → Context Context-from-List [] = ∅ Context-from-List ((x , t) ∷ Γ) = Context-from-List Γ , x ⦂ t Context-from∘to-List : ∀ Γ → Context-from-List (Context-to-List Γ) ≡ Γ Context-from∘to-List ∅ = refl Context-from∘to-List (Γ , x ⦂ t) = cong (_, x ⦂ t) (Context-from∘to-List Γ) Context-to∘from-List : ∀ Γ → Context-to-List (Context-from-List Γ) ≡ Γ Context-to∘from-List [] = refl Context-to∘from-List ((x , t) ∷ Γ) = cong ((x , t) ∷_) (Context-to∘from-List Γ) Context-≃-List : Context ≃ List (Id × Type) Context-≃-List = record { to = Context-to-List ; from = Context-from-List ; from∘to = Context-from∘to-List ; to∘from = Context-to∘from-List } ``` ### Lookup judgment We have two forms of _judgment_. The first is written Γ ∋ x ⦂ A and indicates in context `Γ` that variable `x` has type `A`. It is called _lookup_. For example, * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "z" ⦂ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ `` give us the types associated with variables `` "z" `` and `` "s" ``, respectively. The symbol `∋` (pronounced "ni", for "in" backwards) is chosen because checking that `Γ ∋ x ⦂ A` is analogous to checking whether `x ⦂ A` appears in a list corresponding to `Γ`. If two variables in a context have the same name, then lookup should return the most recently bound variable, which _shadows_ the other variables. For example, * `` ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ∋ "x" ⦂ `ℕ ``. Here `` "x" ⦂ `ℕ ⇒ `ℕ `` is shadowed by `` "x" ⦂ `ℕ ``. Lookup is formalised as follows: ```agda infix 4 _∋_⦂_ data _∋_⦂_ : Context → Id → Type → Set where Z : ∀ {Γ x A} ------------------ → Γ , x ⦂ A ∋ x ⦂ A S : ∀ {Γ x y A B} → x ≢ y → Γ ∋ x ⦂ A ------------------ → Γ , y ⦂ B ∋ x ⦂ A ``` The constructors `Z` and `S` correspond roughly to the constructors `here` and `there` for the element-of relation `_∈_` on lists. Constructor `S` takes an additional parameter, which ensures that when we look up a variable that it is not _shadowed_ by another variable with the same name to its left in the list. It can be rather tedious to use the `S` constructor, as you have to provide proofs that `x ≢ y` each time. For example: ```agda _ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ ⇒ `ℕ _ = S (λ()) (S (λ()) Z) ``` Instead, we'll use a "smart constructor", which uses [proof by reflection](/Decidable/#proof-by-reflection) to check the inequality while type checking: ```agda S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A ------------------ → Γ , y ⦂ B ∋ x ⦂ A S′ {x≢y = x≢y} x = S (toWitnessFalse x≢y) x ``` ### Typing judgment The second judgment is written Γ ⊢ M ⦂ A and indicates in context `Γ` that term `M` has type `A`. Context `Γ` provides types for all the free variables in `M`. For example: * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "z" ⦂ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · ` "z" ⦂ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · (` "s" · ` "z") ⦂ `ℕ `` * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ `ℕ ⇒ `ℕ `` * `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` Typing is formalised as follows: ```agda infix 4 _⊢_⦂_ data _⊢_⦂_ : Context → Term → Type → Set where -- Axiom ⊢` : ∀ {Γ x A} → Γ ∋ x ⦂ A ----------- → Γ ⊢ ` x ⦂ A -- ⇒-I ⊢ƛ : ∀ {Γ x N A B} → Γ , x ⦂ A ⊢ N ⦂ B ------------------- → Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B -- ⇒-E _·_ : ∀ {Γ L M A B} → Γ ⊢ L ⦂ A ⇒ B → Γ ⊢ M ⦂ A ------------- → Γ ⊢ L · M ⦂ B -- ℕ-I₁ ⊢zero : ∀ {Γ} -------------- → Γ ⊢ `zero ⦂ `ℕ -- ℕ-I₂ ⊢suc : ∀ {Γ M} → Γ ⊢ M ⦂ `ℕ --------------- → Γ ⊢ `suc M ⦂ `ℕ -- ℕ-E ⊢case : ∀ {Γ L M x N A} → Γ ⊢ L ⦂ `ℕ → Γ ⊢ M ⦂ A → Γ , x ⦂ `ℕ ⊢ N ⦂ A ------------------------------------- → Γ ⊢ case L [zero⇒ M |suc x ⇒ N ] ⦂ A ⊢μ : ∀ {Γ x M A} → Γ , x ⦂ A ⊢ M ⦂ A ----------------- → Γ ⊢ μ x ⇒ M ⦂ A ``` Each type rule is named after the constructor for the corresponding term. Most of the rules have a second name, derived from a convention in logic, whereby the rule is named after the type connective that it concerns; rules to introduce and to eliminate each connective are labeled `-I` and `-E`, respectively. As we read the rules from top to bottom, introduction and elimination rules do what they say on the tin: the first _introduces_ a formula for the connective, which appears in the conclusion but not in the premises; while the second _eliminates_ a formula for the connective, which appears in a premise but not in the conclusion. An introduction rule describes how to construct a value of the type (abstractions yield functions, successor and zero yield naturals), while an elimination rule describes how to deconstruct a value of the given type (applications use functions, case expressions use naturals). Note also the three places (in `⊢ƛ`, `⊢case`, and `⊢μ`) where the context is extended with `x` and an appropriate type, corresponding to the three places where a bound variable is introduced. The rules are deterministic, in that at most one rule applies to every term. ### Example type derivations {#derivation} Type derivations correspond to trees. In informal notation, here is a type derivation for the Church numeral two, ∋s ∋z ------------------ ⊢` -------------- ⊢` ∋s Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "z" ⦂ A ------------------ ⊢` ------------------------------------- _·_ Γ₂ ⊢ ` "s" ⦂ A ⇒ A Γ₂ ⊢ ` "s" · ` "z" ⦂ A ---------------------------------------------- _·_ Γ₂ ⊢ ` "s" · (` "s" · ` "z") ⦂ A -------------------------------------------- ⊢ƛ Γ₁ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A ------------------------------------------------------------- ⊢ƛ Γ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (A ⇒ A) ⇒ A ⇒ A where `∋s` and `∋z` abbreviate the two derivations, ---------------- Z "s" ≢ "z" Γ₁ ∋ "s" ⦂ A ⇒ A ----------------------------- S ------------- Z Γ₂ ∋ "s" ⦂ A ⇒ A Γ₂ ∋ "z" ⦂ A and where `Γ₁ = Γ , "s" ⦂ A ⇒ A` and `Γ₂ = Γ , "s" ⦂ A ⇒ A , "z" ⦂ A`. The typing derivation is valid for any `Γ` and `A`, for instance, we might take `Γ` to be `∅` and `A` to be `` `ℕ ``. Here is the above typing derivation formalised in Agda: ```agda Ch : Type → Type Ch A = (A ⇒ A) ⇒ A ⇒ A ⊢twoᶜ : ∀ {Γ A} → Γ ⊢ twoᶜ ⦂ Ch A ⊢twoᶜ = ⊢ƛ (⊢ƛ (⊢` ∋s · (⊢` ∋s · ⊢` ∋z))) where ∋s = S′ Z ∋z = Z ``` Here are the typings corresponding to computing two plus two: ```agda ⊢two : ∀ {Γ} → Γ ⊢ two ⦂ `ℕ ⊢two = ⊢suc (⊢suc ⊢zero) ⊢plus : ∀ {Γ} → Γ ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ ⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (⊢` ∋m) (⊢` ∋n) (⊢suc (⊢` ∋+ · ⊢` ∋m′ · ⊢` ∋n′))))) where ∋+ = S′ (S′ (S′ Z)) ∋m = S′ Z ∋n = Z ∋m′ = Z ∋n′ = S′ Z ⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ ⊢2+2 = ⊢plus · ⊢two · ⊢two ``` In contrast to our earlier examples, here we have typed `two` and `plus` in an arbitrary context rather than the empty context; this makes it easy to use them inside other binding contexts as well as at the top level. Here the two lookup judgments `∋m` and `∋m′` refer to two different bindings of variables named `"m"`. In contrast, the two judgments `∋n` and `∋n′` both refer to the same binding of `"n"` but accessed in different contexts, the first where `"n"` is the last binding in the context, and the second after `"m"` is bound in the successor branch of the case. And here are typings for the remainder of the Church example: ```agda ⊢plusᶜ : ∀ {Γ A} → Γ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z))))) where ∋m = S′ (S′ (S′ Z)) ∋n = S′ (S′ Z) ∋s = S′ Z ∋z = Z ⊢sucᶜ : ∀ {Γ} → Γ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ ⊢sucᶜ = ⊢ƛ (⊢suc (⊢` ∋n)) where ∋n = Z ⊢2+2ᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ ⊢2+2ᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero ``` ### Interaction with Agda Construction of a type derivation may be done interactively. Start with the declaration: ⊢sucᶜ : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ ⊢sucᶜ = ? Typing C-c C-l causes Agda to create a hole and tell us its expected type: ⊢sucᶜ = { }0 ?0 : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ Now we fill in the hole by typing C-c C-r. Agda observes that the outermost term in `sucᶜ` is `ƛ`, which is typed using `⊢ƛ`. The `⊢ƛ` rule in turn takes one argument, which Agda leaves as a hole: ⊢sucᶜ = ⊢ƛ { }1 ?1 : ∅ , "n" ⦂ `ℕ ⊢ `suc ` "n" ⦂ `ℕ We can fill in the hole by typing C-c C-r again: ⊢sucᶜ = ⊢ƛ (⊢suc { }2) ?2 : ∅ , "n" ⦂ `ℕ ⊢ ` "n" ⦂ `ℕ And again: ⊢sucᶜ = ⊢ƛ (⊢suc (⊢` { }3)) ?3 : ∅ , "n" ⦂ `ℕ ∋ "n" ⦂ `ℕ A further attempt with C-c C-r yields the message: Don't know which constructor to introduce of Z or S We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are done: ⊢sucᶜ = ⊢ƛ (⊢suc (⊢` Z)) The entire process can be automated using Agsy, invoked with C-c C-a. Chapter [Inference](/Inference/) will show how to use Agda to compute type derivations directly. ### Lookup is functional The lookup relation `Γ ∋ x ⦂ A` is functional, in that for each `Γ` and `x` there is at most one `A` such that the judgment holds: ```agda ∋-functional : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B ∋-functional Z Z = refl ∋-functional Z (S x≢ _) = ⊥-elim (x≢ refl) ∋-functional (S x≢ _) Z = ⊥-elim (x≢ refl) ∋-functional (S _ ∋x) (S _ ∋x′) = ∋-functional ∋x ∋x′ ``` The typing relation `Γ ⊢ M ⦂ A` is not functional. For example, in any `Γ` the term `` ƛ "x" ⇒ ` "x" `` has type `A ⇒ A` for any type `A`. ### Non-examples We can also show that terms are _not_ typeable. For example, here is a formal proof that it is not possible to type the term `` `zero · `suc `zero ``. It cannot be typed, because doing so requires that the first term in the application is both a natural and a function: ```agda nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A) nope₁ (() · _) ``` As a second example, here is a formal proof that it is not possible to type `` ƛ "x" ⇒ ` "x" · ` "x" ``. It cannot be typed, because doing so requires types `A` and `B` such that `A ⇒ B ≡ A`: ```agda nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A) nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′)) = contradiction (∋-functional ∋x ∋x′) where contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A) contradiction () ``` #### Quiz For each of the following, give a type `A` for which it is derivable, or explain why there is no such `A`. 1. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ` "y" · ` "x" ⦂ A `` 2. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ` "x" · ` "y" ⦂ A `` 3. `` ∅ , "y" ⦂ `ℕ ⇒ `ℕ ⊢ ƛ "x" ⇒ ` "y" · ` "x" ⦂ A `` For each of the following, give types `A`, `B`, and `C` for which it is derivable, or explain why there are no such types. 1. `` ∅ , "x" ⦂ A ⊢ ` "x" · ` "x" ⦂ B `` 2. `` ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ` "x" · (` "y" · ` "z") ⦂ C `` #### Exercise `⊢mul` (recommended) Using the term `mul` you defined earlier, write out the derivation showing that it is well typed. ```agda ⊢mul : ∅ ⊢ mul ⦂ (`ℕ ⇒ `ℕ ⇒ `ℕ) ⊢mul = ⊢μ (⊢ƛ (⊢ƛ (⊢case ⊢n ⊢zero ((⊢plus · ⊢n') · ((⊢* · ⊢m) · ⊢n'))))) where ⊢m = ⊢` Z ⊢n = ⊢` (S (λ()) Z) ⊢n' = ⊢` (S (λ()) Z) ⊢* = ⊢` (S (λ()) (S (λ()) (S (λ()) Z))) ``` #### Exercise `⊢mulᶜ` (practice) Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed. ```agda -- The type of church numerals: A number `n` takes a function and a regular -- argument, and applies the function `n` times to the argument. -- Technically we don't have to use `ℕ here, but any type would do. `ℕᶜ : Type `ℕᶜ = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ ⊢mulᶜ : ∅ ⊢ mulᶜ ⦂ (`ℕᶜ ⇒ `ℕᶜ ⇒ `ℕᶜ) ⊢mulᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ ((⊢m · (⊢n · ⊢s)) · ⊢z)))) where ⊢z = ⊢` Z ⊢s = ⊢` (S (λ()) Z) ⊢n = ⊢` (S (λ()) (S (λ()) Z)) ⊢m = ⊢` (S (λ()) (S (λ()) (S (λ()) Z))) ``` ## Unicode This chapter uses the following unicode: ⇒ U+21D2 RIGHTWARDS DOUBLE ARROW (\=>) ƛ U+019B LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-) · U+00B7 MIDDLE DOT (\cdot) ≟ U+225F QUESTIONED EQUAL TO (\?=) — U+2014 EM DASH (\em) ↠ U+21A0 RIGHTWARDS TWO HEADED ARROW (\rr-) ξ U+03BE GREEK SMALL LETTER XI (\Gx or \xi) β U+03B2 GREEK SMALL LETTER BETA (\Gb or \beta) Γ U+0393 GREEK CAPITAL LETTER GAMMA (\GG or \Gamma) ≠ U+2260 NOT EQUAL TO (\=n or \ne) ∋ U+220B CONTAINS AS MEMBER (\ni) ∅ U+2205 EMPTY SET (\0) ⊢ U+22A2 RIGHT TACK (\vdash or \|-) ⦂ U+2982 Z NOTATION TYPE COLON (\:) 😇 U+1F607 SMILING FACE WITH HALO 😈 U+1F608 SMILING FACE WITH HORNS We compose reduction `—→` from an em dash `—` and an arrow `→`. Similarly for reflexive and transitive closure `—↠`.