Siek, Thiemann, and Wadler 10 November 2022

module Eval where

open import Data.Nat using (; zero; suc)
open import Data.Unit using (; tt)
open import Data.Empty using (; ⊥-elim)
open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ; ; Σ-syntax; ∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (¬_)

Types

infixr 7 _⇒_
infix  8 `ℕ

data Type : Set where
  `ℕ : Type
  _⇒_ : Type  Type  Type
  • Contexts and Variables
infixl 6 _▷_

data Context : Set where
     : Context
  _▷_ : Context  Type  Context

infix  4 _∋_
infix  9 S_

data _∋_ : Context  Type  Set where

  Z :  {Γ A}
      ----------
     Γ  A  A

  S_ :  {Γ A B}
     Γ  A
      ---------
     Γ  B  A

Terms

infix  4 _⊢_
infixl 6 _·_
infix  8 `_

data _⊢_ : Context  Type  Set where

  `_ :  {Γ A}
     Γ  A
      -----
     Γ  A

  ƛ_  :  {Γ A B}
     Γ  A  B
      ---------
     Γ  A  B

  _·_ :  {Γ A B}
     Γ  A  B
     Γ  A
      ---------
     Γ  B

  `zero :  {Γ}
      ---------
     Γ  `ℕ

  `suc_ :  {Γ}
     Γ  `ℕ
      ------
     Γ  `ℕ

  case :  {Γ A}
     Γ  `ℕ
     Γ  A
     Γ  `ℕ  A
      ----------
     Γ  A

  μ_ :  {Γ A}
     Γ  A  A
      ---------
     Γ  A

Test examples

First, computing two plus two on naturals:
pattern two = `suc `suc `zero
pattern plus = μ ƛ ƛ (case (` S Z) (` Z) (`suc (` S S S Z · ` Z · ` S Z)))

