2869:(instructions 0,3,4,5, and the pseudo-instruction "implicit cons") are not necessary for universal computation, but make programming more convenient by providing facilities for dealing with binary tree data structures and arithmetic; Nock also provides 5 more instructions (6,7,8,9,10) that could have been built out of these primitives.
2502:
86:
Although the most formal representation of the objects in this system requires binary trees, for simpler typesetting they are often represented as parenthesized expressions, as a shorthand for the tree they represent. Any subtrees may be parenthesized, but often only the right-side subtrees are
2868:
may be seen as an assembly language based on SK combinator calculus in the same way that traditional assembly language is based on Turing machines. Nock instruction 2 (the "Nock operator") is the S combinator and Nock instruction 1 is the K combinator. The other primitive instructions in Nock
2400:
2335:
2433:
888:ββ for the "rest of computation" call (with ββν = α(ββ)ν) is the very definition of recursion: ρν' = ββν' = α(ββ)ν' = ... . α will have to employ some kind of conditional to stop at some "base case" and not make the recursive call then, to avoid divergence.
2594:
883:
If α expresses a "computational step" computed by αρν for some ρ and ν, that assumes ρν' expresses "the rest of the computation" (for some ν' that α will "compute" from ν), then its fixed point ββ expresses the whole recursive computation, since using
2341:
250:
is a substitution operator. It takes three arguments and then returns the first argument applied to the third, which is then applied to the result of the second argument applied to the third. More clearly:
2537:
2286:
151:, transforms into another tree. The "function", "argument" and the "value" are either combinators or binary trees. If they are binary trees, they may be thought of as functions too, if needed.
2497:{\displaystyle {\textrm {KS(I(SKSI))}}\Rightarrow {\textrm {KS(I(KI(SI)))}}\Rightarrow {\textrm {KS(I(I))}}\Rightarrow {\textrm {KS(II)}}\Rightarrow {\textrm {KSI}}\Rightarrow {\textrm {S}}}
2545:
2427:
2280:
859:
375:
From these definitions it can be shown that SKI calculus is not the minimum system that can fully perform the computations of lambda calculus, as all occurrences of
31:. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory of
2824:
2395:{\displaystyle {\textrm {SKI(KIS)}}\Rightarrow {\textrm {SKII}}\Rightarrow {\textrm {KI(II)}}\Rightarrow {\textrm {KII}}\Rightarrow {\textrm {I}}}
634:
Assuming a sequence is a valid derivation to begin with, it can be extended using these rules. All derivations of length 1 are valid derivations.
2204:
2508:
2797:
2777:
2709:
596:: A derivation is a finite sequence of terms defined recursively by the following rules (where α and ι are words over the alphabet {
2845:
2865:
2330:{\displaystyle {\textrm {SKI(KIS)}}\Rightarrow {\textrm {K(KIS)(I(KIS))}}\Rightarrow {\textrm {KIS}}\Rightarrow {\textrm {I}}}
1145:
2244:
752:
Another thing is that it allows one to write a function that applies one thing to the self application of another thing:
2784:
A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
2887:
1829:(as a postfix operator) in terms of SKI notation, this proves that the SKI system can fully express Boolean logic.
2589:{\displaystyle {\textrm {SKIK}}\Rightarrow {\textrm {KK(IK)}}\Rightarrow {\textrm {KKK}}\Rightarrow {\textrm {K}}}
2255:
There may be multiple ways to do a reduction. All are equivalent, as long as you don't break order of operations
2882:
421:
It is possible to define a complete system using only one (improper) combinator. An example is Chris Barker's
2408:
1308:
The key is in defining the two
Boolean expressions. The first works just like one of our basic combinators:
2243:
This connection between the types of combinators and the corresponding logical axioms is an instance of the
2625:
2615:
2261:
2212:
1031:
2767:
2644:
2196:
44:
28:
2812:
are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
526:
The simplest possible term forming a basis is X = λf.f λxyz.x z (y z) λxyz.x, which satisfies X X =
2693:
87:
parenthesized, with left associativity implied for any unparenthesized applications. For example,
2745:
2682:
2803:
2793:
2773:
2728:(1930). "Grundlagen der Kombinatorischen Logik" [Foundations of combinatorial logic].
2705:
2697:
2610:
2605:
1833:
1050:
55:
24:
844:
2763:
2737:
2674:
2226:
2082:
2857:
2851:
2838:
2620:
2208:
403:
40:
36:
2220:
115:). If more explicitness is desired, the implied parentheses can be included as well: ((
2876:
2725:
2686:
1255:
48:
2637:
2149:
810:. If β is the function that applies α to the self application of something else,
422:
1364:
Once true and false are defined, all
Boolean logic can be implemented in terms of
1387:
as the second and third values, so it can be implemented as a postfix operation:
59:
147:, when the function is "applied" to the argument), the tree "returns a value",
684:. One interesting property of it is that its self-application is irreducible:
2807:
650:
is an expression that takes an argument and applies that argument to itself:
807:
542:
The terms and derivations in this system can also be more formally defined:
32:
2630:
2749:
2678:
2665:
Schönfinkel, M. (1924). "Über die
Bausteine der mathematischen Logik".
305:-rule. As no further rule can be applied, the computation halts here.
2831:
1375:(which returns the opposite of a given Boolean) works the same as the
735:
Or, using the equation as its definition directly, we immediately get
1662:
as the third value, so it can be implemented as a postfix operation:
1495:
as the second value, so it can be implemented as an infix operation:
2741:
491:(which is equivalent to application of ι to itself): ι(ι(ιι)) = ι(ιι
398:, and the resulting expression will yield the same result. So the "
834:
then the self-application of this β is the fixed point of that α:
630:β)γ)δ)ι, then Δ followed by the term α((βδ)(γδ))ι is a derivation.
589:
Nothing is a term if not required to be so by the first two rules.
2854:(PostScript) (by Milner, Parrow, and Walker) shows a scheme for
2532:{\displaystyle {\textrm {KS(I(SKSI))}}\Rightarrow {\textrm {S}}}
1266:
structure consists of a
Boolean expression that is either true (
39:
language. It can be likened to a reduced version of the untyped
2229:, would require the combinatory analog to the sentential axiom
788:
or it can be seen as defining yet another combinator directly,
1684:
structure, it can be shown that this has the expected result:
1517:
structure, it can be shown that this has the expected result:
368:
because they always yield the same result when applied to any
99:). Using this notation, a tree whose left subtree is the tree
1418:
structure, it can be shown that this has the expected result
626:
If Δ is a derivation ending in an expression of the form α(((
2640:
programming languages, designed to be even simpler than SKI.
619:
If Δ is a derivation ending in an expression of the form α((
612:
If Δ is a derivation ending in an expression of the form α(
463:
from the iota combinator. Applying ι to itself gives ιι = ι
131:
Informally, and using programming language jargon, a tree (
552:
of terms is defined recursively by the following rules.
623:β)γ)ι, then Δ followed by the term αβι is a derivation.
1483:
if either of the two
Boolean values surrounding it is
2548:
2511:
2436:
2411:
2344:
2289:
2264:
2199:. In order for combinatory logic to have as a model:
1650:
if both of the two
Boolean values surrounding it are
847:
616:β)ι, then Δ followed by the term αβι is a derivation.
54:
All operations in lambda calculus can be encoded via
2825:The SKI Combinator Calculus as a Universal System.
2588:
2531:
2496:
2421:
2394:
2329:
2274:
853:
864:Or, directly again from the derived definition,
511:. Applying ι one more time gives ι(ι(ι(ιι))) = ι
2195:are complete for the implicational fragment of
425:combinator, which can be expressed in terms of
2736:(3). Johns Hopkins University Press: 509–536.
2704:. Harvard University Press. pp. 355–366.
2698:"On the building blocks of mathematical logic"
2211:, would require the combinatory analog to the
1041:This becomes much shorter with the use of the
173:represent expressions made from the functions
2702:A Source Book in Mathematical Logic 1879–1931
2148:Function application corresponds to the rule
8:
410:is optional, the system is also referred as
1254:SKI combinator calculus can also implement
349:will always equal the result of evaluating
1148:syntax it becomes the exceptionally short
487:can be constructed by applying ι twice to
215:, yields a one-argument constant function
62:whose leaves are one of the three symbols
2846:"Drag 'n' Drop Combinators (Java Applet).
2691:Translated by Stefan Bauer-Mengelberg as
2580:
2579:
2570:
2569:
2560:
2559:
2550:
2549:
2547:
2523:
2522:
2513:
2512:
2510:
2488:
2487:
2478:
2477:
2468:
2467:
2458:
2457:
2448:
2447:
2438:
2437:
2435:
2413:
2412:
2410:
2386:
2385:
2376:
2375:
2366:
2365:
2356:
2355:
2346:
2345:
2343:
2321:
2320:
2311:
2310:
2301:
2300:
2291:
2290:
2288:
2266:
2265:
2263:
846:
2657:
2422:{\displaystyle {\textrm {KS(I(SKSI))}}}
2081:correspond to two well-known axioms of
342:, so the ultimate result of evaluating
2852:A Calculus of Mobile Processes, Part I
479:) which is functionally equivalent to
379:in any expression can be replaced by (
364:are "functionally equivalent" for any
222:, which, when applied to any argument
806:This function can be used to achieve
608:, (, )} while β, γ and δ are terms):
7:
2861:for the SKI calculus in pages 25–28.
2275:{\displaystyle {\textrm {SKI(KIS)}}}
103:and whose right subtree is the tree
2790:Diagonalization and Self-Reference
2069:Connection to intuitionistic logic
1334:The second is also fairly simple:
1183:reverses the following two terms:
135:) can be thought of as a function
35:because it is an extremely simple
14:
1836:, it is also possible to express
158:operation is defined as follows:
1274:) and two arguments, such that:
2730:American Journal of Mathematics
211:, when applied to any argument
2576:
2566:
2556:
2519:
2484:
2474:
2464:
2454:
2444:
2382:
2372:
2362:
2352:
2317:
2307:
2297:
643:Self-application and recursion
451:It is possible to reconstruct
1:
2788:— (1994). "Ch. 17–20".
891:This can be formalized, with
1825:(as an infix operator), and
841:β = ββ = α(ββ) = α(α(ββ)) =
16:Simple Turing complete logic
2792:. Oxford University Press.
289:-rule. Then if we evaluate
2904:
2866:Nock programming language
2832:To Dissect a Mockingbird.
2830:Keenan, David C. (2001) "
1821:(as a postfix operator),
58:into the SKI calculus as
2245:Curry–Howard isomorphism
2227:Complete classical logic
323:will always evaluate to
25:combinatory logic system
1832:As the SKI calculus is
1654:) works the same as an
1487:) works the same as an
1164:The reversal expression
854:{\displaystyle \ldots }
139:applied to an argument
56:abstraction elimination
43:. It was introduced by
21:SKI combinator calculus
2626:Functional programming
2616:Fixed point combinator
2590:
2533:
2498:
2423:
2396:
2331:
2276:
2213:law of excluded middle
2205:implicational fragment
855:
669:This is also known as
416:SK combinator calculus
191:returns its argument:
2769:To Mock a Mockingbird
2726:Curry, Haskell Brooks
2667:Mathematische Annalen
2645:To Mock a Mockingbird
2591:
2534:
2499:
2424:
2397:
2332:
2277:
2251:Examples of reduction
1848:as prefix operators:
1809:Because this defines
1680:If this is put in an
1513:If this is put in an
1414:If this is put in an
1032:one possible encoding
856:
273:Example computation:
2694:van Heijenoort, Jean
2633:programming language
2546:
2509:
2434:
2409:
2342:
2287:
2262:
2197:intuitionistic logic
845:
127:Informal description
29:computational system
185:, and set values):
2679:10.1007/BF01448013
2586:
2529:
2494:
2419:
2392:
2327:
2272:
1258:in the form of an
1144:And with a pseudo-
851:
578:are terms, then (τ
143:. When evaluated (
107:can be written as
2888:Combinatory logic
2839:Combinator Birds.
2837:Rathman, Chris, "
2823:O'Donnell, Mike "
2764:Smullyan, Raymond
2611:B, C, K, W system
2606:Combinatory logic
2583:
2573:
2563:
2553:
2526:
2516:
2491:
2481:
2471:
2461:
2451:
2441:
2416:
2389:
2379:
2369:
2359:
2349:
2324:
2314:
2304:
2294:
2269:
886:the same function
538:Formal definition
45:Moses Schönfinkel
2895:
2811:
2783:
2754:
2753:
2722:
2716:
2715:
2690:
2673:(3–4): 305–316.
2662:
2595:
2593:
2592:
2587:
2585:
2584:
2581:
2575:
2574:
2571:
2565:
2564:
2561:
2555:
2554:
2551:
2538:
2536:
2535:
2530:
2528:
2527:
2524:
2518:
2517:
2514:
2503:
2501:
2500:
2495:
2493:
2492:
2489:
2483:
2482:
2479:
2473:
2472:
2469:
2463:
2462:
2459:
2453:
2452:
2449:
2443:
2442:
2439:
2428:
2426:
2425:
2420:
2418:
2417:
2414:
2401:
2399:
2398:
2393:
2391:
2390:
2387:
2381:
2380:
2377:
2371:
2370:
2367:
2361:
2360:
2357:
2351:
2350:
2347:
2336:
2334:
2333:
2328:
2326:
2325:
2322:
2316:
2315:
2312:
2306:
2305:
2302:
2296:
2295:
2292:
2281:
2279:
2278:
2273:
2271:
2270:
2267:
2238:
2178:
2174:
2164:
2160:
2143:
2106:
2083:sentential logic
2073:The combinators
1379:structure, with
1099:or directly, as
1049:combinators, as
860:
858:
857:
852:
530:, and X (X X) =
2903:
2902:
2898:
2897:
2896:
2894:
2893:
2892:
2883:Lambda calculus
2873:
2872:
2858:graph reduction
2820:
2815:
2800:
2787:
2780:
2762:
2758:
2757:
2742:10.2307/2370619
2724:
2723:
2719:
2712:
2696:, ed. (2002) .
2692:
2664:
2663:
2659:
2654:
2621:Lambda calculus
2602:
2544:
2543:
2507:
2506:
2432:
2431:
2407:
2406:
2340:
2339:
2285:
2284:
2260:
2259:
2253:
2230:
2209:classical logic
2191:, and the rule
2176:
2166:
2162:
2156:
2110:
2089:
2071:
1658:structure with
1646:(which returns
1491:structure with
1479:(which returns
1262:structure. An
1252:
1166:
1030:which gives us
843:
842:
645:
640:
638:SKI expressions
585:
581:
577:
573:
540:
404:syntactic sugar
129:
84:
41:lambda calculus
37:Turing complete
17:
12:
11:
5:
2901:
2899:
2891:
2890:
2885:
2875:
2874:
2871:
2870:
2862:
2849:
2842:
2835:
2828:
2819:
2818:External links
2816:
2814:
2813:
2798:
2785:
2778:
2759:
2756:
2755:
2717:
2710:
2656:
2655:
2653:
2650:
2649:
2648:
2641:
2634:
2628:
2623:
2618:
2613:
2608:
2601:
2598:
2597:
2596:
2578:
2568:
2558:
2541:
2540:
2539:
2521:
2504:
2486:
2476:
2466:
2456:
2446:
2404:
2403:
2402:
2384:
2374:
2364:
2354:
2337:
2319:
2309:
2303:K(KIS)(I(KIS))
2299:
2252:
2249:
2241:
2240:
2224:
2181:
2180:
2146:
2145:
2108:
2070:
2067:
2066:
2065:
1990:
1936:
1807:
1806:
1776:
1746:
1716:
1678:
1677:
1640:
1639:
1609:
1579:
1549:
1511:
1510:
1473:
1472:
1446:
1412:
1411:
1362:
1361:
1345:
1332:
1331:
1319:
1306:
1305:
1289:
1288:
1251:
1248:
1247:
1246:
1243:
1237:
1227:
1217:
1203:
1165:
1162:
1142:
1141:
1119:
1097:
1096:
1051:the equivalent
1028:
1027:
953:
952:
862:
861:
850:
832:
831:
786:
785:
733:
732:
667:
666:
644:
641:
639:
636:
632:
631:
624:
617:
591:
590:
587:
583:
579:
575:
571:
568:
539:
536:
449:
448:
353:. We say that
327:in two steps,
312:and all trees
308:For all trees
271:
270:
245:
244:
206:
205:
128:
125:
83:
80:
15:
13:
10:
9:
6:
4:
3:
2:
2900:
2889:
2886:
2884:
2881:
2880:
2878:
2867:
2863:
2860:
2859:
2853:
2850:
2847:
2843:
2840:
2836:
2833:
2829:
2826:
2822:
2821:
2817:
2809:
2805:
2801:
2799:9780198534501
2795:
2791:
2786:
2781:
2779:0-394-53491-3
2775:
2771:
2770:
2765:
2761:
2760:
2751:
2747:
2743:
2739:
2735:
2732:(in German).
2731:
2727:
2721:
2718:
2713:
2711:9780674324497
2707:
2703:
2699:
2695:
2688:
2684:
2680:
2676:
2672:
2668:
2661:
2658:
2651:
2647:
2646:
2642:
2639:
2635:
2632:
2629:
2627:
2624:
2622:
2619:
2617:
2614:
2612:
2609:
2607:
2604:
2603:
2599:
2542:
2505:
2450:KS(I(KI(SI)))
2430:
2429:
2405:
2338:
2283:
2282:
2258:
2257:
2256:
2250:
2248:
2246:
2237:
2233:
2228:
2225:
2222:
2218:
2214:
2210:
2206:
2202:
2201:
2200:
2198:
2194:
2190:
2186:
2173:
2169:
2159:
2155:
2154:
2153:
2151:
2141:
2137:
2133:
2129:
2126:)) → ((
2125:
2121:
2117:
2113:
2109:
2104:
2100:
2096:
2092:
2088:
2087:
2086:
2084:
2080:
2076:
2068:
2063:
2060:
2056:
2053:
2049:
2045:
2041:
2037:
2033:
2029:
2026:
2022:
2018:
2014:
2010:
2006:
2002:
1998:
1994:
1991:
1988:
1985:
1982:
1978:
1974:
1971:
1967:
1964:
1960:
1956:
1952:
1948:
1944:
1940:
1937:
1934:
1931:
1927:
1923:
1920:
1916:
1913:
1909:
1906:
1902:
1898:
1894:
1890:
1886:
1882:
1878:
1874:
1870:
1866:
1862:
1858:
1854:
1851:
1850:
1849:
1847:
1843:
1839:
1835:
1830:
1828:
1824:
1820:
1816:
1812:
1805:
1801:
1797:
1793:
1789:
1785:
1781:
1777:
1775:
1771:
1767:
1763:
1759:
1755:
1751:
1747:
1745:
1741:
1737:
1733:
1729:
1725:
1721:
1717:
1715:
1711:
1707:
1703:
1699:
1695:
1691:
1687:
1686:
1685:
1683:
1676:
1672:
1668:
1665:
1664:
1663:
1661:
1657:
1653:
1649:
1645:
1638:
1634:
1630:
1626:
1622:
1618:
1614:
1610:
1608:
1604:
1600:
1596:
1592:
1588:
1584:
1580:
1578:
1574:
1570:
1566:
1562:
1558:
1554:
1550:
1548:
1544:
1540:
1536:
1532:
1528:
1524:
1520:
1519:
1518:
1516:
1509:
1505:
1501:
1498:
1497:
1496:
1494:
1490:
1486:
1482:
1478:
1471:
1467:
1463:
1459:
1455:
1451:
1447:
1445:
1441:
1437:
1433:
1429:
1425:
1421:
1420:
1419:
1417:
1409:
1405:
1401:
1397:
1393:
1390:
1389:
1388:
1386:
1382:
1378:
1374:
1369:
1367:
1359:
1356:
1352:
1349:
1346:
1344:
1340:
1337:
1336:
1335:
1330:
1326:
1323:
1320:
1318:
1314:
1311:
1310:
1309:
1304:
1300:
1297:
1294:
1293:
1292:
1287:
1283:
1280:
1277:
1276:
1275:
1273:
1269:
1265:
1261:
1257:
1256:Boolean logic
1250:Boolean logic
1249:
1244:
1241:
1238:
1235:
1231:
1228:
1225:
1221:
1218:
1215:
1211:
1207:
1204:
1201:
1197:
1193:
1189:
1186:
1185:
1184:
1182:
1178:
1174:
1170:
1163:
1161:
1159:
1155:
1151:
1147:
1139:
1135:
1131:
1127:
1123:
1120:
1117:
1113:
1109:
1106:αβ = α(ββ) =
1105:
1102:
1101:
1100:
1094:
1090:
1086:
1082:
1078:
1074:
1070:
1066:
1062:
1058:
1055:
1054:
1053:
1052:
1048:
1044:
1039:
1037:
1033:
1025:
1021:
1017:
1013:
1009:
1005:
1001:
997:
993:
989:
985:
981:
977:
973:
969:
965:
961:
958:
957:
956:
950:
946:
942:
938:
934:
930:
926:
922:
918:
914:
910:
906:
902:
898:
894:
893:
892:
889:
887:
881:
879:
875:
871:
867:
848:
840:
837:
836:
835:
829:
825:
821:
817:
813:
812:
811:
809:
804:
802:
798:
794:
791:
783:
779:
775:
771:
767:
763:
759:
755:
754:
753:
750:
748:
745:
741:
738:
730:
726:
722:
718:
714:
710:
706:
702:
698:
694:
690:
687:
686:
685:
683:
679:
676:
672:
664:
660:
656:
653:
652:
651:
649:
642:
637:
635:
629:
625:
622:
618:
615:
611:
610:
609:
607:
603:
599:
595:
588:
569:
566:
562:
558:
555:
554:
553:
551:
547:
543:
537:
535:
533:
529:
524:
522:
518:
514:
510:
506:
502:
498:
494:
490:
486:
482:
478:
474:
470:
466:
462:
458:
454:
447:
444:
440:
436:
435:
434:
432:
428:
424:
419:
417:
413:
409:
405:
401:
397:
393:
390:
386:
382:
378:
373:
371:
367:
363:
359:
356:
352:
348:
345:
341:
337:
333:
330:
326:
322:
319:
315:
311:
306:
304:
300:
296:
292:
288:
284:
280:
277:evaluates to
276:
268:
264:
260:
257:
254:
253:
252:
249:
243:
239:
236:
233:
232:
231:
229:
225:
221:
218:
214:
210:
204:
200:
197:
194:
193:
192:
190:
186:
184:
180:
176:
172:
168:
164:
159:
157:
152:
150:
146:
142:
138:
134:
126:
124:
122:
118:
114:
110:
106:
102:
98:
94:
90:
81:
79:
77:
73:
69:
65:
61:
57:
52:
50:
49:Haskell Curry
46:
42:
38:
34:
30:
26:
22:
2855:
2789:
2768:
2733:
2729:
2720:
2701:
2670:
2666:
2660:
2643:
2638:Iota and Jot
2254:
2242:
2235:
2231:
2221:Peirce's law
2216:
2192:
2188:
2184:
2182:
2171:
2167:
2157:
2150:modus ponens
2147:
2139:
2135:
2131:
2127:
2123:
2119:
2115:
2111:
2102:
2098:
2094:
2090:
2078:
2074:
2072:
2061:
2058:
2054:
2051:
2047:
2043:
2039:
2035:
2031:
2027:
2024:
2020:
2016:
2012:
2008:
2004:
2000:
1996:
1992:
1986:
1983:
1980:
1976:
1972:
1969:
1965:
1962:
1958:
1954:
1950:
1946:
1942:
1938:
1932:
1929:
1925:
1921:
1918:
1914:
1911:
1907:
1904:
1900:
1896:
1892:
1888:
1884:
1880:
1876:
1872:
1868:
1864:
1860:
1856:
1852:
1845:
1841:
1837:
1831:
1826:
1822:
1818:
1814:
1810:
1808:
1803:
1799:
1795:
1791:
1787:
1783:
1779:
1773:
1769:
1765:
1761:
1757:
1753:
1749:
1743:
1739:
1735:
1731:
1727:
1723:
1719:
1713:
1709:
1705:
1701:
1697:
1693:
1689:
1682:if-then-else
1681:
1679:
1674:
1670:
1666:
1659:
1656:if-then-else
1655:
1651:
1647:
1643:
1641:
1636:
1632:
1628:
1624:
1620:
1616:
1612:
1606:
1602:
1598:
1594:
1590:
1586:
1582:
1576:
1572:
1568:
1564:
1560:
1556:
1552:
1546:
1542:
1538:
1534:
1530:
1526:
1522:
1515:if-then-else
1514:
1512:
1507:
1503:
1499:
1492:
1489:if-then-else
1488:
1484:
1480:
1476:
1474:
1469:
1465:
1461:
1457:
1453:
1449:
1443:
1439:
1435:
1431:
1427:
1423:
1416:if-then-else
1415:
1413:
1407:
1403:
1399:
1395:
1391:
1384:
1380:
1377:if-then-else
1376:
1372:
1370:
1368:structures.
1366:if-then-else
1365:
1363:
1357:
1354:
1350:
1347:
1342:
1338:
1333:
1328:
1324:
1321:
1316:
1312:
1307:
1302:
1298:
1295:
1290:
1285:
1281:
1278:
1271:
1270:) or false (
1267:
1264:if-then-else
1263:
1260:if-then-else
1259:
1253:
1239:
1233:
1229:
1223:
1219:
1213:
1209:
1205:
1199:
1195:
1191:
1187:
1180:
1176:
1172:
1168:
1167:
1157:
1153:
1149:
1143:
1137:
1133:
1129:
1125:
1121:
1115:
1111:
1107:
1103:
1098:
1092:
1088:
1084:
1080:
1076:
1072:
1068:
1064:
1060:
1056:
1046:
1042:
1040:
1038:combinator.
1035:
1029:
1023:
1019:
1015:
1011:
1007:
1003:
999:
995:
991:
987:
983:
979:
975:
971:
967:
963:
959:
954:
948:
944:
940:
936:
932:
928:
924:
920:
916:
912:
908:
904:
900:
896:
890:
885:
882:
877:
873:
869:
865:
863:
838:
833:
827:
823:
819:
815:
805:
800:
796:
792:
789:
787:
781:
777:
773:
769:
765:
761:
757:
751:
746:
743:
739:
736:
734:
728:
724:
720:
716:
712:
708:
704:
700:
696:
692:
688:
681:
677:
674:
673:combinator,
670:
668:
662:
658:
654:
647:
646:
633:
627:
620:
613:
605:
601:
597:
593:
592:
586:) is a term.
564:
560:
556:
549:
545:
544:
541:
531:
527:
525:
520:
516:
512:
508:
504:
500:
496:
492:
488:
484:
480:
476:
472:
468:
464:
460:
456:
452:
450:
445:
442:
438:
433:as follows:
430:
426:
420:
415:
411:
407:
402:" is merely
399:
395:
391:
388:
384:
380:
376:
374:
369:
365:
361:
357:
354:
350:
346:
343:
339:
335:
331:
328:
324:
320:
317:
313:
309:
307:
302:
298:
294:
290:
286:
282:
278:
274:
272:
266:
262:
258:
255:
247:
246:
241:
237:
234:
227:
223:
219:
216:
212:
208:
207:
202:
198:
195:
188:
187:
182:
178:
174:
170:
166:
162:
160:
155:
153:
148:
144:
140:
136:
132:
130:
120:
116:
112:
108:
104:
100:
96:
92:
88:
85:
75:
71:
67:
63:
60:binary trees
53:
20:
18:
2856:combinator
2515:KS(I(SKSI))
2440:KS(I(SKSI))
2415:KS(I(SKSI))
2183:The axioms
2134:) → (
784:β)) = α(ββ)
594:Derivations
412:SK calculus
76:combinators
2877:Categories
2652:References
1402:) = λb.b (
567:are terms.
548:: The set
394:) for any
297:), we get
226:, returns
156:evaluation
33:algorithms
2808:473553893
2772:. Knopf.
2687:118507515
2577:⇒
2567:⇒
2557:⇒
2520:⇒
2485:⇒
2475:⇒
2465:⇒
2455:⇒
2445:⇒
2383:⇒
2373:⇒
2363:⇒
2353:⇒
2318:⇒
2308:⇒
2298:⇒
2118:→ (
2097:→ (
849:…
808:recursion
285:) by the
2766:(1985).
2631:Unlambda
2600:See also
2460:KS(I(I))
2348:SKI(KIS)
2293:SKI(KIS)
2268:SKI(KIS)
2234:→
2175:, infer
2170:→
2138:→
2130:→
2122:→
2101:→
1834:complete
1642:Boolean
1475:Boolean
1394:= λb.b (
1371:Boolean
406:. Since
91:means ((
82:Notation
74:(called
2750:2370619
2161:: from
2007:)) (as
1146:Haskell
1034:of the
872:α) = α(
776:β) = α(
665:α) = αα
301:by the
2806:
2796:
2776:
2748:
2708:
2685:
2562:KK(IK)
2470:KS(II)
2368:KI(II)
1949:) (as
1871:) (as
1075:))α =
768:))β =
563:, and
499:) = ι(
495:) = ι(
459:, and
387:) or (
383:) or (
181:, and
169:, and
70:, and
27:and a
2746:JSTOR
2683:S2CID
1358:y(xy)
1236:αβ) →
1226:α)β →
1216:α)β →
1156:. (.
1132:α) =
1026:))) α
974:α) =
880:α)).
723:)) =
711:)) =
574:and τ
546:Terms
23:is a
2864:the
2804:OCLC
2794:ISBN
2774:ISBN
2706:ISBN
2636:The
2552:SKIK
2358:SKII
2217:i.e.
2203:The
2187:and
2165:and
2077:and
2057:) =
1910:) =
1844:and
1802:) =
1772:) =
1742:) =
1712:) =
1635:) =
1623:) =
1605:) =
1593:) =
1575:) =
1563:) =
1545:) =
1533:) =
1468:) =
1442:) =
1383:and
1291:and
1242:βα →
1202:αβ →
1124:α =
1114:β =
1087:) =
1059:α =
1045:and
990:α =
966:β =
962:α =
951:)) α
927:) =
911:) =
899:α =
895:β =
818:α =
814:β =
695:) =
657:α =
570:If τ
505:SKSK
503:) =
469:SSKK
429:and
423:iota
360:and
338:) =
275:SKSK
154:The
149:i.e.
145:i.e.
123:)).
47:and
19:The
2738:doi
2675:doi
2572:KKK
2480:KSI
2378:KII
2313:KIS
2207:of
2114:: (
1993:AND
1883:))(
1867:))(
1853:NOT
1846:AND
1838:NOT
1827:AND
1819:NOT
1788:AND
1758:AND
1728:AND
1698:AND
1667:AND
1644:AND
1454:NOT
1428:NOT
1392:NOT
1373:NOT
1360:= y
1212:)α(
1160:).
1138:CBU
1116:CBU
1093:CBU
1024:SII
1002:))(
1000:SII
984:SII
968:SII
964:SII
955:as
949:SII
925:SII
909:SII
907:α)(
839:SII
828:SII
826:α)(
803:).
774:SII
772:αβ(
766:SII
764:α)(
729:SII
725:SII
721:SII
713:SII
709:SII
701:SII
693:SII
689:SII
655:SII
648:SII
517:KSK
497:ISK
414:or
385:SKS
381:SKK
259:xyz
89:ISK
78:).
2879::
2802:.
2744:.
2734:52
2700:.
2681:.
2671:92
2669:.
2247:.
2219:,
2215:,
2193:MP
2189:AS
2185:AK
2158:MP
2152::
2142:))
2112:AS
2093::
2091:AK
2085::
2059:xy
2052:KF
2048:xy
2046:=
2036:KF
2023:=
2021:xy
2019:))
2017:KF
2009:SS
2005:KF
1997:SS
1995:=
1979:=
1970:KT
1961:=
1959:xy
1955:KT
1951:SI
1947:KT
1943:SI
1941:=
1939:OR
1933:FT
1928:=
1919:KF
1905:KT
1897:KF
1893:SI
1891:=
1885:KT
1881:KF
1877:SI
1869:KT
1865:KF
1861:SI
1855:=
1842:OR
1840:,
1823:OR
1817:,
1813:,
1798:)(
1790:=
1782:)(
1768:)(
1760:=
1752:)(
1738:)(
1730:=
1722:)(
1708:)(
1700:=
1692:)(
1675:SK
1673:=
1669:=
1631:)(
1617:OR
1601:)(
1587:OR
1571:)(
1557:OR
1541:)(
1527:OR
1506:=
1502:=
1500:OR
1477:OR
1464:)(
1456:=
1438:)(
1430:=
1406:)(
1404:SK
1398:)(
1353:=
1351:xy
1348:SK
1343:SK
1341:=
1327:=
1325:xy
1315:=
1301:=
1299:xy
1284:=
1282:xy
1245:βα
1232:β(
1220:SI
1210:SI
1198:))
1196:SI
1179:))
1177:SI
1152:=
1140:)α
1134:BU
1118:αβ
1095:)α
1089:BU
1073:KU
1069:SB
1067:)(
1065:KU
1018:)(
1012:KS
986:))
943:)(
937:KS
923:α(
917:KS
876:α(
868:α(
801:yy
795:=
793:xy
780:β(
749:.
742:=
703:)(
682:xx
680:=
661:α(
604:,
600:,
559:,
534:.
523:.
519:=
515:=
507:=
501:SK
493:SK
483:.
477:KK
473:SK
471:=
467:=
465:SK
455:,
446:SK
441:=
418:.
389:SK
372:.
355:SK
347:xy
344:SK
336:xy
321:xy
318:SK
316:,
295:SK
291:KK
283:SK
279:KK
267:yz
263:xz
261:=
240:=
238:xy
230::
201:=
177:,
165:,
133:xy
121:SK
119:)(
117:KS
113:SK
109:KS
105:SK
101:KS
93:IS
66:,
51:.
2848:"
2844:"
2841:"
2834:"
2827:"
2810:.
2782:.
2752:.
2740::
2714:.
2689:.
2677::
2582:K
2525:S
2490:S
2388:I
2323:I
2239:.
2236:A
2232:F
2223:;
2179:.
2177:B
2172:B
2168:A
2163:A
2144:.
2140:C
2136:A
2132:B
2128:A
2124:C
2120:B
2116:A
2107:,
2105:)
2103:A
2099:B
2095:A
2079:S
2075:K
2064:)
2062:F
2055:y
2050:(
2044:y
2042:)
2040:x
2038:)
2034:(
2032:K
2030:(
2028:x
2025:S
2015:(
2013:K
2011:(
2003:(
2001:K
1999:(
1989:)
1987:y
1984:T
1981:x
1977:y
1975:)
1973:x
1968:(
1966:x
1963:I
1957:)
1953:(
1945:(
1935:)
1930:x
1926:T
1924:)
1922:x
1917:(
1915:x
1912:I
1908:x
1903:(
1901:x
1899:)
1895:(
1889:x
1887:)
1879:(
1875:(
1873:S
1863:(
1859:(
1857:S
1815:F
1811:T
1804:F
1800:F
1796:F
1794:(
1792:F
1786:)
1784:F
1780:F
1778:(
1774:F
1770:F
1766:T
1764:(
1762:F
1756:)
1754:T
1750:F
1748:(
1744:F
1740:F
1736:F
1734:(
1732:T
1726:)
1724:F
1720:T
1718:(
1714:T
1710:F
1706:T
1704:(
1702:T
1696:)
1694:T
1690:T
1688:(
1671:F
1660:F
1652:T
1648:T
1637:F
1633:F
1629:T
1627:(
1625:F
1621:F
1619:(
1615:)
1613:F
1611:(
1607:T
1603:T
1599:T
1597:(
1595:F
1591:T
1589:(
1585:)
1583:F
1581:(
1577:T
1573:F
1569:T
1567:(
1565:T
1561:F
1559:(
1555:)
1553:T
1551:(
1547:T
1543:T
1539:T
1537:(
1535:T
1531:T
1529:(
1525:)
1523:T
1521:(
1508:K
1504:T
1493:T
1485:T
1481:T
1470:T
1466:T
1462:F
1460:(
1458:F
1452:)
1450:F
1448:(
1444:F
1440:T
1436:F
1434:(
1432:T
1426:)
1424:T
1422:(
1410:)
1408:K
1400:T
1396:F
1385:T
1381:F
1355:K
1339:F
1329:x
1322:K
1317:K
1313:T
1303:y
1296:F
1286:x
1279:T
1272:F
1268:T
1240:I
1234:K
1230:I
1224:K
1222:(
1214:K
1208:(
1206:K
1200:K
1194:(
1192:K
1190:(
1188:S
1181:K
1175:(
1173:K
1171:(
1169:S
1158:U
1154:U
1150:Y
1136:(
1130:H
1128:(
1126:U
1122:Y
1112:U
1110:α
1108:B
1104:H
1091:(
1085:U
1083:α
1081:B
1079:(
1077:U
1071:(
1063:(
1061:S
1057:Y
1047:C
1043:B
1036:Y
1022:(
1020:K
1016:K
1014:)
1010:(
1008:S
1006:(
1004:S
998:(
996:K
994:(
992:S
988:H
982:(
980:K
978:(
976:S
972:H
970:(
960:Y
947:(
945:K
941:K
939:)
935:(
933:S
931:(
929:S
921:K
919:)
915:(
913:S
905:K
903:(
901:S
897:H
878:H
874:H
870:H
866:H
830:)
824:K
822:(
820:S
816:H
799:(
797:x
790:H
782:I
778:I
770:K
762:K
760:(
758:S
756:(
747:U
744:U
740:U
737:U
731:)
727:(
719:(
717:I
715:(
707:(
705:I
699:(
697:I
691:(
678:x
675:U
671:U
663:I
659:I
628:S
621:K
614:I
606:I
602:K
598:S
584:2
582:τ
580:1
576:2
572:1
565:I
561:K
557:S
550:T
532:S
528:K
521:S
513:K
509:K
489:I
485:K
481:I
475:(
461:I
457:K
453:S
443:x
439:x
437:ι
431:K
427:S
408:I
400:I
396:x
392:x
377:I
370:y
366:x
362:I
358:x
351:y
340:y
334:(
332:y
329:K
325:y
314:y
310:x
303:K
299:K
293:(
287:S
281:(
269:)
265:(
256:S
248:S
242:x
235:K
228:x
224:y
220:x
217:K
213:x
209:K
203:x
199:x
196:I
189:I
183:I
179:K
175:S
171:z
167:y
163:x
161:(
141:y
137:x
111:(
97:K
95:)
72:I
68:K
64:S
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.