λ Tony’s blog λ

Conjunction
P  Q  P∧Q
0  0  0
0  1  0
1  0  0
1  1  1

Implication
P  Q  P→Q
0  0  1
0  1  1
1  0  0
1  1  1

1  2  3  4    5        6    7      8

A  B  C  A∧B  (A∧B)→C  B→C  A→B→C  ((A∧B)→C)→A→B→C
0  0  0  0    1        1    1      1
0  0  1  0    1        1    1      1
0  1  0  0    1        0    1      1
0  1  1  0    1        1    1      1
1  0  0  0    1        1    1      1
1  0  1  0    1        1    1      1
1  1  0  1    0        0    0      1
1  1  1  1    1        1    1      1

Prelude> :type curry
curry :: forall a b c. ((a, b) -> c) -> a -> b -> c

interface Implication<P, Q> {
  Q implies(P p);
}
 
interface Conjunction<P, Q> {
  P p();
  Q q();
}

class S {
  static <A, B, C> Implication<Implication<Conjunction<A, B>, C>, Implication<A, Implication<B, C>>> s() {
    return null; // todo
  }
}

8 Responses to “Proving the existence of curry”

1. Pseudonym Says:
   September 5th, 2008 at 11:33 am

   Be careful using truth tables. A theorem which is true in Boolean logic may not be true in a topos, and in intuitionistic logic in particular.

2. DavidLG Says:
   September 5th, 2008 at 7:55 pm

   The statement can be quickly proved without a truth table.

   a->b is logically the same as (!a + b), meaning (not a) or b. So the statement in question is !(!(ab) + c) + (!a + (!b + c)), which simplifies with one application of de Morgan’s law to (ab + !c + !a + !b + c), which is obviously true.

   What does the Java snippet show? Do the Implication and Conjunction interfaces have any semantics, or are they interchangeable? How many implementations of static X foo() are there, and why is your method more interesting? I guess I must be missing your point, I’m just a Scala programmer.

3. DavidLG Says:
   September 5th, 2008 at 7:57 pm

   (That was supposed to be static <X> X foo().)

4. Tony Morris Says:
   September 5th, 2008 at 8:04 pm

   David,
   There are many methods of proof, but the point is really the relationship to C-H. I am often faced by people who are baffled by the implication symbol in type signatures and I think it is demystified a little by pointing out its relationship to a simple boolean operator.

5. Pseudonym Says:
   September 5th, 2008 at 9:14 pm

   DavidLG: Even without a truth table, in intuitionistic logic, !!a does not necessarily imply a (though a does imply !!a). This is a direct consequence of not including the law of the excluded middle as an axiom.

6. Apocalisp Says:
   September 6th, 2008 at 12:59 am

   Pseudonym: That’s not not utter nonsense.

7. Bobby Moretti Says:
   September 6th, 2008 at 11:35 am

   @Apocalisp: double negation doesn’t always work so well. You picked a rather specific example. You can think of other ones that are a lot more gray. For example, suppose P stands for “Jim Bob is a likable fellow”.

   Then consider !!P: ‘it’s not the case that Jim Bob is not a likable fellow’. If we allow this form of double negation rule, then this would imply P, or ‘Jim Bob is a likable fellow.’ But can we really infer that? It might be the case that everyone is ambivalent towards Jim Bob: he’s kinda likable, but also kinda unlikable.

   The problem with the !!P |– P form of double negation is that assumes that P is either true or false; there’s no middle ground. That’s what’s known as the law of excluded middle. So there are systems of logic (such as the one that Pseudonym is referring to) that deal with more truth values than just purely true and purely false.

8. Daniel Jimenez Says:
   September 13th, 2008 at 3:47 am

   So I took a crack at implementing S.s (see below).

   I think I understand it: return an implication that, given an implication from a conjunction, returns an implication to an implication.

   My implementation just solves the type signatures, which wasn’t very hard. I don’t like that the two definitions of A (one is an argument to implies, one is an argument to and) aren’t referring to each other, though. I tried to write S.s1 and S.s2 to isolate it but couldn’t quite tie them together.

   Another place where I had trouble understanding it was in the call to what S.s returns. As can be seen from my Call.call, I’m hardcoding the return values of the conjunction and the initial implication. But I want to say that the implication from a conjunction only makes sense if you have both parts of the conjunction, and returning a hardcoded b for any a doesn’t seem right in that way.

   Worse, I end up passing b twice, once hardcoded as the return value from the conjunction, and once when calling the original method.

   Where did I go wrong? I’m pretty sure it’s my understanding of Conjunction that’s incorrect here (I remember and understand first-order logic just fine, I mean how those definitions apply to this Java code).

   // curry.java
   interface Implication<P, Q> {
    Q implies(P p);
   }

   interface Conjunction<P, Q> {
    Q and(P p);
   }

   class S {
    /**
     * return an implication that, given an implication from a conjunction, returns an implication to an implication
     * given: (A^B)->C, return: A->(B->C), overall: [(A^B)->C] -> [A->(B->C)]
     */
    static <A, B, C> Implication<Implication<Conjunction<A, B>, C>, Implication<A, Implication<B, C>>> s() {
     return new Implication<Implication<Conjunction<A, B>, C>, Implication<A, Implication<B, C>>>()
     {
      public Implication<A, Implication<B, C>> implies(final Implication<Conjunction<A, B>, C> i) {
       return new Implication<A, Implication<B, C>>()
       {
        public Implication<B, C> implies(final A a) {
         return new Implication<B, C>()
         {
          public C implies(final B b) {
           return i.implies(new Conjunction<A, B>()
           {
            public B and(A a) {
             return b;
            }
           });
          }
         };
        }
       };
      }
     };
    }
    static <A, B, C> Implication<A, Implication<B, C>> s1(final Implication<Conjunction<A, B>, C> i) {
     return new Implication<A, Implication<B, C>>()
     {
      public Implication<B, C> implies(final A a) {
       return new Implication<B, C>()
       {
        public C implies(final B b) {
         return i.implies(new Conjunction<A, B>()
         {
          public B and(A a) {
           return b;
          }
         });
        }
       };
      }
     };
    }
    static <A, B, C> Implication<B, C> s2(final A a) {
     return new Implication<B, C>()
     {
      public C implies(final B b) {
        throw new Error(); // surely not correct, but I’m stuck here
        // s2(a).implies(conj.and(a))
      }
     };
    }
   }

   class Call {
    static int call(final boolean a, final String b, final int c) {
     Conjunction<Boolean, String> and = new Conjunction<Boolean, String>() {
      public String and(Boolean p) {
       return b;
      }
     };
     Implication<Conjunction<Boolean, String>, Integer> from = new Implication<Conjunction<Boolean, String>, Integer>() {
      public Integer implies(Conjunction<Boolean, String> conjunction) {
       return c;
      }
     };
     Implication<Implication<Conjunction<Boolean, String>, Integer>, Implication<Boolean, Implication<String, Integer>>> s = S.s();
     Implication<Boolean, Implication<String, Integer>> to = s.implies(from);
     return to.implies(a).implies(b);
    }
   }

   public class curry {
     public static void main( String[] args ) {
       int result = Call.call(true, "two", 0);
       System.out.println("call(true, \"two\", 0)=" + result);
     }
   }

Leave a Reply