From 10dfb2fe496f0238cc55b0751ae37adf908bf3f3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 19:01:42 -0700 Subject: [PATCH] Update "church encoding" article to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/lambda_calculus_integers.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/blog/lambda_calculus_integers.md b/content/blog/lambda_calculus_integers.md index 9eabd2d..cb66578 100644 --- a/content/blog/lambda_calculus_integers.md +++ b/content/blog/lambda_calculus_integers.md @@ -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: