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

updates to PUC and Assignments

Browse source
This commit is contained in:
wadler 2019-05-25 11:16:08 -03:00
parent 80398ee5e2
commit af9b369ea3
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/plfa/DeBruijn.lagda
View file

@ -450,10 +450,12 @@ two = `suc `suc `zero
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1))) plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
2+2 : ∀ {Γ} → Γ ⊢ `ℕ
2+2 = plus · two · two
\end{code} \end{code}
We specify that `two` and `plus` can be typed in an arbitrary environment, We generalise to arbitrary contexts because later we will give examples
rather than just the empty environment, because later we will give examples where `two` appears nested inside binders.
where they appear nested inside binders.
Next, computing two plus two on Church numerals: Next, computing two plus two on Church numerals:
\begin{code} \begin{code}
@ -468,6 +470,9 @@ plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ
sucᶜ = ƛ `suc (# 0) sucᶜ = ƛ `suc (# 0)
2+2ᶜ : ∀ {Γ} → Γ ⊢ `ℕ
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
\end{code} \end{code}
As before we generalise everything to arbitrary As before we generalise everything to arbitrary
contexts. While we are at it, we also generalise `twoᶜ` and contexts. While we are at it, we also generalise `twoᶜ` and

2
tspl/PUC.lagda
View file

@ -100,6 +100,6 @@ For instructions on how to set up Agda for PLFA see [Getting Started](/GettingSt
Use file [Exam][Exam]. Despite the rubric, do **all three questions**. Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk). Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
Attach a single file named Assignment1.lagda or the like. Include Attach a single file named `PUC-Assignment1.lagda` or the like. Include
your name and email in the submitted file. your name and email in the submitted file.