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. *) 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. *)