PCF with nested evaluation contexts

Philip Wadler, 2 Aug 2022

```agda
module variants.Evaluation where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ; ∃; Σ-syntax; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
open import Relation.Binary.PropositionalEquality
     using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app; subst; inspect)
     renaming ([_] to [[_]])
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)
```

## Types

```agda
infixr 7 _⇒_
infix  8 `ℕ

data Type : Set where
  `ℕ : Type
  _⇒_ : Type → Type → Type

variable
  A B C : Type
```

* Type environments

```agda
infixl 6 _▷_

data Env : Set where
  ∅   : Env
  _▷_ : Env → Type → Env

variable
  Γ Δ : Env

infix  4 _∋_
infix  9 S_

data _∋_ : Env → Type → Set where

  Z :
      Γ ▷ A ∋ A

  S_ :
      Γ ∋ A
      ---------
    → Γ ▷ B ∋ A

variable
  x y : Γ ∋ A
```

## Terms

```agda
infix  4  _⊢_
infix  5  ƛ_
infix  5  μ_
infixl 6  _·_
infix  7  `suc_
infix  8  `_

data _⊢_ : Env → Type → Set where

  `_ :
      Γ ∋ A
      -----
    → Γ ⊢ A

  ƛ_ :
      Γ ▷ A ⊢ B
      ---------
    → Γ ⊢ A ⇒ B

  _·_ :
      Γ ⊢ A ⇒ B
    → Γ ⊢ A
      ---------
    → Γ ⊢ B

  `zero :
      ------
      Γ ⊢ `ℕ

  `suc_ :
      Γ ⊢ `ℕ
      ------
    → Γ ⊢ `ℕ

  case :
      Γ ⊢ `ℕ
    → Γ ⊢ A
    → Γ ▷ `ℕ ⊢ A
      -----------
    → Γ ⊢ A

  μ_ :
     Γ ▷ A ⊢ A
     ---------
   → Γ ⊢ A

variable
  L M N V W : Γ ⊢ A
```

## Renaming maps, substitution maps, term maps

```agda
_→ᴿ_ : Env → Env → Set
Γ →ᴿ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A

_→ˢ_ : Env → Env → Set
Γ →ˢ Δ = ∀ {A} → Γ ∋ A → Δ ⊢ A

_→ᵀ_ : Env → Env → Set
Γ →ᵀ Δ = ∀ {A} → Γ ⊢ A → Δ ⊢ A

variable
  ρ : Γ →ᴿ Δ
  σ : Γ →ˢ Δ
  θ : Γ →ᵀ Δ
```


## Renaming

```agda
ren▷ :
    (Γ →ᴿ Δ)
    ------------------
  → (Γ ▷ A) →ᴿ (Δ ▷ A)
ren▷ ρ Z      =  Z
ren▷ ρ (S x)  =  S (ρ x)

ren :
    (Γ →ᴿ Δ)
    --------
  → (Γ →ᵀ Δ)
ren ρ (` x)          =  ` (ρ x)
ren ρ (ƛ N)          =  ƛ (ren (ren▷ ρ) N)
ren ρ (L · M)        =  (ren ρ L) · (ren ρ M)
ren ρ `zero          =  `zero
ren ρ (`suc M)       =  `suc (ren ρ M)
ren ρ (case L M N)   =  case (ren ρ L) (ren ρ M) (ren (ren▷ ρ) N)
ren ρ (μ M)          =  μ (ren (ren▷ ρ) M)

lift : Γ →ᵀ (Γ ▷ A)
lift = ren S_
```

## Substitution

```agda
sub▷ :
    (Γ →ˢ Δ)
    ------------------
  → (Γ ▷ A) →ˢ (Δ ▷ A)
sub▷ σ Z      =  ` Z
sub▷ σ (S x)  =  lift (σ x)

sub :
    (Γ →ˢ Δ)
    --------
  → (Γ →ᵀ Δ)
sub σ (` x)          =  σ x
sub σ (ƛ N)          =  ƛ (sub (sub▷ σ) N)
sub σ (L · M)        =  (sub σ L) · (sub σ M)
sub σ `zero          =  `zero
sub σ (`suc M)       =  `suc (sub σ M)
sub σ (case L M N)   =  case (sub σ L) (sub σ M) (sub (sub▷ σ) N)
sub σ (μ M)          =  μ (sub (sub▷ σ) M)
```

Special case of substitution, used in beta rule

```agda
σ₀ :
    Γ ⊢ A
    ------------
  → (Γ ▷ A) →ˢ Γ
σ₀ M Z      =  M
σ₀ M (S x)  =  ` x

_[_] :
    Γ ▷ A ⊢ B
  → Γ ⊢ A
    ---------
  → Γ ⊢ B
_[_] N M =  sub (σ₀ M) N
```

## Values

```agda
data Value : (Γ ⊢ A) → Set where

  ƛ_ :
      (N : Γ ▷ A ⊢ B)
      ---------------
    → Value (ƛ N)

  `zero :
      Value {Γ} `zero

  `suc_ :
      Value V
      --------------
    → Value (`suc V)

  μ_ :
      (N : Γ ▷ A ⊢ A)
      ---------------
    → Value (μ N)

variable
  v : Value V
  w : Value W
```


Extract term from evidence that it is a value.

```agda
value : ∀ {Γ A} {V : Γ ⊢ A}
  → (v : Value V)
    -------------
  → Γ ⊢ A
value {V = V} v  =  V
```


Renaming preserves values
(not needed, but I wanted to check that automatic generalisation works)

```agda
ren-val :
    (ρ : Γ →ᴿ Δ)
  → Value V
    ------------------
  → Value (ren ρ V)
-- ren-val ρ (ƛ N)    =

