Update "church encoding" article to new math delimiters

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 19:01:42 -07:00
parent ef76149112
commit 10dfb2fe49

View File

@ -135,7 +135,7 @@ Just like in our previous examples, we simply replace `f` with `double` during a
We've now created our multiply-by-four function! We can create other functions the same way. For instance, if we had a function `halve`, we could create a function to divide a number by 4 by applying our "apply-twice" function to it.
### Church Encoded Integers
We can represent numbers using just abstraction and application. This is called Church encoding. In church encoding, a number is a function that takes another function, and applies it that many times to a value. 0 would take a function and a value, and apply it no times, returning the value it was given. 1 would take a function `f` and a value `v`, and return the result of applying that function `f` one time: `f v`. We've already seen 2! It's a function that applies a function to a value twice, `f (f v)`. Let's write these numbers in lambda calculus: 0 becomes \\(\lambda \ f \ . \ \lambda \ x \ . \ x\\), 1 becomes \\(\lambda \ f \ . \ \lambda \ x \ . \ f \ x\\), and 2 becomes the familiar \\(\lambda \ f \ . \lambda \ x \ . \ f \ (f \ x)\\).
We can represent numbers using just abstraction and application. This is called Church encoding. In church encoding, a number is a function that takes another function, and applies it that many times to a value. 0 would take a function and a value, and apply it no times, returning the value it was given. 1 would take a function `f` and a value `v`, and return the result of applying that function `f` one time: `f v`. We've already seen 2! It's a function that applies a function to a value twice, `f (f v)`. Let's write these numbers in lambda calculus: 0 becomes \(\lambda \ f \ . \ \lambda \ x \ . \ x\), 1 becomes \(\lambda \ f \ . \ \lambda \ x \ . \ f \ x\), and 2 becomes the familiar \(\lambda \ f \ . \lambda \ x \ . \ f \ (f \ x)\).
Now, let's try represent addition. Addition of two numbers `a` and `b` would be done by taking a function `f` and applying it the first number of times, and then applying it the second number more times. Since addition must take in numbers `a` and `b`, which are functions of two variables, and return a number, we will end up with
something like this: