introduce

The λ calculus is a formal system developed from mathematical logic with rules for binding and substituting variables to study how functions are abstractly defined, how they are applied, and recursively. It was first published in the 1930s by mathematician Alonzo Church. Lambda calculus, as a widely used computing model, can clearly define what is a computable function, and any computable function can be expressed and evaluated in this form, it can simulate the calculation process of a single tape Turing machine; Nevertheless, the lambda calculus emphasizes the application of transformation rules rather than the specific machine that implements them.

Grammar rules

grammar The name of the example instructions
Variable (variable) x The variable named x
Lambda. Function (function) Lambda 7.0.x.x A complete function definition with parameter x and body x.
Application (application) M N Function M applied to parameter N

Free variables and bound variables

λx.xy, where x is a bound variable and y is a free variable

The rules

Alpha transformation

The alpha transform, in which function variable names can be replaced at will, is mainly used to solve the problem of variable name conflicts in expressions. (note: ≡ This symbol means congruence, perfect equivalence)

λx.x ≡ λy.y

 // js

(x => x) === (y => y)
Copy the code

Beta reduction

Replacing parameters in a function with arguments is the process of applying the function abstraction to parameters, called a function call.

(lambda 7.0.x.x) ≡ y y (lambda 7.0.x.x y) (a) (b) ≡ y/b/a js (x = > x) (y) = = = y (x = > x) (a) (b) = = = a (b)Copy the code

For the expression (λ x.xy)((λz.z)s), you can specify (λz.z)s first and then λ x.xy β, or (λ x.xy β first and then λz.z)s β. Since they are pure functions with no side effects, they are not in order.

Eta transform

There is such a function λ x.mx that when applied to the parameter N, (λ x.mx)N. β becomes M N, it shows that M ≡ (λ x.mx).

For λ x.mx, where the expression M does not contain the function abstraction of the binding variable x, it is redundant. This simplification is called the ETA transform. It is generally used to remove redundant function abstractions in λ expressions.

let fn  = (a) => ((b) => 'foo'))(a)
let fn2 = () => 'foo'

fn(1) // 'foo'
fn2() // 'foo'
Copy the code

To avoid ambiguity

For example, for λx. xy, it can represent either (λx.x)y or λx.(x y), according to the syntax.

In addition to using parentheses to make expressions more explicit, we can also define two disambiguation conventions:

  • The body of a function abstraction will expand to the right as far as possible, that isLambda 7.0.x.x yIt represents a functional abstractionLambda x. (x, y)Not function applicationsY (lambda 7.0.x.x)
  • Function applications are left associative,X Y Z meaning(X Y) ZRather thanX (Y Z)

For ease of reading, I’ll separate variables with Spaces, and for functions like λx.M(N), I’ll write lambda x.M in some places.

Let M = λx.x M is an alias for the function λx.x.

In addition, if a variable appears in a λ expression in uppercase, it is a function alias.

Currie,

Functions in Lambda calculus can take only one argument. So for an addition function, it should be written like this

λa.λ b.plus a b // js const fn = a => b => PLUS(a, b)Copy the code

Since Lambda calculus has only functions and no operators, here we use the function PLUS to represent adding two numbers.

We can easily convert a multi-parameter function to a single-parameter function by means of currization.

const curry = (f) => { let args = []; const g = (x) => { args.push(x) if (args.length === f.length) { return f(... args) } else { return g } } return g } const plus = (a, b) => a + b const f = curry(plus) f(1)(2) // 3Copy the code

In a λ expression, the single-parameter form of a function is not as readable as the multi-parameter form. With the help of Coriolization, the following functions in a λ expression will be written in the multi-parameter form for readability.

Conditional branch

In JS, we have ternary operators

(condition, a, b) => condition ? a : b
Copy the code

In the above function, we find that condition is true if it returns a. Condition is false if b is returned.

So, in lambda, we can define Bool like this. If a function takes two arguments, it is considered TRUE if it always returns the first argument, and FALSE if it always returns the second argument

Let TRUE = λx y.x let FALSE = λx y.y let TRUE = (x, y) => x let FALSE = (x, y) => yCopy the code

Now we can write an IF function whose first argument is a conditional expression, the second argument is the expression to be evaluated IF the condition is true, and the third argument is the operation to be evaluated IF the condition is false.

Let IF = λc t f f (IF)(TRUE a b) ≡ (λc t f F)(TRUE a b) ≡ TRUE a b ≡ (λx y.x)(a b) ≡ a // js (a, b) => TRUE? a : b (a, b) => ((x, y) => x)(a, b)Copy the code

We can continue to define and or not

Let AND = λx y.x FALSE let OR = λx y.x TRUE y let NOT = λx.x FALSE // example AND TRUE FALSE ≡ (λx y.x FALSE)(TRUE FALSE) ≡ TRUE FALSE FALSE ≡(λx y.x)(FALSE FALSE) ≡ FALSE OR FALSE TRUE ≡(λx y.x TRUE y)(FALSE TRUE) ≡ FALSE TRUE TRUE ≡ (λx y.x)(TRUE FALSE) ≡ TRUE NOT TRUE ≡ (λx.x FALSE TRUE)(TRUE) ≡ TRUE FALSE TRUE ≡ (λx y.x)(FALSE TRUE) ≡ FALSE NOT FALSE ≡ (λx.x FALSE TRUE)(FALSE) ≡ FALSE FALSE TRUE ≡ (λx y.y)(FALSE TRUE) ≡ TRUECopy the code

Number of church

Now that we’ve defined booleans and some logical operators, let’s define natural numbers.

For the definition of natural numbers, refer to peano’s axiom.

These five axioms of Piano are stated unformally as follows:

  1. 0 is a natural number;
  1. For every certain natural number a, there is a certain successor a’, which is also a natural number;
  1. For each natural number b and c, b=c if and only if the successors of B = the successors of C;
  1. 0 is not the successor of any natural number;
  1. Any statement about natural numbers can be proved to be true for a’ if it is proved that it is true for the natural number 0 and assumed to be true for the natural number A. So, the statement is true for all natural numbers.

To put it simply, 0 is a natural number, 0 has a certain successor 1, and 1 has a certain successor 2. And so on…

Now we can define a successor function S that takes a natural number and returns the successor of that natural number. Then the natural numbers can be expressed in the following way

0
1 = S(0)
2 = S(1) = S(S(0))
3 = S(2) = S(S(1)) = S(S(S(0)))
 // ...
Copy the code

In the lambda calculus, we can represent the above code like this

Let ONE = λs z.s(z) let TWO = λs z.s(s(z)) let THREE = λs z.s(s(z))Copy the code

A good way to think about it is to use z as the name for the zero value and s as the name for the subsequent function.

Thus, 0 is a function that only returns the value “0”; 1 is the function that applied a subsequent function to 0 last time;

2 is the function that applies a successor to the successor of 0, and so on.

In js we’ll write it this way

let ZERO = (s, z) => z
let ONE = (s, z) => s(z)
let TWO = (s, z) => s(s(z))
let THREE = (s, z) => s(s(s(z)))

let s = n => n + 1
let convert = f => f(s, 0)

convert(ZERO) // ZERO(s, 0) === 1
convert(ONE) // ONE(s, 0) === 1
convert(TWO) // TWO(s, 0) === 1
convert(THREE) // THREE(s, 0) === 1
Copy the code

To get the natural number N, we simply apply the successor function S to 0 N times.

The above ONE, TWO and THREE are all listed manually.

Our ONE should be accessible by S(ZERO).

The successor function S here can be expressed as λ

Let S = lambda x y z.y (x, y, z) S (ZERO) ≡ (lambda x y z.y (x, y, z)) (lambda sz. Z) / / alpha transformation: (lambda ab. B) = (lambda sz. Z) ≡ (lambda x y z.y (x, y, z)) (lambda ab. B) / / beta code: x = (lambda ab. B) ≡ lambda y z.y (lambda ab. B) y (z) / / beta code: A = y, b = z ≡ λy z.y(z) // // α transform: Z.s lambda s (z) = lambda y z.y (z) ≡ lambda s z.s (z) / / ONE / / js let s = n = > n + 1 let the convert = f = > f (s) (0) let s = n = > (s, z) => s(n(s, z)) let ONE = S(ZERO) convert(ONE) // 1Copy the code

add

Now that we have numbers, we have to define addition, subtraction, multiplication and division.

The implication of addition is that for 2 + 3 = 5, we only have to apply S to 2 3 times to get 5.

Let PLUS = λx y s z.x s(y s z) ≡ λx y.λs z.x s(y s z) let TWO = λs z.s(s(z)) let THREE = λs z.s(s(z)) PLUS TWO THREE ≡ (λx y.λs z.x s (y s z))(TWO THREE) // β specification: X = TWO, y = THREE ≡ λs z.TWO s (THREE s z) Do alpha ≡ lambda s z. (lambda s2 z2. S2 (s2) (z2)) s ((lambda s3 z3. S3 (s3 (s3 (z3)))) s (z) / / beta code: s3 = s, Z3 ≡ lambda s = z z. (lambda s2 z2. S2 (s2) (z2)) s (s (s, s (z)))) / / beta code: s2 = s, Z2 = s (s) (s) (z) ≡ lambda s z.s (s (s, s (s) (z)))) / / js let PLUS = (x, y) = > (s, z) = > x (s, y, s, z)) let TWO = (s, z) => s(s(z)) let THREE = (s, z) => s(s(s(z))) let s = n => n + 1 let convert = f => f(s, 0) let FIVE = PLUS(TWO, Let PLUS = x => y => s => z => x(s)(y(s)(z)) let TWO = s => z => s(s(z)) let THREE = s => z => s(s(s(z))) let s = n => n + 1 let convert = f => f(s)(0) let FIVE = PLUS(TWO)(THREE) convert(FIVE) // 5Copy the code

Let ‘ ‘PLUS = λx y.x y. These two methods are equivalent

Let PLUS = λx y.x y ≡ λx y.x (λa S z.s(a S z)) y ≡ λx y.x (λ S z.s(y S z)) ≡ λx y.λ S z.x S (y S z) // Here is the same as the previous definition of the addition function PLUS ONE TWO ≡ (λx y.xs Y) (ONE TWO) ≡ ONE S TWO ≡ ONE (λx y z.y(x y z)) TWO ≡ ONE (λa b c.b(a b c)) TWO Z1. S1 (z1)) (lambda b a mount (a, b, c)) (lambda s2 z2. S2 (s2) (z2)) ≡ (lambda b a mount (a, b, c)) (lambda s2 z2. S2 (s2 z2)) / / s1 = b (lambda a mount (a, b, c)), / / z1 = (lambda s2 z2. S2 (z2) s2) ≡ b ((lambda s2 z2. S2 (s2) (z2)) b) c / / a = (lambda s2 z2. S2 (z2) s2) ≡ b (b) (c) (b) / / s2 = b, Z2 = C ≡ s(s(s)(z)) // => THREECopy the code

The multiplication

Let MULTIPLY = λx y s.x(y s) MULTIPLY ONE TWO ≡ (λx y s.x(y s)) (ONE TWO) ≡ λ s.ne (TWO s) // β: X = ONE, y = TWO ≡ lambda s. (lambda s1 z1. S1 (z1)) (lambda s2 z2. S2 (s2) (z2) s) / / alias substitution, at the same time do alpha transformation and beta: S2 = s ≡ lambda s. (lambda s1 z1. S1 (z1)) (lambda z2. S (z2) (s) / / beta: s1 = (lambda z2. S (z2) (s)) ≡ lambda s. lambda z1. (lambda z2. S (z2) (s) (z1) / / beta: Z2 = z1 ≡ lambda s. lambda z1) s (z1) (s) / / alpha: lambda z.s (s) (z) = lambda z1) s (s) (z1) ≡ lambda s. lambda z.s (s) (z) / / TWOCopy the code

See the following figure for more function definitions

cycle

First, all loops can be replaced by recursion. Can all loops be replaced by recursion? – zhihu

Recursion means “a function calls itself directly or indirectly.” In a programming language, a function calls itself by holding a “reference to itself,” which is the name of the function.

In lambda calculus, all functions are anonymous, so how do we refer to themselves?

The answer is Y Combinator.

Y Combinator is used to calculate fixed points of (higher-order) functions, which allows an anonymous function to get itself from Y Combinator and call itself later, thus achieving recursion.

The fixed point

The fixed point of the function f is that applying the function to the input value x returns the same value as the input, such that f(x) = x. For example, 0 and 1 are fixed points of the function f(x) = x^2, because 0^2 = 0 and 1^2 = 1. Since the fixed point of a first-order function (on simple values such as integers) is a first-order value, the fixed point of a higher-order function f is another function g such that f(g) = g. The Y combinator can compute this fixed point g, so g is equal to Y (f), and if we plug in g we get Y (f) is equal to f(Y (f)).

Y Combinator profile

Y Combinator was discovered by Haskell B. Curry. It looks like this in terms of the expression λf.λx.(f(x x))(λx.(f(x x)))

Function (f) {return (function (x) {return f(x))})(function (x) {return f(x))})} => (x => f(x(x)))(x => f(x(x))))Copy the code

This graph looks like an upside down Y, hence the name Y combinator.

Y Combinator derivation process

// If it is an anonymous function with no name, how can it recursively call itself? // Arguments. callee can be used, but for arrow functions, Function f(n) {if (n === 1) {return 1} return n * f(n-1)} // 2. We changed it to an anonymous function. Now we can't get a reference to itself by the function name. We hold a reference to it by argument function (f, Function (f) {return function (n) {if (n === 1) {return 1} return n * f(n-1)} function (f) {return function (n) {if (n === 1) {return n * f(n-1)} Return 1} return n * f(n-1)}} Take your time and read on // 3. After currization, this anonymous function becomes a higher-order function that accepts a function f that can compute factorials. // The function f used to compute the factorial, we can pass in the original naive factorial function, and for the sake of differentiation, G (function (f) {return function (n) {if (n === 1) {return 1} return n * f(n-1)}})(function g(n) {if (n === 1) {return 1} return n * f(n-1)}})(function g(n) {if (n === 1) {return 1} return n * g(n-1)}) Function (f) {return function (n) {if (n === 1) {return 1} So the call has changed // from n * f(n-1) to n * f(🤔, n-1) // so, what should we pass here 🤔? Return n * f(🤔, n-1)}})(function (g, n) {if (n === 1) {return 1} return n * g(n-1)}) It is an anonymous function and takes two arguments. // The first argument g is a factorials function, and the second argument is the number to compute the factorials. // So 🤔 is a factorials function. // the argument is passed in as the parameter f, F (function (f) {return function (n) {if (n === 1) {return 1} return n * f(f, n-1)}})(function (g, N) {if (n === 1) {return 1} return n * g(n-1)}) // Function (g, n) {if (n === 1) {return 1} return n * g(n-1)} N * g(n-1) = n * g(🤔, n-1) = n * g(🤔, n-1) (function (f) {return function (n) {if (n === 1) {return 1} return n * f(f, n - 1) } })(function (g, n) { if (n === 1) { return 1 } return n * g(g, n - 1) }) // 4. Now, we will make the argument function currified, and change the function name back to the original f, namely:  (function (f) { return function (n) { if (n === 1) { return 1 } return n * f(f)(n - 1) } })(function (f) { return Function (n) {if (n === 1) {return 1} return n * f(f)(n-1)}}) You will get 120 (function (f) {return function (n) {if (n === 1) {return 1} return n * f(f)(n-1)}})(function (f) { return function (n) { if (n === 1) { return 1 } return n * f(f)(n - 1) } })(5) // 5. So let's go ahead, we're going to layer IIFE on top of the result of the previous step, which obviously doesn't make any difference to the logic, Function () {(function (f) {return function (n) {if (n === 1) {return 1} return n * f(f)(n-1)} })(function (f) { return function (n) { if (n === 1) { return 1 } return n * f(f)(n - 1) } }) })() // 6. Function (g) {function (g) {function (g) {function (g) { Function (f) {return function (n) {if (n === 1) {return 1} return n * f(f)(n-1)}}) // 7. Const r = (function (g) {return g(g)})(function (f) {// Return function (x: number) {return (function () {// 👆👆👆 Number) {if (n === 1) {return 1} return n * f(f)(n-1)}})()(x)}}) // 8. Function (g) {return g(g)})(function (f) {return function (x: number) {return (function (factorial: (n:number) => number) { return function (n) { if (n === 1) { return 1 } return n * factorial(n - 1) } })(f(f))(x) } }) (5) / / 9. Function (factorial) {... } function (factorial) {// The y combinator is a general-purpose high-order function, so extract it again by wrapping function (factorial) {... Function (h) {return (function (g) {return g(g)})(function (f) {return h(f))(n)  } }) }(function (factorial) { return function (n) { if (n === 1) { return 1 } return n * factorial(n - 1) } }) // 10. Since it is also a higher-order function when extracted as an argument, H (g)) function (h) {return (function (g) {return h(g))})(function (f) {return function (n) { return h(f(f))(n) } }) }(function (factorial) { return function (n) { if (n === 1) { return 1 } return n * factorial(n - H -> f, g -> x, Const y = function (f) {return (function (x) {return f(x))})(function (x) { return function (n) { return f(x(x))(n) } }) } const fa = y(function (factorial) { return function (n) { if (n ===  1) { return 1 } return n * factorial(n - 1) } }) fa(5) // 11. You may notice that the y Combintor obtained in the previous step is a little different from the version I originally translated using the arrow function: (f = > = > f (x) (x (x)) (x = > f (x) (x))) / / arrow actually function of this code is not available, the reason is js immediately evaluation result in the stack, (function (f) {return (function (x) {return f(x))})(function (x) {// Because js is immediately evaluated, there is an overflow here. Function (n) {function(n) {... Return f(x(x))})})Copy the code

reference

  • Lambda Calculus 101: Definition and reduction
  • Numbers in alonzo Church’s genius lambda calculus
  • Church encoding – Wikipidia
  • Lambda Calculus – Learn X in Y minutes
  • You Can Explain Functional Programming Using Emojis
  • Golang description of Y-Combinator derivation
  • Fixed Point Combintor – Wikipedia