10947:
encoded in the lambda calculus in size linearly proportional to the size of the Turing machine. The true cost of reducing lambda terms is not due to β-reduction per se but rather the handling of the duplication of redexes during β-reduction. It is not known if optimal reduction implementations are reasonable when measured with respect to a reasonable cost model such as the number of leftmost-outermost steps to normal form, but it has been shown for fragments of the lambda calculus that the optimal reduction algorithm is efficient and has at most a quadratic overhead compared to leftmost-outermost. In addition the BOHM prototype implementation of optimal reduction outperformed both
15978:
11314:
10939:, the existence of lambda terms which grow exponentially in size for each β-reduction. The result gets around this by working with a compact shared representation. The result makes clear that the amount of space needed to evaluate a lambda term is not proportional to the size of the term during reduction. It is not currently known what a good measure of space complexity would be.
13118:
Some other systems use juxtaposition to mean application, so 'ab' means 'a@b'. This is fine except that it requires that variables have length one so that we know that 'ab' is two variables juxtaposed not one variable of length 2. But we want to labels like 'firstVariable' to mean a single variable,
10946:
reduces all computations with the same label in one step, avoiding duplicated work, but the number of parallel β-reduction steps to reduce a given term to normal form is approximately linear in the size of the term. This is far too small to be a reasonable cost measure, as any Turing machine may be
8771:
would take the form of a collection of previously defined functions, which as lambda-terms are merely particular constants. The pure lambda calculus does not have a concept of named constants since all atomic lambda-terms are variables, but one can emulate having named constants by setting aside a
5739:. Under this view, β-reduction corresponds to a computational step. This step can be repeated by additional β-reductions until there are no more applications left to reduce. In the untyped lambda calculus, as presented here, this reduction process may not terminate. For instance, consider the term
6028:
Another aspect of the untyped lambda calculus is that it does not distinguish between different kinds of data. For instance, it may be desirable to write a function that only operates on numbers. However, in the untyped lambda calculus, there is no way to prevent a function from being applied to
10522:
The leftmost innermost redex is reduced first. As a consequence, a function's arguments are always reduced before they are substituted into the function. Unlike normal order reduction, applicative order reduction may fail to find the beta-normal form of an expression, even if such a normal form
824:
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 is that the lambda calculus treats functions "anonymously;" it does not give them explicit names. For
10648:
Like applicative order, but no reductions are performed inside abstractions. This is similar to the evaluation order of strict languages like C: the arguments to a function are evaluated before calling the function, and function bodies are not even partially evaluated until the arguments are
8908:. Lambda calculus cannot express this: all functions are anonymous in lambda calculus, so we can't refer by name to a value which is yet to be defined, inside the lambda term defining that same value. However, a lambda expression can receive itself as its own argument, for example in
2019:
Nothing else 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
7175:
Therefore, both strongly normalising terms and weakly normalising terms have a unique normal form. For strongly normalising terms, any reduction strategy is guaranteed to yield the normal form, whereas for weakly normalising terms, some reduction strategies may fail to find it.
11126:
The fact that lambda calculus terms act as functions on other lambda calculus terms, and even on themselves, led to questions about the semantics of the lambda calculus. Could a sensible meaning be assigned to lambda calculus terms? The natural semantics was to find a set
10706:
As call by name (hence weak), but function applications that would duplicate terms instead name the argument. The argument may be evaluated "when needed," at which point the name binding is updated with the reduced value. This can save time compared to normal order
8903:
is the definition of a function invoking itself. A definition containing itself inside itself, by value, leads to the whole value being of infinite size. Other notations which support recursion natively overcome this by referring to the function definition
10515:
The leftmost outermost redex is reduced first. That is, whenever possible, arguments are substituted into the body of an abstraction before the arguments are reduced. If a term has a beta-normal form, normal order reduction will always reach that normal
780:
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 a postcard:
8976:(typically the first one) will be assumed to receive the lambda expression itself as its value, so that calling it – applying it to an argument – will amount to recursion. Thus to achieve recursion, the intended-as-self-referencing argument (called
633:
Subsequently, in 1936 Church isolated and published just 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
12474:, to detect possibly infinite unwinding trees; 2) the representational calculus with β-reduction of scoped lambda graphs constitute Ariola/Blom's cyclic extension of lambda calculus; 3) Ariola/Blom reason about strict languages using
7492:, which is why these numerals can be used for arithmetic. (In Church's original lambda calculus, the formal parameter of a lambda expression was required to occur at least once in the function body, which made the above definition of
12077:
6731:
The precise rules for α-conversion are not completely trivial. First, when α-converting an abstraction, the only variable occurrences that are renamed are those that are bound to the same abstraction. For example, an α-conversion of
6023:
11780:
A paper giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is different from proof-theoretic semantics as in the
Dummett–Prawitz tradition since it takes reduction as the rules giving
1626:
2760:
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
10874:
for the lambda calculus is a bit tricky, because the cost of a β-reduction may vary depending on how it is implemented. To be precise, one must somehow find the location of all of the occurrences of the bound variable
9231:). The function does not need to be explicitly passed to itself at any point, for the self-replication is arranged in advance, when it is created, to be done each time it is called. Thus the original lambda expression
8759:. Because several programming languages include the lambda calculus (or something very similar) as a fragment, these techniques also see use in practical programming, but may then be perceived as obscure or foreign.
10609:
10507:
Whether a term is normalising or not, and how much work needs to be done in normalising it if it is, depends to a large extent on the reduction strategy used. Common lambda calculus reduction strategies include:
10431:) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see
4922:
9750:, every recursively defined function can be expressed as a lambda expression. In particular, we can now cleanly define the subtraction, multiplication and comparison predicate of natural numbers recursively.
8840:
By chaining such definitions, one can write a lambda calculus "program" as zero or more function definitions, followed by one lambda-term using those functions that constitutes the main body of the program.
567:). One reason there are many different typed lambda calculi has been 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.
10435:). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus but from another point of view, they can also be considered the more fundamental theory and
919:
5305:
5073:
4773:
2024:, 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
3318:
5802:
5136:
In general, failure to meet the freshness condition can be remedied by alpha-renaming first, with a suitable fresh variable. For example, switching back to our correct notion of substitution, in
397:
9074:
The self-application achieves replication here, passing the function's lambda expression on to the next invocation as an argument value, making it available to be referenced and called there.
13631:
Proceedings of the Joint
Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
1303:
773:
This origin was also reported in . 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.
12205:
480:
1447:
4518:
11055:
datatypes, because a function is a first class datatype if and only if new instances of the function can be created at run-time. And this run-time creation of functions is supported in
6865:. Substitution on terms of the lambda calculus is defined by recursion on the structure of terms, as follows (note: x and y are only variables while M and N are any lambda expression):
2614:
4430:
3025:
2695:
1365:
1174:
1239:
1087:
987:
1691:
10935:
time cost model, that is, the reduction can be simulated on a Turing machine in time polynomially proportional to the number of steps. This was a long-standing open problem, due to
5697:
5603:
6422:
The abstraction operator, λ, is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of an abstraction are said to be
5445:
2156:
661:(λ) 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):
6827:
9744:
Every recursively defined function can be seen as a fixed point of some suitably defined function closing over the recursive call with an extra argument, and therefore, using
2061:
13032:", Invited Talk at the Workshop in honour of Dana Scott’s 85th birthday and 50 years of domain theory, 7–8 July, FLoC 2018 (talk 7 July 2018). The relevant passage begins at
2551:
2465:
12718:
5483:
5351:
2860:
645:
and other linguists' applications in the semantics of natural language, the lambda calculus has begun to enjoy a respectable place in both linguistics and computer science.
12331:
12255:
5184:
2895:
2319:
2227:
1948:
5726:
5632:
5131:
5102:
3713:
3684:
3525:
3391:
3362:
3200:
3141:
3097:
2802:
2643:
2096:
12357:
3229:
3171:
1119:
725:
692:
150:
4363:
1776:
1491:
12141:
12101:: (λx.M) N = M , rewritten as (λx.M) N = M, "where M denotes the substitution of N for every occurrence of x in M". Also denoted M, "the substitution of N for x in M".
10429:
2506:
1046:
4544:
4151:
2260:
748:
768:
10971:
languages can be understood in terms of the lambda calculus, which provides the basic mechanisms for procedural abstraction and procedure (subprogram) application.
12288:
8772:
variable as the name of the constant, using abstraction to bind that variable in the main body, and apply that abstraction to the intended definition. Thus to use
2421:
1858:, 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
563:, 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
12079:. Parentheses can be dropped if the expression is unambiguous. For some applications, terms for logical and mathematical constants and operations may be included.
4125:
4003:
2063:
The focus of this article is the pure lambda calculus without extensions, but lambda terms extended with arithmetic operations are used for explanatory purposes.
1881:
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
232:
4275:
2009:
1986:
12431:
12411:
11960:
10629:
5538:
5518:
5386:
5204:
4969:
4945:
4668:
4648:
4628:
4604:
4584:
4564:
4251:
4231:
4211:
4191:
4171:
4083:
4063:
4043:
4023:
3955:
3935:
3915:
3895:
3860:
3840:
3820:
3800:
3780:
3752:
3732:
3651:
3631:
3611:
3592:
3565:
3545:
3490:
3470:
3431:
3411:
3249:
3065:
3045:
2975:
2955:
2935:
2915:
2822:
2754:
2734:
2714:
2376:
2356:
2284:
2176:
1816:
1796:
1731:
1711:
174:
11620:
1841:
1515:
5807:
11593:
1127:
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
316:
296:
276:
256:
198:
109:
10466:
for programming languages; here typability usually captures desirable properties of the program, e.g. the program will not cause a memory access violation.
9077:
This solves it but requires re-writing each recursive call as self-application. We would like to have a generic solution, without a need for any re-writes:
10637:
Any redex can be reduced at any time. This means essentially the lack of any particular reduction strategy—with regard to reducibility, "all bets are off".
1527:
10887:, implying a time cost, or one must keep track of the locations of free variables in some way, implying a space cost. A naïve search for the locations of
10842:. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a
8142:
Then, with these two lambda terms, we can define some logic operators (these are just possible formulations; other expressions could be equally correct):
14357:
11853:
covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.
7559:
By varying what is being repeated, and varying what argument that function being repeated is applied to, a great many different effects can be achieved.
10098:
but lacks abstraction (except as part of the named constants, if these are considered non-atomic). This can also be viewed as anonymising variables, as
13255:; A note (accessed 2017) at the original location suggests that the authors consider the work originally referenced to have been superseded by a book.
3433:
are not alpha-equivalent, because they are not bound in an abstraction. In many presentations, it is usual to identify alpha-equivalent lambda terms.
551:. 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
11531:
15032:
10377:
combinator actually conflates two functionalities: rearranging arguments, and duplicating an argument so that it may be used in two places. The
4630:) ; substituting a variable which is not bound by an abstraction proceeds in the abstraction's body, provided that the abstracted variable
6779:
Second, α-conversion is not possible if it would result in a variable getting captured by a different abstraction. For example, if we replace
10924:
were an early approach that traded this time cost for a quadratic space usage. More generally this has led to the study of systems that use
15115:
14256:
10526:
1869:
As described above, having no names, all functions in the lambda calculus are anonymous functions. They only accept one input variable, so
7148:
13367:
4778:
3335:. It captures the intuition that the particular choice of a bound variable, in an abstraction, does not (usually) matter. For instance,
16014:
11919:
4432: ; a variable bound by an abstraction is not subject to substitution; substituting such variable leaves the abstraction unchanged
16488:
11615:, 58 (1936), pp. 345–363. This paper contains the proof that the equivalence of lambda expressions is in general not decidable.
8410:
make it convenient to write "if-then-else" expressions in lambda calculus. For example, the predecessor function can be defined as:
13554:
Functional
Programming Languages and Computer Architecture: 5th ACM Conference. Cambridge, MA, USA, August 26-30, 1991. Proceedings
11741:
7172:
when working up to α-conversion (i.e. we consider two normal forms to be equal if it is possible to α-convert one into the other).
831:
10332:
passes the argument on to both subterms of the application, and then applies the result of the first to the result of the second.
15429:
14015:
6815:
3323:
There are several notions of "equivalence" and "reduction" that allow lambda terms to be "reduced" to "equivalent" lambda terms.
8895:
7703:
can be thought of as a function taking two natural numbers as arguments and returning a natural number; it can be verified that
6983:
To substitute into an abstraction, it is sometimes necessary to α-convert the expression. For example, it is not correct for (λ
13238:
3448:
of a term are those variables not bound by an abstraction. The set of free variables of an expression is defined inductively:
641:
Until the 1960s when its relation to programming languages was clarified, the lambda calculus was only a formalism. Thanks to
16730:
15587:
14202:
13482:
13343:
13210:
12700:
12670:
11730:
11639:
5209:
4977:
4677:
14375:
13597:"Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting"
10853:
7036:
reduction) captures the idea of function application. β-reduction is defined in terms of substitution: the β-reduction of (λ
15442:
14765:
12492:
10732:
the question. This was historically the first problem for which undecidability could be proven. As usual for such a proof,
10432:
6474:
is a free variable. Also a variable is bound by its nearest abstraction. In the following example the single occurrence of
3258:
494:
13286:
11650:
5742:
16356:
16023:
13979:
13925:
11911:
8751:
for lambda calculus. Many of these were originally developed in the context of using lambda calculus as a foundation for
6025:. That is, the term reduces to itself in a single β-reduction, and therefore the reduction process will never terminate.
328:
15447:
15437:
15174:
15027:
14380:
12369:
2321:
559:
than the untyped calculus can. On the other hand, typed lambda calculi allow more things to be proven. For example, in
533:
14371:
6708:-conversion), sometimes known as α-renaming, allows bound variable names to be changed. For example, α-conversion of λ
15583:
14218:
13964:
13656:
13579:
13442:
13064:
12979:
12643:
11847:
11815:
11712:
11584:
11543:
1250:
14925:
13974:
12159:
15680:
15424:
14249:
11888:
11576:
10838:
Church's proof of uncomputability first reduces the problem to determining whether a given lambda expression has a
10447:
10060:
411:
13054:
12210:
11690:, 57 (1935), pp. 153–173 and 219–244. Contains the lambda calculus definitions of several familiar functions.
11590:
16443:
14985:
14678:
11687:
11612:
10931:
In 2014, it was shown that the number of β-reduction steps taken by normal order reduction to reduce a term is a
10871:
7169:
4437:
1373:
800:
According to Scott, Church's entire response consisted of returning the postcard with the following annotation: "
591:
14419:
13958:
13506:
3393:
are alpha-equivalent lambda terms, and they both represent the same function (the identity function). The terms
2566:
16725:
16564:
16438:
16097:
16007:
15941:
15643:
15406:
15401:
15226:
14647:
14331:
11792:
11445:
11438:
11246:– A version of lambda calculus with binary I/O, a binary encoding of terms, and a designated universal machine.
11076:
10952:
10455:
8756:
5732:
4370:
2980:
2650:
42:
11552:
6615:, if they can be α-converted into the same expression. β-equivalence and η-equivalence are defined similarly.
1321:
1186:
1130:
1054:
934:
16715:
16216:
16037:
15936:
15719:
15636:
15349:
15280:
15157:
14399:
14116:
14101:
13882:
11516:
11442:
11328:
11072:
11036:
10986:
1312:, transforms a function that takes multiple arguments into a chain of functions each with a single argument.
88:
operations on them. In the simplest form of lambda calculus, terms are built using only the following rules:
13505:
Biernacka, Małgorzata; Charatonik, Witold; Drab, Tomasz (2022). Andronick, June; de Moura, Leonardo (eds.).
13225:
7849:
times and then applying it to zero. Exponentiation has a rather simple rendering in Church numerals, namely
1632:
15861:
15687:
15373:
15007:
14606:
14106:
14043:
11363:
11347:
11068:
10478:
8752:
7136:
7075:
5637:
5543:
635:
560:
11928:
as a common means of evaluating lambda expressions and discusses the applicability of lambda calculus for
11705:
665:
By the way, why did Church choose the notation “λ”? In he stated clearly that it came from the notation “
16102:
15739:
15734:
15344:
15083:
15012:
14341:
14242:
14008:
13877:
11818:
is a recent monograph that covers the main topics of lambda calculus from the type-free variety, to most
10943:
7218:
7189:
5391:
2332:. The definition of a function with an abstraction merely "sets up" the function but does not invoke it.
2113:
1176:
function, can be reworked into an equivalent function that accepts a single input, and as output returns
587:
13059:. Studies in Logic and the Foundations of Mathematics. Vol. 103 (Revised ed.). North Holland.
12112:
For a full history, see
Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
11028:– just a single argument in this case, and an expression that is evaluated as the body of the function,
8097:
By convention, the following two definitions (known as Church
Booleans) are used for the Boolean values
16710:
16584:
16246:
16067:
15668:
15258:
14652:
14620:
14311:
11456:
11100:
10502:
6772:. The latter has a different meaning from the original. This is analogous to the programming notion of
6292:
To keep the notation of lambda expressions uncluttered, the following conventions are usually applied:
6042:
820:
are a fundamental concept within computer science and mathematics. The lambda calculus provides simple
611:
70:
11708:. A classic paper highlighting the importance of lambda calculus as a basis for programming languages.
2027:
532:. Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote
16589:
16539:
16301:
16190:
16000:
15958:
15907:
15804:
15302:
15263:
14740:
14385:
14065:
14060:
13872:
11933:
11701:
11432:
11338:
11332:
11224:
11092:
10490:
6355:
2515:
2429:
627:
498:
14414:
13562:
5450:
5318:
2827:
16705:
16649:
16508:
16087:
15799:
15729:
15268:
15120:
15103:
14826:
14306:
14048:
13072:
12496:
12301:
12225:
11905:
11893:
11881:
11869:
11506:
10832:
5731:
The lambda calculus may be seen as an idealized version of a functional programming language, like
5139:
2865:
2289:
2181:
1918:
1882:
13937:
13037:
12606:
555:
than the untyped lambda calculus, which is the primary subject of this article, in the sense that
16720:
16644:
16185:
15631:
15608:
15569:
15455:
15396:
15042:
14962:
14806:
14750:
14363:
11489:
11280:
10611:
is reduced to itself by applicative order, while normal order reduces it to its beta-normal form
10451:
10408:
10386:
5702:
5608:
5107:
5078:
3689:
3660:
3501:
3367:
3338:
3176:
3117:
3073:
2778:
2619:
2072:
12336:
3208:
3150:
1098:
701:
668:
16674:
16341:
16311:
16286:
16226:
16125:
16057:
15921:
15648:
15626:
15593:
15486:
15332:
15317:
15290:
15241:
15125:
15060:
14885:
14851:
14846:
14720:
14551:
14528:
14111:
14001:
13833:
13557:
11864:
11468:
11416:
11392:
11388:
11243:
11193:
10968:
10459:
8889:
4279:
2553:
is a syntactically valid term and represents a function that adds its input to the yet-unknown
1863:
801:
537:
120:
54:
13892:
To
Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
13549:
13135:
12969:
12126:
10414:
8518:
8343:
The following predicate tests whether the first argument is less-than-or-equal-to the second:
6728:. Frequently, in uses of lambda calculus, α-equivalent terms are considered to be equivalent.
2470:
1738:
1453:
16569:
16463:
16428:
16316:
16291:
16135:
16052:
15851:
15704:
15496:
15214:
14950:
14856:
14715:
14700:
14581:
14556:
14096:
13428:
13143:, vol. 0804, Department of Mathematics and Statistics, University of Ottawa, p. 9,
12690:
11929:
11496:
11407:
11212:
10925:
10443:
10398:
7413:
4523:
4130:
2232:
1011:
730:
695:
13906:
13459:
10756:
of natural numbers is a computable function if and only if there exists a lambda expression
9227:
will return a self-replicating lambda expression representing the recursive function (here,
7003:
was supposed to be free but ended up being bound. The correct substitution in this case is λ
4971:) is crucial in order to ensure that substitution does not change the meaning of functions.
753:
485:, replacing the bound variables with the argument expression in the body of the abstraction.
16554:
16361:
16140:
15824:
15786:
15663:
15467:
15307:
15231:
15209:
15037:
14995:
14894:
14861:
14725:
14513:
14424:
14197:
13629:
Accattoli, Beniamino; Dal Lago, Ugo (14 July 2014). "Beta reduction is invariant, indeed".
13154:
11819:
11402:
11351:
11111:
11052:
10967:'s 1965 paper "A Correspondence between ALGOL 60 and Church's Lambda-notation", sequential
10737:
7158:
6170:
6085:
3252:
3111:', so functions may be used as the inputs, or be returned as outputs from other functions.
1893:
1315:
525:
58:
46:
14141:
13088:
12520:
12264:
12072:{\displaystyle (\lambda x.\lambda y.(\lambda z.(\lambda x.z\ x)\ (\lambda y.z\ y))(x\ y))}
11095:
property of the lambda calculus means that evaluation (β-reduction) can be carried out in
8724:
which allows us to give perhaps the most transparent version of the predecessor function:
2397:
512:, which can create any function behavior by calling it on itself in various combinations.
8:
16639:
16604:
16549:
16493:
16396:
16381:
16351:
16331:
16306:
16175:
16160:
15953:
15844:
15829:
15809:
15766:
15653:
15603:
15529:
15474:
15411:
15204:
15199:
15147:
14915:
14904:
14576:
14476:
14404:
14395:
14391:
14326:
14321:
14131:
14086:
11398:
11103:
10725:
9971:
8768:
7482:
is defined to be the identity function. Such repeated compositions (of a single function
7198:, Booleans, data structures, and recursion, as illustrated in the following sub-sections
6823:
4089:
3967:
817:
521:
493:
is used, then α-conversion is no longer required as there will be no name collisions. If
13312:
13158:
11876:
11301:
combinators, equivalent to lambda calculus, but reducible without variable substitutions
11020:
The above example is an expression that evaluates to a first-class function. The symbol
6018:{\displaystyle (\lambda x.xx)(\lambda x.xx)\to (xx)=(x)(x)=(\lambda x.xx)(\lambda x.xx)}
4257:
1991:
1968:
205:
16684:
16609:
16579:
16544:
16524:
16453:
16433:
16371:
16366:
16276:
16266:
16251:
16195:
15982:
15751:
15714:
15699:
15692:
15675:
15479:
15461:
15327:
15253:
15236:
15189:
15002:
14911:
14745:
14730:
14690:
14642:
14627:
14615:
14571:
14546:
14316:
14265:
14161:
14126:
13766:
13720:
13662:
13634:
13556:. Lecture Notes in Computer Science. Vol. 523. Springer-Verlag. pp. 289–312.
13424:
13390:
13187:
13144:
13033:
12946:
12938:
12900:
12859:
12817:
12775:
12738:
12584:
12576:
12416:
12396:
11937:
11900:
11771:
11378:
11367:
11319:
11249:
11107:
10980:
10614:
10470:
7162:
6819:
6773:
6626:, refers to subterms that can be reduced by one of the reduction rules. For example, (λ
5523:
5488:
5356:
5189:
4974:
For example, a substitution that ignores the freshness condition could lead to errors:
4954:
4930:
4653:
4633:
4613:
4589:
4569:
4549:
4236:
4216:
4196:
4176:
4156:
4068:
4048:
4028:
4008:
3940:
3920:
3900:
3865:
3845:
3825:
3805:
3785:
3765:
3737:
3717:
3636:
3616:
3596:
3577:
3550:
3530:
3475:
3455:
3416:
3396:
3234:
3108:
3050:
3030:
2960:
2940:
2920:
2900:
2807:
2739:
2719:
2699:
2361:
2341:
2269:
2161:
1801:
1781:
1716:
1696:
159:
34:
15992:
14935:
13596:
12537:
12156:
The expression e can be: variables x, lambda abstractions, or applications —in BNF,
11106:
are relevant. However, the lambda calculus does not offer any explicit constructs for
10843:
10700:
As normal order, but computations that have the same label are reduced simultaneously.
7517:
functions defined below, one can define a function that constructs a (linked) list of
1621:{\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}
821:
16664:
16619:
16599:
16559:
16498:
16468:
16448:
16241:
16170:
15977:
15917:
15724:
15534:
15524:
15416:
15297:
15132:
15108:
14889:
14873:
14778:
14755:
14632:
14601:
14566:
14461:
14296:
14166:
13804:
13652:
13575:
13478:
13438:
13339:
13206:
13060:
13003:
12975:
12724:
12696:
12666:
12639:
12478:, and compare to Moggi's calculus, and to Hasegawa's calculus. Conclusions on p. 111.
11843:
11811:
11788:
11726:
11635:
11580:
11539:
11501:
11313:
11274:
11048:
10655:
Like normal order, but no reductions are performed inside abstractions. For example,
10482:
10382:
10070:
8748:
7489:
7132:
7071:
7055:
For example, assuming some encoding of 2, 7, ×, we have the following β-reduction: (λ
6574:
3144:
3068:
1859:
1823:
1497:
13785:
13666:
13394:
13174:(1988). "A Proof-Theoretic Account of Programming and the Role of Reduction Rules".
12950:
11775:
11674:
16669:
16594:
16483:
16261:
15931:
15926:
15819:
15776:
15598:
15559:
15554:
15539:
15365:
15322:
15219:
15017:
14967:
14541:
14503:
14181:
14156:
14151:
14091:
13800:
13770:
13756:
13696:
13644:
13611:
13567:
13521:
13470:
13382:
13331:
13323:
13247:
13183:
12965:
12930:
12892:
12851:
12809:
12767:
12686:
12588:
12568:
11823:
11763:
11669:
11427:
11175:
11064:
10839:
10729:
9453:
Now, to perform our recursive call to the factorial function, we would simply call
3436:
The following definitions are necessary in order to be able to define β-reduction:
793:
642:
583:
502:
301:
281:
261:
241:
183:
94:
13922:
10744:. In fact computability can itself be defined via the lambda calculus: a function
10122:, while still allowing argument values to be substituted into the positions where
8930:
should be an abstraction, applying its parameter to a value to express recursion.
16376:
16271:
16236:
15912:
15902:
15839:
15794:
15756:
15658:
15578:
15385:
15312:
15285:
15273:
15179:
15093:
15067:
15022:
14990:
14791:
14593:
14536:
14486:
14451:
14409:
14136:
14053:
13968:
13952:
13941:
13929:
13899:
13327:
13050:
12660:
12633:
12602:
12516:
11925:
11597:
11549:
11483:
11450:
11372:
11342:
11253:
11115:
10921:
10741:
10716:
There is no algorithm that takes as input any two lambda expressions and outputs
10486:
8982:
here) must always be passed to itself within the function body, at a call point:
8810:
7185:
6834:
2560:
Parentheses may be used and might be needed to disambiguate terms. For example,
750:” to distinguish function-abstraction from class-abstraction, and then changing “
595:
490:
13719:
Asperti, Andrea (16 Jan 2017). "About the efficient reduction of lambda terms".
13701:
13684:
12635:
Categorial
Investigations: Logical and Linguistic Aspects of the Lambek Calculus
11742:
An introduction to λ-calculi and arithmetic with a decent selection of exercises
11051:. However, function pointers are not a sufficient condition for functions to be
6585:
The meaning of lambda expressions is defined by how expressions can be reduced.
6337:
When all variables are single-letter, the space in applications may be omitted:
2426:
A lambda term may refer to a variable that has not been bound, such as the term
16659:
16654:
16574:
16458:
16336:
16231:
16072:
15897:
15876:
15834:
15814:
15709:
15564:
15162:
15152:
15142:
15137:
15071:
14945:
14821:
14710:
14705:
14683:
14284:
14176:
13171:
12793:
11749:
11462:
11421:
11263:
10900:
10816:
10069:
is a lambda-term without abstraction, but possibly containing named constants (
9236:
7235:
7231:
7154:
7098:
7094:
4607:
3251:, no matter the input. As an example of a function operating on functions, the
657:
There is some uncertainty over the reason for Church's use of the Greek letter
619:
594:
implement lambda calculus. Lambda calculus is also a current research topic in
529:
403:
62:
13857:
13526:
13386:
13272:
11767:
8678:
As an example of the use of pairs, the shift-and-increment function that maps
8305:
is a function that returns a
Boolean value. The most fundamental predicate is
7505:, which is often useful when analysing programs, is as an instruction 'repeat
16699:
16346:
16321:
16155:
15871:
15549:
15056:
14841:
14831:
14801:
14786:
14456:
14024:
13474:
12918:
12880:
12835:
12755:
11754:
11535:
11384:
11236:
11179:
11164:
10724:
depending on whether one expression reduces to the other. More precisely, no
10693:
Strategies with sharing reduce computations that are "the same" in parallel:
10674:
is in normal form according to this strategy, although it contains the redex
6814:
In programming languages with static scope, α-conversion can be used to make
789:
607:
66:
38:
30:
13648:
13615:
13029:
11752:(2008). "On Reduction Rules, Meaning-as-Use and Proof-Theoretic Semantics".
11745:. Notes for a course in the Mathematical Logic MSc at Manchester University.
508:
Variable names are not needed if using a universal lambda function, such as
16614:
16534:
16401:
16281:
16165:
16145:
15771:
15618:
15519:
15511:
15391:
15339:
15248:
15184:
15167:
15098:
14957:
14816:
14518:
14301:
13740:
12797:
11693:
11479:
11186:
10964:
10474:
10463:
7101:
they give the same result for all arguments. η-reduction converts between λ
1885:
programs and some are not. A valid lambda calculus expression is called a "
623:
509:
50:
13761:
13744:
13571:
11424:– A kind of constructive logical formula such that proofs are lambda terms
10989:
the "square" function can be expressed as a lambda expression as follows:
9215:
Given a lambda term with first argument representing recursive call (e.g.
8030:. With the predecessor function, subtraction is straightforward. Defining
586:. Lambda calculus has played an important role in the development of the
16529:
16503:
16386:
16150:
16077:
15881:
15761:
14940:
14930:
14877:
14561:
14481:
14466:
14346:
14291:
14223:
14146:
14121:
14081:
13961:, a graphical Java applet demonstrating alternative reduction strategies.
13865:
12556:
11827:
11646:
11228:
11205:
11144:
11040:
6509:) and is defined by recursion on the structure of the terms, as follows:
6030:
5736:
615:
579:
571:
10462:
languages. Typed lambda calculi play an important role in the design of
16679:
16326:
16092:
16047:
16042:
14811:
14666:
14637:
14443:
14171:
13915:
13514:
13th
International Conference on Interactive Theorem Proving (ITP 2022)
13469:. Lecture Notes in Computer Science. Vol. 2566. pp. 420–435.
13335:
12942:
12904:
12863:
12821:
12779:
12580:
12466:
Ariola and Blom employ 1) axioms for a representational calculus using
11171:
11060:
7195:
3571:
3495:
777:
575:
11561:
10835:
for other approaches to defining computability and their equivalence.
8632:
A linked list can be defined as either NIL for the empty list, or the
16478:
16296:
16221:
16200:
16130:
16082:
16062:
15963:
15866:
14919:
14836:
14796:
14760:
14696:
14508:
14498:
14471:
14234:
13725:
13434:
12368:
free variables in lambda
Notation and its Calculus are comparable to
11831:
11473:
11056:
11044:
10604:{\displaystyle (\;\lambda x.y\;\;(\lambda z.(zz)\;\lambda z.(zz))\;)}
8934:
8900:
8399:, it is straightforward to build a predicate for numerical equality.
7015:α-equivalence. Substitution is defined uniquely up to α-equivalence.
57:. Untyped lambda calculus, the topic of this article, is a universal
13986:
12934:
12896:
12855:
12813:
12771:
12572:
7581:, where '(mf)x' means the function 'f' is applied 'm' times on 'x':
16391:
16180:
15948:
15746:
15194:
14899:
14493:
13639:
11512:
11435:– A demonstration that some form of lambda calculus is inconsistent
11239:
are extensions of lambda calculus that are not in the lambda cube:
11218:
10641:
Weak reduction strategies do not reduce under lambda abstractions:
8868:; this means a recursive function definition cannot be used as the
7422:, and returns another single-argument function. The Church numeral
2512:
has not been defined and is considered an unknown. The abstraction
1896:
that can be applied to build all syntactically valid lambda terms:
1870:
1309:
13946:
13825:
13322:. Lecture Notes in Computer Science. Vol. 8560. p. 196.
13149:
11509:– A formal computing machine that is equivalent to lambda calculus
11453:– An abstract machine to interpret call-by-name in lambda calculus
11118:
have been developed for describing communication and concurrency.
10347:, but pass the argument on to only one subterm of an application (
6837:
notation, any two α-equivalent terms are syntactically identical.
4917:{\displaystyle ((\lambda x.y)x)=((\lambda x.y))(x)=(\lambda x.y)y}
15544:
14336:
13860:, a short (12 minutes) Computerphile video on the Lambda Calculus
11924:
by Peter Kelly, Paul Coddington, and Andrew Wendelborn; mentions
11723:
An Introduction to Functional Programming Through Lambda Calculus
11357:
11080:
8880:
construction would allow writing recursive function definitions.
7562:
We can define a successor function, which takes a Church numeral
6611:
We also speak of the resulting equivalences: two expressions are
1521:
whereas evaluation of the curried version requires one more step
13993:
13745:"A Correspondence between ALGOL 60 and Church's Lambda-notation"
13548:
Frandsen, Gudmund Skovbjerg; Sturtivant, Carl (26 August 1991).
13368:"Call-by-Value Lambda Calculus as a Model of Computation in Coq"
13109:
11564:. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.
11039:
and many other imperative languages have long supported passing
11024:
creates an anonymous function, given a list of parameter names,
8972:
In the lambda expression which is to represent this function, a
5307:, and the meaning of the function is preserved by substitution.
4365: ; substitution distributes to both sides of an application
402:, renaming the bound variables in the expression. Used to avoid
13520:. Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 7:1–7:19.
12144:
11562:
The Impact of the Lambda Calculus in Logic and Computer Science
11032:. Anonymous functions are sometimes called lambda expressions.
5075:. This erroneous substitution would turn the constant function
1005:
658:
13226:(29 Dec 2010) Haskell-cafe: What's the motivation for η rules?
11698:
A Correspondence Between ALGOL 60 and Church's Lambda-Notation
8230:
We are now able to compute some logic functions, for example:
7330:
and so on. Or using the alternative syntax presented above in
16256:
15088:
14434:
14279:
13891:
13815:
Written 1969, widely circulated as an unpublished manuscript.
12883:(1936). "An unsolvable problem of elementary number theory".
12258:
10942:
An unreasonable model does not necessarily mean inefficient.
10862:
is applied to its own Gödel number, a contradiction results.
8896:
SKI combinator calculus § Self-application and recursion
7012:
6705:
993:
914:{\displaystyle \operatorname {square\_sum} (x,y)=x^{2}+y^{2}}
156:
is a function definition, taking as input the bound variable
11185:
with the required property could be found, thus providing a
10958:
6565:
An expression that contains no free variables is said to be
5315:
The β-reduction rule states that an application of the form
1180:
function, that in turn accepts a single input. For example,
570:
Lambda calculus has applications in many different areas in
13414:
Types and Programming Languages, p. 273, Benjamin C. Pierce
12800:(July 1935). "The Inconsistency of Certain Formal Logics".
12758:(1932). "A set of postulates for the foundation of logic".
12541:
10948:
10489:, e.g. the simply typed lambda calculus is the language of
8402:
The availability of predicates and the above definition of
7097:, which in this context is that two functions are the same
7033:
3331:
A basic form of equivalence, definable on lambda terms, is
13934:
13507:"The Zoo of Lambda-Calculus Reduction Strategies, and Coq"
13313:"Preciseness of Subtyping on Intersection and Union Types"
13311:
Dezani-Ciancaglini, Mariangiola; Ghilezan, Silvia (2014).
13310:
11786:
An Introduction to Lambda Calculi for Computer Scientists,
11519:
functional programming language based on combinatory logic
10846:
for lambda expressions, he constructs a lambda expression
8817:, to permit writing the above in the more intuitive order
497:
of the reduction steps eventually terminates, then by the
12370:
linear algebra and mathematical concepts of the same name
11704:, vol. 8, no. 2 (1965), pages 89–101. Available from the
9468:
is the number we are calculating the factorial of. Given
7127:η-reduction can be seen to be the same as the concept of
7090:
7066:β-reduction can be seen to be the same as the concept of
65:(and vice versa). It was introduced by the mathematician
13550:"What is an efficient implementation of the λ-calculus?"
11259:
These formal systems are variations of lambda calculus:
6650:. The expression to which a redex reduces is called its
16022:
13504:
12921:(1940). "A Formulation of the Simple Theory of Types".
8786:(another lambda-term, the "main program"), one can say
7533:
times, starting from an empty list. The lambda term is
7234:
in lambda calculus, but by far the most common are the
5300:{\displaystyle (\lambda z.y)=\lambda z.(y)=\lambda z.x}
5068:{\displaystyle (\lambda x.y)=\lambda x.(y)=\lambda x.x}
4768:{\displaystyle (\lambda x.x)=\lambda x.(x)=\lambda x.x}
3657:
For example, the lambda term representing the identity
13916:
Alligator Eggs: A Puzzle Game Based on Lambda Calculus
12491:
Some parts of this article are based on material from
11215:– Lambda calculus with typed variables (and functions)
11139:, of functions on itself. However, no nontrivial such
10061:
Combinatory logic § Completeness of the S-K basis
9242:
In fact, there are many possible definitions for this
9235:
is re-created inside itself, at call-point, achieving
3102:
1826:
1741:
1635:
1530:
1500:
1456:
1376:
1324:
1133:
1014:
414:
331:
304:
284:
264:
244:
208:
186:
123:
97:
13786:"A type-theoretical alternative to ISWIM, CUCH, OWHY"
12559:(December 1937). "Computability and λ-Definability".
12511:
12509:
12507:
12419:
12399:
12339:
12304:
12267:
12228:
12162:
12129:
11963:
11277:– A notation for mathematical logic without variables
11270:
These formal systems are related to lambda calculus:
10617:
10529:
10417:
10355:
to the "function" subterm), thus saving a subsequent
5810:
5745:
5705:
5640:
5611:
5546:
5526:
5491:
5453:
5394:
5359:
5321:
5212:
5192:
5186:
the abstraction can be renamed with a fresh variable
5142:
5110:
5081:
4980:
4957:
4933:
4781:
4680:
4656:
4636:
4616:
4592:
4572:
4552:
4526:
4440:
4373:
4282:
4260:
4239:
4219:
4199:
4179:
4159:
4133:
4092:
4071:
4051:
4031:
4011:
3970:
3943:
3923:
3903:
3868:
3848:
3828:
3808:
3788:
3768:
3740:
3720:
3692:
3663:
3639:
3619:
3599:
3580:
3553:
3533:
3504:
3478:
3458:
3419:
3399:
3370:
3341:
3313:{\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))}
3261:
3237:
3211:
3179:
3153:
3120:
3076:
3053:
3033:
2983:
2963:
2943:
2923:
2903:
2868:
2830:
2810:
2781:
2742:
2722:
2702:
2653:
2622:
2569:
2518:
2473:
2432:
2400:
2386:, that is, it represents the act of calling function
2364:
2344:
2292:
2272:
2235:
2184:
2164:
2116:
2075:
2030:
1994:
1971:
1921:
1873:
is used to implement functions of several variables.
1804:
1784:
1719:
1699:
1253:
1189:
1101:
1057:
937:
834:
756:
733:
704:
671:
162:
12963:
11309:
8742:
6724:. Terms that differ only by α-conversion are called
5797:{\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}
2769:
12515:
11806:Sørensen, Morten Heine and Urzyczyn, Paweł (2006),
11252:– An extension of the lambda calculus for treating
8862:to be outside the scope of the abstraction binding
7018:
2286:is superfluous when using abstraction. The syntax
392:{\textstyle (\lambda x.M)\rightarrow (\lambda y.M)}
13547:
12504:
12425:
12405:
12351:
12325:
12282:
12249:
12199:
12135:
12071:
11465:– An expression closely related to an abstraction.
11147:constraints because the set of all functions from
10623:
10603:
10423:
8455:which can be verified by showing inductively that
7723:are β-equivalent lambda expressions. Since adding
7200:
7153:For the untyped lambda calculus, β-reduction as a
6478:in the expression is bound by the second lambda: λ
6017:
5796:
5720:
5691:
5626:
5597:
5532:
5512:
5477:
5439:
5380:
5345:
5299:
5198:
5178:
5125:
5096:
5067:
4963:
4939:
4916:
4767:
4662:
4642:
4622:
4598:
4578:
4558:
4538:
4512:
4424:
4357:
4269:
4245:
4225:
4205:
4185:
4165:
4145:
4119:
4077:
4057:
4037:
4017:
3997:
3949:
3929:
3909:
3889:
3854:
3834:
3814:
3794:
3774:
3746:
3726:
3707:
3678:
3645:
3625:
3605:
3586:
3559:
3539:
3519:
3484:
3464:
3425:
3405:
3385:
3356:
3312:
3243:
3223:
3194:
3165:
3135:
3091:
3059:
3039:
3019:
2969:
2949:
2929:
2909:
2889:
2854:
2816:
2796:
2748:
2728:
2708:
2689:
2637:
2608:
2545:
2500:
2459:
2415:
2370:
2350:
2313:
2278:
2254:
2221:
2170:
2150:
2090:
2055:
2003:
1980:
1942:
1835:
1810:
1790:
1770:
1733:in the inner expression. This is like β-reduction.
1725:
1705:
1685:
1620:
1509:
1485:
1441:
1359:
1297:
1233:
1168:
1113:
1081:
1040:
981:
913:
762:
742:
719:
686:
610:in the 1930s as part of an investigation into the
474:
391:
310:
290:
270:
250:
226:
192:
168:
144:
115:is a character or string representing a parameter.
103:
13628:
11609:An unsolvable problem of elementary number theory
11532:Structure and Interpretation of Computer Programs
11366:– The formal correspondence between programs and
6313:Applications are assumed to be left associative:
3757:
1604:
1533:
1367:function to the arguments (5, 2), yields at once
16697:
16489:Segmented discourse representation theory (SDRT)
13689:Electronic Notes in Theoretical Computer Science
11645:
11591:History of Lambda-calculus and Combinatory Logic
9974:systems that can express any lambda term - see
8636:of an element and a smaller list. The predicate
7956:can be validated by showing inductively that if
7225:
606:Lambda calculus was introduced by mathematician
73:. In 1936, Church found a formulation which was
13949:a simple yet powerful pure calculus interpreter
13119:so we cannot use this juxtaposition convention.
13083:
13081:
11381:– notation using postfix modification functions
8321:if its argument were any other Church numeral:
7194:The basic lambda calculus may be used to model
6638:is a β-redex in expressing the substitution of
6073:the abstraction symbols λ (lambda) and . (dot);
3107:In lambda calculus, functions are taken to be '
1298:{\displaystyle x\mapsto (y\mapsto x^{2}+y^{2})}
796:. Why did you choose lambda for your operator?
515:
13366:Forster, Yannick; Smolka, Gert (August 2019).
13236:
12957:
12838:(December 1942). "Review of Haskell B. Curry,
12716:
12200:{\displaystyle e::=x\mid \lambda x.e\mid e\,e}
11889:A Tutorial Introduction to the Lambda Calculus
11086:
11047:to other subprograms through the mechanism of
10831:meaning equivalence with β-reduction. See the
10381:combinator does only the latter, yielding the
8675:obviates the need for an explicit NULL test).
7230:There are several possible ways to define the
7142:
6569:. Closed lambda expressions are also known as
3067:. Both examples 1 and 2 would evaluate to the
1854:The lambda calculus consists of a language of
475:{\textstyle ((\lambda x.M)\ N)\rightarrow (M)}
69:in the 1930s as part of his research into the
16008:
14250:
14009:
13678:
13676:
13365:
13200:
13056:The Lambda Calculus: Its Syntax and Semantics
12875:
12873:
12742:Basic Category Theory for Computer Scientists
12659:Bunt, Harry; Muskens, Reinhard, eds. (2008).
12095:Barendregt, Barendsen (2000) call this form
11714:An Introduction to Lambda Calculus and Scheme
11684:A theory of positive integers in formal logic
11589:Cardone, Felice and Hindley, J. Roger, 2006.
11476:– Transformation of formulæ in formal systems
11401:– Rules for the evaluation of expressions in
11221:– A typed lambda calculus with type-variables
9990:, the smallest term that has no normal form.
8883:
7499:One way of thinking about the Church numeral
7168:However, it can be shown that β-reduction is
6976:
4948:
3613:is the union of the set of free variables of
1588:
1540:
13953:Lambda Calculus links on Lambda-the-Ultimate
13866:Step by Step Introduction to Lambda Calculus
13237:Felleisen, Matthias; Flatt, Matthew (2006),
13078:
12792:
12720:Introduction to Lambda Calculus using Racket
11441:– A semi-fictional organization of LISP and
11199:
11099:, even in parallel. This means that various
10469:Typed lambda calculi are closely related to
10263:can reduce by having the initial combinator
9975:
9758:Certain terms have commonly accepted names:
9725:4 × (3 × (2 × (1 × (1, if 0 = 0; else 0 × ((
8509:A pair (2-tuple) can be defined in terms of
7895:is considerably more difficult. The formula
7766:Similarly, multiplication can be defined as
6607:: which captures a notion of extensionality.
4566:does not appear among the free variables of
2158:is an abstraction representing the function
1442:{\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}
1124:where the input is simply mapped to itself.
16:Mathematical-logic system based on functions
13685:"(In)Efficiency and Reasonable Cost Models"
13129:
13127:
12658:
12605:(8 February 2006). Zalta, Edward N. (ed.).
11865:A Short Introduction to the Lambda Calculus
11459:– Formal definition of the lambda calculus.
11375:– notation disambiguating alpha conversions
11266:– A first-order analogue of lambda calculus
8541:returns the first element of the pair, and
7149:Normalization property (abstract rewriting)
6417:
6389:A sequence of abstractions is contracted: λ
4513:{\displaystyle (\lambda y.t)=\lambda y.(t)}
16015:
16001:
14442:
14257:
14243:
14016:
14002:
13714:
13712:
13673:
13170:
13049:
12870:
12840:The Inconsistency of Certain Formal Logics
12695:. Cambridge University Press. p. 57.
12393:The union of the set of free variables of
12380:The set of free variables of M, but with {
11822:, including more recent developments like
11799:Monographs/textbooks for graduate students
11748:
11720:
11530:Abelson, Harold & Gerald Jay Sussman.
10597:
10572:
10547:
10546:
10533:
10054:
6828:α-renaming to make name resolution trivial
6818:simpler by ensuring that no variable name
2609:{\displaystyle \lambda x.((\lambda x.x)x)}
2467:(which represents the function definition
13760:
13724:
13700:
13682:
13638:
13561:
13525:
13460:"Demonstrating Lambda Calculus Reduction"
13218:
13201:Turbak, Franklyn; Gifford, David (2008),
13148:
13110:"The Basic Grammar of Lambda Expressions"
12193:
12120:
12118:
11957:These rules produce expressions such as:
11673:
11410:– The theory of substitution, as used in
10959:Lambda calculus and programming languages
10503:Reduction strategy § Lambda calculus
10036:
8755:, effectively using lambda calculus as a
8023:
7206:
4425:{\displaystyle (\lambda x.t)=\lambda x.t}
3020:{\displaystyle (\lambda x.(\lambda x.x))}
2690:{\displaystyle (\lambda x.(\lambda x.x))}
2378:represents the application of a function
1360:{\textstyle \operatorname {square\_sum} }
1169:{\textstyle \operatorname {square\_sum} }
648:
80:Lambda calculus consists of constructing
13240:Programming Languages and Lambda Calculi
13203:Design concepts in programming languages
13133:
13124:
12685:
12631:
12150:
11940:graph reduction for lambda expressions).
11808:Lectures on the Curry–Howard isomorphism
11717:. A gentle introduction for programmers.
11192:This work also formed the basis for the
10392:
6601:: applying functions to their arguments;
6033:, strings, or other non-number objects.
4927:The freshness condition (requiring that
3686:has no free variables, but the function
1234:{\displaystyle (x,y)\mapsto x^{2}+y^{2}}
1082:{\displaystyle \operatorname {id} (x)=x}
982:{\displaystyle (x,y)\mapsto x^{2}+y^{2}}
13718:
13709:
13457:
13263:
13261:
13008:The Stanford Encyclopedia of Philosophy
12611:The Stanford Encyclopedia of Philosophy
12601:
11625:. Princeton: Princeton University Press
10496:
9682:4 × (3 × (2 × (1, if 1 = 0; else 1 × ((
8092:
1686:{\textstyle =(y\mapsto 5^{2}+y^{2})(2)}
807:
564:
16698:
14264:
13739:
13423:
13002:Alama, Jesse. Zalta, Edward N. (ed.).
12917:
12879:
12834:
12754:
12555:
12460:
12115:
12091:
12089:
12087:
12085:
11837:
11618:
11492:– A theorem about sets of lambda terms
11283:– A computational system based on the
10974:
10442:Typed lambda calculi are foundational
9246:operator, the simplest of them being:
8313:if its argument is the Church numeral
7657:, addition can be defined as follows:
2645:and is therefore an abstraction, while
1849:
1092:can be rewritten in anonymous form as
614:. The original system was shown to be
16444:Discourse representation theory (DRT)
15996:
14238:
14203:University of California, Los Angeles
13997:
13783:
13683:Accattoli, Beniamino (October 2018).
13594:
13040:at the University of Birmingham, UK.)
12717:Chacón Sartori, Camilo (2023-12-05).
11951:
7741:times, an alternative definition is:
7416:—it takes a single-argument function
7179:
6689:is also an η-redex, with a reduct of
6156:and instances of rule 3 are known as
5692:{\displaystyle (\lambda x.y)s\to y=y}
5598:{\displaystyle (\lambda x.x)s\to x=s}
4650:is "fresh" for the substitution term
557:typed lambda calculi can express less
13258:
13137:Lecture Notes on the Lambda Calculus
13089:"Example for Rules of Associativity"
12457:can be pronounced "let f be N in M".
11901:Lecture Notes on the Lambda Calculus
10854:Gödel's first incompleteness theorem
10304:throws the argument away, just like
7873:The predecessor function defined by
7428:is a function that takes a function
6588:There are three kinds of reduction:
6169:This set of rules may be written in
6052:Lambda expressions are composed of:
6036:
3326:
16357:Quantificational variability effect
16024:Formal semantics (natural language)
13980:Internet Encyclopedia of Philosophy
13900:Some executable λ-calculus examples
12971:Mathematical Methods in Linguistics
12211:Simply typed lambda calculus#Syntax
12082:
11921:Lambda Calculus as a Workflow Model
11341:– A setting for lambda calculus in
11335:in the style of the lambda calculus
10439:a special case with only one type.
10245:In either case, a term of the form
10073:), then there exists a lambda-term
7238:, which can be defined as follows:
7017:See Capture-avoiding substitutions
6354:The body of an abstraction extends
6296:Outermost parentheses are dropped:
5634:really is the identity. Similarly,
5440:{\displaystyle (\lambda x.t)s\to t}
3231:, the function that always returns
3103:Functions that operate on functions
2765:is a placeholder in both examples.
2151:{\displaystyle \lambda x.(x^{2}+2)}
176:(between the λ and the punctum/dot
112:
13:
13830:Mathematical and Computer Sciences
13320:Rewriting and Typed Lambda Calculi
13188:10.1111/j.1746-8361.1988.tb00919.x
12737:
12723:(Technical report). Archived from
11739:Schalk, A. and Simmons, H. (2005)
11721:Michaelson, Greg (10 April 2013).
11524:
10852:that closely follows the proof of
10481:and they can be considered as the
9639:4 × (3 × (1, if 2 = 0; else 2 × ((
8762:
6849:, is the process of replacing all
6458:. For example, in the expression λ
5746:
2099:
1892:The following three rules give an
1353:
1350:
1347:
1344:
1341:
1338:
1335:
1332:
1329:
1326:
1162:
1159:
1156:
1153:
1150:
1147:
1144:
1141:
1138:
1135:
863:
860:
857:
854:
851:
848:
845:
842:
839:
836:
322:The reduction operations include:
14:
16742:
14219:Alonzo Church (college president)
14023:
13850:
13030:Looking Backward; Looking Forward
13001:
12692:Concepts in Programming Languages
12413:and the set of free variables of
11131:isomorphic to the function space
11110:. One can add constructs such as
10365:in one subterm. In comparison to
9753:
8743:Additional programming techniques
7837:is the same as repeating the add
7575:by adding another application of
7093:reduction) expresses the idea of
6454:. All other variables are called
6152:Instances of rule 2 are known as
3961:manner. This is defined so that:
3633:and the set of free variables of
3439:
528:that can be used to simulate any
399:
81:
61:that can be used to simulate any
15976:
13965:Implementing the Lambda calculus
13604:Journal of Logic and Computation
13267:Zena M. Ariola and Stefan Blom,
12519:; Barendsen, Erik (March 2000),
12475:
12468:well-formed cyclic lambda graphs
11653:The Calculi of Lambda-Conversion
11622:The Calculi of Lambda-Conversion
11602:Handbook of the History of Logic
11486:designed for the lambda calculus
11411:
11312:
10711:
10448:functional programming languages
8747:There is a considerable body of
7735:can be accomplished by adding 1
7024:
6811:, which is not at all the same.
6446:is getting bound by prepending λ
3527:is the set of free variables of
2756:and is therefore an application.
2056:{\displaystyle \lambda x.x^{2}.}
1818:. Again, similar to β-reduction.
694:” used for class-abstraction by
592:Functional programming languages
482:
153:
13818:
13777:
13733:
13622:
13588:
13541:
13498:
13451:
13430:Types and Programming Languages
13417:
13408:
13359:
13304:
13284:
13278:
13230:
13194:
13164:
13102:
13043:
13022:
12995:
12911:
12885:American Journal of Mathematics
12828:
12786:
12748:
12731:
12710:
12522:Introduction to Lambda Calculus
12435:
12387:
12374:
12362:
12292:
12217:
12106:
11840:Types and Programming Languages
11688:American Journal of Mathematics
11675:10.1090/s0002-9904-1944-08090-7
11613:American Journal of Mathematics
11554:Introduction to Lambda Calculus
11227:– A typed lambda calculus with
8782:(some explicit lambda-term) in
7509:times'. For example, using the
6840:
6696:
6573:and are equivalent to terms in
6080:The set of lambda expressions,
2546:{\displaystyle \lambda x.(x+y)}
2460:{\displaystyle \lambda x.(x+y)}
1876:
770:” to “λ” for ease of printing.
588:theory of programming languages
16439:Combinatory categorial grammar
13375:Journal of Automated Reasoning
12679:
12652:
12625:
12595:
12549:
12531:
12343:
12320:
12305:
12244:
12229:
12130:
12066:
12063:
12051:
12048:
12045:
12024:
12018:
11997:
11985:
11964:
11600:. In Gabbay and Woods (eds.),
11573:Handbook of Mathematical Logic
11439:Knights of the Lambda Calculus
11114:to the lambda calculus. Other
10598:
10594:
10591:
10582:
10569:
10560:
10548:
10530:
10523:exists. For example, the term
10351:to the "argument" subterm and
9472:= 4, for example, this gives:
8844:A notable restriction of this
8757:low-level programming language
8753:programming language semantics
7525:by repeating 'prepend another
7081:
6442:, as a hint that the variable
6012:
5994:
5991:
5973:
5967:
5964:
5940:
5934:
5931:
5928:
5904:
5898:
5892:
5868:
5865:
5856:
5853:
5850:
5832:
5829:
5811:
5791:
5773:
5770:
5752:
5680:
5668:
5662:
5656:
5641:
5586:
5574:
5568:
5562:
5547:
5507:
5495:
5478:{\displaystyle (\lambda x.t)s}
5469:
5454:
5434:
5422:
5416:
5410:
5395:
5375:
5363:
5346:{\displaystyle (\lambda x.t)s}
5337:
5322:
5310:
5279:
5276:
5264:
5258:
5243:
5231:
5228:
5213:
5173:
5161:
5158:
5143:
5047:
5044:
5032:
5026:
5011:
4999:
4996:
4981:
4908:
4893:
4887:
4884:
4872:
4866:
4863:
4860:
4848:
4845:
4830:
4827:
4821:
4809:
4806:
4800:
4785:
4782:
4747:
4744:
4732:
4726:
4711:
4699:
4696:
4681:
4507:
4504:
4492:
4486:
4471:
4459:
4456:
4441:
4404:
4392:
4389:
4374:
4352:
4349:
4337:
4331:
4328:
4325:
4313:
4307:
4301:
4289:
4286:
4261:
4108:
4096:
3986:
3974:
3884:
3872:
3758:Capture-avoiding substitutions
3307:
3304:
3295:
3289:
3215:
3157:
3014:
3011:
2996:
2984:
2884:
2869:
2855:{\displaystyle (\lambda x.x)x}
2846:
2831:
2684:
2681:
2666:
2654:
2603:
2597:
2582:
2579:
2540:
2528:
2508:). In this term, the variable
2483:
2477:
2454:
2442:
2410:
2404:
2308:
2293:
2194:
2188:
2145:
2126:
1998:
1972:
1937:
1922:
1904:is itself a valid lambda term.
1846:to arrive at the same result.
1680:
1674:
1671:
1645:
1639:
1615:
1609:
1599:
1593:
1583:
1557:
1551:
1548:
1436:
1424:
1421:
1395:
1392:
1380:
1377:
1292:
1266:
1260:
1257:
1205:
1202:
1190:
1105:
1070:
1064:
953:
950:
938:
882:
870:
711:
678:
469:
466:
454:
448:
445:
442:
433:
418:
415:
386:
383:
377:
362:
359:
356:
353:
347:
332:
221:
209:
139:
124:
85:
1:
16217:Antecedent-contained deletion
15937:History of mathematical logic
12844:The Journal of Symbolic Logic
12561:The Journal of Symbolic Logic
12485:
12326:{\displaystyle (\lambda x.t)}
12250:{\displaystyle (\lambda x.t)}
11877:A timeline of lambda calculus
11569:The Type Free Lambda Calculus
11354:applicable to lambda calculus
11329:Applicative computing systems
11155:has greater cardinality than
10865:
10433:Kinds of typed lambda calculi
10411:that uses the lambda-symbol (
10359:if there is no occurrence of
10112:) removes all occurrences of
10006:, and can also be defined as
9596:4 × (1, if 3 = 0; else 3 × ((
7476:(considered as an operator);
7332:
7226:Arithmetic in lambda calculus
6047:
5179:{\displaystyle (\lambda x.y)}
3114:For example, the lambda term
2890:{\displaystyle (\lambda x.x)}
2314:{\displaystyle (\lambda x.t)}
2222:{\displaystyle f(x)=x^{2}+2,}
2021:
1943:{\displaystyle (\lambda x.t)}
812:
524:, that is, it is a universal
235:
77:, and documented it in 1940.
16731:Theoretical computer science
15862:Primitive recursive function
14044:Simply typed lambda calculus
13826:"Greg Michaelson's Homepage"
13805:10.1016/0304-3975(93)90095-B
13793:Theoretical Computer Science
13328:10.1007/978-3-319-08918-8_14
13273:(1997) Cyclic lambda calculi
13246:, p. 26, archived from
11567:Barendregt, Hendrik Pieter,
11560:Barendregt, Hendrik Pieter,
11348:Categorical abstract machine
11204:These extensions are in the
11121:
10760:such that for every pair of
10458:and, more indirectly, typed
10039:are commonly abbreviated as
9302: is a fixed-point of
7434:as argument and returns the
6853:occurrences of the variable
6580:
6323:may be written instead of ((
3862:are variables. The notation
3734:has a single free variable,
2011:is a lambda term (called an
1950:is a lambda term (called an
1048:"). Similarly, the function
636:simply typed lambda calculus
561:simply typed lambda calculus
516:Explanation and applications
74:
7:
13908:The Lambda Calculus and A++
13878:Encyclopedia of Mathematics
13702:10.1016/j.entcs.2018.10.003
13287:"Lambda Calculus and Types"
12213:for untyped lambda calculus
11305:
11087:Parallelism and concurrency
10491:Cartesian closed categories
10279:, just like β-reduction of
8022:are given below, one using
8018:. Two other definitions of
7143:Normal forms and confluence
6595:: changing bound variables;
6287:
5721:{\displaystyle \lambda x.y}
5627:{\displaystyle \lambda x.x}
5126:{\displaystyle \lambda x.x}
5097:{\displaystyle \lambda x.y}
3708:{\displaystyle \lambda x.y}
3679:{\displaystyle \lambda x.x}
3520:{\displaystyle \lambda x.t}
3386:{\displaystyle \lambda y.y}
3357:{\displaystyle \lambda x.x}
3195:{\displaystyle \lambda x.y}
3136:{\displaystyle \lambda x.x}
3092:{\displaystyle \lambda x.x}
3027:being applied to the input
2957:, is M applied to N, where
2797:{\displaystyle \lambda x.B}
2638:{\displaystyle \lambda x.B}
2091:{\displaystyle \lambda x.t}
10:
16747:
16098:Syntax–semantics interface
14926:Schröder–Bernstein theorem
14653:Monadic predicate calculus
14312:Foundations of mathematics
13973:Shane Steinert-Threlkeld,
13467:The Essence of Computation
13205:, MIT press, p. 251,
13051:Barendregt, Hendrik Pieter
13038:extract of a May 2016 talk
12632:Moortgat, Michael (1988).
12359:written in anonymous form.
12352:{\displaystyle x\mapsto t}
11550:Barendregt, Hendrik Pieter
11457:Lambda calculus definition
11196:of programming languages.
11178:were considered, a set or
10978:
10500:
10446:and are the base of typed
10396:
10324:has no free occurrence in
10132:. The conversion function
10058:
9958:is the identity function.
9132: to hold, so
9043: to hold, so
8893:
8887:
8884:Recursion and fixed points
8027:
7212:
7183:
7146:
6999:, because the substituted
6163:
6043:Lambda calculus definition
6040:
5699:, which demonstrates that
3897:indicates substitution of
3224:{\displaystyle x\mapsto y}
3166:{\displaystyle x\mapsto x}
2102:that takes a single input
1114:{\displaystyle x\mapsto x}
720:{\displaystyle {\hat {x}}}
687:{\displaystyle {\hat {x}}}
612:foundations of mathematics
601:
145:{\textstyle (\lambda x.M)}
71:foundations of mathematics
16632:
16590:Question under discussion
16540:Conversational scoreboard
16517:
16421:
16414:
16317:Intersective modification
16302:Homogeneity (linguistics)
16209:
16118:
16111:
16030:
15972:
15959:Philosophy of mathematics
15908:Automated theorem proving
15890:
15785:
15617:
15510:
15362:
15079:
15055:
15033:Von Neumann–Bernays–Gödel
14978:
14872:
14776:
14674:
14665:
14592:
14527:
14433:
14355:
14272:
14211:
14190:
14074:
14031:
13749:Communications of the ACM
13527:10.4230/LIPIcs.ITP.2022.7
13387:10.1007/s10817-018-9484-2
12923:Journal of Symbolic Logic
12802:The Annals of Mathematics
11838:Pierce, Benjamin (2002),
11768:10.1007/s11225-008-9150-5
11702:Communications of the ACM
11339:Cartesian closed category
11225:Calculus of constructions
11200:Variations and extensions
11189:for the lambda calculus.
10087:) which is equivalent to
9734:4 × (3 × (2 × (1 × (1))))
8519:Church encoding for pairs
5605:. This demonstrates that
5520:. For example, for every
5447:is used to indicate that
4358:{\displaystyle s)=(t)(s)}
1771:{\textstyle =5^{2}+2^{2}}
1486:{\textstyle =5^{2}+2^{2}}
180:) and returning the body
16650:Distributional semantics
13832:. Riccarton, Edinburgh:
13475:10.1007/3-540-36377-7_19
13172:de Queiroz, Ruy J. G. B.
13134:Selinger, Peter (2008),
12333:represents the function
12257:is sometimes written in
12136:{\displaystyle \mapsto }
11944:
11936:property, which enables
11507:Universal Turing machine
11364:Curry–Howard isomorphism
10991:
10872:computational complexity
10736:means computable by any
10479:Curry–Howard isomorphism
10424:{\displaystyle \lambda }
10002:is standard and defined
9553:1, if 4 = 0; else 4 × ((
9293:In the lambda calculus,
8809:Authors often introduce
8504:
7137:Curry–Howard isomorphism
7120:does not appear free in
7076:Curry–Howard isomorphism
6501:of a lambda expression,
6470:is a bound variable and
6418:Free and bound variables
6356:as far right as possible
6283: :== v1 | v2 | ...
6175:
5728:is a constant function.
2862:, an anonymous function
2501:{\displaystyle f(x)=x+y}
1041:{\textstyle x^{2}+y^{2}}
16645:Computational semantics
16382:Subsective modification
16186:Propositional attitudes
15609:Self-verifying theories
15430:Tarski's axiomatization
14381:Tarski's undefinability
14376:incompleteness theorems
13649:10.1145/2603088.2603105
13458:Sestoft, Peter (2002).
11913:Graphic lambda calculus
11725:. Courier Corporation.
11619:Church, Alonzo (1941).
11281:SKI combinator calculus
11067:, and more recently in
10437:untyped lambda calculus
10387:SKI combinator calculus
10300:returns that argument.
10055:Abstraction elimination
9691:4 × (3 × (2 × (1 × (G (
8945:recursively defined by
8644:. (Alternatively, with
8525:encapsulates the pair (
7885:for a positive integer
7458:times. This is denoted
7190:Mogensen–Scott encoding
6822:a name in a containing
4539:{\displaystyle x\neq y}
4146:{\displaystyle x\neq y}
2255:{\displaystyle x^{2}+2}
1965:are lambda terms, then
785:Dear Professor Church,
743:{\displaystyle \land x}
543:Lambda calculus may be
16675:Philosophy of language
16312:Inalienable possession
16292:Free choice inferences
16287:Faultless disagreement
16058:Generalized quantifier
15983:Mathematics portal
15594:Proof of impossibility
15242:propositional variable
14552:Propositional calculus
13947:LCI Lambda Interpreter
13834:Heriot-Watt University
13010:(Summer 2013 ed.)
12968:; Wall, R. E. (1990).
12638:. Foris Publications.
12613:(Summer 2013 ed.)
12427:
12407:
12353:
12327:
12284:
12251:
12201:
12137:
12073:
11750:de Queiroz, Ruy J.G.B.
11469:Minimalism (computing)
11417:Functional programming
11393:denotational semantics
11360:, programming language
11297:
11291:
11285:
11244:Binary lambda calculus
11194:denotational semantics
10969:procedural programming
10955:on pure lambda terms.
10625:
10605:
10460:imperative programming
10425:
10003:
9996:is another such term.
9700:4 × (3 × (2 × (1 × ((λ
9190:FIX G = G (FIX G) = (λ
8890:Fixed-point combinator
8767:In lambda calculus, a
7521:elements all equal to
7412:A Church numeral is a
6845:Substitution, written
6164:§ reducible expression
6019:
5798:
5722:
5693:
5628:
5599:
5534:
5514:
5479:
5441:
5382:
5347:
5301:
5200:
5180:
5127:
5098:
5069:
4965:
4941:
4918:
4769:
4664:
4644:
4624:
4600:
4580:
4560:
4540:
4514:
4426:
4359:
4271:
4247:
4227:
4207:
4187:
4167:
4147:
4121:
4079:
4059:
4039:
4019:
3999:
3951:
3931:
3911:
3891:
3856:
3836:
3822:are lambda terms, and
3816:
3796:
3776:
3748:
3728:
3709:
3680:
3647:
3627:
3607:
3588:
3561:
3541:
3521:
3486:
3466:
3452:The free variables of
3427:
3407:
3387:
3358:
3314:
3245:
3225:
3196:
3167:
3137:
3093:
3061:
3041:
3021:
2971:
2951:
2931:
2911:
2891:
2856:
2818:
2798:
2750:
2730:
2710:
2691:
2639:
2610:
2547:
2502:
2461:
2417:
2372:
2352:
2315:
2280:
2256:
2223:
2172:
2152:
2092:
2057:
2005:
1982:
1944:
1911:is a lambda term, and
1864:operational definition
1837:
1812:
1792:
1772:
1727:
1707:
1687:
1622:
1511:
1487:
1443:
1361:
1308:This method, known as
1299:
1235:
1170:
1115:
1083:
1042:
983:
915:
825:example, the function
802:eeny, meeny, miny, moe
798:
775:
764:
763:{\displaystyle \land }
744:
721:
698:, by first modifying “
688:
616:logically inconsistent
476:
393:
312:
292:
272:
252:
238:, applying a function
228:
194:
170:
146:
105:
16726:Models of computation
16570:Plural quantification
16464:Inquisitive semantics
16429:Alternative semantics
15852:Kolmogorov complexity
15805:Computably enumerable
15705:Model complete theory
15497:Principia Mathematica
14557:Propositional formula
14386:Banach–Tarski paradox
14097:George Alfred Barnard
14066:Church–Rosser theorem
14061:Frege–Church ontology
13988:Macro Lambda Calculus
13762:10.1145/363744.363749
13616:10.1093/logcom/exi010
13595:Sinot, F.-R. (2005).
13572:10.1007/3540543961_14
13004:"The Lambda Calculus"
12760:Annals of Mathematics
12538:explicit substitution
12428:
12408:
12354:
12328:
12285:
12252:
12202:
12138:
12074:
11930:distributed computing
11662:Bull. Amer. Math. Soc
11500:– An introduction to
11497:To Mock a Mockingbird
11433:Kleene–Rosser paradox
11408:Explicit substitution
11403:programming languages
11231:as first-class values
11213:Typed lambda calculus
11104:evaluation strategies
10926:explicit substitution
10626:
10606:
10444:programming languages
10426:
10405:typed lambda calculus
10399:Typed lambda calculus
10393:Typed lambda calculus
10385:as an alternative to
7452:composed with itself
7414:higher-order function
6020:
5799:
5723:
5694:
5629:
5600:
5535:
5515:
5480:
5442:
5383:
5348:
5302:
5201:
5181:
5128:
5099:
5070:
4966:
4942:
4919:
4770:
4665:
4645:
4625:
4601:
4581:
4561:
4541:
4515:
4427:
4360:
4272:
4248:
4228:
4208:
4188:
4168:
4148:
4122:
4080:
4060:
4040:
4020:
4000:
3952:
3932:
3912:
3892:
3857:
3837:
3817:
3797:
3777:
3749:
3729:
3710:
3681:
3648:
3628:
3608:
3589:
3574:of free variables of
3562:
3542:
3522:
3498:of free variables of
3487:
3467:
3428:
3408:
3388:
3359:
3315:
3246:
3226:
3197:
3168:
3138:
3094:
3062:
3042:
3022:
2972:
2952:
2932:
2912:
2892:
2857:
2819:
2799:
2751:
2731:
2711:
2692:
2640:
2611:
2548:
2503:
2462:
2418:
2373:
2353:
2316:
2281:
2257:
2224:
2173:
2153:
2093:
2058:
2006:
1983:
1945:
1838:
1813:
1793:
1778:// the definition of
1773:
1728:
1708:
1693:// the definition of
1688:
1623:
1512:
1488:
1444:
1362:
1300:
1244:can be reworked into
1236:
1171:
1116:
1084:
1043:
992:(which is read as "a
984:
916:
783:
765:
745:
722:
696:Whitehead and Russell
689:
663:
628:Kleene–Rosser paradox
499:Church–Rosser theorem
477:
394:
313:
293:
273:
253:
229:
195:
171:
147:
106:
16716:Computability theory
16555:Function application
16362:Responsive predicate
16352:Privative adjectives
15800:Church–Turing thesis
15787:Computability theory
14996:continuum hypothesis
14514:Square of opposition
14372:Gödel's completeness
14198:Princeton University
14049:Church–Turing thesis
13905:Georg P. Loczewski,
13784:Scott, Dana (1993).
12417:
12397:
12337:
12302:
12283:{\displaystyle Lx.t}
12265:
12226:
12160:
12127:
11961:
11830:. It does not cover
11820:typed lambda calculi
11352:model of computation
11176:continuous functions
11174:showed that if only
10833:Church–Turing thesis
10827:, respectively and =
10738:model of computation
10615:
10527:
10497:Reduction strategies
10415:
9308:, as it expands to:
9153: where
8640:tests for the value
8545:returns the second.
8204:IFTHENELSE := λ
8093:Logic and predicates
8026:and the other using
7446:, i.e. the function
7159:strongly normalising
6624:reducible expression
6426:. In an expression λ
6096:is a variable, then
5808:
5743:
5703:
5638:
5609:
5544:
5524:
5489:
5451:
5392:
5357:
5353:reduces to the term
5319:
5210:
5190:
5140:
5108:
5079:
4978:
4955:
4931:
4779:
4678:
4654:
4634:
4614:
4590:
4570:
4550:
4524:
4438:
4371:
4280:
4258:
4237:
4217:
4197:
4177:
4157:
4131:
4090:
4069:
4049:
4029:
4009:
3968:
3941:
3921:
3901:
3866:
3846:
3826:
3806:
3786:
3766:
3738:
3718:
3690:
3661:
3637:
3617:
3597:
3578:
3551:
3531:
3502:
3476:
3456:
3417:
3397:
3368:
3339:
3259:
3253:function composition
3235:
3209:
3177:
3151:
3118:
3074:
3051:
3031:
2981:
2961:
2941:
2921:
2901:
2866:
2828:
2808:
2779:
2740:
2720:
2700:
2651:
2620:
2567:
2516:
2471:
2430:
2416:{\displaystyle t(s)}
2398:
2362:
2342:
2290:
2270:
2233:
2182:
2162:
2114:
2100:§ anonymous function
2073:
2028:
1992:
1969:
1919:
1915:is a variable, then
1894:inductive definition
1824:
1802:
1782:
1739:
1717:
1697:
1633:
1528:
1498:
1454:
1374:
1322:
1316:Function application
1251:
1187:
1131:
1099:
1055:
1012:
935:
924:can be rewritten in
832:
818:Computable functions
808:Informal description
754:
731:
702:
669:
526:model of computation
495:repeated application
412:
329:
302:
282:
262:
242:
206:
184:
160:
121:
95:
75:logically consistent
59:model of computation
16640:Cognitive semantics
16605:Strawson entailment
16550:Existential closure
16494:Situation semantics
16397:Temperature paradox
16367:Rising declaratives
16332:Modal subordination
16307:Hurford disjunction
16267:Discourse relations
15954:Mathematical object
15845:P versus NP problem
15810:Computable function
15604:Reverse mathematics
15530:Logical consequence
15407:primitive recursive
15402:elementary function
15175:Free/bound variable
15028:Tarski–Grothendieck
14547:Logical connectives
14477:Logical equivalence
14327:Logical consequence
14132:Stephen Cole Kleene
14087:C. Anthony Anderson
13985:Anton Salikhmetov,
13425:Pierce, Benjamin C.
13271:Sendai, Japan 1997
13159:2008arXiv0804.3434S
12739:Pierce, Benjamin C.
11908:) by Peter Selinger
11604:, vol. 5. Elsevier.
11490:Scott–Curry theorem
11399:Evaluation strategy
11395:for lambda calculus
11387:– Study of certain
10975:Anonymous functions
10726:computable function
10136:can be defined by:
9972:combinator calculus
7651:-th composition of
7635:-th composition of
7623:-th composition of
7464:and is in fact the
7440:-th composition of
6505:, is denoted as FV(
6405:is abbreviated as λ
6086:defined inductively
4120:{\displaystyle y=y}
3998:{\displaystyle x=r}
2977:is the lambda term
2917:; while example 2,
1850:The lambda calculus
1798:has been used with
1713:has been used with
520:Lambda calculus is
227:{\textstyle (M\ N)}
16685:Semantics of logic
16610:Strict conditional
16580:Quantifier raising
16545:Downward entailing
16525:Autonomy of syntax
16454:Generative grammar
16434:Categorial grammar
16372:Scalar implicature
16277:Epistemic modality
16252:De dicto and de re
15752:Transfer principle
15715:Semantics of logic
15700:Categorical theory
15676:Non-standard model
15190:Logical connective
14317:Information theory
14266:Mathematical logic
14162:Hartley Rogers, Jr
14127:John George Kemeny
13940:2021-05-02 at the
13928:2012-10-14 at the
13091:. Lambda-bound.com
12964:Partee, B. B. H.;
12794:Kleene, Stephen C.
12423:
12403:
12349:
12323:
12280:
12247:
12197:
12133:
12069:
11596:2021-05-06 at the
11379:De Bruijn notation
11320:Mathematics portal
11250:Lambda-mu calculus
11079:("delegates") and
10981:Anonymous function
10963:As pointed out by
10881:in the expression
10621:
10601:
10471:mathematical logic
10421:
10275:grab the argument
9648:4 × (3 × (2 × (G (
9058:F := G G = (λ
8854:be not defined in
8749:programming idioms
8702:can be defined as
7825:since multiplying
7629:composed with the
7180:Encoding datatypes
7163:weakly normalising
7129:local completeness
7068:local reducibility
6857:in the expression
6774:variable shadowing
6654:; the reduct of (λ
6109:is a variable and
6015:
5794:
5718:
5689:
5624:
5595:
5530:
5510:
5475:
5437:
5378:
5343:
5297:
5196:
5176:
5123:
5104:into the identity
5094:
5065:
4961:
4937:
4914:
4765:
4660:
4640:
4620:
4596:
4576:
4556:
4536:
4510:
4422:
4355:
4270:{\displaystyle (t}
4267:
4243:
4223:
4203:
4183:
4163:
4143:
4117:
4075:
4055:
4035:
4015:
3995:
3947:
3927:
3907:
3887:
3852:
3832:
3812:
3792:
3772:
3744:
3724:
3705:
3676:
3643:
3623:
3603:
3584:
3557:
3537:
3517:
3482:
3462:
3423:
3403:
3383:
3354:
3310:
3255:can be defined as
3241:
3221:
3192:
3163:
3133:
3109:first class values
3089:
3057:
3037:
3017:
2967:
2947:
2927:
2907:
2887:
2852:
2814:
2794:
2746:
2726:
2706:
2687:
2635:
2606:
2543:
2498:
2457:
2413:
2368:
2348:
2311:
2276:
2252:
2219:
2168:
2148:
2088:
2053:
2004:{\displaystyle s)}
2001:
1981:{\displaystyle (t}
1978:
1940:
1833:
1808:
1788:
1768:
1723:
1703:
1683:
1618:
1507:
1483:
1439:
1357:
1295:
1231:
1166:
1111:
1079:
1038:
979:
911:
792:, Hilbert had the
760:
740:
717:
684:
501:it will produce a
491:De Bruijn indexing
472:
389:
308:
288:
268:
248:
224:
190:
166:
154:lambda abstraction
142:
101:
41:based on function
35:mathematical logic
16711:1936 in computing
16693:
16692:
16665:Logic translation
16628:
16627:
16620:Universal grinder
16600:Squiggle operator
16560:Meaning postulate
16499:Supervaluationism
16469:Intensional logic
16449:Dynamic semantics
16410:
16409:
16242:Crossover effects
16191:Tense–aspect–mood
16171:Lexical semantics
15990:
15989:
15922:Abstract category
15725:Theories of truth
15535:Rule of inference
15525:Natural deduction
15506:
15505:
15051:
15050:
14756:Cartesian product
14661:
14660:
14567:Many-valued logic
14542:Boolean functions
14425:Russell's paradox
14400:diagonal argument
14297:First-order logic
14232:
14231:
14167:J. Barkley Rosser
13935:Safalra's Website
13889:David C. Keenan,
13873:"Lambda-calculus"
13633:. pp. 1–10.
13484:978-3-540-00326-7
13345:978-3-319-08917-1
13212:978-0-262-20175-9
13036:. (See also this
12702:978-0-521-78098-8
12687:Mitchell, John C.
12672:978-1-4020-5957-5
12662:Computing Meaning
12426:{\displaystyle N}
12406:{\displaystyle M}
12209:from Knowledge's
12059:
12041:
12023:
12014:
11824:pure type systems
11732:978-0-486-28029-5
11682:Kleene, Stephen,
11655:by Alonzo Church"
11640:978-0-691-08394-0
11502:combinatory logic
11275:Combinatory logic
11049:function pointers
10944:Optimal reduction
10819:corresponding to
10697:Optimal reduction
10634:Full β-reductions
10624:{\displaystyle y}
10519:Applicative order
10483:internal language
10383:B, C, K, W system
9657:4 × (3 × (2 × ((λ
8848:is that the name
8673:) (deal_with_nil)
8646:NIL := FALSE
8495:− 1 function for
8294:is equivalent to
7490:laws of exponents
7133:natural deduction
7072:natural deduction
6744:could result in λ
6575:combinatory logic
6037:Formal definition
5533:{\displaystyle s}
5513:{\displaystyle t}
5381:{\displaystyle t}
5199:{\displaystyle z}
4964:{\displaystyle r}
4940:{\displaystyle y}
4663:{\displaystyle r}
4643:{\displaystyle y}
4623:{\displaystyle r}
4599:{\displaystyle y}
4579:{\displaystyle r}
4559:{\displaystyle y}
4246:{\displaystyle y}
4226:{\displaystyle x}
4206:{\displaystyle y}
4186:{\displaystyle x}
4166:{\displaystyle r}
4078:{\displaystyle r}
4058:{\displaystyle x}
4038:{\displaystyle x}
4018:{\displaystyle r}
3950:{\displaystyle t}
3930:{\displaystyle x}
3910:{\displaystyle r}
3890:{\displaystyle t}
3855:{\displaystyle y}
3835:{\displaystyle x}
3815:{\displaystyle r}
3795:{\displaystyle s}
3775:{\displaystyle t}
3747:{\displaystyle y}
3727:{\displaystyle x}
3646:{\displaystyle s}
3626:{\displaystyle t}
3606:{\displaystyle s}
3587:{\displaystyle t}
3560:{\displaystyle x}
3540:{\displaystyle t}
3485:{\displaystyle x}
3465:{\displaystyle x}
3426:{\displaystyle y}
3406:{\displaystyle x}
3333:alpha equivalence
3327:Alpha equivalence
3244:{\displaystyle y}
3204:constant function
3145:identity function
3069:identity function
3060:{\displaystyle x}
3040:{\displaystyle N}
2970:{\displaystyle M}
2950:{\displaystyle N}
2930:{\displaystyle M}
2910:{\displaystyle x}
2817:{\displaystyle B}
2749:{\displaystyle N}
2729:{\displaystyle M}
2709:{\displaystyle x}
2371:{\displaystyle s}
2351:{\displaystyle t}
2279:{\displaystyle f}
2171:{\displaystyle f}
1860:equational theory
1811:{\displaystyle 2}
1791:{\displaystyle y}
1726:{\displaystyle 5}
1706:{\displaystyle x}
714:
681:
438:
318:are lambda terms.
217:
169:{\displaystyle x}
22:(also written as
16738:
16670:Linguistics wars
16595:Semantic parsing
16484:Montague grammar
16419:
16418:
16262:Deontic modality
16116:
16115:
16103:Truth conditions
16038:Compositionality
16031:Central concepts
16017:
16010:
16003:
15994:
15993:
15981:
15980:
15932:History of logic
15927:Category of sets
15820:Decision problem
15599:Ordinal analysis
15540:Sequent calculus
15438:Boolean algebras
15378:
15377:
15352:
15323:logical/constant
15077:
15076:
15063:
14986:Zermelo–Fraenkel
14737:Set operations:
14672:
14671:
14609:
14440:
14439:
14420:Löwenheim–Skolem
14307:Formal semantics
14259:
14252:
14245:
14236:
14235:
14182:Raymond Smullyan
14157:Nicholas Rescher
14152:Michael O. Rabin
14018:
14011:
14004:
13995:
13994:
13975:"Lambda Calculi"
13886:
13845:
13844:
13842:
13840:
13822:
13816:
13814:
13812:
13811:
13799:(1–2): 411–440.
13790:
13781:
13775:
13774:
13764:
13737:
13731:
13730:
13728:
13716:
13707:
13706:
13704:
13680:
13671:
13670:
13642:
13626:
13620:
13619:
13601:
13592:
13586:
13585:
13565:
13545:
13539:
13538:
13536:
13534:
13529:
13511:
13502:
13496:
13495:
13493:
13491:
13464:
13455:
13449:
13448:
13421:
13415:
13412:
13406:
13405:
13403:
13401:
13372:
13363:
13357:
13356:
13354:
13352:
13317:
13308:
13302:
13301:
13299:
13297:
13291:
13282:
13276:
13265:
13256:
13254:
13252:
13245:
13234:
13228:
13222:
13216:
13215:
13198:
13192:
13191:
13168:
13162:
13161:
13152:
13142:
13131:
13122:
13121:
13106:
13100:
13099:
13097:
13096:
13085:
13076:
13070:
13047:
13041:
13026:
13020:
13019:
13017:
13015:
12999:
12993:
12992:
12990:
12988:
12961:
12955:
12954:
12915:
12909:
12908:
12877:
12868:
12867:
12832:
12826:
12825:
12790:
12784:
12783:
12752:
12746:
12745:
12735:
12729:
12728:
12714:
12708:
12706:
12683:
12677:
12676:
12656:
12650:
12649:
12629:
12623:
12622:
12620:
12618:
12603:Coquand, Thierry
12599:
12593:
12592:
12553:
12547:
12535:
12529:
12528:
12527:
12517:Barendregt, Henk
12513:
12479:
12473:
12464:
12458:
12453:
12447:
12439:
12433:
12432:
12430:
12429:
12424:
12412:
12410:
12409:
12404:
12391:
12385:
12378:
12372:
12366:
12360:
12358:
12356:
12355:
12350:
12332:
12330:
12329:
12324:
12298:The lambda term
12296:
12290:
12289:
12287:
12286:
12281:
12256:
12254:
12253:
12248:
12221:
12215:
12206:
12204:
12203:
12198:
12154:
12148:
12142:
12140:
12139:
12134:
12122:
12113:
12110:
12104:
12093:
12080:
12078:
12076:
12075:
12070:
12057:
12039:
12021:
12012:
11955:
11916:by Marius Buliga
11852:
11779:
11736:
11679:
11677:
11659:
11647:Frink Jr., Orrin
11633:
11631:
11630:
11607:Church, Alonzo,
11428:Interaction nets
11322:
11317:
11316:
11101:nondeterministic
11083:, among others.
11065:Wolfram Language
11031:
11027:
11023:
11016:
11013:
11010:
11007:
11004:
11001:
10998:
10995:
10985:For example, in
10922:Director strings
10919:
10898:
10892:
10886:
10880:
10861:
10851:
10814:
10808:
10802:
10792:
10723:
10719:
10688:
10673:
10630:
10628:
10627:
10622:
10610:
10608:
10607:
10602:
10430:
10428:
10427:
10422:
10364:
10335:The combinators
10323:
10317:
10311:
10292:
10286:
10254:
10236:
10222:
10202:
10186:
10169:
10154:
10148:
10131:
10117:
10107:
10094:
10082:
10050:
10044:
10034:
10030:
10026:
10015:
10001:
9995:
9989:
9983:
9976:the next section
9969:
9963:
9957:
9949:
9938:
9912:
9887:
9858:
9827:
9808:
9774:
9749:
9740:
9735:
9730:
9721:
9720:−1)))) (1−1)))))
9696:
9687:
9678:
9653:
9644:
9635:
9610:
9601:
9592:
9567:
9558:
9549:
9524:
9491:
9482:
9463:
9449:
9434:
9396:
9361:
9319:
9307:
9301:
9289:
9245:
9234:
9230:
9226:
9218:
9207:
9183:
9152:
9142:
9131:
9107:
9070:
9049:
9042:
9015:
8981:
8967:
8944:
8925:
8879:
8875:
8867:
8853:
8847:
8833:
8827:
8816:
8802:
8796:
8777:
8738:
8720:
8715:) (SUCC (SECOND
8701:
8689:
8674:
8665:.deal_with_head_
8648:, the construct
8647:
8643:
8639:
8635:
8628:
8607:
8598:
8589:SECOND := λ
8585:
8572:
8544:
8540:
8536:
8530:
8524:
8516:
8512:
8500:
8494:
8488:
8451:
8409:
8405:
8398:
8388:
8378:
8364:
8339:
8326:ISZERO := λ
8320:
8316:
8312:
8309:, which returns
8308:
8297:
8293:
8290:and we see that
8284:
8263:
8236:
8226:
8200:
8187:
8165:
8138:
8122:
8104:
8100:
8088:
8084:
8074:
8064:
8051:
8021:
8017:
8010:
7982:
7952:
7894:
7890:
7884:
7869:
7848:
7842:
7836:
7830:
7821:
7795:
7762:
7740:
7734:
7728:
7719:
7709:
7702:
7696:
7656:
7650:
7640:
7634:
7628:
7622:
7613:
7580:
7574:
7567:
7555:
7516:
7512:
7504:
7495:
7487:
7481:
7475:
7469:
7463:
7457:
7451:
7445:
7439:
7433:
7427:
7421:
7408:
7384:
7364:
7349:
7326:
7298:
7274:
7255:
7063:× 2) 7 → 7 × 2.
6991:) to result in λ
6977:above for the FV
6861:with expression
6561:
6438:is often called
6282:
6279:
6276:
6272:
6269:
6266:
6263:
6260:
6257:
6253:
6250:
6247:
6244:
6241:
6238:
6234:
6231:
6228:
6224:
6221:
6218:
6215:
6212:
6209:
6205:
6202:
6199:
6195:
6192:
6189:
6185:
6182:
6179:
6171:Backus–Naur form
6148:
6140:
6127:
6115:
6102:
6083:
6024:
6022:
6021:
6016:
5803:
5801:
5800:
5795:
5727:
5725:
5724:
5719:
5698:
5696:
5695:
5690:
5633:
5631:
5630:
5625:
5604:
5602:
5601:
5596:
5539:
5537:
5536:
5531:
5519:
5517:
5516:
5511:
5484:
5482:
5481:
5476:
5446:
5444:
5443:
5438:
5387:
5385:
5384:
5379:
5352:
5350:
5349:
5344:
5306:
5304:
5303:
5298:
5205:
5203:
5202:
5197:
5185:
5183:
5182:
5177:
5132:
5130:
5129:
5124:
5103:
5101:
5100:
5095:
5074:
5072:
5071:
5066:
4970:
4968:
4967:
4962:
4946:
4944:
4943:
4938:
4923:
4921:
4920:
4915:
4774:
4772:
4771:
4766:
4669:
4667:
4666:
4661:
4649:
4647:
4646:
4641:
4629:
4627:
4626:
4621:
4605:
4603:
4602:
4597:
4585:
4583:
4582:
4577:
4565:
4563:
4562:
4557:
4545:
4543:
4542:
4537:
4519:
4517:
4516:
4511:
4431:
4429:
4428:
4423:
4364:
4362:
4361:
4356:
4276:
4274:
4273:
4268:
4252:
4250:
4249:
4244:
4232:
4230:
4229:
4224:
4212:
4210:
4209:
4204:
4192:
4190:
4189:
4184:
4173:substituted for
4172:
4170:
4169:
4164:
4152:
4150:
4149:
4144:
4126:
4124:
4123:
4118:
4084:
4082:
4081:
4076:
4064:
4062:
4061:
4056:
4044:
4042:
4041:
4036:
4025:substituted for
4024:
4022:
4021:
4016:
4004:
4002:
4001:
3996:
3959:capture-avoiding
3956:
3954:
3953:
3948:
3936:
3934:
3933:
3928:
3916:
3914:
3913:
3908:
3896:
3894:
3893:
3888:
3861:
3859:
3858:
3853:
3841:
3839:
3838:
3833:
3821:
3819:
3818:
3813:
3801:
3799:
3798:
3793:
3781:
3779:
3778:
3773:
3753:
3751:
3750:
3745:
3733:
3731:
3730:
3725:
3714:
3712:
3711:
3706:
3685:
3683:
3682:
3677:
3652:
3650:
3649:
3644:
3632:
3630:
3629:
3624:
3612:
3610:
3609:
3604:
3593:
3591:
3590:
3585:
3566:
3564:
3563:
3558:
3546:
3544:
3543:
3538:
3526:
3524:
3523:
3518:
3491:
3489:
3488:
3483:
3471:
3469:
3468:
3463:
3432:
3430:
3429:
3424:
3412:
3410:
3409:
3404:
3392:
3390:
3389:
3384:
3363:
3361:
3360:
3355:
3319:
3317:
3316:
3311:
3250:
3248:
3247:
3242:
3230:
3228:
3227:
3222:
3201:
3199:
3198:
3193:
3172:
3170:
3169:
3164:
3142:
3140:
3139:
3134:
3098:
3096:
3095:
3090:
3066:
3064:
3063:
3058:
3046:
3044:
3043:
3038:
3026:
3024:
3023:
3018:
2976:
2974:
2973:
2968:
2956:
2954:
2953:
2948:
2936:
2934:
2933:
2928:
2916:
2914:
2913:
2908:
2896:
2894:
2893:
2888:
2861:
2859:
2858:
2853:
2823:
2821:
2820:
2815:
2803:
2801:
2800:
2795:
2764:
2755:
2753:
2752:
2747:
2735:
2733:
2732:
2727:
2715:
2713:
2712:
2707:
2696:
2694:
2693:
2688:
2644:
2642:
2641:
2636:
2615:
2613:
2612:
2607:
2556:
2552:
2550:
2549:
2544:
2511:
2507:
2505:
2504:
2499:
2466:
2464:
2463:
2458:
2422:
2420:
2419:
2414:
2393:
2389:
2385:
2381:
2377:
2375:
2374:
2369:
2357:
2355:
2354:
2349:
2331:
2327:
2320:
2318:
2317:
2312:
2285:
2283:
2282:
2277:
2265:
2261:
2259:
2258:
2253:
2245:
2244:
2228:
2226:
2225:
2220:
2209:
2208:
2177:
2175:
2174:
2169:
2157:
2155:
2154:
2149:
2138:
2137:
2109:
2105:
2097:
2095:
2094:
2089:
2062:
2060:
2059:
2054:
2049:
2048:
2010:
2008:
2007:
2002:
1987:
1985:
1984:
1979:
1964:
1960:
1949:
1947:
1946:
1941:
1914:
1910:
1903:
1842:
1840:
1839:
1836:{\textstyle =29}
1834:
1817:
1815:
1814:
1809:
1797:
1795:
1794:
1789:
1777:
1775:
1774:
1769:
1767:
1766:
1754:
1753:
1732:
1730:
1729:
1724:
1712:
1710:
1709:
1704:
1692:
1690:
1689:
1684:
1670:
1669:
1657:
1656:
1627:
1625:
1624:
1619:
1608:
1607:
1592:
1591:
1582:
1581:
1569:
1568:
1544:
1543:
1537:
1536:
1516:
1514:
1513:
1510:{\textstyle =29}
1508:
1492:
1490:
1489:
1484:
1482:
1481:
1469:
1468:
1448:
1446:
1445:
1440:
1420:
1419:
1407:
1406:
1366:
1364:
1363:
1358:
1356:
1304:
1302:
1301:
1296:
1291:
1290:
1278:
1277:
1240:
1238:
1237:
1232:
1230:
1229:
1217:
1216:
1175:
1173:
1172:
1167:
1165:
1120:
1118:
1117:
1112:
1088:
1086:
1085:
1080:
1047:
1045:
1044:
1039:
1037:
1036:
1024:
1023:
1003:
999:
988:
986:
985:
980:
978:
977:
965:
964:
920:
918:
917:
912:
910:
909:
897:
896:
866:
794:epsilon operator
788:Russell had the
769:
767:
766:
761:
749:
747:
746:
741:
726:
724:
723:
718:
716:
715:
707:
693:
691:
690:
685:
683:
682:
674:
643:Richard Montague
584:computer science
536:a variable in a
481:
479:
478:
473:
436:
398:
396:
395:
390:
317:
315:
314:
309:
297:
295:
294:
289:
277:
275:
274:
269:
257:
255:
254:
249:
233:
231:
230:
225:
215:
199:
197:
196:
191:
175:
173:
172:
167:
151:
149:
148:
143:
110:
108:
107:
102:
16746:
16745:
16741:
16740:
16739:
16737:
16736:
16735:
16706:Lambda calculus
16696:
16695:
16694:
16689:
16624:
16513:
16474:Lambda calculus
16406:
16377:Sloppy identity
16337:Opaque contexts
16272:Donkey anaphora
16237:Counterfactuals
16205:
16107:
16026:
16021:
15991:
15986:
15975:
15968:
15913:Category theory
15903:Algebraic logic
15886:
15857:Lambda calculus
15795:Church encoding
15781:
15757:Truth predicate
15613:
15579:Complete theory
15502:
15371:
15367:
15363:
15358:
15350:
15070: and
15066:
15061:
15047:
15023:New Foundations
14991:axiom of choice
14974:
14936:Gödel numbering
14876: and
14868:
14772:
14657:
14607:
14588:
14537:Boolean algebra
14523:
14487:Equiconsistency
14452:Classical logic
14429:
14410:Halting problem
14398: and
14374: and
14362: and
14361:
14356:Theorems (
14351:
14268:
14263:
14233:
14228:
14207:
14186:
14137:Simon B. Kochen
14070:
14054:Church encoding
14039:Lambda calculus
14027:
14022:
13959:Lambda Animator
13942:Wayback Machine
13930:Wayback Machine
13923:Lambda Calculus
13871:
13863:Helmut Brandl,
13858:Lambda Calculus
13856:Graham Hutton,
13853:
13848:
13838:
13836:
13824:
13823:
13819:
13809:
13807:
13788:
13782:
13778:
13738:
13734:
13717:
13710:
13681:
13674:
13659:
13627:
13623:
13599:
13593:
13589:
13582:
13563:10.1.1.139.6913
13546:
13542:
13532:
13530:
13509:
13503:
13499:
13489:
13487:
13485:
13462:
13456:
13452:
13445:
13422:
13418:
13413:
13409:
13399:
13397:
13370:
13364:
13360:
13350:
13348:
13346:
13315:
13309:
13305:
13295:
13293:
13289:
13285:Ker, Andrew D.
13283:
13279:
13266:
13259:
13250:
13243:
13235:
13231:
13223:
13219:
13213:
13199:
13195:
13169:
13165:
13140:
13132:
13125:
13108:
13107:
13103:
13094:
13092:
13087:
13086:
13079:
13067:
13048:
13044:
13027:
13023:
13013:
13011:
13000:
12996:
12986:
12984:
12982:
12962:
12958:
12935:10.2307/2266170
12916:
12912:
12897:10.2307/2371045
12878:
12871:
12856:10.2307/2268117
12833:
12829:
12814:10.2307/1968646
12791:
12787:
12772:10.2307/1968337
12753:
12749:
12736:
12732:
12715:
12711:
12703:
12684:
12680:
12673:
12657:
12653:
12646:
12630:
12626:
12616:
12614:
12600:
12596:
12573:10.2307/2268280
12557:Turing, Alan M.
12554:
12550:
12536:
12532:
12525:
12514:
12505:
12488:
12483:
12482:
12476:§ call-by-value
12471:
12465:
12461:
12451:
12441:
12440:
12436:
12418:
12415:
12414:
12398:
12395:
12394:
12392:
12388:
12379:
12375:
12367:
12363:
12338:
12335:
12334:
12303:
12300:
12299:
12297:
12293:
12266:
12263:
12262:
12227:
12224:
12223:
12222:
12218:
12161:
12158:
12157:
12155:
12151:
12143:is pronounced "
12128:
12125:
12124:
12123:
12116:
12111:
12107:
12094:
12083:
11962:
11959:
11958:
11956:
11952:
11947:
11926:graph reduction
11896:) by Raúl Rojas
11884:) by Dana Scott
11872:) by Achim Jung
11850:
11784:Hankin, Chris,
11733:
11657:
11628:
11626:
11598:Wayback Machine
11571:pp1091–1132 of
11527:
11525:Further reading
11522:
11484:virtual machine
11451:Krivine machine
11373:De Bruijn index
11343:category theory
11331:– Treatment of
11318:
11311:
11308:
11254:classical logic
11202:
11124:
11116:process calculi
11089:
11029:
11025:
11021:
11018:
11017:
11014:
11011:
11008:
11005:
11002:
10999:
10996:
10993:
10983:
10977:
10961:
10915:
10894:
10888:
10882:
10876:
10868:
10857:
10847:
10844:Gödel numbering
10830:
10817:Church numerals
10810:
10804:
10798:
10796:
10788:
10784:if and only if
10742:Turing complete
10721:
10717:
10714:
10675:
10656:
10649:substituted in.
10616:
10613:
10612:
10528:
10525:
10524:
10505:
10499:
10416:
10413:
10412:
10401:
10395:
10360:
10343:are similar to
10319:
10315:
10305:
10290:
10280:
10250:
10232:
10218:
10198:
10187:is not free in
10182:
10165:
10150:
10144:
10127:
10113:
10103:
10088:
10078:
10063:
10057:
10046:
10040:
10032:
10028:
10017:
10007:
9997:
9991:
9985:
9979:
9965:
9959:
9953:
9941:
9915:
9890:
9861:
9830:
9811:
9777:
9762:
9756:
9745:
9738:
9733:
9724:
9699:
9690:
9681:
9677:−1)))) (2−1))))
9656:
9647:
9638:
9613:
9604:
9595:
9570:
9561:
9552:
9527:
9494:
9485:
9476:
9454:
9437:
9399:
9364:
9322:
9312:
9303:
9294:
9250:
9243:
9232:
9228:
9224:
9216:
9189:
9188:so that
9154:
9151:F := FIX G
9150:
9133:
9113:
9081:
9057:
9044:
9021:
8986:
8977:
8949:
8938:
8909:
8898:
8892:
8886:
8877:
8873:
8863:
8849:
8845:
8831:
8821:
8814:
8811:syntactic sugar
8800:
8790:
8773:
8765:
8763:Named constants
8745:
8728:
8706:
8691:
8679:
8649:
8645:
8641:
8637:
8633:
8610:
8601:
8588:
8576:FIRST := λ
8575:
8549:
8542:
8538:
8532:
8526:
8522:
8521:. For example,
8517:, by using the
8514:
8510:
8507:
8496:
8490:
8456:
8414:
8407:
8403:
8390:
8380:
8370:
8347:
8325:
8318:
8314:
8310:
8306:
8295:
8291:
8282:
8266:
8262:TRUE FALSE TRUE
8261:
8239:
8234:
8203:
8190:
8168:
8146:
8126:FALSE := λ
8125:
8109:
8102:
8098:
8095:
8086:
8076:
8066:
8056:
8034:
8019:
8012:
7984:
7961:
7899:
7892:
7886:
7874:
7853:
7844:
7838:
7832:
7826:
7803:
7770:
7745:
7736:
7730:
7724:
7717:
7707:
7700:
7661:
7652:
7642:
7636:
7630:
7624:
7618:
7585:
7576:
7569:
7563:
7537:
7514:
7510:
7500:
7493:
7483:
7477:
7471:
7465:
7459:
7453:
7447:
7441:
7435:
7429:
7423:
7417:
7387:
7367:
7352:
7340:
7301:
7277:
7258:
7242:
7236:Church numerals
7232:natural numbers
7228:
7192:
7186:Church encoding
7184:Main articles:
7182:
7151:
7145:
7084:
7027:
6920:
6914:
6907:
6901:
6843:
6835:De Bruijn index
6816:name resolution
6756:, but it could
6699:
6677:is not free in
6583:
6547:
6420:
6290:
6285:
6284:
6280:
6277:
6274:
6270:
6267:
6264:
6261:
6258:
6255:
6251:
6248:
6245:
6242:
6239:
6236:
6232:
6229:
6226:
6222:
6219:
6216:
6213:
6210:
6207:
6203:
6200:
6197:
6193:
6190:
6187:
6183:
6180:
6177:
6142:
6131:
6117:
6110:
6097:
6081:
6076:parentheses ().
6069:
6062:
6050:
6045:
6039:
5809:
5806:
5805:
5744:
5741:
5740:
5704:
5701:
5700:
5639:
5636:
5635:
5610:
5607:
5606:
5545:
5542:
5541:
5525:
5522:
5521:
5490:
5487:
5486:
5452:
5449:
5448:
5393:
5390:
5389:
5388:. The notation
5358:
5355:
5354:
5320:
5317:
5316:
5313:
5211:
5208:
5207:
5191:
5188:
5187:
5141:
5138:
5137:
5109:
5106:
5105:
5080:
5077:
5076:
4979:
4976:
4975:
4956:
4953:
4952:
4932:
4929:
4928:
4780:
4777:
4776:
4679:
4676:
4675:
4655:
4652:
4651:
4635:
4632:
4631:
4615:
4612:
4611:
4606:is said to be "
4591:
4588:
4587:
4571:
4568:
4567:
4551:
4548:
4547:
4525:
4522:
4521:
4439:
4436:
4435:
4372:
4369:
4368:
4281:
4278:
4277:
4259:
4256:
4255:
4238:
4235:
4234:
4218:
4215:
4214:
4198:
4195:
4194:
4178:
4175:
4174:
4158:
4155:
4154:
4132:
4129:
4128:
4091:
4088:
4087:
4070:
4067:
4066:
4050:
4047:
4046:
4030:
4027:
4026:
4010:
4007:
4006:
3969:
3966:
3965:
3942:
3939:
3938:
3922:
3919:
3918:
3902:
3899:
3898:
3867:
3864:
3863:
3847:
3844:
3843:
3827:
3824:
3823:
3807:
3804:
3803:
3787:
3784:
3783:
3767:
3764:
3763:
3760:
3739:
3736:
3735:
3719:
3716:
3715:
3691:
3688:
3687:
3662:
3659:
3658:
3638:
3635:
3634:
3618:
3615:
3614:
3598:
3595:
3594:
3579:
3576:
3575:
3552:
3549:
3548:
3532:
3529:
3528:
3503:
3500:
3499:
3477:
3474:
3473:
3457:
3454:
3453:
3442:
3418:
3415:
3414:
3398:
3395:
3394:
3369:
3366:
3365:
3340:
3337:
3336:
3329:
3260:
3257:
3256:
3236:
3233:
3232:
3210:
3207:
3206:
3202:represents the
3178:
3175:
3174:
3152:
3149:
3148:
3143:represents the
3119:
3116:
3115:
3105:
3075:
3072:
3071:
3052:
3049:
3048:
3032:
3029:
3028:
2982:
2979:
2978:
2962:
2959:
2958:
2942:
2939:
2938:
2922:
2919:
2918:
2902:
2899:
2898:
2867:
2864:
2863:
2829:
2826:
2825:
2809:
2806:
2805:
2780:
2777:
2776:
2762:
2741:
2738:
2737:
2721:
2718:
2717:
2701:
2698:
2697:
2652:
2649:
2648:
2621:
2618:
2617:
2568:
2565:
2564:
2554:
2517:
2514:
2513:
2509:
2472:
2469:
2468:
2431:
2428:
2427:
2399:
2396:
2395:
2391:
2387:
2383:
2379:
2363:
2360:
2359:
2343:
2340:
2339:
2329:
2325:
2291:
2288:
2287:
2271:
2268:
2267:
2263:
2240:
2236:
2234:
2231:
2230:
2229:using the term
2204:
2200:
2183:
2180:
2179:
2163:
2160:
2159:
2133:
2129:
2115:
2112:
2111:
2110:. For example,
2107:
2103:
2074:
2071:
2070:
2044:
2040:
2029:
2026:
2025:
1993:
1990:
1989:
1970:
1967:
1966:
1962:
1958:
1920:
1917:
1916:
1912:
1908:
1901:
1879:
1852:
1825:
1822:
1821:
1803:
1800:
1799:
1783:
1780:
1779:
1762:
1758:
1749:
1745:
1740:
1737:
1736:
1718:
1715:
1714:
1698:
1695:
1694:
1665:
1661:
1652:
1648:
1634:
1631:
1630:
1603:
1602:
1587:
1586:
1577:
1573:
1564:
1560:
1539:
1538:
1532:
1531:
1529:
1526:
1525:
1499:
1496:
1495:
1477:
1473:
1464:
1460:
1455:
1452:
1451:
1415:
1411:
1402:
1398:
1375:
1372:
1371:
1325:
1323:
1320:
1319:
1286:
1282:
1273:
1269:
1252:
1249:
1248:
1225:
1221:
1212:
1208:
1188:
1185:
1184:
1134:
1132:
1129:
1128:
1100:
1097:
1096:
1056:
1053:
1052:
1032:
1028:
1019:
1015:
1013:
1010:
1009:
1001:
997:
973:
969:
960:
956:
936:
933:
932:
905:
901:
892:
888:
835:
833:
830:
829:
815:
810:
755:
752:
751:
732:
729:
728:
706:
705:
703:
700:
699:
673:
672:
670:
667:
666:
655:
604:
596:category theory
522:Turing complete
518:
413:
410:
409:
404:name collisions
330:
327:
326:
303:
300:
299:
283:
280:
279:
263:
260:
259:
258:to an argument
243:
240:
239:
207:
204:
203:
185:
182:
181:
161:
158:
157:
122:
119:
118:
96:
93:
92:
84:and performing
49:using variable
37:for expressing
20:Lambda calculus
17:
12:
11:
5:
16744:
16734:
16733:
16728:
16723:
16721:Formal methods
16718:
16713:
16708:
16691:
16690:
16688:
16687:
16682:
16677:
16672:
16667:
16662:
16660:Inferentialism
16657:
16655:Formal grammar
16652:
16647:
16642:
16636:
16634:
16630:
16629:
16626:
16625:
16623:
16622:
16617:
16612:
16607:
16602:
16597:
16592:
16587:
16582:
16577:
16575:Possible world
16572:
16567:
16562:
16557:
16552:
16547:
16542:
16537:
16532:
16527:
16521:
16519:
16515:
16514:
16512:
16511:
16506:
16501:
16496:
16491:
16486:
16481:
16476:
16471:
16466:
16461:
16459:Glue semantics
16456:
16451:
16446:
16441:
16436:
16431:
16425:
16423:
16422:Formal systems
16416:
16412:
16411:
16408:
16407:
16405:
16404:
16399:
16394:
16389:
16384:
16379:
16374:
16369:
16364:
16359:
16354:
16349:
16347:Polarity items
16344:
16339:
16334:
16329:
16324:
16319:
16314:
16309:
16304:
16299:
16294:
16289:
16284:
16279:
16274:
16269:
16264:
16259:
16254:
16249:
16244:
16239:
16234:
16232:Conservativity
16229:
16224:
16219:
16213:
16211:
16207:
16206:
16204:
16203:
16198:
16196:Quantification
16193:
16188:
16183:
16178:
16173:
16168:
16163:
16158:
16153:
16148:
16143:
16138:
16133:
16128:
16122:
16120:
16113:
16109:
16108:
16106:
16105:
16100:
16095:
16090:
16085:
16080:
16075:
16073:Presupposition
16070:
16065:
16060:
16055:
16050:
16045:
16040:
16034:
16032:
16028:
16027:
16020:
16019:
16012:
16005:
15997:
15988:
15987:
15973:
15970:
15969:
15967:
15966:
15961:
15956:
15951:
15946:
15945:
15944:
15934:
15929:
15924:
15915:
15910:
15905:
15900:
15898:Abstract logic
15894:
15892:
15888:
15887:
15885:
15884:
15879:
15877:Turing machine
15874:
15869:
15864:
15859:
15854:
15849:
15848:
15847:
15842:
15837:
15832:
15827:
15817:
15815:Computable set
15812:
15807:
15802:
15797:
15791:
15789:
15783:
15782:
15780:
15779:
15774:
15769:
15764:
15759:
15754:
15749:
15744:
15743:
15742:
15737:
15732:
15722:
15717:
15712:
15710:Satisfiability
15707:
15702:
15697:
15696:
15695:
15685:
15684:
15683:
15673:
15672:
15671:
15666:
15661:
15656:
15651:
15641:
15640:
15639:
15634:
15627:Interpretation
15623:
15621:
15615:
15614:
15612:
15611:
15606:
15601:
15596:
15591:
15581:
15576:
15575:
15574:
15573:
15572:
15562:
15557:
15547:
15542:
15537:
15532:
15527:
15522:
15516:
15514:
15508:
15507:
15504:
15503:
15501:
15500:
15492:
15491:
15490:
15489:
15484:
15483:
15482:
15477:
15472:
15452:
15451:
15450:
15448:minimal axioms
15445:
15434:
15433:
15432:
15421:
15420:
15419:
15414:
15409:
15404:
15399:
15394:
15381:
15379:
15360:
15359:
15357:
15356:
15355:
15354:
15342:
15337:
15336:
15335:
15330:
15325:
15320:
15310:
15305:
15300:
15295:
15294:
15293:
15288:
15278:
15277:
15276:
15271:
15266:
15261:
15251:
15246:
15245:
15244:
15239:
15234:
15224:
15223:
15222:
15217:
15212:
15207:
15202:
15197:
15187:
15182:
15177:
15172:
15171:
15170:
15165:
15160:
15155:
15145:
15140:
15138:Formation rule
15135:
15130:
15129:
15128:
15123:
15113:
15112:
15111:
15101:
15096:
15091:
15086:
15080:
15074:
15057:Formal systems
15053:
15052:
15049:
15048:
15046:
15045:
15040:
15035:
15030:
15025:
15020:
15015:
15010:
15005:
15000:
14999:
14998:
14993:
14982:
14980:
14976:
14975:
14973:
14972:
14971:
14970:
14960:
14955:
14954:
14953:
14946:Large cardinal
14943:
14938:
14933:
14928:
14923:
14909:
14908:
14907:
14902:
14897:
14882:
14880:
14870:
14869:
14867:
14866:
14865:
14864:
14859:
14854:
14844:
14839:
14834:
14829:
14824:
14819:
14814:
14809:
14804:
14799:
14794:
14789:
14783:
14781:
14774:
14773:
14771:
14770:
14769:
14768:
14763:
14758:
14753:
14748:
14743:
14735:
14734:
14733:
14728:
14718:
14713:
14711:Extensionality
14708:
14706:Ordinal number
14703:
14693:
14688:
14687:
14686:
14675:
14669:
14663:
14662:
14659:
14658:
14656:
14655:
14650:
14645:
14640:
14635:
14630:
14625:
14624:
14623:
14613:
14612:
14611:
14598:
14596:
14590:
14589:
14587:
14586:
14585:
14584:
14579:
14574:
14564:
14559:
14554:
14549:
14544:
14539:
14533:
14531:
14525:
14524:
14522:
14521:
14516:
14511:
14506:
14501:
14496:
14491:
14490:
14489:
14479:
14474:
14469:
14464:
14459:
14454:
14448:
14446:
14437:
14431:
14430:
14428:
14427:
14422:
14417:
14412:
14407:
14402:
14390:Cantor's
14388:
14383:
14378:
14368:
14366:
14353:
14352:
14350:
14349:
14344:
14339:
14334:
14329:
14324:
14319:
14314:
14309:
14304:
14299:
14294:
14289:
14288:
14287:
14276:
14274:
14270:
14269:
14262:
14261:
14254:
14247:
14239:
14230:
14229:
14227:
14226:
14221:
14215:
14213:
14209:
14208:
14206:
14205:
14200:
14194:
14192:
14188:
14187:
14185:
14184:
14179:
14177:Norman Shapiro
14174:
14169:
14164:
14159:
14154:
14149:
14144:
14142:Maurice L'Abbé
14139:
14134:
14129:
14124:
14119:
14114:
14112:William Easton
14109:
14104:
14099:
14094:
14089:
14084:
14078:
14076:
14072:
14071:
14069:
14068:
14063:
14058:
14057:
14056:
14051:
14046:
14035:
14033:
14029:
14028:
14021:
14020:
14013:
14006:
13998:
13992:
13991:
13983:
13971:
13962:
13955:
13950:
13944:
13919:
13911:
13903:
13895:
13887:
13869:
13861:
13852:
13851:External links
13849:
13847:
13846:
13817:
13776:
13732:
13708:
13672:
13657:
13621:
13610:(2): 201–218.
13587:
13580:
13540:
13497:
13483:
13450:
13443:
13437:. p. 56.
13416:
13407:
13381:(2): 393–413.
13358:
13344:
13303:
13277:
13269:Proc. TACS '94
13257:
13229:
13217:
13211:
13193:
13182:(4): 265–282.
13163:
13123:
13101:
13077:
13065:
13042:
13021:
12994:
12980:
12966:ter Meulen, A.
12956:
12919:Church, Alonzo
12910:
12891:(2): 345–363.
12881:Church, Alonzo
12869:
12850:(4): 170–171.
12836:Church, Alonzo
12827:
12785:
12766:(2): 346–366.
12756:Church, Alonzo
12747:
12730:
12727:on 2023-12-07.
12709:
12701:
12678:
12671:
12651:
12644:
12624:
12594:
12567:(4): 153–163.
12548:
12530:
12502:
12487:
12484:
12481:
12480:
12470:extended with
12459:
12434:
12422:
12402:
12386:
12373:
12361:
12348:
12345:
12342:
12322:
12319:
12316:
12313:
12310:
12307:
12291:
12279:
12276:
12273:
12270:
12246:
12243:
12240:
12237:
12234:
12231:
12216:
12196:
12192:
12189:
12186:
12183:
12180:
12177:
12174:
12171:
12168:
12165:
12149:
12132:
12114:
12105:
12103:
12102:
12081:
12068:
12065:
12062:
12056:
12053:
12050:
12047:
12044:
12038:
12035:
12032:
12029:
12026:
12020:
12017:
12011:
12008:
12005:
12002:
11999:
11996:
11993:
11990:
11987:
11984:
11981:
11978:
11975:
11972:
11969:
11966:
11949:
11948:
11946:
11943:
11942:
11941:
11917:
11909:
11897:
11885:
11873:
11860:
11859:
11855:
11854:
11848:
11835:
11803:
11802:
11800:
11796:
11795:
11782:
11762:(2): 211–247.
11746:
11737:
11731:
11718:
11709:
11691:
11680:
11668:(3): 169–172.
11643:
11616:
11605:
11587:
11565:
11558:
11547:
11526:
11523:
11521:
11520:
11510:
11504:
11493:
11487:
11477:
11471:
11466:
11463:Let expression
11460:
11454:
11448:
11436:
11430:
11425:
11422:Harrop formula
11419:
11414:
11405:
11396:
11382:
11376:
11370:
11361:
11355:
11345:
11336:
11325:
11324:
11323:
11307:
11304:
11303:
11302:
11278:
11268:
11267:
11264:Kappa calculus
11257:
11256:
11247:
11237:formal systems
11233:
11232:
11222:
11216:
11201:
11198:
11170:In the 1970s,
11143:can exist, by
11123:
11120:
11088:
11085:
10992:
10979:Main article:
10976:
10973:
10960:
10957:
10937:size explosion
10910:in the length
10870:The notion of
10867:
10864:
10828:
10803:, where
10794:
10713:
10710:
10709:
10708:
10704:
10701:
10698:
10691:
10690:
10653:
10650:
10646:
10639:
10638:
10635:
10632:
10620:
10600:
10596:
10593:
10590:
10587:
10584:
10581:
10578:
10575:
10571:
10568:
10565:
10562:
10559:
10556:
10553:
10550:
10545:
10542:
10539:
10536:
10532:
10520:
10517:
10513:
10501:Main article:
10498:
10495:
10485:of classes of
10420:
10397:Main article:
10394:
10391:
10243:
10242:
10192:
10159:
10059:Main article:
10056:
10053:
9970:form complete
9951:
9950:
9939:
9913:
9888:
9859:
9828:
9809:
9775:
9755:
9754:Standard terms
9752:
9742:
9741:
9736:
9731:
9722:
9697:
9688:
9679:
9654:
9645:
9636:
9634:−1)))) (3−1)))
9611:
9602:
9593:
9568:
9559:
9550:
9525:
9492:
9483:
9464:, where
9451:
9450:
9435:
9397:
9362:
9320:
9291:
9290:
9237:self-reference
9213:
9212:
9211:
9210:
9209:
9208:
9148:
9147:
9146:
9145:
9144:
9072:
9071:
9055:
9054:
9053:
9052:
9051:
8970:
8969:
8888:Main article:
8885:
8882:
8838:
8837:
8807:
8806:
8764:
8761:
8744:
8741:
8740:
8739:
8737:Φ (PAIR 0 0)).
8729:PRED := λ
8722:
8721:
8711:.PAIR (SECOND
8630:
8629:
8611:NULL := λ
8608:
8599:
8586:
8573:
8550:PAIR := λ
8506:
8503:
8453:
8452:
8415:PRED := λ
8367:
8366:
8341:
8340:
8292:AND TRUE FALSE
8288:
8287:
8286:
8285:
8280:
8279:) FALSE TRUE →
8264:
8259:
8258:) TRUE FALSE →
8235:AND TRUE FALSE
8228:
8227:
8201:
8188:
8166:
8140:
8139:
8123:
8110:TRUE := λ
8094:
8091:
8054:
8053:
7954:
7953:
7900:PRED := λ
7871:
7870:
7823:
7822:
7804:MULT := λ
7799:Alternatively
7797:
7796:
7771:MULT := λ
7764:
7763:
7746:PLUS := λ
7721:
7720:
7711:
7710:
7698:
7697:
7662:PLUS := λ
7615:
7614:
7586:SUCC := λ
7557:
7556:
7410:
7409:
7385:
7365:
7350:
7328:
7327:
7299:
7275:
7256:
7227:
7224:
7181:
7178:
7155:rewriting rule
7147:Main article:
7144:
7141:
7099:if and only if
7095:extensionality
7083:
7080:
7026:
7023:
6981:
6980:
6939:
6921:
6918:
6912:
6905:
6899:
6893:
6876:
6842:
6839:
6698:
6695:
6609:
6608:
6602:
6596:
6582:
6579:
6563:
6562:
6545:
6526:
6525:is a variable.
6499:free variables
6419:
6416:
6415:
6414:
6387:
6352:
6335:
6311:
6289:
6286:
6176:
6150:
6149:
6128:
6103:
6078:
6077:
6074:
6071:
6067:
6060:
6049:
6046:
6041:Main article:
6038:
6035:
6014:
6011:
6008:
6005:
6002:
5999:
5996:
5993:
5990:
5987:
5984:
5981:
5978:
5975:
5972:
5969:
5966:
5963:
5960:
5957:
5954:
5951:
5948:
5945:
5942:
5939:
5936:
5933:
5930:
5927:
5924:
5921:
5918:
5915:
5912:
5909:
5906:
5903:
5900:
5897:
5894:
5891:
5888:
5885:
5882:
5879:
5876:
5873:
5870:
5867:
5864:
5861:
5858:
5855:
5852:
5849:
5846:
5843:
5840:
5837:
5834:
5831:
5828:
5825:
5822:
5819:
5816:
5813:
5793:
5790:
5787:
5784:
5781:
5778:
5775:
5772:
5769:
5766:
5763:
5760:
5757:
5754:
5751:
5748:
5717:
5714:
5711:
5708:
5688:
5685:
5682:
5679:
5676:
5673:
5670:
5667:
5664:
5661:
5658:
5655:
5652:
5649:
5646:
5643:
5623:
5620:
5617:
5614:
5594:
5591:
5588:
5585:
5582:
5579:
5576:
5573:
5570:
5567:
5564:
5561:
5558:
5555:
5552:
5549:
5529:
5509:
5506:
5503:
5500:
5497:
5494:
5474:
5471:
5468:
5465:
5462:
5459:
5456:
5436:
5433:
5430:
5427:
5424:
5421:
5418:
5415:
5412:
5409:
5406:
5403:
5400:
5397:
5377:
5374:
5371:
5368:
5365:
5362:
5342:
5339:
5336:
5333:
5330:
5327:
5324:
5312:
5309:
5296:
5293:
5290:
5287:
5284:
5281:
5278:
5275:
5272:
5269:
5266:
5263:
5260:
5257:
5254:
5251:
5248:
5245:
5242:
5239:
5236:
5233:
5230:
5227:
5224:
5221:
5218:
5215:
5195:
5175:
5172:
5169:
5166:
5163:
5160:
5157:
5154:
5151:
5148:
5145:
5122:
5119:
5116:
5113:
5093:
5090:
5087:
5084:
5064:
5061:
5058:
5055:
5052:
5049:
5046:
5043:
5040:
5037:
5034:
5031:
5028:
5025:
5022:
5019:
5016:
5013:
5010:
5007:
5004:
5001:
4998:
4995:
4992:
4989:
4986:
4983:
4960:
4949:free variables
4947:is not in the
4936:
4913:
4910:
4907:
4904:
4901:
4898:
4895:
4892:
4889:
4886:
4883:
4880:
4877:
4874:
4871:
4868:
4865:
4862:
4859:
4856:
4853:
4850:
4847:
4844:
4841:
4838:
4835:
4832:
4829:
4826:
4823:
4820:
4817:
4814:
4811:
4808:
4805:
4802:
4799:
4796:
4793:
4790:
4787:
4784:
4764:
4761:
4758:
4755:
4752:
4749:
4746:
4743:
4740:
4737:
4734:
4731:
4728:
4725:
4722:
4719:
4716:
4713:
4710:
4707:
4704:
4701:
4698:
4695:
4692:
4689:
4686:
4683:
4672:
4671:
4659:
4639:
4619:
4595:
4575:
4555:
4535:
4532:
4529:
4509:
4506:
4503:
4500:
4497:
4494:
4491:
4488:
4485:
4482:
4479:
4476:
4473:
4470:
4467:
4464:
4461:
4458:
4455:
4452:
4449:
4446:
4443:
4433:
4421:
4418:
4415:
4412:
4409:
4406:
4403:
4400:
4397:
4394:
4391:
4388:
4385:
4382:
4379:
4376:
4366:
4354:
4351:
4348:
4345:
4342:
4339:
4336:
4333:
4330:
4327:
4324:
4321:
4318:
4315:
4312:
4309:
4306:
4303:
4300:
4297:
4294:
4291:
4288:
4285:
4266:
4263:
4253:
4242:
4222:
4213:(which is not
4202:
4182:
4162:
4142:
4139:
4136:
4116:
4113:
4110:
4107:
4104:
4101:
4098:
4095:
4085:
4074:
4054:
4034:
4014:
3994:
3991:
3988:
3985:
3982:
3979:
3976:
3973:
3946:
3926:
3906:
3886:
3883:
3880:
3877:
3874:
3871:
3851:
3831:
3811:
3791:
3771:
3759:
3756:
3743:
3723:
3704:
3701:
3698:
3695:
3675:
3672:
3669:
3666:
3655:
3654:
3642:
3622:
3602:
3583:
3568:
3556:
3536:
3516:
3513:
3510:
3507:
3492:
3481:
3461:
3446:free variables
3441:
3440:Free variables
3438:
3422:
3402:
3382:
3379:
3376:
3373:
3353:
3350:
3347:
3344:
3328:
3325:
3309:
3306:
3303:
3300:
3297:
3294:
3291:
3288:
3285:
3282:
3279:
3276:
3273:
3270:
3267:
3264:
3240:
3220:
3217:
3214:
3191:
3188:
3185:
3182:
3162:
3159:
3156:
3132:
3129:
3126:
3123:
3104:
3101:
3088:
3085:
3082:
3079:
3056:
3036:
3016:
3013:
3010:
3007:
3004:
3001:
2998:
2995:
2992:
2989:
2986:
2966:
2946:
2926:
2906:
2886:
2883:
2880:
2877:
2874:
2871:
2851:
2848:
2845:
2842:
2839:
2836:
2833:
2813:
2793:
2790:
2787:
2784:
2758:
2757:
2745:
2725:
2705:
2686:
2683:
2680:
2677:
2674:
2671:
2668:
2665:
2662:
2659:
2656:
2646:
2634:
2631:
2628:
2625:
2605:
2602:
2599:
2596:
2593:
2590:
2587:
2584:
2581:
2578:
2575:
2572:
2542:
2539:
2536:
2533:
2530:
2527:
2524:
2521:
2497:
2494:
2491:
2488:
2485:
2482:
2479:
2476:
2456:
2453:
2450:
2447:
2444:
2441:
2438:
2435:
2412:
2409:
2406:
2403:
2367:
2347:
2310:
2307:
2304:
2301:
2298:
2295:
2275:
2251:
2248:
2243:
2239:
2218:
2215:
2212:
2207:
2203:
2199:
2196:
2193:
2190:
2187:
2167:
2147:
2144:
2141:
2136:
2132:
2128:
2125:
2122:
2119:
2087:
2084:
2081:
2078:
2052:
2047:
2043:
2039:
2036:
2033:
2017:
2016:
2000:
1997:
1977:
1974:
1955:
1939:
1936:
1933:
1930:
1927:
1924:
1905:
1878:
1875:
1851:
1848:
1844:
1843:
1832:
1829:
1819:
1807:
1787:
1765:
1761:
1757:
1752:
1748:
1744:
1734:
1722:
1702:
1682:
1679:
1676:
1673:
1668:
1664:
1660:
1655:
1651:
1647:
1644:
1641:
1638:
1628:
1617:
1614:
1611:
1606:
1601:
1598:
1595:
1590:
1585:
1580:
1576:
1572:
1567:
1563:
1559:
1556:
1553:
1550:
1547:
1542:
1535:
1519:
1518:
1506:
1503:
1493:
1480:
1476:
1472:
1467:
1463:
1459:
1449:
1438:
1435:
1432:
1429:
1426:
1423:
1418:
1414:
1410:
1405:
1401:
1397:
1394:
1391:
1388:
1385:
1382:
1379:
1355:
1352:
1349:
1346:
1343:
1340:
1337:
1334:
1331:
1328:
1306:
1305:
1294:
1289:
1285:
1281:
1276:
1272:
1268:
1265:
1262:
1259:
1256:
1242:
1241:
1228:
1224:
1220:
1215:
1211:
1207:
1204:
1201:
1198:
1195:
1192:
1164:
1161:
1158:
1155:
1152:
1149:
1146:
1143:
1140:
1137:
1122:
1121:
1110:
1107:
1104:
1090:
1089:
1078:
1075:
1072:
1069:
1066:
1063:
1060:
1035:
1031:
1027:
1022:
1018:
990:
989:
976:
972:
968:
963:
959:
955:
952:
949:
946:
943:
940:
926:anonymous form
922:
921:
908:
904:
900:
895:
891:
887:
884:
881:
878:
875:
872:
869:
865:
862:
859:
856:
853:
850:
847:
844:
841:
838:
814:
811:
809:
806:
759:
739:
736:
713:
710:
680:
677:
654:
649:Origin of the
647:
626:developed the
620:Stephen Kleene
603:
600:
530:Turing machine
517:
514:
487:
486:
471:
468:
465:
462:
459:
456:
453:
450:
447:
444:
441:
435:
432:
429:
426:
423:
420:
417:
407:
400:: α-conversion
388:
385:
382:
379:
376:
373:
370:
367:
364:
361:
358:
355:
352:
349:
346:
343:
340:
337:
334:
320:
319:
311:{\textstyle N}
307:
291:{\textstyle M}
287:
271:{\textstyle N}
267:
251:{\textstyle M}
247:
223:
220:
214:
211:
201:
193:{\textstyle M}
189:
165:
141:
138:
135:
132:
129:
126:
116:
104:{\textstyle x}
100:
63:Turing machine
15:
9:
6:
4:
3:
2:
16743:
16732:
16729:
16727:
16724:
16722:
16719:
16717:
16714:
16712:
16709:
16707:
16704:
16703:
16701:
16686:
16683:
16681:
16678:
16676:
16673:
16671:
16668:
16666:
16663:
16661:
16658:
16656:
16653:
16651:
16648:
16646:
16643:
16641:
16638:
16637:
16635:
16631:
16621:
16618:
16616:
16613:
16611:
16608:
16606:
16603:
16601:
16598:
16596:
16593:
16591:
16588:
16586:
16583:
16581:
16578:
16576:
16573:
16571:
16568:
16566:
16563:
16561:
16558:
16556:
16553:
16551:
16548:
16546:
16543:
16541:
16538:
16536:
16533:
16531:
16528:
16526:
16523:
16522:
16520:
16516:
16510:
16507:
16505:
16502:
16500:
16497:
16495:
16492:
16490:
16487:
16485:
16482:
16480:
16477:
16475:
16472:
16470:
16467:
16465:
16462:
16460:
16457:
16455:
16452:
16450:
16447:
16445:
16442:
16440:
16437:
16435:
16432:
16430:
16427:
16426:
16424:
16420:
16417:
16413:
16403:
16400:
16398:
16395:
16393:
16390:
16388:
16385:
16383:
16380:
16378:
16375:
16373:
16370:
16368:
16365:
16363:
16360:
16358:
16355:
16353:
16350:
16348:
16345:
16343:
16342:Performatives
16340:
16338:
16335:
16333:
16330:
16328:
16325:
16323:
16322:Logophoricity
16320:
16318:
16315:
16313:
16310:
16308:
16305:
16303:
16300:
16298:
16295:
16293:
16290:
16288:
16285:
16283:
16280:
16278:
16275:
16273:
16270:
16268:
16265:
16263:
16260:
16258:
16255:
16253:
16250:
16248:
16245:
16243:
16240:
16238:
16235:
16233:
16230:
16228:
16225:
16223:
16220:
16218:
16215:
16214:
16212:
16208:
16202:
16199:
16197:
16194:
16192:
16189:
16187:
16184:
16182:
16179:
16177:
16174:
16172:
16169:
16167:
16164:
16162:
16159:
16157:
16156:Evidentiality
16154:
16152:
16149:
16147:
16144:
16142:
16139:
16137:
16134:
16132:
16129:
16127:
16124:
16123:
16121:
16117:
16114:
16110:
16104:
16101:
16099:
16096:
16094:
16091:
16089:
16086:
16084:
16081:
16079:
16076:
16074:
16071:
16069:
16066:
16064:
16061:
16059:
16056:
16054:
16051:
16049:
16046:
16044:
16041:
16039:
16036:
16035:
16033:
16029:
16025:
16018:
16013:
16011:
16006:
16004:
15999:
15998:
15995:
15985:
15984:
15979:
15971:
15965:
15962:
15960:
15957:
15955:
15952:
15950:
15947:
15943:
15940:
15939:
15938:
15935:
15933:
15930:
15928:
15925:
15923:
15919:
15916:
15914:
15911:
15909:
15906:
15904:
15901:
15899:
15896:
15895:
15893:
15889:
15883:
15880:
15878:
15875:
15873:
15872:Recursive set
15870:
15868:
15865:
15863:
15860:
15858:
15855:
15853:
15850:
15846:
15843:
15841:
15838:
15836:
15833:
15831:
15828:
15826:
15823:
15822:
15821:
15818:
15816:
15813:
15811:
15808:
15806:
15803:
15801:
15798:
15796:
15793:
15792:
15790:
15788:
15784:
15778:
15775:
15773:
15770:
15768:
15765:
15763:
15760:
15758:
15755:
15753:
15750:
15748:
15745:
15741:
15738:
15736:
15733:
15731:
15728:
15727:
15726:
15723:
15721:
15718:
15716:
15713:
15711:
15708:
15706:
15703:
15701:
15698:
15694:
15691:
15690:
15689:
15686:
15682:
15681:of arithmetic
15679:
15678:
15677:
15674:
15670:
15667:
15665:
15662:
15660:
15657:
15655:
15652:
15650:
15647:
15646:
15645:
15642:
15638:
15635:
15633:
15630:
15629:
15628:
15625:
15624:
15622:
15620:
15616:
15610:
15607:
15605:
15602:
15600:
15597:
15595:
15592:
15589:
15588:from ZFC
15585:
15582:
15580:
15577:
15571:
15568:
15567:
15566:
15563:
15561:
15558:
15556:
15553:
15552:
15551:
15548:
15546:
15543:
15541:
15538:
15536:
15533:
15531:
15528:
15526:
15523:
15521:
15518:
15517:
15515:
15513:
15509:
15499:
15498:
15494:
15493:
15488:
15487:non-Euclidean
15485:
15481:
15478:
15476:
15473:
15471:
15470:
15466:
15465:
15463:
15460:
15459:
15457:
15453:
15449:
15446:
15444:
15441:
15440:
15439:
15435:
15431:
15428:
15427:
15426:
15422:
15418:
15415:
15413:
15410:
15408:
15405:
15403:
15400:
15398:
15395:
15393:
15390:
15389:
15387:
15383:
15382:
15380:
15375:
15369:
15364:Example
15361:
15353:
15348:
15347:
15346:
15343:
15341:
15338:
15334:
15331:
15329:
15326:
15324:
15321:
15319:
15316:
15315:
15314:
15311:
15309:
15306:
15304:
15301:
15299:
15296:
15292:
15289:
15287:
15284:
15283:
15282:
15279:
15275:
15272:
15270:
15267:
15265:
15262:
15260:
15257:
15256:
15255:
15252:
15250:
15247:
15243:
15240:
15238:
15235:
15233:
15230:
15229:
15228:
15225:
15221:
15218:
15216:
15213:
15211:
15208:
15206:
15203:
15201:
15198:
15196:
15193:
15192:
15191:
15188:
15186:
15183:
15181:
15178:
15176:
15173:
15169:
15166:
15164:
15161:
15159:
15156:
15154:
15151:
15150:
15149:
15146:
15144:
15141:
15139:
15136:
15134:
15131:
15127:
15124:
15122:
15121:by definition
15119:
15118:
15117:
15114:
15110:
15107:
15106:
15105:
15102:
15100:
15097:
15095:
15092:
15090:
15087:
15085:
15082:
15081:
15078:
15075:
15073:
15069:
15064:
15058:
15054:
15044:
15041:
15039:
15036:
15034:
15031:
15029:
15026:
15024:
15021:
15019:
15016:
15014:
15011:
15009:
15008:Kripke–Platek
15006:
15004:
15001:
14997:
14994:
14992:
14989:
14988:
14987:
14984:
14983:
14981:
14977:
14969:
14966:
14965:
14964:
14961:
14959:
14956:
14952:
14949:
14948:
14947:
14944:
14942:
14939:
14937:
14934:
14932:
14929:
14927:
14924:
14921:
14917:
14913:
14910:
14906:
14903:
14901:
14898:
14896:
14893:
14892:
14891:
14887:
14884:
14883:
14881:
14879:
14875:
14871:
14863:
14860:
14858:
14855:
14853:
14852:constructible
14850:
14849:
14848:
14845:
14843:
14840:
14838:
14835:
14833:
14830:
14828:
14825:
14823:
14820:
14818:
14815:
14813:
14810:
14808:
14805:
14803:
14800:
14798:
14795:
14793:
14790:
14788:
14785:
14784:
14782:
14780:
14775:
14767:
14764:
14762:
14759:
14757:
14754:
14752:
14749:
14747:
14744:
14742:
14739:
14738:
14736:
14732:
14729:
14727:
14724:
14723:
14722:
14719:
14717:
14714:
14712:
14709:
14707:
14704:
14702:
14698:
14694:
14692:
14689:
14685:
14682:
14681:
14680:
14677:
14676:
14673:
14670:
14668:
14664:
14654:
14651:
14649:
14646:
14644:
14641:
14639:
14636:
14634:
14631:
14629:
14626:
14622:
14619:
14618:
14617:
14614:
14610:
14605:
14604:
14603:
14600:
14599:
14597:
14595:
14591:
14583:
14580:
14578:
14575:
14573:
14570:
14569:
14568:
14565:
14563:
14560:
14558:
14555:
14553:
14550:
14548:
14545:
14543:
14540:
14538:
14535:
14534:
14532:
14530:
14529:Propositional
14526:
14520:
14517:
14515:
14512:
14510:
14507:
14505:
14502:
14500:
14497:
14495:
14492:
14488:
14485:
14484:
14483:
14480:
14478:
14475:
14473:
14470:
14468:
14465:
14463:
14460:
14458:
14457:Logical truth
14455:
14453:
14450:
14449:
14447:
14445:
14441:
14438:
14436:
14432:
14426:
14423:
14421:
14418:
14416:
14413:
14411:
14408:
14406:
14403:
14401:
14397:
14393:
14389:
14387:
14384:
14382:
14379:
14377:
14373:
14370:
14369:
14367:
14365:
14359:
14354:
14348:
14345:
14343:
14340:
14338:
14335:
14333:
14330:
14328:
14325:
14323:
14320:
14318:
14315:
14313:
14310:
14308:
14305:
14303:
14300:
14298:
14295:
14293:
14290:
14286:
14283:
14282:
14281:
14278:
14277:
14275:
14271:
14267:
14260:
14255:
14253:
14248:
14246:
14241:
14240:
14237:
14225:
14222:
14220:
14217:
14216:
14214:
14210:
14204:
14201:
14199:
14196:
14195:
14193:
14189:
14183:
14180:
14178:
14175:
14173:
14170:
14168:
14165:
14163:
14160:
14158:
14155:
14153:
14150:
14148:
14145:
14143:
14140:
14138:
14135:
14133:
14130:
14128:
14125:
14123:
14120:
14118:
14117:Alfred Foster
14115:
14113:
14110:
14108:
14105:
14103:
14102:William Boone
14100:
14098:
14095:
14093:
14092:Peter Andrews
14090:
14088:
14085:
14083:
14080:
14079:
14077:
14073:
14067:
14064:
14062:
14059:
14055:
14052:
14050:
14047:
14045:
14042:
14041:
14040:
14037:
14036:
14034:
14032:Notable ideas
14030:
14026:
14025:Alonzo Church
14019:
14014:
14012:
14007:
14005:
14000:
13999:
13996:
13990:
13989:
13984:
13982:
13981:
13976:
13972:
13970:
13969:C++ Templates
13966:
13963:
13960:
13956:
13954:
13951:
13948:
13945:
13943:
13939:
13936:
13932:
13931:
13927:
13924:
13920:
13918:
13917:
13913:Bret Victor,
13912:
13910:
13909:
13904:
13902:
13901:
13896:
13894:
13893:
13888:
13884:
13880:
13879:
13874:
13870:
13868:
13867:
13862:
13859:
13855:
13854:
13835:
13831:
13827:
13821:
13806:
13802:
13798:
13794:
13787:
13780:
13772:
13768:
13763:
13758:
13755:(2): 89–101.
13754:
13750:
13746:
13742:
13741:Landin, P. J.
13736:
13727:
13722:
13715:
13713:
13703:
13698:
13694:
13690:
13686:
13679:
13677:
13668:
13664:
13660:
13658:9781450328869
13654:
13650:
13646:
13641:
13636:
13632:
13625:
13617:
13613:
13609:
13605:
13598:
13591:
13583:
13581:9783540543961
13577:
13573:
13569:
13564:
13559:
13555:
13551:
13544:
13528:
13523:
13519:
13515:
13508:
13501:
13486:
13480:
13476:
13472:
13468:
13461:
13454:
13446:
13444:0-262-16209-1
13440:
13436:
13432:
13431:
13426:
13420:
13411:
13396:
13392:
13388:
13384:
13380:
13376:
13369:
13362:
13347:
13341:
13337:
13333:
13329:
13325:
13321:
13314:
13307:
13288:
13281:
13274:
13270:
13264:
13262:
13253:on 2009-02-05
13249:
13242:
13241:
13233:
13227:
13221:
13214:
13208:
13204:
13197:
13189:
13185:
13181:
13177:
13173:
13167:
13160:
13156:
13151:
13146:
13139:
13138:
13130:
13128:
13120:
13115:
13111:
13105:
13090:
13084:
13082:
13074:
13068:
13066:0-444-87508-5
13062:
13058:
13057:
13052:
13046:
13039:
13035:
13031:
13028:Dana Scott, "
13025:
13009:
13005:
12998:
12983:
12981:9789027722454
12977:
12973:
12972:
12967:
12960:
12952:
12948:
12944:
12940:
12936:
12932:
12928:
12924:
12920:
12914:
12906:
12902:
12898:
12894:
12890:
12886:
12882:
12876:
12874:
12865:
12861:
12857:
12853:
12849:
12845:
12841:
12837:
12831:
12823:
12819:
12815:
12811:
12807:
12803:
12799:
12798:Rosser, J. B.
12795:
12789:
12781:
12777:
12773:
12769:
12765:
12761:
12757:
12751:
12744:. p. 53.
12743:
12740:
12734:
12726:
12722:
12721:
12713:
12704:
12698:
12694:
12693:
12688:
12682:
12674:
12668:
12664:
12663:
12655:
12647:
12645:9789067653879
12641:
12637:
12636:
12628:
12612:
12608:
12607:"Type Theory"
12604:
12598:
12590:
12586:
12582:
12578:
12574:
12570:
12566:
12562:
12558:
12552:
12546:
12544:
12539:
12534:
12524:
12523:
12518:
12512:
12510:
12508:
12503:
12501:
12500:
12498:
12494:
12477:
12469:
12463:
12456:
12450:
12445:
12438:
12420:
12400:
12390:
12383:
12377:
12371:
12365:
12346:
12340:
12317:
12314:
12311:
12308:
12295:
12277:
12274:
12271:
12268:
12260:
12241:
12238:
12235:
12232:
12220:
12214:
12212:
12194:
12190:
12187:
12184:
12181:
12178:
12175:
12172:
12169:
12166:
12163:
12153:
12146:
12121:
12119:
12109:
12100:
12097:
12096:
12092:
12090:
12088:
12086:
12060:
12054:
12042:
12036:
12033:
12030:
12027:
12015:
12009:
12006:
12003:
12000:
11994:
11991:
11988:
11982:
11979:
11976:
11973:
11970:
11967:
11954:
11950:
11939:
11935:
11934:Church–Rosser
11931:
11927:
11923:
11922:
11918:
11915:
11914:
11910:
11907:
11903:
11902:
11898:
11895:
11891:
11890:
11886:
11883:
11879:
11878:
11874:
11871:
11867:
11866:
11862:
11861:
11857:
11856:
11851:
11849:0-262-16209-1
11845:
11842:, MIT Press,
11841:
11836:
11833:
11829:
11825:
11821:
11817:
11816:0-444-52077-5
11813:
11809:
11805:
11804:
11801:
11798:
11797:
11794:
11790:
11787:
11783:
11777:
11773:
11769:
11765:
11761:
11757:
11756:
11755:Studia Logica
11751:
11747:
11744:
11743:
11738:
11734:
11728:
11724:
11719:
11716:
11715:
11711:Larson, Jim,
11710:
11707:
11703:
11699:
11695:
11694:Landin, Peter
11692:
11689:
11685:
11681:
11676:
11671:
11667:
11663:
11656:
11654:
11648:
11644:
11641:
11637:
11624:
11623:
11617:
11614:
11610:
11606:
11603:
11599:
11595:
11592:
11588:
11586:
11585:0-7204-2285-X
11582:
11578:
11577:North-Holland
11574:
11570:
11566:
11563:
11559:
11556:
11555:
11551:
11548:
11545:
11544:0-262-51087-1
11541:
11537:
11536:The MIT Press
11533:
11529:
11528:
11518:
11514:
11511:
11508:
11505:
11503:
11499:
11498:
11494:
11491:
11488:
11485:
11481:
11478:
11475:
11472:
11470:
11467:
11464:
11461:
11458:
11455:
11452:
11449:
11447:
11444:
11440:
11437:
11434:
11431:
11429:
11426:
11423:
11420:
11418:
11415:
11413:
11409:
11406:
11404:
11400:
11397:
11394:
11390:
11386:
11385:Domain theory
11383:
11380:
11377:
11374:
11371:
11369:
11365:
11362:
11359:
11356:
11353:
11349:
11346:
11344:
11340:
11337:
11334:
11330:
11327:
11326:
11321:
11315:
11310:
11300:
11299:
11294:
11293:
11288:
11287:
11282:
11279:
11276:
11273:
11272:
11271:
11265:
11262:
11261:
11260:
11255:
11251:
11248:
11245:
11242:
11241:
11240:
11238:
11230:
11226:
11223:
11220:
11217:
11214:
11211:
11210:
11209:
11207:
11197:
11195:
11190:
11188:
11184:
11181:
11177:
11173:
11168:
11166:
11165:singleton set
11162:
11158:
11154:
11150:
11146:
11142:
11138:
11134:
11130:
11119:
11117:
11113:
11109:
11105:
11102:
11098:
11094:
11093:Church–Rosser
11084:
11082:
11078:
11074:
11070:
11066:
11062:
11058:
11054:
11050:
11046:
11042:
11038:
11035:For example,
11033:
10990:
10988:
10982:
10972:
10970:
10966:
10956:
10954:
10950:
10945:
10940:
10938:
10934:
10929:
10927:
10923:
10918:
10913:
10909:
10907:
10903:
10897:
10891:
10885:
10879:
10873:
10863:
10860:
10855:
10850:
10845:
10841:
10836:
10834:
10826:
10822:
10818:
10813:
10807:
10801:
10791:
10787:
10783:
10779:
10775:
10771:
10767:
10763:
10759:
10755:
10751:
10747:
10743:
10739:
10735:
10731:
10727:
10712:Computability
10705:
10702:
10699:
10696:
10695:
10694:
10687:
10683:
10679:
10672:
10668:
10664:
10660:
10654:
10651:
10647:
10645:Call by value
10644:
10643:
10642:
10636:
10633:
10618:
10588:
10585:
10579:
10576:
10573:
10566:
10563:
10557:
10554:
10551:
10543:
10540:
10537:
10534:
10521:
10518:
10514:
10511:
10510:
10509:
10504:
10494:
10492:
10488:
10484:
10480:
10476:
10472:
10467:
10465:
10461:
10457:
10453:
10449:
10445:
10440:
10438:
10434:
10418:
10410:
10406:
10400:
10390:
10388:
10384:
10380:
10376:
10372:
10368:
10363:
10358:
10354:
10350:
10346:
10342:
10338:
10333:
10331:
10327:
10322:
10314:
10309:
10303:
10299:
10295:
10289:
10284:
10278:
10274:
10270:
10266:
10262:
10258:
10253:
10248:
10240:
10235:
10230:
10226:
10221:
10216:
10213:
10209:
10206:
10201:
10196:
10193:
10190:
10185:
10180:
10177:
10173:
10168:
10163:
10160:
10158:
10153:
10147:
10142:
10139:
10138:
10137:
10135:
10130:
10125:
10121:
10116:
10111:
10106:
10101:
10097:
10092:
10086:
10081:
10076:
10072:
10068:
10062:
10052:
10049:
10043:
10038:
10024:
10020:
10014:
10010:
10005:
10000:
9994:
9988:
9982:
9977:
9973:
9968:
9962:
9956:
9948:
9944:
9940:
9937:
9934:
9930:
9926:
9922:
9918:
9914:
9911:
9908:
9905:
9901:
9897:
9893:
9889:
9886:
9883:
9880:
9876:
9872:
9868:
9864:
9860:
9856:
9853:
9849:
9845:
9841:
9837:
9833:
9829:
9826:
9822:
9818:
9814:
9810:
9806:
9803:
9799:
9796:
9792:
9788:
9784:
9780:
9776:
9773:
9769:
9765:
9761:
9760:
9759:
9751:
9748:
9737:
9732:
9729:G) (0−1))))))
9728:
9723:
9719:
9715:
9711:
9707:
9703:
9698:
9694:
9689:
9685:
9680:
9676:
9672:
9668:
9664:
9660:
9655:
9651:
9646:
9642:
9637:
9633:
9629:
9625:
9621:
9617:
9612:
9608:
9605:4 × (3 × (G (
9603:
9599:
9594:
9591:−1)))) (4−1))
9590:
9586:
9582:
9578:
9574:
9569:
9565:
9560:
9556:
9551:
9547:
9543:
9539:
9535:
9531:
9526:
9522:
9518:
9514:
9510:
9506:
9502:
9498:
9493:
9489:
9484:
9480:
9475:
9474:
9473:
9471:
9467:
9462:
9458:
9447:
9444:
9440:
9436:
9432:
9429:
9425:
9421:
9417:
9414:
9410:
9406:
9402:
9398:
9394:
9391:
9387:
9383:
9379:
9376:
9372:
9368:
9363:
9360:
9356:
9353:
9349:
9345:
9341:
9338:
9334:
9330:
9326:
9321:
9318:
9315:
9311:
9310:
9309:
9306:
9300:
9297:
9287:
9284:
9280:
9276:
9272:
9269:
9265:
9261:
9257:
9253:
9249:
9248:
9247:
9240:
9238:
9222:
9205:
9201:
9197:
9193:
9187:
9186:
9185:
9184:
9181:
9177:
9173:
9170:
9166:
9162:
9158:
9149:
9140:
9136:
9130:
9127:
9123:
9119:
9116:
9111:
9110:
9109:
9108:
9105:
9101:
9097:
9093:
9089:
9085:
9080:
9079:
9078:
9075:
9068:
9065:
9061:
9056:
9047:
9041:
9038:
9034:
9030:
9027:
9024:
9019:
9018:
9017:
9016:
9013:
9009:
9006:
9002:
8998:
8994:
8990:
8985:
8984:
8983:
8980:
8975:
8965:
8961:
8957:
8953:
8948:
8947:
8946:
8942:
8936:
8933:Consider the
8931:
8929:
8924:
8920:
8917:
8913:
8907:
8902:
8897:
8891:
8881:
8871:
8866:
8861:
8857:
8852:
8842:
8836:
8830:
8825:
8820:
8819:
8818:
8812:
8805:
8799:
8794:
8789:
8788:
8787:
8785:
8781:
8776:
8770:
8760:
8758:
8754:
8750:
8736:
8732:
8727:
8726:
8725:
8718:
8714:
8710:
8705:
8704:
8703:
8699:
8695:
8687:
8683:
8676:
8672:
8668:
8664:
8660:
8656:
8652:
8626:
8622:
8618:
8614:
8609:
8605:
8602:NIL := λ
8600:
8596:
8592:
8587:
8583:
8579:
8574:
8571:
8568:
8565:
8561:
8557:
8553:
8548:
8547:
8546:
8535:
8529:
8520:
8502:
8499:
8493:
8486:
8482:
8479:
8475:
8471:
8467:
8463:
8459:
8449:
8445:
8442:
8438:
8434:
8430:
8426:
8422:
8418:
8413:
8412:
8411:
8400:
8397:
8394:
8387:
8384:
8377:
8373:
8362:
8359:
8356:.ISZERO (SUB
8355:
8351:
8348:LEQ := λ
8346:
8345:
8344:
8337:
8333:
8329:
8324:
8323:
8322:
8304:
8299:
8278:
8274:
8270:
8265:
8257:
8254:
8251:
8247:
8243:
8238:
8237:
8233:
8232:
8231:
8225:
8222:
8219:
8215:
8211:
8207:
8202:
8198:
8194:
8191:NOT := λ
8189:
8186:
8183:
8180:
8176:
8172:
8167:
8164:
8161:
8158:
8154:
8150:
8147:AND := λ
8145:
8144:
8143:
8137:
8133:
8129:
8124:
8121:
8117:
8113:
8108:
8107:
8106:
8090:
8083:
8079:
8073:
8069:
8063:
8060:
8050:
8046:
8042:
8038:
8035:SUB := λ
8033:
8032:
8031:
8029:
8025:
8015:
8008:
8004:
8000:
7996:
7992:
7988:
7980:
7977:
7973:
7969:
7965:
7959:
7950:
7946:
7942:
7938:
7934:
7931:
7927:
7923:
7919:
7915:
7911:
7907:
7903:
7898:
7897:
7896:
7889:
7882:
7878:
7868:
7865:
7861:
7857:
7854:POW := λ
7852:
7851:
7850:
7847:
7841:
7835:
7829:
7819:
7815:
7811:
7807:
7802:
7801:
7800:
7793:
7790:
7786:
7782:
7778:
7774:
7769:
7768:
7767:
7761:
7757:
7753:
7749:
7744:
7743:
7742:
7739:
7733:
7727:
7716:
7715:
7714:
7706:
7705:
7704:
7694:
7691:
7688:
7684:
7681:
7677:
7673:
7669:
7665:
7660:
7659:
7658:
7655:
7649:
7645:
7639:
7633:
7627:
7621:
7611:
7608:
7605:
7601:
7597:
7593:
7589:
7584:
7583:
7582:
7579:
7572:
7566:
7560:
7553:
7549:
7545:
7541:
7536:
7535:
7534:
7532:
7528:
7524:
7520:
7508:
7503:
7497:
7496:impossible.)
7491:
7486:
7480:
7474:
7470:-th power of
7468:
7462:
7456:
7450:
7444:
7438:
7432:
7426:
7420:
7415:
7406:
7403:
7399:
7395:
7391:
7386:
7382:
7379:
7375:
7371:
7366:
7363:
7360:
7356:
7351:
7348:
7344:
7339:
7338:
7337:
7335:
7334:
7324:
7321:
7317:
7313:
7309:
7305:
7300:
7296:
7293:
7289:
7285:
7281:
7276:
7273:
7270:
7266:
7262:
7257:
7254:
7250:
7246:
7241:
7240:
7239:
7237:
7233:
7223:
7221:
7220:
7215:
7214:
7209:
7208:
7203:
7202:
7197:
7191:
7187:
7177:
7173:
7171:
7166:
7164:
7160:
7156:
7150:
7140:
7138:
7134:
7130:
7125:
7123:
7119:
7115:
7111:
7108:
7104:
7100:
7096:
7092:
7088:
7079:
7077:
7073:
7069:
7064:
7062:
7058:
7053:
7051:
7047:
7043:
7039:
7035:
7031:
7022:
7021:
7020:
7014:
7010:
7006:
7002:
6998:
6994:
6990:
6986:
6979:
6978:
6972:
6968:
6964:
6960:
6956:
6952:
6948:
6944:
6940:
6938:
6934:
6930:
6926:
6922:
6917:
6911:
6904:
6898:
6894:
6892:
6888:
6884:
6880:
6877:
6875:
6871:
6868:
6867:
6866:
6864:
6860:
6856:
6852:
6848:
6838:
6836:
6831:
6829:
6825:
6821:
6817:
6812:
6810:
6806:
6802:
6798:
6794:
6790:
6786:
6782:
6777:
6775:
6771:
6767:
6763:
6759:
6755:
6751:
6747:
6743:
6739:
6735:
6729:
6727:
6723:
6719:
6716:might yield λ
6715:
6711:
6707:
6703:
6694:
6692:
6688:
6684:
6680:
6676:
6671:
6669:
6665:
6661:
6657:
6653:
6649:
6645:
6641:
6637:
6633:
6629:
6625:
6621:
6616:
6614:
6606:
6603:
6600:
6597:
6594:
6591:
6590:
6589:
6586:
6578:
6576:
6572:
6568:
6559:
6555:
6551:
6546:
6543:
6539:
6535:
6531:
6527:
6524:
6520:
6516:
6512:
6511:
6510:
6508:
6504:
6500:
6495:
6493:
6489:
6485:
6481:
6477:
6473:
6469:
6465:
6461:
6457:
6453:
6449:
6445:
6441:
6437:
6433:
6429:
6425:
6412:
6408:
6404:
6400:
6396:
6392:
6388:
6385:
6381:
6377:
6373:
6369:
6365:
6361:
6357:
6353:
6350:
6347:
6344:
6340:
6336:
6333:
6329:
6326:
6322:
6319:
6316:
6312:
6309:
6306:
6302:
6299:
6295:
6294:
6293:
6174:
6172:
6167:
6166:
6165:
6159:
6155:
6146:
6138:
6134:
6129:
6125:
6121:
6113:
6108:
6104:
6100:
6095:
6091:
6090:
6089:
6087:
6075:
6072:
6066:
6059:
6055:
6054:
6053:
6044:
6034:
6032:
6026:
6009:
6006:
6003:
6000:
5997:
5988:
5985:
5982:
5979:
5976:
5970:
5961:
5958:
5955:
5952:
5949:
5946:
5943:
5937:
5925:
5922:
5919:
5916:
5913:
5910:
5907:
5901:
5895:
5889:
5886:
5883:
5880:
5877:
5874:
5871:
5862:
5859:
5847:
5844:
5841:
5838:
5835:
5826:
5823:
5820:
5817:
5814:
5788:
5785:
5782:
5779:
5776:
5767:
5764:
5761:
5758:
5755:
5749:
5738:
5734:
5729:
5715:
5712:
5709:
5706:
5686:
5683:
5677:
5674:
5671:
5665:
5659:
5653:
5650:
5647:
5644:
5621:
5618:
5615:
5612:
5592:
5589:
5583:
5580:
5577:
5571:
5565:
5559:
5556:
5553:
5550:
5527:
5504:
5501:
5498:
5492:
5485:β-reduces to
5472:
5466:
5463:
5460:
5457:
5431:
5428:
5425:
5419:
5413:
5407:
5404:
5401:
5398:
5372:
5369:
5366:
5360:
5340:
5334:
5331:
5328:
5325:
5308:
5294:
5291:
5288:
5285:
5282:
5273:
5270:
5267:
5261:
5255:
5252:
5249:
5246:
5240:
5237:
5234:
5225:
5222:
5219:
5216:
5193:
5170:
5167:
5164:
5155:
5152:
5149:
5146:
5134:
5120:
5117:
5114:
5111:
5091:
5088:
5085:
5082:
5062:
5059:
5056:
5053:
5050:
5041:
5038:
5035:
5029:
5023:
5020:
5017:
5014:
5008:
5005:
5002:
4993:
4990:
4987:
4984:
4972:
4958:
4950:
4934:
4925:
4911:
4905:
4902:
4899:
4896:
4890:
4881:
4878:
4875:
4869:
4857:
4854:
4851:
4842:
4839:
4836:
4833:
4824:
4818:
4815:
4812:
4803:
4797:
4794:
4791:
4788:
4762:
4759:
4756:
4753:
4750:
4741:
4738:
4735:
4729:
4723:
4720:
4717:
4714:
4708:
4705:
4702:
4693:
4690:
4687:
4684:
4674:For example,
4657:
4637:
4617:
4609:
4593:
4573:
4553:
4533:
4530:
4527:
4501:
4498:
4495:
4489:
4483:
4480:
4477:
4474:
4468:
4465:
4462:
4453:
4450:
4447:
4444:
4434:
4419:
4416:
4413:
4410:
4407:
4401:
4398:
4395:
4386:
4383:
4380:
4377:
4367:
4346:
4343:
4340:
4334:
4322:
4319:
4316:
4310:
4304:
4298:
4295:
4292:
4283:
4264:
4254:
4240:
4220:
4200:
4180:
4160:
4153: ; with
4140:
4137:
4134:
4114:
4111:
4105:
4102:
4099:
4093:
4086:
4072:
4052:
4032:
4012:
4005: ; with
3992:
3989:
3983:
3980:
3977:
3971:
3964:
3963:
3962:
3960:
3944:
3924:
3904:
3881:
3878:
3875:
3869:
3849:
3829:
3809:
3789:
3769:
3755:
3741:
3721:
3702:
3699:
3696:
3693:
3673:
3670:
3667:
3664:
3640:
3620:
3600:
3581:
3573:
3569:
3554:
3534:
3514:
3511:
3508:
3505:
3497:
3493:
3479:
3459:
3451:
3450:
3449:
3447:
3437:
3434:
3420:
3400:
3380:
3377:
3374:
3371:
3351:
3348:
3345:
3342:
3334:
3324:
3321:
3301:
3298:
3292:
3286:
3283:
3280:
3277:
3274:
3271:
3268:
3265:
3262:
3254:
3238:
3218:
3212:
3205:
3189:
3186:
3183:
3180:
3160:
3154:
3146:
3130:
3127:
3124:
3121:
3112:
3110:
3100:
3086:
3083:
3080:
3077:
3070:
3054:
3034:
3008:
3005:
3002:
2999:
2993:
2990:
2987:
2964:
2944:
2924:
2904:
2897:, with input
2881:
2878:
2875:
2872:
2849:
2843:
2840:
2837:
2834:
2811:
2791:
2788:
2785:
2782:
2774:
2771:
2766:
2743:
2723:
2703:
2678:
2675:
2672:
2669:
2663:
2660:
2657:
2647:
2632:
2629:
2626:
2623:
2600:
2594:
2591:
2588:
2585:
2576:
2573:
2570:
2563:
2562:
2561:
2558:
2537:
2534:
2531:
2525:
2522:
2519:
2495:
2492:
2489:
2486:
2480:
2474:
2451:
2448:
2445:
2439:
2436:
2433:
2424:
2407:
2401:
2365:
2345:
2338:
2333:
2324:the variable
2323:
2305:
2302:
2299:
2296:
2273:
2249:
2246:
2241:
2237:
2216:
2213:
2210:
2205:
2201:
2197:
2191:
2185:
2165:
2142:
2139:
2134:
2130:
2123:
2120:
2117:
2101:
2085:
2082:
2079:
2076:
2069:
2064:
2050:
2045:
2041:
2037:
2034:
2031:
2023:
2014:
1995:
1975:
1956:
1953:
1934:
1931:
1928:
1925:
1906:
1899:
1898:
1897:
1895:
1890:
1888:
1884:
1874:
1872:
1867:
1865:
1861:
1857:
1847:
1830:
1827:
1820:
1805:
1785:
1763:
1759:
1755:
1750:
1746:
1742:
1735:
1720:
1700:
1677:
1666:
1662:
1658:
1653:
1649:
1642:
1636:
1629:
1612:
1596:
1578:
1574:
1570:
1565:
1561:
1554:
1545:
1524:
1523:
1522:
1504:
1501:
1494:
1478:
1474:
1470:
1465:
1461:
1457:
1450:
1433:
1430:
1427:
1416:
1412:
1408:
1403:
1399:
1389:
1386:
1383:
1370:
1369:
1368:
1317:
1313:
1311:
1287:
1283:
1279:
1274:
1270:
1263:
1254:
1247:
1246:
1245:
1226:
1222:
1218:
1213:
1209:
1199:
1196:
1193:
1183:
1182:
1181:
1179:
1125:
1108:
1102:
1095:
1094:
1093:
1076:
1073:
1067:
1061:
1058:
1051:
1050:
1049:
1033:
1029:
1025:
1020:
1016:
1007:
995:
974:
970:
966:
961:
957:
947:
944:
941:
931:
930:
929:
927:
906:
902:
898:
893:
889:
885:
879:
876:
873:
867:
828:
827:
826:
823:
819:
805:
803:
797:
795:
791:
790:iota operator
786:
782:
779:
774:
771:
757:
737:
734:
708:
697:
675:
662:
660:
652:
646:
644:
639:
637:
631:
629:
625:
621:
618:in 1935 when
617:
613:
609:
608:Alonzo Church
599:
597:
593:
589:
585:
581:
577:
573:
568:
566:
562:
558:
554:
550:
546:
541:
539:
535:
531:
527:
523:
513:
511:
506:
504:
503:β-normal form
500:
496:
492:
484:
483:: β-reduction
463:
460:
457:
451:
439:
430:
427:
424:
421:
408:
405:
401:
380:
374:
371:
368:
365:
350:
344:
341:
338:
335:
325:
324:
323:
305:
285:
265:
245:
237:
218:
212:
202:
187:
179:
163:
155:
136:
133:
130:
127:
117:
114:
98:
91:
90:
89:
87:
83:
78:
76:
72:
68:
67:Alonzo Church
64:
60:
56:
52:
48:
44:
40:
36:
32:
31:formal system
28:
26:
21:
16615:Type shifter
16585:Quantization
16535:Continuation
16473:
16402:Veridicality
16282:Exhaustivity
16247:Cumulativity
16166:Indexicality
16146:Definiteness
16141:Conditionals
16068:Logical form
15974:
15856:
15772:Ultraproduct
15619:Model theory
15584:Independence
15520:Formal proof
15512:Proof theory
15495:
15468:
15425:real numbers
15397:second-order
15308:Substitution
15185:Metalanguage
15126:conservative
15099:Axiom schema
15043:Constructive
15013:Morse–Kelley
14979:Set theories
14958:Aleph number
14951:inaccessible
14857:Grothendieck
14741:intersection
14628:Higher-order
14616:Second-order
14562:Truth tables
14519:Venn diagram
14302:Formal proof
14191:Institutions
14107:Martin Davis
14038:
13987:
13978:
13957:Mike Thyer,
13921:
13914:
13907:
13898:
13897:L. Allison,
13890:
13876:
13864:
13837:. Retrieved
13829:
13820:
13808:. Retrieved
13796:
13792:
13779:
13752:
13748:
13735:
13726:1701.04240v1
13692:
13688:
13630:
13624:
13607:
13603:
13590:
13553:
13543:
13531:. Retrieved
13517:
13513:
13500:
13488:. Retrieved
13466:
13453:
13429:
13419:
13410:
13398:. Retrieved
13378:
13374:
13361:
13349:. Retrieved
13319:
13306:
13294:. Retrieved
13280:
13268:
13248:the original
13239:
13232:
13224:Luke Palmer
13220:
13202:
13196:
13179:
13175:
13166:
13136:
13117:
13113:
13104:
13093:. Retrieved
13055:
13045:
13024:
13014:November 17,
13012:. Retrieved
13007:
12997:
12985:. Retrieved
12974:. Springer.
12970:
12959:
12929:(2): 56–68.
12926:
12922:
12913:
12888:
12884:
12847:
12843:
12839:
12830:
12805:
12801:
12788:
12763:
12762:. Series 2.
12759:
12750:
12741:
12733:
12725:the original
12719:
12712:
12691:
12681:
12665:. Springer.
12661:
12654:
12634:
12627:
12617:November 17,
12615:. Retrieved
12610:
12597:
12564:
12560:
12551:
12542:
12533:
12521:
12495:, used with
12490:
12489:
12467:
12462:
12454:
12448:
12443:
12437:
12389:
12381:
12376:
12364:
12294:
12219:
12208:
12152:
12108:
12098:
11953:
11932:(due to the
11920:
11912:
11899:
11887:
11875:
11863:
11839:
11810:, Elsevier,
11807:
11785:
11759:
11753:
11740:
11722:
11713:
11697:
11683:
11665:
11661:
11652:
11627:. Retrieved
11621:
11608:
11601:
11572:
11568:
11553:
11495:
11480:SECD machine
11296:
11290:
11284:
11269:
11258:
11234:
11203:
11191:
11182:
11169:
11160:
11156:
11152:
11148:
11140:
11136:
11132:
11128:
11125:
11096:
11090:
11075:("agents"),
11034:
11019:
10984:
10965:Peter Landin
10962:
10941:
10936:
10932:
10930:
10916:
10911:
10905:
10901:
10895:
10889:
10883:
10877:
10869:
10858:
10848:
10837:
10824:
10820:
10811:
10805:
10799:
10789:
10785:
10781:
10777:
10773:
10769:
10765:
10761:
10757:
10753:
10749:
10745:
10733:
10715:
10703:Call by need
10692:
10685:
10681:
10677:
10670:
10666:
10662:
10658:
10652:Call by name
10640:
10512:Normal order
10506:
10475:proof theory
10468:
10464:type systems
10441:
10436:
10404:
10402:
10378:
10374:
10370:
10366:
10361:
10356:
10352:
10348:
10344:
10340:
10336:
10334:
10329:
10325:
10320:
10318:would do if
10312:
10307:
10301:
10297:
10293:
10287:
10282:
10276:
10272:
10268:
10264:
10260:
10256:
10251:
10246:
10244:
10238:
10233:
10228:
10224:
10219:
10214:
10211:
10207:
10204:
10199:
10194:
10188:
10183:
10178:
10175:
10171:
10166:
10161:
10156:
10151:
10145:
10140:
10133:
10128:
10126:contains an
10123:
10119:
10114:
10109:
10104:
10099:
10095:
10090:
10084:
10079:
10074:
10066:
10064:
10047:
10041:
10022:
10018:
10012:
10008:
9998:
9992:
9986:
9980:
9966:
9960:
9954:
9952:
9946:
9942:
9935:
9932:
9928:
9924:
9920:
9916:
9909:
9906:
9903:
9899:
9895:
9891:
9884:
9881:
9878:
9874:
9870:
9866:
9862:
9854:
9851:
9847:
9843:
9839:
9835:
9831:
9824:
9820:
9816:
9812:
9804:
9801:
9797:
9794:
9790:
9786:
9782:
9778:
9771:
9767:
9763:
9757:
9746:
9743:
9726:
9717:
9713:
9709:
9705:
9701:
9695:G) (1−1)))))
9692:
9686:G) (1−1)))))
9683:
9674:
9670:
9666:
9662:
9658:
9649:
9640:
9631:
9627:
9623:
9619:
9615:
9614:4 × (3 × ((λ
9606:
9597:
9588:
9584:
9580:
9576:
9572:
9563:
9554:
9545:
9541:
9537:
9533:
9529:
9520:
9516:
9512:
9508:
9504:
9500:
9496:
9487:
9478:
9469:
9465:
9460:
9456:
9452:
9445:
9442:
9438:
9430:
9427:
9423:
9419:
9415:
9412:
9408:
9404:
9400:
9392:
9389:
9385:
9381:
9377:
9374:
9370:
9366:
9358:
9354:
9351:
9347:
9343:
9339:
9336:
9332:
9328:
9324:
9316:
9313:
9304:
9298:
9295:
9292:
9285:
9282:
9278:
9274:
9270:
9267:
9263:
9259:
9255:
9251:
9241:
9220:
9214:
9203:
9202:× ((FIX G) (
9199:
9195:
9191:
9179:
9175:
9171:
9168:
9164:
9160:
9156:
9138:
9134:
9128:
9125:
9121:
9117:
9114:
9112:with
9103:
9099:
9095:
9091:
9087:
9083:
9076:
9073:
9066:
9063:
9059:
9045:
9039:
9036:
9032:
9028:
9025:
9022:
9020:with
9011:
9007:
9004:
9000:
8996:
8992:
8988:
8978:
8973:
8971:
8963:
8959:
8955:
8951:
8940:
8932:
8927:
8922:
8918:
8915:
8911:
8905:
8899:
8869:
8864:
8859:
8855:
8850:
8843:
8839:
8834:
8828:
8823:
8808:
8803:
8797:
8792:
8783:
8779:
8774:
8766:
8746:
8734:
8730:
8723:
8716:
8712:
8708:
8697:
8693:
8685:
8681:
8677:
8670:
8666:
8662:
8658:
8654:
8650:
8631:
8624:
8620:
8616:
8612:
8603:
8594:
8590:
8581:
8577:
8569:
8566:
8563:
8559:
8555:
8551:
8533:
8527:
8508:
8497:
8491:
8484:
8480:
8477:
8473:
8469:
8465:
8461:
8457:
8454:
8447:
8443:
8440:
8436:
8432:
8428:
8424:
8420:
8416:
8401:
8395:
8392:
8385:
8382:
8375:
8371:
8368:
8360:
8357:
8353:
8349:
8342:
8338:.FALSE) TRUE
8335:
8331:
8327:
8302:
8300:
8289:
8276:
8272:
8268:
8255:
8252:
8249:
8245:
8241:
8229:
8223:
8220:
8217:
8213:
8209:
8205:
8196:
8192:
8184:
8181:
8178:
8174:
8170:
8169:OR := λ
8162:
8159:
8156:
8152:
8148:
8141:
8135:
8131:
8127:
8119:
8115:
8111:
8096:
8081:
8077:
8071:
8067:
8061:
8058:
8055:
8048:
8044:
8040:
8036:
8024:conditionals
8013:
8006:
8002:
7998:
7994:
7990:
7986:
7978:
7975:
7971:
7967:
7963:
7957:
7955:
7948:
7944:
7940:
7936:
7932:
7929:
7925:
7921:
7917:
7913:
7909:
7905:
7901:
7887:
7880:
7876:
7872:
7866:
7863:
7859:
7855:
7845:
7839:
7833:
7827:
7824:
7817:
7813:
7809:
7805:
7798:
7791:
7788:
7784:
7780:
7776:
7772:
7765:
7759:
7755:
7751:
7747:
7737:
7731:
7729:to a number
7725:
7722:
7712:
7699:
7692:
7689:
7686:
7682:
7679:
7675:
7671:
7667:
7663:
7653:
7647:
7643:
7637:
7631:
7625:
7619:
7617:Because the
7616:
7609:
7606:
7603:
7599:
7595:
7591:
7587:
7577:
7570:
7568:and returns
7564:
7561:
7558:
7551:
7547:
7543:
7539:
7530:
7526:
7522:
7518:
7506:
7501:
7498:
7484:
7478:
7472:
7466:
7460:
7454:
7448:
7442:
7436:
7430:
7424:
7418:
7411:
7404:
7401:
7397:
7393:
7389:
7380:
7377:
7373:
7369:
7361:
7358:
7354:
7346:
7342:
7331:
7329:
7322:
7319:
7315:
7311:
7307:
7303:
7294:
7291:
7287:
7283:
7279:
7271:
7268:
7264:
7260:
7252:
7248:
7244:
7229:
7217:
7211:
7205:
7199:
7193:
7174:
7167:
7152:
7128:
7126:
7121:
7117:
7113:
7109:
7106:
7102:
7086:
7085:
7067:
7065:
7060:
7056:
7054:
7049:
7045:
7041:
7037:
7029:
7028:
7016:
7008:
7004:
7000:
6996:
6992:
6988:
6984:
6982:
6974:
6970:
6966:
6962:
6958:
6954:
6950:
6946:
6942:
6936:
6932:
6928:
6924:
6915:
6909:
6902:
6896:
6890:
6886:
6882:
6878:
6873:
6869:
6862:
6858:
6854:
6850:
6846:
6844:
6841:Substitution
6832:
6813:
6808:
6804:
6800:
6796:
6792:
6788:
6784:
6780:
6778:
6769:
6765:
6761:
6757:
6753:
6749:
6745:
6741:
6737:
6733:
6730:
6726:α-equivalent
6725:
6721:
6717:
6713:
6709:
6702:α-conversion
6701:
6700:
6697:α-conversion
6690:
6686:
6682:
6678:
6674:
6672:
6667:
6663:
6659:
6655:
6651:
6647:
6643:
6639:
6635:
6631:
6627:
6623:
6622:, short for
6619:
6617:
6613:α-equivalent
6612:
6610:
6604:
6598:
6593:α-conversion
6592:
6587:
6584:
6570:
6566:
6564:
6557:
6553:
6549:
6541:
6537:
6533:
6529:
6522:
6518:
6514:
6506:
6502:
6498:
6496:
6491:
6487:
6483:
6479:
6475:
6471:
6467:
6463:
6459:
6455:
6451:
6447:
6443:
6439:
6435:
6434:, the part λ
6431:
6427:
6423:
6421:
6410:
6406:
6402:
6398:
6394:
6390:
6383:
6379:
6375:
6374:) and not (λ
6371:
6367:
6363:
6359:
6348:
6345:
6342:
6338:
6331:
6327:
6324:
6320:
6317:
6314:
6307:
6304:
6303:instead of (
6300:
6297:
6291:
6254: :== (
6225: :== λ
6168:
6161:
6158:applications
6157:
6154:abstractions
6153:
6151:
6144:
6136:
6132:
6123:
6119:
6111:
6106:
6098:
6093:
6079:
6064:
6057:
6051:
6031:truth values
6027:
5730:
5314:
5206:, to obtain
5135:
4973:
4926:
4673:
3958:
3761:
3656:
3445:
3443:
3435:
3332:
3330:
3322:
3203:
3113:
3106:
2772:
2767:
2759:
2559:
2425:
2382:to an input
2336:
2334:
2328:in the term
2106:and returns
2067:
2065:
2018:
2012:
1951:
1891:
1886:
1880:
1877:Lambda terms
1868:
1856:lambda terms
1855:
1853:
1845:
1520:
1314:
1307:
1243:
1177:
1126:
1123:
1091:
991:
925:
923:
816:
799:
787:
784:
776:
772:
664:
656:
650:
640:
632:
624:J. B. Rosser
605:
569:
556:
552:
548:
544:
542:
519:
510:Iota and Jot
507:
488:
321:
177:
82:lambda terms
79:
55:substitution
24:
23:
19:
18:
16530:Context set
16504:Type theory
16387:Subtrigging
16151:Disjunction
16078:Proposition
15882:Type theory
15830:undecidable
15762:Truth value
15649:equivalence
15328:non-logical
14941:Enumeration
14931:Isomorphism
14878:cardinality
14862:Von Neumann
14827:Ultrafilter
14792:Uncountable
14726:equivalence
14643:Quantifiers
14633:Fixed-point
14602:First-order
14482:Consistency
14467:Proposition
14444:Traditional
14415:Lindström's
14405:Compactness
14347:Type theory
14292:Cardinality
14224:A. C. Croom
14147:Gary R. Mar
14122:Leon Henkin
14082:Alan Turing
13336:2318/149874
13292:. p. 6
13073:Corrections
11834:extensions.
11828:lambda cube
11412:β-reduction
11206:lambda cube
11145:cardinality
11108:parallelism
11053:first class
11041:subprograms
10840:normal form
10707:evaluation.
10407:is a typed
10071:combinators
9652:G) (2−1))))
9643:G) (2−1))))
9223:combinator
9221:fixed-point
9219:here), the
9082:G := λ
8987:G := λ
8707:Φ := λ
8489:is the add
8089:otherwise.
7488:) obey the
7388:3 := λ
7368:2 := λ
7353:1 := λ
7341:0 := λ
7302:3 := λ
7278:2 := λ
7259:1 := λ
7243:0 := λ
7157:is neither
7087:η-reduction
7082:η-reduction
7030:β-reduction
7025:β-reduction
6760:result in λ
6605:η-reduction
6599:β-reduction
6571:combinators
6497:The set of
6341:instead of
6249:application
6220:abstraction
6201:application
6191:abstraction
5737:Standard ML
5311:β-reduction
3547:, but with
3173:. Further,
2775:a function
2716:is of form
2616:is of form
2394:to produce
2337:application
2266:. The name
2178:defined by
2098:denotes an
2068:abstraction
2013:application
1952:abstraction
1887:lambda term
580:linguistics
572:mathematics
236:application
47:application
43:abstraction
39:computation
16700:Categories
16680:Pragmatics
16327:Mirativity
16093:Speech act
16048:Entailment
16043:Denotation
15693:elementary
15386:arithmetic
15254:Quantifier
15232:functional
15104:Expression
14822:Transitive
14766:identities
14751:complement
14684:hereditary
14667:Set theory
14172:Dana Scott
13839:6 November
13810:2022-12-01
13640:1601.01233
13400:14 January
13351:14 January
13296:14 January
13275:114 pages.
13176:Dialectica
13114:SoftOption
13095:2012-06-18
12808:(3): 630.
12497:permission
12486:References
11793:0954300653
11629:2020-04-14
11172:Dana Scott
11061:JavaScript
10949:Caml Light
10933:reasonable
10866:Complexity
10734:computable
10487:categories
10296:would do.
10210:) :=
10174:) :=
10155:) :=
10016:, so that
9927: := λ
9894: := λ
9865: := λ
9834: := λ
9815: := λ
9781: := λ
9766: := λ
9708:= 0; else
9665:= 0; else
9622:= 0; else
9609:G) (3−1)))
9600:G) (3−1)))
9579:= 0; else
9536:= 0; else
9507:= 0; else
9254: := λ
9198:= 0; else
9159: := (
9143: and
9094:= 0; else
9050: and
8999:= 0; else
8958:= 0; else
8954:) = 1, if
8894:See also:
8813:, such as
8669:_and_tail_
8369:and since
8199:FALSE TRUE
7893:PRED 0 = 0
7641:gives the
7196:arithmetic
7135:, via the
7074:, via the
6799:, we get λ
6268:expression
6259:expression
6240:expression
6186: :==
6181:expression
6056:variables
6048:Definition
4233:) remains
2022:§ Notation
813:Motivation
778:Dana Scott
576:philosophy
16479:Mereology
16415:Formalism
16297:Givenness
16222:Cataphora
16210:Phenomena
16201:Vagueness
16131:Ambiguity
16083:Reference
16063:Intension
16053:Extension
15964:Supertask
15867:Recursion
15825:decidable
15659:saturated
15637:of models
15560:deductive
15555:axiomatic
15475:Hilbert's
15462:Euclidean
15443:canonical
15366:axiomatic
15298:Signature
15227:Predicate
15116:Extension
15038:Ackermann
14963:Operation
14842:Universal
14832:Recursive
14807:Singleton
14802:Inhabited
14787:Countable
14777:Types of
14761:power set
14731:partition
14648:Predicate
14594:Predicate
14509:Syllogism
14499:Soundness
14472:Inference
14462:Tautology
14364:paradoxes
13883:EMS Press
13695:: 23–43.
13558:CiteSeerX
13533:22 August
13490:22 August
13435:MIT Press
13150:0804.3434
12384:} removed
12344:↦
12309:λ
12233:λ
12188:∣
12176:λ
12173:∣
12131:↦
12028:λ
12001:λ
11989:λ
11977:λ
11968:λ
11858:Documents
11832:subtyping
11651:"Review:
11474:Rewriting
11159:, unless
11122:Semantics
11097:any order
11057:Smalltalk
11045:arguments
10574:λ
10552:λ
10535:λ
10419:λ
10409:formalism
9945: :=
9566:G) (4−1))
9557:G) (4−1))
8974:parameter
8937:function
8935:factorial
8901:Recursion
8468:.ISZERO (
8431:.ISZERO (
8303:predicate
7843:function
7529:element'
7170:confluent
7116:whenever
6618:The term
6581:Reduction
6521:}, where
6084:, can be
5998:λ
5977:λ
5950:λ
5914:λ
5878:λ
5854:→
5836:λ
5815:λ
5777:λ
5756:λ
5747:Ω
5707:λ
5663:→
5645:λ
5613:λ
5569:→
5551:λ
5458:λ
5417:→
5399:λ
5326:λ
5286:λ
5250:λ
5217:λ
5147:λ
5112:λ
5083:λ
5054:λ
5018:λ
4985:λ
4897:λ
4834:λ
4789:λ
4754:λ
4718:λ
4685:λ
4531:≠
4478:λ
4445:λ
4411:λ
4378:λ
4138:≠
3694:λ
3665:λ
3506:λ
3472:are just
3372:λ
3343:λ
3281:λ
3272:λ
3263:λ
3216:↦
3181:λ
3158:↦
3122:λ
3078:λ
3047:which is
3000:λ
2988:λ
2873:λ
2835:λ
2783:λ
2770:example 1
2670:λ
2658:λ
2624:λ
2586:λ
2571:λ
2520:λ
2434:λ
2390:on input
2297:λ
2118:λ
2077:λ
2032:λ
1926:λ
1900:variable
1862:or as an
1646:↦
1558:↦
1549:↦
1396:↦
1345:_
1267:↦
1258:↦
1206:↦
1154:_
1106:↦
1062:
954:↦
868:
855:_
822:semantics
758:∧
735:∧
712:^
679:^
446:→
422:λ
366:λ
360:→
336:λ
128:λ
86:reduction
27:-calculus
16633:See also
16518:Concepts
16392:Telicity
16227:Coercion
16181:Negation
16176:Modality
16126:Anaphora
15949:Logicism
15942:timeline
15918:Concrete
15777:Validity
15747:T-schema
15740:Kripke's
15735:Tarski's
15730:semantic
15720:Strength
15669:submodel
15664:spectrum
15632:function
15480:Tarski's
15469:Elements
15456:geometry
15412:Robinson
15333:variable
15318:function
15291:spectrum
15281:Sentence
15237:variable
15180:Language
15133:Relation
15094:Automata
15084:Alphabet
15068:language
14922:-jection
14900:codomain
14886:Function
14847:Universe
14817:Infinite
14721:Relation
14504:Validity
14494:Argument
14392:theorem,
14075:Students
13938:Archived
13926:Archived
13743:(1965).
13667:11485010
13427:(2002).
13395:53087112
13053:(1984).
12951:15889861
12689:(2003).
11938:parallel
11826:and the
11781:meaning.
11776:11321602
11706:ACM site
11649:(1944).
11594:Archived
11517:esoteric
11513:Unlambda
11306:See also
11219:System F
10815:are the
10740:that is
10493:(CCCs).
10477:via the
10450:such as
10035:defined
9704:.(1, if
9661:.(1, if
9618:.(1, if
9575:.(1, if
9562:4 × (G (
9548:−1)))) 4
9532:.(1, if
9519:−1)))) (
9503:.(1, if
9194:.(1, if
9141:=: FIX G
9090:.(1, if
8995:.(1, if
8778:to mean
8733:.FIRST (
8501:> 0.
8483:) 1)) (λ
8446:) 1)) (λ
7960:denotes
7760:n
7708:PLUS 2 3
7333:Notation
6288:Notation
6278:variable
6230:variable
6211:variable
4065:becomes
3762:Suppose
2804:, where
1871:currying
1310:currying
538:function
113:variable
16136:Binding
15891:Related
15688:Diagram
15586: (
15565:Hilbert
15550:Systems
15545:Theorem
15423:of the
15368:systems
15148:Formula
15143:Grammar
15059: (
15003:General
14716:Forcing
14701:Element
14621:Monadic
14396:paradox
14337:Theorem
14273:General
13885:, 2001
13771:6505810
13155:Bibcode
12943:2266170
12905:2371045
12864:2268117
12822:1968646
12780:1968337
12589:2317046
12581:2268280
12540:at the
12145:maps to
12099:axiom β
11579:(1977)
11446:hackers
11391:giving
11358:Clojure
11333:objects
11112:Futures
10953:Haskell
10793: =
10456:Haskell
10013:BU(CBU)
9571:4 × ((λ
9233:(FIX G)
8926:. Here
8906:by name
8769:library
8627:.FALSE)
8476:(PLUS (
8439:(PLUS (
8065:yields
7983:, then
6833:In the
6556:) ∪ FV(
6552:) = FV(
6536:) = FV(
6366:means λ
5804:. Here
5733:Haskell
3567:removed
2773:defines
2736:
2358:
1988:
1318:of the
1178:another
602:History
545:untyped
534:binding
278:. Both
51:binding
29:) is a
16565:Monads
16112:Topics
15654:finite
15417:Skolem
15370:
15345:Theory
15313:Symbol
15303:String
15286:atomic
15163:ground
15158:closed
15153:atomic
15109:ground
15072:syntax
14968:binary
14895:domain
14812:Finite
14577:finite
14435:Logics
14394:
14342:Theory
14212:Family
13967:using
13769:
13665:
13655:
13578:
13560:
13481:
13441:
13393:
13342:
13209:
13063:
12987:29 Dec
12978:
12949:
12941:
12903:
12862:
12820:
12778:
12699:
12669:
12642:
12587:
12579:
12493:FOLDOC
12472:letrec
12058:
12040:
12022:
12013:
11846:
11814:
11791:
11774:
11729:
11638:
11583:
11542:
11443:Scheme
11389:posets
11368:proofs
11235:These
11180:domain
11073:Eiffel
11037:Pascal
11022:lambda
10997:lambda
10987:Python
10797:
10730:decide
10373:, the
9206:−1))))
9163:where
8878:letrec
8876:. The
8858:, for
8543:SECOND
8317:, but
8307:ISZERO
8016:> 0
7993:) = (λ
7816:(PLUS
7550:(PAIR
7216:, and
6957:), if
6652:reduct
6567:closed
6440:binder
6147:) ∈ Λ.
6126:) ∈ Λ.
6070:, ...;
4775:, and
4610:" for
2937:
2768:Here,
1006:mapped
727:” to “
659:lambda
653:symbol
582:, and
553:weaker
437:
216:
16257:De se
16161:Focus
16119:Areas
16088:Scope
15644:Model
15392:Peano
15249:Proof
15089:Arity
15018:Naive
14905:image
14837:Fuzzy
14797:Empty
14746:union
14691:Class
14332:Model
14322:Lemma
14280:Axiom
13789:(PDF)
13767:S2CID
13721:arXiv
13663:S2CID
13635:arXiv
13600:(PDF)
13510:(PDF)
13463:(PDF)
13391:S2CID
13371:(PDF)
13316:(PDF)
13290:(PDF)
13251:(PDF)
13244:(PDF)
13145:arXiv
13141:(PDF)
13034:32:50
12947:S2CID
12939:JSTOR
12901:JSTOR
12860:JSTOR
12818:JSTOR
12776:JSTOR
12585:S2CID
12577:JSTOR
12526:(PDF)
12259:ASCII
11945:Notes
11772:S2CID
11658:(PDF)
11515:– An
11229:types
11187:model
11163:is a
11081:C++11
11069:Scala
10856:. If
10722:FALSE
10516:form.
10271:, or
10118:from
10037:above
10033:FALSE
10004:above
9490:G) 4
9481:G) 4
9418:)) (λ
9380:)) (λ
9342:)) (λ
9273:)) (λ
9178:(FIX
9106:−1)))
9014:−1)))
8872:with
8606:.TRUE
8597:FALSE
8539:FIRST
8515:FALSE
8505:Pairs
8450:.0) 0
8408:FALSE
8379:, if
8319:FALSE
8296:FALSE
8283:FALSE
8103:FALSE
8080:>
8075:when
8047:PRED
8028:pairs
7935:)) (λ
7875:PRED
7758:SUCC
7554:) NIL
7019:above
7013:up to
6969:∉ FV(
6949:) = λ
6931:) = λ
6885:, if
6826:(see
6824:scope
6820:masks
6783:with
6706:alpha
6620:redex
6540:) \ {
6517:) = {
6464:x x y
6424:bound
6141:then
6116:then
4608:fresh
3957:in a
2322:binds
994:tuple
565:below
549:typed
234:: An
15767:Type
15570:list
15374:list
15351:list
15340:Term
15274:rank
15168:open
15062:list
14874:Maps
14779:sets
14638:Free
14608:list
14358:list
14285:list
13841:2022
13653:ISBN
13576:ISBN
13535:2022
13492:2022
13479:ISBN
13439:ISBN
13402:2022
13353:2022
13340:ISBN
13298:2022
13207:ISBN
13061:ISBN
13016:2020
12989:2016
12976:ISBN
12697:ISBN
12667:ISBN
12640:ISBN
12619:2020
11844:ISBN
11812:ISBN
11789:ISBN
11727:ISBN
11636:ISBN
11581:ISBN
11540:ISBN
11482:– A
11350:– A
11295:and
11091:The
11063:and
11030:x**2
10951:and
10823:and
10809:and
10728:can
10718:TRUE
10473:and
10454:and
10369:and
10339:and
10045:and
10031:and
10029:TRUE
10021:g=g(
9967:BCKW
9964:and
9716:G) (
9712:× ((
9673:G) (
9669:× ((
9630:G) (
9626:× ((
9587:G) (
9583:× ((
9544:G) (
9540:× ((
9523:G) 4
9357:)))
9174:) =
9155:FIX
9137:= G
9124:= G
9120:= F
9035:= G
9031:= F
8966:− 1)
8962:× F(
8822:let
8700:+ 1)
8638:NULL
8634:PAIR
8584:TRUE
8523:PAIR
8513:and
8511:TRUE
8406:and
8404:TRUE
8391:LEQ
8389:and
8381:LEQ
8311:TRUE
8267:≡ (λ
8240:≡ (λ
8101:and
8099:TRUE
8085:and
8057:SUB
8020:PRED
8011:for
7943:) (λ
7891:and
7831:and
7713:and
7701:PLUS
7513:and
7511:PAIR
7219:§ iv
7188:and
7161:nor
7112:and
7034:beta
6975:See
6965:and
6908:) =
6851:free
6787:in λ
6642:for
6528:FV(λ
6456:free
6281:>
6275:<
6271:>
6265:<
6262:>
6256:<
6252:>
6246:<
6243:>
6237:<
6233:>
6227:<
6223:>
6217:<
6214:>
6208:<
6204:>
6198:<
6194:>
6188:<
6184:>
6178:<
6173:as:
6162:See
6139:∈ Λ,
6114:∈ Λ,
6101:∈ Λ.
4546:and
3917:for
3842:and
3802:and
3570:The
3494:The
3444:The
3413:and
3364:and
2262:for
1961:and
1000:and
622:and
298:and
152:: A
111:: A
53:and
45:and
16509:TTR
15454:of
15436:of
15384:of
14916:Sur
14890:Map
14697:Ur-
14679:Set
13933:on
13801:doi
13797:121
13757:doi
13697:doi
13693:338
13645:doi
13612:doi
13568:doi
13522:doi
13518:237
13471:doi
13383:doi
13332:hdl
13324:doi
13184:doi
12931:doi
12893:doi
12852:doi
12842:".
12810:doi
12768:doi
12569:doi
12545:Lab
12261:as
12207:.—
12167:::=
11906:PDF
11894:PDF
11882:PDF
11870:PDF
11764:doi
11670:doi
11151:to
11043:as
10914:of
10899:is
10893:in
10768:in
10720:or
10661:.(λ
10181:if
10065:If
9984:is
9947:ω ω
9923:or
9919:or
9511:× (
9486:G (
9459:G)
9433:)))
9403:((λ
9327:.(λ
9258:.(λ
9244:FIX
9225:FIX
9098:× (
9086:. λ
9069:) G
9048:= G
9003:× (
8991:. λ
8874:let
8846:let
8832:in
8815:let
8690:to
8642:NIL
8537:),
8487:.0)
8472:1)
8435:1)
8009:)))
7985:T(λ
7883:− 1
7820:) 0
7573:+ 1
7515:NIL
7213:iii
7131:in
7091:eta
7070:in
7048:is
6973:)
6830:).
6758:not
6687:M x
6681:, λ
6673:If
6666:is
6646:in
6550:M N
6548:FV(
6513:FV(
6494:).
6492:z x
6450:to
6407:xyz
6372:M N
6364:M N
6358:: λ
6339:MNP
6273:)
6145:M N
6130:If
6105:If
6092:If
5735:or
4951:of
4520:if
4127:if
3937:in
3572:set
3496:set
2824:is
2335:An
2066:An
1957:if
1907:if
1889:".
1008:to
1004:is
996:of
928:as
804:".
547:or
489:If
33:in
16702::
15840:NP
15464::
15458::
15388::
15065:),
14920:Bi
14912:In
13977:,
13881:,
13875:,
13828:.
13795:.
13791:.
13765:.
13751:.
13747:.
13711:^
13691:.
13687:.
13675:^
13661:.
13651:.
13643:.
13608:15
13606:.
13602:.
13574:.
13566:.
13552:.
13516:.
13512:.
13477:.
13465:.
13433:.
13389:.
13379:63
13377:.
13373:.
13338:.
13330:.
13318:.
13260:^
13180:42
13178:.
13153:,
13126:^
13116:.
13112:.
13080:^
13075:).
13006:.
12945:.
12937:.
12925:.
12899:.
12889:58
12887:.
12872:^
12858:.
12846:.
12816:.
12806:36
12804:.
12796:;
12774:.
12764:33
12609:.
12583:.
12575:.
12563:.
12506:^
12442:(λ
12147:".
12117:^
12084:^
11904:-(
11892:-(
11880:-(
11868:-(
11770:.
11760:90
11758:.
11700:,
11696:,
11686:,
11666:50
11664:.
11660:.
11611:,
11575:,
11538:.
11534:.
11289:,
11208::
11167:.
11135:→
11077:C#
11071:,
11059:,
11009:**
10928:.
10920:.
10780:)=
10772:,
10764:,
10752:→
10748::
10676:(λ
10452:ML
10403:A
10389:.
10328:.
10306:(λ
10281:(λ
10267:,
10259:)
10237:,
10227:)
10223:,
10203:,
10170:,
10149:,
10051:.
10027:.
10025:g)
9993:YI
9987:UU
9978:.
9961:SK
9898:.λ
9873:.λ
9869:.λ
9842:.λ
9838:.λ
9819:.λ
9789:.λ
9785:.λ
9739:24
9528:(λ
9499:.λ
9495:(λ
9395:))
9365:(λ
9323:(λ
9288:))
9239:.
9167:=
8950:F(
8939:F(
8921:)
8910:(λ
8791:(λ
8719:))
8696:,
8684:,
8661:.λ
8657:.λ
8653:(λ
8623:.λ
8619:(λ
8558:.λ
8554:.λ
8464:.λ
8460:(λ
8427:.λ
8423:(λ
8374:=
8352:.λ
8334:(λ
8301:A
8298:.
8271:.λ
8244:.λ
8212:.λ
8208:.λ
8173:.λ
8151:.λ
8130:.λ
8114:.λ
8105::
8070:−
8039:.λ
7981:))
7966:.λ
7962:(λ
7920:.λ
7916:(λ
7908:.λ
7904:.λ
7879:=
7858:.λ
7808:.λ
7779:.λ
7775:.λ
7750:.λ
7674:.λ
7670:.λ
7666:.λ
7594:.λ
7590:.λ
7542:.λ
7407:))
7390:fx
7370:fx
7355:fx
7343:fx
7336::
7325:))
7306:.λ
7282:.λ
7263:.λ
7247:.λ
7222:.
7210:,
7207:ii
7204:,
7165:.
7139:.
7124:.
7078:.
7052:.
7044:)
7011:,
6961:≠
6953:.(
6941:(λ
6923:(λ
6889:≠
6881:=
6872:=
6803:.λ
6791:.λ
6776:.
6764:.λ
6748:.λ
6736:.λ
6693:.
6670:.
6662:)
6634:)
6577:.
6560:).
6544:}.
6486:(λ
6466:,
6397:.λ
6393:.λ
6382:)
6370:.(
6334:).
6330:)
6310:).
6235:.
6206:|
6196:|
6160:.
6135:,
6118:(λ
6088::
6063:,
5947::=
5911::=
5875::=
5675::=
5581::=
5540:,
5502::=
5429::=
5370::=
5271::=
5238::=
5168::=
5133:.
5039::=
5006::=
4924:.
4879::=
4855::=
4816::=
4739::=
4706::=
4499::=
4466::=
4399::=
4344::=
4320::=
4296::=
4193:,
4103::=
4045:,
3981::=
3879::=
3782:,
3754:.
3320:.
3147:,
3099:.
2557:.
2423:.
2015:).
1954:);
1866:.
1831:29
1505:29
1059:id
638:.
630:.
598:.
590:.
578:,
574:,
540:.
505:.
461::=
16016:e
16009:t
16002:v
15920:/
15835:P
15590:)
15376:)
15372:(
15269:∀
15264:!
15259:∃
15220:=
15215:↔
15210:→
15205:∧
15200:∨
15195:¬
14918:/
14914:/
14888:/
14699:)
14695:(
14582:∞
14572:3
14360:)
14258:e
14251:t
14244:v
14017:e
14010:t
14003:v
13843:.
13813:.
13803::
13773:.
13759::
13753:8
13729:.
13723::
13705:.
13699::
13669:.
13647::
13637::
13618:.
13614::
13584:.
13570::
13537:.
13524::
13494:.
13473::
13447:.
13404:.
13385::
13355:.
13334::
13326::
13300:.
13190:.
13186::
13157::
13147::
13098:.
13071:(
13069:.
13018:.
12991:.
12953:.
12933::
12927:5
12907:.
12895::
12866:.
12854::
12848:7
12824:.
12812::
12782:.
12770::
12707:.
12705:.
12675:.
12648:.
12621:.
12591:.
12571::
12565:2
12543:n
12499:.
12455:N
12452:)
12449:M
12446:.
12444:f
12421:N
12401:M
12382:x
12347:t
12341:x
12321:)
12318:t
12315:.
12312:x
12306:(
12278:t
12275:.
12272:x
12269:L
12245:)
12242:t
12239:.
12236:x
12230:(
12195:e
12191:e
12185:e
12182:.
12179:x
12170:x
12164:e
12067:)
12064:)
12061:y
12055:x
12052:(
12049:)
12046:)
12043:y
12037:z
12034:.
12031:y
12025:(
12019:)
12016:x
12010:z
12007:.
12004:x
11998:(
11995:.
11992:z
11986:(
11983:.
11980:y
11974:.
11971:x
11965:(
11778:.
11766::
11735:.
11678:.
11672::
11642:)
11634:(
11632:.
11557:.
11546:.
11298:I
11292:K
11286:S
11183:D
11161:D
11157:D
11153:D
11149:D
11141:D
11137:D
11133:D
11129:D
11026:x
11015:)
11012:2
11006:x
11003::
11000:x
10994:(
10917:E
10912:n
10908:)
10906:n
10904:(
10902:O
10896:E
10890:V
10884:E
10878:V
10859:e
10849:e
10829:β
10825:y
10821:x
10812:y
10806:x
10800:y
10795:β
10790:x
10786:f
10782:y
10778:x
10776:(
10774:F
10770:N
10766:y
10762:x
10758:f
10754:N
10750:N
10746:F
10689:.
10686:x
10684:)
10682:y
10680:.
10678:y
10671:x
10669:)
10667:y
10665:.
10663:y
10659:x
10657:λ
10631:.
10619:y
10599:)
10595:)
10592:)
10589:z
10586:z
10583:(
10580:.
10577:z
10570:)
10567:z
10564:z
10561:(
10558:.
10555:z
10549:(
10544:y
10541:.
10538:x
10531:(
10379:W
10375:S
10371:C
10367:B
10362:x
10357:K
10353:C
10349:B
10345:S
10341:C
10337:B
10330:S
10326:N
10321:x
10316:)
10313:N
10310:.
10308:x
10302:K
10298:I
10294:P
10291:)
10288:N
10285:.
10283:x
10277:P
10273:S
10269:K
10265:I
10261:P
10257:N
10255:,
10252:x
10249:(
10247:T
10241:)
10239:N
10234:x
10231:(
10229:T
10225:M
10220:x
10217:(
10215:T
10212:S
10208:N
10205:M
10200:x
10197:(
10195:T
10191:.
10189:N
10184:x
10179:N
10176:K
10172:N
10167:x
10164:(
10162:T
10157:I
10152:x
10146:x
10143:(
10141:T
10134:T
10129:x
10124:N
10120:N
10115:x
10110:N
10108:,
10105:x
10102:(
10100:T
10096:N
10093:.
10091:x
10089:λ
10085:N
10083:,
10080:x
10077:(
10075:T
10067:N
10048:F
10042:T
10023:Y
10019:Y
10011:=
10009:Y
9999:Y
9981:Ω
9955:I
9943:Ω
9936:x
9933:x
9931:.
9929:x
9925:U
9921:Δ
9917:ω
9910:y
9907:y
9904:x
9902:.
9900:y
9896:x
9892:W
9885:y
9882:z
9879:x
9877:.
9875:z
9871:y
9867:x
9863:C
9857:)
9855:z
9852:y
9850:(
9848:x
9846:.
9844:z
9840:y
9836:x
9832:B
9825:x
9823:.
9821:y
9817:x
9813:K
9807:)
9805:z
9802:y
9800:(
9798:z
9795:x
9793:.
9791:z
9787:y
9783:x
9779:S
9772:x
9770:.
9768:x
9764:I
9747:Y
9727:Y
9718:n
9714:Y
9710:n
9706:n
9702:n
9693:Y
9684:Y
9675:n
9671:Y
9667:n
9663:n
9659:n
9650:Y
9641:Y
9632:n
9628:Y
9624:n
9620:n
9616:n
9607:Y
9598:Y
9589:n
9585:Y
9581:n
9577:n
9573:n
9564:Y
9555:Y
9546:n
9542:Y
9538:n
9534:n
9530:n
9521:Y
9517:n
9515:(
9513:r
9509:n
9505:n
9501:n
9497:r
9488:Y
9479:Y
9477:(
9470:n
9466:n
9461:n
9457:Y
9455:(
9448:)
9446:g
9443:Y
9441:(
9439:g
9431:x
9428:x
9426:(
9424:g
9422:.
9420:x
9416:x
9413:x
9411:(
9409:g
9407:.
9405:x
9401:g
9393:x
9390:x
9388:(
9386:g
9384:.
9382:x
9378:x
9375:x
9373:(
9371:g
9369:.
9367:x
9359:g
9355:x
9352:x
9350:(
9348:h
9346:.
9344:x
9340:x
9337:x
9335:(
9333:h
9331:.
9329:x
9325:h
9317:g
9314:Y
9305:g
9299:g
9296:Y
9286:x
9283:x
9281:(
9279:g
9277:.
9275:x
9271:x
9268:x
9266:(
9264:g
9262:.
9260:x
9256:g
9252:Y
9229:F
9217:G
9204:n
9200:n
9196:n
9192:n
9182:)
9180:g
9176:g
9172:r
9169:g
9165:r
9161:r
9157:g
9139:r
9135:r
9129:x
9126:r
9122:x
9118:x
9115:r
9104:n
9102:(
9100:r
9096:n
9092:n
9088:n
9084:r
9067:x
9064:x
9062:.
9060:x
9046:r
9040:x
9037:r
9033:x
9029:x
9026:r
9023:r
9012:n
9010:(
9008:r
9005:r
9001:n
8997:n
8993:n
8989:r
8979:r
8968:.
8964:n
8960:n
8956:n
8952:n
8943:)
8941:n
8928:E
8923:E
8919:x
8916:x
8914:.
8912:x
8870:N
8865:f
8860:N
8856:N
8851:f
8835:M
8829:N
8826:=
8824:f
8804:N
8801:)
8798:M
8795:.
8793:f
8784:M
8780:N
8775:f
8735:n
8731:n
8717:x
8713:x
8709:x
8698:n
8694:n
8692:(
8688:)
8686:n
8682:m
8680:(
8671:t
8667:h
8663:z
8659:t
8655:h
8651:l
8625:y
8621:x
8617:p
8615:.
8613:p
8604:x
8595:p
8593:.
8591:p
8582:p
8580:.
8578:p
8570:y
8567:x
8564:f
8562:.
8560:f
8556:y
8552:x
8534:y
8531:,
8528:x
8498:n
8492:n
8485:v
8481:k
8478:g
8474:k
8470:g
8466:k
8462:g
8458:n
8448:v
8444:k
8441:g
8437:k
8433:g
8429:k
8425:g
8421:n
8419:.
8417:n
8396:m
8393:n
8386:n
8383:m
8376:n
8372:m
8365:,
8363:)
8361:n
8358:m
8354:n
8350:m
8336:x
8332:n
8330:.
8328:n
8315:0
8281:β
8277:x
8275:.
8273:y
8269:x
8260:β
8256:p
8253:q
8250:p
8248:.
8246:q
8242:p
8224:b
8221:a
8218:p
8216:.
8214:b
8210:a
8206:p
8197:p
8195:.
8193:p
8185:q
8182:p
8179:p
8177:.
8175:q
8171:p
8163:p
8160:q
8157:p
8155:.
8153:q
8149:p
8136:y
8134:.
8132:y
8128:x
8120:x
8118:.
8116:y
8112:x
8087:0
8082:n
8078:m
8072:n
8068:m
8062:n
8059:m
8052:,
8049:m
8045:n
8043:.
8041:n
8037:m
8014:n
8007:x
8005:(
8003:f
8001:(
7999:h
7997:.
7995:h
7991:x
7989:.
7987:u
7979:f
7976:g
7974:(
7972:h
7970:.
7968:h
7964:g
7958:T
7951:)
7949:u
7947:.
7945:u
7941:x
7939:.
7937:u
7933:f
7930:g
7928:(
7926:h
7924:.
7922:h
7918:g
7914:n
7912:.
7910:x
7906:f
7902:n
7888:n
7881:n
7877:n
7867:b
7864:e
7862:.
7860:e
7856:b
7846:m
7840:n
7834:n
7828:m
7818:n
7814:m
7812:.
7810:n
7806:m
7794:)
7792:f
7789:n
7787:(
7785:m
7783:.
7781:f
7777:n
7773:m
7756:m
7754:.
7752:n
7748:m
7738:m
7732:n
7726:m
7718:5
7695:)
7693:x
7690:f
7687:n
7685:(
7683:f
7680:m
7678:.
7676:x
7672:f
7668:n
7664:m
7654:f
7648:n
7646:+
7644:m
7638:f
7632:n
7626:f
7620:m
7612:)
7610:x
7607:f
7604:n
7602:(
7600:f
7598:.
7596:x
7592:f
7588:n
7578:f
7571:n
7565:n
7552:x
7548:n
7546:.
7544:x
7540:n
7538:λ
7531:n
7527:x
7523:x
7519:n
7507:n
7502:n
7494:0
7485:f
7479:f
7473:f
7467:n
7461:f
7455:n
7449:f
7443:f
7437:n
7431:f
7425:n
7419:f
7405:x
7402:f
7400:(
7398:f
7396:(
7394:f
7392:.
7383:)
7381:x
7378:f
7376:(
7374:f
7372:.
7362:x
7359:f
7357:.
7347:x
7345:.
7323:x
7320:f
7318:(
7316:f
7314:(
7312:f
7310:.
7308:x
7304:f
7297:)
7295:x
7292:f
7290:(
7288:f
7286:.
7284:x
7280:f
7272:x
7269:f
7267:.
7265:x
7261:f
7253:x
7251:.
7249:x
7245:f
7201:i
7122:f
7118:x
7114:f
7110:x
7107:f
7105:.
7103:x
7089:(
7061:n
7059:.
7057:n
7050:M
7046:N
7042:M
7040:.
7038:x
7032:(
7009:x
7007:.
7005:z
7001:x
6997:x
6995:.
6993:x
6989:y
6987:.
6985:x
6971:N
6967:y
6963:y
6959:x
6955:M
6951:y
6947:M
6945:.
6943:y
6937:M
6935:.
6933:x
6929:M
6927:.
6925:x
6919:2
6916:M
6913:1
6910:M
6906:2
6903:M
6900:1
6897:M
6895:(
6891:y
6887:x
6883:y
6879:y
6874:N
6870:x
6863:N
6859:M
6855:x
6847:M
6809:y
6807:.
6805:y
6801:y
6797:x
6795:.
6793:y
6789:x
6785:y
6781:x
6770:y
6768:.
6766:x
6762:y
6754:x
6752:.
6750:x
6746:y
6742:x
6740:.
6738:x
6734:x
6732:λ
6722:y
6720:.
6718:y
6714:x
6712:.
6710:x
6704:(
6691:M
6685:.
6683:x
6679:M
6675:x
6668:M
6664:N
6660:M
6658:.
6656:x
6648:M
6644:x
6640:N
6636:N
6632:M
6630:.
6628:x
6558:N
6554:M
6542:x
6538:M
6534:M
6532:.
6530:x
6523:x
6519:x
6515:x
6507:M
6503:M
6490:.
6488:x
6484:y
6482:.
6480:x
6476:x
6472:x
6468:y
6462:.
6460:y
6452:M
6448:x
6444:x
6436:x
6432:M
6430:.
6428:x
6413:.
6411:N
6409:.
6403:N
6401:.
6399:z
6395:y
6391:x
6386:.
6384:N
6380:M
6378:.
6376:x
6368:x
6362:.
6360:x
6351:.
6349:P
6346:N
6343:M
6332:P
6328:N
6325:M
6321:P
6318:N
6315:M
6308:N
6305:M
6301:N
6298:M
6143:(
6137:N
6133:M
6124:M
6122:.
6120:x
6112:M
6107:x
6099:x
6094:x
6082:Λ
6068:2
6065:v
6061:1
6058:v
6013:)
6010:x
6007:x
6004:.
6001:x
5995:(
5992:)
5989:x
5986:x
5983:.
5980:x
5974:(
5971:=
5968:)
5965:]
5962:x
5959:x
5956:.
5953:x
5944:x
5941:[
5938:x
5935:(
5932:)
5929:]
5926:x
5923:x
5920:.
5917:x
5908:x
5905:[
5902:x
5899:(
5896:=
5893:]
5890:x
5887:x
5884:.
5881:x
5872:x
5869:[
5866:)
5863:x
5860:x
5857:(
5851:)
5848:x
5845:x
5842:.
5839:x
5833:(
5830:)
5827:x
5824:x
5821:.
5818:x
5812:(
5792:)
5789:x
5786:x
5783:.
5780:x
5774:(
5771:)
5768:x
5765:x
5762:.
5759:x
5753:(
5750:=
5716:y
5713:.
5710:x
5687:y
5684:=
5681:]
5678:s
5672:x
5669:[
5666:y
5660:s
5657:)
5654:y
5651:.
5648:x
5642:(
5622:x
5619:.
5616:x
5593:s
5590:=
5587:]
5584:s
5578:x
5575:[
5572:x
5566:s
5563:)
5560:x
5557:.
5554:x
5548:(
5528:s
5508:]
5505:s
5499:x
5496:[
5493:t
5473:s
5470:)
5467:t
5464:.
5461:x
5455:(
5435:]
5432:s
5426:x
5423:[
5420:t
5414:s
5411:)
5408:t
5405:.
5402:x
5396:(
5376:]
5373:s
5367:x
5364:[
5361:t
5341:s
5338:)
5335:t
5332:.
5329:x
5323:(
5295:x
5292:.
5289:z
5283:=
5280:)
5277:]
5274:x
5268:y
5265:[
5262:y
5259:(
5256:.
5253:z
5247:=
5244:]
5241:x
5235:y
5232:[
5229:)
5226:y
5223:.
5220:z
5214:(
5194:z
5174:]
5171:x
5165:y
5162:[
5159:)
5156:y
5153:.
5150:x
5144:(
5121:x
5118:.
5115:x
5092:y
5089:.
5086:x
5063:x
5060:.
5057:x
5051:=
5048:)
5045:]
5042:x
5036:y
5033:[
5030:y
5027:(
5024:.
5021:x
5015:=
5012:]
5009:x
5003:y
5000:[
4997:)
4994:y
4991:.
4988:x
4982:(
4959:r
4935:y
4912:y
4909:)
4906:y
4903:.
4900:x
4894:(
4891:=
4888:)
4885:]
4882:y
4876:x
4873:[
4870:x
4867:(
4864:)
4861:]
4858:y
4852:x
4849:[
4846:)
4843:y
4840:.
4837:x
4831:(
4828:(
4825:=
4822:]
4819:y
4813:x
4810:[
4807:)
4804:x
4801:)
4798:y
4795:.
4792:x
4786:(
4783:(
4763:x
4760:.
4757:x
4751:=
4748:)
4745:]
4742:y
4736:y
4733:[
4730:x
4727:(
4724:.
4721:x
4715:=
4712:]
4709:y
4703:y
4700:[
4697:)
4694:x
4691:.
4688:x
4682:(
4670:.
4658:r
4638:y
4618:r
4594:y
4586:(
4574:r
4554:y
4534:y
4528:x
4508:)
4505:]
4502:r
4496:x
4493:[
4490:t
4487:(
4484:.
4481:y
4475:=
4472:]
4469:r
4463:x
4460:[
4457:)
4454:t
4451:.
4448:y
4442:(
4420:t
4417:.
4414:x
4408:=
4405:]
4402:r
4396:x
4393:[
4390:)
4387:t
4384:.
4381:x
4375:(
4353:)
4350:]
4347:r
4341:x
4338:[
4335:s
4332:(
4329:)
4326:]
4323:r
4317:x
4314:[
4311:t
4308:(
4305:=
4302:]
4299:r
4293:x
4290:[
4287:)
4284:s
4265:t
4262:(
4241:y
4221:x
4201:y
4181:x
4161:r
4141:y
4135:x
4115:y
4112:=
4109:]
4106:r
4100:x
4097:[
4094:y
4073:r
4053:x
4033:x
4013:r
3993:r
3990:=
3987:]
3984:r
3978:x
3975:[
3972:x
3945:t
3925:x
3905:r
3885:]
3882:r
3876:x
3873:[
3870:t
3850:y
3830:x
3810:r
3790:s
3770:t
3742:y
3722:x
3703:y
3700:.
3697:x
3674:x
3671:.
3668:x
3653:.
3641:s
3621:t
3601:s
3582:t
3555:x
3535:t
3515:t
3512:.
3509:x
3480:x
3460:x
3421:y
3401:x
3381:y
3378:.
3375:y
3352:x
3349:.
3346:x
3308:)
3305:)
3302:x
3299:g
3296:(
3293:f
3290:(
3287:.
3284:x
3278:.
3275:g
3269:.
3266:f
3239:y
3219:y
3213:x
3190:y
3187:.
3184:x
3161:x
3155:x
3131:x
3128:.
3125:x
3087:x
3084:.
3081:x
3055:x
3035:N
3015:)
3012:)
3009:x
3006:.
3003:x
2997:(
2994:.
2991:x
2985:(
2965:M
2945:N
2925:M
2905:x
2885:)
2882:x
2879:.
2876:x
2870:(
2850:x
2847:)
2844:x
2841:.
2838:x
2832:(
2812:B
2792:B
2789:.
2786:x
2763:x
2744:N
2724:M
2704:x
2685:)
2682:)
2679:x
2676:.
2673:x
2667:(
2664:.
2661:x
2655:(
2633:B
2630:.
2627:x
2604:)
2601:x
2598:)
2595:x
2592:.
2589:x
2583:(
2580:(
2577:.
2574:x
2555:y
2541:)
2538:y
2535:+
2532:x
2529:(
2526:.
2523:x
2510:y
2496:y
2493:+
2490:x
2487:=
2484:)
2481:x
2478:(
2475:f
2455:)
2452:y
2449:+
2446:x
2443:(
2440:.
2437:x
2411:)
2408:s
2405:(
2402:t
2392:s
2388:t
2384:s
2380:t
2366:s
2346:t
2330:t
2326:x
2309:)
2306:t
2303:.
2300:x
2294:(
2274:f
2264:t
2250:2
2247:+
2242:2
2238:x
2217:,
2214:2
2211:+
2206:2
2202:x
2198:=
2195:)
2192:x
2189:(
2186:f
2166:f
2146:)
2143:2
2140:+
2135:2
2131:x
2127:(
2124:.
2121:x
2108:t
2104:x
2086:t
2083:.
2080:x
2051:.
2046:2
2042:x
2038:.
2035:x
1999:)
1996:s
1976:t
1973:(
1963:s
1959:t
1938:)
1935:t
1932:.
1929:x
1923:(
1913:x
1909:t
1902:x
1883:C
1828:=
1806:2
1786:y
1764:2
1760:2
1756:+
1751:2
1747:5
1743:=
1721:5
1701:x
1681:)
1678:2
1675:(
1672:)
1667:2
1663:y
1659:+
1654:2
1650:5
1643:y
1640:(
1637:=
1616:)
1613:2
1610:(
1605:)
1600:)
1597:5
1594:(
1589:)
1584:)
1579:2
1575:y
1571:+
1566:2
1562:x
1555:y
1552:(
1546:x
1541:(
1534:(
1517:,
1502:=
1479:2
1475:2
1471:+
1466:2
1462:5
1458:=
1437:)
1434:2
1431:,
1428:5
1425:(
1422:)
1417:2
1413:y
1409:+
1404:2
1400:x
1393:)
1390:y
1387:,
1384:x
1381:(
1378:(
1354:m
1351:u
1348:s
1342:e
1339:r
1336:a
1333:u
1330:q
1327:s
1293:)
1288:2
1284:y
1280:+
1275:2
1271:x
1264:y
1261:(
1255:x
1227:2
1223:y
1219:+
1214:2
1210:x
1203:)
1200:y
1197:,
1194:x
1191:(
1163:m
1160:u
1157:s
1151:e
1148:r
1145:a
1142:u
1139:q
1136:s
1109:x
1103:x
1077:x
1074:=
1071:)
1068:x
1065:(
1034:2
1030:y
1026:+
1021:2
1017:x
1002:y
998:x
975:2
971:y
967:+
962:2
958:x
951:)
948:y
945:,
942:x
939:(
907:2
903:y
899:+
894:2
890:x
886:=
883:)
880:y
877:,
874:x
871:(
864:m
861:u
858:s
852:e
849:r
846:a
843:u
840:q
837:s
738:x
709:x
676:x
651:λ
470:)
467:]
464:N
458:x
455:[
452:M
449:(
443:)
440:N
434:)
431:M
428:.
425:x
419:(
416:(
406:.
387:)
384:]
381:y
378:[
375:M
372:.
369:y
363:(
357:)
354:]
351:x
348:[
345:M
342:.
339:x
333:(
306:N
286:M
266:N
246:M
222:)
219:N
213:M
210:(
200:.
188:M
178:.
164:x
140:)
137:M
134:.
131:x
125:(
99:x
25:λ
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.