first draft of DeBruijn
This commit is contained in:
parent
fb2c3ab076
commit
155375a559
3 changed files with 79 additions and 11 deletions
|
@ -33,8 +33,33 @@ count b e = sum . map length . strip b e
|
||||||
test2 :: Bool
|
test2 :: Bool
|
||||||
test2 = count (== 'b') (== 'e') ex1 == 6
|
test2 = count (== 'b') (== 'e') ex1 == 6
|
||||||
|
|
||||||
agda :: String -> IO Int
|
info :: String -> IO (Int , Int)
|
||||||
agda f =
|
info f =
|
||||||
do xs <- readFile f
|
do xs <- readFile f
|
||||||
return ((count (prefix begin) (prefix end) . lines) xs)
|
return ((length . lines) xs),
|
||||||
|
(count (prefix begin) (prefix end) . lines) xs)
|
||||||
|
|
||||||
|
pad :: Int -> String -> String
|
||||||
|
pad n s = take n (s ++ repeat ' ')
|
||||||
|
|
||||||
|
rjust :: Int -> String -> String
|
||||||
|
rjust n = reverse . pad n . reverse
|
||||||
|
|
||||||
|
format :: String -> IO String
|
||||||
|
format "--" = ""
|
||||||
|
format f =
|
||||||
|
do (lines, code) <- info f
|
||||||
|
return (replicate 4 ' ' ++
|
||||||
|
pad 28 f ++
|
||||||
|
rjust 4 lines ++
|
||||||
|
replicate 4 ' ' ++
|
||||||
|
rjust 4 ' ')
|
||||||
|
|
||||||
|
config : IO [String]
|
||||||
|
config =
|
||||||
|
do stuff <- readFile "config.txt"
|
||||||
|
return (lines stuff)
|
||||||
|
|
||||||
|
answer : IO String
|
||||||
|
answer =
|
||||||
|
do
|
|
@ -1106,10 +1106,45 @@ eval (gas (suc m)) L with progress L
|
||||||
... | step {M} L—→M with eval (gas m) M
|
... | step {M} L—→M with eval (gas m) M
|
||||||
... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
|
... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
|
||||||
\end{code}
|
\end{code}
|
||||||
The definition is mu
|
The definition is a little simpler than previously, as we no longer need
|
||||||
|
to invoke preservation.
|
||||||
|
|
||||||
## Examples
|
## Examples
|
||||||
|
|
||||||
|
We reiterate each of our previous examples. We re-define the term
|
||||||
|
`sucμ` that loops forever.
|
||||||
|
\begin{code}
|
||||||
|
sucμ : ∅ ⊢ `ℕ
|
||||||
|
sucμ = μ (`suc (# 0))
|
||||||
|
\end{code}
|
||||||
|
To compute the first three steps of the infinite reduction sequence,
|
||||||
|
we evaluate with three steps worth of gas.
|
||||||
|
\begin{code}
|
||||||
|
_ : eval (gas 3) sucμ ≡
|
||||||
|
steps
|
||||||
|
(μ `suc ` Z —→⟨ β-μ ⟩
|
||||||
|
`suc (μ `suc ` Z) —→⟨ ξ-suc β-μ ⟩
|
||||||
|
`suc (`suc (μ `suc ` Z)) —→⟨ ξ-suc (ξ-suc β-μ) ⟩
|
||||||
|
`suc (`suc (`suc (μ `suc ` Z))) ∎)
|
||||||
|
out-of-gas
|
||||||
|
_ = refl
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
The Church numeral two applied to successor and zero.
|
||||||
|
\begin{code}
|
||||||
|
_ : eval (gas 100) (twoᶜ · sucᶜ · `zero) ≡
|
||||||
|
steps
|
||||||
|
((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) · `zero —→⟨
|
||||||
|
ξ-·₁ (β-ƛ V-ƛ) ⟩
|
||||||
|
(ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) · `zero —→⟨ β-ƛ V-zero ⟩
|
||||||
|
(ƛ `suc ` Z) · ((ƛ `suc ` Z) · `zero) —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
|
||||||
|
(ƛ `suc ` Z) · `suc `zero —→⟨ β-ƛ (V-suc V-zero) ⟩
|
||||||
|
`suc (`suc `zero) ∎)
|
||||||
|
(done (V-suc (V-suc V-zero)))
|
||||||
|
_ = refl
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
Two plus two is four.
|
||||||
\begin{code}
|
\begin{code}
|
||||||
_ : eval (gas 100) (plus · two · two) ≡
|
_ : eval (gas 100) (plus · two · two) ≡
|
||||||
steps
|
steps
|
||||||
|
@ -1249,6 +1284,7 @@ _ : eval (gas 100) (plus · two · two) ≡
|
||||||
_ = refl
|
_ = refl
|
||||||
\end{code}
|
\end{code}
|
||||||
|
|
||||||
|
And the corresponding term for Church numerals.
|
||||||
\begin{code}
|
\begin{code}
|
||||||
_ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
|
_ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
|
||||||
steps
|
steps
|
||||||
|
@ -1306,3 +1342,10 @@ _ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
|
||||||
(done (V-suc (V-suc (V-suc (V-suc V-zero)))))
|
(done (V-suc (V-suc (V-suc (V-suc V-zero)))))
|
||||||
_ = refl
|
_ = refl
|
||||||
\end{code}
|
\end{code}
|
||||||
|
|
||||||
|
We omit the proof that reduction is deterministic, since it is
|
||||||
|
tedious and almost identical to the previous proof.
|
||||||
|
|
||||||
|
Counting the lines of code is instructive. While this chapter
|
||||||
|
covers the same formal development as the previous two
|
||||||
|
chapters, it has about half the number of lines of code.
|
||||||
|
|
|
@ -1376,7 +1376,7 @@ three typical cases.
|
||||||
* Two instances of `ξ-·₁`.
|
* Two instances of `ξ-·₁`.
|
||||||
|
|
||||||
L —→ L′ L —→ L″
|
L —→ L′ L —→ L″
|
||||||
-------------- ξ-·₁ -------------- ξ-·₁
|
--------------- ξ-·₁ --------------- ξ-·₁
|
||||||
L · M —→ L′ · M L · M —→ L″ · M
|
L · M —→ L′ · M L · M —→ L″ · M
|
||||||
|
|
||||||
By induction we have `L′ ≡ L″`, and hence by congruence
|
By induction we have `L′ ≡ L″`, and hence by congruence
|
||||||
|
@ -1384,9 +1384,9 @@ three typical cases.
|
||||||
|
|
||||||
* An instance of `ξ-·₁` and an instance of `ξ-·₂`.
|
* An instance of `ξ-·₁` and an instance of `ξ-·₂`.
|
||||||
|
|
||||||
Value L
|
Value L
|
||||||
L —→ L′ M —→ M″
|
L —→ L′ M —→ M″
|
||||||
-------------- ξ-·₁ -------------- ξ-·₂
|
--------------- ξ-·₁ --------------- ξ-·₂
|
||||||
L · M —→ L′ · M L · M —→ L · M″
|
L · M —→ L′ · M L · M —→ L · M″
|
||||||
|
|
||||||
The rule on the left requires `L` to reduce, but the rule on the right
|
The rule on the left requires `L` to reduce, but the rule on the right
|
||||||
|
@ -1396,12 +1396,12 @@ three typical cases.
|
||||||
|
|
||||||
* Two instances of `β-ƛ`.
|
* Two instances of `β-ƛ`.
|
||||||
|
|
||||||
Value V Value V
|
Value V Value V
|
||||||
---------------------------- β-ƛ ---------------------------- β-ƛ
|
----------------------------- β-ƛ ----------------------------- β-ƛ
|
||||||
(ƛ x ⇒ N) · V —→ N [ x := V ] (ƛ x ⇒ N) · V —→ N [ x := V ]
|
(ƛ x ⇒ N) · V —→ N [ x := V ] (ƛ x ⇒ N) · V —→ N [ x := V ]
|
||||||
|
|
||||||
Since the left-hand sides are identical, the right-hand sides are
|
Since the left-hand sides are identical, the right-hand sides are
|
||||||
also identical.
|
also identical. The formal proof invokes `refl`.
|
||||||
|
|
||||||
Almost half the lines in the above proof are redundant, e.g., the case
|
Almost half the lines in the above proof are redundant, e.g., the case
|
||||||
when one rule is `ξ-·₁` and the other is `ξ-·₂` is considered twice,
|
when one rule is `ξ-·₁` and the other is `ξ-·₂` is considered twice,
|
||||||
|
|
Loading…
Reference in a new issue