[Agda] Double Negation as Monad

[Edward Kmett]

You might find the following paper useful:

http://research.microsoft.com/en-us/um/people/simonpj/papers/not-not-ml/index.htm
It talks about this relationship a bit further, including using the Devil's
bargain to show ~~~a -> ~a works even in constructive logic. What I liked
about the paper was the only lambdas they use return bottom.

There is also an obvious tie to continuation passing style, and a less
obvious tie that shows that this is just a codensity monad of the trivial
functor that maps everything to bottom and hence a right Kan extension in
category theory, but since it is in the form of a codensity monad, the monad
comes for free.

-Edward Kmett
On Thu, Oct 29, 2009 at 1:22 PM, Vag Vagoff <vag.vagoff at gmail.com> wrote:

> If constructive mathematics is equivalent to classic one without double
> negation elimination law (from wich law of Excluded Middle is derivable)
> then constructive mathematics is strictly as  powerful as classic because
> simple algorithm may be created which converts classic proofs to
> constructive ones automatically using proof continuations and double
> negation monad (but converted proof will be surrounded by double negation).
>
> Is this correct?
>
> module DoubleNegationIsMonad where
>
> -- libraries --
>
> data ⊥ : Set where
> infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡-refl : a ≡ a
> infixr 90 _∘_ ; _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) ; f
> ∘ g = λ x → f (g x)
> ¬_ : (P : Set) → Set ; ¬ P = P → ⊥
> ¬¬ = λ (p : Set) → ¬ ¬ p
>
> -- helpers --
>
> ¬¬-intro : ∀ {P} → P → ¬¬ P
> ¬¬-intro p = λ f → f p
>
> →¬¬-intro : ∀ {P Q} → (P → Q) → (P → ¬¬ Q)
> →¬¬-intro = _∘_ ¬¬-intro
>
> ¬¬¬→¬  : ∀ {P} → ¬ ¬ ¬ P → ¬ P
> ¬¬¬→¬ {P} nnnp = λ p → (¬¬-intro (¬¬-intro p)) nnnp
>
> ¬¬¬¬→¬¬  : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P
> ¬¬¬¬→¬¬ = ¬¬¬→¬
>
> swap : ∀ {P Q} → (P → ¬ Q) → (Q → ¬ P)
> swap pq qp p = (pq p) qp
>
> swap&intro : ∀ {P Q} → (P → Q) → ¬  Q → ¬  P
> swap&intro = swap ∘ →¬¬-intro
>
> lift : ∀ {P Q} → (P → Q) → ¬¬ P → ¬¬ Q
> lift = swap&intro ∘ swap&intro
>
> -- monad --
>
> return : ∀ {P} → P → ¬¬ P
> return = ¬¬-intro
>
> infixl 10 _>>=_
> _>>=_ : ∀ {P Q} → ¬¬ P → (P → ¬¬ Q)  → ¬¬ Q
> ma >>= f = ¬¬¬¬→¬¬ (lift f ma)
>
> join : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P
> join = ¬¬¬¬→¬¬
>
> -- monad laws --
>
> left-identity : ∀ {A B} → (a : A) → (f : A → ¬¬ B) → return a >>= f ≡ f a
> left-identity a f = ≡-refl
>
> right-identity : ∀ {A} → (a : ¬¬ A) → a >>= return ≡ a
> right-identity a = ≡-refl
>
> associativity : ∀ {A B C} → (a : ¬¬ A) → (b : A → ¬¬ B) → (c : B → ¬¬ C)
> → (a >>= b) >>= c ≡ a >>= (λ x → b x >>= c)
> associativity a b c = ≡-refl
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091029/5f7936b6/attachment-0001.html