Conditions and Booleans
-----------------------
We will use the convention that first is TRUE and second is FALSE.
This is not "weird" when you think of it. We tend to use TRUE and
FALSE but represent true as an odd number (1 in least significant
position) and false as an even number (0 in least significant
position). We could just as well say that TRUE is elephant and
FALSE is zebra. These are just conventions!

- val first = fn x => fn y => x;
val first = fn : 'a -> 'b -> 'a
- val second = fn x => fn y => y;
val second = fn : 'a -> 'b -> 'b

- val TRUE = first; (* true = Lx.Ly.x *)
val TRUE = fn : 'a -> 'b -> 'a

- val FALSE = second; (* false = Lx.Ly.y *)
val FALSE = fn : 'a -> 'b -> 'b

NOTE: I have to use TRUE (rather than true) and FALSE (rather
than false), since true/false are reserved in ml.

Generally we have "if C then E1 else E2" where C is a condition
(boolean expression) and E1 and E2 are expressions. We can "step
side-ways" and allow ourselves a function "cond E1 E2 C" which
delivers as a result E1 if C is TRUE, and E2 if C is FALSE:

  cond = Le1.Le2.Lc.((c e1) e2)

- val cond = fn E1 => fn E2 => fn c => ((c E1) E2);
val cond = fn : 'a -> 'b -> ('a -> 'b -> 'c) -> 'c

Remember that TRUE = first and FALSE = second. 
Therefore lets see what happens when we have the following
examples:

   (((cond a) b) TRUE)
   => (((Le1.Le2.Lc.((c e1) e2) a) b) TRUE)
   => ((Le2.Lc.((c a) e2) b) TRUE)
   => (Lc.((c a) b) TRUE)
   => (Lc.((c a) b) Lx.Ly.x)
   => ((Lx.Ly.x a) b)
   => (Ly.a b)
   => a

   (((cond a) b) FALSE)
   => (((Le1.Le2.Lc.((c e1) e2) a) b) FALSE)
   => ((Le2.Lc.((c a) e2) b) FALSE)
   => (Lc.((c a) b) FALSE)
   => (Lc.((c a) b) Lx.Ly.y)
   => ((Lx.Ly.y a) b)
   => (Ly.y b)
   => b

- (((cond 1) 2) TRUE);
val it = 1 : int
- (((cond 1) 2) FALSE);
val it = 2 : int

Clearly, if we have cond (if ... then ... else) the world opens
up! We should now be able to implement NOT, AND, OR with relative
ease. For example we could consider the following:

   NOT  if E1 then FALSE else TRUE
   AND  if E1 then E2 else FALSE
   OR   if E1 then TRUE else E2

The Lambda and ml equivalents are therefore as follows:

  NOT = Lx.(((cond FALSE) TRUE) x)

- val NOT = fn x => (((cond FALSE) TRUE) x);
val NOT = fn : (('a -> 'b -> 'b) -> ('c -> 'd -> 'c) -> 'e) -> 'e
- (NOT TRUE);
val it = fn : 'a -> 'b -> 'b
- T;
val it = fn : 'a -> 'b -> 'a
- (NOT FALSE);
val it = fn : 'a -> 'b -> 'a

  AND = Lx.Ly.(((cond y) FALSE) x)

- val AND = fn x => fn y => (((cond y) FALSE) x);
val AND = fn : ('a -> ('b -> 'c -> 'c) -> 'd) -> 'a -> 'd
- ((AND TRUE) TRUE);
val it = fn : 'a -> 'b -> 'a
- ((AND TRUE) FALSE);
val it = fn : 'a -> 'b -> 'b

  OR = Lx.Ly.(((cond TRUE) y) x)

- val OR = fn x => fn y => (((cond TRUE) y) x);
val OR = fn : (('a -> 'b -> 'a) -> 'c -> 'd) -> 'c -> 'd
- ((OR FALSE) TRUE);
val it = fn : 'a -> 'b -> 'a
- ((OR TRUE) FALSE);
val it = fn : 'a -> 'b -> 'a
- ((OR FALSE) FALSE);
val it = fn : 'a -> 'b -> 'b


Look Back at pair
-----------------
If we look back to the earlier section "Making pairs from two
arguments" we introduced the two functions first and
second, and the function pair:

   pair = Lx.Ly.Lf.((f x) y)

In this section we have introduced the conditional cond:

   cond = Le1.Le2.Lc.((c e1) e2)

and adopted the convention of TRUE = first, and FALSE = second.
This has allowed us to then define negation, disjunction, and
conjunction. This is all that is required within Boolean
Algebra. In fact, we have described Boolean Algebra in terms of
"pair", "first", and "second". This is somewhat surprising.

Generally it is better to define or conditional statement more
conventionally, in terms of IF

       IF = Lc.Le1.Le2.((c e1) e2)

   and in ml

   val IF = fn c => fn e1 => fn e2 => ((c e1) e2);

Therefore a more conventional definition of NOT, AND, and OR is
as follows:

      NOT = Lx.(((IF x) FALSE) TRUE)
      AND = Lx.Ly.(((IF x) y) FALSE)
      OR  = Lx.Ly.(((IF x) TRUE) y)

(********************** ml source *****************************)

val TRUE = fn x => fn y => x;
val FALSE = fn x => fn y => y;

val IF = fn c => fn e1 => fn e2 => ((c e1) e2);

val AND = fn x => fn y => (((IF x) y) FALSE);
val OR = fn x => fn y => (((IF x) TRUE) y);
val NOT = fn x => (((IF x) FALSE) TRUE);


(*
   (not true)
   => (Lx.(((IF x) false) true) true)
   => (((IF true) false) true)
   => (((Lc.Le1.Le2.((c e1) e2) true) false) true)
   => ((Le1.Le2.((true e1) e2) false) true)
   => (Le2.((true false) e2) true)
   => ((true false) true)
   => ((Lx.Ly.x false) true)
   => (Ly.false true)
   => false => Lx.Ly.y

*)

(* Implication is defined as follows:

     X       Y    X implies Y
   -----   -----  -----------
   false   false     true
   false   true      true
   true    false     false
   true    true      true

Write a lambda function 

      implies = Lx.Ly.<body>

*)

val implies = fn x => fn y => (NOT ((AND x) (NOT y)));

(*
 The above is possible given the definitions of TRUE, FALSE,
 AND, OR, NOT, and IF. This allows all of propositional logic.
*)