Misplaced Pages

#66933

78-419: Lambda calculus consists of constructing lambda terms and performing reduction operations on them. In the simplest form of lambda calculus, terms are built using only the following rules: The reduction operations include: If De Bruijn indexing is used, then α-conversion is no longer required as there will be no name collisions. If repeated application of the reduction steps eventually terminates, then by

156-766: A capture-avoiding manner. This is defined so that: For example, ( λ x . x ) [ y := y ] = λ x . ( x [ y := y ] ) = λ x . x {\displaystyle (\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x} , and ( ( λ x . y ) x ) [ x := y ] = ( ( λ x . y ) [ x := y ] ) ( x [ x := y ] ) = ( λ x . y ) y {\displaystyle ((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y} . The freshness condition (requiring that y {\displaystyle y}

234-412: A formalist theory , the "logicistic" theory of PM has no "precise statement of the syntax of the formalism". Furthermore in the theory, it is almost immediately observable that interpretations (in the sense of model theory ) are presented in terms of truth-values for the behaviour of the symbols "⊢" (assertion of truth), "~" (logical not), and "V" (logical inclusive OR). Truth-values : PM embeds

312-422: A "predicative function" actually is: this is taken as a primitive notion. Russell and Whitehead found it impossible to develop mathematics while maintaining the difference between predicative and non-predicative functions, so they introduced the axiom of reducibility , saying that for every non-predicative function there is a predicative function taking the same values. In practice this axiom essentially means that

390-419: A 2-element set {true,false}. The ramified type (τ 1 ,...,τ m |σ 1 ,...,σ n ) can be modeled as the product of the type (τ 1 ,...,τ m ,σ 1 ,...,σ n ) with the set of sequences of n quantifiers (∀ or ∃) indicating which quantifier should be applied to each variable σ i . (One can vary this slightly by allowing the σs to be quantified in any order, or allowing them to occur before some of

468-407: A contemporary formal theory. Kleene states that "this deduction of mathematics from logic was offered as intuitive axiomatics. The axioms were intended to be believed, or at least to be accepted as plausible hypotheses concerning the world". Indeed, unlike a Formalist theory that manipulates symbols according to rules of grammar, PM introduces the notion of "truth-values", i.e., truth and falsity in

546-405: A function can only occur in a proposition through its values. (...) [Working through the consequences] ... the theory of inductive cardinals and ordinals survives; but it seems that the theory of infinite Dedekindian and well-ordered series largely collapses, so that irrationals, and real numbers generally, can no longer be adequately dealt with. Also Cantor's proof that 2n > n breaks down unless n

624-513: A left or right parenthesis or the logical symbol ∧. More than one dot indicates the "depth" of the parentheses, for example, " . ", " : " or " :. ", " :: ". However the position of the matching right or left parenthesis is not indicated explicitly in the notation but has to be deduced from some rules that are complex and at times ambiguous. Moreover, when the dots stand for a logical symbol ∧ its left and right operands have to be deduced using similar rules. First one has to decide based on context whether

702-626: A postcard: Dear Professor Church, Russell had the iota operator , Hilbert had the epsilon operator . Why did you choose lambda for your operator? According to Scott, Church's entire response consisted of returning the postcard with the following annotation: " eeny, meeny, miny, moe ". Computable functions are a fundamental concept within computer science and mathematics. The lambda calculus provides simple semantics for computation which are useful for formally studying properties of computation. The lambda calculus incorporates two simplifications that make its semantics simple. The first simplification

780-426: A single input. For example, can be reworked into 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 s q u a r e _ s u m {\textstyle \operatorname {square\_sum} } function to the arguments (5, 2), yields at once whereas evaluation of

858-1004: A substitution s to a term M is written M [ s ]. The composition of two substitutions s 1 and s 2 is written s 1 s 2 and is defined by satisfying the property and substitution is defined on terms as follows: n [ N 1 … N n … ] = N n ( M 1 M 2 ) [ s ] = ( M 1 [ s ] ) ( M 2 [ s ] ) ( λ M ) [ s ] = λ ( M [ 1. s ′ ] ) where  s ′ = s ↑ 1 {\displaystyle {\begin{aligned}n[N_{1}\ldots N_{n}\ldots ]=&N_{n}\\(M_{1}\;M_{2})[s]=&(M_{1}[s])(M_{2}[s])\\(\lambda \;M)[s]=&\lambda \;(M[1.s'])\\&{\text{where }}s'=s\uparrow ^{1}\end{aligned}}} The steps outlined for

SECTION 10

#1733106531067

936-419: A term with other terms. In the β-reduction (λ M ) N , for example, we must To illustrate, consider the application which might correspond to the following term written in the usual notation After step 1, we obtain the term λ 4 □ (λ 1 □), where the variables that are destined for substitution are replaced with boxes. Step 2 decrements the free variables, giving λ 3 □ (λ 1 □). Finally, in step 3, we replace

1014-480: A variable that has not been bound, such as the term λ x . ( x + y ) {\displaystyle \lambda x.(x+y)} (which represents the function definition f ( x ) = x + y {\displaystyle f(x)=x+y} ). In this term, the variable y has not been defined and is considered an unknown. The abstraction λ x . ( x + y ) {\displaystyle \lambda x.(x+y)}

1092-625: Is alpha equivalence . It captures the intuition that the particular choice of a bound variable, in an abstraction, does not (usually) matter. For instance, λ x . x {\displaystyle \lambda x.x} and λ y . y {\displaystyle \lambda y.y} are alpha-equivalent lambda terms, and they both represent the same function (the identity function). The terms x {\displaystyle x} and y {\displaystyle y} are not alpha-equivalent, because they are not bound in an abstraction. In many presentations, it

1170-598: Is M applied to N, where M {\displaystyle M} is the lambda term ( λ x . ( λ x . x ) ) {\displaystyle (\lambda x.(\lambda x.x))} being applied to the input N {\displaystyle N} which is x {\displaystyle x} . Both examples 1 and 2 would evaluate to the identity function λ x . x {\displaystyle \lambda x.x} . In lambda calculus, functions are taken to be ' first class values ', so functions may be used as

1248-611: Is a lambda term. That is, a lambda term is valid if and only if it can be obtained by repeated application of these three rules. For convenience, some parentheses can be omitted when writing a lambda term. For example, the outermost parentheses are usually not written. See § Notation , below, for an explicit description of which parentheses are optional. It is also common to extend the syntax presented here with additional operations, which allows making sense of terms such as λ x . x 2 . {\displaystyle \lambda x.x^{2}.} The focus of this article

1326-595: Is a placeholder in both examples. Here, example 1 defines a function λ x . B {\displaystyle \lambda x.B} , where B {\displaystyle B} is ( λ x . x ) x {\displaystyle (\lambda x.x)x} , an anonymous function ( λ x . x ) {\displaystyle (\lambda x.x)} , with input x {\displaystyle x} ; while example 2, M {\displaystyle M}   N {\displaystyle N} ,

1404-413: Is a syntactically valid term and represents a function that adds its input to the yet-unknown y . Parentheses may be used and might be needed to disambiguate terms. For example, The examples 1 and 2 denote different terms, differing only in where the parentheses are placed. They have different meanings: example 1 is a function definition, while example 2 is a function application. The lambda variable x

1482-403: Is a type (τ 1 ,...,τ m ) that can be thought of as the class of propositional functions of τ 1 ,...,τ m (which in set theory is essentially the set of subsets of τ 1 ×...×τ m ). In particular there is a type () of propositions, and there may be a type ι (iota) of "individuals" from which other types are built. Russell and Whitehead's notation for building up types from other types

1560-399: Is able to benefit from the α-canonical form of de Bruijn indexed terms when appropriate. Barendregt's variable convention is a convention commonly used in proofs and definitions where it is assumed that: In the general context of an inductive definition, it is not possible to apply α-conversion as needed to convert an inductive definition using the convention to one where the convention

1638-463: Is also a current research topic in category theory . Lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics . The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox . Subsequently, in 1936 Church isolated and published just

SECTION 20

#1733106531067

1716-514: Is an abstraction representing the function f {\displaystyle f} defined by f ( x ) = x 2 + 2 , {\displaystyle f(x)=x^{2}+2,} using the term x 2 + 2 {\displaystyle x^{2}+2} for t . The name f {\displaystyle f} is superfluous when using abstraction. The syntax ( λ x . t ) {\displaystyle (\lambda x.t)} binds

1794-488: Is an elementary proposition, ~ p is an elementary proposition. Pp ✱1.71 . If p and q are elementary propositions, p ∨ q is an elementary proposition. Pp ✱1.72 . If φ p and ψ p are elementary propositional functions which take elementary propositions as arguments, φ p ∨ ψ p is an elementary proposition. Pp Together with the "Introduction to the Second Edition", the second edition's Appendix A abandons

1872-516: Is finite. It might be possible to sacrifice infinite well-ordered series to logical rigour, but the theory of real numbers is an integral part of ordinary mathematics, and can hardly be the subject of reasonable doubt. We are therefore justified (sic) in supposing that some logical axioms which is true will justify it. The axiom required may be more restricted than the axiom of reducibility, but if so, it remains to be discovered. One author observes that "The notation in that work has been superseded by

1950-534: Is not in the free variables of r {\displaystyle r} ) is crucial in order to ensure that substitution does not change the meaning of functions. De Bruijn index In mathematical logic , the de Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bound variables. Terms written using these indices are invariant with respect to α-conversion , so

2028-555: Is not used, because a variable may appear in both a binding position and a non-binding position in the rule. The induction principle holds if every rule satisfies the following two conditions: Principia Mathematica I can remember Bertrand Russell telling me of a horrible dream. He was in the top floor of the University Library, about A.D. 2100. A library assistant was going round the shelves carrying an enormous bucket, taking down books, glancing at them, restoring them to

2106-511: Is one approach, where the representation of a λ-term is treated as an equivalence class of all terms rewritable to it using variable permutations. This approach is taken by the Nominal Datatype Package of Isabelle/HOL . Another common alternative is an appeal to higher-order representations where the λ-binder is treated as a true function. In such representations, the issues of α-equivalence, substitution, etc. are identified with

2184-556: Is rather cumbersome, and the notation here is due to Church . In the ramified type theory of PM all objects are elements of various disjoint ramified types. Ramified types are implicitly built up as follows. If τ 1 ,...,τ m ,σ 1 ,...,σ n are ramified types then as in simple type theory there is a type (τ 1 ,...,τ m ,σ 1 ,...,σ n ) of "predicative" propositional functions of τ 1 ,...,τ m ,σ 1 ,...,σ n . However, there are also ramified types (τ 1 ,...,τ m |σ 1 ,...,σ n ) that can be thought of as

2262-459: Is simply mapped to itself. The second simplification is that the lambda calculus only uses functions of a single input. An ordinary function that requires two inputs, for instance the s q u a r e _ s u m {\textstyle \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

2340-637: Is that formulas such as would allow the comprehension of objects like the Russell set turn out to be ill-formed: they violate the grammatical restrictions of the system of PM . PM sparked interest in symbolic logic and advanced the subject, popularizing it and demonstrating its power. The Modern Library placed PM 23rd in their list of the top 100 English-language nonfiction books of the twentieth century. The Principia covered only set theory , cardinal numbers , ordinal numbers , and real numbers . Deeper theorems from real analysis were not included, but by

2418-400: Is that the lambda calculus treats functions "anonymously;" it does not give them explicit names. For example, the function can be rewritten in anonymous form as (which is read as "a tuple of x and y is mapped to x 2 + y 2 {\textstyle x^{2}+y^{2}} "). Similarly, the function can be rewritten in anonymous form as where the input

Lambda calculus - Misplaced Pages Continue

2496-440: Is the pure lambda calculus without extensions, but lambda terms extended with arithmetic operations are used for explanatory purposes. An abstraction λ x . t {\displaystyle \lambda x.t} denotes an § anonymous function that takes a single input x and returns t . For example, λ x . ( x 2 + 2 ) {\displaystyle \lambda x.(x^{2}+2)}

2574-478: Is true. Pp modus ponens ( ✱1.11 was abandoned in the second edition.) ✱1.2 . ⊦ : p ∨ p . ⊃ . p . Pp principle of tautology ✱1.3 . ⊦ : q . ⊃ . p ∨ q . Pp principle of addition ✱1.4 . ⊦ : p ∨ q . ⊃ . q ∨ p . Pp principle of permutation ✱1.5 . ⊦ : p ∨ ( q ∨ r ) . ⊃ . q ∨ ( p ∨ r ). Pp associative principle ✱1.6 . ⊦ :. q ⊃ r . ⊃ : p ∨ q . ⊃ . p ∨ r . Pp principle of summation ✱1.7 . If p

2652-448: Is usual to identify alpha-equivalent lambda terms. The following definitions are necessary in order to be able to define β-reduction: The free variables of a term are those variables not bound by an abstraction. The set of free variables of an expression is defined inductively: For example, the lambda term representing the identity λ x . x {\displaystyle \lambda x.x} has no free variables, but

2730-468: Is yet obtainable. Dr Leon Chwistek [Theory of Constructive Types] took the heroic course of dispensing with the axiom without adopting any substitute; from his work it is clear that this course compels us to sacrifice a great deal of ordinary mathematics. There is another course, recommended by Wittgenstein† (†Tractatus Logico-Philosophicus, *5.54ff) for philosophical reasons. This is to assume that functions of propositions are always truth-functions, and that

2808-454: The Church–Rosser theorem it will produce a β-normal form . Variable names are not needed if using a universal lambda function, such as Iota and Jot , which can create any function behavior by calling it on itself in various combinations. Lambda calculus is Turing complete , that is, it is a universal model of computation that can be used to simulate any Turing machine . Its namesake,

2886-467: The i th free variable. The increasing operation in step 3 is sometimes called shift and written ↑ where k is a natural number indicating the amount to increase the variables, and is defined by For example, ↑ is the identity substitution, leaving a term unchanged. A finite list of terms M 1 . M 2 ... M n abbreviates the substitution M 1 . M 2 ... M n .(n+1).(n+2)... leaving all variables greater than n unchanged. The application of

2964-424: The real-world sense, and the "assertion of truth" almost immediately as the fifth and sixth elements in the structure of the theory ( PM 1962:4–36): Cf. PM 1962:90–94, for the first edition: The first edition (see discussion relative to the second edition, below) begins with a definition of the sign "⊃" ✱1.01 . p ⊃ q . = . ~ p ∨ q . Df . ✱1.1 . Anything implied by a true elementary proposition

3042-485: The "formation rules" (syntactical rules leading to "well formed formulas") would have prevented the formation of this string. Source of the notation : Chapter I "Preliminary Explanations of Ideas and Notations" begins with the source of the elementary parts of the notation (the symbols =⊃≡−ΛVε and the system of dots): PM changed Peano's Ɔ to ⊃, and also adopted a few of Peano's later symbols, such as ℩ and ι, and Peano's practice of turning letters upside down. PM adopts

3120-459: The Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote binding a variable in a function . Lambda calculus may be untyped or typed . In typed lambda calculus, functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are weaker than the untyped lambda calculus, which is the primary subject of this article, in

3198-734: The Introduction presents the notion of "atomic proposition", a "datum" that "belongs to the philosophical part of logic". These have no parts that are propositions and do not contain the notions "all" or "some". For example: "this is red", or "this is earlier than that". Such things can exist ad finitum , i.e., even an "infinite enumeration" of them to replace "generality" (i.e., the notion of "for all"). PM then "advance[s] to molecular propositions" that are all linked by "the stroke". Definitions give equivalences for "~", "∨", "⊃", and " . ". The new introduction defines "elementary propositions" as atomic and molecular positions together. It then replaces all

Lambda calculus - Misplaced Pages Continue

3276-452: The Second Edition , an Appendix A that replaced ✱9 with a new Appendix B and Appendix C . PM was conceived as a sequel to Russell's 1903 The Principles of Mathematics , but as PM states, this became an unworkable suggestion for practical and philosophical reasons: "The present work was originally intended by us to be comprised in a second volume of Principles of Mathematics ... But as we advanced, it became increasingly evident that

3354-449: The assertion sign "⊦" from Frege's 1879 Begriffsschrift : Thus to assert a proposition p PM writes: (Observe that, as in the original, the left dot is square and of greater size than the full stop on the right.) Most of the rest of the notation in PM was invented by Whitehead. PM ' s dots are used in a manner similar to parentheses. Each dot (or multiple dot) represents either

3432-399: The boxes with the argument, namely λ 5 1; the first box is under one binder, so we replace it with λ 6 1 (which is λ 5 1 with the free variables increased by 1); the second is under two binders, so we replace it with λ 7 1. The final result is λ 3 (λ 6 1) (λ 1 (λ 7 1)). Formally, a substitution is an unbounded list of terms, written M 1 . M 2 ..., where M i is the replacement for

3510-556: The check for α-equivalence is the same as that for syntactic equality. Each de Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. The following are some examples: [REDACTED] De Bruijn indices are commonly used in higher-order reasoning systems such as automated theorem provers and logic programming systems. Formally, λ-terms ( M , N , ...) written using de Bruijn indices have

3588-474: The classes of propositional functions of τ 1 ,...τ m obtained from propositional functions of type (τ 1 ,...,τ m ,σ 1 ,...,σ n ) by quantifying over σ 1 ,...,σ n . When n =0 (so there are no σs) these propositional functions are called predicative functions or matrices. This can be confusing because modern mathematical practice does not distinguish between predicative and non-predicative functions, and in any case PM never defines exactly what

3666-410: The curried version requires one more step to arrive at the same result. The lambda calculus consists of a language of lambda terms , that are defined by a certain formal syntax, and a set of transformation rules for manipulating the lambda terms. These transformation rules can be viewed as an equational theory or as an operational definition . As described above, having no names, all functions in

3744-450: The desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus. Lambda calculus has applications in many different areas in mathematics , philosophy , linguistics , and computer science . Lambda calculus has played an important role in the development of the theory of programming languages . Functional programming languages implement lambda calculus. Lambda calculus

3822-441: The dots stand for a left or right parenthesis or a logical symbol. Then one has to decide how far the other corresponding parenthesis is: here one carries on until one meets either a larger number of dots, or the same number of dots next that have equal or greater "force", or the end of the line. Dots next to the signs ⊃, ≡,∨, =Df have greater force than dots next to ( x ), (∃ x ) and so on, which have greater force than dots indicating

3900-478: The elements of type (τ 1 ,...,τ m |σ 1 ,...,σ n ) can be identified with the elements of type (τ 1 ,...,τ m ), which causes the hierarchy of ramified types to collapse down to simple type theory. (Strictly speaking, PM allows two propositional functions to be different even if they take the same values on all arguments; this differs from modern mathematical practice where one normally identifies two such functions.) In Zermelo set theory one can model

3978-436: The end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be. A fourth volume on the foundations of geometry had been planned, but the authors admitted to intellectual exhaustion upon completion of the third. As noted in the criticism of the theory by Kurt Gödel (below), unlike

SECTION 50

#1733106531067

4056-509: The entire section ✱9 . This includes six primitive propositions ✱9 through ✱9.15 together with the Axioms of reducibility. The revised theory is made difficult by the introduction of the Sheffer stroke ("|") to symbolise "incompatibility" (i.e., if both elementary propositions p and q are true, their "stroke" p | q is false), the contemporary logical NAND (not-AND). In the revised theory,

4134-433: The following syntax (parentheses allowed freely): where n — natural numbers greater than 0—are the variables. A variable n is bound if it is in the scope of at least n binders (λ); otherwise it is free . The binding site for a variable n is the n th binder it is in the scope of, starting from the innermost binder. The most primitive operation on λ-terms is substitution : replacing free variables in

4212-492: The formulas are saying. Thus in the formal Kleene symbol set below, the "interpretation" of what the symbols commonly mean, and by implication how they end up being used, is given in parentheses, e.g., "¬ (not)". But this is not a pure Formalist theory. The following formalist theory is offered as contrast to the logicistic theory of PM . A contemporary formal system would be constructed as follows: The theory of PM has both significant similarities, and similar differences, to

4290-763: The function λ x . y {\displaystyle \lambda x.y} x {\displaystyle x} has a single free variable, y {\displaystyle y} . Suppose t {\displaystyle t} , s {\displaystyle s} and r {\displaystyle r} are lambda terms, and x {\displaystyle x} and y {\displaystyle y} are variables. The notation t [ x := r ] {\displaystyle t[x:=r]} indicates substitution of r {\displaystyle r} for x {\displaystyle x} in t {\displaystyle t} in

4368-568: The function that always returns y {\displaystyle y} , no matter the input. As an example of a function operating on functions, the function composition can be defined as λ f . λ g . λ x . ( f ( g x ) ) {\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))} . There are several notions of "equivalence" and "reduction" that allow lambda terms to be "reduced" to "equivalent" lambda terms. A basic form of equivalence, definable on lambda terms,

4446-476: The inputs, or be returned as outputs from other functions. For example, the lambda term λ x . x {\displaystyle \lambda x.x} represents the identity function , x ↦ x {\displaystyle x\mapsto x} . Further, λ x . y {\displaystyle \lambda x.y} represents the constant function x ↦ y {\displaystyle x\mapsto y} ,

4524-548: The lambda calculus are anonymous functions. They only accept one input variable, so currying is used to implement functions of several variables. The syntax of the lambda calculus defines some expressions as valid lambda calculus expressions and some as invalid, just as some strings of characters are valid C programs and some are not. A valid lambda calculus expression is called a " lambda term ". The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms: Nothing else

4602-469: The most convenient notation that precise expression allows; (3) to solve the paradoxes that plagued logic and set theory at the turn of the 20th century, like Russell's paradox . This third aim motivated the adoption of the theory of types in PM . The theory of types adopts grammatical restrictions on formulas that rules out the unrestricted comprehension of classes, properties, and functions. The effect of this

4680-437: The notions of "truth" and "falsity" in the notion "primitive proposition". A raw (pure) formalist theory would not provide the meaning of the symbols that form a "primitive proposition"—the symbols themselves could be absolutely arbitrary and unfamiliar. The theory would specify only how the symbols behave based on the grammar of the theory . Then later, by assignment of "values", a model would specify an interpretation of what

4758-420: The other hand, the named representation of λ-terms is more pervasive and can be more immediately understandable by others because the variables can be given descriptive names. Thus, even if a system uses de Bruijn indices internally, it will present a user interface with names. An alternative way to view de Bruijn indices is as de Bruijn levels, which indexes variables from the bottom of the stack rather than from

SECTION 60

#1733106531067

4836-400: The portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus . Until the 1960s when its relation to programming languages was clarified, the lambda calculus was only a formalism. Thanks to Richard Montague and other linguists' applications in

4914-634: The primitive propositions ✱1.2 to ✱1.72 with a single primitive proposition framed in terms of the stroke: The new introduction keeps the notation for "there exists" (now recast as "sometimes true") and "for all" (recast as "always true"). Appendix A strengthens the notion of "matrix" or "predicative function" (a "primitive idea", PM 1962:164) and presents four new Primitive propositions as ✱8.1–✱8.13 . ✱88 . Multiplicative axiom ✱120 . Axiom of infinity In simple type theory objects are elements of various disjoint "types". Types are implicitly built up as follows. If τ 1 ,...,τ m are types then there

4992-467: The ramified type theory of PM as follows. One picks a set ι to be the type of individuals. For example, ι might be the set of natural numbers, or the set of atoms (in a set theory with atoms) or any other set one is interested in. Then if τ 1 ,...,τ m are types, the type (τ 1 ,...,τ m ) is the power set of the product τ 1 ×...×τ m , which can also be thought of informally as the set of (propositional predicative) functions from this product to

5070-423: The same operations in a meta-logic . When reasoning about the meta-theoretic properties of a deductive system in a proof assistant , it is sometimes desirable to limit oneself to first-order representations and to have the ability to name or rename assumptions. The locally nameless approach uses a mixed representation of variables—de Bruijn indices for bound variables and names for free variables—that

5148-408: The semantics of natural language, the lambda calculus has begun to enjoy a respectable place in both linguistics and computer science. There is some uncertainty over the reason for Church's use of the Greek letter lambda (λ) as the notation for function-abstraction in the lambda calculus, perhaps in part due to conflicting explanations by Church himself. According to Cardone and Hindley (2006): By

5226-442: The sense that typed lambda calculi can express less than the untyped calculus can. On the other hand, typed lambda calculi allow more things to be proven. For example, in simply typed lambda calculus , it is a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate (see below ). One reason there are many different typed lambda calculi has been

5304-471: The shelves or dumping them into the bucket. At last he came to three large volumes which Russell could recognize as the last surviving copy of Principia Mathematica . He took down one of the volumes, turned over a few pages, seemed puzzled for a moment by the curious symbolism, closed the volume, balanced it in his hand and hesitated.... He [Russell] said once, after some contact with the Chinese language, that he

5382-536: The subject is a very much larger one than we had supposed; moreover on many fundamental questions which had been left obscure and doubtful in the former work, we have now arrived at what we believe to be satisfactory solutions." PM , according to its introduction, had three aims: (1) to analyze to the greatest possible extent the ideas and methods of mathematical logic and to minimize the number of primitive notions , axioms , and inference rules ; (2) to precisely express mathematical propositions in symbolic logic using

5460-400: The subsequent development of logic during the 20th century, to the extent that the beginner has trouble reading PM at all"; while much of the symbolic content can be converted to modern notation, the original notation itself is "a subject of scholarly dispute", and some notation "embodies substantive logical doctrines so that it cannot simply be replaced by contemporary symbolism". Kurt Gödel

5538-425: The top. This eliminates the need to reindex free variables, for example when weakening the context, whereas de Bruijn indices eliminate the need to reindex bound variables, for example when substituting a closed expression in another context. De Bruijn indices are not the only representation of λ-terms that obviates the problem of α-conversion. Among named representations, the nominal techniques of Pitts and Gabbay

5616-489: The variable x in the term t . The definition of a function with an abstraction merely "sets up" the function but does not invoke it. An application t {\displaystyle t}   s {\displaystyle s} represents the application of a function t to an input s , that is, it represents the act of calling function t on input s to produce t ( s ) {\displaystyle t(s)} . A lambda term may refer to

5694-637: The way, why did Church choose the notation “λ”? In [an unpublished 1964 letter to Harald Dickson] he stated clearly that it came from the notation “ x ^ {\displaystyle {\hat {x}}} ” used for class-abstraction by Whitehead and Russell , by first modifying “ x ^ {\displaystyle {\hat {x}}} ” to “ ∧ x {\displaystyle \land x} ” to distinguish function-abstraction from class-abstraction, and then changing “ ∧ {\displaystyle \land } ” to “λ” for ease of printing. This origin

5772-403: The β-reduction above are thus more concisely expressed as: When using the standard "named" representation of λ-terms, where variables are treated as labels or strings, one must explicitly handle α-conversion when defining any operation on the terms. In practice this is cumbersome, inefficient, and often error-prone. It has therefore led to the search for different representations of such terms. On

5850-417: The τs, but this makes little difference except to the bookkeeping.) The introduction to the second edition cautions: One point in regard to which improvement is obviously desirable is the axiom of reducibility ... . This axiom has a purely pragmatic justification ... but it is clearly not the sort of axiom with which we can rest content. On this subject, however, it cannot be said that a satisfactory solution

5928-453: Was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and λ just happened to be chosen. Dana Scott has also addressed this question in various public lectures. Scott recounts that he once posed a question about the origin of the lambda symbol to Church's former student and son-in-law John W. Addison Jr., who then wrote his father-in-law

6006-484: Was harshly critical of the notation: "What is missing, above all, is a precise statement of the syntax of the formalism. Syntactical considerations are omitted even in cases where they are necessary for the cogency of the proofs." This is reflected in the example below of the symbols " p ", " q ", " r " and "⊃" that can be formed into the string " p ⊃ q ⊃ r ". PM requires a definition of what this symbol-string means in terms of other symbols; in contemporary treatments

6084-420: Was horrified to find that the language of Principia Mathematica was an Indo-European one. The Principia Mathematica (often abbreviated PM ) is a three-volume work on the foundations of mathematics written by the mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. In 1925–1927, it appeared in a second edition with an important Introduction to

#66933