added proto-monad

[lambda.git] / curry-howard

diff --git a/curry-howard b/curry-howard
index 7840e37..f3c1be7 100644 (file)
--- a/curry-howard
+++ b/curry-howard
@@ -139,4 +139,28 @@ show beta reduction, so "normal" proof.
 
 [To do: add pairs and destructors; unit and negation...]
 
 
 [To do: add pairs and destructors; unit and negation...]
 

-Excercise: construct a proof whose labeling is the combinator S.
+Excercise: construct a proof whose labeling is the combinator S,
+something like this:
+
+           --------- Ax  --------- Ax   ------- Ax
+           !a --> !a     !b --> !b      c --> c
+           ----------------------- L->  -------- L!
+              !a,!a->!b --> !b          !c --> c
+--------- Ax  ---------------------------------- L->
+!a --> !a           !a,!b->!c,!a->!b --> c
+------------------------------------------ L->
+      !a,!a,!a->!b->!c,!a->!b --> c
+      ----------------------------- C!
+       !a,!a->!b->!c,!a->!b --> c
+       ------------------------------ L!
+       !a,!a->!b->!c,! (!a->!b) --> c
+       ---------------------------------- L!
+       !a,! (!a->!b->!c),! (!a->!b) --> c
+       ----------------------------------- R!
+       !a,! (!a->!b->!c),! (!a->!b) --> !c
+       ------------------------------------ R->
+       ! (!a->!b->!c),! (!a->!b) --> !a->!c
+       ------------------------------------- R->
+       ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
+       --------------------------------------- R->
+        --> ! (!a->!b)->! (!a->!b->!c)->!a->!c