1227:
727:
1222:{\displaystyle {\begin{aligned}&(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}}
2081:
1481:. There are only two possible ÎČ-reductions to be done here, on x and on y. Reducing the outer x term first results in the inner y term being duplicated, and each copy will have to be reduced, but reducing the inner y term first will duplicate its argument z, which will cause work to be duplicated when the values of h and w are made known.
1791:
2083:
The system can be proven to be confluent. Optimal reduction is then defined to be normal order or leftmost-outermost reduction using reduction by families, i.e. the parallel reduction of all redexes with the same function part label. The strategy is optimal in the sense that it performs the optimal
1377:. In fact, applicative order reduction was also originally introduced to model the call-by-value parameter passing technique found in Algol 60 and modern programming languages. When combined with the idea of weak reduction, the resulting call-by-value reduction is indeed a faithful approximation.
2103:
can be defined similarly to optimal reduction as weak leftmost-outermost reduction using parallel reduction of redexes with the same label, for a slightly different labelled lambda calculus. An alternate definition changes the beta rule to an operation that finds the next "needed" computation,
1380:
Unfortunately, weak reduction is not confluent, and the traditional reduction equations of the lambda calculus are useless, because they suggest relationships that violate the weak evaluation regime. However, it is possible to extend the system to be confluent by allowing a restricted form of
2104:
evaluates it, and substitutes the result into all locations. This requires extending the beta rule to allow reducing terms that are not syntactically adjacent. As with call-by-name and call-by-value, call-by-need reduction was devised to mimic the behavior of the
2087:
A practical algorithm for optimal reduction was first described in 1989, more than a decade after optimal reduction was first defined in 1974. The
Bologna Optimal Higher-order Machine (BOHM) is a prototype implementation of an extension of the technique to
723:
refers to leftmost-innermost reduction. In contrast to normal order, applicative order reduction may not terminate, even when the term has a normal form. For example, using applicative order reduction, the following sequence of reductions is possible:
562:
for all almost-orthogonal term rewriting systems, meaning that these strategies will eventually reach a normal form if it exists, even when performing (finitely many) arbitrary reductions between successive applications of the strategy.
1676:
2076:{\displaystyle {\begin{aligned}x^{\alpha }&=\alpha \cdot N&\quad (\lambda y.M)^{\alpha }&=(\lambda y.M)^{\alpha }\\y^{\alpha }&=y^{\alpha }&\quad (MN)^{\alpha }&=(MN)^{\alpha }\end{aligned}}}
1484:
Optimal reduction is not a reduction strategy for the lambda calculus in a narrow sense because performing ÎČ-reduction loses the information about the substituted redexes being shared. Instead it is defined for the
1320:
596:. Normal-order reduction is normalizing, in the sense that if a term has a normal form, then normalâorder reduction will eventually reach it, hence the name normal. This is known as the standardization theorem.
606:
the notions coincide, and similarly the leftmost-outermost redex is the redex with leftmost starting character when the lambda term is considered as a string of characters. When "leftmost" is defined using an
1569:
of labels. A labelled term is a lambda calculus term where each subterm has a label. The standard initial labeling of a lambda term gives each subterm a unique atomic label. Labelled ÎČ-reduction is given by:
1747:
174:
2216:
1796:
732:
665:
343:
1463:
Optimal reduction is motivated by the existence of lambda terms where there does not exist a sequence of reductions which reduces them without duplicating work. For example, consider
1373:
is the weak reduction strategy that reduces the leftmost innermost redex not inside a lambda abstraction. These strategies were devised to reflect the call-by-name and call-by-value
380:
201:
1573:
1567:
1540:
1342:
501:
691:
418:
110:
83:
38:
or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an
715:
1698:
448:
291:
225:
227:(but not the reflexive closure). In addition the normal forms of the strategy must be the same as the normal forms of the original rewriting system, i.e. for all
1513:
1782:
468:
265:
245:
134:
1234:
17:
537:
leftmost-outermost: in each step the leftmost of the outermost redexes is contracted, where an outermost redex is a redex not contained in any redexes
534:
leftmost-innermost: in each step the leftmost of the innermost redexes is contracted, where an innermost redex is a redex not containing any redexes
2555:
2759:
Processes, Terms and Cycles: Steps on the Road to
Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday
1381:
reduction under an abstraction, in particular when the redex does not involve the variable bound by the abstraction. For example,
548:
parallel-innermost: reduces all innermost redexes simultaneously. This is well-defined because the redexes are pairwise disjoint.
1703:
3149:
3007:
2784:
2565:
2367:
2226:
554:
Gross-Knuth reduction, also called full substitution or Kleene reduction: all redexes in the term are simultaneously reduced
139:
3024:
2844:
1361:
Normal and applicative order reduction are strong in that they allow reduction under lambda abstractions. In contrast,
614:
2816:
2597:
2452:
Barendregt, H. P.; Eekelen, M. C. J. D.; Glauert, J. R. W.; Kennaway, J. R.; Plasmeijer, M. J.; Sleep, M. R. (1987).
2317:
2273:
1324:
2861:
2688:
2923:
FernĂĄndez, Maribel; Siafakas, Nikolaos (30 March 2010). "Labelled Lambda-calculi with
Explicit Copy and Erase".
1369:
is the weak reduction strategy that reduces the leftmost outermost redex not inside a lambda abstraction, while
2982:
2977:. Second Franco-Japanese Symposium on Programming of Future Generation Computers. Cannes, France. p. 187.
2904:
355:
296:
1349:
refers to the nondeterministic one-step strategy that allows reducing any redex at each step. Takahashi's
179:
2218:
Logic, Rewriting, and
Concurrency: Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday
2476:
3191:
3032:. 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90. pp. 16â30.
2426:
1545:
579:
1518:
51:
2350:
3196:
2809:
The
Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones
2767:
567:
2154:, and is constructed by making wrappers which make the identity function available to the binders
1489:, an annotated lambda calculus which captures a precise notion of the work that should be shared.
3106:
2696:. 1st International Conference on Formal Structures for Computation and Deduction. p. 32:3.
2092:. Lambdascope is a more recent implementation of optimal reduction, also using interaction nets.
2801:
2757:
Blanc, Tomasz; LĂ©vy, Jean-Jacques; Maranget, Luc (2005). "Sharing in the Weak Lambda-Calculus".
694:
473:
2762:
2345:
670:
396:
88:
56:
2303:
1785:
700:
516:
1683:
427:
270:
2250:
1231:
But using normal-order reduction, the same starting point reduces quickly to normal form:
210:
8:
3176:
2126:
2105:
1671:{\displaystyle ((\lambda x.M)^{\alpha }N)^{\beta }\to \beta {\overline {\alpha }}\cdot M}
1374:
603:
39:
2811:. Lecture Notes in Computer Science. Vol. 2566. Springer-Verlag. pp. 420â435.
1495:
3155:
3052:
2950:
2932:
2660:
2299:
1752:
608:
453:
250:
230:
204:
119:
2534:
2517:
3145:
3126:
3061:
3003:
2978:
2900:
2840:
2812:
2780:
2593:
2561:
2495:
2363:
2313:
2269:
2222:
2954:
2614:
2183:
A summary of recent research on optimal reduction can be found in the short article
3159:
3137:
3033:
2942:
2870:
2772:
2730:
2697:
2529:
2491:
2457:
2355:
2261:
2121:
2089:
1434:
can still be reduced under the extended weak reduction strategy, because the redex
421:
27:
Relation specifying a rewrite for each object, compatible with a reduction relation
2393:
2334:
2969:
2265:
2109:
585:
113:
3141:
2875:
2702:
2456:. Parallel Architectures and Languages Europe. Vol. 259. pp. 141â158.
2359:
1492:
Labels consist of a countably infinite set of atomic labels, and concatenations
2869:. 24th International Conference on Types for Proofs and Programs (TYPES 2018).
2212:
2640:
3185:
3065:
2581:
2461:
2735:
2718:
2215:. In MartĂ-Oliet, Narciso; Ălveczky, Peter Csaba; Talcott, Carolyn (eds.).
3108:] (Lambdascope): Another optimal implementation of the lambda-calculus
3105:
van
Oostrom, Vincent; van de Looij, Kees-Jan; Zwitserlood, Marijn (2004).
2585:
2554:
Mazzola, Guerino; Milmeister, GĂ©rard; Weissmann, Jody (21 October 2004).
3037:
1315:{\displaystyle (\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))}
3136:. Lecture Notes in Computer Science. Vol. 7211. pp. 128â147.
2946:
2776:
3087:
2344:. Lecture Notes in Computer Science. Vol. 4600. pp. 89â112.
1466:((λg.(g(g(λx.x)))) (λh.((λf.(f(f(λz.z)))) (λw.(h(w(λy.y)))))))
2333:
Klop, Jan Willem; van
Oostrom, Vincent; van Raamsdonk, Femke (2007).
2309:
2184:
1353:
is the strategy that reduces all redexes in the term simultaneously.
31:
2937:
519:
a rewriting strategy specifies, out of all the reducible subterms (
3104:
1400:
is in normal form for a weak reduction strategy because the redex
570:
designed specifically for programming term rewriting strategies.
2451:
602:
is sometimes used to refer to normal order reduction, as with a
3114:. Workshop on Algebra and Logic on Programming Systems (ALPS).
2897:
The optimal implementation of functional programming languages
2150:
Incidentally, the above term reduces to the identity function
2131:
717:
while the leftmost-outermost redex is the entire expression.
520:
2332:
2863:
Normalization by
Evaluation for Typed Weak lambda-Reduction
2592:. Vol. I. Amsterdam: North Holland. pp. 139â142.
2170:(at first), all of which are applied to the innermost term
3060:(PhD) (in French). UniversitĂ© Paris VII. pp. 81â109.
3002:. Cambridge, UK: Cambridge University Press. p. 518.
2553:
592:
refers to leftmost-outermost reduction in the sense given
1742:{\displaystyle \beta \cdot T^{\alpha }=T^{\beta \alpha }}
2807:. In Mogensen, T; Schmidt, D; Sudborough, I. H. (eds.).
2925:
2642:
Non-Idempotent Typing
Operators, beyond the λ-Calculus
2615:"A Proof of the Standardization Theorem in λ-Calculus"
2560:. Springer Science & Business Media. p. 323.
1365:
reduction does not reduce under a lambda abstraction.
169:{\displaystyle \to _{S}\subseteq {\overset {+}{\to }}}
2213:"Rewriting Strategies and Strategic Rewrite Programs"
1794:
1755:
1706:
1686:
1576:
1548:
1521:
1498:
1327:
1237:
730:
703:
673:
617:
476:
456:
430:
399:
358:
299:
273:
253:
233:
213:
182:
142:
122:
91:
59:
3088:"Bologna Optimal Higher-Order Machine, Version 1.1"
2557:
Comprehensive Mathematics for Computer Scientists 2
1415:is contained in a lambda abstraction. But the term
611:the notions are distinct. For example, in the term
540:
rightmost-innermost, rightmost-outermost: similarly
3026:An algorithm for optimal lambda calculus reduction
2668:(PhD). University of North Carolina at Chapel Hill
2475:Antoy, Sergio; Middeldorp, Aart (September 1996).
2075:
1776:
1741:
1692:
1670:
1561:
1534:
1507:
1336:
1314:
1221:
709:
697:, the leftmost redex of the in-order traversal is
685:
659:
495:
462:
442:
412:
374:
337:
285:
259:
239:
219:
195:
168:
128:
104:
77:
2922:
2756:
2686:
660:{\displaystyle (\lambda x.x\Omega )(\lambda y.I)}
558:Parallel outermost and Gross-Knuth reduction are
3183:
2687:Van Oostrom, Vincent; Toyama, Yoshihito (2016).
2522:Electronic Notes in Theoretical Computer Science
530:One-step strategies for term rewriting include:
2971:Sharing in the Evaluation of lambda Expressions
2894:
2474:
2248:
3124:
2752:
2750:
2748:
2746:
3127:"The Call-by-Need Lambda Calculus, Revisited"
2899:. Cambridge, UK: Cambridge University Press.
2185:About the efficient reduction of lambda terms
3125:Chang, Stephen; Felleisen, Matthias (2012).
2918:
2916:
2830:
2828:
2084:(minimal) number of family reduction steps.
2895:Asperti, Andrea; Guerrini, Stefano (1998).
2839:. Cambridge, Mass.: MIT Press. p. 42.
2743:
580:Lambda calculus § Reduction strategies
2890:
2888:
2886:
2549:
2547:
2545:
2258:Semantic Techniques in Quantum Computation
2206:
2204:
2968:LĂ©vy, Jean-Jacques (9â11 November 1987).
2936:
2913:
2874:
2834:
2825:
2802:"Demonstrating Lambda Calculus Reduction"
2766:
2734:
2716:
2701:
2580:
2533:
2420:
2418:
2349:
2249:Selinger, Peter; Valiron, BenoĂźt (2009).
2095:
2515:
2401:Papers by Nachum Dershowitz and students
2294:
2292:
2210:
3022:
2883:
2859:
2799:
2658:
2648:(PhD). Sorbonne Paris Cité. p. 62.
2542:
2201:
14:
3184:
3054:RĂ©ductions sures dans le lambda-calcul
2997:
2516:Kieburtz, Richard B. (November 2001).
2415:
2387:
2385:
2383:
2381:
2379:
2298:
1469:It is composed of three nested terms,
375:{\displaystyle \to _{S}\subseteq \to }
338:{\displaystyle \exists b'.a\to _{S}b'}
2659:Partain, William D. (December 1989).
2335:"Reduction Strategies and Acyclicity"
2289:
3050:
3044:
2967:
2837:Semantics engineering with PLT Redex
2638:
1458:
196:{\displaystyle {\overset {+}{\to }}}
18:Reduction strategy (lambda calculus)
3177:Lambda calculus reduction workbench
3085:
2719:"Parallel Reductions in λ-Calculus"
2612:
2424:
2376:
2211:Kirchner, HĂ©lĂšne (26 August 2015).
593:
24:
2518:"A Logic for Rewriting Strategies"
704:
674:
633:
573:
300:
25:
3208:
3170:
3134:Programming Languages and Systems
2477:"A sequential reduction strategy"
2433:. University of Wisconsin Madison
2403:. Tel Aviv University. p. 77
1784:is defined as follows (using the
1356:
510:
3051:LĂ©vy, Jean-Jacques (June 1974).
2662:Graph Reduction Without Pointers
2639:Vial, Pierre (7 December 2017).
2391:
2342:Rewriting, Computation and Proof
1562:{\displaystyle {\underline {a}}}
523:), which one should be reduced (
352:reduction strategy is one where
3118:
3098:
3079:
3016:
2991:
2961:
2853:
2793:
2710:
2690:Normalisation by Random Descent
2680:
2652:
2632:
2620:. Tokyo Institute of Technology
2606:
2574:
2305:Types and Programming Languages
2177:
2144:
1978:
1842:
1535:{\displaystyle {\overline {a}}}
2509:
2468:
2445:
2326:
2242:
2060:
2056:
2050:
2044:
2038:
2032:
2026:
2020:
2010:
2004:
1998:
1989:
1979:
1956:
1950:
1944:
1921:
1917:
1911:
1905:
1890:
1880:
1874:
1868:
1859:
1843:
1821:
1815:
1809:
1771:
1765:
1759:
1665:
1646:
1640:
1618:
1609:
1596:
1580:
1577:
1328:
1309:
1306:
1285:
1282:
1261:
1258:
1255:
1238:
1202:
1199:
1178:
1175:
1154:
1151:
1130:
1127:
1106:
1103:
1082:
1079:
1076:
1061:
1054:
1047:
1044:
1023:
1020:
999:
996:
975:
972:
951:
948:
945:
930:
923:
916:
913:
892:
889:
868:
865:
844:
841:
838:
823:
816:
809:
806:
785:
782:
761:
758:
755:
738:
654:
639:
636:
618:
544:Many-step strategies include:
481:
401:
360:
318:
277:
214:
185:
158:
144:
93:
72:
69:
60:
45:
13:
1:
2535:10.1016/S1571-0661(04)00283-X
2194:
1337:{\displaystyle \rightarrow z}
551:parallel-outermost: similarly
2835:Felleisen, Matthias (2009).
2761:. Springer. pp. 70â87.
2717:Takahashi, M. (April 1995).
2496:10.1016/0304-3975(96)00041-2
2484:Theoretical Computer Science
2266:10.1017/CBO9781139193313.005
1629:
1527:
7:
3142:10.1007/978-3-642-28869-2_7
2876:10.4230/LIPIcs.TYPES.2018.6
2723:Information and Computation
2703:10.4230/LIPIcs.FSCD.2016.32
2360:10.1007/978-3-540-73147-4_5
2115:
2108:known as "call-by-need" or
721:Applicative order reduction
10:
3213:
577:
496:{\displaystyle a\to _{S}b}
2860:Sestini, Filippo (2019).
2251:"Quantum Lambda Calculus"
686:{\displaystyle \Omega ,I}
52:abstract rewriting system
2394:"Term Rewriting Systems"
2137:
1487:labelled lambda calculus
568:domain-specific language
413:{\displaystyle \to _{S}}
105:{\displaystyle \to _{S}}
78:{\displaystyle (A,\to )}
2800:Sestoft, Peter (2002).
2462:10.1007/3-540-17945-3_8
1371:call-by-value reduction
710:{\displaystyle \Omega }
85:, a reduction strategy
3023:Lamping, John (1990).
3000:Term rewriting systems
2736:10.1006/inco.1995.1057
2101:Call by need reduction
2096:Call by need reduction
2077:
1778:
1743:
1694:
1693:{\displaystyle \cdot }
1672:
1563:
1536:
1509:
1367:Call-by-name reduction
1338:
1316:
1223:
711:
687:
661:
590:normal-order reduction
584:In the context of the
497:
464:
444:
443:{\displaystyle a\in A}
414:
393:strategy is one where
376:
339:
287:
286:{\displaystyle a\to b}
261:
241:
221:
197:
170:
130:
106:
79:
2078:
1786:Barendregt convention
1779:
1744:
1700:concatenates labels,
1695:
1673:
1564:
1537:
1510:
1475:y=((λf. ...) (λw.z) )
1471:x=((λg. ... ) (λh.y))
1375:evaluation strategies
1339:
1317:
1224:
712:
688:
662:
517:term rewriting system
498:
465:
450:there is at most one
445:
415:
377:
340:
288:
262:
242:
222:
198:
171:
131:
107:
80:
2454:Term graph rewriting
1792:
1753:
1704:
1684:
1574:
1546:
1519:
1496:
1351:parallel ÎČ-reduction
1325:
1235:
728:
701:
671:
615:
503:. Otherwise it is a
474:
454:
428:
397:
382:. Otherwise it is a
356:
297:
271:
251:
231:
220:{\displaystyle \to }
211:
180:
140:
120:
89:
57:
3038:10.1145/96709.96711
2300:Pierce, Benjamin C.
2127:Reduction semantics
2106:evaluation strategy
1749:, and substitution
604:pre-order traversal
40:evaluation strategy
2947:10.4204/EPTCS.22.5
2777:10.1007/11601548_7
2425:Horwitz, Susan B.
2073:
2071:
1774:
1739:
1690:
1668:
1657:
1559:
1557:
1532:
1508:{\displaystyle ab}
1505:
1449:does not refer to
1334:
1312:
1219:
1217:
707:
683:
657:
609:in-order traversal
600:Leftmost reduction
493:
460:
440:
410:
372:
370:⊆ →
335:
283:
257:
237:
217:
205:transitive closure
193:
166:
126:
102:
75:
36:reduction strategy
3192:Rewriting systems
3151:978-3-642-28868-5
3086:Asperti, Andrea.
3009:978-0-521-39115-3
2786:978-3-540-32425-6
2590:Combinatory Logic
2582:Curry, Haskell B.
2567:978-3-540-20861-7
2427:"Lambda Calculus"
2369:978-3-540-73146-7
2228:978-3-319-23165-5
1777:{\displaystyle M}
1650:
1632:
1550:
1542:and underlinings
1530:
1479:z=λw.(h(w(λy.y)))
1459:Optimal reduction
527:) within a term.
463:{\displaystyle b}
260:{\displaystyle b}
247:, there exists a
240:{\displaystyle a}
191:
164:
129:{\displaystyle A}
50:Formally, for an
16:(Redirected from
3204:
3164:
3163:
3131:
3122:
3116:
3115:
3113:
3102:
3096:
3095:
3083:
3077:
3076:
3074:
3072:
3059:
3048:
3042:
3041:
3031:
3020:
3014:
3013:
2995:
2989:
2988:
2976:
2965:
2959:
2958:
2940:
2920:
2911:
2910:
2892:
2881:
2880:
2878:
2868:
2857:
2851:
2850:
2832:
2823:
2822:
2806:
2797:
2791:
2790:
2770:
2754:
2741:
2740:
2738:
2714:
2708:
2707:
2705:
2695:
2684:
2678:
2677:
2675:
2673:
2667:
2656:
2650:
2649:
2647:
2636:
2630:
2629:
2627:
2625:
2619:
2610:
2604:
2603:
2578:
2572:
2571:
2551:
2540:
2539:
2537:
2513:
2507:
2506:
2504:
2502:
2481:
2472:
2466:
2465:
2449:
2443:
2442:
2440:
2438:
2422:
2413:
2412:
2410:
2408:
2398:
2389:
2374:
2373:
2353:
2339:
2330:
2324:
2323:
2296:
2287:
2286:
2284:
2282:
2255:
2246:
2240:
2239:
2237:
2235:
2208:
2188:
2181:
2175:
2173:
2169:
2166:(at first), and
2165:
2161:
2157:
2153:
2148:
2122:Reduction system
2090:interaction nets
2082:
2080:
2079:
2074:
2072:
2068:
2067:
1997:
1996:
1975:
1974:
1943:
1942:
1929:
1928:
1867:
1866:
1808:
1807:
1783:
1781:
1780:
1775:
1748:
1746:
1745:
1740:
1738:
1737:
1722:
1721:
1699:
1697:
1696:
1691:
1677:
1675:
1674:
1669:
1658:
1633:
1625:
1617:
1616:
1604:
1603:
1568:
1566:
1565:
1560:
1558:
1541:
1539:
1538:
1533:
1531:
1523:
1514:
1512:
1511:
1506:
1480:
1476:
1472:
1454:
1448:
1433:
1414:
1399:
1347:Full ÎČ-reduction
1343:
1341:
1340:
1335:
1321:
1319:
1318:
1313:
1245:
1228:
1226:
1225:
1220:
1218:
1208:
745:
734:
716:
714:
713:
708:
692:
690:
689:
684:
666:
664:
663:
658:
560:hypernormalizing
505:nondeterministic
502:
500:
499:
494:
489:
488:
469:
467:
466:
461:
449:
447:
446:
441:
424:, i.e. for each
422:partial function
419:
417:
416:
411:
409:
408:
381:
379:
378:
373:
368:
367:
344:
342:
341:
336:
334:
326:
325:
310:
292:
290:
289:
284:
266:
264:
263:
258:
246:
244:
243:
238:
226:
224:
223:
218:
202:
200:
199:
194:
192:
184:
175:
173:
172:
167:
165:
157:
152:
151:
135:
133:
132:
127:
111:
109:
108:
103:
101:
100:
84:
82:
81:
76:
21:
3212:
3211:
3207:
3206:
3205:
3203:
3202:
3201:
3197:Lambda calculus
3182:
3181:
3173:
3168:
3167:
3152:
3129:
3123:
3119:
3111:
3103:
3099:
3084:
3080:
3070:
3068:
3057:
3049:
3045:
3029:
3021:
3017:
3010:
2998:Terese (2003).
2996:
2992:
2985:
2974:
2966:
2962:
2921:
2914:
2907:
2893:
2884:
2866:
2858:
2854:
2847:
2833:
2826:
2819:
2804:
2798:
2794:
2787:
2755:
2744:
2715:
2711:
2693:
2685:
2681:
2671:
2669:
2665:
2657:
2653:
2645:
2637:
2633:
2623:
2621:
2617:
2611:
2607:
2600:
2579:
2575:
2568:
2552:
2543:
2514:
2510:
2500:
2498:
2479:
2473:
2469:
2450:
2446:
2436:
2434:
2423:
2416:
2406:
2404:
2396:
2390:
2377:
2370:
2351:10.1.1.104.9139
2337:
2331:
2327:
2320:
2297:
2290:
2280:
2278:
2276:
2253:
2247:
2243:
2233:
2231:
2229:
2209:
2202:
2197:
2192:
2191:
2182:
2178:
2171:
2167:
2163:
2159:
2155:
2151:
2149:
2145:
2140:
2118:
2110:lazy evaluation
2098:
2070:
2069:
2063:
2059:
2013:
1992:
1988:
1976:
1970:
1966:
1959:
1938:
1934:
1931:
1930:
1924:
1920:
1883:
1862:
1858:
1840:
1824:
1803:
1799:
1795:
1793:
1790:
1789:
1754:
1751:
1750:
1730:
1726:
1717:
1713:
1705:
1702:
1701:
1685:
1682:
1681:
1649:
1624:
1612:
1608:
1599:
1595:
1575:
1572:
1571:
1549:
1547:
1544:
1543:
1522:
1520:
1517:
1516:
1497:
1494:
1493:
1478:
1474:
1470:
1467:
1461:
1450:
1435:
1416:
1401:
1382:
1359:
1326:
1323:
1322:
1241:
1236:
1233:
1232:
1216:
1215:
1206:
1205:
1057:
1051:
1050:
926:
920:
919:
819:
813:
812:
741:
731:
729:
726:
725:
702:
699:
698:
672:
669:
668:
616:
613:
612:
586:lambda calculus
582:
576:
574:Lambda calculus
513:
484:
480:
475:
472:
471:
455:
452:
451:
429:
426:
425:
404:
400:
398:
395:
394:
363:
359:
357:
354:
353:
327:
321:
317:
303:
298:
295:
294:
272:
269:
268:
252:
249:
248:
232:
229:
228:
212:
209:
208:
183:
181:
178:
177:
156:
147:
143:
141:
138:
137:
121:
118:
117:
114:binary relation
96:
92:
90:
87:
86:
58:
55:
54:
48:
28:
23:
22:
15:
12:
11:
5:
3210:
3200:
3199:
3194:
3180:
3179:
3172:
3171:External links
3169:
3166:
3165:
3150:
3117:
3097:
3078:
3043:
3015:
3008:
2990:
2983:
2960:
2912:
2905:
2882:
2852:
2846:978-0262062756
2845:
2824:
2817:
2792:
2785:
2768:10.1.1.129.147
2742:
2729:(1): 120â127.
2709:
2679:
2651:
2631:
2613:Kashima, Ryo.
2605:
2598:
2573:
2566:
2541:
2528:(2): 138â154.
2508:
2467:
2444:
2414:
2375:
2368:
2325:
2318:
2312:. p. 56.
2288:
2274:
2241:
2227:
2199:
2198:
2196:
2193:
2190:
2189:
2176:
2142:
2141:
2139:
2136:
2135:
2134:
2129:
2124:
2117:
2114:
2097:
2094:
2066:
2062:
2058:
2055:
2052:
2049:
2046:
2043:
2040:
2037:
2034:
2031:
2028:
2025:
2022:
2019:
2016:
2014:
2012:
2009:
2006:
2003:
2000:
1995:
1991:
1987:
1984:
1981:
1977:
1973:
1969:
1965:
1962:
1960:
1958:
1955:
1952:
1949:
1946:
1941:
1937:
1933:
1932:
1927:
1923:
1919:
1916:
1913:
1910:
1907:
1904:
1901:
1898:
1895:
1892:
1889:
1886:
1884:
1882:
1879:
1876:
1873:
1870:
1865:
1861:
1857:
1854:
1851:
1848:
1845:
1841:
1839:
1836:
1833:
1830:
1827:
1825:
1823:
1820:
1817:
1814:
1811:
1806:
1802:
1798:
1797:
1773:
1770:
1767:
1764:
1761:
1758:
1736:
1733:
1729:
1725:
1720:
1716:
1712:
1709:
1689:
1667:
1664:
1661:
1656:
1653:
1648:
1645:
1642:
1639:
1636:
1631:
1628:
1623:
1620:
1615:
1611:
1607:
1602:
1598:
1594:
1591:
1588:
1585:
1582:
1579:
1556:
1553:
1529:
1526:
1515:, overlinings
1504:
1501:
1465:
1460:
1457:
1358:
1357:Weak reduction
1355:
1333:
1330:
1311:
1308:
1305:
1302:
1299:
1296:
1293:
1290:
1287:
1284:
1281:
1278:
1275:
1272:
1269:
1266:
1263:
1260:
1257:
1254:
1251:
1248:
1244:
1240:
1214:
1211:
1209:
1207:
1204:
1201:
1198:
1195:
1192:
1189:
1186:
1183:
1180:
1177:
1174:
1171:
1168:
1165:
1162:
1159:
1156:
1153:
1150:
1147:
1144:
1141:
1138:
1135:
1132:
1129:
1126:
1123:
1120:
1117:
1114:
1111:
1108:
1105:
1102:
1099:
1096:
1093:
1090:
1087:
1084:
1081:
1078:
1075:
1072:
1069:
1066:
1063:
1060:
1058:
1056:
1053:
1052:
1049:
1046:
1043:
1040:
1037:
1034:
1031:
1028:
1025:
1022:
1019:
1016:
1013:
1010:
1007:
1004:
1001:
998:
995:
992:
989:
986:
983:
980:
977:
974:
971:
968:
965:
962:
959:
956:
953:
950:
947:
944:
941:
938:
935:
932:
929:
927:
925:
922:
921:
918:
915:
912:
909:
906:
903:
900:
897:
894:
891:
888:
885:
882:
879:
876:
873:
870:
867:
864:
861:
858:
855:
852:
849:
846:
843:
840:
837:
834:
831:
828:
825:
822:
820:
818:
815:
814:
811:
808:
805:
802:
799:
796:
793:
790:
787:
784:
781:
778:
775:
772:
769:
766:
763:
760:
757:
754:
751:
748:
744:
740:
737:
735:
733:
706:
682:
679:
676:
656:
653:
650:
647:
644:
641:
638:
635:
632:
629:
626:
623:
620:
575:
572:
566:Stratego is a
556:
555:
552:
549:
542:
541:
538:
535:
512:
511:Term rewriting
509:
492:
487:
483:
479:
459:
439:
436:
433:
407:
403:
371:
366:
362:
333:
330:
324:
320:
316:
313:
309:
306:
302:
282:
279:
276:
256:
236:
216:
190:
187:
163:
160:
155:
150:
146:
125:
99:
95:
74:
71:
68:
65:
62:
47:
44:
26:
9:
6:
4:
3:
2:
3209:
3198:
3195:
3193:
3190:
3189:
3187:
3178:
3175:
3174:
3161:
3157:
3153:
3147:
3143:
3139:
3135:
3128:
3121:
3110:
3109:
3101:
3093:
3089:
3082:
3067:
3063:
3056:
3055:
3047:
3039:
3035:
3028:
3027:
3019:
3011:
3005:
3001:
2994:
2986:
2980:
2973:
2972:
2964:
2956:
2952:
2948:
2944:
2939:
2934:
2930:
2926:
2919:
2917:
2908:
2902:
2898:
2891:
2889:
2887:
2877:
2872:
2865:
2864:
2856:
2848:
2842:
2838:
2831:
2829:
2820:
2818:3-540-00326-6
2814:
2810:
2803:
2796:
2788:
2782:
2778:
2774:
2769:
2764:
2760:
2753:
2751:
2749:
2747:
2737:
2732:
2728:
2724:
2720:
2713:
2704:
2699:
2692:
2691:
2683:
2664:
2663:
2655:
2644:
2643:
2635:
2616:
2609:
2601:
2599:0-7204-2208-6
2595:
2591:
2587:
2583:
2577:
2569:
2563:
2559:
2558:
2550:
2548:
2546:
2536:
2531:
2527:
2523:
2519:
2512:
2497:
2493:
2489:
2485:
2478:
2471:
2463:
2459:
2455:
2448:
2432:
2428:
2421:
2419:
2402:
2395:
2388:
2386:
2384:
2382:
2380:
2371:
2365:
2361:
2357:
2352:
2347:
2343:
2336:
2329:
2321:
2319:0-262-16209-1
2315:
2311:
2307:
2306:
2301:
2295:
2293:
2277:
2275:9780521513746
2271:
2267:
2263:
2259:
2252:
2245:
2230:
2224:
2220:
2219:
2214:
2207:
2205:
2200:
2186:
2180:
2147:
2143:
2133:
2130:
2128:
2125:
2123:
2120:
2119:
2113:
2111:
2107:
2102:
2093:
2091:
2085:
2064:
2053:
2047:
2041:
2035:
2029:
2023:
2017:
2015:
2007:
2001:
1993:
1985:
1982:
1971:
1967:
1963:
1961:
1953:
1947:
1939:
1935:
1925:
1914:
1908:
1902:
1899:
1896:
1893:
1887:
1885:
1877:
1871:
1863:
1855:
1852:
1849:
1846:
1837:
1834:
1831:
1828:
1826:
1818:
1812:
1804:
1800:
1787:
1768:
1762:
1756:
1734:
1731:
1727:
1723:
1718:
1714:
1710:
1707:
1687:
1678:
1662:
1659:
1654:
1651:
1643:
1637:
1634:
1626:
1621:
1613:
1605:
1600:
1592:
1589:
1586:
1583:
1554:
1551:
1524:
1502:
1499:
1490:
1488:
1482:
1464:
1456:
1453:
1447:
1443:
1439:
1432:
1428:
1424:
1420:
1413:
1409:
1405:
1398:
1394:
1390:
1386:
1378:
1376:
1372:
1368:
1364:
1354:
1352:
1348:
1344:
1331:
1303:
1300:
1297:
1294:
1291:
1288:
1279:
1276:
1273:
1270:
1267:
1264:
1252:
1249:
1246:
1242:
1229:
1212:
1210:
1196:
1193:
1190:
1187:
1184:
1181:
1172:
1169:
1166:
1163:
1160:
1157:
1148:
1145:
1142:
1139:
1136:
1133:
1124:
1121:
1118:
1115:
1112:
1109:
1100:
1097:
1094:
1091:
1088:
1085:
1073:
1070:
1067:
1064:
1059:
1041:
1038:
1035:
1032:
1029:
1026:
1017:
1014:
1011:
1008:
1005:
1002:
993:
990:
987:
984:
981:
978:
969:
966:
963:
960:
957:
954:
942:
939:
936:
933:
928:
910:
907:
904:
901:
898:
895:
886:
883:
880:
877:
874:
871:
862:
859:
856:
853:
850:
847:
835:
832:
829:
826:
821:
803:
800:
797:
794:
791:
788:
779:
776:
773:
770:
767:
764:
752:
749:
746:
742:
736:
722:
718:
696:
680:
677:
651:
648:
645:
642:
630:
627:
624:
621:
610:
605:
601:
597:
595:
591:
587:
581:
571:
569:
564:
561:
553:
550:
547:
546:
545:
539:
536:
533:
532:
531:
528:
526:
522:
518:
508:
506:
490:
485:
477:
457:
437:
434:
431:
423:
405:
392:
391:deterministic
387:
385:
369:
364:
351:
346:
331:
328:
322:
314:
311:
307:
304:
280:
274:
254:
234:
206:
188:
161:
153:
148:
123:
115:
97:
66:
63:
53:
43:
41:
37:
33:
19:
3133:
3120:
3107:
3100:
3091:
3081:
3069:. Retrieved
3053:
3046:
3025:
3018:
2999:
2993:
2970:
2963:
2928:
2924:
2896:
2862:
2855:
2836:
2808:
2795:
2758:
2726:
2722:
2712:
2689:
2682:
2670:. Retrieved
2661:
2654:
2641:
2634:
2622:. Retrieved
2608:
2589:
2586:Feys, Robert
2576:
2556:
2525:
2521:
2511:
2499:. Retrieved
2490:(1): 75â95.
2487:
2483:
2470:
2453:
2447:
2435:. Retrieved
2430:
2405:. Retrieved
2400:
2392:Klop, J. W.
2341:
2328:
2304:
2279:. Retrieved
2257:
2244:
2232:. Retrieved
2221:. Springer.
2217:
2179:
2146:
2100:
2099:
2086:
1679:
1491:
1486:
1483:
1468:
1462:
1451:
1445:
1441:
1437:
1430:
1426:
1422:
1418:
1411:
1407:
1403:
1396:
1392:
1388:
1384:
1379:
1370:
1366:
1362:
1360:
1350:
1346:
1345:
1230:
720:
719:
599:
598:
589:
583:
565:
559:
557:
543:
529:
524:
514:
504:
390:
388:
383:
349:
347:
49:
35:
29:
2938:1003.5515v1
2501:8 September
2431:CS704 Notes
46:Definitions
3186:Categories
2984:0444705260
2906:0521621127
2672:10 January
2195:References
578:See also:
525:contracted
507:strategy.
470:such that
386:strategy.
3071:17 August
3066:476040273
2931:: 49â64.
2763:CiteSeerX
2624:19 August
2437:19 August
2407:14 August
2346:CiteSeerX
2310:MIT Press
2281:21 August
2234:14 August
2065:α
2051:↦
2033:↦
2005:↦
1994:α
1972:α
1951:↦
1940:α
1926:α
1912:↦
1894:λ
1875:↦
1864:α
1847:λ
1835:⋅
1832:α
1816:↦
1805:α
1766:↦
1735:α
1732:β
1719:α
1711:⋅
1708:β
1688:⋅
1660:⋅
1655:_
1652:α
1647:↦
1635:⋅
1630:¯
1627:α
1622:β
1619:→
1614:β
1601:α
1584:λ
1555:_
1528:¯
1329:→
1289:λ
1265:λ
1243:λ
1213:…
1182:λ
1158:λ
1134:λ
1110:λ
1086:λ
1065:λ
1055:→
1027:λ
1003:λ
979:λ
955:λ
934:λ
924:→
896:λ
872:λ
848:λ
827:λ
817:→
789:λ
765:λ
743:λ
705:Ω
675:Ω
643:λ
634:Ω
622:λ
482:→
435:∈
402:→
384:many step
361:→
319:→
301:∃
278:→
215:→
186:→
159:→
154:⊆
145:→
94:→
70:→
32:rewriting
2955:15500633
2588:(1958).
2302:(2002).
2116:See also
693:defined
350:one step
332:′
308:′
176:, where
3160:6350826
2160:f=λw...
2156:g=λh...
521:redexes
203:is the
3158:
3148:
3092:GitHub
3064:
3006:
2981:
2953:
2903:
2843:
2815:
2783:
2765:
2596:
2564:
2366:
2348:
2316:
2272:
2260:: 23.
2225:
2168:w=λz.z
2164:h=λx.x
2152:(λy.y)
1680:where
1477:, and
3156:S2CID
3130:(PDF)
3112:(PDF)
3058:(PDF)
3030:(PDF)
2975:(PDF)
2951:S2CID
2933:arXiv
2867:(PDF)
2805:(PDF)
2694:(PDF)
2666:(PDF)
2646:(PDF)
2618:(PDF)
2480:(PDF)
2397:(PDF)
2338:(PDF)
2254:(PDF)
2138:Notes
2132:Thunk
667:with
594:above
515:In a
420:is a
267:with
136:with
112:is a
3146:ISBN
3073:2021
3062:OCLC
3004:ISBN
2979:ISBN
2901:ISBN
2841:ISBN
2813:ISBN
2781:ISBN
2674:2022
2626:2021
2594:ISBN
2562:ISBN
2503:2021
2439:2021
2409:2021
2364:ISBN
2314:ISBN
2283:2021
2270:ISBN
2236:2021
2223:ISBN
2172:λy.y
1363:weak
695:here
293:iff
34:, a
3138:doi
3034:doi
2943:doi
2871:doi
2773:doi
2731:doi
2727:118
2698:doi
2530:doi
2492:doi
2488:165
2458:doi
2356:doi
2262:doi
1788:):
1421:.(λ
1387:.(λ
207:of
116:on
30:In
3188::
3154:.
3144:.
3132:.
3090:.
2949:.
2941:.
2929:22
2927:.
2915:^
2885:^
2827:^
2779:.
2771:.
2745:^
2725:.
2721:.
2584:;
2544:^
2526:58
2524:.
2520:.
2486:.
2482:.
2429:.
2417:^
2399:.
2378:^
2362:.
2354:.
2340:.
2308:.
2291:^
2268:.
2256:.
2203:^
2162:,
2158:,
2112:.
1473:,
1455:.
1436:(λ
1402:(λ
588:,
389:A
348:A
345:.
42:.
3162:.
3140::
3094:.
3075:.
3040:.
3036::
3012:.
2987:.
2957:.
2945::
2935::
2909:.
2879:.
2873::
2849:.
2821:.
2789:.
2775::
2739:.
2733::
2706:.
2700::
2676:.
2628:.
2602:.
2570:.
2538:.
2532::
2505:.
2494::
2464:.
2460::
2441:.
2411:.
2372:.
2358::
2322:.
2285:.
2264::
2238:.
2187:.
2174:.
2061:)
2057:]
2054:P
2048:x
2045:[
2042:N
2039:]
2036:P
2030:x
2027:[
2024:M
2021:(
2018:=
2011:]
2008:P
2002:x
1999:[
1990:)
1986:N
1983:M
1980:(
1968:y
1964:=
1957:]
1954:N
1948:x
1945:[
1936:y
1922:)
1918:]
1915:N
1909:x
1906:[
1903:M
1900:.
1897:y
1891:(
1888:=
1881:]
1878:N
1872:x
1869:[
1860:)
1856:M
1853:.
1850:y
1844:(
1838:N
1829:=
1822:]
1819:N
1813:x
1810:[
1801:x
1772:]
1769:N
1763:x
1760:[
1757:M
1728:T
1724:=
1715:T
1666:]
1663:N
1644:x
1641:[
1638:M
1610:)
1606:N
1597:)
1593:M
1590:.
1587:x
1581:(
1578:(
1552:a
1525:a
1503:b
1500:a
1452:x
1446:z
1444:)
1442:y
1440:.
1438:y
1431:z
1429:)
1427:y
1425:.
1423:y
1419:x
1417:λ
1412:z
1410:)
1408:x
1406:.
1404:y
1397:z
1395:)
1393:x
1391:.
1389:y
1385:x
1383:λ
1332:z
1310:)
1307:)
1304:w
1301:w
1298:w
1295:.
1292:w
1286:(
1283:)
1280:w
1277:w
1274:w
1271:.
1268:w
1262:(
1259:(
1256:)
1253:z
1250:.
1247:x
1239:(
1203:)
1200:)
1197:w
1194:w
1191:w
1188:.
1185:w
1179:(
1176:)
1173:w
1170:w
1167:w
1164:.
1161:w
1155:(
1152:)
1149:w
1146:w
1143:w
1140:.
1137:w
1131:(
1128:)
1125:w
1122:w
1119:w
1116:.
1113:w
1107:(
1104:)
1101:w
1098:w
1095:w
1092:.
1089:w
1083:(
1080:(
1077:)
1074:z
1071:.
1068:x
1062:(
1048:)
1045:)
1042:w
1039:w
1036:w
1033:.
1030:w
1024:(
1021:)
1018:w
1015:w
1012:w
1009:.
1006:w
1000:(
997:)
994:w
991:w
988:w
985:.
982:w
976:(
973:)
970:w
967:w
964:w
961:.
958:w
952:(
949:(
946:)
943:z
940:.
937:x
931:(
917:)
914:)
911:w
908:w
905:w
902:.
899:w
893:(
890:)
887:w
884:w
881:w
878:.
875:w
869:(
866:)
863:w
860:w
857:w
854:.
851:w
845:(
842:(
839:)
836:z
833:.
830:x
824:(
810:)
807:)
804:w
801:w
798:w
795:.
792:w
786:(
783:)
780:w
777:w
774:w
771:.
768:w
762:(
759:(
756:)
753:z
750:.
747:x
739:(
681:I
678:,
655:)
652:I
649:.
646:y
640:(
637:)
631:x
628:.
625:x
619:(
491:b
486:S
478:a
458:b
438:A
432:a
406:S
365:S
329:b
323:S
315:a
312:.
305:b
281:b
275:a
255:b
235:a
189:+
162:+
149:S
124:A
98:S
73:)
67:,
64:A
61:(
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.