michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

halfway through DeBruijn

Browse source
This commit is contained in:
wadler 2018-02-24 16:31:35 +01:00
parent b0226ccb41
commit edfbdd1a0d
1 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/extra/DeBruijn.lagda
View file

@ -57,16 +57,16 @@ env (Γ , A) = env Γ × type A
Church : Type Church : Type
Church = (o ⇒ o) ⇒ o ⇒ o Church = (o ⇒ o) ⇒ o ⇒ o
plus : Exp ε (Church ⇒ Church ⇒ Church) plus : ∀ {Γ : Env} → Exp Γ (Church ⇒ Church ⇒ Church)
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))))))) 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 : ∀ {Γ : Env} → Exp Γ Church
one = (abs (abs (app (var (S Z)) (var Z)))) one = (abs (abs (app (var (S Z)) (var Z))))
two : Exp ε Church two : ∀ {Γ : Env} → Exp Γ Church
two = (app (app plus one) one) two = (app (app plus one) one)
four : Exp ε Church four : ∀ {Γ : Env} → Exp Γ Church
four = (app (app plus two) two) four = (app (app plus two) two)
\end{code} \end{code}
@ -232,18 +232,20 @@ M ∎ = reflexive
ex₁ : (app (abs (var Z)) (abs (var Z))) ⟶* (abs (var Z)) ex₁ : (app (abs (var Z)) (abs (var Z))) ⟶* (abs (var Z))
ex₁ = ex₁ =
begin begin
(app (abs (var Z)) (abs (var Z))) (app (abs {Γ = ε} {A = o ⇒ o} (var Z)) (abs (var Z)))
⟶⟨ β ⟩ ⟶⟨ β Fun ⟩
(abs (var Z)) (abs (var Z))
∎ ∎
\end{code} \end{code}
ex₁ : (app (app plus one) one) ⟶ (abs (abs (app (var (S Z)) (app (var (S Z)) (var Z))))) \begin{code}
ex₁ = ex₂ : (app {Γ = ε} (app plus one) one) ⟶* (abs (abs (app (app one (var (S Z))) (app (app one (var (S Z))) (var Z)))))
ex₂ =
begin begin
(app (app plus one) one) (app (app plus one) one)
⟶⟨ ξ_1 β ⟩ ⟶⟨ ξ₁ (β Fun) ⟩
(app (abs (abs (abs (app (app one) (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z))))) one) (app (abs (abs (abs (app (app one (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z)))))) one)
⟶⟨ β ⟩ ⟶⟨ β Fun ⟩
(abs (abs (app (app one) (var (S Z))) (app (app one (var (S Z))) (var Z)))) (abs (abs (app (app one (var (S Z))) (app (app one (var (S Z))) (var Z)))))
⟶⟨ ⟩ ∎
\end{code}