If-Then-Else in Church Encoding

Below are the λ expressions that we used to encode the Boolean constants and one Boolean operator:

   • TRUE = λx.λy.x
   • FALSE = λx.λy.y
   • AND = λp.λq.((p q) FALSE)

Suppose that we now want to encode a representation of the if/then/else expression as a function of three arguments. The first argument is the representation of the Boolean value that makes up the condition to be tested. The second argument is the value of the if/then/else expression when the Boolean condition evaluates to true. The third argument is the value of the if/then/else expression when the Boolean condition evaluates to false. Which one of the following encodings achieves this goal?

IF = λb.λx.λy.((b x) y)

```
IF = λb.λx.λy.(b (x y))
```
```
IF = λb.λx.λy.(b (y x))
```
```
IF = λb.λx.λy.((b y) x)
```

Recall that, in the chosen encoding, TRUE is a curried function of two arguments that returns its first argument.

Similarly, FALSE is a curried function of two arguments that returns its second argument.

Observe that IF is a curried function of three arguments, namely a Boolean expression, the value of the then expression, and the value of the else expression, in this order.

Pick the expression that implements the semantics of the if/then/else expression using appropriate function calls in the λ calculus, given the above conventions.