More concretely, to perform 2 + 3 you start with 2 fingers up, and add one finger three times. You start with a number of fingers up, and then you add one more finger as many times as the second number tells you. Think of how you used to add when you were a kid (if you are like me, you may still do it!). This insight allows us to define more complex operations on numbers, like addition. You can use a Boolean as a function to choose between two alternatives, and you can use a number as a function to repeat an operation. In the same way that Booleans directly encode conditional choice, Church numerals directly encode repetition. In case you’re not fully convinced, we can work out an example: addOne(two) = f => x => f(two(f)(x)) As we said, we need to apply f once more, but we need to remember to still pass f and x to the original number n! addOne is a function that accepts one Church numeral – the n – and gives back another numeral – hence the f => x => in the underlined section. To understand this code, let’s break it into pieces. For example, let’s build the function that represents the operation x => x + 1 the idea is that the resulting Church numeral should apply its f argument once more. One simple operation we can define is the addition of a constant number to a Church numeral. In other words, it should return the x untouched. Solution: The Church numeral for 0 must apply its argument f no times. Pause here for a minute and think how the number 0 would look in this encoding. You can surely see the pattern here: we have as many nested fs as the number we seek to represent. Let me show you how the numbers 1 to 3 are represented in this fashion: const one = f => x => f(x) In our case, this iteration is going to be done by repeatedly applying the same function. As in the case of Booleans, we are going to use a function of two arguments to represent each number the trick is to find something that we can somehow iterate. That’s a cool name, but the regular name for the representation of numbers in the lambda calculus is Church numerals, named after its creator Alonzo Church. using our definitions for if_, true_, and false_Ĭonst not = (a) => a(x => y => y)(x => y => x) Let’s simply replace each of the JavaScript components with those from lambda calculus. Solution: If we were to write this function using regular JavaScript, we would end up with something along the lines of the following code block. Would you be able to write the not function on Booleans? Victory! We were able to define the Boolean values, and their main operation – conditional choice – using only functions. This means cond is a function that accepts two arguments the exact arguments we have! The definition of if_ can then be refined to: const if_ = cond => a => b => cond(a)(b)ĭoes this work? Let’s try to compute with both choices of cond: // cond = true_ Here comes the magic trick! □ We know that cond is going to be one of our true or false Boolean values. All that we know at this point is the shape it should have: const if_ = cond => a => b => ? The conditional, which we usually represent as if (cond) a else b, also has to be represented as a function. Those functions can be defined using the blocks of lambda calculus: const true_ = x => y => x Note that we could reverse the particular choice for true and false we only need to be consistent. The output of this gate comes from one of the wires which one it is depends on the Boolean value. In our encoding, each Boolean value is thought of as a “gate” with two wires. In fact, to reconcile both views, we are going to work with the logic gate analogy. This point of view is quite different from looking at Booleans as tiny objects – true or false, high or low voltage. Boolean valuesĮverything in lambda calculus is a function at the end of the day. Then we’ll introduce Church numerals to encode numbers. Now, in this post, we are going to continue our journey by looking at conditionals first. The previous post in this series introduced the constraints we had to obey to use JavaScript as untyped lambda calculus, and then we relaxed some of those constraints via currying (for functions of more than one argument) and translation (to turn const local variables into a combination of functions). This article was originally published at on January 7, 2021.
0 Comments
Leave a Reply. |