---
title     : "Untyped: Untyped lambda calculus with full normalisation"
permalink : /Untyped/
---

```agda
module plfa.part2.Untyped where
```

In this chapter we play with variations on a theme:

* Previous chapters consider intrinsically-typed calculi;
  here we consider one that is untyped but intrinsically scoped.

* Previous chapters consider call-by-value calculi;
  here we consider call-by-name.

* Previous chapters consider _weak head normal form_,
  where reduction stops at a lambda abstraction;
  here we consider _full normalisation_,
  where reduction continues underneath a lambda.

* Previous chapters consider _deterministic_ reduction,
  where there is at most one redex in a given term;
  here we consider _non-deterministic_ reduction
  where a term may contain many redexes and any one of them may reduce.

* Previous chapters consider reduction of _closed_ terms,
  those with no free variables;
  here we consider _open_ terms,
  those which may have free variables.

* Previous chapters consider lambda calculus extended
  with natural numbers and fixpoints;
  here we consider a tiny calculus with just variables,
  abstraction, and application, in which the other
  constructs may be encoded.

In general, one may mix and match these features,
save that full normalisation requires open terms and
encoding naturals and fixpoints requires being untyped.
The aim of this chapter is to give some appreciation for
the range of different lambda calculi one may encounter.


# Imports

```agda
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _<_; z<s; s<s; _≤_; z≤n; s≤s; _≤?_)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Decidable using (True; toWitness)
```


# Untyped is Uni-typed

Our development will be close to that in
Chapter [DeBruijn](/DeBruijn/),
save that every term will have exactly the same type, written `★`
and pronounced "any".
This matches a slogan introduced by Dana Scott
and echoed by Robert Harper: "Untyped is Uni-typed".
One consequence of this approach is that constructs which previously
had to be given separately (such as natural numbers and fixpoints)
can now be defined in the language itself.


# Syntax

First, we get all our infix declarations out of the way:

```agda
infix  4  _⊢_
infix  4  _∋_
infixl 5  _,_

infix  6  ƛ_
infix  6  ′_
infixl 7  _·_
```

# Types

We have just one type:

```agda
data Type : Set where
  ★ : Type
```

## Exercise (`Type≃⊤`) (practice)

Show that `Type` is isomorphic to `⊤`, the unit type.

```agda
-- Your code goes here
```

# Contexts

As before, a context is a list of types, with the type of the
most recently bound variable on the right:

```agda
data Context : Set where
  ∅   : Context
  _,_ : Context → Type → Context
```

We let `Γ` and `Δ` range over contexts.

## Exercise (`Context≃ℕ`) (practice)

Show that `Context` is isomorphic to `ℕ`.

```agda
-- Your code goes here
```

# Variables and the lookup judgment

Intrinsically-scoped variables correspond to the lookup judgment.  The
rules are as before:

```agda
data _∋_ : Context → Type → Set where

  Z : ∀ {Γ A}
     ---------
   → Γ , A ∋ A

  S_ : ∀ {Γ A B}
    → Γ ∋ A
      ---------
    → Γ , B ∋ A
```

We could write the rules with all instances of `A` and `B`
replaced by `★`, but arguably it is clearer not to do so.

Because `★` is the only type, the judgment doesn't guarantee anything
useful about types.  But it does ensure that all variables are in
scope.  For instance, we cannot use `S S Z` in a context that only
binds two variables.


# Terms and the scoping judgment

Intrinsically-scoped terms correspond to the typing judgment, but with
`★` as the only type.  The result is that we check that terms are
well scoped — that is, that all variables they mention are in scope —
but not that they are well typed:

```agda
data _⊢_ : Context → Type → Set where

  `_ : ∀ {Γ A}
    → Γ ∋ A
      -----
    → Γ ⊢ A

  ƛ_  :  ∀ {Γ}
    → Γ , ★ ⊢ ★
      ---------
    → Γ ⊢ ★

  _·_ : ∀ {Γ}
    → Γ ⊢ ★
    → Γ ⊢ ★
      ------
    → Γ ⊢ ★
