Interpreting the untyped lambda calculus in Agda

UntypedLambda.agda

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where
    now   : A → Delay A i
    later : ∞Delay A i → Delay A i

  record ∞Delay (A : Set) (i : Size) : Set where
    coinductive
    constructor [_]
    field
      force : {j : Size< i} → Delay A j

open import Data.Nat
open import Data.Fin

data Expr (n : ℕ) : Set where
  Var : Fin n → Expr n
  App : Expr n → Expr n → Expr n
  Lam : Expr (suc n) → Expr n

renm : {m n : ℕ} (t : Expr n) (ρ : Fin n → Fin m) → Expr m
renm (Var x)   ρ = Var (ρ x)
renm (App t u) ρ = App (renm t ρ) (renm u ρ)
renm (Lam t)   ρ = Lam $ renm t $ λ k → case k of λ
                                          { zero    → zero
                                          ; (suc l) → suc (ρ l)
                                          }

subst : {m n : ℕ} (t : Expr n) (ρ : Fin n → Expr m) → Expr m
subst (Var x)   ρ = ρ x
subst (App t u) ρ = App (subst t ρ) (subst u ρ)
subst (Lam t)   ρ = Lam $ subst t $ λ k → case k of λ
                                            { zero    → Var zero
                                            ; (suc l) → renm (ρ l) suc
                                            }

_⟨_⟩ : {m : ℕ} (t : Expr (suc m)) (u : Expr m) → Expr m
t ⟨ u ⟩ = subst t $ λ k → case k of λ
                            { zero    → u
                            ; (suc l) → Var l
                            }

open import Data.Maybe as Maybe

redex : {n : ℕ} (t : Expr n) → Maybe (Expr n)
redex (Var x)         = nothing
redex (App (Lam t) u) = just (t ⟨ u ⟩)
redex (App t u)       = case redex t of λ
                           { nothing   → Maybe.map (App t) (redex u) 
                           ; (just t') → just (App t' u)
                           }
redex (Lam t)         = Maybe.map Lam (redex t)


mutual

  run : {n : ℕ} (t : Expr n) → {i : Size} → Delay (Expr n) i
  run t = case redex t of λ
            { nothing   → now t
            ; (just t') → later (∞run t')
            }

  ∞run : {n : ℕ} (t : Expr n) → {i : Size} → ∞Delay (Expr n) i
  ∞Delay.force (∞run t) = run t

identity : Expr 0
identity = Lam $ Var zero

delta : Expr 0
delta = Lam $ App (Var zero) (Var zero)

omega : Expr 0
omega = App delta delta

identity′ : Delay (Expr 0) ∞
identity′ = run (App identity identity)

open import Relation.Binary.PropositionalEquality

extract : {A : Set} (n : ℕ) (da : Delay A ∞) → Maybe A
extract n       (now a)     = just a
extract zero    (later ∞da) = nothing
extract (suc n) (later ∞da) = extract n (∞Delay.force ∞da)

lemmaIdentity′ : extract 1 identity′ ≡ just identity
lemmaIdentity′ = refl

lemmaOmega : (n : ℕ) → extract n (run omega) ≡ nothing
lemmaOmega zero    = refl
lemmaOmega (suc n) = lemmaOmega n