halfway through DeBruijn
This commit is contained in:
wadler
parent
543017049d
commit
b0226ccb41
1 changed files with 150 additions and 30 deletions
|
|
@ -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))))
|
||||
⟶⟨ ⟩
|
||||
|
|
|
|||
Loading…
Reference in a new issue