```

Now we have a tiny calculus, with only variables, abstraction, and
application.  Below we will see how to encode naturals and
fixpoints into this calculus.

# Writing variables as numerals

As before, we can convert a natural to the corresponding de Bruijn
index.  We no longer need to lookup the type in the context, since
every variable has the same type:

```agda
size : Context → ℕ
size ∅        =  zero
size (Γ , _)  =  suc (size Γ)

count : ∀ {Γ} → {n : ℕ} → (p : n < size Γ) → Γ ∋ ★
count {Γ , ★} {zero}    (s≤s z≤n)  =  Z
count {Γ , ★} {(suc n)} (s≤s p)    =  S (count p)
```

We can then introduce a convenient abbreviation for variables:

```agda
#_ : ∀ {Γ}
  → (n : ℕ)
  → {n∈Γ : True (suc n ≤? size Γ)}
    --------------------------------
  → Γ ⊢ ★
#_ n {n∈Γ}  =  ` count (toWitness n∈Γ)
```

# Test examples

Our only example is computing two plus two on Church numerals:

```agda
twoᶜ : ∀ {Γ} → Γ ⊢ ★
twoᶜ = ƛ ƛ (# 1 · (# 1 · # 0))

fourᶜ : ∀ {Γ} → Γ ⊢ ★
fourᶜ = ƛ ƛ (# 1 · (# 1 · (# 1 · (# 1 · # 0))))

plusᶜ : ∀ {Γ} → Γ ⊢ ★
plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))

2+2ᶜ : ∅ ⊢ ★
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ
```

Before, reduction stopped when we reached a lambda term, so we had to
compute `` plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero `` to ensure we reduced
to a representation of the natural four.  Now, reduction continues
under lambda, so we don't need the extra arguments.  It is convenient
to define a term to represent four as a Church numeral, as well as
two.

# Renaming

Our definition of renaming is as before.  First, we need an extension lemma:

```agda
ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
    -----------------------------------
  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)
```

We could replace all instances of `A` and `B` by `★`, but arguably it is
clearer not to do so.

Now it is straightforward to define renaming:

```agda
rename : ∀ {Γ Δ}
  → (∀ {A} → Γ ∋ A → Δ ∋ A)
    ------------------------
  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (` x)          =  ` (ρ x)
rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
```

This is exactly as before, save that there are fewer term forms.

# Simultaneous substitution

Our definition of substitution is also exactly as before.
First we need an extension lemma:

```agda
exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
    ----------------------------------
  → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
exts σ Z      =  ` Z
exts σ (S x)  =  rename S_ (σ x)
```

Again, we could replace all instances of `A` and `B` by `★`.

Now it is straightforward to define substitution:

```agda
subst : ∀ {Γ Δ}
  → (∀ {A} → Γ ∋ A → Δ ⊢ A)
    ------------------------
  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
subst σ (` k)          =  σ k
subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
subst σ (L · M)        =  (subst σ L) · (subst σ M)
```

Again, this is exactly as before, save that there are fewer term forms.

# Single substitution

It is easy to define the special case of substitution for one free variable:

```agda
subst-zero : ∀ {Γ B} → (Γ ⊢ B) → ∀ {A} → (Γ , B ∋ A) → (Γ ⊢ A)
subst-zero M Z      =  M
subst-zero M (S x)  =  ` x

_[_] : ∀ {Γ A B}
        → Γ , B ⊢ A
        → Γ ⊢ B
          ---------
        → Γ ⊢ A
_[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} (subst-zero M) {A} N
```

# Neutral and normal terms

Reduction continues until a term is fully normalised.  Hence, instead
of values, we are now interested in _normal forms_.  Terms in normal
form are defined by mutual recursion with _neutral_ terms:

```agda
data Neutral : ∀ {Γ A} → Γ ⊢ A → Set
data Normal  : ∀ {Γ A} → Γ ⊢ A → Set
```

Neutral terms arise because we now consider reduction of open terms,
which may contain free variables.  A term is neutral if it is a
variable or a neutral term applied to a normal term:

