Ī step of computation in lambda calculus is called beta-reduction. We will also eschew parentheses for nested abstractions, e.g. However, we might need parenthesis around the whole abstraction itself. Since application binds more tightly, we don’t need parentheses around the body of an abstraction. f f f is applied to a a a, then the result is applied to b b b, then to c c c. Hence, f a b c f\ a\ b\ c f a b c is ( ( f a ) b ) c ((f\ a)\ b)\ c (( f a ) b ) c, i.e. We’ll use parentheses where necessary to avoid it.Īdditionally, we will assume that application is left-associative and binds more tightly than abstractions. You might notice that using whitespace can lead to ambiguity.
Since all abstractions are univariate by definition, there’s no special syntax for multivariate application. In the standard notation, application is denoted simply by whitespace.įor example, f x f\ x f x is the application of f f f to x x x. It’s the only operation defined in the pure untyped lambda calculus. Īpplication is the operation of substituting a specific value for the parameter in the abstraction. Here we’ll be using the equals sign ( =) for that.įor example: i d = λ x. z are not.Īnd, as usual in abstract mathematics, we can assign a name to an expression. The choice of bound variable names is arbitrary.Įxpressions that differ only in the names of bound variables are called alpha-equivalent.įor example, λ x. is a combinator because x x x, y y y, and z z z are bound in one of the outer (relative to their use) abstractions.
Lambda calculus beta reduction examples free#
introduces) it before it is used.Īn expression without free variables is called a closed term or a combinator.įor example, the expression λ x. … z is also free, because no abstraction binds (i.e. The last variable z z z in the outer abstraction λ y. Variables y, y, y, z z z in the body of the inner abstraction ( x y z ) (x\ y\ z) ( x y z ) are bound in this expression. Other variables are called free variables. Variables in the body of an abstraction that are parameters of said abstraction are called bound variables. However, there’s some evidence (Cardone, 2006) that the notation was derived from x ^ \hat x x ^ used for class abstraction by Whitehead and Russell in Principia Mathematica, morphing first into Λ x \Lambda x Λ x and later into λ x \lambda x λ x. Lambda calculus derives its name from the λ \lambda λ symbol used in this notation.Ĭhurch has stated a couple times the symbol was chosen arbitrarily. The head contains the λ \lambda λ symbol and the argument name.įor example, λ x. We introduce new abstractions using the λ \lambda λ symbol.Īn abstraction consists of a head and a body, separated by the dot (. Lambda calculus only defines univariate (single-variable) functions, but we can easily extend it to include multivariate functions too, as we’ll see later. In the mid-1960s, Peter Landin showed that lambda calculus models arbitrarily complex programming languages.Īrguably, this insight kickstarted the research on functional programming languages.Īn abstraction, or a functional abstraction, is a parametric expression, that is to say, a function. It has weaker expressive power, but it’s logically consistent. Later, in 1940, a typed version of lambda calculus based on Russel’s type theory was introduced. This isolate is now known as the untyped lambda calculus. To sidestep this issue, Church isolated the part of lambda calculus relevant only to computation in 1936. The initial formulation had a logical inconsistency known as the Kleene–Rosser paradox (Cantini, 2007). Lambda calculus, initially envisioned as a formal logic system, was developed by Alonzo Church around the 1930s to explore the foundations of mathematics. – James Iry, A Brief, Incomplete, and Mostly Wrong History of Programming Languages This criticism occurs in spite of the fact that C has not yet been invented. His lambda calculus is ignored because it is insufficiently C-like.
1936 - Alan Turing invents every programming language that will ever be but is shanghaied by British Intelligence to be 007 before he can patent them.ġ936 - Alonzo Church also invents every language that will ever be but does it better.
0 kommentar(er)
