From b0226ccb41f2f8ce09c947f56713673cb28725b5 Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 24 Feb 2018 13:45:45 +0100 Subject: [PATCH] halfway through DeBruijn --- src/extra/DeBruijn.lagda | 180 ++++++++++++++++++++++++++++++++------- 1 file changed, 150 insertions(+), 30 deletions(-) diff --git a/src/extra/DeBruijn.lagda b/src/extra/DeBruijn.lagda index 66b71256..92d4432b 100644 --- a/src/extra/DeBruijn.lagda +++ b/src/extra/DeBruijn.lagda @@ -9,7 +9,7 @@ module DeBruijn where \begin{code} import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong) -open Eq.≡-Reasoning +-- open Eq.≡-Reasoning open import Data.Nat using (ℕ; zero; suc; _+_) open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_; inj₁; inj₂) @@ -34,8 +34,8 @@ data Env : Set where _,_ : Env → Type → Env data Var : Env → Type → Set where - zero : ∀ {Γ : Env} {A : Type} → Var (Γ , A) A - suc : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (Γ , A) B + Z : ∀ {Γ : Env} {A : Type} → Var (Γ , A) A + S : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (Γ , A) B data Exp : Env → Type → Set where var : ∀ {Γ : Env} {A : Type} → Var Γ A → Exp Γ A @@ -58,10 +58,10 @@ Church : Type Church = (o ⇒ o) ⇒ o ⇒ o plus : Exp ε (Church ⇒ Church ⇒ Church) -plus = (abs (abs (abs (abs (app (app (var (suc (suc (suc zero)))) (var (suc zero))) (app (app (var (suc (suc zero))) (var (suc zero))) (var zero))))))) +plus = (abs (abs (abs (abs (app (app (var (S (S (S Z)))) (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z))))))) one : Exp ε Church -one = (abs (abs (app (var (suc zero)) (var zero)))) +one = (abs (abs (app (var (S Z)) (var Z)))) two : Exp ε Church two = (app (app plus one) one) @@ -75,55 +75,175 @@ four = (app (app plus two) two) \begin{code} lookup : ∀ {Γ : Env} {A : Type} → Var Γ A → env Γ → type A -lookup zero ⟨ ρ , v ⟩ = v -lookup (suc n) ⟨ ρ , v ⟩ = lookup n ρ +lookup Z ⟨ ρ , v ⟩ = v +lookup (S n) ⟨ ρ , v ⟩ = lookup n ρ eval : ∀ {Γ : Env} {A : Type} → Exp Γ A → env Γ → type A eval (var n) ρ = lookup n ρ eval (abs N) ρ = λ{ v → eval N ⟨ ρ , v ⟩ } eval (app L M) ρ = eval L ρ (eval M ρ) -ex : eval four tt suc 0 ≡ 4 +ex : eval four tt suc zero ≡ 4 ex = refl \end{code} -# Operational semantics +# Operational semantics - with substitution a la Darais (31 lines) -## Substitution +## Remove variable from environment (4 lines) \begin{code} -extr : ∀ {Γ Δ : Env} {B : Type} → (∀ {A : Type} → Var Γ A → Var Δ A) → Var Δ B → (∀ {A : Type} → Var (Γ , B) A → Var Δ A) -extr ρ v zero = v -extr ρ v (suc k) = ρ k - -ren : ∀ {Γ Δ : Env} → (∀ {A : Type} → Var Γ A → Var Δ A) → (∀ {A : Type} → Exp Γ A → Exp Δ A) -ren ρ (var n) = var (ρ n) -ren ρ (app L M) = app (ren ρ L) (ren ρ M) -ren ρ (abs N) = abs (ren (extr (suc ∘ ρ) zero) N) +infix 4 _⊝_ +_⊝_ : ∀ {A : Type} (Γ : Env) → Var Γ A → Env +(Γ , B) ⊝ Z = Γ +(Γ , B) ⊝ S k = (Γ ⊝ k) , B \end{code} +## Rebuild environment (6 lines) + +\begin{code} +shunt : ∀ (Γ Δ : Env) → Env +shunt Γ ε = Γ +shunt Γ (Δ , A) = shunt (Γ , A) Δ + +weaken : ∀ (Γ Δ : Env) {A : Type} (k : Var Γ A) → Var (shunt Γ Δ) A +weaken Γ ε k = k +weaken Γ (Δ , A) k = weaken (Γ , A) Δ (S k) +\end{code} + +## Lift term to a larger environment (8 lines) + +\begin{code} +liftvar : ∀ {Γ : Env} {A B : Type} (j : Var Γ B) (k : Var (Γ ⊝ j) A) → Var Γ A +liftvar Z k = S k +liftvar (S j) Z = Z +liftvar (S j) (S k) = S (liftvar j k) + +lift : ∀ {Γ : Env} {A B : Type} (j : Var Γ B) (M : Exp (Γ ⊝ j) A) → Exp Γ A +lift j (var k) = var (liftvar j k) +lift j (abs N) = abs (lift (S j) N) +lift j (app L M) = app (lift j L) (lift j M) +\end{code} + +## Substitution (13 lines) + +\begin{code} +substvar : ∀ (Γ Δ : Env) {A B : Type} (j : Var Γ B) (k : Var Γ A) (P : Exp (shunt (Γ ⊝ k) Δ) A) → Exp (shunt (Γ ⊝ k) Δ) B +substvar Γ Δ Z Z P = P +substvar (Γ , A) Δ Z (S k) P = var (weaken ((Γ ⊝ k) , A) Δ Z) +substvar (Γ , A) Δ (S j) Z P = var (weaken Γ Δ j) +substvar (Γ , A) Δ (S j) (S k) P = substvar Γ (Δ , A) j k P + +subst : ∀ {Γ : Env} {A B : Type} (N : Exp Γ B) (k : Var Γ A) (M : Exp (Γ ⊝ k) A) → Exp (Γ ⊝ k) B +subst {Γ} (var j) k P = substvar Γ ε j k P +subst (abs N) k P = abs (subst N (S k) (lift Z P)) +subst (app L M) k P = app (subst L k P) (subst M k P) +\end{code} + +# Operational semantics - with simultaneous substitution, a la McBride (18 lines) + +## Renaming (7 lines) + +\begin{code} +extend : ∀ {Γ Δ : Env} {B : Type} → (∀ {A : Type} → Var Γ A → Var Δ A) → Var Δ B → (∀ {A : Type} → Var (Γ , B) A → Var Δ A) +extend ρ j Z = j +extend ρ j (S k) = ρ k + +rename : ∀ {Γ Δ : Env} → (∀ {A : Type} → Var Γ A → Var Δ A) → (∀ {A : Type} → Exp Γ A → Exp Δ A) +rename ρ (var n) = var (ρ n) +rename ρ (abs N) = abs (rename (extend (S ∘ ρ) Z) N) +rename ρ (app L M) = app (rename ρ L) (rename ρ M) +\end{code} + +## Substitution (9 lines) + \begin{code} ext : ∀ {Γ Δ : Env} {B : Type} → (∀ {A : Type} → Var Γ A → Exp Δ A) → Exp Δ B → (∀ {A : Type} → Var (Γ , B) A → Exp Δ A) -ext ρ v zero = v -ext ρ v (suc k) = ρ k - -emp : ∀ {Γ : Env} → (∀ {A : Type} → Var Γ A → Exp Γ A) -emp k = var k +ext ρ j Z = j +ext ρ j (S k) = ρ k sub : ∀ {Γ Δ : Env} → (∀ {A : Type} → Var Γ A → Exp Δ A) → (∀ {A : Type} → Exp Γ A → Exp Δ A) sub ρ (var n) = ρ n sub ρ (app L M) = app (sub ρ L) (sub ρ M) -sub ρ (abs N) = abs (sub (ext (ren suc ∘ ρ) (var zero)) N) +sub ρ (abs N) = abs (sub (ext (rename S ∘ ρ) (var Z)) N) -subst : ∀ {Γ : Env} {A B : Type} → Exp (Γ , A) B → Exp Γ A → Exp Γ B -subst N M = sub (ext emp M) N +substitute : ∀ {Γ : Env} {A B : Type} → Exp (Γ , A) B → Exp Γ A → Exp Γ B +substitute N M = sub (ext var M) N +\end{code} + +## Value + +\begin{code} +data Val : {Γ : Env} {A : Type} → Exp Γ A → Set where + Fun : ∀ {Γ : Env} {A B : Type} {N : Exp (Γ , A) B} → + Val (abs N) \end{code} ## Reduction step \begin{code} -data Val : {Γ : Env} {A : Type} → Exp Γ A → Set where - -data Step : {Γ : Env} {A : Type} → Exp Γ A → Exp Γ A → Set where - beta : ∀ {Γ : Env} {A B : Type} {N : Exp (Γ , A) B} {M : Exp Γ A} → Step (app (abs N) M) (subst N M) +data _⟶_ : {Γ : Env} {A : Type} → Exp Γ A → Exp Γ A → Set where + ξ₁ : ∀ {Γ : Env} {A B : Type} {L : Exp Γ (A ⇒ B)} {L′ : Exp Γ (A ⇒ B)} {M : Exp Γ A} → + L ⟶ L′ → + app L M ⟶ app L′ M + ξ₂ : ∀ {Γ : Env} {A B : Type} {L : Exp Γ (A ⇒ B)} {M : Exp Γ A} {M′ : Exp Γ A} → + Val L → + M ⟶ M′ → + app L M ⟶ app L M′ + β : ∀ {Γ : Env} {A B : Type} {N : Exp (Γ , A) B} {M : Exp Γ A} → + Val M → + app (abs N) M ⟶ substitute N M \end{code} + +## Reflexive and transitive closure + +\begin{code} +data _⟶*_ : {Γ : Env} {A : Type} → Exp Γ A → Exp Γ A → Set where + reflexive : ∀ {Γ : Env} {A : Type} {M : Exp Γ A} → + M ⟶* M + inclusion : ∀ {Γ : Env} {A : Type} {L M : Exp Γ A} → + L ⟶ M → + L ⟶* M + transitive : ∀ {Γ : Env} {A : Type} {L M N : Exp Γ A} → + L ⟶* M → + M ⟶* N → + L ⟶* N +\end{code} + +## Displaying reduction sequences + +\begin{code} +infix 1 begin_ +infixr 2 _⟶⟨_⟩_ +infix 3 _∎ + +begin_ : {Γ : Env} {A : Type} {M N : Exp Γ A} → (M ⟶* N) → (M ⟶* N) +begin steps = steps + +_⟶⟨_⟩_ : {Γ : Env} {A : Type} (L : Exp Γ A) {M N : Exp Γ A} → (L ⟶ M) → (M ⟶* N) → (L ⟶* N) +L ⟶⟨ L⟶M ⟩ M⟶*N = transitive (inclusion L⟶M) M⟶*N + +_∎ : {Γ : Env} {A : Type} (M : Exp Γ A) → M ⟶* M +M ∎ = reflexive +\end{code} + +## Example reduction sequence + +\begin{code} +ex₁ : (app (abs (var Z)) (abs (var Z))) ⟶* (abs (var Z)) +ex₁ = + begin + (app (abs (var Z)) (abs (var Z))) + ⟶⟨ β ⟩ + (abs (var Z)) + ∎ +\end{code} + +ex₁ : (app (app plus one) one) ⟶ (abs (abs (app (var (S Z)) (app (var (S Z)) (var Z))))) +ex₁ = + begin + (app (app plus one) one) + ⟶⟨ ξ_1 β ⟩ + (app (abs (abs (abs (app (app one) (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z))))) one) + ⟶⟨ β ⟩ + (abs (abs (app (app one) (var (S Z))) (app (app one (var (S Z))) (var Z)))) + ⟶⟨ ⟩