```agda
data Neutral where

  `_  : ∀ {Γ A} (x : Γ ∋ A)
      -------------
    → Neutral (` x)

  _·_  : ∀ {Γ} {L M : Γ ⊢ ★}
    → Neutral L
    → Normal M
      ---------------
    → Neutral (L · M)
```

A term is a normal form if it is neutral or an abstraction where the
body is a normal form. We use `′_` to label neutral terms.
Like `` `_ ``, it is unobtrusive:

```agda
data Normal where

  ′_ : ∀ {Γ A} {M : Γ ⊢ A}
    → Neutral M
      ---------
    → Normal M

  ƛ_  : ∀ {Γ} {N : Γ , ★ ⊢ ★}
    → Normal N
      ------------
    → Normal (ƛ N)
```

We introduce a convenient abbreviation for evidence that a variable is neutral:

```agda
#′_ : ∀ {Γ} (n : ℕ) {n∈Γ : True (suc n ≤? size Γ)} → Neutral {Γ} (# n)
#′_ n {n∈Γ}  =  ` count (toWitness n∈Γ)
```

For example, here is the evidence that the Church numeral two is in
normal form:

```agda
_ : Normal (twoᶜ {∅})
_ = ƛ ƛ (′ #′ 1 · (′ #′ 1 · (′ #′ 0)))
```

The evidence that a term is in normal form is almost identical to
the term itself, decorated with some additional primes to indicate
neutral terms, and using `#′` in place of `#`


# Reduction step

The reduction rules are altered to switch from call-by-value to
call-by-name and to enable full normalisation:

* The rule `ξ₁` remains the same as it was for the simply-typed
  lambda calculus.

* In rule `ξ₂`, the requirement that the term `L` is a value
  is dropped. So this rule can overlap with `ξ₁` and
  reduction is _non-deterministic_. One can choose to reduce
  a term inside either `L` or `M`.

* In rule `β`, the requirement that the argument is a value
  is dropped, corresponding to call-by-name evaluation.
  This introduces further non-determinism, as `β` overlaps
  with `ξ₂` when there are redexes in the argument.

* A new rule `ζ` is added, to enable reduction underneath a lambda.

Here are the formalised rules:

```agda
infix 2 _—→_

data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

  ξ₁ : ∀ {Γ} {L L′ M : Γ ⊢ ★}
    → L —→ L′
      ----------------
    → L · M —→ L′ · M

  ξ₂ : ∀ {Γ} {L M M′ : Γ ⊢ ★}
    → M —→ M′
      ----------------
    → L · M —→ L · M′

  β : ∀ {Γ} {N : Γ , ★ ⊢ ★} {M : Γ ⊢ ★}
      ---------------------------------
    → (ƛ N) · M —→ N [ M ]

  ζ : ∀ {Γ} {N N′ : Γ , ★ ⊢ ★}
    → N —→ N′
      -----------
    → ƛ N —→ ƛ N′
```

## Exercise (`variant-1`) (practice)

How would the rules change if we want call-by-value where terms
normalise completely?  Assume that `β` should not permit reduction
unless both terms are in normal form.

```agda
-- Your code goes here
```

## Exercise (`variant-2`) (practice)

How would the rules change if we want call-by-value where terms
do not reduce underneath lambda?  Assume that `β`
permits reduction when both terms are values (that is, lambda
abstractions).  What would `2+2ᶜ` reduce to in this case?

```agda
-- Your code goes here
```


# Reflexive and transitive closure

We cut-and-paste the previous definition:

```agda
infix  2 _—↠_
infix  1 begin_
infixr 2 _—→⟨_⟩_
infix  3 _∎

data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where

  _∎ : (M : Γ ⊢ A)
      ------
    → M —↠ M

  step—→ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
    → M —↠ N
    → L —→ M
      ------
    → L —↠ N

pattern _—→⟨_⟩_ L L—→M M—↠N = step—→ L M—↠N L—→M

begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
  → M —↠ N
    ------
  → M —↠ N
begin M—↠N = M—↠N
```


# Example reduction sequence

Here is the demonstration that two plus two is four:

```agda
_ : 2+2ᶜ —↠ fourᶜ
_ =
  begin
    plusᶜ · twoᶜ · twoᶜ
  —→⟨ ξ₁ β ⟩
    (ƛ ƛ ƛ twoᶜ · # 1 · (# 2 · # 1 · # 0)) · twoᶜ
  —→⟨ β ⟩
    ƛ ƛ twoᶜ · # 1 · (twoᶜ · # 1 · # 0)
  —→⟨ ζ (ζ (ξ₁ β)) ⟩
    ƛ ƛ ((ƛ # 2 · (# 2 · # 0)) · (twoᶜ · # 1 · # 0))
  —→⟨ ζ (ζ β) ⟩
    ƛ ƛ # 1 · (# 1 · (twoᶜ · # 1 · # 0))
  —→⟨ ζ (ζ (ξ₂ (ξ₂ (ξ₁ β)))) ⟩
    ƛ ƛ # 1 · (# 1 · ((ƛ # 2 · (# 2 · # 0)) · # 0))
  —→⟨ ζ (ζ (ξ₂ (ξ₂ β))) ⟩
   ƛ (ƛ # 1 · (# 1 · (# 1 · (# 1 · # 0))))
  ∎
```

After just two steps the top-level term is an abstraction,
and `ζ` rules drive the rest of the normalisation.


# Progress

Progress adapts.  Instead of claiming that every term either is a value
or takes a reduction step, we claim that every term is either in normal
form or takes a reduction step.

Previously, progress only applied to closed, well-typed terms.  We had
to rule out terms where we apply something other than a function (such
as `` `zero ``) or terms with a free variable.  Now we can demonstrate
it for open, well-scoped terms.  The definition of normal form permits
free variables, and we have no terms that are not functions.

A term makes progress if it can take a step or is in normal form:

```agda
data Progress {Γ A} (M : Γ ⊢ A) : Set where

  step : ∀ {N : Γ ⊢ A}
    → M —→ N
      ----------
    → Progress M

  done :
      Normal M
      ----------
    → Progress M
```

If a term is well scoped then it satisfies progress:

```agda
progress : ∀ {Γ A} → (M : Γ ⊢ A) → Progress M
progress (` x)                                 =  done (′ ` x)
progress (ƛ N)  with  progress N
... | step N—→N′                               =  step (ζ N—→N′)
... | done NrmN                                =  done (ƛ NrmN)
progress (` x · M) with progress M
... | step M—→M′                               =  step (ξ₂ M—→M′)
... | done NrmM                                =  done (′ (` x) · NrmM)
progress ((ƛ N) · M)                           =  step β
progress (L@(_ · _) · M) with progress L
... | step L—→L′                               =  step (ξ₁ L—→L′)
... | done (′ NeuL) with progress M
...    | step M—→M′                            =  step (ξ₂ M—→M′)
...    | done NrmM                             =  done (′ NeuL · NrmM)
```

We induct on the evidence that the term is well scoped:

* If the term is a variable, then it is in normal form.
  (This contrasts with previous proofs, where the variable case was
  ruled out by the restriction to closed terms.)
* If the term is an abstraction, recursively invoke progress on the body.
  (This contrast with previous proofs, where an abstraction is
  immediately a value.):
  + If it steps, then the whole term steps via `ζ`.
  + If it is in normal form, then so is the whole term.
* If the term is an application, consider the function subterm:
  + If it is a variable, recursively invoke progress on the argument:
    - If it steps, then the whole term steps via `ξ₂`;
    - If it is normal, then so is the whole term.
  + If it is an abstraction, then the whole term steps via `β`.
  + If it is an application, recursively apply progress to the function subterm:
    - If it steps, then the whole term steps via `ξ₁`.
    - If it is normal, recursively apply progress to the argument subterm:
      * If it steps, then the whole term steps via `ξ₂`.
      * If it is normal, then so is the whole term.

The final equation for progress uses an _at pattern_ of the form `P@Q`,
which matches only if both pattern `P` and pattern `Q` match.  Character
`@` is one of the few that Agda doesn't allow in names, so spaces are not
required around it.  In this case, the pattern ensures that `L` is an
application.

# Evaluation

As previously, progress immediately yields an evaluator.

We relate gas to the number of steps in a reduction sequence.

```agda
length : ∀ {Γ A} {M N : Γ ⊢ A} → M —↠ N → ℕ
length (M ∎)                =  zero
length (L —→⟨ L—→M ⟩ M—↠N)  =  suc (length M—↠N)
```

If the evaluator runs out of gas it returns a sequence
of length equal to the amount of gas, while if it terminates in returns
a sequence of length less than the amount of gas and ending in a
normal form.

```agda
data Eval {Γ A} (M : Γ ⊢ A) (g : ℕ) : Set where

  out-of-gas : {N : Γ ⊢ A}
    → (M—↠N : M —↠ N)
    → length M—↠N ≡ g
      ---------------
    → Eval M g

  terminates : {N : Γ ⊢ A}
    → (M—↠N : M —↠ N)
    → length M—↠N < g
    → Normal N
      ---------------
    → Eval M g
```

The evaluator takes gas and a term and returns the corresponding steps.

```agda
eval : ∀ {Γ A}
  → (g : ℕ)
  → (L : Γ ⊢ A)
    ---------
  → Eval L g
eval zero L            =  out-of-gas (L ∎) refl
eval (suc g) L with progress L
... | done VL                  =  terminates (L ∎) z<s VL
... | step {M} L—→M with eval g M
...   | out-of-gas M—↠N ≡g     =  out-of-gas (L —→⟨ L—→M ⟩ M—↠N) (cong suc ≡g)
...   | terminates M—↠N <g VN  =  terminates (L —→⟨ L—→M ⟩ M—↠N) (s<s <g) VN
```

The definition is as before, save that the empty context `∅`
generalises to an arbitrary context `Γ`.

# Example

We reiterate our previous example. Two plus two is four, with Church numerals:

```agda
_ : eval 100 2+2ᶜ ≡
  terminates
   ((ƛ
     (ƛ
      (ƛ
       (ƛ
        (` (S (S (S Z)))) · (` (S Z)) ·
        ((` (S (S Z))) · (` (S Z)) · (` Z))))))
    · (ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z))))
    · (ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z))))
   —→⟨ ξ₁ β ⟩
    (ƛ
     (ƛ
      (ƛ
       (ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z)))) · (` (S Z)) ·
       ((` (S (S Z))) · (` (S Z)) · (` Z)))))
    · (ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z))))
   —→⟨ β ⟩
    ƛ
    (ƛ
     (ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z)))) · (` (S Z)) ·
     ((ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z)))) · (` (S Z)) · (` Z)))
   —→⟨ ζ (ζ (ξ₁ β)) ⟩
    ƛ
    (ƛ
     (ƛ (` (S (S Z))) · ((` (S (S Z))) · (` Z))) ·
     ((ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z)))) · (` (S Z)) · (` Z)))
   —→⟨ ζ (ζ β) ⟩
    ƛ
    (ƛ
     (` (S Z)) ·
     ((` (S Z)) ·
      ((ƛ (ƛ (` (S Z)) · ((` (S Z)) · (` Z)))) · (` (S Z)) · (` Z))))
   —→⟨ ζ (ζ (ξ₂ (ξ₂ (ξ₁ β)))) ⟩
    ƛ
    (ƛ
     (` (S Z)) ·
     ((` (S Z)) ·
      ((ƛ (` (S (S Z))) · ((` (S (S Z))) · (` Z))) · (` Z))))
   —→⟨ ζ (ζ (ξ₂ (ξ₂ β))) ⟩
    ƛ (ƛ (` (S Z)) · ((` (S Z)) · ((` (S Z)) · ((` (S Z)) · (` Z)))))
   ∎)
   (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))
   (ƛ
    (ƛ
     (′
      (` (S Z)) ·
      (′ (` (S Z)) · (′ (` (S Z)) · (′ (` (S Z)) · (′ (` Z))))))))
