Booleans as lambda terms.md (2456B)
1 +++ 2 title = "Booleans as lambda terms" 3 +++ 4 5 # Booleans as lambda terms 6 Church's thesis: everything computable can be defined in pure untyped lambda calculus 7 8 ## Finding booleans 9 Try to find two different closed normal terms that let us calculate. 10 11 1. Two normal terms: x, y 12 2. Closed: λx.x, λy.y 13 - but these are alpha-equivalent! 14 3. Different: λx.y.x, λx.y.y 15 16 Therefore: 17 - true = λxy.x 18 - false = λxy.y 19 20 ## Negation 21 - not true =β false 22 - not false =β true 23 24 Deriving the definition for 'not': 25 26 ``` 27 (not) (true) 28 (λu.u__) (true) => replace the u with true. 29 true takes two arguments and returns first (by definition above). 30 therefore two arguments must be false, true. 31 ``` 32 33 ∴ not = λx.x false true 34 35 Verifying: 36 37 ``` 38 (not) (true) 39 => (λu.u false true) (true) 40 => (true) (false) (true) 41 => (λxy.x) (false) (true) 42 => false 43 not true == false, so definition is OK 44 ``` 45 46 ## Conjunction (AND) 47 Start with a truth table (specification): 48 49 ``` 50 and true true =β true 51 and true false =β false 52 and false true =β false 53 and false false =β false 54 ``` 55 56 We see that there are two arguments x and y. The value is given by the logical statement "if x then y otherwise false". So if the first argument is true, then the value depends on the truth value of the second argument. If the first argument is false, the whole thing is automatically false. 57 58 In lambda calculus: 59 60 `and := λxy.x y false` 61 62 Checking for correctness: 63 64 ``` 65 and false true = (λxy.x y false) (false) (true) 66 ⇒β (false) (true) (false) 67 = (λxy.y) (true) (false) 68 ⇒β false 69 false =β and false true 70 ``` 71 `` 72 This makes sense, so the definition is correct. 73 74 ## Disjunction (OR) 75 Start with a truth table (specification): 76 77 ``` 78 or true true =β true 79 or true false =β true 80 or false true =β true 81 or false false =β false 82 ``` 83 84 We see that there are two arguments x and y. The value is given by the logical statement "if x then true otherwise y". So if the first argument is true, the whole thing is automatically true. If the first argument is false, the value depends on the truth value of the second argument. 85 86 In lambda calculus: 87 88 `or := λxy.x true y` 89 90 Checking for correctness: 91 92 ``` 93 or false true = (λxy.x true y) (false) (true) 94 ⇒β (false) (true) (true) 95 = (λxy.y) (true) (true) 96 ⇒β true 97 true =β or false true 98 ``` 99 100 This makes sense, so the definition is correct.