6512:-equivalence is undecidable. Huet showed in 1973 that 3rd order unification is undecidable and this was improved upon by Baxter in 1978 then by Goldfarb in 1981 by showing that 2nd order unification is already undecidable. A proof that higher order matching (unification where only one term contains existential variables) is decidable was announced by Colin Stirling in 2006, and a full proof was published in 2009.
2833:
197:, as a formal language based on symbolic expressions, consisted of a denumerably infinite series of axioms and variables, but also a finite set of primitive symbols, denoting abstraction and scope, as well as four constants: negation, disjunction, universal quantification, and selection respectively; and also, a finite set of rules I to VI. This finite set of rules included rule V
3413:). The essential difference between intrinsic and extrinsic approaches is just whether the typing rules are viewed as defining the language, or as a formalism for verifying properties of a more primitive underlying language. Most of the different semantic interpretations discussed below can be seen through either an intrinsic or extrinsic perspective.
1962:
1837:
5512:
6734:
Plotkin introduced logical relations in 1973 to characterize the elements of a model that are definable by lambda terms. In 1993 Jung and Tiuryn showed that a general form of logical relation (Kripke logical relations with varying arity) exactly characterizes lambda definability. Plotkin and
Statman
3249:
may mean different things. (The classic intended interpretations are the identity function on integers and the identity function on boolean values.) In contrast, an extrinsic semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language. In this view,
3396:
The distinction between intrinsic and extrinsic semantics is sometimes associated with the presence or absence of annotations on lambda abstractions, but strictly speaking this usage is imprecise. It is possible to define an extrinsic semantics on annotated terms simply by ignoring the types
3133:
Broadly speaking, there are two different ways of assigning meaning to the simply typed lambda calculus, as to typed languages more generally, variously called intrinsic vs. extrinsic, ontological vs. semantical, or Church-style vs. Curry-style. An intrinsic semantics only assigns meaning to
203:
as well as IV and VI for substitution and generalization respectively. Rules I to III are known as alpha, beta, and eta conversion in the lambda calculus. Church sought to use
English only as a syntax language (that is, a metamathematical language) for describing symbolic expressions with no
4492:
6199:
Because of these last two rules coercing between synthesis and checking, it is easy to see that any well-typed but unannotated term can be checked in the bidirectional system, so long as we insert "enough" type annotations. And in fact, annotations are needed only at β-redexes.
2639:
5400:
4758:
The presentation given above is not the only way of defining the syntax of the simply typed lambda calculus. One alternative is to remove type annotations entirely (so that the syntax is identical to the untyped lambda calculus), while ensuring that terms are well-typed via
6931:
2589:
4746:, p. 60, which Henkin 1949 filled in with type domains (e.g. the natural numbers, the real numbers, etc.). Henkin 1996 p. 146 described how Church's logistic method could seek to provide a foundation for mathematics (Peano arithmetic and real analysis), via
5642:
1657:
5256:
1844:
1723:
4294:
1714:
5570:
5308:
4373:
7056:
3134:
well-typed terms, or more precisely, assigns meaning directly to typing derivations. This has the effect that terms differing only by type annotations can nonetheless be assigned different meanings. For example, the identity term
5406:
3864:. Conversely, the simply typed lambda calculus with product types and pairing operators over a collection of base types and given terms forms a CCC whose objects are the types, and morphisms are equivalence classes of terms.
6379:. All programs in the simply typed lambda calculus halt. For the untyped lambda calculus, there are programs that do not halt, and moreover there is no general decision procedure that can determine whether a program halts.
725:
7166:
2476:
3588:
3012:
1173:
4379:
2828:{\displaystyle \lambda x{\mathbin {:}}\tau \to \tau '\to \tau ''.\lambda y{\mathbin {:}}\tau \to \tau '.\lambda z{\mathbin {:}}\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''}
7492:
3513:
5316:
3689:
4631:
3355:
3243:
6032:
need any annotation on the lambda abstraction in rule , because the type of the bound variable can be deduced from the type at which we check the function. Finally, we explain rules and as follows:
3300:
3184:
6291:
4049:
6778:
4895:
3624:
1473:
2634:
4843:
4155:
4102:
3731:
3118:
2200:
5132:
5004:
6366:
5100:
4972:
3062:
1301:
2514:
617:
6328:
579:
5576:
6173:
5819:
5685:
3911:
1391:
1357:
6567:
3941:
1043:
999:
4532:
3999:
6472:
4921:
386:
5915:
5789:
4575:
2282:
2226:
487:
6636:
6598:
360:
48:
331:
2509:
949:
5763:
4797:
3391:
8180:
6729:
6694:
6671:
6510:
6433:
6002:
3842:
2369:
7266:
7302:
767:
8157:
4182:
2893:
1957:{\displaystyle {\frac {\Gamma \vdash e_{1}{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash e_{2}{\mathbin {:}}\sigma }{\Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}}
1599:
7226:
5962:
5705:
5152:
5024:
4655:
3536:
2329:
2098:
2052:
2012:
1832:{\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau }{\Gamma \vdash (\lambda x{\mathbin {:}}\sigma .~e){\mathbin {:}}(\sigma \to \tau )}}}
1577:
1533:
1513:
1431:
507:
434:
6406:
5202:
4763:. The inference algorithm is terminating, sound, and complete: whenever a term is typable, the algorithm computes its type. More precisely, it computes the term's
2928:
911:
885:
859:
833:
285:
245:
8057:
6193:
6137:
6094:
6074:
6022:
5942:
5889:
5859:
5192:
5064:
4679:
3973:
2864:
2421:
2389:
2309:
2256:
2138:
1083:
527:
454:
547:
406:
179:
84:
4221:
1664:
5520:
4209:
6117:
6054:
5839:
5725:
5507:{\displaystyle {\frac {\Gamma \vdash e_{1}\Rightarrow \sigma \to \tau \quad \Gamma \vdash e_{2}\Leftarrow \sigma }{\Gamma \vdash e_{1}~e_{2}\Rightarrow \tau }}}
5262:
5172:
5044:
4300:
3771:
3751:
2158:
2118:
2078:
2032:
1992:
1553:
1493:
1411:
1240:
1216:
1196:
1063:
807:
787:
648:
305:
265:
225:
6944:
7343:
6212:: every sequence of reductions eventually terminates. This is because recursion is not allowed by the typing rules: it is impossible to find types for
207:
In 1940 Church settled on a subscript notation for denoting the type in a symbolic expression. In his presentation, Church used only two base types:
664:
6028:
Observe that the rules for synthesis are read top-to-bottom, whereas the rules for checking are read bottom-to-top. Note in particular that we do
7072:
2426:
3541:
4487:{\displaystyle (\pi _{1}(u{\mathbin {:}}\sigma \times \tau ),\pi _{2}(u{\mathbin {:}}\sigma \times \tau ))=u{\mathbin {:}}\sigma \times \tau }
2933:
1111:
130:
1318:
To define the set of well-typed lambda terms of a given type, one defines a typing relation between terms and types. First, one introduces
1591:(wherein the premises above the line allow us to derive the conclusion below the line). Simply typed lambda calculus uses these rules:
5395:{\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e\Leftarrow \tau }{\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }}}
3438:
90:. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by
3635:
6409:
6209:
4584:
456:
can range over types. The infinite number of axioms were then seen to be a consequence of applying rules I to VI to the types (see
8402:
3305:
3193:
7794:
7706:
6926:{\displaystyle a_{\alpha },b_{\alpha },...z_{\alpha },...{\bar {a}}_{\alpha },{\bar {b}}_{\alpha },...{\bar {z}}_{\alpha },...}
3773:. The advantage of typed lambda calculus is that STLC allows potentially nonterminating computations to be cut short (that is,
3253:
3137:
6735:
conjectured that it is decidable whether a given element of a model generated from finite sets is definable by a lambda term (
6604:
are representable as functions over Church numerals; these are roughly the polynomials closed up under a conditional operator.
6219:
4004:
8589:
8316:
8121:
7684:
4720:
4848:
3593:
1442:
8374:
8006:
4802:
4107:
4054:
3697:
3070:
2163:
5105:
4977:
2584:{\displaystyle \lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma }
8605:
8347:
8279:
7864:
7572:
6333:
5073:
4945:
4760:
3405:), as it is possible to give an intrinsic semantics on unannotated terms when the types can be deduced from context (
3020:
1255:
7384:
584:
5637:{\displaystyle {\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e{\mathbin {:}}\tau )\Rightarrow \tau }}}
4685:. The set of terms in the language is the closure of this set of terms under the operations of abstraction and
8636:
7444:
6296:
552:
8503:
8488:
5653:, except for the careful choice of checking or synthesis judgments. These choices can be explained like so:
6142:
5794:
5660:
3886:
1366:
1330:
416:. By the 1970s stand-alone arrow notation was in use; for example in this article non-subscripted symbols
8493:
7401:
4724:
3426:
1015:
The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. The term
6522:
3916:
2597:
1018:
954:
8395:
6479:
4498:
3978:
3849:
7168:
are four constants denoting negation, disjunction, universal quantification, and selection respectively.
6446:
4900:
4696:
between the category of
Cartesian closed categories, and the category of simply typed lambda theories.
365:
5894:
5768:
4554:
3821:
The simply typed lambda calculus enriched with product types, pairing and projection operators (with
2261:
2205:
466:
8452:
8447:
7351:
6614:
6576:
4930:, which requires more type annotations than Hindley–Milner inference but is easier to describe. The
336:
122:
26:
8339:
7969:
Goldfarb, Warren D. (1 January 1981). "The undecidability of the second-order unification problem".
310:
8631:
8435:
7546:(presents an extrinsically typed combinatory logic, later adapted by others to the lambda calculus)
4715:
The simply typed lambda calculus is closely related to the implicational fragment of propositional
4700:
4545:
3857:
2488:
916:
5736:
4770:
3364:
8162:
7893:
6711:
6676:
6653:
6492:
6486:
6415:
5967:
3824:
2334:
1652:{\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }}}
1008:
is also fixed for the base types. For example, it might be assumed that one of the base types is
134:
95:
8231:
7244:
8498:
8388:
7280:
6213:
5251:{\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x\Rightarrow \sigma }}}
734:
146:
8142:
6673:-equivalence, if the base types are interpreted by infinite sets. Statman showed in 1983 that
4160:
2869:
8483:
7664:
7211:
6475:
5947:
5690:
5137:
5009:
4640:
3786:
3521:
2314:
2083:
2037:
1997:
1562:
1518:
1498:
1416:
492:
419:
55:
6391:
4289:{\displaystyle \pi _{1}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=s{\mathbin {:}}\sigma }
2898:
1709:{\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c{\mathbin {:}}T}}}
890:
864:
838:
812:
270:
230:
8641:
8584:
8362:
7501:
6647:
6440:
6436:
6178:
6122:
6079:
6059:
6007:
5920:
5867:
5844:
5565:{\displaystyle {\frac {\Gamma \vdash e\Rightarrow \tau }{\Gamma \vdash e\Leftarrow \tau }}}
5177:
5049:
4716:
4664:
3946:
3806:
2849:
2406:
2374:
2287:
2234:
2123:
1249:
In comparison, the syntax of untyped lambda calculus has no such typing or term constants:
1086:
1068:
512:
439:
8528:
5303:{\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c\Rightarrow T}}}
4368:{\displaystyle \pi _{2}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=t{\mathbin {:}}\tau }
532:
391:
164:
69:
8:
8518:
8473:
8369:
7051:{\displaystyle \lambda ,(,),N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}
3798:
3014:. That is, the order of a type measures the depth of the most left-nested arrow. Hence:
7588:
7505:
7268:' denotes the process of producing the substitution of expression u for x, in the form t
4191:
8548:
8513:
8209:
8082:
8033:
8015:
7870:
7645:
7637:
7561:
7532:
7487:
7376:
7368:
7229:
6708:
holds, i.e. finite sets are sufficient to distinguish terms that are not identified by
6102:
6039:
5824:
5710:
5157:
5029:
4704:
3789:
of simply typed lambda calculus can be fixed as for the untyped lambda calculus, using
3756:
3736:
2143:
2103:
2063:
2017:
1977:
1538:
1478:
1396:
1324:
1225:
1201:
1181:
1048:
792:
772:
633:
290:
250:
210:
7946:
7929:
7906:
6443:, a proof that was later simplified by Mairson. The problem is known to be in the set
8553:
8343:
8312:
8275:
8201:
8117:
8074:
7986:
7982:
7951:
7910:
7860:
7823:
7808:
7789:
7770:
7766:
7735:
7720:
7701:
7680:
7629:
7568:
7537:
7519:
6639:
4736:
4732:
4728:
4578:
3845:
3422:
3246:
2840:
2479:
623:
110:
8213:
8086:
7874:
7380:
3805:
is a fundamental property of all of these evaluation strategies. Additionally, the
8568:
8543:
8538:
8478:
8342:, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993.
8304:
8267:
8193:
8109:
8066:
8037:
8025:
7978:
7941:
7902:
7852:
7848:[1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science
7813:
7803:
7762:
7725:
7715:
7672:
7649:
7621:
7556:
7527:
7509:
7360:
63:
8029:
7457:
8523:
8440:
8425:
8308:
7753:
Mairson, Harry G. (14 September 1992). "A simple proof of a theorem of
Statman".
7605:
6376:
194:
158:
59:
8266:. Lecture Notes in Computer Science. Vol. 664. Springer. pp. 245–257.
7671:. Lecture Notes in Computer Science. Vol. 242. Springer. pp. 136–175.
2839:
These are the typed lambda calculus representations of the basic combinators of
287:
has one term constant. Frequently the calculus with only one base type, usually
8563:
8296:
8227:
7493:
Proceedings of the
National Academy of Sciences of the United States of America
6643:
6570:
6516:
6369:
4764:
3856:. Given any CCC, the basic types of the corresponding lambda calculus are the
3853:
3813:
implies that any evaluation strategy will terminate on all simply typed terms.
3430:
3410:
142:
118:
7888:
6941:
Church 1940, p.57: the 2nd and 3rd primitive symbols listed ( ) denote scope:
6293:. Recursion can be added to the language by either having a special operator
720:{\displaystyle \tau ::=\tau \to \tau \mid T\quad \mathrm {where} \quad T\in B}
8625:
8411:
8335:
8205:
8078:
7990:
7955:
7914:
7856:
7827:
7774:
7739:
7676:
7633:
7523:
7483:
7432:
7416:
7339:
6756:
4926:
Another alternative presentation of simply typed lambda calculus is based on
3794:
3627:
91:
87:
7445:(Last updated on November 25, 2021 14:00 UTC) Understanding typing judgments
7161:{\displaystyle N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}
6375:
Unlike the untyped lambda calculus, the simply typed lambda calculus is not
4692:
This correspondence can be extended to include "language homomorphisms" and
7842:
7541:
7514:
4747:
4743:
4212:
3790:
3402:
457:
199:
7891:(1 April 1973). "The undecidability of unification in third order logic".
2471:{\displaystyle \lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau }
8610:
8533:
8508:
8468:
8108:. Lecture Notes in Mathematics. Vol. 453. Springer. pp. 22–37.
8004:
Stirling, Colin (22 July 2009). "Decidability of higher-order matching".
7818:
7730:
4931:
3868:
3802:
3583:{\displaystyle \Gamma ,x{\mathbin {:}}\sigma \vdash t{\mathbin {:}}\tau }
1588:
51:
7846:
4544:
The above can then be turned into a category by taking the types as the
8558:
8271:
8197:
8113:
8070:
7641:
7372:
7304:' denotes the process of producing the expansion of form t applied to x
6601:
3007:{\displaystyle o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))}
1168:{\displaystyle e::=x\mid \lambda x{\mathbin {:}}\tau .e\mid e\,e\mid c}
181:
and suitable type variables, while polymorphism and dependency cannot.
153:. The simple types, except for full recursion, are still considered
8259:
8138:
8101:
8052:
7567:. Cambridge, England: Cambridge University Press. pp. 327, 334.
126:
114:
7843:"An inverse of the evaluation functional for typed lambda -calculus"
7625:
7364:
6775:
Church 1940, p.57 denotes variables with subscripts for their type:
4549:
3861:
138:
106:
8020:
7930:"The undecidability of the third order dyadic unification problem"
7609:
7417:(Sep 1949) The Completeness of the First-Order Functional Calculus
6208:
Given the standard semantics, the simply typed lambda calculus is
5194:
as output. These judgments are derived via the following rules:
4693:
3508:{\displaystyle (\lambda x{\mathbin {:}}\sigma .~t)\,u=_{\beta }t}
3187:
8380:
6439:. Statman showed in 1979 that the normalisation problem is not
4215:. The equational theory is extended likewise, so that one has
105:
is also used to refer to extensions of the simply typed lambda
3684:{\displaystyle \lambda x{\mathbin {:}}\sigma .~t\,x=_{\eta }t}
1583:. The validity of a typing judgement is shown by providing a
7610:"Intensional interpretations of functionals of finite type I"
7198:
5730:
The types of term constants are fixed and can be synthesized.
4686:
4626:{\displaystyle (x{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )}
489:
refers to the type of functions that, given an input of type
4184:
correspond to the projections of the
Cartesian product. The
333:, etc. denote type variables; the parenthesized subscripted
5649:
Observe that rules – are nearly identical to rules (1)–(4)
4681:), having no free variables in it, except for (optionally)
7459:
Church and Curry: Combining
Intrinsic and Extrinsic Typing
6739:). The conjecture was shown to be false by Loader in 2001.
3350:{\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}
3238:{\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}
3128:
3295:{\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}
3179:{\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}
6286:{\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)}
4044:{\displaystyle u{\mathbin {:}}\tau _{1}\times \tau _{2}}
1012:, and its term constants could be the natural numbers.
7177:
Church 1940, p.59 Henkin 1949 p.160; Henkin 1996 p.144
1310:(i.e. function) must specify the type of its argument.
8186:
8058:
7589:(Spring 2019) Reduction Strategies for Lambda Calculus
6646:. Friedman showed in 1975 that this interpretation is
4897:, etc., which are all instances of the principal type
4742:
From his logistic method Church 1940 p.58 laid out an
3429:, but subject to type restrictions. The equation for
2959:
94:
in 1940 as an attempt to avoid paradoxical use of the
8165:
8145:
7283:
7247:
7214:
7075:
6947:
6781:
6714:
6679:
6656:
6617:
6579:
6525:
6495:
6449:
6418:
6394:
6336:
6299:
6222:
6181:
6145:
6125:
6105:
6082:
6062:
6042:
6010:
5970:
5950:
5923:
5897:
5870:
5847:
5827:
5797:
5771:
5739:
5713:
5693:
5663:
5579:
5523:
5409:
5319:
5265:
5205:
5180:
5160:
5140:
5108:
5076:
5052:
5032:
5012:
4980:
4948:
4903:
4851:
4805:
4773:
4667:
4643:
4587:
4557:
4501:
4382:
4303:
4224:
4194:
4163:
4110:
4057:
4007:
3981:
3949:
3919:
3889:
3827:
3759:
3739:
3700:
3638:
3596:
3544:
3524:
3441:
3421:
The simply typed lambda calculus (STLC) has the same
3367:
3308:
3256:
3196:
3140:
3073:
3023:
2936:
2901:
2872:
2852:
2642:
2600:
2517:
2491:
2429:
2409:
2377:
2337:
2317:
2290:
2264:
2237:
2208:
2166:
2146:
2126:
2106:
2086:
2066:
2040:
2020:
2000:
1980:
1847:
1726:
1667:
1602:
1565:
1541:
1521:
1501:
1481:
1445:
1419:
1399:
1369:
1333:
1258:
1228:
1204:
1184:
1114:
1071:
1051:
1021:
957:
919:
893:
867:
841:
815:
795:
775:
737:
667:
636:
587:
555:
535:
515:
495:
469:
442:
422:
394:
368:
339:
313:
293:
273:
253:
233:
213:
167:
72:
29:
7840:
4890:{\displaystyle {\mathtt {bool}}\to {\mathtt {bool}}}
3619:{\displaystyle \Gamma \vdash u{\mathbin {:}}\sigma }
1468:{\displaystyle \Gamma \vdash e{\mathbin {:}}\sigma }
650:, must first be defined. These are sometimes called
8044:
5006:respectively. Operationally, the three components
769:, generates an infinite set of types starting with
8174:
8151:
7790:"The typed λ-calculus is not elementary recursive"
7702:"The typed λ-calculus is not elementary recursive"
7560:
7433:(Jun 1996) The Discovery of My Completeness Proofs
7296:
7260:
7220:
7160:
7050:
6925:
6723:
6688:
6665:
6630:
6592:
6561:
6504:
6466:
6427:
6400:
6360:
6322:
6285:
6187:
6167:
6131:
6111:
6088:
6068:
6048:
6016:
5996:
5956:
5936:
5909:
5883:
5853:
5833:
5813:
5783:
5757:
5719:
5699:
5679:
5636:
5564:
5506:
5394:
5302:
5250:
5186:
5166:
5146:
5126:
5094:
5058:
5038:
5018:
4998:
4966:
4915:
4889:
4838:{\displaystyle {\mathtt {int}}\to {\mathtt {int}}}
4837:
4791:
4673:
4649:
4625:
4569:
4526:
4486:
4367:
4288:
4203:
4176:
4150:{\displaystyle \pi _{2}(u){\mathbin {:}}\tau _{2}}
4149:
4097:{\displaystyle \pi _{1}(u){\mathbin {:}}\tau _{1}}
4096:
4043:
3993:
3967:
3935:
3905:
3836:
3765:
3745:
3726:{\displaystyle \Gamma \vdash t\!:\sigma \to \tau }
3725:
3683:
3618:
3582:
3530:
3507:
3385:
3349:
3294:
3237:
3178:
3112:
3056:
3006:
2922:
2887:
2858:
2827:
2628:
2583:
2503:
2470:
2415:
2383:
2363:
2323:
2303:
2276:
2250:
2220:
2194:
2152:
2132:
2112:
2092:
2072:
2046:
2026:
2006:
1986:
1956:
1831:
1708:
1651:
1571:
1547:
1527:
1507:
1487:
1467:
1425:
1405:
1385:
1351:
1295:
1234:
1210:
1190:
1167:
1077:
1057:
1037:
993:
943:
905:
879:
853:
827:
801:
781:
761:
719:
642:
611:
573:
541:
521:
501:
481:
448:
428:
400:
380:
354:
325:
299:
279:
259:
239:
219:
173:
78:
42:
7665:"Cartesian closed categories and typed λ-calculi"
6482:) was given by Berger and Schwichtenberg in 1991.
4934:is divided into two judgments, representing both
3710:
3113:{\displaystyle o((\iota \to \iota )\to \iota )=2}
2195:{\displaystyle \lambda x{\mathbin {:}}\sigma .~e}
8623:
7669:Combinators and Functional Programming Languages
7443:Hedonistic Learning: Learning for the fun of it
6696:-equivalence is the maximal equivalence that is
5127:{\displaystyle \Gamma \vdash e\Rightarrow \tau }
4999:{\displaystyle \Gamma \vdash e\Rightarrow \tau }
1579:). Instances of the typing relation are called
8260:"A new characterization of lambda definability"
7427:
7425:
7411:
7409:
7195:Church 1940 p.58 lists 24 abbreviated formulas.
6771:
6769:
6361:{\displaystyle (\alpha \to \alpha )\to \alpha }
5196:
5095:{\displaystyle \Gamma \vdash e\Leftarrow \tau }
4967:{\displaystyle \Gamma \vdash e\Leftarrow \tau }
4699:Part of this correspondence can be extended to
3057:{\displaystyle o(\iota \to \iota \to \iota )=1}
2057:Term constants have the appropriate base types.
1593:
8053:"Definierbare Funktionen imλ-Kalkül mit Typen"
8050:
7065:
7063:
6372:, though both eliminate strong normalization.
1296:{\displaystyle e::=x\mid \lambda x.e\mid e\,e}
8396:
8093:
7962:
7344:"A formulation of the simple theory of types"
7334:
7332:
7330:
7328:
7326:
7324:
7322:
7320:
7318:
7316:
7180:
6478:. A purely semantic normalisation proof (see
307:, is considered. The Greek letter subscripts
8220:
8130:
7841:Berger, U.; Schwichtenberg, H. (July 1991).
7746:
7693:
7600:
7598:
7596:
7422:
7406:
6935:
6766:
5791:in some context, we extend the context with
4710:
756:
744:
8288:
8051:Schwichtenberg, Helmut (1 September 1975).
7921:
7834:
7656:
7171:
7060:
4767:, since often an unannotated term (such as
1359:, which are sets of typing assumptions. A
658:. With this fixed, the syntax of types is:
612:{\displaystyle \sigma \to (\tau \to \rho )}
8403:
8389:
8303:. Springer Netherlands. pp. 331–342.
8257:
7437:
7313:
7204:This article displays 4 typing judgements
5687:is in the context, we can synthesize type
4727:: terms correspond precisely to proofs in
1222:if it is inside of an abstraction binding
161:of such structures can be done using only
8251:
8233:Lambda-definability and logical relations
8019:
7945:
7881:
7817:
7807:
7729:
7719:
7593:
7531:
7513:
7402:(1956) Introduction to Mathematical Logic
6573:). Schwichtenberg showed in 1975 that in
6323:{\displaystyle {\mathtt {fix}}_{\alpha }}
3664:
3473:
2399:terms typable in the empty context, are:
1289:
1198:is a term constant. A variable reference
1155:
574:{\displaystyle \sigma \to \tau \to \rho }
189:In the 1930s Alonzo Church sought to use
8239:(Technical report). Edinburgh University
8099:
8003:
7968:
7555:
7394:
7189:
6700:, i.e. closed under type substitutions (
6642:and function types by the set-theoretic
3816:
3780:
247:for "the type of individuals". The type
8363:"Notes on Simply Typed Lambda Calculus"
8226:
8136:
7787:
7752:
7699:
7581:
6750:
6638:is given by interpreting base types as
6203:
4753:
4539:if t has type 1, then it reduces to nil
3129:Intrinsic vs. extrinsic interpretations
1306:Whereas in typed lambda calculus every
133:). In contrast, systems that introduce
8624:
8360:
8297:"The Undecidability of λ-Definability"
8294:
7927:
7662:
7338:
6168:{\displaystyle (e{\mathbin {:}}\tau )}
5814:{\displaystyle x{\mathbin {:}}\sigma }
5680:{\displaystyle x{\mathbin {:}}\sigma }
3906:{\displaystyle s{\mathbin {:}}\sigma }
3810:
1386:{\displaystyle x{\mathbin {:}}\sigma }
1352:{\displaystyle \Gamma ,\Delta ,\dots }
8590:University of California, Los Angeles
8384:
8264:Typed Lambda Calculi and Applications
7482:
7476:
6309:
6306:
6303:
6139:, then the explicitly annotated term
4882:
4879:
4876:
4873:
4863:
4860:
4857:
4854:
4830:
4827:
4824:
4814:
4811:
4808:
3333:
3330:
3327:
3324:
3278:
3275:
3272:
3221:
3218:
3215:
3212:
3162:
3159:
3156:
7887:
7604:
7488:"Functionality in Combinatory Logic"
7455:
6562:{\displaystyle (o\to o)\to (o\to o)}
6382:
4721:implicational propositional calculus
4701:closed symmetric monoidal categories
3936:{\displaystyle t{\mathbin {:}}\tau }
3416:
2629:{\displaystyle \tau ,\tau ',\tau ''}
2140:, then, in the same context without
1038:{\displaystyle x{\mathbin {:}}\tau }
994:{\displaystyle (b\to a)\to (a\to b)}
8375:Stanford Encyclopedia of Philosophy
8258:Jung, Achim; Tiuryn, Jerzy (1993).
8007:Logical Methods in Computer Science
6704:). A corollary of this is that the
6702:Statman's Typical Ambiguity Theorem
4527:{\displaystyle t{\mathbin {:}}1=()}
3994:{\displaystyle \sigma \times \tau }
1246:if there are no unbound variables.
227:for "the type of propositions" and
16:Formal system in mathematical logic
13:
7928:Baxter, Lewis D. (1 August 1978).
7215:
7112:
7002:
6761:Introduction to Mathematical Logic
6467:{\displaystyle {\mathcal {E}}^{4}}
6453:
6223:
5600:
5583:
5544:
5527:
5466:
5442:
5413:
5356:
5323:
5282:
5230:
5225:
5141:
5109:
5077:
5013:
4981:
4949:
4916:{\displaystyle \alpha \to \alpha }
3701:
3597:
3545:
3525:
1912:
1884:
1851:
1767:
1730:
1684:
1627:
1622:
1522:
1446:
1340:
1334:
703:
700:
697:
694:
691:
388:. Church 1940 p.58 used 'arrow or
14:
8653:
8606:Alonzo Church (college president)
8410:
8354:
7563:Theories of Programming Languages
7205:
6076:, it suffices to synthesize type
5650:
5274: is a constant of type
5102:, whereas the synthesis judgment
3852:(CCCs), as was first observed by
1676: is a constant of type
381:{\displaystyle \beta \to \alpha }
7700:Statman, Richard (1 July 1979).
5910:{\displaystyle \sigma \to \tau }
5784:{\displaystyle \sigma \to \tau }
4570:{\displaystyle \sigma \to \tau }
2277:{\displaystyle \sigma \to \tau }
2221:{\displaystyle \sigma \to \tau }
482:{\displaystyle \sigma \to \tau }
8361:Loader, Ralph (February 1998).
8137:Statman, R. (1 December 1983).
7997:
7781:
7549:
7449:
7271:
7235:
6631:{\displaystyle \lambda ^{\to }}
6593:{\displaystyle \lambda ^{\to }}
5441:
4799:) may have more than one type (
4211:and vocalized as 'nil', is the
4001:. Likewise, if one has a term
2866:is assigned an order, a number
1883:
1313:
707:
689:
355:{\displaystyle (\alpha \beta )}
267:has no term constants, whereas
43:{\displaystyle \lambda ^{\to }}
8301:Logic, Meaning and Computation
8102:"Equality between functionals"
7788:Statman, Richard (July 1979).
7153:
7144:
7128:
7119:
7043:
7034:
7018:
7009:
6960:
6954:
6899:
6868:
6846:
6623:
6585:
6556:
6550:
6544:
6541:
6538:
6532:
6526:
6352:
6349:
6343:
6337:
6280:
6256:
6253:
6229:
6162:
6146:
5901:
5775:
5625:
5622:
5606:
5592:
5553:
5536:
5495:
5458:
5435:
5429:
5383:
5377:
5348:
5291:
5239:
5174:as inputs, producing the type
5118:
5086:
4990:
4958:
4907:
4868:
4819:
4620:
4588:
4561:
4521:
4518:
4459:
4456:
4434:
4418:
4396:
4383:
4346:
4314:
4267:
4235:
4198:
4195:
4127:
4121:
4074:
4068:
3962:
3950:
3801:. As for any typed language,
3717:
3502:
3490:
3470:
3442:
3101:
3095:
3092:
3086:
3080:
3077:
3045:
3039:
3033:
3027:
3001:
2998:
2992:
2977:
2971:
2965:
2952:
2946:
2940:
2911:
2905:
2882:
2876:
2814:
2808:
2805:
2794:
2788:
2785:
2782:
2771:
2760:
2754:
2748:
2739:
2700:
2670:
2659:
2575:
2569:
2462:
2268:
2212:
2060:If, in a certain context with
1877:
1823:
1817:
1811:
1801:
1773:
988:
982:
976:
973:
970:
964:
958:
938:
932:
926:
923:
897:
871:
845:
819:
677:
606:
600:
594:
591:
565:
559:
536:
473:
395:
372:
349:
340:
326:{\displaystyle \alpha ,\beta }
168:
73:
35:
1:
8329:
7947:10.1016/S0019-9958(78)90172-9
7907:10.1016/S0019-9958(73)90301-X
7614:The Journal of Symbolic Logic
4761:Hindley–Milner type inference
2504:{\displaystyle \sigma ,\tau }
944:{\displaystyle a\to (a\to a)}
8431:Simply typed lambda calculus
8309:10.1007/978-94-010-0526-5_15
7983:10.1016/0304-3975(81)90040-2
7971:Theoretical Computer Science
7809:10.1016/0304-3975(79)90007-0
7795:Theoretical Computer Science
7767:10.1016/0304-3975(92)90020-G
7755:Theoretical Computer Science
7721:10.1016/0304-3975(79)90007-0
7707:Theoretical Computer Science
5964:(in the same context), then
5758:{\displaystyle \lambda x.~e}
5573:
5517:
5403:
5313:
5259:
5199:
4792:{\displaystyle \lambda x.~x}
3386:{\displaystyle \lambda x.~x}
3123:
1841:
1720:
1661:
1596:
509:, produce an output of type
21:simply typed lambda calculus
7:
8175:{\displaystyle \beta \eta }
8159:-definable functionals and
6724:{\displaystyle \beta \eta }
6689:{\displaystyle \beta \eta }
6666:{\displaystyle \beta \eta }
6505:{\displaystyle \beta \eta }
6480:normalisation by evaluation
6428:{\displaystyle \beta \eta }
5997:{\displaystyle e_{1}~e_{2}}
4928:bidirectional type checking
3850:Cartesian closed categories
3837:{\displaystyle \beta \eta }
2364:{\displaystyle e_{1}~e_{2}}
10:
8658:
7261:{\displaystyle =_{\beta }}
6737:Plotkin–Statman conjecture
2395:Examples of closed terms,
2231:If, in a certain context,
1045:denotes that the variable
362:denotes the function type
8598:
8577:
8461:
8418:
8340:Lambda Calculi with Types
8100:Friedman, Harvey (1975).
7352:Journal of Symbolic Logic
7297:{\displaystyle =_{\eta }}
6388:Tait showed in 1967 that
5070:to the checking judgment
4711:Proof-theoretic semantics
3626:, while the equation for
762:{\displaystyle B=\{a,b\}}
549:associates to the right:
184:
8152:{\displaystyle \lambda }
7857:10.1109/LICS.1991.151645
7677:10.1007/3-540-17184-3_44
6743:
4725:Curry–Howard isomorphism
4188:, of type 1, written as
4177:{\displaystyle \pi _{i}}
3860:, and the terms are the
3753:does not appear free in
2888:{\displaystyle o(\tau )}
109:with constructs such as
8030:10.2168/LMCS-5(3:2)2009
7934:Information and Control
7894:Information and Control
7221:{\displaystyle \Gamma }
6214:fixed-point combinators
6034:
5957:{\displaystyle \sigma }
5917:(in some context), and
5700:{\displaystyle \sigma }
5147:{\displaystyle \Gamma }
5019:{\displaystyle \Gamma }
4650:{\displaystyle \sigma }
4637:is a variable (of type
4051:, then there are terms
3531:{\displaystyle \Gamma }
3427:untyped lambda calculus
2591:(the K-combinator), and
2324:{\displaystyle \sigma }
2093:{\displaystyle \sigma }
2047:{\displaystyle \sigma }
2007:{\displaystyle \sigma }
1572:{\displaystyle \sigma }
1528:{\displaystyle \Gamma }
1508:{\displaystyle \sigma }
1426:{\displaystyle \sigma }
1085:. The term syntax, in
622:To define the types, a
502:{\displaystyle \sigma }
429:{\displaystyle \sigma }
96:untyped lambda calculus
8370:"Church's Type Theory"
8295:Loader, Ralph (2001).
8176:
8153:
7515:10.1073/pnas.20.11.584
7298:
7262:
7222:
7162:
7052:
6927:
6725:
6690:
6667:
6632:
6594:
6563:
6506:
6468:
6429:
6402:
6401:{\displaystyle \beta }
6362:
6324:
6287:
6189:
6169:
6133:
6113:
6090:
6070:
6050:
6018:
5998:
5958:
5938:
5911:
5885:
5855:
5835:
5815:
5785:
5759:
5721:
5701:
5681:
5638:
5566:
5508:
5396:
5304:
5252:
5188:
5168:
5148:
5128:
5096:
5060:
5040:
5020:
5000:
4968:
4917:
4891:
4839:
4793:
4675:
4651:
4627:
4571:
4537:This last is read as "
4528:
4488:
4369:
4290:
4205:
4178:
4151:
4098:
4045:
3995:
3969:
3937:
3907:
3838:
3767:
3747:
3727:
3685:
3620:
3584:
3532:
3509:
3387:
3351:
3296:
3239:
3190:and the identity term
3180:
3114:
3058:
3008:
2930:; for function types,
2924:
2923:{\displaystyle o(T)=0}
2889:
2860:
2829:
2630:
2585:
2505:
2472:
2417:
2385:
2365:
2325:
2305:
2278:
2252:
2222:
2196:
2154:
2134:
2114:
2094:
2074:
2048:
2028:
2008:
1988:
1958:
1833:
1710:
1653:
1573:
1549:
1529:
1509:
1489:
1469:
1427:
1407:
1387:
1353:
1297:
1236:
1212:
1192:
1169:
1079:
1059:
1039:
995:
945:
907:
906:{\displaystyle b\to a}
881:
880:{\displaystyle b\to b}
855:
854:{\displaystyle a\to b}
829:
828:{\displaystyle a\to a}
803:
783:
763:
721:
644:
613:
575:
543:
523:
503:
483:
450:
430:
414:is an abbreviation for
402:
382:
356:
327:
301:
281:
280:{\displaystyle \iota }
261:
241:
240:{\displaystyle \iota }
221:
175:
80:
44:
8637:Theory of computation
8484:George Alfred Barnard
8453:Church–Rosser theorem
8448:Frege–Church ontology
8177:
8154:
7299:
7263:
7223:
7163:
7053:
6928:
6726:
6706:finite model property
6691:
6668:
6633:
6600:exactly the extended
6595:
6564:
6519:by terms of the type
6507:
6476:Grzegorczyk hierarchy
6469:
6430:
6403:
6363:
6325:
6288:
6216:and the looping term
6190:
6188:{\displaystyle \tau }
6170:
6134:
6132:{\displaystyle \tau }
6114:
6091:
6089:{\displaystyle \tau }
6071:
6069:{\displaystyle \tau }
6051:
6019:
6017:{\displaystyle \tau }
5999:
5959:
5939:
5937:{\displaystyle e_{2}}
5912:
5886:
5884:{\displaystyle e_{1}}
5856:
5854:{\displaystyle \tau }
5836:
5816:
5786:
5760:
5722:
5702:
5682:
5639:
5567:
5509:
5397:
5305:
5253:
5189:
5187:{\displaystyle \tau }
5169:
5149:
5129:
5097:
5061:
5059:{\displaystyle \tau }
5041:
5021:
5001:
4969:
4918:
4892:
4840:
4794:
4676:
4674:{\displaystyle \tau }
4652:
4628:
4572:
4529:
4489:
4370:
4291:
4206:
4179:
4152:
4099:
4046:
3996:
3970:
3968:{\displaystyle (s,t)}
3938:
3908:
3844:-equivalence) is the
3839:
3817:Categorical semantics
3799:evaluation strategies
3787:operational semantics
3781:Operational semantics
3768:
3748:
3728:
3686:
3621:
3585:
3533:
3510:
3425:of βη-equivalence as
3388:
3357:mean the same thing (
3352:
3297:
3240:
3181:
3115:
3059:
3009:
2925:
2890:
2861:
2859:{\displaystyle \tau }
2830:
2631:
2586:
2506:
2473:
2418:
2416:{\displaystyle \tau }
2386:
2384:{\displaystyle \tau }
2366:
2326:
2306:
2304:{\displaystyle e_{2}}
2279:
2253:
2251:{\displaystyle e_{1}}
2223:
2197:
2155:
2135:
2133:{\displaystyle \tau }
2115:
2095:
2075:
2049:
2029:
2014:in the context, then
2009:
1989:
1959:
1834:
1711:
1654:
1574:
1550:
1530:
1510:
1490:
1470:
1428:
1408:
1388:
1354:
1298:
1237:
1213:
1193:
1170:
1080:
1078:{\displaystyle \tau }
1060:
1040:
996:
946:
908:
882:
856:
830:
804:
784:
764:
722:
645:
614:
576:
544:
524:
522:{\displaystyle \tau }
504:
484:
451:
449:{\displaystyle \tau }
431:
403:
383:
357:
328:
302:
282:
262:
242:
222:
176:
149:) are not considered
81:
45:
8585:Princeton University
8436:Church–Turing thesis
8163:
8143:
7851:. pp. 203–211.
7281:
7245:
7212:
7073:
6945:
6779:
6712:
6677:
6654:
6615:
6577:
6523:
6493:
6447:
6441:elementary recursive
6416:
6410:strongly normalizing
6392:
6334:
6297:
6220:
6210:strongly normalizing
6204:General observations
6179:
6143:
6123:
6119:checks against type
6103:
6080:
6060:
6040:
6008:
5968:
5948:
5944:checks against type
5921:
5895:
5868:
5845:
5825:
5795:
5769:
5737:
5711:
5691:
5661:
5577:
5521:
5407:
5317:
5263:
5203:
5178:
5158:
5138:
5106:
5074:
5050:
5030:
5010:
4978:
4946:
4901:
4849:
4803:
4771:
4754:Alternative syntaxes
4717:intuitionistic logic
4665:
4641:
4585:
4555:
4499:
4380:
4301:
4222:
4192:
4161:
4108:
4055:
4005:
3979:
3947:
3917:
3887:
3825:
3807:strong normalization
3757:
3737:
3698:
3636:
3594:
3542:
3522:
3439:
3365:
3361:, the same thing as
3306:
3254:
3194:
3138:
3071:
3021:
2934:
2899:
2870:
2850:
2640:
2598:
2515:
2489:
2427:
2407:
2375:
2335:
2315:
2288:
2262:
2235:
2206:
2164:
2144:
2124:
2104:
2084:
2064:
2038:
2018:
1998:
1978:
1845:
1724:
1665:
1600:
1587:, constructed using
1563:
1539:
1519:
1499:
1479:
1443:
1417:
1397:
1367:
1331:
1256:
1226:
1202:
1182:
1112:
1069:
1049:
1019:
955:
917:
891:
865:
839:
813:
793:
773:
735:
665:
634:
585:
553:
542:{\displaystyle \to }
533:
513:
493:
467:
440:
420:
401:{\displaystyle \to }
392:
366:
337:
311:
291:
271:
251:
231:
211:
174:{\displaystyle \to }
165:
79:{\displaystyle \to }
70:
56:typed interpretation
27:
8519:Stephen Cole Kleene
8474:C. Anthony Anderson
7663:Lambek, J. (1986).
7506:1934PNAS...20..584C
7390:on 12 January 2019.
7069:Church 1940, p.60:
6698:typically ambiguous
4661:is a term (of type
4579:equivalence classes
2835:(the S-combinator).
1393:, meaning variable
1325:typing environments
460:). Informally, the
191:the logistic method
8549:Hartley Rogers, Jr
8514:John George Kemeny
8272:10.1007/BFb0037110
8198:10.1007/BF02023009
8172:
8149:
8114:10.1007/BFb0064870
8071:10.1007/BF02276799
7294:
7258:
7230:typing environment
7218:
7158:
7048:
6923:
6721:
6686:
6663:
6628:
6590:
6559:
6502:
6464:
6425:
6398:
6368:or adding general
6358:
6320:
6283:
6185:
6165:
6129:
6109:
6086:
6066:
6046:
6014:
5994:
5954:
5934:
5907:
5881:
5851:
5831:
5811:
5781:
5755:
5717:
5697:
5677:
5634:
5562:
5504:
5392:
5300:
5248:
5184:
5164:
5144:
5124:
5092:
5056:
5036:
5016:
4996:
4964:
4913:
4887:
4835:
4789:
4705:linear type system
4671:
4647:
4623:
4567:
4524:
4484:
4365:
4286:
4204:{\displaystyle ()}
4201:
4174:
4147:
4094:
4041:
3991:
3965:
3933:
3903:
3883:. Given two terms
3834:
3763:
3743:
3723:
3681:
3616:
3580:
3528:
3505:
3383:
3347:
3292:
3235:
3176:
3110:
3054:
3004:
2963:
2920:
2895:. For base types,
2885:
2856:
2825:
2626:
2581:
2501:
2468:
2413:
2381:
2361:
2321:
2301:
2274:
2248:
2218:
2192:
2150:
2130:
2110:
2090:
2070:
2044:
2024:
2004:
1984:
1954:
1829:
1706:
1649:
1569:
1545:
1525:
1505:
1495:is a term of type
1485:
1465:
1423:
1403:
1383:
1349:
1293:
1232:
1208:
1188:
1165:
1091:variable reference
1075:
1055:
1035:
991:
941:
903:
877:
851:
825:
799:
779:
759:
717:
640:
609:
571:
539:
519:
499:
479:
446:
426:
398:
378:
352:
323:
297:
277:
257:
237:
217:
171:
76:
40:
8619:
8618:
8554:J. Barkley Rosser
8318:978-94-010-3891-1
8123:978-3-540-07155-6
7686:978-3-540-47253-7
7456:Pfenning, Frank,
7186:Church 1940, p.57
6902:
6871:
6849:
6412:. As a corollary
6383:Important results
6276:
6270:
6249:
6243:
6112:{\displaystyle e}
6049:{\displaystyle e}
6004:synthesizes type
5983:
5891:synthesizes type
5834:{\displaystyle e}
5751:
5720:{\displaystyle x}
5647:
5646:
5632:
5560:
5502:
5484:
5390:
5373:
5298:
5275:
5246:
5167:{\displaystyle e}
5039:{\displaystyle e}
4785:
4729:natural deduction
3846:internal language
3766:{\displaystyle t}
3746:{\displaystyle x}
3660:
3518:holds in context
3466:
3423:equational theory
3417:Equational theory
3379:
3343:
3288:
3231:
3172:
2962:
2841:combinatory logic
2480:identity function
2350:
2188:
2153:{\displaystyle x}
2113:{\displaystyle e}
2073:{\displaystyle x}
2027:{\displaystyle x}
1987:{\displaystyle x}
1968:
1967:
1952:
1930:
1827:
1797:
1704:
1677:
1647:
1585:typing derivation
1581:typing judgements
1548:{\displaystyle e}
1488:{\displaystyle e}
1406:{\displaystyle x}
1361:typing assumption
1235:{\displaystyle x}
1211:{\displaystyle x}
1191:{\displaystyle c}
1058:{\displaystyle x}
802:{\displaystyle b}
782:{\displaystyle a}
643:{\displaystyle B}
529:. By convention,
300:{\displaystyle o}
260:{\displaystyle o}
220:{\displaystyle o}
204:interpretations.
147:Logical Framework
135:polymorphic types
8649:
8569:Raymond Smullyan
8544:Nicholas Rescher
8539:Michael O. Rabin
8405:
8398:
8391:
8382:
8381:
8366:
8323:
8322:
8292:
8286:
8285:
8255:
8249:
8248:
8246:
8244:
8238:
8224:
8218:
8217:
8181:
8179:
8178:
8173:
8158:
8156:
8155:
8150:
8134:
8128:
8127:
8106:Logic Colloquium
8097:
8091:
8090:
8048:
8042:
8041:
8023:
8001:
7995:
7994:
7966:
7960:
7959:
7949:
7925:
7919:
7918:
7885:
7879:
7878:
7838:
7832:
7831:
7821:
7811:
7785:
7779:
7778:
7750:
7744:
7743:
7733:
7723:
7697:
7691:
7690:
7660:
7654:
7653:
7602:
7591:
7585:
7579:
7578:
7566:
7553:
7547:
7545:
7535:
7517:
7484:Curry, Haskell B
7480:
7474:
7473:
7472:
7470:
7464:
7453:
7447:
7441:
7435:
7429:
7420:
7413:
7404:
7398:
7392:
7391:
7389:
7383:. Archived from
7348:
7336:
7305:
7303:
7301:
7300:
7295:
7293:
7292:
7275:
7269:
7267:
7265:
7264:
7259:
7257:
7256:
7239:
7233:
7227:
7225:
7224:
7219:
7202:
7196:
7193:
7187:
7184:
7178:
7175:
7169:
7167:
7165:
7164:
7159:
7157:
7156:
7132:
7131:
7107:
7106:
7088:
7087:
7067:
7058:
7057:
7055:
7054:
7049:
7047:
7046:
7022:
7021:
6997:
6996:
6978:
6977:
6939:
6933:
6932:
6930:
6929:
6924:
6910:
6909:
6904:
6903:
6895:
6879:
6878:
6873:
6872:
6864:
6857:
6856:
6851:
6850:
6842:
6826:
6825:
6804:
6803:
6791:
6790:
6773:
6764:
6754:
6730:
6728:
6727:
6722:
6695:
6693:
6692:
6687:
6672:
6670:
6669:
6664:
6637:
6635:
6634:
6629:
6627:
6626:
6599:
6597:
6596:
6591:
6589:
6588:
6568:
6566:
6565:
6560:
6511:
6509:
6508:
6503:
6473:
6471:
6470:
6465:
6463:
6462:
6457:
6456:
6435:-equivalence is
6434:
6432:
6431:
6426:
6407:
6405:
6404:
6399:
6367:
6365:
6364:
6359:
6329:
6327:
6326:
6321:
6319:
6318:
6313:
6312:
6292:
6290:
6289:
6284:
6274:
6268:
6247:
6241:
6194:
6192:
6191:
6186:
6174:
6172:
6171:
6166:
6158:
6157:
6138:
6136:
6135:
6130:
6118:
6116:
6115:
6110:
6095:
6093:
6092:
6087:
6075:
6073:
6072:
6067:
6055:
6053:
6052:
6047:
6023:
6021:
6020:
6015:
6003:
6001:
6000:
5995:
5993:
5992:
5981:
5980:
5979:
5963:
5961:
5960:
5955:
5943:
5941:
5940:
5935:
5933:
5932:
5916:
5914:
5913:
5908:
5890:
5888:
5887:
5882:
5880:
5879:
5860:
5858:
5857:
5852:
5840:
5838:
5837:
5832:
5820:
5818:
5817:
5812:
5807:
5806:
5790:
5788:
5787:
5782:
5764:
5762:
5761:
5756:
5749:
5726:
5724:
5723:
5718:
5706:
5704:
5703:
5698:
5686:
5684:
5683:
5678:
5673:
5672:
5643:
5641:
5640:
5635:
5633:
5631:
5618:
5617:
5598:
5581:
5571:
5569:
5568:
5563:
5561:
5559:
5542:
5525:
5513:
5511:
5510:
5505:
5503:
5501:
5494:
5493:
5482:
5481:
5480:
5464:
5457:
5456:
5428:
5427:
5411:
5401:
5399:
5398:
5393:
5391:
5389:
5371:
5354:
5338:
5337:
5321:
5309:
5307:
5306:
5301:
5299:
5297:
5280:
5276:
5273:
5267:
5257:
5255:
5254:
5249:
5247:
5245:
5228:
5218:
5217:
5207:
5197:
5193:
5191:
5190:
5185:
5173:
5171:
5170:
5165:
5153:
5151:
5150:
5145:
5133:
5131:
5130:
5125:
5101:
5099:
5098:
5093:
5065:
5063:
5062:
5057:
5045:
5043:
5042:
5037:
5025:
5023:
5022:
5017:
5005:
5003:
5002:
4997:
4973:
4971:
4970:
4965:
4922:
4920:
4919:
4914:
4896:
4894:
4893:
4888:
4886:
4885:
4867:
4866:
4844:
4842:
4841:
4836:
4834:
4833:
4818:
4817:
4798:
4796:
4795:
4790:
4783:
4735:are exactly the
4680:
4678:
4677:
4672:
4656:
4654:
4653:
4648:
4632:
4630:
4629:
4624:
4616:
4615:
4600:
4599:
4576:
4574:
4573:
4568:
4533:
4531:
4530:
4525:
4511:
4510:
4493:
4491:
4490:
4485:
4474:
4473:
4446:
4445:
4433:
4432:
4408:
4407:
4395:
4394:
4374:
4372:
4371:
4366:
4361:
4360:
4342:
4341:
4326:
4325:
4313:
4312:
4295:
4293:
4292:
4287:
4282:
4281:
4263:
4262:
4247:
4246:
4234:
4233:
4210:
4208:
4207:
4202:
4183:
4181:
4180:
4175:
4173:
4172:
4156:
4154:
4153:
4148:
4146:
4145:
4136:
4135:
4120:
4119:
4103:
4101:
4100:
4095:
4093:
4092:
4083:
4082:
4067:
4066:
4050:
4048:
4047:
4042:
4040:
4039:
4027:
4026:
4017:
4016:
4000:
3998:
3997:
3992:
3974:
3972:
3971:
3966:
3942:
3940:
3939:
3934:
3929:
3928:
3912:
3910:
3909:
3904:
3899:
3898:
3843:
3841:
3840:
3835:
3772:
3770:
3769:
3764:
3752:
3750:
3749:
3744:
3732:
3730:
3729:
3724:
3690:
3688:
3687:
3682:
3677:
3676:
3658:
3651:
3650:
3625:
3623:
3622:
3617:
3612:
3611:
3589:
3587:
3586:
3581:
3576:
3575:
3560:
3559:
3537:
3535:
3534:
3529:
3514:
3512:
3511:
3506:
3486:
3485:
3464:
3457:
3456:
3392:
3390:
3389:
3384:
3377:
3356:
3354:
3353:
3348:
3341:
3337:
3336:
3321:
3320:
3301:
3299:
3298:
3293:
3286:
3282:
3281:
3269:
3268:
3244:
3242:
3241:
3236:
3229:
3225:
3224:
3209:
3208:
3185:
3183:
3182:
3177:
3170:
3166:
3165:
3153:
3152:
3119:
3117:
3116:
3111:
3063:
3061:
3060:
3055:
3013:
3011:
3010:
3005:
2964:
2960:
2929:
2927:
2926:
2921:
2894:
2892:
2891:
2886:
2865:
2863:
2862:
2857:
2834:
2832:
2831:
2826:
2824:
2804:
2781:
2770:
2726:
2725:
2710:
2696:
2695:
2680:
2669:
2655:
2654:
2635:
2633:
2632:
2627:
2625:
2614:
2590:
2588:
2587:
2582:
2565:
2564:
2549:
2548:
2530:
2529:
2510:
2508:
2507:
2502:
2477:
2475:
2474:
2469:
2458:
2457:
2442:
2441:
2422:
2420:
2419:
2414:
2390:
2388:
2387:
2382:
2370:
2368:
2367:
2362:
2360:
2359:
2348:
2347:
2346:
2330:
2328:
2327:
2322:
2310:
2308:
2307:
2302:
2300:
2299:
2283:
2281:
2280:
2275:
2257:
2255:
2254:
2249:
2247:
2246:
2227:
2225:
2224:
2219:
2201:
2199:
2198:
2193:
2186:
2179:
2178:
2159:
2157:
2156:
2151:
2139:
2137:
2136:
2131:
2119:
2117:
2116:
2111:
2099:
2097:
2096:
2091:
2079:
2077:
2076:
2071:
2053:
2051:
2050:
2045:
2033:
2031:
2030:
2025:
2013:
2011:
2010:
2005:
1993:
1991:
1990:
1985:
1963:
1961:
1960:
1955:
1953:
1951:
1947:
1946:
1940:
1939:
1928:
1927:
1926:
1910:
1906:
1905:
1899:
1898:
1873:
1872:
1866:
1865:
1849:
1838:
1836:
1835:
1830:
1828:
1826:
1810:
1809:
1795:
1788:
1787:
1765:
1761:
1760:
1745:
1744:
1728:
1715:
1713:
1712:
1707:
1705:
1703:
1699:
1698:
1682:
1678:
1675:
1669:
1658:
1656:
1655:
1650:
1648:
1646:
1642:
1641:
1625:
1615:
1614:
1604:
1594:
1578:
1576:
1575:
1570:
1554:
1552:
1551:
1546:
1535:. In this case
1534:
1532:
1531:
1526:
1514:
1512:
1511:
1506:
1494:
1492:
1491:
1486:
1474:
1472:
1471:
1466:
1461:
1460:
1432:
1430:
1429:
1424:
1412:
1410:
1409:
1404:
1392:
1390:
1389:
1384:
1379:
1378:
1358:
1356:
1355:
1350:
1302:
1300:
1299:
1294:
1241:
1239:
1238:
1233:
1217:
1215:
1214:
1209:
1197:
1195:
1194:
1189:
1174:
1172:
1171:
1166:
1139:
1138:
1087:Backus–Naur form
1084:
1082:
1081:
1076:
1064:
1062:
1061:
1056:
1044:
1042:
1041:
1036:
1031:
1030:
1011:
1000:
998:
997:
992:
950:
948:
947:
942:
912:
910:
909:
904:
886:
884:
883:
878:
860:
858:
857:
852:
834:
832:
831:
826:
808:
806:
805:
800:
788:
786:
785:
780:
768:
766:
765:
760:
726:
724:
723:
718:
706:
649:
647:
646:
641:
618:
616:
615:
610:
580:
578:
577:
572:
548:
546:
545:
540:
528:
526:
525:
520:
508:
506:
505:
500:
488:
486:
485:
480:
455:
453:
452:
447:
435:
433:
432:
427:
407:
405:
404:
399:
387:
385:
384:
379:
361:
359:
358:
353:
332:
330:
329:
324:
306:
304:
303:
298:
286:
284:
283:
278:
266:
264:
263:
258:
246:
244:
243:
238:
226:
224:
223:
218:
180:
178:
177:
172:
159:Church encodings
85:
83:
82:
77:
64:type constructor
49:
47:
46:
41:
39:
38:
8657:
8656:
8652:
8651:
8650:
8648:
8647:
8646:
8632:Lambda calculus
8622:
8621:
8620:
8615:
8594:
8573:
8524:Simon B. Kochen
8457:
8441:Church encoding
8426:Lambda calculus
8414:
8409:
8357:
8332:
8327:
8326:
8319:
8293:
8289:
8282:
8256:
8252:
8242:
8240:
8236:
8225:
8221:
8164:
8161:
8160:
8144:
8141:
8140:
8135:
8131:
8124:
8098:
8094:
8049:
8045:
8002:
7998:
7967:
7963:
7926:
7922:
7889:Huet, GĂ©rard P.
7886:
7882:
7867:
7839:
7835:
7786:
7782:
7751:
7747:
7698:
7694:
7687:
7661:
7657:
7626:10.2307/2271658
7608:(August 1967).
7603:
7594:
7586:
7582:
7575:
7554:
7550:
7481:
7477:
7468:
7466:
7462:
7454:
7450:
7442:
7438:
7430:
7423:
7414:
7407:
7400:Church, Alonzo
7399:
7395:
7387:
7365:10.2307/2266170
7346:
7337:
7314:
7309:
7308:
7288:
7284:
7282:
7279:
7278:
7276:
7272:
7252:
7248:
7246:
7243:
7242:
7240:
7236:
7213:
7210:
7209:
7203:
7199:
7194:
7190:
7185:
7181:
7176:
7172:
7140:
7136:
7115:
7111:
7096:
7092:
7080:
7076:
7074:
7071:
7070:
7068:
7061:
7030:
7026:
7005:
7001:
6986:
6982:
6970:
6966:
6946:
6943:
6942:
6940:
6936:
6905:
6894:
6893:
6892:
6874:
6863:
6862:
6861:
6852:
6841:
6840:
6839:
6821:
6817:
6799:
6795:
6786:
6782:
6780:
6777:
6776:
6774:
6767:
6755:
6751:
6746:
6713:
6710:
6709:
6678:
6675:
6674:
6655:
6652:
6651:
6622:
6618:
6616:
6613:
6612:
6584:
6580:
6578:
6575:
6574:
6571:Church numerals
6524:
6521:
6520:
6517:natural numbers
6494:
6491:
6490:
6458:
6452:
6451:
6450:
6448:
6445:
6444:
6417:
6414:
6413:
6393:
6390:
6389:
6385:
6377:Turing complete
6370:recursive types
6335:
6332:
6331:
6314:
6302:
6301:
6300:
6298:
6295:
6294:
6221:
6218:
6217:
6206:
6180:
6177:
6176:
6153:
6152:
6144:
6141:
6140:
6124:
6121:
6120:
6104:
6101:
6100:
6081:
6078:
6077:
6061:
6058:
6057:
6041:
6038:
6037:
6009:
6006:
6005:
5988:
5984:
5975:
5971:
5969:
5966:
5965:
5949:
5946:
5945:
5928:
5924:
5922:
5919:
5918:
5896:
5893:
5892:
5875:
5871:
5869:
5866:
5865:
5846:
5843:
5842:
5826:
5823:
5822:
5821:and check that
5802:
5801:
5796:
5793:
5792:
5770:
5767:
5766:
5738:
5735:
5734:
5712:
5709:
5708:
5692:
5689:
5688:
5668:
5667:
5662:
5659:
5658:
5613:
5612:
5599:
5582:
5580:
5578:
5575:
5574:
5543:
5526:
5524:
5522:
5519:
5518:
5489:
5485:
5476:
5472:
5465:
5452:
5448:
5423:
5419:
5412:
5410:
5408:
5405:
5404:
5355:
5333:
5332:
5322:
5320:
5318:
5315:
5314:
5281:
5272:
5268:
5266:
5264:
5261:
5260:
5229:
5213:
5212:
5208:
5206:
5204:
5201:
5200:
5179:
5176:
5175:
5159:
5156:
5155:
5139:
5136:
5135:
5107:
5104:
5103:
5075:
5072:
5071:
5051:
5048:
5047:
5031:
5028:
5027:
5011:
5008:
5007:
4979:
4976:
4975:
4947:
4944:
4943:
4902:
4899:
4898:
4872:
4871:
4853:
4852:
4850:
4847:
4846:
4823:
4822:
4807:
4806:
4804:
4801:
4800:
4772:
4769:
4768:
4756:
4739:of this logic.
4733:inhabited types
4713:
4666:
4663:
4662:
4642:
4639:
4638:
4611:
4610:
4595:
4594:
4586:
4583:
4582:
4556:
4553:
4552:
4506:
4505:
4500:
4497:
4496:
4469:
4468:
4441:
4440:
4428:
4424:
4403:
4402:
4390:
4386:
4381:
4378:
4377:
4356:
4355:
4337:
4336:
4321:
4320:
4308:
4304:
4302:
4299:
4298:
4277:
4276:
4258:
4257:
4242:
4241:
4229:
4225:
4223:
4220:
4219:
4193:
4190:
4189:
4168:
4164:
4162:
4159:
4158:
4141:
4137:
4131:
4130:
4115:
4111:
4109:
4106:
4105:
4088:
4084:
4078:
4077:
4062:
4058:
4056:
4053:
4052:
4035:
4031:
4022:
4018:
4012:
4011:
4006:
4003:
4002:
3980:
3977:
3976:
3948:
3945:
3944:
3924:
3923:
3918:
3915:
3914:
3894:
3893:
3888:
3885:
3884:
3826:
3823:
3822:
3819:
3811:described below
3783:
3758:
3755:
3754:
3738:
3735:
3734:
3699:
3696:
3695:
3694:holds whenever
3672:
3668:
3646:
3645:
3637:
3634:
3633:
3607:
3606:
3595:
3592:
3591:
3571:
3570:
3555:
3554:
3543:
3540:
3539:
3523:
3520:
3519:
3481:
3477:
3452:
3451:
3440:
3437:
3436:
3419:
3366:
3363:
3362:
3323:
3322:
3316:
3315:
3307:
3304:
3303:
3271:
3270:
3264:
3263:
3255:
3252:
3251:
3211:
3210:
3204:
3203:
3195:
3192:
3191:
3155:
3154:
3148:
3147:
3139:
3136:
3135:
3131:
3126:
3072:
3069:
3068:
3022:
3019:
3018:
2958:
2935:
2932:
2931:
2900:
2897:
2896:
2871:
2868:
2867:
2851:
2848:
2847:
2817:
2797:
2774:
2763:
2721:
2720:
2703:
2691:
2690:
2673:
2662:
2650:
2649:
2641:
2638:
2637:
2618:
2607:
2599:
2596:
2595:
2560:
2559:
2544:
2543:
2525:
2524:
2516:
2513:
2512:
2490:
2487:
2486:
2482:/I-combinator),
2453:
2452:
2437:
2436:
2428:
2425:
2424:
2408:
2405:
2404:
2403:For every type
2376:
2373:
2372:
2355:
2351:
2342:
2338:
2336:
2333:
2332:
2316:
2313:
2312:
2295:
2291:
2289:
2286:
2285:
2263:
2260:
2259:
2242:
2238:
2236:
2233:
2232:
2207:
2204:
2203:
2174:
2173:
2165:
2162:
2161:
2145:
2142:
2141:
2125:
2122:
2121:
2105:
2102:
2101:
2085:
2082:
2081:
2065:
2062:
2061:
2039:
2036:
2035:
2019:
2016:
2015:
1999:
1996:
1995:
1979:
1976:
1975:
1942:
1941:
1935:
1931:
1922:
1918:
1911:
1901:
1900:
1894:
1890:
1868:
1867:
1861:
1857:
1850:
1848:
1846:
1843:
1842:
1805:
1804:
1783:
1782:
1766:
1756:
1755:
1740:
1739:
1729:
1727:
1725:
1722:
1721:
1694:
1693:
1683:
1674:
1670:
1668:
1666:
1663:
1662:
1637:
1636:
1626:
1610:
1609:
1605:
1603:
1601:
1598:
1597:
1564:
1561:
1560:
1540:
1537:
1536:
1520:
1517:
1516:
1500:
1497:
1496:
1480:
1477:
1476:
1475:indicates that
1456:
1455:
1444:
1441:
1440:
1438:typing relation
1418:
1415:
1414:
1398:
1395:
1394:
1374:
1373:
1368:
1365:
1364:
1332:
1329:
1328:
1320:typing contexts
1316:
1257:
1254:
1253:
1227:
1224:
1223:
1203:
1200:
1199:
1183:
1180:
1179:
1134:
1133:
1113:
1110:
1109:
1070:
1067:
1066:
1050:
1047:
1046:
1026:
1025:
1020:
1017:
1016:
1009:
956:
953:
952:
918:
915:
914:
892:
889:
888:
866:
863:
862:
840:
837:
836:
814:
811:
810:
794:
791:
790:
774:
771:
770:
736:
733:
732:
690:
666:
663:
662:
635:
632:
631:
586:
583:
582:
554:
551:
550:
534:
531:
530:
514:
511:
510:
494:
491:
490:
468:
465:
464:
441:
438:
437:
421:
418:
417:
393:
390:
389:
367:
364:
363:
338:
335:
334:
312:
309:
308:
292:
289:
288:
272:
269:
268:
252:
249:
248:
232:
229:
228:
212:
209:
208:
195:lambda calculus
187:
166:
163:
162:
143:dependent types
125:) or even full
119:natural numbers
71:
68:
67:
60:lambda calculus
34:
30:
28:
25:
24:
17:
12:
11:
5:
8655:
8645:
8644:
8639:
8634:
8617:
8616:
8614:
8613:
8608:
8602:
8600:
8596:
8595:
8593:
8592:
8587:
8581:
8579:
8575:
8574:
8572:
8571:
8566:
8564:Norman Shapiro
8561:
8556:
8551:
8546:
8541:
8536:
8531:
8529:Maurice L'Abbé
8526:
8521:
8516:
8511:
8506:
8501:
8499:William Easton
8496:
8491:
8486:
8481:
8476:
8471:
8465:
8463:
8459:
8458:
8456:
8455:
8450:
8445:
8444:
8443:
8438:
8433:
8422:
8420:
8416:
8415:
8408:
8407:
8400:
8393:
8385:
8379:
8378:
8372:entry in the
8367:
8356:
8355:External links
8353:
8352:
8351:
8331:
8328:
8325:
8324:
8317:
8287:
8280:
8250:
8219:
8171:
8168:
8148:
8129:
8122:
8092:
8065:(3): 113–114.
8043:
7996:
7977:(2): 225–230.
7961:
7940:(2): 170–178.
7920:
7901:(3): 257–267.
7880:
7865:
7833:
7780:
7761:(2): 387–394.
7745:
7692:
7685:
7655:
7620:(2): 198–212.
7592:
7587:Norman Ramsey
7580:
7573:
7557:Reynolds, John
7548:
7500:(11): 584–90.
7486:(1934-09-20).
7475:
7448:
7436:
7421:
7405:
7393:
7340:Church, Alonzo
7311:
7310:
7307:
7306:
7291:
7287:
7270:
7255:
7251:
7234:
7217:
7197:
7188:
7179:
7170:
7155:
7152:
7149:
7146:
7143:
7139:
7135:
7130:
7127:
7124:
7121:
7118:
7114:
7110:
7105:
7102:
7099:
7095:
7091:
7086:
7083:
7079:
7059:
7045:
7042:
7039:
7036:
7033:
7029:
7025:
7020:
7017:
7014:
7011:
7008:
7004:
7000:
6995:
6992:
6989:
6985:
6981:
6976:
6973:
6969:
6965:
6962:
6959:
6956:
6953:
6950:
6934:
6922:
6919:
6916:
6913:
6908:
6901:
6898:
6891:
6888:
6885:
6882:
6877:
6870:
6867:
6860:
6855:
6848:
6845:
6838:
6835:
6832:
6829:
6824:
6820:
6816:
6813:
6810:
6807:
6802:
6798:
6794:
6789:
6785:
6765:
6748:
6747:
6745:
6742:
6741:
6740:
6732:
6720:
6717:
6685:
6682:
6662:
6659:
6644:function space
6625:
6621:
6605:
6587:
6583:
6558:
6555:
6552:
6549:
6546:
6543:
6540:
6537:
6534:
6531:
6528:
6515:We can encode
6513:
6501:
6498:
6483:
6461:
6455:
6424:
6421:
6408:-reduction is
6397:
6384:
6381:
6357:
6354:
6351:
6348:
6345:
6342:
6339:
6317:
6311:
6308:
6305:
6282:
6279:
6273:
6267:
6264:
6261:
6258:
6255:
6252:
6246:
6240:
6237:
6234:
6231:
6228:
6225:
6205:
6202:
6197:
6196:
6184:
6164:
6161:
6156:
6151:
6148:
6128:
6108:
6097:
6085:
6065:
6045:
6036:To check that
6026:
6025:
6013:
5991:
5987:
5978:
5974:
5953:
5931:
5927:
5906:
5903:
5900:
5878:
5874:
5862:
5850:
5830:
5810:
5805:
5800:
5780:
5777:
5774:
5754:
5748:
5745:
5742:
5733:To check that
5731:
5728:
5716:
5696:
5676:
5671:
5666:
5645:
5644:
5630:
5627:
5624:
5621:
5616:
5611:
5608:
5605:
5602:
5597:
5594:
5591:
5588:
5585:
5572:
5558:
5555:
5552:
5549:
5546:
5541:
5538:
5535:
5532:
5529:
5515:
5514:
5500:
5497:
5492:
5488:
5479:
5475:
5471:
5468:
5463:
5460:
5455:
5451:
5447:
5444:
5440:
5437:
5434:
5431:
5426:
5422:
5418:
5415:
5402:
5388:
5385:
5382:
5379:
5376:
5370:
5367:
5364:
5361:
5358:
5353:
5350:
5347:
5344:
5341:
5336:
5331:
5328:
5325:
5311:
5310:
5296:
5293:
5290:
5287:
5284:
5279:
5271:
5258:
5244:
5241:
5238:
5235:
5232:
5227:
5224:
5221:
5216:
5211:
5183:
5163:
5143:
5123:
5120:
5117:
5114:
5111:
5091:
5088:
5085:
5082:
5079:
5055:
5035:
5015:
4995:
4992:
4989:
4986:
4983:
4963:
4960:
4957:
4954:
4951:
4912:
4909:
4906:
4884:
4881:
4878:
4875:
4870:
4865:
4862:
4859:
4856:
4832:
4829:
4826:
4821:
4816:
4813:
4810:
4788:
4782:
4779:
4776:
4765:principal type
4755:
4752:
4712:
4709:
4670:
4646:
4622:
4619:
4614:
4609:
4606:
4603:
4598:
4593:
4590:
4566:
4563:
4560:
4535:
4534:
4523:
4520:
4517:
4514:
4509:
4504:
4494:
4483:
4480:
4477:
4472:
4467:
4464:
4461:
4458:
4455:
4452:
4449:
4444:
4439:
4436:
4431:
4427:
4423:
4420:
4417:
4414:
4411:
4406:
4401:
4398:
4393:
4389:
4385:
4375:
4364:
4359:
4354:
4351:
4348:
4345:
4340:
4335:
4332:
4329:
4324:
4319:
4316:
4311:
4307:
4296:
4285:
4280:
4275:
4272:
4269:
4266:
4261:
4256:
4253:
4250:
4245:
4240:
4237:
4232:
4228:
4200:
4197:
4171:
4167:
4144:
4140:
4134:
4129:
4126:
4123:
4118:
4114:
4091:
4087:
4081:
4076:
4073:
4070:
4065:
4061:
4038:
4034:
4030:
4025:
4021:
4015:
4010:
3990:
3987:
3984:
3964:
3961:
3958:
3955:
3952:
3932:
3927:
3922:
3902:
3897:
3892:
3854:Joachim Lambek
3833:
3830:
3818:
3815:
3785:Likewise, the
3782:
3779:
3762:
3742:
3722:
3719:
3716:
3713:
3709:
3706:
3703:
3692:
3691:
3680:
3675:
3671:
3667:
3663:
3657:
3654:
3649:
3644:
3641:
3615:
3610:
3605:
3602:
3599:
3579:
3574:
3569:
3566:
3563:
3558:
3553:
3550:
3547:
3527:
3516:
3515:
3504:
3501:
3498:
3495:
3492:
3489:
3484:
3480:
3476:
3472:
3469:
3463:
3460:
3455:
3450:
3447:
3444:
3431:beta reduction
3418:
3415:
3411:type inference
3382:
3376:
3373:
3370:
3346:
3340:
3335:
3332:
3329:
3326:
3319:
3314:
3311:
3291:
3285:
3280:
3277:
3274:
3267:
3262:
3259:
3234:
3228:
3223:
3220:
3217:
3214:
3207:
3202:
3199:
3175:
3169:
3164:
3161:
3158:
3151:
3146:
3143:
3130:
3127:
3125:
3122:
3121:
3120:
3109:
3106:
3103:
3100:
3097:
3094:
3091:
3088:
3085:
3082:
3079:
3076:
3065:
3064:
3053:
3050:
3047:
3044:
3041:
3038:
3035:
3032:
3029:
3026:
3003:
3000:
2997:
2994:
2991:
2988:
2985:
2982:
2979:
2976:
2973:
2970:
2967:
2957:
2954:
2951:
2948:
2945:
2942:
2939:
2919:
2916:
2913:
2910:
2907:
2904:
2884:
2881:
2878:
2875:
2855:
2837:
2836:
2823:
2820:
2816:
2813:
2810:
2807:
2803:
2800:
2796:
2793:
2790:
2787:
2784:
2780:
2777:
2773:
2769:
2766:
2762:
2759:
2756:
2753:
2750:
2747:
2744:
2741:
2738:
2735:
2732:
2729:
2724:
2719:
2716:
2713:
2709:
2706:
2702:
2699:
2694:
2689:
2686:
2683:
2679:
2676:
2672:
2668:
2665:
2661:
2658:
2653:
2648:
2645:
2624:
2621:
2617:
2613:
2610:
2606:
2603:
2592:
2580:
2577:
2574:
2571:
2568:
2563:
2558:
2555:
2552:
2547:
2542:
2539:
2536:
2533:
2528:
2523:
2520:
2500:
2497:
2494:
2483:
2467:
2464:
2461:
2456:
2451:
2448:
2445:
2440:
2435:
2432:
2412:
2393:
2392:
2380:
2358:
2354:
2345:
2341:
2320:
2298:
2294:
2273:
2270:
2267:
2245:
2241:
2229:
2217:
2214:
2211:
2191:
2185:
2182:
2177:
2172:
2169:
2149:
2129:
2109:
2089:
2069:
2058:
2055:
2043:
2023:
2003:
1983:
1966:
1965:
1950:
1945:
1938:
1934:
1925:
1921:
1917:
1914:
1909:
1904:
1897:
1893:
1889:
1886:
1882:
1879:
1876:
1871:
1864:
1860:
1856:
1853:
1840:
1825:
1822:
1819:
1816:
1813:
1808:
1803:
1800:
1794:
1791:
1786:
1781:
1778:
1775:
1772:
1769:
1764:
1759:
1754:
1751:
1748:
1743:
1738:
1735:
1732:
1718:
1717:
1702:
1697:
1692:
1689:
1686:
1681:
1673:
1660:
1645:
1640:
1635:
1632:
1629:
1624:
1621:
1618:
1613:
1608:
1568:
1555:is said to be
1544:
1524:
1504:
1484:
1464:
1459:
1454:
1451:
1448:
1422:
1402:
1382:
1377:
1372:
1348:
1345:
1342:
1339:
1336:
1315:
1312:
1304:
1303:
1292:
1288:
1285:
1282:
1279:
1276:
1273:
1270:
1267:
1264:
1261:
1231:
1207:
1187:
1176:
1175:
1164:
1161:
1158:
1154:
1151:
1148:
1145:
1142:
1137:
1132:
1129:
1126:
1123:
1120:
1117:
1074:
1054:
1034:
1029:
1024:
1006:term constants
990:
987:
984:
981:
978:
975:
972:
969:
966:
963:
960:
940:
937:
934:
931:
928:
925:
922:
902:
899:
896:
876:
873:
870:
850:
847:
844:
824:
821:
818:
798:
778:
758:
755:
752:
749:
746:
743:
740:
729:
728:
716:
713:
710:
705:
702:
699:
696:
693:
688:
685:
682:
679:
676:
673:
670:
656:type constants
639:
608:
605:
602:
599:
596:
593:
590:
570:
567:
564:
561:
558:
538:
518:
498:
478:
475:
472:
445:
425:
397:
377:
374:
371:
351:
348:
345:
342:
322:
319:
316:
296:
276:
256:
236:
216:
186:
183:
170:
88:function types
86:) that builds
75:
62:with only one
37:
33:
15:
9:
6:
4:
3:
2:
8654:
8643:
8640:
8638:
8635:
8633:
8630:
8629:
8627:
8612:
8609:
8607:
8604:
8603:
8601:
8597:
8591:
8588:
8586:
8583:
8582:
8580:
8576:
8570:
8567:
8565:
8562:
8560:
8557:
8555:
8552:
8550:
8547:
8545:
8542:
8540:
8537:
8535:
8532:
8530:
8527:
8525:
8522:
8520:
8517:
8515:
8512:
8510:
8507:
8505:
8504:Alfred Foster
8502:
8500:
8497:
8495:
8492:
8490:
8489:William Boone
8487:
8485:
8482:
8480:
8479:Peter Andrews
8477:
8475:
8472:
8470:
8467:
8466:
8464:
8460:
8454:
8451:
8449:
8446:
8442:
8439:
8437:
8434:
8432:
8429:
8428:
8427:
8424:
8423:
8421:
8419:Notable ideas
8417:
8413:
8412:Alonzo Church
8406:
8401:
8399:
8394:
8392:
8387:
8386:
8383:
8377:
8376:
8371:
8368:
8364:
8359:
8358:
8349:
8348:0-19-853761-1
8345:
8341:
8337:
8336:H. Barendregt
8334:
8333:
8320:
8314:
8310:
8306:
8302:
8298:
8291:
8283:
8281:3-540-56517-5
8277:
8273:
8269:
8265:
8261:
8254:
8235:
8234:
8229:
8228:Plotkin, G.D.
8223:
8215:
8211:
8207:
8203:
8199:
8195:
8191:
8187:
8183:
8169:
8166:
8146:
8133:
8125:
8119:
8115:
8111:
8107:
8103:
8096:
8088:
8084:
8080:
8076:
8072:
8068:
8064:
8061:(in German).
8060:
8059:
8054:
8047:
8039:
8035:
8031:
8027:
8022:
8017:
8013:
8009:
8008:
8000:
7992:
7988:
7984:
7980:
7976:
7972:
7965:
7957:
7953:
7948:
7943:
7939:
7935:
7931:
7924:
7916:
7912:
7908:
7904:
7900:
7896:
7895:
7890:
7884:
7876:
7872:
7868:
7866:0-8186-2230-X
7862:
7858:
7854:
7850:
7849:
7844:
7837:
7829:
7825:
7820:
7819:2027.42/23535
7815:
7810:
7805:
7801:
7797:
7796:
7791:
7784:
7776:
7772:
7768:
7764:
7760:
7756:
7749:
7741:
7737:
7732:
7731:2027.42/23535
7727:
7722:
7717:
7713:
7709:
7708:
7703:
7696:
7688:
7682:
7678:
7674:
7670:
7666:
7659:
7651:
7647:
7643:
7639:
7635:
7631:
7627:
7623:
7619:
7615:
7611:
7607:
7601:
7599:
7597:
7590:
7584:
7576:
7574:9780521594141
7570:
7565:
7564:
7558:
7552:
7543:
7539:
7534:
7529:
7525:
7521:
7516:
7511:
7507:
7503:
7499:
7495:
7494:
7489:
7485:
7479:
7461:
7460:
7452:
7446:
7440:
7434:
7428:
7426:
7418:
7412:
7410:
7403:
7397:
7386:
7382:
7378:
7374:
7370:
7366:
7362:
7358:
7354:
7353:
7345:
7342:(June 1940).
7341:
7335:
7333:
7331:
7329:
7327:
7325:
7323:
7321:
7319:
7317:
7312:
7289:
7285:
7274:
7253:
7249:
7238:
7231:
7207:
7201:
7192:
7183:
7174:
7150:
7147:
7141:
7137:
7133:
7125:
7122:
7116:
7108:
7103:
7100:
7097:
7093:
7089:
7084:
7081:
7077:
7066:
7064:
7040:
7037:
7031:
7027:
7023:
7015:
7012:
7006:
6998:
6993:
6990:
6987:
6983:
6979:
6974:
6971:
6967:
6963:
6957:
6951:
6948:
6938:
6920:
6917:
6914:
6911:
6906:
6896:
6889:
6886:
6883:
6880:
6875:
6865:
6858:
6853:
6843:
6836:
6833:
6830:
6827:
6822:
6818:
6814:
6811:
6808:
6805:
6800:
6796:
6792:
6787:
6783:
6772:
6770:
6762:
6758:
6757:Alonzo Church
6753:
6749:
6738:
6733:
6731:-equivalence.
6718:
6715:
6707:
6703:
6699:
6683:
6680:
6660:
6657:
6649:
6645:
6641:
6619:
6610:
6606:
6603:
6581:
6572:
6553:
6547:
6535:
6529:
6518:
6514:
6499:
6496:
6488:
6484:
6481:
6477:
6459:
6442:
6438:
6422:
6419:
6411:
6395:
6387:
6386:
6380:
6378:
6373:
6371:
6355:
6346:
6340:
6315:
6277:
6271:
6265:
6262:
6259:
6250:
6244:
6238:
6235:
6232:
6226:
6215:
6211:
6201:
6182:
6159:
6154:
6149:
6126:
6106:
6098:
6083:
6063:
6043:
6035:
6033:
6031:
6011:
5989:
5985:
5976:
5972:
5951:
5929:
5925:
5904:
5898:
5876:
5872:
5863:
5848:
5828:
5808:
5803:
5798:
5778:
5772:
5752:
5746:
5743:
5740:
5732:
5729:
5714:
5694:
5674:
5669:
5664:
5656:
5655:
5654:
5652:
5628:
5619:
5614:
5609:
5603:
5595:
5589:
5586:
5556:
5550:
5547:
5539:
5533:
5530:
5516:
5498:
5490:
5486:
5477:
5473:
5469:
5461:
5453:
5449:
5445:
5438:
5432:
5424:
5420:
5416:
5386:
5380:
5374:
5368:
5365:
5362:
5359:
5351:
5345:
5342:
5339:
5334:
5329:
5326:
5312:
5294:
5288:
5285:
5277:
5269:
5242:
5236:
5233:
5222:
5219:
5214:
5209:
5198:
5195:
5181:
5161:
5121:
5115:
5112:
5089:
5083:
5080:
5069:
5053:
5033:
4993:
4987:
4984:
4961:
4955:
4952:
4941:
4937:
4933:
4929:
4924:
4910:
4904:
4786:
4780:
4777:
4774:
4766:
4762:
4751:
4749:
4745:
4740:
4738:
4734:
4730:
4726:
4722:
4718:
4708:
4706:
4702:
4697:
4695:
4690:
4688:
4684:
4668:
4660:
4644:
4636:
4617:
4612:
4607:
4604:
4601:
4596:
4591:
4580:
4564:
4558:
4551:
4547:
4542:
4540:
4515:
4512:
4507:
4502:
4495:
4481:
4478:
4475:
4470:
4465:
4462:
4453:
4450:
4447:
4442:
4437:
4429:
4425:
4421:
4415:
4412:
4409:
4404:
4399:
4391:
4387:
4376:
4362:
4357:
4352:
4349:
4343:
4338:
4333:
4330:
4327:
4322:
4317:
4309:
4305:
4297:
4283:
4278:
4273:
4270:
4264:
4259:
4254:
4251:
4248:
4243:
4238:
4230:
4226:
4218:
4217:
4216:
4214:
4187:
4169:
4165:
4142:
4138:
4132:
4124:
4116:
4112:
4089:
4085:
4079:
4071:
4063:
4059:
4036:
4032:
4028:
4023:
4019:
4013:
4008:
3988:
3985:
3982:
3959:
3956:
3953:
3930:
3925:
3920:
3900:
3895:
3890:
3882:
3878:
3874:
3870:
3865:
3863:
3859:
3855:
3851:
3847:
3831:
3828:
3814:
3812:
3808:
3804:
3800:
3796:
3795:call by value
3792:
3788:
3778:
3776:
3760:
3740:
3720:
3714:
3711:
3707:
3704:
3678:
3673:
3669:
3665:
3661:
3655:
3652:
3647:
3642:
3639:
3632:
3631:
3630:
3629:
3628:eta reduction
3613:
3608:
3603:
3600:
3577:
3572:
3567:
3564:
3561:
3556:
3551:
3548:
3499:
3496:
3493:
3487:
3482:
3478:
3474:
3467:
3461:
3458:
3453:
3448:
3445:
3435:
3434:
3433:
3432:
3428:
3424:
3414:
3412:
3408:
3404:
3400:
3394:
3380:
3374:
3371:
3368:
3360:
3344:
3338:
3317:
3312:
3309:
3289:
3283:
3265:
3260:
3257:
3248:
3232:
3226:
3205:
3200:
3197:
3189:
3173:
3167:
3149:
3144:
3141:
3107:
3104:
3098:
3089:
3083:
3074:
3067:
3066:
3051:
3048:
3042:
3036:
3030:
3024:
3017:
3016:
3015:
2995:
2989:
2986:
2983:
2980:
2974:
2968:
2955:
2949:
2943:
2937:
2917:
2914:
2908:
2902:
2879:
2873:
2853:
2844:
2842:
2821:
2818:
2811:
2801:
2798:
2791:
2778:
2775:
2767:
2764:
2757:
2751:
2745:
2742:
2736:
2733:
2730:
2727:
2722:
2717:
2714:
2711:
2707:
2704:
2697:
2692:
2687:
2684:
2681:
2677:
2674:
2666:
2663:
2656:
2651:
2646:
2643:
2622:
2619:
2615:
2611:
2608:
2604:
2601:
2593:
2578:
2572:
2566:
2561:
2556:
2553:
2550:
2545:
2540:
2537:
2534:
2531:
2526:
2521:
2518:
2498:
2495:
2492:
2484:
2481:
2465:
2459:
2454:
2449:
2446:
2443:
2438:
2433:
2430:
2410:
2402:
2401:
2400:
2398:
2378:
2356:
2352:
2343:
2339:
2318:
2296:
2292:
2271:
2265:
2243:
2239:
2230:
2215:
2209:
2189:
2183:
2180:
2175:
2170:
2167:
2147:
2127:
2107:
2087:
2067:
2059:
2056:
2041:
2021:
2001:
1981:
1973:
1972:
1971:
1948:
1943:
1936:
1932:
1923:
1919:
1915:
1907:
1902:
1895:
1891:
1887:
1880:
1874:
1869:
1862:
1858:
1854:
1820:
1814:
1806:
1798:
1792:
1789:
1784:
1779:
1776:
1770:
1762:
1757:
1752:
1749:
1746:
1741:
1736:
1733:
1719:
1700:
1695:
1690:
1687:
1679:
1671:
1643:
1638:
1633:
1630:
1619:
1616:
1611:
1606:
1595:
1592:
1590:
1586:
1582:
1566:
1559:(having type
1558:
1542:
1502:
1482:
1462:
1457:
1452:
1449:
1439:
1434:
1420:
1400:
1380:
1375:
1370:
1363:has the form
1362:
1346:
1343:
1337:
1327:
1326:
1321:
1311:
1309:
1290:
1286:
1283:
1280:
1277:
1274:
1271:
1268:
1265:
1262:
1259:
1252:
1251:
1250:
1247:
1245:
1242:. A term is
1229:
1221:
1205:
1185:
1162:
1159:
1156:
1152:
1149:
1146:
1143:
1140:
1135:
1130:
1127:
1124:
1121:
1118:
1115:
1108:
1107:
1106:
1104:
1100:
1096:
1092:
1088:
1072:
1052:
1032:
1027:
1022:
1013:
1007:
1002:
985:
979:
967:
961:
935:
929:
920:
900:
894:
874:
868:
848:
842:
822:
816:
796:
776:
753:
750:
747:
741:
738:
731:For example,
714:
711:
708:
686:
683:
680:
674:
671:
668:
661:
660:
659:
657:
653:
637:
629:
625:
620:
603:
597:
588:
568:
562:
556:
516:
496:
476:
470:
463:
462:function type
459:
443:
423:
415:
411:
375:
369:
346:
343:
320:
317:
314:
294:
274:
254:
234:
214:
205:
202:
201:
196:
192:
182:
160:
156:
152:
148:
144:
140:
136:
132:
128:
124:
120:
116:
112:
108:
104:
99:
97:
93:
92:Alonzo Church
89:
65:
61:
57:
53:
50:), a form of
31:
22:
8578:Institutions
8494:Martin Davis
8430:
8373:
8300:
8290:
8263:
8253:
8243:30 September
8241:. Retrieved
8232:
8222:
8192:(1): 21–26.
8189:
8185:
8132:
8105:
8095:
8062:
8056:
8046:
8011:
8005:
7999:
7974:
7970:
7964:
7937:
7933:
7923:
7898:
7892:
7883:
7847:
7836:
7802:(1): 73–81.
7799:
7793:
7783:
7758:
7754:
7748:
7714:(1): 73–81.
7711:
7705:
7695:
7668:
7658:
7617:
7613:
7583:
7562:
7551:
7497:
7491:
7478:
7467:, retrieved
7458:
7451:
7439:
7431:Leon Henkin
7415:Leon Henkin
7396:
7385:the original
7359:(2): 56–68.
7356:
7350:
7273:
7237:
7208:, in words.
7200:
7191:
7182:
7173:
6937:
6760:
6752:
6736:
6705:
6701:
6697:
6608:
6489:problem for
6374:
6207:
6198:
6175:synthesizes
6029:
6027:
5648:
5067:
4939:
4935:
4927:
4925:
4757:
4748:model theory
4744:axiom schema
4741:
4719:, i.e., the
4714:
4698:
4691:
4682:
4658:
4634:
4543:
4538:
4536:
4213:final object
4185:
3880:
3876:
3872:
3869:typing rules
3866:
3820:
3791:call by name
3784:
3774:
3693:
3517:
3420:
3406:
3403:type erasure
3398:
3395:
3358:
3132:
2845:
2838:
2396:
2394:
2080:having type
1969:
1589:typing rules
1584:
1580:
1556:
1437:
1435:
1360:
1323:
1319:
1317:
1314:Typing rules
1307:
1305:
1248:
1243:
1219:
1177:
1102:
1098:
1095:abstractions
1094:
1090:
1014:
1005:
1003:
730:
655:
652:atomic types
651:
627:
621:
461:
458:Peano axioms
413:
409:
408:' to denote
206:
200:modus ponens
198:
190:
188:
157:because the
154:
151:simply typed
150:
102:
100:
20:
18:
8642:Type theory
8611:A. C. Croom
8534:Gary R. Mar
8509:Leon Henkin
8469:Alan Turing
8182:conversion"
8014:(3): 1–52.
7606:Tait, W. W.
7469:26 February
7465:, p. 1
6602:polynomials
6487:unification
5134:only takes
4932:type system
4737:tautologies
4703:by using a
4687:application
3943:, the term
3803:type safety
3797:, or other
1515:in context
1308:abstraction
1099:application
1065:is of type
581:is read as
103:simple type
52:type theory
8626:Categories
8559:Dana Scott
8330:References
6609:full model
4942:, written
4723:, via the
4157:where the
3877:projection
3867:There are
3409:, through
3401:, through
2846:Each type
2594:For types
2485:For types
1970:In words,
1557:well-typed
628:base types
410:stands for
145:(like the
115:coproducts
8206:1432-0665
8170:η
8167:β
8147:λ
8079:1432-0665
8021:0907.3804
7991:0304-3975
7956:0019-9958
7915:0019-9958
7828:0304-3975
7775:0304-3975
7740:0304-3975
7634:0022-4812
7524:0027-8424
7290:η
7254:β
7216:Γ
7151:α
7142:α
7138:ι
7126:α
7113:Π
7041:α
7032:α
7028:ι
7016:α
7003:Π
6949:λ
6907:α
6900:¯
6876:α
6869:¯
6854:α
6847:¯
6823:α
6801:α
6788:α
6763:pp.47-68
6719:η
6716:β
6684:η
6681:β
6661:η
6658:β
6624:→
6620:λ
6586:→
6582:λ
6551:→
6542:→
6533:→
6500:η
6497:β
6437:decidable
6423:η
6420:β
6396:β
6356:α
6353:→
6347:α
6344:→
6341:α
6316:α
6260:λ
6233:λ
6224:Ω
6183:τ
6160:τ
6127:τ
6084:τ
6064:τ
6056:has type
6012:τ
5952:σ
5905:τ
5902:→
5899:σ
5849:τ
5841:has type
5809:σ
5779:τ
5776:→
5773:σ
5765:has type
5741:λ
5695:σ
5675:σ
5629:τ
5626:⇒
5620:τ
5604:⊢
5601:Γ
5596:τ
5593:⇐
5587:⊢
5584:Γ
5557:τ
5554:⇐
5548:⊢
5545:Γ
5540:τ
5537:⇒
5531:⊢
5528:Γ
5499:τ
5496:⇒
5470:⊢
5467:Γ
5462:σ
5459:⇐
5446:⊢
5443:Γ
5439:τ
5436:→
5433:σ
5430:⇒
5417:⊢
5414:Γ
5387:τ
5384:→
5381:σ
5378:⇐
5363:λ
5360:⊢
5357:Γ
5352:τ
5349:⇐
5343:⊢
5340:σ
5324:Γ
5292:⇒
5286:⊢
5283:Γ
5243:σ
5240:⇒
5234:⊢
5231:Γ
5226:Γ
5223:∈
5220:σ
5182:τ
5142:Γ
5122:τ
5119:⇒
5113:⊢
5110:Γ
5090:τ
5087:⇐
5081:⊢
5078:Γ
5054:τ
5014:Γ
4994:τ
4991:⇒
4985:⊢
4982:Γ
4962:τ
4959:⇐
4953:⊢
4950:Γ
4940:synthesis
4911:α
4908:→
4905:α
4869:→
4820:→
4775:λ
4669:τ
4645:σ
4618:τ
4602:σ
4581:of pairs
4565:τ
4562:→
4559:σ
4550:morphisms
4482:τ
4479:×
4476:σ
4454:τ
4451:×
4448:σ
4426:π
4416:τ
4413:×
4410:σ
4388:π
4363:τ
4344:τ
4328:σ
4306:π
4284:σ
4265:τ
4249:σ
4227:π
4186:unit term
4166:π
4139:τ
4113:π
4086:τ
4060:π
4033:τ
4029:×
4020:τ
3989:τ
3986:×
3983:σ
3975:has type
3931:τ
3901:σ
3881:unit term
3862:morphisms
3832:η
3829:β
3809:property
3721:τ
3718:→
3715:σ
3705:⊢
3702:Γ
3674:η
3653:σ
3640:λ
3614:σ
3601:⊢
3598:Γ
3578:τ
3565:⊢
3562:σ
3546:Γ
3538:whenever
3526:Γ
3483:β
3459:σ
3446:λ
3369:λ
3310:λ
3258:λ
3198:λ
3142:λ
3124:Semantics
3099:ι
3096:→
3090:ι
3087:→
3084:ι
3043:ι
3040:→
3037:ι
3034:→
3031:ι
2996:τ
2975:σ
2950:τ
2947:→
2944:σ
2880:τ
2854:τ
2819:τ
2815:→
2812:τ
2809:→
2799:τ
2795:→
2792:τ
2786:→
2776:τ
2772:→
2765:τ
2761:→
2758:τ
2728:τ
2715:λ
2705:τ
2701:→
2698:τ
2685:λ
2675:τ
2671:→
2664:τ
2660:→
2657:τ
2644:λ
2636:, a term
2620:τ
2609:τ
2602:τ
2579:σ
2576:→
2573:τ
2570:→
2567:σ
2551:τ
2538:λ
2532:σ
2519:λ
2511:, a term
2499:τ
2493:σ
2466:τ
2463:→
2460:τ
2444:τ
2431:λ
2423:, a term
2411:τ
2379:τ
2371:has type
2319:σ
2311:has type
2272:τ
2269:→
2266:σ
2258:has type
2216:τ
2213:→
2210:σ
2202:has type
2181:σ
2168:λ
2128:τ
2120:has type
2088:σ
2042:σ
2034:has type
2002:σ
1994:has type
1949:τ
1916:⊢
1913:Γ
1908:σ
1888:⊢
1885:Γ
1881:τ
1878:→
1875:σ
1855:⊢
1852:Γ
1821:τ
1818:→
1815:σ
1790:σ
1777:λ
1771:⊢
1768:Γ
1763:τ
1750:⊢
1747:σ
1731:Γ
1688:⊢
1685:Γ
1644:σ
1631:⊢
1628:Γ
1623:Γ
1620:∈
1617:σ
1567:σ
1523:Γ
1503:σ
1463:σ
1450:⊢
1447:Γ
1421:σ
1413:has type
1381:σ
1347:…
1341:Δ
1335:Γ
1284:∣
1272:λ
1269:∣
1160:∣
1150:∣
1141:τ
1128:λ
1125:∣
1073:τ
1033:τ
1004:A set of
983:→
974:→
965:→
933:→
924:→
898:→
872:→
846:→
820:→
712:∈
684:∣
681:τ
678:→
675:τ
669:τ
604:ρ
601:→
598:τ
592:→
589:σ
569:ρ
566:→
563:τ
560:→
557:σ
537:→
517:τ
497:σ
477:τ
474:→
471:σ
444:τ
424:σ
396:→
376:α
373:→
370:β
347:β
344:α
321:β
315:α
275:ι
235:ι
169:→
127:recursion
101:The term
74:→
36:→
32:λ
8462:Students
8230:(1973).
8214:33920306
8087:11598130
7875:40441974
7559:(1998).
7542:16577644
7381:15889861
6648:complete
6330:of type
5066:are all
4936:checking
4694:functors
3879:, and a
3247:booleans
3188:integers
2822:″
2802:′
2779:″
2768:′
2708:′
2678:″
2667:′
2623:″
2612:′
1103:constant
139:System F
123:System T
111:products
107:calculus
8038:1478837
7650:9569863
7642:2271658
7533:1076489
7502:Bibcode
7373:2266170
7228:is the
6759:(1956)
6474:of the
4546:objects
3873:pairing
3858:objects
3775:reduced
2331:, then
951:, ...,
58:of the
54:, is a
8599:Family
8346:
8315:
8278:
8212:
8204:
8120:
8085:
8077:
8036:
7989:
7954:
7913:
7873:
7863:
7826:
7773:
7738:
7683:
7648:
7640:
7632:
7571:
7540:
7530:
7522:
7379:
7371:
6275:
6269:
6248:
6242:
5982:
5750:
5483:
5372:
5068:inputs
5046:, and
4784:
4731:, and
4657:) and
4633:where
4548:. The
3659:
3465:
3378:
3342:
3287:
3230:
3171:
2349:
2284:, and
2187:
1929:
1796:
1244:closed
1178:where
1089:, is
1001:, ...
193:: his
185:Syntax
155:simple
137:(like
129:(like
8237:(PDF)
8210:S2CID
8083:S2CID
8034:S2CID
8016:arXiv
7871:S2CID
7646:S2CID
7638:JSTOR
7463:(PDF)
7419:p.160
7388:(PDF)
7377:S2CID
7369:JSTOR
7347:(PDF)
7277:The '
7241:The '
7206:below
6744:Notes
5651:above
1322:, or
1220:bound
1101:, or
412:, or
141:) or
8344:ISBN
8313:ISBN
8276:ISBN
8245:2022
8202:ISSN
8118:ISBN
8075:ISSN
7987:ISSN
7952:ISSN
7911:ISSN
7861:ISBN
7824:ISSN
7771:ISSN
7736:ISSN
7681:ISBN
7630:ISSN
7569:ISBN
7538:PMID
7520:ISSN
7471:2022
6650:for
6640:sets
6485:The
5707:for
5154:and
4974:and
4938:and
4577:are
4104:and
3913:and
3871:for
3733:and
3590:and
3407:i.e.
3399:i.e.
3359:i.e.
3302:and
2397:i.e.
1964:(4)
1839:(3)
1716:(2)
1659:(1)
1436:The
436:and
19:The
8305:doi
8268:doi
8194:doi
8110:doi
8067:doi
8026:doi
7979:doi
7942:doi
7903:doi
7853:doi
7814:hdl
7804:doi
7763:doi
7759:103
7726:hdl
7716:doi
7673:doi
7622:doi
7528:PMC
7510:doi
7361:doi
6611:of
6099:If
6030:not
5864:If
5657:If
4923:).
4689:.
4541:".
3848:of
3777:).
3393:).
3245:on
3186:on
2961:max
1974:If
1263:::=
1218:is
1119:::=
1010:nat
672:::=
654:or
626:of
624:set
131:PCF
117:or
8628::
8338:,
8311:.
8299:.
8274:.
8262:.
8208:.
8200:.
8190:23
8188:.
8184:.
8116:.
8104:.
8081:.
8073:.
8063:17
8055:.
8032:.
8024:.
8010:.
7985:.
7975:13
7973:.
7950:.
7938:38
7936:.
7932:.
7909:.
7899:22
7897:.
7869:.
7859:.
7845:.
7822:.
7812:.
7798:.
7792:.
7769:.
7757:.
7734:.
7724:.
7710:.
7704:.
7679:.
7667:.
7644:.
7636:.
7628:.
7618:32
7616:.
7612:.
7595:^
7536:.
7526:.
7518:.
7508:.
7498:20
7496:.
7490:.
7424:^
7408:^
7375:.
7367:.
7355:.
7349:.
7315:^
7062:^
6768:^
6607:A
6195:.
5026:,
4845:,
4750:.
4707:.
3875:,
3793:,
3497::=
2843:.
2160:,
2100:,
1433:.
1105::
1097:,
1093:,
913:,
887:,
861:,
835:,
809:,
789:,
630:,
619:.
113:,
98:.
8404:e
8397:t
8390:v
8365:.
8350:.
8321:.
8307::
8284:.
8270::
8247:.
8216:.
8196::
8139:"
8126:.
8112::
8089:.
8069::
8040:.
8028::
8018::
8012:5
7993:.
7981::
7958:.
7944::
7917:.
7905::
7877:.
7855::
7830:.
7816::
7806::
7800:9
7777:.
7765::
7742:.
7728::
7718::
7712:9
7689:.
7675::
7652:.
7624::
7577:.
7544:.
7512::
7504::
7363::
7357:5
7286:=
7250:=
7232:.
7154:)
7148:o
7145:(
7134:,
7129:)
7123:o
7120:(
7117:o
7109:,
7104:o
7101:o
7098:o
7094:A
7090:,
7085:o
7082:o
7078:N
7044:)
7038:o
7035:(
7024:,
7019:)
7013:o
7010:(
7007:o
6999:,
6994:o
6991:o
6988:o
6984:A
6980:,
6975:o
6972:o
6968:N
6964:,
6961:)
6958:,
6955:(
6952:,
6921:.
6918:.
6915:.
6912:,
6897:z
6890:.
6887:.
6884:.
6881:,
6866:b
6859:,
6844:a
6837:.
6834:.
6831:.
6828:,
6819:z
6815:.
6812:.
6809:.
6806:,
6797:b
6793:,
6784:a
6569:(
6557:)
6554:o
6548:o
6545:(
6539:)
6536:o
6530:o
6527:(
6460:4
6454:E
6350:)
6338:(
6310:x
6307:i
6304:f
6281:)
6278:x
6272:x
6266:.
6263:x
6257:(
6254:)
6251:x
6245:x
6239:.
6236:x
6230:(
6227:=
6163:)
6155::
6150:e
6147:(
6107:e
6096:.
6044:e
6024:.
5990:2
5986:e
5977:1
5973:e
5930:2
5926:e
5877:1
5873:e
5861:.
5829:e
5804::
5799:x
5753:e
5747:.
5744:x
5727:.
5715:x
5670::
5665:x
5623:)
5615::
5610:e
5607:(
5590:e
5551:e
5534:e
5491:2
5487:e
5478:1
5474:e
5454:2
5450:e
5425:1
5421:e
5375:e
5369:.
5366:x
5346:e
5335::
5330:x
5327:,
5295:T
5289:c
5278:T
5270:c
5237:x
5215::
5210:x
5162:e
5116:e
5084:e
5034:e
4988:e
4956:e
4883:l
4880:o
4877:o
4874:b
4864:l
4861:o
4858:o
4855:b
4831:t
4828:n
4825:i
4815:t
4812:n
4809:i
4787:x
4781:.
4778:x
4683:x
4659:t
4635:x
4621:)
4613::
4608:t
4605:,
4597::
4592:x
4589:(
4522:)
4519:(
4516:=
4513:1
4508::
4503:t
4471::
4466:u
4463:=
4460:)
4457:)
4443::
4438:u
4435:(
4430:2
4422:,
4419:)
4405::
4400:u
4397:(
4392:1
4384:(
4358::
4353:t
4350:=
4347:)
4339::
4334:t
4331:,
4323::
4318:s
4315:(
4310:2
4279::
4274:s
4271:=
4268:)
4260::
4255:t
4252:,
4244::
4239:s
4236:(
4231:1
4199:)
4196:(
4170:i
4143:2
4133::
4128:)
4125:u
4122:(
4117:2
4090:1
4080::
4075:)
4072:u
4069:(
4064:1
4037:2
4024:1
4014::
4009:u
3963:)
3960:t
3957:,
3954:s
3951:(
3926::
3921:t
3896::
3891:s
3761:t
3741:x
3712::
3708:t
3679:t
3670:=
3666:x
3662:t
3656:.
3648::
3643:x
3609::
3604:u
3573::
3568:t
3557::
3552:x
3549:,
3503:]
3500:u
3494:x
3491:[
3488:t
3479:=
3475:u
3471:)
3468:t
3462:.
3454::
3449:x
3443:(
3397:(
3381:x
3375:.
3372:x
3345:x
3339:.
3334:l
3331:o
3328:o
3325:b
3318::
3313:x
3290:x
3284:.
3279:t
3276:n
3273:i
3266::
3261:x
3233:x
3227:.
3222:l
3219:o
3216:o
3213:b
3206::
3201:x
3174:x
3168:.
3163:t
3160:n
3157:i
3150::
3145:x
3108:2
3105:=
3102:)
3093:)
3081:(
3078:(
3075:o
3052:1
3049:=
3046:)
3028:(
3025:o
3002:)
2999:)
2993:(
2990:o
2987:,
2984:1
2981:+
2978:)
2972:(
2969:o
2966:(
2956:=
2953:)
2941:(
2938:o
2918:0
2915:=
2912:)
2909:T
2906:(
2903:o
2883:)
2877:(
2874:o
2806:)
2789:(
2783:)
2755:(
2752::
2749:)
2746:z
2743:y
2740:(
2737:z
2734:x
2731:.
2723::
2718:z
2712:.
2693::
2688:y
2682:.
2652::
2647:x
2616:,
2605:,
2562::
2557:x
2554:.
2546::
2541:y
2535:.
2527::
2522:x
2496:,
2478:(
2455::
2450:x
2447:.
2439::
2434:x
2391:.
2357:2
2353:e
2344:1
2340:e
2297:2
2293:e
2244:1
2240:e
2228:.
2190:e
2184:.
2176::
2171:x
2148:x
2108:e
2068:x
2054:.
2022:x
1982:x
1944::
1937:2
1933:e
1924:1
1920:e
1903::
1896:2
1892:e
1870::
1863:1
1859:e
1824:)
1812:(
1807::
1802:)
1799:e
1793:.
1785::
1780:x
1774:(
1758::
1753:e
1742::
1737:x
1734:,
1701:T
1696::
1691:c
1680:T
1672:c
1639::
1634:x
1612::
1607:x
1543:e
1483:e
1458::
1453:e
1401:x
1376::
1371:x
1344:,
1338:,
1291:e
1287:e
1281:e
1278:.
1275:x
1266:x
1260:e
1230:x
1206:x
1186:c
1163:c
1157:e
1153:e
1147:e
1144:.
1136::
1131:x
1122:x
1116:e
1053:x
1028::
1023:x
989:)
986:b
980:a
977:(
971:)
968:a
962:b
959:(
939:)
936:a
930:a
927:(
921:a
901:a
895:b
875:b
869:b
849:b
843:a
823:a
817:a
797:b
777:a
757:}
754:b
751:,
748:a
745:{
742:=
739:B
727:.
715:B
709:T
704:e
701:r
698:e
695:h
692:w
687:T
638:B
607:)
595:(
350:)
341:(
318:,
295:o
255:o
215:o
121:(
66:(
23:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.