_ = refl
```

# Naturals and fixpoint

We could simulate naturals using Church numerals, but computing
predecessor is tricky and expensive.  Instead, we use a different
representation, called Scott numerals, where a number is essentially
defined by the expression that corresponds to its own case statement.

Recall that Church numerals apply a given function for the
corresponding number of times.  Using named terms, we represent the
first three Church numerals as follows:

    zero  =  ƛ s ⇒ ƛ z ⇒ z
    one   =  ƛ s ⇒ ƛ z ⇒ s · z
    two   =  ƛ s ⇒ ƛ z ⇒ s · (s · z)

In contrast, for Scott numerals, we represent the first three naturals
as follows:

    zero = ƛ s ⇒ ƛ z ⇒ z
    one  = ƛ s ⇒ ƛ z ⇒ s · zero
    two  = ƛ s ⇒ ƛ z ⇒ s · one

Each representation expects two arguments, one corresponding to
the successor branch of the case (it expects an additional argument,
the predecessor of the current argument) and one corresponding to the
zero branch of the case.  (The cases could be in either order.
We put the successor case first to ease comparison with Church numerals.)

Here is the Scott representation of naturals encoded with de Bruijn indexes:

```agda
`zero : ∀ {Γ} → (Γ ⊢ ★)
`zero = ƛ ƛ (# 0)

`suc_ : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★)
`suc_ M  = (ƛ ƛ ƛ (# 1 · # 2)) · M

case : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★) → (Γ , ★ ⊢ ★)  → (Γ ⊢ ★)
case L M N = L · (ƛ N) · M
```

Here we have been careful to retain the exact form of our previous
definitions.  The successor branch expects an additional variable to
be in scope (as indicated by its type), so it is converted to an
ordinary term using lambda abstraction.

Applying successor to the zero indeed reduces to the Scott numeral
for one.

```agda
_ : eval 100 (`suc_ {∅} `zero) ≡
    terminates
        ((ƛ (ƛ (ƛ # 1 · # 2))) · (ƛ (ƛ # 0))
    —→⟨ β ⟩
         ƛ (ƛ # 1 · (ƛ (ƛ # 0)))
    ∎)
    (s≤s (s≤s z≤n))
    (ƛ (ƛ (′ (` (S Z)) · (ƛ (ƛ (′ (` Z)))))))
_ = refl
```

We can also define fixpoint.  Using named terms, we define:

    μ f = (ƛ x ⇒ f · (x · x)) · (ƛ x ⇒ f · (x · x))

This works because:

      μ f
    ≡
      (ƛ x ⇒ f · (x · x)) · (ƛ x ⇒ f · (x · x))
    —→
      f · ((ƛ x ⇒ f · (x · x)) · (ƛ x ⇒ f · (x · x)))
    ≡
      f · (μ f)

With de Bruijn indices, we have the following:

```agda
μ_ : ∀ {Γ} → (Γ , ★ ⊢ ★) → (Γ ⊢ ★)
μ N  =  (ƛ ((ƛ (# 1 · (# 0 · # 0))) · (ƛ (# 1 · (# 0 · # 0))))) · (ƛ N)
```

The argument to fixpoint is treated similarly to the successor branch of case.

We can now define two plus two exactly as before:

```agda
infix 5 μ_

two : ∀ {Γ} → Γ ⊢ ★
two = `suc `suc `zero

four : ∀ {Γ} → Γ ⊢ ★
four = `suc `suc `suc `suc `zero

plus : ∀ {Γ} → Γ ⊢ ★
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
```

Because `` `suc `` is now a defined term rather than primitive,
it is no longer the case that `plus · two · two` reduces to `four`,
but they do both reduce to the same normal term.


## Exercise `plus-eval` (practice)

Use the evaluator to confirm that `plus · two · two` and `four`
normalise to the same term.

```agda
-- Your code goes here
```

## Exercise `multiplication-untyped` (recommended)

Use the encodings above to translate your definition of
multiplication from previous chapters with the Scott
representation and the encoding of the fixpoint operator.
Confirm that two times two is four.

```agda
-- Your code goes here
```

## Exercise `encode-more` (stretch)

Along the lines above, encode all of the constructs of
Chapter [More](/More/),
save for primitive numbers, in the untyped lambda calculus.

```agda
-- Your code goes here
```


# Multi-step reduction is transitive

In our formulation of the reflexive transitive closure of reduction,
i.e., the `—↠` relation, there is not an explicit rule for
transitivity. Instead the relation mimics the structure of lists by
providing a case for an empty reduction sequence and a case for adding
one reduction to the front of a reduction sequence.  The following is
the proof of transitivity, which has the same structure as the append
function `_++_` on lists.

```agda
—↠-trans : ∀{Γ}{A}{L M N : Γ ⊢ A}
         → L —↠ M
         → M —↠ N
         → L —↠ N
—↠-trans (M ∎) mn = mn
—↠-trans (L —→⟨ r ⟩ lm) mn = L —→⟨ r ⟩ (—↠-trans lm mn)
```

The following notation makes it convenient to employ
transitivity of `—↠`.

```agda
infixr 2 _—↠⟨_⟩_

_—↠⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
    → L —↠ M
    → M —↠ N
      ---------
    → L —↠ N
L —↠⟨ L—↠M ⟩ M—↠N = —↠-trans L—↠M M—↠N
```

# Multi-step reduction is a congruence

Recall from Chapter [Induction](/Induction/) that a
relation `R` is a _congruence_ for a given function `f` if it is
preserved by that function, i.e., if `R x y` then `R (f x) (f y)`.
The term constructors `ƛ_` and `_·_` are functions, and so
the notion of congruence applies to them as well. Furthermore, when a
relation is a congruence for all of the term constructors, we
say that the relation is a congruence for the language in question, in
this case the untyped lambda calculus.

The rules `ξ₁`, `ξ₂`, and `ζ` ensure that the reduction relation is a
congruence for the untyped lambda calculus. The multi-step reduction
relation `—↠` is also a congruence, which we prove in the following
three lemmas.

```agda
appL-cong : ∀ {Γ} {L L' M : Γ ⊢ ★}
         → L —↠ L'
           ---------------
         → L · M —↠ L' · M
appL-cong {Γ}{L}{L'}{M} (L ∎) = L · M ∎
appL-cong {Γ}{L}{L'}{M} (L —→⟨ r ⟩ rs) = L · M —→⟨ ξ₁ r ⟩ appL-cong rs
```

The proof of `appL-cong` is by induction on the reduction sequence `L —↠ L'`.
* Suppose `L —↠ L` by `L ∎`. Then we have
  `L · M —↠ L · M` by `L · M ∎`.
* Suppose `L —↠ L''` by `L —→⟨ r ⟩ rs`, so
  `L —→ L'` by `r` and `L' —↠ L''` by `rs`.
  We have `L · M —→ L' · M` by `ξ₁ r` and
  `L' · M —↠ L'' · M` by the induction hypothesis applied to `rs`.
  We conclude that ``L · M —↠ L'' · M`` by putting these two
  facts together using `_—→⟨_⟩_`.

The proofs of `appR-cong` and `abs-cong` follow the same pattern as
the proof for `appL-cong`.

```agda
appR-cong : ∀ {Γ} {L M M' : Γ ⊢ ★}
         → M —↠ M'
           ---------------
         → L · M —↠ L · M'
appR-cong {Γ}{L}{M}{M'} (M ∎) = L · M ∎
appR-cong {Γ}{L}{M}{M'} (M —→⟨ r ⟩ rs) = L · M —→⟨ ξ₂ r ⟩ appR-cong rs
```

```agda
abs-cong : ∀ {Γ} {N N' : Γ , ★ ⊢ ★}
         → N —↠ N'
           ----------
         → ƛ N —↠ ƛ N'
abs-cong (M ∎) = ƛ M ∎
abs-cong (L —→⟨ r ⟩ rs) = ƛ L —→⟨ ζ r ⟩ abs-cong rs
```

# Unicode

This chapter uses the following unicode:

    ★  U+2605  BLACK STAR (\st)

The `\st` command permits navigation among many different stars;
the one we use is number 7.
