The only thing we can do in the lambda calculus is define functions. Therefore, data types such as booleans, integers, or anything else are encoded into particular choices of functions. Any choice of encoding is possible, but for the data types to work, we need to be able to define operations that do the things we would normally expect to be able to do with that data type.

The following is how boolean values are typically encoded in the lambda calculus: T = (xy.x)

F = (xy.y) Here is a definition of the boolean function NOT:

(x.x(uv.v)(ab.a)) Here is the same NOT in syntax that you can type into the online interpreter:

(lambda x . (x (lambda u v . v) (lambda a b . a)))

(a): Write the lambda expression for NOT F. (Write the expression that would compute NOT F, not the result of the computation.)

(b): Show step-by-step how the term for NOT F that you gave in (a) reduces. Hint: It should reduce to T!(c): Why does this definition of NOT work?

Hint: You may want to refer to slides 12-15 from the lecture that explain why AND works, and/or section 3.1 in the R. Rojas tutorial. It may also be useful to notice that NOT = (x.x(uv.v)(ab.a)) = (x.xFT).