ren-val ρ (ƛ N)     = ƛ (ren (ren▷ ρ) N)
ren-val ρ `zero     = `zero
ren-val ρ (`suc M)  = `suc (ren-val ρ M)
ren-val ρ (μ M)     = μ (ren (ren▷ ρ) M)
```

## Evaluation contexts

```agda
infix  6 [_]·_
infix  6 _·[_]
infix  7 `suc[_]
infix  7 case[_]
infix  9 _⟦_⟧

data _⊢_=>_ : Env → Type → Type → Set where

  □ : Γ ⊢ C => C

  [_]·_ :
      Γ ⊢ C => (A ⇒ B)
    → Γ ⊢ A
      ---------------
    → Γ ⊢ C => B

  _·[_] :
      {V : Γ ⊢ A ⇒ B}
    → Value V
    → Γ ⊢ C => A
      ----------------
    → Γ ⊢ C => B

  `suc[_] :
      Γ ⊢ C => `ℕ
      -----------
    → Γ ⊢ C => `ℕ

  case[_] :
      Γ ⊢ C => `ℕ
    → Γ ⊢ A
    → Γ ▷ `ℕ ⊢ A
      -----------
    → Γ ⊢ C => A
```

The plug function inserts an expression into the hole of a frame.

```agda
_⟦_⟧ :
    Γ ⊢ A => B
  → Γ ⊢ A
    ----------
  → Γ ⊢ B
□ ⟦ M ⟧                 =  M
([ E ]· M) ⟦ L ⟧        =  E ⟦ L ⟧ · M
(v ·[ E ]) ⟦ M ⟧        =  value v · E ⟦ M ⟧
(`suc[ E ]) ⟦ M ⟧       =  `suc (E ⟦ M ⟧)
(case[ E ] M N) ⟦ L ⟧   =  case (E ⟦ L ⟧) M N
```

Composition of two frames

```agda
_∘_ :
    Γ ⊢ B => C
  → Γ ⊢ A => B
    ----------
  → Γ ⊢ A => C
□ ∘ F                 =  F
([ E ]· M) ∘ F        =  [ E ∘ F ]· M
(v ·[ E ]) ∘ F        =  v ·[ E ∘ F ]
(`suc[ E ]) ∘ F       =  `suc[ E ∘ F ]
(case[ E ] M N) ∘ F   =  case[ E ∘ F ] M N
```

Composition and plugging

```agda
∘-lemma :
    (E : Γ ⊢ B => C)
  → (F : Γ ⊢ A => B)
  → (P : Γ ⊢ A)
    -----------------------------
  → E ⟦ F ⟦ P ⟧ ⟧ ≡ (E ∘ F) ⟦ P ⟧
∘-lemma □ F P                                         =  refl
∘-lemma ([ E ]· M) F P         rewrite ∘-lemma E F P  =  refl
∘-lemma (v ·[ E ]) F P         rewrite ∘-lemma E F P  =  refl
∘-lemma (`suc[ E ]) F P        rewrite ∘-lemma E F P  =  refl
∘-lemma (case[ E ] M N) F P    rewrite ∘-lemma E F P  =  refl
```

## Reduction

```agda
infix 2 _↦_ _—→_

data _↦_ : (Γ ⊢ A) → (Γ ⊢ A) → Set where

  β-ƛ :
      Value V
      --------------------
    → (ƛ N) · V ↦ N [ V ]

  β-zero :
      ------------------
      case `zero M N ↦ M

  β-suc :
      Value V
      ---------------------------
    → case (`suc V) M N ↦ N [ V ]

  μ-· :
     Value V
     -------------------------
   → (μ N) · V ↦ (N [ μ N ]) · V

  μ-case :
     -------------------------------------
     case (μ L) M N ↦ case (L [ μ L ]) M N

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

  ξ-refl :
      {M′ N′ : Γ ⊢ B}
    → (E : Γ ⊢ A => B)
    → M′ ≡ E ⟦ M ⟧
    → N′ ≡ E ⟦ N ⟧
    → M ↦ N
      --------
    → M′ —→ N′
```

Notation

```agda
pattern ξ E M—→N = ξ-refl E refl refl M—→N
```

## Reflexive and transitive closure of reduction

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

data _—↠_ : Γ ⊢ A → Γ ⊢ A → Set where

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

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

begin_ : (M —↠ N) → (M —↠ N)
begin M—↠N = M—↠N
```

## Irreducible terms

Values are irreducible.  The auxiliary definition rearranges the
order of the arguments because it works better for Agda.

```agda
value-irreducible : Value V → ¬ (V —→ M)
value-irreducible v V—→M  =  nope V—→M v
  where
  nope : V —→ M → Value V → ⊥
  nope (ξ □ (β-ƛ v)) ()
  nope (ξ `suc[ E ] V—→M) (`suc w)  =  nope (ξ E V—→M) w
```

Variables are irreducible.

```agda
variable-irreducible :
    ------------
    ¬ (` x —→ N)
variable-irreducible (ξ □ ())
```

## Progress

Every term that is well typed and closed is either
blame or a value or takes a reduction step.

```agda
data Progress : (∅ ⊢ A) → Set where

  step :
      L —→ M
      ----------
    → Progress L

  done :
      Value V
      ----------
    → Progress V

progress :
    (M : ∅ ⊢ A)
    -----------
  → Progress M

progress (ƛ N)                           =  done (ƛ N)
progress (L · M) with progress L
... | step (ξ E L↦L′)                    =  step (ξ ([ E ]· M) L↦L′)
... | done v with progress M
...     | step (ξ E M↦M′)                =  step (ξ (v ·[ E ]) M↦M′)
...     | done w with v
...         | (ƛ N)                      =  step (ξ □ (β-ƛ w))
...         | (μ N)                      =  step (ξ □ (μ-· w))
progress `zero                           =  done `zero
progress (`suc M) with progress M
... | step (ξ E M↦M′)                    =  step (ξ (`suc[ E ]) M↦M′)
... | done v                             =  done (`suc v)
progress (case L M N) with progress L
... | step (ξ E L↦L′)                    =  step (ξ (case[ E ] M N) L↦L′)
... | done v with v
...     | `zero                          =  step (ξ □ β-zero)
...     | (`suc v)                       =  step (ξ □ (β-suc v))
...     | (μ N)                          =  step (ξ □ μ-case)
progress (μ N)                           =  done (μ N)
```


## Evaluation

Gas is specified by a natural number:

```agda
record Gas : Set where
  constructor gas
  field
    amount : ℕ
```

When our evaluator returns a term `N`, it will either give evidence that
`N` is a value, or indicate that blame occurred or it ran out of gas.

```agda
data Finished : (∅ ⊢ A) → Set where

   done :
       Value N
       ----------
     → Finished N

   out-of-gas :
       ----------
       Finished N
```

Given a term `L` of type `A`, the evaluator will, for some `N`, return
a reduction sequence from `L` to `N` and an indication of whether
reduction finished:

```agda
data Steps : ∅ ⊢ A → Set where

  steps :
      L —↠ M
    → Finished M
      ----------
    → Steps L
```

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

```agda
eval :
    Gas
  → (L : ∅ ⊢ A)
    -----------
  → Steps L
eval (gas zero) L          =  steps (L ∎) out-of-gas
eval (gas (suc m)) L
    with progress L
... | done v               =  steps (L ∎) (done v)
... | step {M = M} L—→M
    with eval (gas m) M
... | steps M—↠N fin       =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
```

# Example

Computing two plus two on naturals:

```agda
pattern two = `suc `suc `zero

pattern x′ = ` S Z
pattern y′ = ` Z
pattern p′ = ` S S S Z
pattern x″ = ` Z
pattern y″ = ` S Z
pattern plus = μ ƛ ƛ (case x′ y′ (`suc (p′ · x″ · y″)))
```

Next, a sample reduction demonstrating that two plus two is four:

```agda
_ : plus · two · two —↠ `suc `suc `suc `suc (`zero {∅})
_ = begin
      plus · two · two
    —→⟨ ξ ([ □ ]· two) (μ-· two) ⟩
      (ƛ (ƛ case y″ x″ (`suc (plus · x″ · y″)))) · two · two
    —→⟨ ξ ([ □ ]· two) (β-ƛ two) ⟩
      (ƛ case two x″ (`suc (plus · x″ · y″))) · two
    —→⟨ ξ □ (β-ƛ two) ⟩
      case two two (`suc (plus · x″ · two))
    —→⟨ ξ □ (β-suc (`suc `zero)) ⟩
      `suc (plus · `suc `zero · two)
    —→⟨ ξ `suc[ [ □ ]· two ] (μ-· (`suc `zero)) ⟩
      `suc ((ƛ (ƛ case y″ x″ (`suc (plus · x″ · y″)))) · `suc `zero · two)
    —→⟨ ξ `suc[ [ □ ]· two ] (β-ƛ (`suc `zero)) ⟩
      `suc ((ƛ case (`suc `zero) x″ (`suc (plus · x″ · y″))) · two)
    —→⟨ ξ `suc[ □ ] (β-ƛ two) ⟩
      `suc case (`suc `zero) two (`suc (plus · x″ · two))
    —→⟨ ξ `suc[ □ ] (β-suc `zero) ⟩
      `suc (`suc (plus · `zero · two))
    —→⟨ ξ `suc[ `suc[ [ □ ]· two ] ] (μ-· `zero) ⟩
      `suc (`suc ((ƛ (ƛ case y″ x″ (`suc (plus · x″ · y″)))) · `zero · two))
    —→⟨ ξ `suc[ `suc[ [ □ ]· two ] ] (β-ƛ `zero) ⟩
      `suc (`suc ((ƛ case `zero x″ (`suc (plus · x″ · y″))) · two))
    —→⟨ ξ `suc[ `suc[ □ ] ] (β-ƛ two) ⟩
      `suc (`suc case `zero two (`suc (plus · x″ · two)))
    —→⟨ ξ `suc[ `suc[ □ ] ] β-zero ⟩
      `suc (`suc two)
    ∎
```