2+2 :   `ℕ
2+2 = plus · two · two
Next, computing two plus two on Church numerals:
pattern twoᶜ = ƛ ƛ (` S Z · (` S Z · ` Z))
pattern plusᶜ = ƛ ƛ ƛ ƛ (` S S S Z · ` S Z · (` S S Z · ` S Z · ` Z))
pattern sucᶜ = ƛ `suc (` Z)

2+2ᶜ :   `ℕ
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero

Renaming maps, substitution maps, term maps

_→ʳ_ : Context  Context  Set
Γ →ʳ Δ =  {A}  Γ  A  Δ  A

_→ˢ_ : Context  Context  Set
Γ →ˢ Δ =  {A}  Γ  A  Δ  A

_→ᵗ_ : Context  Context  Set
Γ →ᵗ Δ =  {A}  Γ  A  Δ  A

Renaming

Extension of renaming maps
ren▷ :  {Γ Δ A}
   (Γ →ʳ Δ)
    ----------------------------
   ((Γ  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 ρ (μ N)          = μ (ren (ren▷ ρ) N)

lift :  {Γ : Context} {A : Type}  Γ →ᵗ (Γ  A)
lift = ren S_

Substitution

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

sub :  {Γ Δ : Context}
   (Γ →ˢ Δ)
    --------
   (Γ →ᵗ Δ)
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 ρ (μ N)          = μ (sub (sub▷ ρ) N)
Special case of substitution, used in beta rule
σ₀ :  {Γ A}  (M : Γ  A)  (Γ  A) →ˢ Γ
σ₀ M Z      =  M
σ₀ M (S x)  =  ` x

_[_] :  {Γ A B}
         Γ  A  B
         Γ  A
          ---------
         Γ  B
_[_] {Γ} {A} N M =  sub {Γ  A} {Γ} (σ₀ M) N

Values

data Value {Γ} :  {A}  Γ  A  Set where

  ƛ_ : ∀{A B}
     (N : Γ  A  B)
      ---------------
     Value (ƛ N)

  `zero :
      -----------
      Value `zero

  `suc_ :  {V : Γ  `ℕ}
     Value V
      --------------
     Value (`suc V)
Extract term from evidence that it is a value.
value :  {Γ A} {V : Γ  A}
   (v : Value V)
    -------------
   Γ  A
value {V = V} v  =  V

Frames (aka Evaluation Contexts)

Here is how evaluation contexts are written informally:

E ::= □ | E · M | V · E | `suc E | `case E M N

M —→ M′
------------- ξ
E[M] —→ E[M′]

Since now values uniquely dermine the underlying term, we can now write, for instance

(ƛ N) ·[ E ]

instead of

_·[_] { ƛ N } V-ƛ E
infix  4 _⊢_==>_
infix  6 [_]·_
infix  6 _·[_]
infix  6 `suc[_]
infix  6 case[_]
infix  7 _⟦_⟧

data _⊢_==>_ (Γ : Context) (C : Type) : Type  Set where

   : Γ  C ==> C

  [_]·_ :  {A B}
     Γ  C ==> (A  B)
     Γ  A
      ---------------
     Γ  C ==> B

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

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

  case[_] :  {A}
     Γ  C ==> `ℕ
     Γ  A
     Γ  `ℕ  A
      -----------
     Γ  C ==> A
The plug function inserts an expression into the hole of a frame.
_⟦_⟧ : ∀{Γ A B}
   Γ  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

Reduction

infix 2 _↦_ _—→_

data _↦_ :  {Γ A}  (Γ  A)  (Γ  A)  Set where

  β-λ :  {Γ A B} {N : Γ  A  B} {W : Γ  A}
     Value W
      -------------------
     (ƛ N) · W  N [ W ]

  β-zero :   {Γ A} {M : Γ  A} {N : Γ  `ℕ  A}
      ------------------
     case `zero M N  M

  β-suc :  {Γ A} {V : Γ  `ℕ} {M : Γ  A} {N : Γ  `ℕ  A}
     Value V
      ---------------------------
     case (`suc V) M N  N [ V ]

  β-μ :  {Γ A} {N : Γ  A  A}
      ---------------
     μ N  N [ μ N ]



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

  ξξ :  {Γ A B} {M N : Γ  A} {M′ N′ : Γ  B}
     ( E : Γ  A ==> B)
     M′  E  M 
     N′  E  N 
     M  N
      --------
     M′ —→ N′
Notation
pattern ξ E M—→N = ξξ E refl refl M—→N

Reflexive and transitive closure of reduction

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

data _—↠_ : ∀{Γ A}  Γ  A  Γ  A  Set where

  _∎ :  {Γ A} (M : Γ  A)
      ---------
     M —↠ M

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

begin_ :  {Γ A} {M N : Γ  A}  (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.
value-irreducible :  {Γ A} {V M : Γ  A}
   Value V
    ----------
   ¬ (V —→ M)
value-irreducible v V—→M = nope V—→M v
   where
   nope :  {Γ A} {V M : Γ  A}
      V —→ M
      Value V
       -------
      
   nope (ξ  (β-λ v)) ()
   nope (ξ  β-zero) ()
   nope (ξ  (β-suc x)) ()
   nope (ξ  β-μ) ()
   nope (ξ `suc[ E ] V↦M) (`suc v)  =  nope (ξ E V↦M) v
redex : ∀{Γ A} (M : Γ  A)  Set
redex M = ∃[ N ] (M  N)

Progress

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

data Progress {A} (M :   A) : Set where

  step :  {N :   A}
     M —→ N
      ----------
     Progress M

  done :
      Value M
      ----------
     Progress M

progress :  {A}
   (M :   A)
    -----------
   Progress M
progress (ƛ N)                           =  done (ƛ N)
progress (L · M) with progress L
... | step (ξ E L↦L′)                    =  step (ξ ([ E  M) L↦L′)
... | done (ƛ N) with progress M
...     | step (ξ E M↦M′)                =  step (ξ ((ƛ N) ·[ E ]) M↦M′)
...     | done w                         =  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 `zero                         =  step (ξ  β-zero)
... | done (`suc v)                      =  step (ξ  (β-suc v))
progress (μ M)                           =  step (ξ  β-μ)

Evaluation

Gas is specified by a natural number:
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 it ran out of gas.
data Finished {A} : (  A)  Set where

   done :  {N :   A}
      Value N
       ----------
      Finished N

   out-of-gas : {N :   A}
       ----------
      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:
data Steps {A} :   A  Set where

  steps : {L N :   A}
     L —↠ N
     Finished N
      ----------
     Steps L
The evaluator takes gas and a term and returns the corresponding steps:
eval :  {A}
   Gas
   (L :   A)
    -----------
   Steps L

eval (gas zero)    L                     =  steps (L ) out-of-gas
eval (gas (suc m)) L with progress L
... | done VL                            =  steps (L ) (done VL)
... | step {M} L—→M with eval (gas m) M
...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M  M—↠N) fin

Examples

_ : 2+2 —↠ `suc `suc `suc `suc `zero
_ =
  begin
    2+2
  —→⟨ ξ ([ [   two  two) β-μ 
    (ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · two · two
  —→⟨ ξ ([   two) (β-λ (`suc (`suc `zero))) 
    (ƛ case two (` Z) (`suc (plus · ` Z · ` S Z))) · two
  —→⟨ ξ  (β-λ (`suc (`suc `zero))) 
    case two two (`suc (plus · ` Z · two))
  —→⟨ ξ  (β-suc (`suc `zero)) 
    `suc (plus · (`suc `zero) · two)
  —→⟨ ξ `suc[ [ [   (`suc `zero)  two ] β-μ 
    `suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · (`suc `zero) · two)
  —→⟨ ξ `suc[ [   two ] (β-λ (`suc `zero)) 
    `suc ((ƛ case (`suc `zero) (` Z) (`suc (plus · ` Z · ` S Z))) · two)
  —→⟨ ξ `suc[  ] (β-λ (`suc (`suc `zero))) 
    `suc (case (`suc `zero) two (`suc (plus · ` Z · two)))
  —→⟨ ξ `suc[  ] (β-suc `zero) 
    `suc `suc (plus · `zero · two)
  —→⟨ ξ `suc[ `suc[ [ [   `zero  two ] ] β-μ 
    `suc `suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · `zero · two)
  —→⟨ ξ `suc[ `suc[ [   two ] ] (β-λ `zero) 
    `suc `suc ((ƛ case `zero (` Z) (`suc (plus · ` Z · ` S Z))) · two)
  —→⟨ ξ `suc[ `suc[  ] ] (β-λ (`suc (`suc `zero))) 
    `suc `suc (case `zero two (`suc (plus · ` Z · two)))
  —→⟨ ξ `suc[ `suc[  ] ] β-zero 
    `suc `suc two
  

_ : 2+2ᶜ —↠ `suc `suc `suc `suc `zero
_ =
  begin
    plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
  —→⟨ ξ ([ [ [   twoᶜ  sucᶜ  `zero) (β-λ (ƛ ƛ (` S Z · (` S Z · ` Z)))) 
    (ƛ ƛ ƛ (twoᶜ · ` S Z · (` S (S Z) · ` S Z · ` Z))) · twoᶜ · sucᶜ · `zero
  —→⟨ ξ ([ [   sucᶜ  `zero) (β-λ (ƛ ƛ (` S Z · (` S Z · ` Z)))) 
    (ƛ ƛ (twoᶜ · ` S Z · (twoᶜ · ` S Z · ` Z))) · sucᶜ · `zero
  —→⟨ ξ ([   `zero) (β-λ (ƛ (`suc (` Z)))) 
    (ƛ (twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` Z))) · `zero
  —→⟨ ξ  (β-λ `zero) 
    twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero)
  —→⟨ ξ ([   (twoᶜ · sucᶜ · `zero)) (β-λ (ƛ (`suc (` Z)))) 
    (ƛ (sucᶜ · (sucᶜ · ` Z))) · (twoᶜ · sucᶜ · `zero)
  —→⟨ ξ ((ƛ (sucᶜ · (sucᶜ · ` Z))) ·[ [   `zero ]) (β-λ (ƛ (`suc (` Z)))) 
    (ƛ (sucᶜ · (sucᶜ · ` Z))) · ((ƛ (sucᶜ · (sucᶜ · ` Z))) · `zero)
  —→⟨ ξ ((ƛ (sucᶜ · (sucᶜ · ` Z))) ·[  ]) (β-λ `zero) 
    (ƛ (sucᶜ · (sucᶜ · ` Z))) · (sucᶜ · (sucᶜ · `zero))
  —→⟨ ξ ((ƛ (sucᶜ · (sucᶜ · ` Z))) ·[ (ƛ (`suc (` Z))) ·[  ] ]) (β-λ `zero) 
    (ƛ (sucᶜ · (sucᶜ · ` Z))) · (sucᶜ · (`suc `zero))
  —→⟨ ξ ((ƛ (sucᶜ · (sucᶜ · ` Z))) ·[  ]) (β-λ (`suc `zero)) 
    (ƛ (sucᶜ · (sucᶜ · ` Z))) · two
  —→⟨ ξ  (β-λ (`suc (`suc `zero))) 
    sucᶜ · (sucᶜ · two)
  —→⟨ ξ ((ƛ (`suc (` Z))) ·[  ]) (β-λ (`suc (`suc `zero))) 
    sucᶜ · (`suc two)
  —→⟨ ξ  (β-λ (`suc (`suc (`suc `zero)))) 
    (`suc (`suc two))