1049:
1425:
340:. In other words,it addresses the idea of "parametrization" or "indexing" of computable functions. It's like creating a simplified version of a function that takes an additional parameter (index) to mimic the behavior of a more complex function.
1962:
1783:
2260:
856:
765:
1671:
1246:
2020:
2063:
1523:
2145:
2101:
1814:
266:
629:
1205:
1592:
1559:
1234:
1133:
1821:
503:
408:
2612:
1703:
1088:
811:
535:
373:
563:
664:
192:
1708:
1159:
338:
312:
468:
448:
428:
286:
2152:
1044:{\displaystyle \varphi _{S_{n}^{m}(p,x_{1},\dots ,x_{m})}\simeq \lambda y_{1},\dots ,y_{n}.\varphi _{p}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n}).}
2509:
688:
1614:
2758:
1420:{\displaystyle \forall z_{1},\dots ,z_{n}:{\text{TM}}_{x}(y_{1},\dots ,y_{m},z_{1},\dots ,z_{n})={\text{TM}}_{k}(z_{1},\dots ,z_{n}).}
1976:
2542:
2025:
2712:
2627:
1449:
2582:(This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the
2696:
2677:
2658:
2106:
545:
The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering
2068:
1788:
2753:
2490:
205:
566:
583:
1164:
1957:{\displaystyle \phi _{e}^{m+n}({\vec {x}},{\vec {y}})=\phi _{s_{m,n}{(e,{\vec {x}})}}^{n}({\vec {y}})}
2270:
1568:
1535:
1210:
1109:
152:
values. This algorithm generates source code that effectively substitutes the values for the first
119:
In practical terms, the theorem says that for a given programming language and positive integers
473:
378:
2585:
1676:
1061:
784:
508:
346:
548:
1778:{\displaystyle \forall {\vec {x}}\in \mathbb {N} ^{m},\forall {\vec {y}}\in \mathbb {N} ^{n}}
634:
162:
675:
68:
20:
2637:
8:
2717:
1605:
1138:
317:
291:
195:
80:
76:
2647:
2573:
2565:
2529:
2495:
453:
433:
413:
271:
410:
when given the appropriate parameters. Essentially, by selecting the right values for
72:
2714:
2692:
2673:
2654:
2623:
2533:
674:, and their values are equal for any such combination. In other words, the following
2577:
2633:
2557:
2521:
288:. It's like partially applying an argument to a function. This is generalized over
470:
behave like for a specific computation. Instead of dealing with the complexity of
1595:
2255:{\displaystyle f({\vec {x}},{\vec {y}})=\phi _{S({\vec {x}})}^{(n)}({\vec {y}})}
1602:
199:
145:
2747:
1966:
There is also a simplified version of the same theorem (defined infact as "
1970:", which basically uses a total computable function as index as follows:
132:
2569:
2525:
2622:. Oxford Logic Guides. Vol. 51. Oxford: Oxford University Press.
2022:
be a computable function. There, there is a total computable function
16:
On transforming a program by substituting constants for free variables
2734:
572:
of two arguments with the following property: for every Gödel number
128:
2561:
760:{\displaystyle \varphi _{s(p,x)}\simeq \lambda y.\varphi _{p}(x,y).}
2485:
1666:{\displaystyle s_{m,n}:\mathbb {N} ^{m+1}\rightarrow \mathbb {N} }
159:
The smn-theorem states that given a function of two arguments
2670:
The Theory of
Recursive Functions and Effective Computability
2015:{\displaystyle f:\mathbb {N} ^{n+m}\rightarrow \mathbb {N} }
2058:{\displaystyle s:\mathbb {N} ^{m}\rightarrow \mathbb {N} }
820:
arguments that behaves as follows: for every Gödel number
666:
are defined for the same combinations of natural numbers
156:
free variables, leaving the rest of the variables free.
116:
in the original formulation of the theorem (see below).
2691:. Perspectives in Mathematical Logic. Springer-Verlag.
2588:
2155:
2109:
2071:
2028:
1979:
1824:
1791:
1711:
1679:
1617:
1571:
1538:
1452:
1249:
1213:
1167:
1141:
1112:
1064:
859:
787:
691:
637:
586:
551:
511:
476:
456:
436:
416:
381:
349:
320:
294:
274:
208:
165:
79:) (Soare 1987, Rogers 1967). It was first proved by
2646:
2606:
2254:
2139:
2095:
2057:
2014:
1956:
1808:
1777:
1697:
1665:
1586:
1553:
1517:
1419:
1228:
1199:
1153:
1127:
1082:
1043:
805:
759:
658:
623:
557:
529:
497:
462:
442:
422:
402:
367:
332:
306:
280:
260:
186:
1518:{\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})}
2745:
2510:"General recursive functions of natural numbers"
1561:that is the result of hardcoding the values of
2140:{\displaystyle {\vec {y}}\in \mathbb {N} ^{n}}
781:, there exists a primitive recursive function
537:that captures the essence of the computation.
2644:
2096:{\displaystyle \forall x\in \mathbb {N} ^{m}}
2667:
2686:
2127:
2083:
2051:
2037:
2008:
1988:
1809:{\displaystyle \forall e\in \mathbb {N} }
1802:
1765:
1732:
1659:
1639:
268:basically "fixing" the first argument of
2689:Recursively enumerable sets and degrees
1430:Furthermore, there is a Turing machine
2746:
2540:
2507:
1161:and for all possible values of inputs
824:of a partial computable function with
261:{\displaystyle \phi _{s}(x)(y)=g(x,y)}
2713:
2672:. First MIT press paperback edition.
375:is designed to mimic the behavior of
2617:
624:{\displaystyle \varphi _{s(p,x)}(y)}
580:with two arguments, the expressions
1093:
1058:described above can be taken to be
565:of recursive functions, there is a
13:
2543:"On Notations for Ordinal Numbers"
2072:
1792:
1745:
1712:
1611:Given a total computable function
1250:
1200:{\displaystyle y_{1},\dots ,y_{m}}
202:and computable function such that
14:
2770:
2759:Theorems in theory of computation
2706:
576:of a partial computable function
1594:. The result generalizes to any
1207:, there exists a Turing machine
104:comes from the occurrence of an
2417:
2366:
1587:{\displaystyle {\text{TM}}_{x}}
1554:{\displaystyle {\text{TM}}_{k}}
1229:{\displaystyle {\text{TM}}_{k}}
1128:{\displaystyle {\text{TM}}_{x}}
2249:
2243:
2234:
2229:
2223:
2218:
2212:
2203:
2189:
2183:
2168:
2159:
2116:
2047:
2004:
1951:
1945:
1936:
1925:
1919:
1904:
1876:
1870:
1855:
1846:
1754:
1721:
1655:
1512:
1474:
1411:
1379:
1361:
1297:
1035:
971:
918:
880:
751:
739:
712:
700:
653:
641:
618:
612:
607:
595:
492:
480:
397:
385:
255:
243:
234:
228:
225:
219:
181:
169:
1:
2550:The Journal of Symbolic Logic
2501:
1601:This can also be extended to
834:arguments, and all values of
678:of functions holds for every
505:, we can work with a simpler
2620:Computability and randomness
567:primitive recursive function
127:, there exists a particular
7:
2479:
1106:, for every Turing Machine
10:
2775:
2649:Classical Recursion Theory
2491:Kleene's recursion theorem
2264:
540:
498:{\displaystyle \phi (x,y)}
403:{\displaystyle \phi (x,y)}
131:that accepts as input the
67:) is a basic result about
2607:{\displaystyle S_{n}^{m}}
1698:{\displaystyle m,n\geq 1}
1532:finds the Turing Machine
1083:{\displaystyle S_{1}^{1}}
806:{\displaystyle S_{n}^{m}}
530:{\displaystyle s_{m}^{n}}
368:{\displaystyle s_{m}^{n}}
2279:
770:More generally, for any
558:{\displaystyle \varphi }
65:parameterization theorem
2645:Odifreddi, P. (1999).
2608:
2541:Kleene, S. C. (1938).
2508:Kleene, S. C. (1936).
2256:
2141:
2097:
2059:
2016:
1968:simplified smn-theorem
1958:
1810:
1779:
1699:
1667:
1588:
1555:
1519:
1438:to be calculated from
1421:
1230:
1201:
1155:
1129:
1084:
1045:
807:
761:
660:
659:{\displaystyle f(x,y)}
625:
559:
531:
499:
464:
444:
424:
404:
369:
334:
308:
282:
262:
188:
187:{\displaystyle g(x,y)}
71:(and, more generally,
2609:
2514:Mathematische Annalen
2257:
2142:
2098:
2060:
2017:
1959:
1811:
1780:
1700:
1668:
1589:
1556:
1520:
1422:
1231:
1202:
1156:
1130:
1085:
1046:
808:
762:
661:
626:
560:
532:
500:
465:
445:
425:
405:
370:
335:
309:
283:
263:
189:
69:programming languages
2754:Computability theory
2668:Rogers, H. (1987) .
2586:
2153:
2107:
2069:
2026:
1977:
1822:
1789:
1709:
1677:
1615:
1606:computable functions
1569:
1536:
1450:
1247:
1211:
1165:
1139:
1110:
1062:
857:
785:
689:
676:extensional equality
635:
584:
549:
509:
474:
454:
434:
414:
379:
347:
318:
292:
272:
206:
163:
77:computable functions
21:computability theory
2603:
2233:
1935:
1845:
1473:
1154:{\displaystyle m+n}
1079:
879:
802:
526:
364:
333:{\displaystyle x,y}
307:{\displaystyle m,n}
81:Stephen Cole Kleene
55:" (also called the
47:, written also as "
2715:Weisstein, Eric W.
2687:Soare, R. (1987).
2604:
2589:
2526:10.1007/BF01565439
2496:Partial evaluation
2252:
2195:
2137:
2093:
2055:
2012:
1954:
1882:
1825:
1806:
1775:
1695:
1663:
1584:
1551:
1515:
1459:
1417:
1226:
1197:
1151:
1125:
1080:
1065:
1041:
865:
803:
788:
757:
656:
621:
555:
527:
512:
495:
460:
440:
420:
400:
365:
350:
330:
304:
278:
258:
184:
135:of a program with
2653:. North-Holland.
2629:978-0-19-923076-1
2618:Nies, A. (2009).
2273:code implements s
2246:
2215:
2186:
2171:
2119:
1948:
1922:
1873:
1858:
1757:
1724:
1598:computing model.
1576:
1543:
1371:
1289:
1218:
1117:
463:{\displaystyle s}
443:{\displaystyle n}
423:{\displaystyle m}
281:{\displaystyle g}
198:, there exists a
83:(1943). The name
61:parameter theorem
57:translation lemma
2766:
2740:
2739:
2702:
2683:
2664:
2652:
2641:
2613:
2611:
2610:
2605:
2602:
2597:
2581:
2547:
2537:
2475:
2474:
2471:
2468:
2465:
2462:
2459:
2456:
2453:
2450:
2447:
2444:
2441:
2438:
2435:
2432:
2429:
2426:
2423:
2420:
2415:
2414:
2411:
2408:
2405:
2402:
2399:
2396:
2393:
2390:
2387:
2384:
2381:
2378:
2375:
2372:
2369:
2361:
2358:
2355:
2352:
2349:
2346:
2343:
2340:
2337:
2334:
2331:
2328:
2325:
2322:
2319:
2316:
2313:
2310:
2307:
2304:
2301:
2298:
2295:
2292:
2289:
2286:
2283:
2261:
2259:
2258:
2253:
2248:
2247:
2239:
2232:
2221:
2217:
2216:
2208:
2188:
2187:
2179:
2173:
2172:
2164:
2146:
2144:
2143:
2138:
2136:
2135:
2130:
2121:
2120:
2112:
2102:
2100:
2099:
2094:
2092:
2091:
2086:
2064:
2062:
2061:
2056:
2054:
2046:
2045:
2040:
2021:
2019:
2018:
2013:
2011:
2003:
2002:
1991:
1963:
1961:
1960:
1955:
1950:
1949:
1941:
1934:
1929:
1928:
1924:
1923:
1915:
1902:
1901:
1875:
1874:
1866:
1860:
1859:
1851:
1844:
1833:
1815:
1813:
1812:
1807:
1805:
1784:
1782:
1781:
1776:
1774:
1773:
1768:
1759:
1758:
1750:
1741:
1740:
1735:
1726:
1725:
1717:
1704:
1702:
1701:
1696:
1672:
1670:
1669:
1664:
1662:
1654:
1653:
1642:
1633:
1632:
1593:
1591:
1590:
1585:
1583:
1582:
1577:
1574:
1564:
1560:
1558:
1557:
1552:
1550:
1549:
1544:
1541:
1531:
1524:
1522:
1521:
1516:
1511:
1510:
1492:
1491:
1472:
1467:
1446:; it is denoted
1445:
1441:
1437:
1433:
1426:
1424:
1423:
1418:
1410:
1409:
1391:
1390:
1378:
1377:
1372:
1369:
1360:
1359:
1341:
1340:
1328:
1327:
1309:
1308:
1296:
1295:
1290:
1287:
1281:
1280:
1262:
1261:
1239:
1235:
1233:
1232:
1227:
1225:
1224:
1219:
1216:
1206:
1204:
1203:
1198:
1196:
1195:
1177:
1176:
1160:
1158:
1157:
1152:
1134:
1132:
1131:
1126:
1124:
1123:
1118:
1115:
1105:
1101:
1094:Formal statement
1089:
1087:
1086:
1081:
1078:
1073:
1050:
1048:
1047:
1042:
1034:
1033:
1015:
1014:
1002:
1001:
983:
982:
970:
969:
957:
956:
938:
937:
922:
921:
917:
916:
898:
897:
878:
873:
833:
819:
812:
810:
809:
804:
801:
796:
780:
766:
764:
763:
758:
738:
737:
716:
715:
665:
663:
662:
657:
630:
628:
627:
622:
611:
610:
564:
562:
561:
556:
536:
534:
533:
528:
525:
520:
504:
502:
501:
496:
469:
467:
466:
461:
449:
447:
446:
441:
429:
427:
426:
421:
409:
407:
406:
401:
374:
372:
371:
366:
363:
358:
339:
337:
336:
331:
313:
311:
310:
305:
287:
285:
284:
279:
267:
265:
264:
259:
218:
217:
193:
191:
190:
185:
148:, together with
144:
112:and superscript
102:
101:
100:
97:
91:
88:
73:Gödel numberings
43:
42:
41:
38:
32:
29:
2774:
2773:
2769:
2768:
2767:
2765:
2764:
2763:
2744:
2743:
2709:
2699:
2680:
2661:
2630:
2598:
2593:
2587:
2584:
2583:
2562:10.2307/2267778
2545:
2504:
2482:
2472:
2469:
2466:
2463:
2460:
2457:
2454:
2451:
2448:
2445:
2442:
2439:
2436:
2433:
2430:
2427:
2424:
2421:
2418:
2412:
2409:
2406:
2403:
2400:
2397:
2394:
2391:
2388:
2385:
2382:
2379:
2376:
2373:
2370:
2367:
2363:
2362:
2359:
2356:
2353:
2350:
2347:
2344:
2341:
2338:
2335:
2332:
2329:
2326:
2323:
2320:
2317:
2314:
2311:
2308:
2305:
2302:
2299:
2296:
2293:
2290:
2287:
2284:
2281:
2276:
2267:
2238:
2237:
2222:
2207:
2206:
2199:
2178:
2177:
2163:
2162:
2154:
2151:
2150:
2131:
2126:
2125:
2111:
2110:
2108:
2105:
2104:
2087:
2082:
2081:
2070:
2067:
2066:
2050:
2041:
2036:
2035:
2027:
2024:
2023:
2007:
1992:
1987:
1986:
1978:
1975:
1974:
1940:
1939:
1930:
1914:
1913:
1903:
1891:
1887:
1886:
1865:
1864:
1850:
1849:
1834:
1829:
1823:
1820:
1819:
1801:
1790:
1787:
1786:
1769:
1764:
1763:
1749:
1748:
1736:
1731:
1730:
1716:
1715:
1710:
1707:
1706:
1678:
1675:
1674:
1658:
1643:
1638:
1637:
1622:
1618:
1616:
1613:
1612:
1596:Turing-complete
1578:
1573:
1572:
1570:
1567:
1566:
1562:
1545:
1540:
1539:
1537:
1534:
1533:
1529:
1506:
1502:
1487:
1483:
1468:
1463:
1451:
1448:
1447:
1443:
1439:
1435:
1431:
1405:
1401:
1386:
1382:
1373:
1368:
1367:
1355:
1351:
1336:
1332:
1323:
1319:
1304:
1300:
1291:
1286:
1285:
1276:
1272:
1257:
1253:
1248:
1245:
1244:
1237:
1220:
1215:
1214:
1212:
1209:
1208:
1191:
1187:
1172:
1168:
1166:
1163:
1162:
1140:
1137:
1136:
1119:
1114:
1113:
1111:
1108:
1107:
1103:
1099:
1096:
1074:
1069:
1063:
1060:
1059:
1029:
1025:
1010:
1006:
997:
993:
978:
974:
965:
961:
952:
948:
933:
929:
912:
908:
893:
889:
874:
869:
864:
860:
858:
855:
854:
849:
840:
825:
814:
797:
792:
786:
783:
782:
775:
733:
729:
696:
692:
690:
687:
686:
636:
633:
632:
591:
587:
585:
582:
581:
550:
547:
546:
543:
521:
516:
510:
507:
506:
475:
472:
471:
455:
452:
451:
450:, you can make
435:
432:
431:
415:
412:
411:
380:
377:
376:
359:
354:
348:
345:
344:
319:
316:
315:
293:
290:
289:
273:
270:
269:
213:
209:
207:
204:
203:
164:
161:
160:
136:
108:with subscript
98:
95:
93:
92:
89:
86:
85:
39:
36:
34:
33:
30:
27:
26:
17:
12:
11:
5:
2772:
2762:
2761:
2756:
2742:
2741:
2708:
2707:External links
2705:
2704:
2703:
2697:
2684:
2678:
2665:
2659:
2642:
2628:
2615:
2601:
2596:
2592:
2538:
2520:(1): 727–742.
2503:
2500:
2499:
2498:
2493:
2488:
2481:
2478:
2280:
2274:
2269:The following
2266:
2263:
2251:
2245:
2242:
2236:
2231:
2228:
2225:
2220:
2214:
2211:
2205:
2202:
2198:
2194:
2191:
2185:
2182:
2176:
2170:
2167:
2161:
2158:
2134:
2129:
2124:
2118:
2115:
2090:
2085:
2080:
2077:
2074:
2053:
2049:
2044:
2039:
2034:
2031:
2010:
2006:
2001:
1998:
1995:
1990:
1985:
1982:
1953:
1947:
1944:
1938:
1933:
1927:
1921:
1918:
1912:
1909:
1906:
1900:
1897:
1894:
1890:
1885:
1881:
1878:
1872:
1869:
1863:
1857:
1854:
1848:
1843:
1840:
1837:
1832:
1828:
1804:
1800:
1797:
1794:
1772:
1767:
1762:
1756:
1753:
1747:
1744:
1739:
1734:
1729:
1723:
1720:
1714:
1694:
1691:
1688:
1685:
1682:
1661:
1657:
1652:
1649:
1646:
1641:
1636:
1631:
1628:
1625:
1621:
1581:
1548:
1514:
1509:
1505:
1501:
1498:
1495:
1490:
1486:
1482:
1479:
1476:
1471:
1466:
1462:
1458:
1455:
1428:
1427:
1416:
1413:
1408:
1404:
1400:
1397:
1394:
1389:
1385:
1381:
1376:
1366:
1363:
1358:
1354:
1350:
1347:
1344:
1339:
1335:
1331:
1326:
1322:
1318:
1315:
1312:
1307:
1303:
1299:
1294:
1284:
1279:
1275:
1271:
1268:
1265:
1260:
1256:
1252:
1223:
1194:
1190:
1186:
1183:
1180:
1175:
1171:
1150:
1147:
1144:
1122:
1098:Given arities
1095:
1092:
1077:
1072:
1068:
1052:
1051:
1040:
1037:
1032:
1028:
1024:
1021:
1018:
1013:
1009:
1005:
1000:
996:
992:
989:
986:
981:
977:
973:
968:
964:
960:
955:
951:
947:
944:
941:
936:
932:
928:
925:
920:
915:
911:
907:
904:
901:
896:
892:
888:
885:
882:
877:
872:
868:
863:
845:
838:
800:
795:
791:
768:
767:
756:
753:
750:
747:
744:
741:
736:
732:
728:
725:
722:
719:
714:
711:
708:
705:
702:
699:
695:
655:
652:
649:
646:
643:
640:
620:
617:
614:
609:
606:
603:
600:
597:
594:
590:
554:
542:
539:
524:
519:
515:
494:
491:
488:
485:
482:
479:
459:
439:
419:
399:
396:
393:
390:
387:
384:
362:
357:
353:
329:
326:
323:
303:
300:
297:
277:
257:
254:
251:
248:
245:
242:
239:
236:
233:
230:
227:
224:
221:
216:
212:
183:
180:
177:
174:
171:
168:
146:free variables
15:
9:
6:
4:
3:
2:
2771:
2760:
2757:
2755:
2752:
2751:
2749:
2737:
2736:
2731:
2729:
2725:
2721:
2716:
2711:
2710:
2700:
2698:3-540-15299-7
2694:
2690:
2685:
2681:
2679:0-262-68052-1
2675:
2671:
2666:
2662:
2660:0-444-87295-7
2656:
2651:
2650:
2643:
2639:
2635:
2631:
2625:
2621:
2616:
2599:
2594:
2590:
2579:
2575:
2571:
2567:
2563:
2559:
2555:
2551:
2544:
2539:
2535:
2531:
2527:
2523:
2519:
2515:
2511:
2506:
2505:
2497:
2494:
2492:
2489:
2487:
2484:
2483:
2477:
2416:evaluates to
2365:For example,
2278:
2272:
2262:
2240:
2226:
2209:
2200:
2196:
2192:
2180:
2174:
2165:
2156:
2148:
2132:
2122:
2113:
2088:
2078:
2075:
2042:
2032:
2029:
1999:
1996:
1993:
1983:
1980:
1971:
1969:
1964:
1942:
1931:
1916:
1910:
1907:
1898:
1895:
1892:
1888:
1883:
1879:
1867:
1861:
1852:
1841:
1838:
1835:
1830:
1826:
1817:
1798:
1795:
1770:
1760:
1751:
1742:
1737:
1727:
1718:
1692:
1689:
1686:
1683:
1680:
1650:
1647:
1644:
1634:
1629:
1626:
1623:
1619:
1609:
1607:
1604:
1599:
1597:
1579:
1546:
1526:
1507:
1503:
1499:
1496:
1493:
1488:
1484:
1480:
1477:
1469:
1464:
1460:
1456:
1453:
1414:
1406:
1402:
1398:
1395:
1392:
1387:
1383:
1374:
1364:
1356:
1352:
1348:
1345:
1342:
1337:
1333:
1329:
1324:
1320:
1316:
1313:
1310:
1305:
1301:
1292:
1282:
1277:
1273:
1269:
1266:
1263:
1258:
1254:
1243:
1242:
1241:
1221:
1192:
1188:
1184:
1181:
1178:
1173:
1169:
1148:
1145:
1142:
1120:
1091:
1075:
1070:
1066:
1057:
1054:The function
1038:
1030:
1026:
1022:
1019:
1016:
1011:
1007:
1003:
998:
994:
990:
987:
984:
979:
975:
966:
962:
958:
953:
949:
945:
942:
939:
934:
930:
926:
923:
913:
909:
905:
902:
899:
894:
890:
886:
883:
875:
870:
866:
861:
853:
852:
851:
848:
844:
837:
832:
828:
823:
817:
798:
793:
789:
778:
773:
754:
748:
745:
742:
734:
730:
726:
723:
720:
717:
709:
706:
703:
697:
693:
685:
684:
683:
681:
677:
673:
669:
650:
647:
644:
638:
615:
604:
601:
598:
592:
588:
579:
575:
571:
568:
552:
538:
522:
517:
513:
489:
486:
483:
477:
457:
437:
417:
394:
391:
388:
382:
360:
355:
351:
343:The function
341:
327:
324:
321:
301:
298:
295:
275:
252:
249:
246:
240:
237:
231:
222:
214:
210:
201:
197:
178:
175:
172:
166:
157:
155:
151:
147:
143:
139:
134:
130:
126:
122:
117:
115:
111:
107:
103:
82:
78:
74:
70:
66:
62:
58:
54:
53:s-m-n theorem
50:
46:
44:
22:
2733:
2727:
2723:
2719:
2688:
2669:
2648:
2619:
2553:
2549:
2517:
2513:
2364:
2268:
2149:
1972:
1967:
1965:
1818:
1610:
1608:as follows:
1600:
1528:Informally,
1527:
1434:that allows
1429:
1240:, such that
1097:
1055:
1053:
846:
842:
835:
830:
826:
821:
815:
776:
771:
769:
679:
671:
667:
577:
573:
569:
544:
342:
158:
153:
149:
141:
137:
124:
120:
118:
113:
109:
105:
84:
64:
60:
56:
52:
48:
25:
24:
18:
2556:: 150–155.
2330:'lambda
314:tuples for
133:source code
49:smn-theorem
2748:Categories
2718:"Kleene's
2638:1169.03034
2502:References
2277:for Lisp.
2065:such that
1705:such that
196:computable
63:, and the
2735:MathWorld
2614:theorem.)
2534:120517999
2244:→
2213:→
2197:ϕ
2184:→
2169:→
2123:∈
2117:→
2079:∈
2073:∀
2048:→
2005:→
1946:→
1920:→
1884:ϕ
1871:→
1856:→
1827:ϕ
1799:∈
1793:∀
1761:∈
1755:→
1746:∀
1728:∈
1722:→
1713:∀
1690:≥
1656:→
1497:…
1396:…
1346:…
1314:…
1267:…
1251:∀
1236:of arity
1182:…
1135:of arity
1020:…
988:…
963:φ
943:…
927:λ
924:≃
903:…
862:φ
731:φ
721:λ
718:≃
694:φ
589:φ
553:φ
478:ϕ
383:ϕ
211:ϕ
194:which is
129:algorithm
2730:Theorem"
2578:34314018
2486:Currying
2480:See also
2570:2267778
2265:Example
541:Details
75:of the
45:theorem
2695:
2676:
2657:
2636:
2626:
2576:
2568:
2532:
2437:lambda
2422:lambda
2380:lambda
2318:gensym
779:> 0
99:
90:
51:" or "
40:
31:
2574:S2CID
2566:JSTOR
2546:(PDF)
2530:S2CID
2374:'
2285:defun
1603:total
1565:into
841:, …,
200:total
2693:ISBN
2674:ISBN
2655:ISBN
2624:ISBN
2360:))))
2348:list
2336:list
2327:list
2271:Lisp
1973:Let
1673:and
1442:and
1102:and
670:and
631:and
430:and
123:and
23:the
2634:Zbl
2558:doi
2522:doi
2518:112
2470:g42
2428:g42
2371:s11
2321:)))
2306:let
2288:s11
818:+ 1
813:of
19:In
2750::
2732:.
2632:.
2572:.
2564:.
2552:.
2548:.
2528:.
2516:.
2512:.
2476:.
2473:))
2464:))
2434:((
2407:))
2309:((
2275:11
2147::
2103:,
1816::
1785:,
1575:TM
1542:TM
1525:.
1370:TM
1288:TM
1217:TM
1116:TM
1090:.
850::
829:+
774:,
682::
140:+
59:,
2738:.
2728:n
2726:-
2724:m
2722:-
2720:s
2701:.
2682:.
2663:.
2640:.
2600:m
2595:n
2591:S
2580:.
2560::
2554:3
2536:.
2524::
2467:3
2461:y
2458:x
2455:+
2452:(
2449:)
2446:y
2443:x
2440:(
2431:)
2425:(
2419:(
2413:)
2410:3
2404:y
2401:x
2398:+
2395:(
2392:)
2389:y
2386:x
2383:(
2377:(
2368:(
2357:y
2354:x
2351:f
2345:(
2342:)
2339:y
2333:(
2324:(
2315:(
2312:y
2303:(
2300:)
2297:x
2294:f
2291:(
2282:(
2250:)
2241:y
2235:(
2230:)
2227:n
2224:(
2219:)
2210:x
2204:(
2201:S
2193:=
2190:)
2181:y
2175:,
2166:x
2160:(
2157:f
2133:n
2128:N
2114:y
2089:m
2084:N
2076:x
2052:N
2043:m
2038:N
2033::
2030:s
2009:N
2000:m
1997:+
1994:n
1989:N
1984::
1981:f
1952:)
1943:y
1937:(
1932:n
1926:)
1917:x
1911:,
1908:e
1905:(
1899:n
1896:,
1893:m
1889:s
1880:=
1877:)
1868:y
1862:,
1853:x
1847:(
1842:n
1839:+
1836:m
1831:e
1803:N
1796:e
1771:n
1766:N
1752:y
1743:,
1738:m
1733:N
1719:x
1693:1
1687:n
1684:,
1681:m
1660:N
1651:1
1648:+
1645:m
1640:N
1635::
1630:n
1627:,
1624:m
1620:s
1580:x
1563:y
1547:k
1530:S
1513:)
1508:m
1504:y
1500:,
1494:,
1489:1
1485:y
1481:,
1478:x
1475:(
1470:m
1465:n
1461:S
1457:=
1454:k
1444:y
1440:x
1436:k
1432:S
1415:.
1412:)
1407:n
1403:z
1399:,
1393:,
1388:1
1384:z
1380:(
1375:k
1365:=
1362:)
1357:n
1353:z
1349:,
1343:,
1338:1
1334:z
1330:,
1325:m
1321:y
1317:,
1311:,
1306:1
1302:y
1298:(
1293:x
1283::
1278:n
1274:z
1270:,
1264:,
1259:1
1255:z
1238:n
1222:k
1193:m
1189:y
1185:,
1179:,
1174:1
1170:y
1149:n
1146:+
1143:m
1121:x
1104:n
1100:m
1076:1
1071:1
1067:S
1056:s
1039:.
1036:)
1031:n
1027:y
1023:,
1017:,
1012:1
1008:y
1004:,
999:m
995:x
991:,
985:,
980:1
976:x
972:(
967:p
959:.
954:n
950:y
946:,
940:,
935:1
931:y
919:)
914:m
910:x
906:,
900:,
895:1
891:x
887:,
884:p
881:(
876:m
871:n
867:S
847:m
843:x
839:1
836:x
831:n
827:m
822:p
816:m
799:m
794:n
790:S
777:n
772:m
755:.
752:)
749:y
746:,
743:x
740:(
735:p
727:.
724:y
713:)
710:x
707:,
704:p
701:(
698:s
680:x
672:y
668:x
654:)
651:y
648:,
645:x
642:(
639:f
619:)
616:y
613:(
608:)
605:x
602:,
599:p
596:(
593:s
578:f
574:p
570:s
523:n
518:m
514:s
493:)
490:y
487:,
484:x
481:(
458:s
438:n
418:m
398:)
395:y
392:,
389:x
386:(
361:n
356:m
352:s
328:y
325:,
322:x
302:n
299:,
296:m
276:g
256:)
253:y
250:,
247:x
244:(
241:g
238:=
235:)
232:y
229:(
226:)
223:x
220:(
215:s
182:)
179:y
176:,
173:x
170:(
167:g
154:m
150:m
142:n
138:m
125:n
121:m
114:m
110:n
106:S
96:n
94:m
87:S
37:n
35:m
28:S
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.