Clarify lecture 3

parent f3744b6d
...@@ -592,6 +592,7 @@ We consider the purely negative fragment of propositional logic:: ...@@ -592,6 +592,7 @@ We consider the purely negative fragment of propositional logic::
Atom : (a : A) → Formula Atom : (a : A) → Formula
_⊃_ : (P Q : Formula) → Formula _⊃_ : (P Q : Formula) → Formula
The decision procedure checks whether a Formula (in a context) is The decision procedure checks whether a Formula (in a context) is
true. This amounts to implementing a traditional focusing presentation true. This amounts to implementing a traditional focusing presentation
of the sequent calculus:: of the sequent calculus::
...@@ -703,6 +704,7 @@ context/list:: ...@@ -703,6 +704,7 @@ context/list::
With a bit of refactoring, we can integrate indices as well as absorb With a bit of refactoring, we can integrate indices as well as absorb
the zipper traversal, making the structural recursion slightly more the zipper traversal, making the structural recursion slightly more
obvious (to us, not to Agda):: obvious (to us, not to Agda)::
...@@ -761,17 +763,17 @@ definitions on ``Formulas``:: ...@@ -761,17 +763,17 @@ definitions on ``Formulas``::
{-# TERMINATING #-} {-# TERMINATING #-}
search : ∀ {n} → Context n → A → Bool search : ∀ {n} → Context n → A → Bool
search {zero} tt α = false search {zero} tt α = false
search {suc n} ((l , B) , Γ) α = search {suc m} ((l , B) , Γ) α =
let try = map (λ { (P , B) → B / Γ [ P ]⊢ α }) let try = map (λ { (P , B) → B / Γ [ P ]⊢ α })
(pick1 B) (pick1 B)
in in
any try ∨ search Γ α any try ∨ search Γ α
where _/_[_]⊢_ : Vec (Formula n) (pred l) → Context n → Formula n → A → Bool where _/_[_]⊢_ : Vec (Formula m) (pred l) → Context m → Formula m → A → Bool
B / Γ [ Atom α ]⊢ β = ⌊ α ≟ β ⌋ B / Γ [ Atom α ]⊢ β = ⌊ α ≟ β ⌋
B / Γ [ _⊃_ {n} P Q ]⊢ β = B / Γ [ Q ]⊢ β ∧ B / Γ ⊢ P B / Γ [ _⊃_ {n} P Q ]⊢ β = B / Γ [ Q ]⊢ β ∧ B / Γ ⊢ P
where _/_⊢_ : Vec (Formula (suc n)) (pred l) → Context (suc n) → Formula n → Bool where _/_⊢_ : Vec (Formula (suc n)) (pred l) → Context (suc n) → Formula n → Bool
B / Γ ⊢ Atom α = search ((, B) , Γ) α B / Γ ⊢ Atom α = search ((, B) , Γ) α
B / B₂ , Γ ⊢ P ⊃ Q = B / B₂ , Γ ▹C P ⊢ Q B / B' , Γ ⊢ P ⊃ Q = B / B' , Γ ▹C P ⊢ Q
_⊢_ : ∀ {n} → Context n → Formula n → Bool _⊢_ : ∀ {n} → Context n → Formula n → Bool
Γ ⊢ Atom α = search Γ α Γ ⊢ Atom α = search Γ α
...@@ -809,10 +811,11 @@ With `The View from the Left`_ came the idea that one could get the ...@@ -809,10 +811,11 @@ With `The View from the Left`_ came the idea that one could get the
benefits of pattern-matching *syntax* while actually appealing to benefits of pattern-matching *syntax* while actually appealing to
induction principles to back them up *semantically*. induction principles to back them up *semantically*.
Assuming that we had this machinery (which we have not), it becomes Assuming that we had this machinery (which we have not in Agda but is
interesting to study and develop the algebra of induction available in Coq thanks to `Equations
principles. Let us dissect the induction principle for natural <http://mattam82.github.io/Coq-Equations/>`_), it becomes interesting
numbers. to study and develop the algebra of induction principles. Let us
dissect the induction principle for natural numbers.
The first ingredient of an induction principle is the *induction The first ingredient of an induction principle is the *induction
hypothesis*. We can generically define an induction hypothesis as a hypothesis*. We can generically define an induction hypothesis as a
...@@ -1103,10 +1106,13 @@ Let ``M : Set → Set`` be a monad. We have: ...@@ -1103,10 +1106,13 @@ Let ``M : Set → Set`` be a monad. We have:
.. code-block:: guess .. code-block:: guess
Monad(RecMon X, M X) Monad(RecMon, M)
≅ Set(Σ[ a ∈ A ] B a → X, M X) -- by the free/forgetful adjunction ≅ Monad(Free(λ X → Σ[ a ∈ A ] B a → X), M) -- by def. of RecMon
≅ (a : A) → ∀ X → (B a → X) → M X -- by uncurry, etc. ≅ [Set,Set](λ X → Σ[ a ∈ A ] B a → X, U(M)) -- by the free/forgetful adjunction
≅ (a : A) → M (B a) -- by Yoneda lemma ≅ ∀ X → (Σ[ a ∈ A ] B a → X) → M X -- morphism of functors are natural trans.
≅ (a : A) → ∀ X → (B a → X) → M X -- by uncurry, etc.
≅ (a : A) → M (B a) -- by Yoneda lemma
Or, put otherwise, a monad morphism from RecMon is entirely specified Or, put otherwise, a monad morphism from RecMon is entirely specified
by a mere function of type ``(a : A) → M (B a)``:: by a mere function of type ``(a : A) → M (B a)``::
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment