Lambda, wikipedia abstract to jog my memory every now and then on the notation, terms/words/lexicon, meaning of symbols etc.

1.asciidoc

Computable functions are a fundamental concept within computer science and mathematics. And there are analytical techniques that can only be applied to functions with a single argument.

Practical functions frequently take more arguments than this. Frege showed that it was sufficient to provide solutions for the single argument case, as it was possible to transform a function with multiple arguments into a chain of single-argument functions instead. This transformation is the process now known as `currying'.

Currying is similar to the process of calculating a function of multiple variables for some given values on paper.

For example, given the function f(x,y) = y / x:

To evaluate f(2,3), first replace x with 2 Since the result is a function of y, this new function g(y) can be defined as g(y) = f(2,y) = y/2 Next, replace the y argument with 3, producing g(3) = f(2,3) = 3/2 On paper, using classical notation, this is usually done all in one step. However, each argument can be replaced sequentially as well. Each replacement results in a function taking exactly one argument. This produces a chain of functions as in lambda calculus, and multi-argument functions are usually represented in curried form.

The λ-calculus provides a simple semantics for computation, enabling properties of computation to be studied formally. The λ-calculus incorporates two simplifications that make this semantics simple. The first simplification is that the λ-calculus treats functions "anonymously", which means without giving explicit names. For example, the function:

\[squareSum(x, y) = x \times x + y \times y\]

can be rewritten in anonymous form as:

\[(x, y) \rightarrow x \times x + y \times y\]

(read as "\(the pair of x and y is mapped to x \times x + y \times y\)"). Similarly,

\[id(x) = x\]

can be rewritten in anonymous form as \(x \mapsto x\), where the input is simply mapped to itself.

The second simplification is that the λ-calculus only uses functions of a single input. An ordinary function that requires two inputs, for instance the \(\operatorname{square\_sum}\) function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts a single input. For example,

\((x, y) \mapsto x \times x + y \times y\)

can be reworked into

\(x \mapsto (y \mapsto x \times x + y \times y)\)

This method, known as currying, transforms a function that takes multiple arguments into a chain of functions each with a single argument.

Function application of the \(\operatorname{square\_sum}\) function to the arguments (5, 2), yields at once

\[((x, y) \mapsto x \times x + y \times y)(5, 2) = 5 \times 5 + 2 \times 2 = 29\]

whereas evaluation of the curried version requires one more step

\[((x \mapsto (y \mapsto x \times x + y \times y))(5))(2) = (y \mapsto 5 \times 5 + y \times y)(2) = 5 \times 5 + 2 \times 2 = 29\]

to arrive at the same result.

Formal definition

Definition

Lambda expressions are composed of:

1. variables v1, v2, …​, vn, …​ (usually x, y and z)

2. the abstraction symbols lambda λ and dot .

3. parentheses ( (open) and ) (close) used for grouping operations or (order of precedence)

The set of lambda expressions, Λ (capital λ), can be defined inductively:

1. If x is a variable, then x ∈ Λ (if x is a variable then x is part of the set of lambda expressions)

2. If x is a variable and M ∈ Λ, then (λx.M) ∈ Λ (if x is a variable and a lambda expression M is part of the set of lambda expressions, then x is a bound variable in the lambda expression scope)????

3. If M, N ∈ Λ, then (M N) ∈ Λ (is this M(N)? or M N = (M N) right? I guess the comma, which isn’t explained means summary…​

Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications

Notation

To keep the notation of lambda expressions uncluttered, the following conventions are usually applied.

1. Outermost parentheses are dropped: M N instead of (M N)

2. Applications are assumed to be left associative: M N P may be written instead of ((M N) P)

3. The body of an abstraction extends as far right as possible: λx.M N means λx.(M N) and not (λx.M) N

4. A sequence of abstractions is contracted: λx.λy.λz.N is abbreviated as λxyz.N