1329:
613:
1324:{\displaystyle {\begin{aligned}\uparrow _{\alpha }t&=\mathbf {SYN} \ t\\\uparrow _{\tau _{1}\to \tau _{2}}v&=\mathbf {LAM} (\lambda S.\ \uparrow _{\tau _{2}}(\mathbf {app} \ (v,\downarrow ^{\tau _{1}}S)))\\\uparrow _{\tau _{1}\times \tau _{2}}v&=\mathbf {PAIR} (\uparrow _{\tau _{1}}(\mathbf {fst} \ v),\uparrow _{\tau _{2}}(\mathbf {snd} \ v))\\\downarrow ^{\alpha }(\mathbf {SYN} \ t)&=t\\\downarrow ^{\tau _{1}\to \tau _{2}}(\mathbf {LAM} \ S)&=\mathbf {lam} \ (x,\downarrow ^{\tau _{2}}(S\ (\uparrow _{\tau _{1}}(\mathbf {var} \ x)))){\text{ where }}x{\text{ is fresh}}\\\downarrow ^{\tau _{1}\times \tau _{2}}(\mathbf {PAIR} \ (S,T))&=\mathbf {pair} \ (\downarrow ^{\tau _{1}}S,\downarrow ^{\tau _{2}}T)\end{aligned}}}
2489:
1871:
2484:{\displaystyle {\begin{aligned}\|\mathbf {var} \ x\|_{\Gamma }&=\Gamma (x)\\\|\mathbf {lam} \ (x,s)\|_{\Gamma }&=\mathbf {LAM} \ (\lambda S.\ \|s\|_{\Gamma ,x\mapsto S})\\\|\mathbf {app} \ (s,t)\|_{\Gamma }&=S\ (\|t\|_{\Gamma }){\text{ where }}\|s\|_{\Gamma }=\mathbf {LAM} \ S\\\|\mathbf {pair} \ (s,t)\|_{\Gamma }&=\mathbf {PAIR} \ (\|s\|_{\Gamma },\|t\|_{\Gamma })\\\|\mathbf {fst} \ s\|_{\Gamma }&=S{\text{ where }}\|s\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\\\|\mathbf {snd} \ t\|_{\Gamma }&=T{\text{ where }}\|t\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\end{aligned}}}
33:
618:
1876:
105:
the denotation. Such an essentially semantic, reduction-free, approach differs from the more traditional syntactic, reduction-based, description of normalisation as reductions in a
528:
Note that there are no variables or elimination forms in the semantics; they are represented simply as syntax. These semantic objects are represented by the following datatype:
3674:
47:
78:
595:
There are a pair of type-indexed functions that move back and forth between the syntactic and semantic layer. The first function, usually written ↑
3842:
3696:
54:
3711:
3626:
3807:
3761:
471:
of (closed) terms in the meta-language interprets the constructs of the syntax in terms of features of the meta-language; thus,
101:
into a denotational model of the λ-term structure, and then a canonical (β-normal and η-long) representative is extracted by
145:
117:
3666:
3650:
3546:
133:
3837:
3480:) then makes it clear that the result is normalized. And if the datatype of normal forms is typed, the type of
2982:
well-typed term, none of these missing cases are ever encountered. The NBE operation on closed terms is then:
3309:
The result is actually in η-long form, as can be easily seen by normalizing it at a different identity type:
125:
3642:
3496:
1834:
468:
357:
94:
3541:
3590:
Coquand, Thierry; Dybjer, Peter (1997). "Intuitionistic model constructions and normalization proofs".
607:
the semantics as a syntactic term (written as ↓). Their definitions are mutually recursive as follows:
149:
148:, where types τ can be basic types (α), function types (→), or products (×), given by the following
75:
106:
3813:
3803:
3618:
3224:
3220:
361:
345:
3793:
3770:
3735:
3599:
3570:
349:
86:
17:
3519:
3454:
90:
1865:, where Γ is a context of bindings, proceeds by induction solely on the term structure:
3643:"Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements"
3491:
Normalization by evaluation also scales to the simply typed lambda calculus with sums (
110:
3831:
3692:
1845:
of type τ, then reifying the object (i.e., ↓ S) produces the β-normal η-long form of
129:
53:
You can help
Knowledge (XXG) by formatting it if you know how. Please also consider
3817:
1849:. All that remains is, therefore, to construct the initial semantic interpretation
3756:
3727:
3562:
180:
121:
3774:
3740:
3704:
3603:
3575:
3619:"Normalization by Evaluation for Martin-Löf Type Theory with One Universe"
3468:
The datatype of residual terms can also be the datatype of residual terms
176:
3798:
3544:(1991). "An inverse of the evaluation functional for typed λ-calculus".
2978:
Note that there are many non-exhaustive cases; however, if applied to a
479:
as application, etc. The semantic objects constructed are as follows:
3515:
3567:
Foundations of
Software Science and Computation Structures (FOSSACS)
1837:
on the structure of types, it follows that if the semantic object
3788:
Danvy, Olivier; Filinski, Andrzej (1990). "Abstracting
Control".
132:
approach, and to richer type systems such as several variants of
3701:
3563:"A denotational account of untyped normalization by evaluation"
1334:
These definitions are easily implemented in the meta-language:
26:
3488:) then makes it clear that normalization is type preserving.
252:
level) is the representation that one intends to normalise.
3755:
Danvy, Olivier; Rhiger, Morten; Rose, Kristoffer (2001).
3757:"Normalization by Evaluation with Typed Abstract Syntax"
3728:"A Semantic Account of Type-Directed Partial Evaluation"
3665:
Gratzer, Daniel; Sterling, Jon; Birkedal, Lars (2019).
3641:
Abel, Andreas; Coquand, Thierry; Dybjer, Peter (2007).
3028:
As an example of its use, consider the syntactic term
1874:
616:
603:
the term syntax into the semantics, while the second
3617:
Abel, Andreas; Aehlig, Klaus; Dybjer, Peter (2007).
3561:Filinski, Andrzej; Rohde, Henning Korsholm (2005).
3732:Principles and Practice of Declarative Programming
2483:
1323:
360:. These terms are intended to be implemented as a
152:grammar (→ associating to the right, as usual):
3687:
3685:
3227:. Normalising it at an identity type produces:
3457:instead of names in the residual syntax makes
2541:(* lookup : ctx -> string -> sem *)
3461:a pure function in that there is no need for
8:
3667:"Implementing a Modal Dependent Type Theory"
2433:
2426:
2402:
2381:
2333:
2326:
2302:
2281:
2265:
2258:
2246:
2239:
2203:
2167:
2134:
2127:
2110:
2103:
2078:
2045:
2017:
2010:
1965:
1932:
1900:
1879:
120:. It has since been extended both to weaker
2616:(* meaning : ctx -> tm -> sem *)
244:Terms are defined at two levels. The lower
3592:Mathematical Structure in Computer Science
1603:(* reify : ty -> sem -> tm *)
1414:(* reflect : ty -> tm -> sem *)
3797:
3739:
3574:
2445:
2436:
2421:
2405:
2384:
2345:
2336:
2321:
2305:
2284:
2268:
2249:
2219:
2206:
2170:
2146:
2137:
2122:
2113:
2081:
2048:
2020:
1981:
1968:
1935:
1903:
1882:
1875:
1873:
1303:
1298:
1280:
1275:
1251:
1209:
1198:
1185:
1180:
1167:
1159:
1130:
1119:
1114:
1090:
1085:
1058:
1031:
1020:
1007:
1002:
964:
955:
924:
913:
908:
881:
870:
865:
844:
826:
813:
808:
780:
775:
748:
737:
732:
702:
684:
671:
666:
641:
625:
617:
615:
1339:(* fresh_var : unit -> string *)
55:changing this notice to be more specific
3532:
3219:This is the well-known encoding of the
179:in the meta-language; for example, for
2987:(* nbe : ty -> tm -> tm *)
7:
3522:that uses NBE as its rewrite engine.
3697:"Type-directed partial evaluation"
2437:
2406:
2337:
2306:
2269:
2250:
2207:
2138:
2114:
2082:
2021:
1969:
1916:
1904:
25:
3762:Journal of Functional Programming
113:are allowed deep inside λ-terms.
83:normalisation by evaluation (NBE)
2455:
2452:
2449:
2446:
2391:
2388:
2385:
2355:
2352:
2349:
2346:
2291:
2288:
2285:
2229:
2226:
2223:
2220:
2180:
2177:
2174:
2171:
2153:
2150:
2147:
2055:
2052:
2049:
1988:
1985:
1982:
1942:
1939:
1936:
1889:
1886:
1883:
1261:
1258:
1255:
1252:
1219:
1216:
1213:
1210:
1137:
1134:
1131:
1065:
1062:
1059:
1038:
1035:
1032:
971:
968:
965:
931:
928:
925:
888:
885:
882:
854:
851:
848:
845:
755:
752:
749:
709:
706:
703:
648:
645:
642:
116:NBE was first described for the
31:
3790:LISP and Functional Programming
475:is interpreted as abstraction,
364:datatype in the meta-language:
3843:Programming language semantics
2474:
2462:
2374:
2362:
2274:
2236:
2199:
2187:
2119:
2100:
2074:
2062:
2038:
2030:
1995:
1961:
1949:
1925:
1919:
1314:
1295:
1272:
1268:
1241:
1238:
1226:
1206:
1177:
1156:
1153:
1150:
1147:
1127:
1111:
1107:
1098:
1082:
1072:
1048:
1028:
1013:
999:
981:
961:
952:
944:
941:
921:
905:
898:
878:
862:
858:
805:
797:
794:
791:
772:
762:
745:
729:
713:
677:
663:
622:
175:These can be implemented as a
1:
85:is a method of obtaining the
248:level (sometimes called the
146:simply typed lambda calculus
118:simply typed lambda calculus
3497:delimited control operators
1857:. This operation, written ∥
352:forms for → (resp. ×), and
18:Normalization by evaluation
3859:
1841:denotes a well-typed term
3775:10.1017/S0956796801004166
3741:10.7146/brics.v6i17.20074
3604:10.1017/S0960129596002150
3576:10.7146/brics.v12i4.21870
3311:
3229:
3034:
2984:
2496:
1336:
530:
366:
185:
156:(Types) τ ::= α | τ
2494:In the implementation:
126:untyped lambda calculus
3542:Schwichtenberg, Helmut
2492:
2485:
1853:from a syntactic term
1332:
1325:
469:denotational semantics
134:Martin-Löf type theory
95:denotational semantics
93:by appealing to their
2486:
1867:
1326:
609:
3792:. pp. 151–160.
1872:
614:
76:programming language
3799:10.1145/91556.91622
3726:Filinski, Andrzej.
107:term rewrite system
3484:(and therefore of
3476:(and therefore of
2481:
2479:
1321:
1319:
97:. A term is first
3225:combinatory logic
3221:identity function
2461:
2424:
2423: where
2397:
2361:
2324:
2323: where
2297:
2235:
2186:
2159:
2125:
2124: where
2099:
2061:
2009:
1994:
1948:
1895:
1267:
1225:
1170:
1162:
1161: where
1143:
1106:
1071:
1044:
977:
937:
894:
761:
727:
654:
483:(Semantic Terms)
72:
71:
16:(Redirected from
3850:
3822:
3821:
3801:
3785:
3779:
3778:
3752:
3746:
3745:
3743:
3723:
3717:
3716:
3708:
3689:
3680:
3679:
3671:
3662:
3656:
3655:
3647:
3638:
3632:
3631:
3623:
3614:
3608:
3607:
3587:
3581:
3580:
3578:
3569:. Vol. 10.
3558:
3552:
3551:
3540:Berger, Ulrich;
3537:
3505:
3501:
3494:
3487:
3483:
3479:
3475:
3464:
3460:
3455:de Bruijn levels
3444:
3441:
3438:
3435:
3432:
3429:
3426:
3423:
3420:
3417:
3414:
3411:
3408:
3405:
3402:
3399:
3396:
3393:
3390:
3387:
3384:
3381:
3378:
3375:
3372:
3369:
3366:
3363:
3360:
3357:
3354:
3351:
3348:
3345:
3342:
3339:
3336:
3333:
3330:
3327:
3324:
3321:
3318:
3315:
3305:
3302:
3299:
3296:
3293:
3290:
3287:
3284:
3281:
3278:
3275:
3272:
3269:
3266:
3263:
3260:
3257:
3254:
3251:
3248:
3245:
3242:
3239:
3236:
3233:
3215:
3212:
3209:
3206:
3203:
3200:
3197:
3194:
3191:
3188:
3185:
3182:
3179:
3176:
3173:
3170:
3167:
3164:
3161:
3158:
3155:
3152:
3149:
3146:
3143:
3140:
3137:
3134:
3131:
3128:
3125:
3122:
3119:
3116:
3113:
3110:
3107:
3104:
3101:
3098:
3095:
3092:
3089:
3086:
3083:
3080:
3077:
3074:
3071:
3068:
3065:
3062:
3059:
3056:
3053:
3050:
3047:
3044:
3041:
3038:
3031:
3024:
3021:
3018:
3015:
3012:
3009:
3006:
3003:
3000:
2997:
2994:
2991:
2988:
2974:
2971:
2968:
2965:
2962:
2959:
2956:
2953:
2950:
2947:
2944:
2941:
2938:
2935:
2932:
2929:
2926:
2923:
2920:
2917:
2914:
2911:
2908:
2905:
2902:
2899:
2896:
2893:
2890:
2887:
2884:
2881:
2878:
2875:
2872:
2869:
2866:
2863:
2860:
2857:
2854:
2851:
2848:
2845:
2842:
2839:
2836:
2833:
2830:
2827:
2824:
2821:
2818:
2815:
2812:
2809:
2806:
2803:
2800:
2797:
2794:
2791:
2788:
2785:
2782:
2779:
2776:
2773:
2770:
2767:
2764:
2761:
2758:
2755:
2752:
2749:
2746:
2743:
2740:
2737:
2734:
2731:
2728:
2725:
2722:
2719:
2716:
2713:
2710:
2707:
2704:
2701:
2698:
2695:
2692:
2689:
2686:
2683:
2680:
2677:
2674:
2671:
2668:
2665:
2662:
2659:
2656:
2653:
2650:
2647:
2644:
2641:
2638:
2635:
2632:
2629:
2626:
2623:
2620:
2617:
2614:
2611:
2608:
2605:
2602:
2599:
2596:
2593:
2590:
2587:
2584:
2581:
2578:
2575:
2572:
2569:
2566:
2563:
2560:
2557:
2554:
2551:
2548:
2545:
2542:
2539:
2536:
2533:
2530:
2527:
2524:
2521:
2518:
2515:
2512:
2509:
2506:
2503:
2500:
2490:
2488:
2487:
2482:
2480:
2459:
2458:
2441:
2440:
2425:
2422:
2410:
2409:
2395:
2394:
2359:
2358:
2341:
2340:
2325:
2322:
2310:
2309:
2295:
2294:
2273:
2272:
2254:
2253:
2233:
2232:
2211:
2210:
2184:
2183:
2157:
2156:
2142:
2141:
2126:
2123:
2118:
2117:
2097:
2086:
2085:
2059:
2058:
2037:
2036:
2007:
1992:
1991:
1973:
1972:
1946:
1945:
1908:
1907:
1893:
1892:
1829:
1826:
1823:
1820:
1817:
1814:
1811:
1808:
1805:
1802:
1799:
1796:
1793:
1790:
1787:
1784:
1781:
1778:
1775:
1772:
1769:
1766:
1763:
1760:
1757:
1754:
1751:
1748:
1745:
1742:
1739:
1736:
1733:
1730:
1727:
1724:
1721:
1718:
1715:
1712:
1709:
1706:
1703:
1700:
1697:
1694:
1691:
1688:
1685:
1682:
1679:
1676:
1673:
1670:
1667:
1664:
1661:
1658:
1655:
1652:
1649:
1646:
1643:
1640:
1637:
1634:
1631:
1628:
1625:
1622:
1619:
1616:
1613:
1610:
1607:
1604:
1601:
1598:
1595:
1592:
1589:
1586:
1583:
1580:
1577:
1574:
1571:
1568:
1565:
1562:
1559:
1556:
1553:
1550:
1547:
1544:
1541:
1538:
1535:
1532:
1529:
1526:
1523:
1520:
1517:
1514:
1511:
1508:
1505:
1502:
1499:
1496:
1493:
1490:
1487:
1484:
1481:
1478:
1475:
1472:
1469:
1466:
1463:
1460:
1457:
1454:
1451:
1448:
1445:
1442:
1439:
1436:
1433:
1430:
1427:
1424:
1421:
1418:
1415:
1412:
1409:
1406:
1403:
1400:
1397:
1394:
1391:
1388:
1385:
1382:
1379:
1376:
1373:
1370:
1367:
1364:
1361:
1358:
1355:
1352:
1349:
1346:
1343:
1340:
1330:
1328:
1327:
1322:
1320:
1310:
1309:
1308:
1307:
1287:
1286:
1285:
1284:
1265:
1264:
1223:
1222:
1205:
1204:
1203:
1202:
1190:
1189:
1171:
1168:
1163:
1160:
1141:
1140:
1126:
1125:
1124:
1123:
1104:
1097:
1096:
1095:
1094:
1069:
1068:
1042:
1041:
1027:
1026:
1025:
1024:
1012:
1011:
975:
974:
960:
959:
935:
934:
920:
919:
918:
917:
892:
891:
877:
876:
875:
874:
857:
833:
832:
831:
830:
818:
817:
787:
786:
785:
784:
759:
758:
744:
743:
742:
741:
725:
712:
691:
690:
689:
688:
676:
675:
652:
651:
630:
629:
591:
588:
585:
582:
579:
576:
573:
570:
567:
564:
561:
558:
555:
552:
549:
546:
543:
540:
537:
534:
463:
460:
457:
454:
451:
448:
445:
442:
439:
436:
433:
430:
427:
424:
421:
418:
415:
412:
409:
406:
403:
400:
397:
394:
391:
388:
385:
382:
379:
376:
373:
370:
240:
237:
234:
231:
228:
225:
222:
219:
216:
213:
210:
207:
204:
201:
198:
195:
192:
189:
183:, we might use:
150:Backus–Naur form
130:domain theoretic
89:of terms in the
67:
64:
58:
43:
35:
34:
27:
21:
3858:
3857:
3853:
3852:
3851:
3849:
3848:
3847:
3838:Lambda calculus
3828:
3827:
3826:
3825:
3810:
3787:
3786:
3782:
3754:
3753:
3749:
3725:
3724:
3720:
3699:
3691:
3690:
3683:
3669:
3664:
3663:
3659:
3645:
3640:
3639:
3635:
3621:
3616:
3615:
3611:
3589:
3588:
3584:
3560:
3559:
3555:
3539:
3538:
3534:
3529:
3520:proof assistant
3512:
3503:
3499:
3492:
3485:
3481:
3477:
3473:
3462:
3458:
3451:
3446:
3445:
3442:
3439:
3436:
3433:
3430:
3427:
3424:
3421:
3418:
3415:
3412:
3409:
3406:
3403:
3400:
3397:
3394:
3391:
3388:
3385:
3382:
3379:
3376:
3373:
3370:
3367:
3364:
3361:
3358:
3355:
3352:
3349:
3346:
3343:
3340:
3337:
3334:
3331:
3328:
3325:
3322:
3319:
3316:
3313:
3307:
3306:
3303:
3300:
3297:
3294:
3291:
3288:
3285:
3282:
3279:
3276:
3273:
3270:
3267:
3264:
3261:
3258:
3255:
3252:
3249:
3246:
3243:
3240:
3237:
3234:
3231:
3217:
3216:
3213:
3210:
3207:
3204:
3201:
3198:
3195:
3192:
3189:
3186:
3183:
3180:
3177:
3174:
3171:
3168:
3165:
3162:
3159:
3156:
3153:
3150:
3147:
3144:
3141:
3138:
3135:
3132:
3129:
3126:
3123:
3120:
3117:
3114:
3111:
3108:
3105:
3102:
3099:
3096:
3093:
3090:
3087:
3084:
3081:
3078:
3075:
3072:
3069:
3066:
3063:
3060:
3057:
3054:
3051:
3048:
3045:
3042:
3039:
3036:
3032:defined below:
3029:
3026:
3025:
3022:
3019:
3016:
3013:
3010:
3007:
3004:
3001:
2998:
2995:
2992:
2989:
2986:
2976:
2975:
2972:
2969:
2966:
2963:
2960:
2957:
2954:
2951:
2948:
2945:
2942:
2939:
2936:
2933:
2930:
2927:
2924:
2921:
2918:
2915:
2912:
2909:
2906:
2903:
2900:
2897:
2894:
2891:
2888:
2885:
2882:
2879:
2876:
2873:
2870:
2867:
2864:
2861:
2858:
2855:
2852:
2849:
2846:
2843:
2840:
2837:
2834:
2831:
2828:
2825:
2822:
2819:
2816:
2813:
2810:
2807:
2804:
2801:
2798:
2795:
2792:
2789:
2786:
2783:
2780:
2777:
2774:
2771:
2768:
2765:
2762:
2759:
2756:
2753:
2750:
2747:
2744:
2741:
2738:
2735:
2732:
2729:
2726:
2723:
2720:
2717:
2714:
2711:
2708:
2705:
2702:
2699:
2696:
2693:
2690:
2687:
2684:
2681:
2678:
2675:
2672:
2669:
2666:
2663:
2660:
2657:
2654:
2651:
2648:
2645:
2642:
2639:
2636:
2633:
2630:
2627:
2624:
2621:
2618:
2615:
2612:
2609:
2606:
2603:
2600:
2597:
2594:
2591:
2588:
2585:
2582:
2579:
2576:
2573:
2570:
2567:
2564:
2561:
2558:
2555:
2552:
2549:
2546:
2543:
2540:
2537:
2534:
2531:
2528:
2525:
2522:
2519:
2516:
2513:
2510:
2507:
2504:
2501:
2498:
2478:
2477:
2432:
2411:
2401:
2378:
2377:
2332:
2311:
2301:
2278:
2277:
2264:
2245:
2212:
2202:
2164:
2163:
2133:
2109:
2087:
2077:
2042:
2041:
2016:
1974:
1964:
1929:
1928:
1909:
1899:
1870:
1869:
1864:
1831:
1830:
1827:
1824:
1821:
1818:
1815:
1812:
1809:
1806:
1803:
1800:
1797:
1794:
1791:
1788:
1785:
1782:
1779:
1776:
1773:
1770:
1767:
1764:
1761:
1758:
1755:
1752:
1749:
1746:
1743:
1740:
1737:
1734:
1731:
1728:
1725:
1722:
1719:
1716:
1713:
1710:
1707:
1704:
1701:
1698:
1695:
1692:
1689:
1686:
1683:
1680:
1677:
1674:
1671:
1668:
1665:
1662:
1659:
1656:
1653:
1650:
1647:
1644:
1641:
1638:
1635:
1632:
1629:
1626:
1623:
1620:
1617:
1614:
1611:
1608:
1605:
1602:
1599:
1596:
1593:
1590:
1587:
1584:
1581:
1578:
1575:
1572:
1569:
1566:
1563:
1560:
1557:
1554:
1551:
1548:
1545:
1542:
1539:
1536:
1533:
1530:
1527:
1524:
1521:
1518:
1515:
1512:
1509:
1506:
1503:
1500:
1497:
1494:
1491:
1488:
1485:
1482:
1479:
1476:
1473:
1470:
1467:
1464:
1461:
1458:
1455:
1452:
1449:
1446:
1443:
1440:
1437:
1434:
1431:
1428:
1425:
1422:
1419:
1416:
1413:
1410:
1407:
1404:
1401:
1398:
1395:
1392:
1389:
1386:
1383:
1380:
1377:
1374:
1371:
1368:
1365:
1362:
1359:
1356:
1353:
1350:
1347:
1344:
1341:
1338:
1318:
1317:
1299:
1294:
1276:
1271:
1244:
1194:
1181:
1176:
1173:
1172:
1115:
1110:
1086:
1081:
1051:
1016:
1003:
998:
995:
994:
984:
951:
948:
947:
909:
904:
866:
861:
837:
822:
809:
804:
801:
800:
776:
771:
733:
728:
695:
680:
667:
662:
659:
658:
634:
621:
612:
611:
598:
593:
592:
589:
586:
583:
580:
577:
574:
571:
568:
565:
562:
559:
556:
553:
550:
547:
544:
541:
538:
535:
532:
465:
464:
461:
458:
455:
452:
449:
446:
443:
440:
437:
434:
431:
428:
425:
422:
419:
416:
413:
410:
407:
404:
401:
398:
395:
392:
389:
386:
383:
380:
377:
374:
371:
368:
256:(Syntax Terms)
242:
241:
238:
235:
232:
229:
226:
223:
220:
217:
214:
211:
208:
205:
202:
199:
196:
193:
190:
187:
171:
167:
163:
159:
142:
68:
62:
59:
52:
46:may need to be
41:
36:
32:
23:
22:
15:
12:
11:
5:
3856:
3854:
3846:
3845:
3840:
3830:
3829:
3824:
3823:
3808:
3780:
3769:(6): 673–680.
3747:
3718:
3693:Danvy, Olivier
3681:
3657:
3633:
3609:
3582:
3553:
3531:
3530:
3528:
3525:
3524:
3523:
3511:
3508:
3472:. The type of
3470:in normal form
3450:
3447:
3434:"v2"
3425:"v1"
3410:"v2"
3398:"v1"
3312:
3295:"v0"
3286:"v0"
3230:
3035:
2985:
2497:
2476:
2473:
2470:
2467:
2464:
2457:
2454:
2451:
2448:
2444:
2439:
2435:
2431:
2428:
2420:
2417:
2414:
2412:
2408:
2404:
2400:
2393:
2390:
2387:
2383:
2380:
2379:
2376:
2373:
2370:
2367:
2364:
2357:
2354:
2351:
2348:
2344:
2339:
2335:
2331:
2328:
2320:
2317:
2314:
2312:
2308:
2304:
2300:
2293:
2290:
2287:
2283:
2280:
2279:
2276:
2271:
2267:
2263:
2260:
2257:
2252:
2248:
2244:
2241:
2238:
2231:
2228:
2225:
2222:
2218:
2215:
2213:
2209:
2205:
2201:
2198:
2195:
2192:
2189:
2182:
2179:
2176:
2173:
2169:
2166:
2165:
2162:
2155:
2152:
2149:
2145:
2140:
2136:
2132:
2129:
2121:
2116:
2112:
2108:
2105:
2102:
2096:
2093:
2090:
2088:
2084:
2080:
2076:
2073:
2070:
2067:
2064:
2057:
2054:
2051:
2047:
2044:
2043:
2040:
2035:
2032:
2029:
2026:
2023:
2019:
2015:
2012:
2006:
2003:
2000:
1997:
1990:
1987:
1984:
1980:
1977:
1975:
1971:
1967:
1963:
1960:
1957:
1954:
1951:
1944:
1941:
1938:
1934:
1931:
1930:
1927:
1924:
1921:
1918:
1915:
1912:
1910:
1906:
1902:
1898:
1891:
1888:
1885:
1881:
1878:
1877:
1862:
1337:
1316:
1313:
1306:
1302:
1297:
1293:
1290:
1283:
1279:
1274:
1270:
1263:
1260:
1257:
1254:
1250:
1247:
1245:
1243:
1240:
1237:
1234:
1231:
1228:
1221:
1218:
1215:
1212:
1208:
1201:
1197:
1193:
1188:
1184:
1179:
1175:
1174:
1169: is fresh
1166:
1158:
1155:
1152:
1149:
1146:
1139:
1136:
1133:
1129:
1122:
1118:
1113:
1109:
1103:
1100:
1093:
1089:
1084:
1080:
1077:
1074:
1067:
1064:
1061:
1057:
1054:
1052:
1050:
1047:
1040:
1037:
1034:
1030:
1023:
1019:
1015:
1010:
1006:
1001:
997:
996:
993:
990:
987:
985:
983:
980:
973:
970:
967:
963:
958:
954:
950:
949:
946:
943:
940:
933:
930:
927:
923:
916:
912:
907:
903:
900:
897:
890:
887:
884:
880:
873:
869:
864:
860:
856:
853:
850:
847:
843:
840:
838:
836:
829:
825:
821:
816:
812:
807:
803:
802:
799:
796:
793:
790:
783:
779:
774:
770:
767:
764:
757:
754:
751:
747:
740:
736:
731:
724:
721:
718:
715:
711:
708:
705:
701:
698:
696:
694:
687:
683:
679:
674:
670:
665:
661:
660:
657:
650:
647:
644:
640:
637:
635:
633:
628:
624:
620:
619:
596:
531:
526:
525:
367:
322:
321:
186:
173:
172:
169:
165:
161:
157:
141:
138:
70:
69:
39:
37:
30:
24:
14:
13:
10:
9:
6:
4:
3:
2:
3855:
3844:
3841:
3839:
3836:
3835:
3833:
3819:
3815:
3811:
3809:0-89791-368-X
3805:
3800:
3795:
3791:
3784:
3781:
3776:
3772:
3768:
3764:
3763:
3758:
3751:
3748:
3742:
3737:
3733:
3729:
3722:
3719:
3714:
3713:
3706:
3703:
3698:
3694:
3688:
3686:
3682:
3677:
3676:
3668:
3661:
3658:
3653:
3652:
3644:
3637:
3634:
3629:
3628:
3620:
3613:
3610:
3605:
3601:
3597:
3593:
3586:
3583:
3577:
3572:
3568:
3564:
3557:
3554:
3549:
3548:
3543:
3536:
3533:
3526:
3521:
3517:
3514:
3513:
3509:
3507:
3498:
3495:), using the
3489:
3471:
3466:
3456:
3448:
3371:"b"
3362:"a"
3347:"b"
3338:"a"
3310:
3259:"a"
3250:"a"
3228:
3226:
3222:
3172:"z"
3163:"y"
3148:"z"
3139:"x"
3118:"z"
3106:"y"
3094:"x"
3073:"x"
3064:"y"
3052:"x"
3033:
2983:
2981:
2495:
2491:
2471:
2468:
2465:
2442:
2429:
2418:
2415:
2413:
2398:
2371:
2368:
2365:
2342:
2329:
2318:
2315:
2313:
2298:
2261:
2255:
2242:
2216:
2214:
2196:
2193:
2190:
2160:
2143:
2130:
2106:
2094:
2091:
2089:
2071:
2068:
2065:
2033:
2027:
2024:
2013:
2004:
2001:
1998:
1978:
1976:
1958:
1955:
1952:
1922:
1913:
1911:
1896:
1866:
1860:
1856:
1852:
1848:
1844:
1840:
1836:
1408:!variable_ctr
1390:"v"
1384:!variable_ctr
1335:
1331:
1311:
1304:
1300:
1291:
1288:
1281:
1277:
1248:
1246:
1235:
1232:
1229:
1199:
1195:
1191:
1186:
1182:
1164:
1144:
1120:
1116:
1101:
1091:
1087:
1078:
1075:
1055:
1053:
1045:
1021:
1017:
1008:
1004:
991:
988:
986:
978:
956:
938:
914:
910:
901:
895:
871:
867:
841:
839:
834:
827:
823:
819:
814:
810:
788:
781:
777:
768:
765:
738:
734:
722:
719:
716:
699:
697:
692:
685:
681:
672:
668:
655:
638:
636:
631:
626:
608:
606:
602:
529:
524:
521:
517:
513:
509:
505:
502:
498:
494:
490:
486:
482:
481:
480:
478:
474:
470:
365:
363:
359:
355:
351:
347:
343:
339:
335:
331:
327:
320:
317:
313:
310:
306:
302:
298:
294:
290:
286:
282:
278:
274:
270:
267:
263:
259:
255:
254:
253:
251:
247:
184:
182:
178:
155:
154:
153:
151:
147:
144:Consider the
139:
137:
135:
131:
127:
123:
119:
114:
112:
108:
104:
100:
96:
92:
88:
84:
80:
77:
66:
56:
51:
49:
38:
29:
28:
19:
3789:
3783:
3766:
3760:
3750:
3731:
3721:
3710:
3673:
3660:
3649:
3636:
3625:
3612:
3598:(1): 75–94.
3595:
3591:
3585:
3566:
3556:
3545:
3535:
3490:
3469:
3467:
3452:
3308:
3218:
3027:
2979:
2977:
2493:
1868:
1858:
1854:
1850:
1846:
1842:
1838:
1832:
1372:variable_ctr
1345:variable_ctr
1333:
610:
604:
600:
594:
527:
522:
519:
515:
511:
507:
503:
500:
496:
492:
491:,… ::=
488:
484:
476:
472:
466:
353:
341:
337:
333:
329:
325:
323:
318:
315:
311:
308:
304:
300:
296:
292:
288:
284:
280:
276:
272:
268:
265:
264:,… ::=
261:
257:
249:
245:
243:
174:
143:
124:such as the
122:type systems
115:
111:β-reductions
102:
98:
82:
73:
60:
45:
40:This article
362:first-order
181:Standard ML
99:interpreted
87:normal form
44:or section
3832:Categories
3715:: 242–257.
3705:PostScript
3527:References
344:) are the
91:λ-calculus
63:April 2014
3463:fresh_var
2438:Γ
2434:‖
2427:‖
2407:Γ
2403:‖
2382:‖
2338:Γ
2334:‖
2327:‖
2307:Γ
2303:‖
2282:‖
2270:Γ
2266:‖
2259:‖
2251:Γ
2247:‖
2240:‖
2208:Γ
2204:‖
2168:‖
2139:Γ
2135:‖
2128:‖
2115:Γ
2111:‖
2104:‖
2083:Γ
2079:‖
2046:‖
2031:↦
2022:Γ
2018:‖
2011:‖
1999:λ
1970:Γ
1966:‖
1933:‖
1917:Γ
1905:Γ
1901:‖
1880:‖
1835:induction
1660:fresh_var
1360:fresh_var
1301:τ
1296:↓
1278:τ
1273:↓
1196:τ
1192:×
1183:τ
1178:↓
1117:τ
1112:↑
1088:τ
1083:↓
1018:τ
1014:→
1005:τ
1000:↓
957:α
953:↓
911:τ
906:↑
868:τ
863:↑
824:τ
820:×
811:τ
806:↑
778:τ
773:↓
735:τ
730:↑
717:λ
682:τ
678:→
669:τ
664:↑
627:α
623:↑
358:variables
246:syntactic
79:semantics
48:formatted
3695:(1996).
3510:See also
3449:Variants
2499:datatype
1402:toString
601:reflects
533:datatype
369:datatype
188:datatype
177:datatype
128:using a
103:reifying
3818:6426191
3702:gzipped
3014:meaning
2937:meaning
2880:meaning
2850:meaning
2838:meaning
2796:meaning
2769:meaning
2700:meaning
2622:meaning
1696:reflect
1579:reflect
1558:reflect
1540:reflect
1504:reflect
1465:reflect
1420:reflect
605:reifies
332:(resp.
250:dynamic
140:Outline
3816:
3806:
3516:MINLOG
3453:Using
2980:closed
2652:lookup
2607:lookup
2547:lookup
2529:string
2460:
2396:
2360:
2296:
2234:
2185:
2158:
2098:
2060:
2008:
1993:
1947:
1894:
1266:
1224:
1142:
1105:
1070:
1043:
976:
936:
893:
760:
726:
653:
396:string
384:string
203:string
109:where
42:
3814:S2CID
3670:(PDF)
3646:(PDF)
3622:(PDF)
3504:reset
3500:shift
3482:reify
3474:reify
3459:reify
3368:Basic
3359:Basic
3353:Arrow
3344:Basic
3335:Basic
3329:Arrow
3323:Arrow
3256:Basic
3247:Basic
3241:Arrow
3175:)))))
3017:empty
3005:reify
2967:=>
2928:=>
2910:=>
2871:=>
2829:=>
2787:=>
2760:=>
2697:=>
2682:=>
2649:=>
2610:remdr
2601:value
2574:value
2559:remdr
2508:empty
1807:Basic
1801:reify
1786:reify
1774:reify
1720:reify
1681:reify
1615:Arrow
1609:reify
1585:Basic
1489:reify
1462:=>
1426:Arrow
554:->
346:intro
324:Here
209:Arrow
197:Basic
3804:ISBN
3712:POPL
3675:ICFP
3651:LICS
3627:MFPS
3547:LICS
3518:, a
3502:and
2949:PAIR
2934:case
2892:PAIR
2877:case
2832:PAIR
2811:pair
2766:case
2634:case
2604:else
2598:then
1768:pair
1747:PAIR
1726:Prod
1711:))))
1534:PAIR
1510:Prod
1498:))))
566:PAIR
518:) |
508:PAIR
506:) |
467:The
426:pair
356:are
350:elim
334:pair
307:) |
297:pair
295:) |
283:) |
227:Prod
3794:doi
3771:doi
3736:doi
3600:doi
3571:doi
3486:nbe
3478:nbe
3437:)))
3431:var
3422:var
3416:app
3404:lam
3392:lam
3383:val
3377:SKK
3374:)))
3317:nbe
3292:var
3280:lam
3271:val
3265:SKK
3235:nbe
3223:in
3193:app
3187:app
3181:SKK
3178:val
3169:var
3160:var
3154:app
3145:var
3136:var
3130:app
3124:app
3112:lam
3100:lam
3088:lam
3079:val
3070:var
3058:lam
3046:lam
3037:val
3030:SKK
2993:nbe
2990:fun
2922:snd
2865:fst
2781:LAM
2742:app
2730:)))
2706:add
2685:LAM
2664:lam
2643:var
2619:fun
2577:)))
2553:add
2544:fun
2535:sem
2520:ctx
2514:add
2502:ctx
1833:By
1816:SYN
1714:end
1705:var
1669:lam
1651:val
1648:let
1636:LAM
1606:and
1597:SYN
1567:snd
1549:fst
1474:app
1450:LAM
1417:fun
1396:Int
1357:fun
1351:ref
1342:val
584:SYN
578:sem
572:sem
557:sem
551:sem
542:LAM
536:sem
520:SYN
493:LAM
477:app
473:lam
456:snd
444:fst
408:app
390:lam
378:var
342:snd
338:fst
330:app
326:lam
316:snd
309:fst
285:app
273:lam
266:var
168:× τ
164:| τ
160:→ τ
74:In
3834::
3812:.
3802:.
3767:11
3765:.
3759:.
3734:.
3730:.
3709:.
3684:^
3672:.
3648:.
3624:.
3594:.
3565:.
3506:.
3465:.
3443:tm
3386:it
3350:),
3304:tm
3274:it
3262:))
3208:),
3151:),
3076:))
2946:of
2889:of
2805:))
2778:of
2691:fn
2640:of
2586:if
2517:of
1810:_)
1762:))
1741:))
1666:in
1663:()
1630:))
1588:_)
1573:))
1555:),
1525:))
1456:fn
1441:))
1411:))
1375::=
1363:()
1354:~1
599:,
590:tm
587:of
569:of
545:of
514:,
499:.
495:(λ
462:tm
459:of
450:tm
447:of
438:tm
432:tm
429:of
420:tm
414:tm
411:of
402:tm
393:of
381:of
372:tm
314:|
303:,
291:,
279:,
271:|
239:ty
233:ty
230:of
221:ty
215:ty
212:of
200:of
191:ty
136:.
81:,
3820:.
3796::
3777:.
3773::
3744:.
3738::
3707:)
3700:(
3678:.
3654:.
3630:.
3606:.
3602::
3596:7
3579:.
3573::
3550:.
3493:+
3440::
3428:,
3419:(
3413:,
3407:(
3401:,
3395:(
3389:=
3380:;
3365:,
3356:(
3341:,
3332:(
3326:(
3320:(
3314:-
3301::
3298:)
3289:,
3283:(
3277:=
3268:;
3253:,
3244:(
3238:(
3232:-
3214:)
3211:K
3205:K
3202:,
3199:S
3196:(
3190:(
3184:=
3166:,
3157:(
3142:,
3133:(
3127:(
3121:,
3115:(
3109:,
3103:(
3097:,
3091:(
3085:=
3082:S
3067:,
3061:(
3055:,
3049:(
3043:=
3040:K
3023:)
3020:t
3011:(
3008:a
3002:=
2999:t
2996:a
2973:)
2970:T
2964:)
2961:T
2958:,
2955:S
2952:(
2943:t
2940:G
2931:(
2925:t
2919:|
2916:)
2913:S
2907:)
2904:T
2901:,
2898:S
2895:(
2886:s
2883:G
2874:(
2868:s
2862:|
2859:)
2856:t
2853:G
2847:,
2844:s
2841:G
2835:(
2826:)
2823:t
2820:,
2817:s
2814:(
2808:|
2802:t
2799:G
2793:(
2790:S
2784:S
2775:s
2772:G
2763:(
2757:)
2754:t
2751:,
2748:s
2745:(
2739:|
2736:)
2733:s
2727:S
2724:,
2721:x
2718:(
2715:,
2712:G
2709:(
2703:(
2694:S
2688:(
2679:)
2676:s
2673:,
2670:x
2667:(
2661:|
2658:x
2655:G
2646:x
2637:t
2631:=
2628:t
2625:G
2613:x
2595:y
2592:=
2589:x
2583:=
2580:x
2571:,
2568:y
2565:(
2562:,
2556:(
2550:(
2538:)
2532:*
2526:(
2523:*
2511:|
2505:=
2475:)
2472:T
2469:,
2466:S
2463:(
2456:R
2453:I
2450:A
2447:P
2443:=
2430:t
2419:T
2416:=
2399:t
2392:d
2389:n
2386:s
2375:)
2372:T
2369:,
2366:S
2363:(
2356:R
2353:I
2350:A
2347:P
2343:=
2330:s
2319:S
2316:=
2299:s
2292:t
2289:s
2286:f
2275:)
2262:t
2256:,
2243:s
2237:(
2230:R
2227:I
2224:A
2221:P
2217:=
2200:)
2197:t
2194:,
2191:s
2188:(
2181:r
2178:i
2175:a
2172:p
2161:S
2154:M
2151:A
2148:L
2144:=
2131:s
2120:)
2107:t
2101:(
2095:S
2092:=
2075:)
2072:t
2069:,
2066:s
2063:(
2056:p
2053:p
2050:a
2039:)
2034:S
2028:x
2025:,
2014:s
2005:.
2002:S
1996:(
1989:M
1986:A
1983:L
1979:=
1962:)
1959:s
1956:,
1953:x
1950:(
1943:m
1940:a
1937:l
1926:)
1923:x
1920:(
1914:=
1897:x
1890:r
1887:a
1884:v
1863:Γ
1861:∥
1859:s
1855:s
1851:S
1847:s
1843:s
1839:S
1828:t
1825:=
1822:)
1819:t
1813:(
1804:(
1798:|
1795:)
1792:T
1789:b
1783:,
1780:S
1777:a
1771:(
1765:=
1759:T
1756:,
1753:S
1750:(
1744:(
1738:b
1735:,
1732:a
1729:(
1723:(
1717:|
1708:x
1702:(
1699:a
1693:(
1690:S
1687:(
1684:b
1678:,
1675:x
1672:(
1657:=
1654:x
1645:=
1642:)
1639:S
1633:(
1627:b
1624:,
1621:a
1618:(
1612:(
1600:t
1594:=
1591:t
1582:(
1576:|
1570:t
1564:(
1561:b
1552:t
1546:(
1543:a
1537:(
1531:=
1528:t
1522:b
1519:,
1516:a
1513:(
1507:(
1501:|
1495:S
1492:a
1486:(
1483:,
1480:t
1477:(
1471:(
1468:b
1459:S
1453:(
1447:=
1444:t
1438:b
1435:,
1432:a
1429:(
1423:(
1405:(
1399:.
1393:^
1387:;
1381:+
1378:1
1369:(
1366:=
1348:=
1315:)
1312:T
1305:2
1292:,
1289:S
1282:1
1269:(
1262:r
1259:i
1256:a
1253:p
1249:=
1242:)
1239:)
1236:T
1233:,
1230:S
1227:(
1220:R
1217:I
1214:A
1211:P
1207:(
1200:2
1187:1
1165:x
1157:)
1154:)
1151:)
1148:)
1145:x
1138:r
1135:a
1132:v
1128:(
1121:1
1108:(
1102:S
1099:(
1092:2
1079:,
1076:x
1073:(
1066:m
1063:a
1060:l
1056:=
1049:)
1046:S
1039:M
1036:A
1033:L
1029:(
1022:2
1009:1
992:t
989:=
982:)
979:t
972:N
969:Y
966:S
962:(
945:)
942:)
939:v
932:d
929:n
926:s
922:(
915:2
902:,
899:)
896:v
889:t
886:s
883:f
879:(
872:1
859:(
855:R
852:I
849:A
846:P
842:=
835:v
828:2
815:1
798:)
795:)
792:)
789:S
782:1
769:,
766:v
763:(
756:p
753:p
750:a
746:(
739:2
723:.
720:S
714:(
710:M
707:A
704:L
700:=
693:v
686:2
673:1
656:t
649:N
646:Y
643:S
639:=
632:t
597:τ
581:|
575:*
563:|
560:)
548:(
539:=
523:t
516:T
512:S
510:(
504:x
501:S
497:x
489:T
487:,
485:S
453:|
441:|
435:*
423:|
417:*
405:|
399:*
387:|
375:=
354:x
348:/
340:,
336:/
328:/
319:t
312:t
305:t
301:s
299:(
293:t
289:s
287:(
281:t
277:x
275:(
269:x
262:t
260:,
258:s
236:*
224:|
218:*
206:|
194:=
170:2
166:1
162:2
158:1
65:)
61:(
57:.
50:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.