Created
September 7, 2015 18:53
-
-
Save gallais/303cfcfe053fbc63eb61 to your computer and use it in GitHub Desktop.
Interpreting the untyped lambda calculus in Agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment