<div>You might find the following paper useful:</div>
<div> </div>
<div><a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/not-not-ml/index.htm">http://research.microsoft.com/en-us/um/people/simonpj/papers/not-not-ml/index.htm</a><br></div>
<div>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.</div>
<div> </div>
<div>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.</div>
<div> </div>
<div>-Edward Kmett<br></div>
<div class="gmail_quote">On Thu, Oct 29, 2009 at 1:22 PM, Vag Vagoff <span dir="ltr"><<a href="mailto:vag.vagoff@gmail.com">vag.vagoff@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">If constructive mathematics is equivalent to classic one without double<br>negation elimination law (from wich law of Excluded Middle is derivable)<br>
then constructive mathematics is strictly as powerful as classic because<br>simple algorithm may be created which converts classic proofs to<br>constructive ones automatically using proof continuations and double<br>negation monad (but converted proof will be surrounded by double negation).<br>
<br>Is this correct?<br><br>module DoubleNegationIsMonad where<br><br>-- libraries --<br><br>data ⊥ : Set where<br>infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡-refl : a ≡ a<br>infixr 90 _∘_ ; _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) ; f<br>
∘ g = λ x → f (g x)<br>¬_ : (P : Set) → Set ; ¬ P = P → ⊥<br>¬¬ = λ (p : Set) → ¬ ¬ p<br><br>-- helpers --<br><br>¬¬-intro : ∀ {P} → P → ¬¬ P<br>¬¬-intro p = λ f → f p<br><br>→¬¬-intro : ∀ {P Q} → (P → Q) → (P → ¬¬ Q)<br>
→¬¬-intro = _∘_ ¬¬-intro<br><br>¬¬¬→¬ : ∀ {P} → ¬ ¬ ¬ P → ¬ P<br>¬¬¬→¬ {P} nnnp = λ p → (¬¬-intro (¬¬-intro p)) nnnp<br><br>¬¬¬¬→¬¬ : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P<br>¬¬¬¬→¬¬ = ¬¬¬→¬<br><br>swap : ∀ {P Q} → (P → ¬ Q) → (Q → ¬ P)<br>
swap pq qp p = (pq p) qp<br><br>swap&intro : ∀ {P Q} → (P → Q) → ¬ Q → ¬ P<br>swap&intro = swap ∘ →¬¬-intro<br><br>lift : ∀ {P Q} → (P → Q) → ¬¬ P → ¬¬ Q<br>lift = swap&intro ∘ swap&intro<br><br>-- monad --<br>
<br>return : ∀ {P} → P → ¬¬ P<br>return = ¬¬-intro<br><br>infixl 10 _>>=_<br>_>>=_ : ∀ {P Q} → ¬¬ P → (P → ¬¬ Q) → ¬¬ Q<br>ma >>= f = ¬¬¬¬→¬¬ (lift f ma)<br><br>join : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P<br>join = ¬¬¬¬→¬¬<br>
<br>-- monad laws --<br><br>left-identity : ∀ {A B} → (a : A) → (f : A → ¬¬ B) → return a >>= f ≡ f a<br>left-identity a f = ≡-refl<br><br>right-identity : ∀ {A} → (a : ¬¬ A) → a >>= return ≡ a<br>right-identity a = ≡-refl<br>
<br>associativity : ∀ {A B C} → (a : ¬¬ A) → (b : A → ¬¬ B) → (c : B → ¬¬ C)<br>→ (a >>= b) >>= c ≡ a >>= (λ x → b x >>= c)<br>associativity a b c = ≡-refl<br><br>_______________________________________________<br>
Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br>