Knowledge

Recursive definition

Source 📝

31: 427:
Properties of recursively defined functions and sets can often be proved by an induction principle that follows the recursive definition. For example, the definition of the natural numbers presented here directly implies the principle of mathematical induction for natural numbers: if a property holds
836: 1322: 1056: 1362:, for which it is essential that the second clause says "if and only if"; if it had just said "if", the primality of, for instance, the number 4 would not be clear, and the further application of the second clause would be impossible. 1153: 209: 954: 469:
In contrast, a circular definition may have no base case, and even may define the value of a function in terms of that value itself — rather than on other values of the function. Such a situation would lead to an
692: 1167: 1172: 1075: 973: 865: 697: 126: 684: 579: 592:. The formal criteria for what constitutes a valid recursive definition are more complex for the general case. An outline of the general proof and the criteria can be found in 385: 317: 412: 349: 280: 481:, the proof of which is non-trivial. Where the domain of the function is the natural numbers, sufficient conditions for the definition to be valid are that the value of 968: 1070: 121: 2147:
Warren, D.S. and Denecker, M., 2023. A better logical semantics for prolog. In Prolog: The Next 50 Years (pp. 82-92). Cham: Springer Nature Switzerland.
860: 477:
That recursive definitions are valid – meaning that a recursive definition identifies a unique function – is a theorem of set theory known as the
104:
defines values of the function for some inputs in terms of the values of the same function for other (usually smaller) inputs. For example, the
258:
An inductive definition of a set describes the elements in a set in terms of other elements in the set. For example, one definition of the set
462:
being defined in terms of the definition itself, and that all other instances in the inductive clauses must be "smaller" in some sense (i.e.,
831:{\displaystyle {\begin{aligned}h(1)&=a_{0}\\h(i)&=\rho \left(h|_{\{1,2,\ldots ,i-1\}}\right){\text{ for }}i>1.\end{aligned}}} 424:
satisfies the definition. However, condition (3) specifies the set of natural numbers by removing the sets with extraneous members.
1317:{\displaystyle {\begin{aligned}&{\binom {a}{0}}=1,\\&{\binom {1+a}{1+n}}={\frac {(1+a){\binom {a}{n}}}{1+n}}.\end{aligned}}} 2325: 2315: 2403: 2236: 1763:
The program can be used not only to check whether a query is true, but also to generate answers that are true. For example:
2300: 17: 2138:
Denecker, M., Ternovska, E.: A logic of nonmonotone inductive definitions. ACM Trans. Comput. Log. 9(2), 14:1–14:52 (2008)
1346:
any other positive integer is a prime number if and only if it is not divisible by any prime number smaller than itself.
2275: 1905:
Logic programs significantly extend recursive definitions by including the use of negative conditions, implemented by
2213: 2123: 224:
of 0. The definition may also be thought of as giving a procedure for computing the value of the function 
2330: 2197: 648: 513: 2090: 2228: 1998: 466:
to those base cases that terminate the recursion) — a rule also known as "recur only with a simpler case".
2398: 2066: 1424:(wff) in propositional logic is defined recursively as the smallest set satisfying the three rules: 365: 297: 395: 332: 263: 2320: 2305: 2372: 2367: 2342: 2310: 2268: 2115: 2108: 1983: 252: 101: 1350:
The primality of the integer 2 is the base case; checking the primality of any larger integer
447:
Most recursive definitions have two foundations: a base case (basis) and an inductive clause.
2352: 2173: 1158: 1051:{\displaystyle {\begin{aligned}&0\cdot a=0,\\&(1+n)\cdot a=a+n\cdot a.\end{aligned}}} 589: 220: 63: 1578:. For example, the recursive definition of even number can be written as the logic program: 1463:
The definition can be used to determine whether any particular string of symbols is a wff:
2357: 2347: 2003: 478: 248: 1358:, which is well defined by this definition. That last point can be proved by induction on 604:
instead of any well-ordered set) of the general recursive definition will be given below.
8: 2393: 2295: 1988: 1906: 1421: 451: 584:
More generally, recursive definitions of functions can be made whenever the domain is a
2408: 2337: 2048: 1148:{\displaystyle {\begin{aligned}&a^{0}=1,\\&a^{1+n}=a\cdot a^{n}.\end{aligned}}} 251:
states that such a definition indeed defines a function that is unique. The proof uses
2205: 1566: 2261: 2242: 2232: 2209: 2177: 2119: 2040: 1978: 1691: 1571: 67: 204:{\displaystyle {\begin{aligned}&0!=1.\\&(n+1)!=(n+1)\cdot n!.\end{aligned}}} 2201: 2166: 2032: 1680: 471: 83: 51: 1354:
by this definition requires knowing the primality of every integer between 2 and
949:{\displaystyle {\begin{aligned}&0+a=a,\\&(1+n)+a=1+(n+a).\end{aligned}}} 1061: 959: 285: 79: 35: 2387: 2246: 2181: 2044: 1411:
unless it is obtained from the basis and inductive clauses (extremal clause).
593: 1333: 454:
and a recursive definition is that a recursive definition must always have
2192:(1977). "An Introduction to Inductive Definitions". In Barwise, J. (ed.). 2189: 2161: 1371: 71: 47: 2284: 2052: 1973: 1575: 1340: 585: 97: 87: 2196:. Studies in Logic and the Foundations of Mathematics. Vol. 90. 1993: 105: 94: 75: 2036: 420:
There are many sets that satisfy (1) and (2) – for example, the set
74:
1977:740ff). Some examples of recursively-definable objects include
851: 439:, then the property holds of all natural numbers (Aczel 1977:742). 1459:
are wffs and • is one of the logical connectives ∨, ∧, →, or ↔.
1336:
can be defined as the unique set of positive integers satisfying
601: 600:. However, a specific case (domain is restricted to the positive 39: 1694:
to solve goals and answer queries. For example, given the query
27:
Defining elements of a set in terms of other elements in the set
1687: 428:
of the natural number 0 (or 1), and the property holds of
2253: 30: 1560: 637:
mapping a nonempty section of the positive integers into
1170: 1073: 971: 863: 695: 651: 516: 398: 368: 335: 300: 266: 124: 42:, the stages are obtained via a recursive definition. 841: 607: 2114:(1st ed.). New Jersey: Prentice-Hall. p.  2165: 2107: 2023:Henkin, Leon (1960). "On Mathematical Induction". 1316: 1147: 1050: 948: 830: 678: 573: 406: 379: 343: 311: 274: 203: 1244: 1215: 1192: 1179: 214:This definition is valid for each natural number 2385: 442: 218:, because the recursion eventually reaches the 1478:is a wff, because the propositional variables 2269: 2225:Discrete Structures, Logic, and Computability 1287: 1274: 633:is a function which assigns to each function 1365: 854:is defined recursively based on counting as 800: 770: 416:is the smallest set satisfying (1) and (2). 2276: 2262: 660: 488:(i.e., base case) is given, and that for 400: 370: 337: 302: 268: 1574:can be understood as sets of recursive 495:, an algorithm is given for determining 29: 2105: 1561:Recursive definitions as logic programs 846: 679:{\displaystyle h:\mathbb {Z} _{+}\to A} 574:{\displaystyle f(0),f(1),\dots ,f(n-1)} 70:in terms of other elements in the set ( 14: 2386: 2160: 2099: 2089:For a proof of Recursion Theorem, see 2022: 1415: 645:, then there exists a unique function 2257: 2188: 1382:of non-negative evens (basis clause), 34:Four stages in the construction of a 2222: 458:, cases that satisfy the definition 24: 1278: 1219: 1183: 422:{1, 1.649, 2, 2.649, 3, 3.649, …} 25: 2420: 2025:The American Mathematical Monthly 842:Examples of recursive definitions 608:Principle of recursive definition 1567:Definition § Logic programs 1374:can be defined as consisting of 1327: 1686:The logic programming language 2283: 2194:Handbook of Mathematical Logic 2141: 2132: 2083: 2059: 2016: 1268: 1256: 1161:can be defined recursively as 1014: 1002: 936: 924: 906: 894: 765: 742: 736: 709: 703: 670: 568: 556: 541: 535: 526: 520: 182: 170: 161: 149: 13: 1: 2206:10.1016/S0049-237X(08)71120-0 2154: 443:Form of recursive definitions 380:{\displaystyle \mathbb {N} .} 312:{\displaystyle \mathbb {N} .} 2404:Theoretical computer science 1999:Recursion (computer science) 1661:represents the successor of 1435:is a propositional variable. 407:{\displaystyle \mathbb {N} } 344:{\displaystyle \mathbb {N} } 275:{\displaystyle \mathbb {N} } 238:and proceeding onwards with 7: 1967: 10: 2425: 1564: 1064:is defined recursively as 962:is defined recursively as 581:(i.e., inductive clause). 2291: 2092:On Mathematical Induction 1755: 1731: 1725: 1695: 1668: 1662: 1647: 1637: 1366:Non-negative even numbers 588:, using the principle of 450:The difference between a 2110:Topology, a first course 2009: 1911: 1909:, as in the definition: 1765: 1580: 1556:is a logical connective. 1494:is a logical connective. 115:is defined by the rules 62:, is used to define the 2223:Hein, James L. (2010). 2116:68, exercises 10 and 12 2106:Munkres, James (1975). 1754:it produces the answer 1724:it produces the answer 1984:Mathematical induction 1318: 1149: 1052: 950: 832: 680: 575: 408: 381: 345: 313: 276: 253:mathematical induction 205: 43: 2094:(1960) by Leon Henkin 2067:"All About Recursion" 1319: 1159:Binomial coefficients 1150: 1053: 951: 833: 681: 590:transfinite recursion 576: 435:whenever it holds of 409: 382: 346: 314: 277: 249:The recursion theorem 206: 38:. As with many other 33: 2229:Jones & Bartlett 2200:. pp. 739–782. 2004:Structural induction 1989:Recursive data types 1168: 1071: 969: 861: 847:Elementary functions 693: 649: 514: 396: 366: 333: 298: 264: 122: 60:inductive definition 56:recursive definition 18:Inductive definition 1907:negation as failure 1422:well-formed formula 1416:Well formed formula 1404:(inductive clause), 452:circular definition 2399:Mathematical logic 1730:. Given the query 1692:backward reasoning 1538:is a wff, because 1510:is a wff, because 1343:is a prime number, 1314: 1312: 1145: 1143: 1048: 1046: 946: 944: 828: 826: 676: 571: 404: 377: 341: 309: 272: 201: 199: 88:Cantor ternary set 44: 2381: 2380: 2331:Genus–differentia 2238:978-0-7637-7206-2 2071:www.cis.upenn.edu 1979:Logic programming 1305: 1285: 1242: 1190: 813: 625:be an element of 616:be a set and let 479:recursion theorem 84:Fibonacci numbers 16:(Redirected from 2416: 2278: 2271: 2264: 2255: 2254: 2250: 2219: 2185: 2171: 2168:Naive set theory 2148: 2145: 2139: 2136: 2130: 2129: 2113: 2103: 2097: 2087: 2081: 2080: 2078: 2077: 2063: 2057: 2056: 2020: 1963: 1960: 1957: 1954: 1951: 1948: 1945: 1942: 1939: 1936: 1933: 1930: 1927: 1924: 1921: 1918: 1915: 1901: 1898: 1895: 1892: 1889: 1886: 1883: 1880: 1877: 1874: 1871: 1868: 1865: 1862: 1859: 1856: 1853: 1850: 1847: 1844: 1841: 1838: 1835: 1832: 1829: 1826: 1823: 1820: 1817: 1814: 1811: 1808: 1805: 1802: 1799: 1796: 1793: 1790: 1787: 1784: 1781: 1778: 1775: 1772: 1769: 1759: 1758: 1753: 1752: 1749: 1746: 1743: 1740: 1737: 1734: 1729: 1728: 1723: 1722: 1719: 1716: 1713: 1710: 1707: 1704: 1701: 1698: 1681:Peano arithmetic 1678: 1677: 1674: 1671: 1666: 1665: 1660: 1659: 1656: 1653: 1650: 1641: 1640: 1632: 1629: 1626: 1623: 1620: 1617: 1614: 1611: 1608: 1605: 1602: 1599: 1596: 1593: 1590: 1587: 1584: 1555: 1551: 1544: 1537: 1521: 1509: 1493: 1489: 1483: 1477: 1458: 1454: 1450: 1444: 1440: 1434: 1430: 1420:The notion of a 1410: 1403: 1399: 1392: 1388: 1385:For any element 1381: 1378:0 is in the set 1361: 1357: 1353: 1323: 1321: 1320: 1315: 1313: 1306: 1304: 1293: 1292: 1291: 1290: 1277: 1254: 1249: 1248: 1247: 1241: 1230: 1218: 1210: 1197: 1196: 1195: 1182: 1174: 1154: 1152: 1151: 1146: 1144: 1137: 1136: 1118: 1117: 1101: 1088: 1087: 1077: 1057: 1055: 1054: 1049: 1047: 998: 975: 955: 953: 952: 947: 945: 890: 867: 837: 835: 834: 829: 827: 814: 811: 809: 805: 804: 803: 768: 728: 727: 685: 683: 682: 677: 669: 668: 663: 644: 641:, an element of 640: 636: 632: 628: 624: 615: 586:well-ordered set 580: 578: 577: 572: 509: 505: 494: 487: 472:infinite regress 438: 434: 423: 415: 413: 411: 410: 405: 403: 388: 386: 384: 383: 378: 373: 359: 352: 350: 348: 347: 342: 340: 320: 318: 316: 315: 310: 305: 283: 281: 279: 278: 273: 271: 244: 237: 231:, starting from 230: 217: 210: 208: 207: 202: 200: 145: 128: 114: 52:computer science 21: 2424: 2423: 2419: 2418: 2417: 2415: 2414: 2413: 2384: 2383: 2382: 2377: 2287: 2282: 2239: 2216: 2157: 2152: 2151: 2146: 2142: 2137: 2133: 2126: 2104: 2100: 2088: 2084: 2075: 2073: 2065: 2064: 2060: 2037:10.2307/2308975 2021: 2017: 2012: 1970: 1965: 1964: 1961: 1958: 1955: 1952: 1949: 1946: 1943: 1940: 1937: 1934: 1931: 1928: 1925: 1922: 1919: 1916: 1913: 1903: 1902: 1899: 1896: 1893: 1890: 1887: 1884: 1881: 1878: 1875: 1872: 1869: 1866: 1863: 1860: 1857: 1854: 1851: 1848: 1845: 1842: 1839: 1836: 1833: 1830: 1827: 1824: 1821: 1818: 1815: 1812: 1809: 1806: 1803: 1800: 1797: 1794: 1791: 1788: 1785: 1782: 1779: 1776: 1773: 1770: 1767: 1756: 1750: 1747: 1744: 1741: 1738: 1735: 1732: 1726: 1720: 1717: 1714: 1711: 1708: 1705: 1702: 1699: 1696: 1675: 1672: 1669: 1663: 1657: 1654: 1651: 1648: 1638: 1634: 1633: 1630: 1627: 1624: 1621: 1618: 1615: 1612: 1609: 1606: 1603: 1600: 1597: 1594: 1591: 1588: 1585: 1582: 1569: 1563: 1553: 1546: 1539: 1527: 1511: 1499: 1491: 1485: 1479: 1467: 1456: 1452: 1448: 1442: 1438: 1432: 1428: 1418: 1408: 1401: 1394: 1390: 1386: 1379: 1368: 1359: 1355: 1351: 1330: 1311: 1310: 1294: 1286: 1273: 1272: 1271: 1255: 1253: 1243: 1231: 1220: 1214: 1213: 1212: 1208: 1207: 1191: 1178: 1177: 1176: 1171: 1169: 1166: 1165: 1142: 1141: 1132: 1128: 1107: 1103: 1099: 1098: 1083: 1079: 1074: 1072: 1069: 1068: 1045: 1044: 996: 995: 972: 970: 967: 966: 943: 942: 888: 887: 864: 862: 859: 858: 849: 844: 825: 824: 812: for  810: 769: 764: 763: 759: 755: 745: 730: 729: 723: 719: 712: 696: 694: 691: 690: 664: 659: 658: 650: 647: 646: 642: 638: 634: 630: 626: 623: 617: 613: 610: 515: 512: 511: 507: 496: 489: 482: 445: 436: 429: 421: 399: 397: 394: 393: 391: 369: 367: 364: 363: 361: 354: 336: 334: 331: 330: 328: 301: 299: 296: 295: 293: 286:natural numbers 267: 265: 262: 261: 259: 239: 232: 225: 215: 198: 197: 143: 142: 125: 123: 120: 119: 109: 80:natural numbers 28: 23: 22: 15: 12: 11: 5: 2422: 2412: 2411: 2406: 2401: 2396: 2379: 2378: 2376: 2375: 2370: 2365: 2360: 2355: 2350: 2345: 2340: 2335: 2334: 2333: 2323: 2318: 2313: 2308: 2303: 2298: 2292: 2289: 2288: 2281: 2280: 2273: 2266: 2258: 2252: 2251: 2237: 2220: 2214: 2186: 2156: 2153: 2150: 2149: 2140: 2131: 2124: 2098: 2082: 2058: 2031:(4): 323–338. 2014: 2013: 2011: 2008: 2007: 2006: 2001: 1996: 1991: 1986: 1981: 1976: 1969: 1966: 1912: 1766: 1581: 1572:Logic programs 1562: 1559: 1558: 1557: 1524: 1523: 1496: 1495: 1461: 1460: 1446: 1436: 1417: 1414: 1413: 1412: 1407:Nothing is in 1405: 1383: 1367: 1364: 1348: 1347: 1344: 1329: 1326: 1325: 1324: 1309: 1303: 1300: 1297: 1289: 1284: 1281: 1276: 1270: 1267: 1264: 1261: 1258: 1252: 1246: 1240: 1237: 1234: 1229: 1226: 1223: 1217: 1211: 1209: 1206: 1203: 1200: 1194: 1189: 1186: 1181: 1175: 1173: 1156: 1155: 1140: 1135: 1131: 1127: 1124: 1121: 1116: 1113: 1110: 1106: 1102: 1100: 1097: 1094: 1091: 1086: 1082: 1078: 1076: 1062:Exponentiation 1059: 1058: 1043: 1040: 1037: 1034: 1031: 1028: 1025: 1022: 1019: 1016: 1013: 1010: 1007: 1004: 1001: 999: 997: 994: 991: 988: 985: 982: 979: 976: 974: 960:Multiplication 957: 956: 941: 938: 935: 932: 929: 926: 923: 920: 917: 914: 911: 908: 905: 902: 899: 896: 893: 891: 889: 886: 883: 880: 877: 874: 871: 868: 866: 848: 845: 843: 840: 839: 838: 823: 820: 817: 808: 802: 799: 796: 793: 790: 787: 784: 781: 778: 775: 772: 767: 762: 758: 754: 751: 748: 746: 744: 741: 738: 735: 732: 731: 726: 722: 718: 715: 713: 711: 708: 705: 702: 699: 698: 675: 672: 667: 662: 657: 654: 621: 609: 606: 570: 567: 564: 561: 558: 555: 552: 549: 546: 543: 540: 537: 534: 531: 528: 525: 522: 519: 444: 441: 418: 417: 402: 389: 376: 372: 339: 323:If an element 321: 308: 304: 270: 212: 211: 196: 193: 190: 187: 184: 181: 178: 175: 172: 169: 166: 163: 160: 157: 154: 151: 148: 146: 144: 141: 138: 135: 132: 129: 127: 36:Koch snowflake 26: 9: 6: 4: 3: 2: 2421: 2410: 2407: 2405: 2402: 2400: 2397: 2395: 2392: 2391: 2389: 2374: 2371: 2369: 2366: 2364: 2361: 2359: 2356: 2354: 2351: 2349: 2346: 2344: 2341: 2339: 2336: 2332: 2329: 2328: 2327: 2324: 2322: 2319: 2317: 2314: 2312: 2309: 2307: 2304: 2302: 2299: 2297: 2294: 2293: 2290: 2286: 2279: 2274: 2272: 2267: 2265: 2260: 2259: 2256: 2248: 2244: 2240: 2234: 2230: 2226: 2221: 2217: 2215:0-444-86388-5 2211: 2207: 2203: 2199: 2198:North-Holland 2195: 2191: 2187: 2183: 2179: 2175: 2170: 2169: 2163: 2159: 2158: 2144: 2135: 2127: 2125:0-13-925495-1 2121: 2117: 2112: 2111: 2102: 2095: 2093: 2086: 2072: 2068: 2062: 2054: 2050: 2046: 2042: 2038: 2034: 2030: 2026: 2019: 2015: 2005: 2002: 2000: 1997: 1995: 1992: 1990: 1987: 1985: 1982: 1980: 1977: 1975: 1972: 1971: 1910: 1908: 1764: 1761: 1693: 1689: 1684: 1682: 1645: 1579: 1577: 1573: 1568: 1552:are wffs and 1550: 1543: 1535: 1531: 1526: 1525: 1519: 1515: 1507: 1503: 1498: 1497: 1490:are wffs and 1488: 1482: 1475: 1471: 1466: 1465: 1464: 1447: 1437: 1427: 1426: 1425: 1423: 1406: 1397: 1384: 1377: 1376: 1375: 1373: 1363: 1345: 1342: 1339: 1338: 1337: 1335: 1334:prime numbers 1328:Prime numbers 1307: 1301: 1298: 1295: 1282: 1279: 1265: 1262: 1259: 1250: 1238: 1235: 1232: 1227: 1224: 1221: 1204: 1201: 1198: 1187: 1184: 1164: 1163: 1162: 1160: 1138: 1133: 1129: 1125: 1122: 1119: 1114: 1111: 1108: 1104: 1095: 1092: 1089: 1084: 1080: 1067: 1066: 1065: 1063: 1041: 1038: 1035: 1032: 1029: 1026: 1023: 1020: 1017: 1011: 1008: 1005: 1000: 992: 989: 986: 983: 980: 977: 965: 964: 963: 961: 939: 933: 930: 927: 921: 918: 915: 912: 909: 903: 900: 897: 892: 884: 881: 878: 875: 872: 869: 857: 856: 855: 853: 821: 818: 815: 806: 797: 794: 791: 788: 785: 782: 779: 776: 773: 760: 756: 752: 749: 747: 739: 733: 724: 720: 716: 714: 706: 700: 689: 688: 687: 673: 665: 655: 652: 620: 605: 603: 599: 595: 594:James Munkres 591: 587: 582: 565: 562: 559: 553: 550: 547: 544: 538: 532: 529: 523: 517: 503: 499: 492: 485: 480: 475: 473: 467: 465: 461: 457: 453: 448: 440: 432: 425: 390: 374: 357: 326: 322: 306: 291: 290: 289: 287: 256: 254: 250: 246: 242: 235: 228: 223: 222: 194: 191: 188: 185: 179: 176: 173: 167: 164: 158: 155: 152: 147: 139: 136: 133: 130: 118: 117: 116: 112: 107: 103: 99: 96: 91: 89: 85: 81: 77: 73: 69: 65: 61: 57: 53: 49: 41: 37: 32: 19: 2362: 2321:Fallacies of 2306:Coordinative 2224: 2193: 2190:Aczel, Peter 2174:van Nostrand 2167: 2162:Halmos, Paul 2143: 2134: 2109: 2101: 2091: 2085: 2074:. Retrieved 2070: 2061: 2028: 2024: 2018: 1904: 1762: 1685: 1643: 1635: 1570: 1548: 1541: 1533: 1529: 1517: 1513: 1505: 1501: 1486: 1480: 1473: 1469: 1462: 1451:is a wff if 1441:is a wff if 1431:is a wff if 1419: 1395: 1372:even numbers 1369: 1349: 1331: 1157: 1060: 958: 850: 618: 611: 597: 583: 506:in terms of 501: 497: 490: 483: 476: 468: 463: 459: 455: 449: 446: 430: 426: 419: 355: 324: 257: 247: 240: 233: 226: 219: 213: 110: 92: 59: 55: 45: 2373:Theoretical 2368:Stipulative 2343:Operational 2326:Intensional 2316:Extensional 2311:Enumerative 1642:represents 1576:definitions 1389:in the set 1332:The set of 48:mathematics 2394:Definition 2388:Categories 2353:Persuasive 2285:Definition 2155:References 2076:2019-10-24 1974:Definition 1565:See also: 686:such that 456:base cases 98:definition 86:, and the 76:factorials 2409:Recursion 2363:Recursive 2358:Precising 2348:Ostensive 2247:636352297 2182:802530334 2045:0002-9890 1994:Recursion 1667:, namely 1522:is a wff. 1445:is a wff. 1126:⋅ 1036:⋅ 1018:⋅ 981:⋅ 795:− 786:… 753:ρ 671:→ 563:− 548:… 243:= 1, 2, 3 221:base case 186:⋅ 108:function 106:factorial 95:recursive 2296:Circular 2164:(1960). 1968:See also 1679:, as in 852:Addition 602:integers 598:Topology 292:1 is in 102:function 64:elements 40:fractals 2338:Lexical 2301:Concept 2053:2308975 1449:(p • q) 460:without 414:⁠ 392:⁠ 387:⁠ 362:⁠ 351:⁠ 329:⁠ 319:⁠ 294:⁠ 282:⁠ 260:⁠ 2245:  2235:  2212:  2180:  2122:  2051:  2043:  1897:)))))) 1688:Prolog 1646:, and 1400:is in 493:> 0 464:closer 360:is in 327:is in 2049:JSTOR 2010:Notes 1900:..... 1757:false 1690:uses 1636:Here 1532:∧ ¬ 629:. If 353:then 245:etc. 100:of a 72:Aczel 66:in a 58:, or 2243:OCLC 2233:ISBN 2210:ISBN 2178:OCLC 2120:ISBN 2041:ISSN 1953:even 1926:even 1914:even 1849:)))) 1771:even 1736:even 1727:true 1700:even 1622:even 1595:even 1583:even 1545:and 1484:and 1455:and 1370:The 819:> 612:Let 288:is: 54:, a 50:and 2202:doi 2033:doi 1962:)). 1947:not 1721:))) 1683:. 1616:))) 1528:(¬ 1500:¬ ( 1439:¬ p 1398:+ 2 486:(0) 433:+ 1 358:+ 1 284:of 236:= 0 68:set 46:In 2390:: 2241:. 2231:. 2227:. 2208:. 2176:. 2172:. 2118:. 2069:. 2047:. 2039:. 2029:67 2027:. 1944::- 1941:)) 1923:). 1813:)) 1780:). 1768:?- 1760:. 1751:)) 1733:?- 1697:?- 1644:if 1639::- 1631:). 1619::- 1592:). 1547:¬ 1540:¬ 1516:∧ 1504:∧ 1472:∧ 1393:, 822:1. 596:' 510:, 474:. 255:. 140:1. 93:A 90:. 82:, 78:, 2277:e 2270:t 2263:v 2249:. 2218:. 2204:: 2184:. 2128:. 2096:. 2079:. 2055:. 2035:: 1959:X 1956:( 1950:( 1938:X 1935:( 1932:s 1929:( 1920:0 1917:( 1894:0 1891:( 1888:s 1885:( 1882:s 1879:( 1876:s 1873:( 1870:s 1867:( 1864:s 1861:( 1858:s 1855:= 1852:X 1846:0 1843:( 1840:s 1837:( 1834:s 1831:( 1828:s 1825:( 1822:s 1819:= 1816:X 1810:0 1807:( 1804:s 1801:( 1798:s 1795:= 1792:X 1789:0 1786:= 1783:X 1777:X 1774:( 1748:0 1745:( 1742:s 1739:( 1718:0 1715:( 1712:s 1709:( 1706:s 1703:( 1676:1 1673:+ 1670:X 1664:X 1658:) 1655:X 1652:( 1649:s 1628:X 1625:( 1613:X 1610:( 1607:s 1604:( 1601:s 1598:( 1589:0 1586:( 1554:∧ 1549:q 1542:p 1536:) 1534:q 1530:p 1520:) 1518:q 1514:p 1512:( 1508:) 1506:q 1502:p 1492:∧ 1487:q 1481:p 1476:) 1474:q 1470:p 1468:( 1457:q 1453:p 1443:p 1433:p 1429:p 1409:E 1402:E 1396:x 1391:E 1387:x 1380:E 1360:X 1356:X 1352:X 1341:2 1308:. 1302:n 1299:+ 1296:1 1288:) 1283:n 1280:a 1275:( 1269:) 1266:a 1263:+ 1260:1 1257:( 1251:= 1245:) 1239:n 1236:+ 1233:1 1228:a 1225:+ 1222:1 1216:( 1205:, 1202:1 1199:= 1193:) 1188:0 1185:a 1180:( 1139:. 1134:n 1130:a 1123:a 1120:= 1115:n 1112:+ 1109:1 1105:a 1096:, 1093:1 1090:= 1085:0 1081:a 1042:. 1039:a 1033:n 1030:+ 1027:a 1024:= 1021:a 1015:) 1012:n 1009:+ 1006:1 1003:( 993:, 990:0 987:= 984:a 978:0 940:. 937:) 934:a 931:+ 928:n 925:( 922:+ 919:1 916:= 913:a 910:+ 907:) 904:n 901:+ 898:1 895:( 885:, 882:a 879:= 876:a 873:+ 870:0 816:i 807:) 801:} 798:1 792:i 789:, 783:, 780:2 777:, 774:1 771:{ 766:| 761:h 757:( 750:= 743:) 740:i 737:( 734:h 725:0 721:a 717:= 710:) 707:1 704:( 701:h 674:A 666:+ 661:Z 656:: 653:h 643:A 639:A 635:f 631:ρ 627:A 622:0 619:a 614:A 569:) 566:1 560:n 557:( 554:f 551:, 545:, 542:) 539:1 536:( 533:f 530:, 527:) 524:0 521:( 518:f 508:n 504:) 502:n 500:( 498:f 491:n 484:f 437:n 431:n 401:N 375:. 371:N 356:n 338:N 325:n 307:. 303:N 269:N 241:n 234:n 229:! 227:n 216:n 195:. 192:! 189:n 183:) 180:1 177:+ 174:n 171:( 168:= 165:! 162:) 159:1 156:+ 153:n 150:( 137:= 134:! 131:0 113:! 111:n 20:)

Index

Inductive definition

Koch snowflake
fractals
mathematics
computer science
elements
set
Aczel
factorials
natural numbers
Fibonacci numbers
Cantor ternary set
recursive
definition
function
factorial
base case
The recursion theorem
mathematical induction
natural numbers
circular definition
infinite regress
recursion theorem
well-ordered set
transfinite recursion
James Munkres
integers
Addition
Multiplication

Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.