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

tidied examples in Lambda

Browse source
This commit is contained in:
wadler 2018-06-30 13:59:00 -03:00
parent be3f59a3dd
commit 0baf3a784e
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/plta/Lambda.lagda
View file

@ -1060,7 +1060,7 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A
∋z = Z ∋z = Z
\end{code} \end{code}
Here are the typings corresponding to our first example. Here are the typings corresponding to computing two plus two.
\begin{code} \begin{code}
⊢two : ∅ ⊢ two ⦂ `ℕ ⊢two : ∅ ⊢ two ⦂ `ℕ
⊢two = ⊢suc (⊢suc ⊢zero) ⊢two = ⊢suc (⊢suc ⊢zero)
@ -1075,8 +1075,8 @@ Here are the typings corresponding to our first example.
∋m′ = Z ∋m′ = Z
∋n′ = (S ("n" ≠ "m") Z) ∋n′ = (S ("n" ≠ "m") Z)
⊢four : ∅ ⊢ four ⦂ `ℕ ⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ
⊢four = ⊢plus · ⊢two · ⊢two ⊢2+2 = ⊢plus · ⊢two · ⊢two
\end{code} \end{code}
The two occcurrences of variable `"n"` in the original term appear The two occcurrences of variable `"n"` in the original term appear
in different contexts, and correspond here to the two different in different contexts, and correspond here to the two different
@ -1085,7 +1085,7 @@ a context that ends with the binding for "n", while the second looks
it up in a context extended by the binding for "m" in the second it up in a context extended by the binding for "m" in the second
branch of the case expression. branch of the case expression.
Here are typings for the remainder of the Church example. And here are typings for the remainder of the Church example.
\begin{code} \begin{code}
⊢plusᶜ : ∀ {A} → ∅ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A ⊢plusᶜ : ∀ {A} → ∅ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (Ax ∋m · Ax ∋s · (Ax ∋n · Ax ∋s · Ax ∋z))))) ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (Ax ∋m · Ax ∋s · (Ax ∋n · Ax ∋s · Ax ∋z)))))
@ -1100,8 +1100,11 @@ Here are typings for the remainder of the Church example.
where where
∋n = Z ∋n = Z
⊢fourᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ ⊢2ᶜ : ∅ ⊢ twoᶜ · sucᶜ · `zero ⦂ `ℕ
⊢fourᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero ⊢2ᶜ = ⊢twoᶜ · ⊢sucᶜ · ⊢zero
⊢2+2ᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ
⊢2+2ᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero
\end{code} \end{code}