Meta tags:
Headings (most frequently used words):
functions, primitive, recursive, predicate, definition, to, and, or, equal, operations, on, numbers, function, contents, examples, relationship, limitations, variants, finitism, consistency, results, history, see, also, notes, references, recursiveness, of, vector, valued, addition, doubling, multiplication, predecessor, truncated, subtraction, converting, predicates, numeric, is, zero, less, greater, if, then, else, junctors, equality, other, natural, integers, rational, some, common, constant, iterative, pure, recursion, additional, forms, computer, language,
Text of the page (most frequently used words):
the (255), displaystyle (183), recursive (140), primitive (123), operatorname (121), #function (108), and (105), functions (90), that (78), def (54), for (53), add (47), are (44), text (43), circ (41), can (38), edit (35), theory (33), pred (33), not (32), this (31), leq (31), aligned (30), rho (30), with (26), then (26), from (23), all (22), definition (22), ldots (22), iszero (22), recursion (21), predicate (21), number (21), ary (21), total (21), set (20), case (20), logic (19), loop (19), which (19), defined (19), such (18), rsub (18), begin (17), end (17), mul (16), computable (15), numbers (15), argument (15), one (15), value (14), proof (14), true (14), example (14), language (14), natural (13), gödel (13), also (13), where (13), every (13), geq (13), isbn (12), some (12), sub (12), operations (11), there (11), turing (10), truth (10), arithmetic (10), logical (10), its (10), obtained (10), returns (10), operator (10), arguments (10), property (10), else (10), was (9), mathematical (9), theorem (9), list (9), first (9), many (9), consistency (9), but (9), definitions (9), may (8), computation (8), general (8), doi (8), unary (8), known (8), less (8), pra (8), define (8), given (8), addition (8), dots (8), wikipedia (7), using (7), mathematics (7), complexity (7), rule (7), formal (7), constant (7), 1967 (7), press (7), only (7), initial (7), called (7), proofs (7), than (7), input (7), loops (7), these (7), subtraction (7), successor (7), examples (7), predicates (7), non (6), computability (6), history (6), enumerable (6), tarski (6), finite (6), order (6), valued (6), recursively (6), gladstone (6), see (6), computer (6), used (6), more (6), following (6), other (6), basic (6), values (6), two (6), composition (6), multiplication (6), mathbin (6), dot (6), calculations (6), languages (5), toggle (5), search (5), page (5), calculus (5), model (5), robinson (5), second (5), variable (5), ackermann (5), 1974 (5), university (5), most (5), bounded (5), programming (5), proved (5), results (5), each (5), will (5), forms (5), fact (5), pure (5), way (5), zero (5), partial (5), otherwise (5), predecessor (5), mathbb (5), stackrel (5), mathrm (5), contents (4), additional (4), use (4), articles (4), machine (4), problem (4), complete (4), prime (4), skolem (4), peano (4), propositional (4), axiom (4), enumeration (4), class (4), fixed (4), jstor (4), symbolic (4), vector (4), kleene (4), 978 (4), fachini (4), maggiolo (4), schettini (4), sequence (4), cambridge (4), form (4), here (4), implies (4), similarly (4), steps (4), equals (4), greater (4), main (4), course (4), does (4), have (4), always (4), show (4), enumerated (4), however (4), those (4), once (4), since (4), computed (4), subset (4), they (4), common (4), similar (4), integers (4), equal (4), equations (4), hide (4), move (4), sidebar (4), view (3), unsourced (3), statements (3), 2025 (3), category (3), sets (3), related (3), type (3), theories (3), semantics (3), elementary (3), standard (3), equivalence (3), atomic (3), ordinal (3), systems (3), axioms (3), boolean (3), substitution (3), functional (3), free (3), bound (3), relation (3), foundations (3), power (3), paradox (3), diagonal (3), theorems (3), 2307 (3), severin (3), journal (3), 1947 (3), introduction (3), computational (3), applied (3), current (3), after (3), had (3), what (3), been (3), before (3), finitistic (3), any (3), into (3), syntactic (3), system (3), finitism (3), their (3), while (3), characterization (3), times (3), truncated (3), get (3), possible (3), even (3), iteration (3), namely (3), parameters (3), just (3), identity (3), variants (3), takes (3), explicitly (3), same (3), effectively (3), itself (3), very (3), create (3), limitations (3), provably (3), well (3), sum (3), has (3), equation (3), cases (3), represent (3), false (3), converting (3), rational (3), implements (3), equality (3), junctors (3), part (3), numeric (3), article (3), quad (3), tools (3), subsection (3), table (2), contact (2), about (2), privacy (2), policy (2), terms (2), categories (2), short (2), description (2), different (2), wikidata (2), retrieved (2), index (2), portal (2), abstract (2), lambda (2), undecidable (2), computably (2), church (2), validity (2), schema (2), kripke (2), diagram (2), spectrum (2), models (2), interpretation (2), reverse (2), hilbert (2), axiomatic (2), inference (2), consequence (2), euclidean (2), real (2), sentence (2), ground (2), formula (2), automata (2), constructive (2), von (2), neumann (2), grothendieck (2), new (2), numbering (2), domain (2), cardinality (2), product (2), forcing (2), monadic (2), halting (2), cantor (2), incompleteness (2), information (2), 321 (2), 420992 (2), bulletin (2), soare (2), robert (2), 1987 (2), 2008 (2), american (2), society (2), reprint (2), planetmath (2), 2nd (2), 1989 (2), proceedings (2), vol (2), hartmanis (2), 1971 (2), scheme (2), 2272468 (2), 2270177 (2), emanuela (2), andrea (2), 1982 (2), und (2), 1979 (2), pdf (2), hierarchy (2), brainerd (2), landweber (2), 2002 (2), jeffrey (2), richard (2), burgess (2), boolos (2), george (2), references (2), 1923 (2), van (2), thoralf (2), 107 (2), legacy (2), peter (2), ritchie (2), dennis (2), meyer (2), albert (2), follows (2), time (2), 2011 (2), 332 (2), science (2), notes (2), terminology (2), need (2), were (2), simply (2), construction (2), certain (2), defines (2), unique (2), interest (2), themselves (2), inconsistency (2), formalized (2), closely (2), particularly (2), them (2), halts (2), hand (2), variant (2), unbounded (2), goto (2), operators (2), upper (2), body (2), generality (2), gives (2), run (2), suffices (2), generate (2), include (2), without (2), enough (2), restrictions (2), below (2), considered (2), access (2), iterative (2), citation (2), needed (2), cannot (2), particular (2), uses (2), assumed (2), indeed (2), means (2), would (2), now (2), contradiction (2), converse (2), thus (2), encoded (2), states (2), result (2), equivalent (2), relationship (2), satisfies (2), shall (2), least (2), denotes (2), exists (2), definable (2), meaning (2), logarithm (2), convention (2), item (2), remainder (2), signum (2), factorial (2), exponentiation (2), mark (2), expressed (2), appear (2), above (2), easy (2), defining (2), identification (2), runs (2), over (2), reversed (2), denoted (2), acts (2), doubling (2), suggests (2), choose (2), obtain (2), right (2), projection (2), recursiveness (2), applying (2), rest (2), conditions (2), immutable (2), perform (2), parameter (2), fed (2), previous (2), appearance (2), upload (2), file (2), changes (2), links (2), read (2), log (2), account (2), donate (2), menu (2), topic, mobile, cookie, statement, statistics, developers, code, conduct, legal, safety, contacts, disclaimers, available, under, apply, site, you, agree, registered, trademark, profit, organization, wikimedia, foundation, inc, creative, commons, attribution, sharealike, license, rendered, parsoid, last, edited, august, 2026, utc, hidden, july, january, mappings, https, org, php, title, primitive_recursive_function, oldid, 1372483162, supertask, philosophy, object, logicism, timeline, concrete, automated, proving, algebraic, kolmogorov, versus, decidable, decision, thesis, encoding, ultraproduct, transfer, principle, semantic, strength, satisfiability, categorical, submodel, saturated, self, verifying, analysis, impossibility, zfc, independence, deductive, sequent, deduction, principia, mathematica, elements, geometry, minimal, canonical, algebras, axiomatization, term, symbol, string, signature, rank, quantifier, connective, metalanguage, open, closed, grammar, formation, conservative, extension, expression, arity, alphabet, syntax, bernays, naive, morse, kelley, platek, continuum, hypothesis, choice, zermelo, fraenkel, binary, operation, aleph, inaccessible, large, cardinal, isomorphism, schröder, bernstein, jection, sur, image, codomain, map, maps, constructible, universe, universal, fuzzy, ultrafilter, transitive, infinite, singleton, inhabited, empty, uncountable, countable, types, identities, cartesian, complement, union, intersection, partition, extensionality, element, hereditary, quantifiers, point, higher, tables, connectives, algebra, venn, square, opposition, syllogism, soundness, equiconsistency, proposition, tautology, classical, traditional, logics, russell, löwenheim, lindström, compactness, banach, undefinability, completeness, paradoxes, lemma, 1996, 1416870, 284, springer, verlag, 387, 15299, degrees, daniel, 1138, 2467207, 275903221, 2178, jsl, 1230396909, 0603063, arxiv, 1122, raphael, 942, 0022536, 1090, s0002, 9904, 08911, 925, rogers, hartley, 9780262680523, mit, effective, 1952, chapter, 7th, 3757798, oclc, 0444100881, north, holland, publishing, company, metamathematics, stephen, cole, overview, symposia, 1020807, 8218, 0131, juris, simplifications, 665, 0305993, 653, reduction, 508, 0224460, 505, comparing, hierarchies, 445, 1002, malq, 19820282705, 431, zeitschrift, für, mathematische, logik, grundlagen, der, mathematik, 1051, ita, 1979130100491, rairo, informatique, théorique, wiley, 0471095850, 4th, 9780521007580, john, translator, harvard, univ, 302, frege, source, book, 1879, 1931, jean, heijenoort, rod, downey, 2014, 474, 04348, developments, ideas, tourlakis, 2003, 129, 139, 43942, lectures, volume, smith, 2013, 02284, programs, 469, 1145, 800196, 806014, 465, acm, 22nd, national, conference, facts, quickly, growing, former, latter, mertens, stephan, oxford, 287, 9780191620805, nature, moore, cristopher, linz, jones, bartlett, publishers, 9781449615529, 226, 227, 331, 1990, handbook, theoretical, elsevier, 364, 444, 88074, jan, leeuwen, henk, barendregt, tail, call, double, grzegorczyk, coined, 1934, 1928, today, named, him, event, prompted, rename, until, rózsa, péter, proposed, formally, traced, back, 126, his, 1888, work, give, sind, sollen, die, zahlen, dedekind, finitistically, acceptable, establishes, producing, transform, sufficient, condition, ability, formalize, recast, carry, out, corresponding, transformations, satisfying, hypotheses, proves, implication, con, much, weaker, nevertheless, giving, several, contexts, desired, often, purpose, introduced, paper, computing, coincides, adding, makes, world, escher, bach, bloop, douglas, hofstadter, contains, subtract, conditionals, comparison, calculable, neither, nor, modifiable, control, structures, plus, admitted, programmed, exactly, limitation, compared, specified, begins, easier, find, reading, writing, mutual, extend, additionally, further, improvements, prove, improved, combination, another, restriction, induction, still, various, assume, loss, instead, alternative, build, goodstein, sudan, involves, paris, harrington, shows, note, instance, enumerating, encodings, machines, essentially, expressions, atoms, contain, though, occur, composing, generates, infinitely, determined, encode, let, denote, suppose, occurs, evaluator, clearly, determine, being, tend, correspond, our, intuition, must, certainly, intuitively, simplicity, straightforward, seen, provides, sketch, enumerate, largest, constructed, iteratively, repeating, ways, creating, leading, diagonalization, inverses, pairing, important, single, enumerates, provable, within, fewer, broader, introducing, fail, encodes, original, mutually, exclusive, clause, applies, minimization, not_q, substituting, respective, variables, constants, abbreviation, subscripts, requires, base, greatest, length, vanishing, exponents, exponent, 1th, presently, especially, computers, amounts, changing, next, leftover, divide, evenly, mod, divides, absolute, difference, maximum, minimum, proper, decrement, usually, thought, respect, extracting, arithmetical, names, either, depending, exact, derivation, 222, 231, extended, operate, objects, including, rationals, represented, field, numberings, when, primality, testing, lead, appropriate, negation, disjunction, based, obtains, both, conjunction, arbitrary, precisely, iff, achieved, settings, consider, take, inputs, tuples, mix, produce, outputs, accomplished, identifying, manner, identify, made, viewed, tells, whether, characteristic, rid, limited, monus, opposite, rules, reproduces, doubles, rephrased, therefore, compute, appropriately, moreover, reasons, authors, adds, left, pairs, respectively, component, scalar, written, during, side, performs, subsequent, performed, mentioned, earlier, altered, ordinary, complex, postulates, nonnegative, integer, importance, lies, studied, generally, showing, size, hence, devise, shown, section, exponential, division, roughly, speaking, whose, iterations, entering, strict, program, encyclopedia, projects, printable, version, download, print, export, switch, parser, shortened, url, cite, permanent, link, actions, english, talk, українська, српски, srpski, português, nederlands, 한국어, 日本語, italiano, עברית, français, español, deutsch, čeština, català, العربية, top, personal, special, pages, recent, community, learn, help, contribute, random, events, navigation, jump, content,
Text of the page (random words):
n menu move to sidebar hide navigation main page contents current events random article about wikipedia contact us contribute help learn to edit community portal recent changes upload file special pages search search appearance donate create account log in personal tools donate create account log in contents move to sidebar hide top 1 definition toggle definition subsection 1 1 primitive recursiveness of vector valued functions 2 examples toggle examples subsection 2 1 addition 2 2 doubling 2 3 multiplication 2 4 predecessor 2 5 truncated subtraction 2 6 converting predicates to numeric functions 2 7 predicate is zero 2 8 predicate less or equal 2 9 predicate greater or equal 2 10 if then else 2 11 junctors 2 12 equality predicate 2 13 other operations on natural numbers 2 14 operations on integers and rational numbers 2 15 some common primitive recursive functions 3 relationship to recursive functions 4 limitations 5 variants toggle variants subsection 5 1 constant functions 5 2 iterative functions 5 3 pure recursion 5 4 additional primitive recursive forms 5 5 computer language definition 6 finitism and consistency results 7 history 8 see also 9 notes 10 references toggle the table of contents primitive recursive function 15 languages العربية català čeština deutsch español français עברית italiano 日本語 한국어 nederlands português српски srpski українська 中文 edit links article talk english read edit view history tools tools move to sidebar hide actions read edit view history general what links here related changes upload file permanent link page information cite this page get shortened url switch to legacy parser print export download as pdf printable version in other projects wikidata item appearance move to sidebar hide from wikipedia the free encyclopedia function computable with bounded loops in computability theory a primitive recursive function is roughly speaking a function that can be computed by a computer program whose loops are all for loops that is an upper bound of the number of iterations of every loop is fixed before entering the loop primitive recursive functions form a strict subset of those general recursive functions that are also total functions the importance of primitive recursive functions lies in the fact that most computable functions that are studied in number theory and more generally in mathematics are primitive recursive for example addition and division the factorial and exponential function and the function which returns the n th prime are all primitive recursive 1 in fact for showing that a computable function is primitive recursive it suffices to show that its time complexity is bounded above by a primitive recursive function of the input size 2 it is hence not particularly easy to devise a computable function that is not primitive recursive some examples are shown in section limitations below the set of primitive recursive functions is known as pr in computational complexity theory definition edit a primitive recursive function takes a fixed number of arguments each a natural number nonnegative integer 0 1 2 and returns a natural number if it takes n arguments it is called n ary the basic primitive recursive functions are given by these axioms constant functions c n k displaystyle c_ n k for each natural number n displaystyle n and every k displaystyle k the k ary constant function defined by c n k x 1 x k d e f n displaystyle c_ n k x_ 1 ldots x_ k stackrel mathrm def n is primitive recursive successor function the 1 ary successor function s which returns the successor of its argument see peano postulates that is s x d e f x 1 displaystyle s x stackrel mathrm def x 1 is primitive recursive projection functions p i k displaystyle p_ i k for all natural numbers i k displaystyle i k such that 1 i k displaystyle 1 leq i leq k the k ary function defined by p i k x 1 x k d e f x i displaystyle p_ i k x_ 1 ldots x_ k stackrel mathrm def x_ i is primitive recursive more complex primitive recursive functions can be obtained by applying the operations given by these axioms composition operator displaystyle circ also called the substitution operator given an m ary function h x 1 x m displaystyle h x_ 1 ldots x_ m and m k ary functions g 1 x 1 x k g m x 1 x k displaystyle g_ 1 x_ 1 ldots x_ k ldots g_ m x_ 1 ldots x_ k h g 1 g m d e f f where f x 1 x k h g 1 x 1 x k g m x 1 x k displaystyle h circ g_ 1 ldots g_ m stackrel mathrm def f quad text where quad f x_ 1 ldots x_ k h g_ 1 x_ 1 ldots x_ k ldots g_ m x_ 1 ldots x_ k for m 1 displaystyle m 1 the ordinary function composition h g 1 displaystyle h circ g_ 1 is obtained primitive recursion operator ρ displaystyle rho given the k ary function g x 1 x k displaystyle g x_ 1 ldots x_ k and the k 2 displaystyle k 2 ary function h y z x 1 x k displaystyle h y z x_ 1 ldots x_ k ρ g h d e f f where the k 1 ary function f is defined by f y x 1 x k g x 1 x k if y 0 h y f y x 1 x k x 1 x k if y s y for a y n displaystyle begin aligned rho g h stackrel mathrm def f quad text where the k 1 text ary function f text is defined by f y x_ 1 dots x_ k begin cases g x_ 1 dots x_ k text if y 0 h y f y x_ 1 dots x_ k x_ 1 dots x_ k text if y s y text for a y in mathbb n end cases end aligned interpretation the function f displaystyle f acts as a for loop from 0 displaystyle 0 up to the value of its first argument the rest of the arguments for f displaystyle f denoted here with x 1 x k displaystyle x_ 1 ldots x_ k are a set of initial conditions for the for loop which may be used by it during calculations but which are immutable by it the functions g displaystyle g and h displaystyle h on the right hand side of the equations that define f displaystyle f represent the body of the loop which performs calculations the function g displaystyle g is used only once to perform initial calculations calculations for subsequent steps of the loop are performed by h displaystyle h the first parameter of h displaystyle h is fed the current value of the for loop s index the second parameter of h displaystyle h is fed the result of the for loop s previous calculations from previous steps the rest of the parameters for h displaystyle h are those immutable initial conditions for the for loop mentioned earlier they may be used by h displaystyle h to perform calculations but they will not themselves be altered by h displaystyle h the primitive recursive functions are the basic functions and those obtained from the basic functions by applying these operations a finite number of times primitive recursiveness of vector valued functions edit a vector valued function 5 f n m n n displaystyle f mathbb n m to mathbb n n is primitive recursive if it can be written as f x 1 x m f 1 x 1 x m f n x 1 x m displaystyle f x_ 1 dots x_ m f_ 1 x_ 1 dots x_ m dots f_ n x_ 1 dots x_ m where each component f i n m n displaystyle f_ i mathbb n m to mathbb n is a scalar valued primitive recursive function 6 examples edit c 0 1 displaystyle c_ 0 1 is a 1 ary function which returns 0 displaystyle 0 for every input c 0 1 x 0 displaystyle c_ 0 1 x 0 c 1 1 displaystyle c_ 1 1 is a 1 ary function which returns 1 displaystyle 1 for every input c 1 1 x 1 displaystyle c_ 1 1 x 1 c 3 0 displaystyle c_ 3 0 is a 0 ary function i e a constant c 3 0 3 displaystyle c_ 3 0 3 p 1 1 displaystyle p_ 1 1 is the identity function on the natural numbers p 1 1 x x displaystyle p_ 1 1 x x p 1 2 displaystyle p_ 1 2 and p 2 2 displaystyle p_ 2 2 is the left and right projection on natural number pairs respectively p 1 2 x y x displaystyle p_ 1 2 x y x and p 2 2 x y y displaystyle p_ 2 2 x y y s s displaystyle s circ s is a 1 ary function that adds 2 to its input s s x x 2 displaystyle s circ s x x 2 s c 0 1 displaystyle s circ c_ 0 1 is a 1 ary function which returns 1 for every input s c 0 1 x s c 0 1 x s 0 1 displaystyle s circ c_ 0 1 x s c_ 0 1 x s 0 1 that is s c 0 1 displaystyle s circ c_ 0 1 and c 1 1 displaystyle c_ 1 1 are the same function s c 0 1 c 1 1 displaystyle s circ c_ 0 1 c_ 1 1 in a similar way every c n k displaystyle c_ n k can be expressed as a composition of appropriately many s displaystyle s and c 0 k displaystyle c_ 0 k moreover c 0 k displaystyle c_ 0 k equals c 0 1 p 1 k displaystyle c_ 0 1 circ p_ 1 k since c 0 k x 1 x k 0 c 0 1 x 1 c 0 1 p 1 k x 1 x k c 0 1 p 1 k x 1 x k displaystyle c_ 0 k x_ 1 ldots x_ k 0 c_ 0 1 x_ 1 c_ 0 1 p_ 1 k x_ 1 ldots x_ k c_ 0 1 circ p_ 1 k x_ 1 ldots x_ k for these reasons some authors 7 define c n k displaystyle c_ n k only for n 0 displaystyle n 0 and k 1 displaystyle k 1 addition edit a definition of the 2 ary function add displaystyle operatorname add to compute the sum of its arguments can be obtained using the primitive recursion operator ρ displaystyle rho to this end the well known equations 0 y y s x y s x y displaystyle begin aligned 0 y y s x y s x y end aligned are rephrased in primitive recursive function terminology in the definition of ρ g h displaystyle rho g h the first equation suggests to choose g p 1 1 displaystyle g p_ 1 1 to obtain add 0 y g y y displaystyle operatorname add 0 y g y y the second equation suggests to choose h s p 2 3 displaystyle h s circ p_ 2 3 to obtain add s x y h x add x y y s p 2 3 x add x y y s add x y displaystyle operatorname add s x y h x operatorname add x y y s circ p_ 2 3 x operatorname add x y y s operatorname add x y therefore the addition function can be defined as add ρ p 1 1 s p 2 3 displaystyle operatorname add rho p_ 1 1 s circ p_ 2 3 as a computation example add 1 7 ρ p 1 1 s p 2 3 s 0 7 by def add s s p 2 3 0 add 0 7 7 by case ρ g h s s add 0 7 by def p 2 3 s ρ p 1 1 s p 2 3 0 7 by def add s p 1 1 7 by case ρ g h 0 s 7 by def p 1 1 8 by def s displaystyle begin aligned operatorname add 1 7 rho p_ 1 1 s circ p_ 2 3 s 0 7 text by def operatorname add s s circ p_ 2 3 0 operatorname add 0 7 7 text by case rho g h s s operatorname add 0 7 text by def circ p_ 2 3 s rho p_ 1 1 s circ p_ 2 3 0 7 text by def operatorname add s p_ 1 1 7 text by case rho g h 0 s 7 text by def p_ 1 1 8 text by def s end aligned doubling edit given add displaystyle operatorname add the 1 ary function add p 1 1 p 1 1 displaystyle operatorname add circ p_ 1 1 p_ 1 1 doubles its argument add p 1 1 p 1 1 x add x x x x displaystyle operatorname add circ p_ 1 1 p_ 1 1 x operatorname add x x x x multiplication edit in a similar way as addition multiplication can be defined by mul ρ c 0 1 add p 2 3 p 3 3 displaystyle operatorname mul rho c_ 0 1 operatorname add circ p_ 2 3 p_ 3 3 this reproduces the well known multiplication equations mul 0 y ρ c 0 1 add p 2 3 p 3 3 0 y by def mul c 0 1 y by case ρ g h 0 0 by def c 0 1 displaystyle begin aligned operatorname mul 0 y rho c_ 0 1 operatorname add circ p_ 2 3 p_ 3 3 0 y text by def operatorname mul c_ 0 1 y text by case rho g h 0 0 text by def c_ 0 1 end aligned and mul s x y ρ c 0 1 add p 2 3 p 3 3 s x y by def mul add p 2 3 p 3 3 x mul x y y by case ρ g h s add mul x y y by def p 2 3 p 3 3 mul x y y by property of add displaystyle begin aligned operatorname mul s x y rho c_ 0 1 operatorname add circ p_ 2 3 p_ 3 3 s x y text by def operatorname mul operatorname add circ p_ 2 3 p_ 3 3 x operatorname mul x y y text by case rho g h s operatorname add operatorname mul x y y text by def circ p_ 2 3 p_ 3 3 operatorname mul x y y text by property of operatorname add end aligned predecessor edit the predecessor function acts as the opposite of the successor function and is recursively defined by the rules pred 0 0 displaystyle operatorname pred 0 0 and pred s n n displaystyle operatorname pred s n n a primitive recursive definition is pred ρ c 0 0 p 1 2 displaystyle operatorname pred rho c_ 0 0 p_ 1 2 as a computation example pred 8 ρ c 0 0 p 1 2 s 7 by def pred s p 1 2 7 pred 7 by case ρ g h s 7 by def p 1 2 displaystyle begin aligned operatorname pred 8 rho c_ 0 0 p_ 1 2 s 7 text by def operatorname pred s p_ 1 2 7 operatorname pred 7 text by case rho g h s 7 text by def p_ 1 2 end aligned truncated subtraction edit the limited subtraction function also called monus and denoted displaystyle mathbin dot is definable from the predecessor function it satisfies the equations y 0 y y s x pred y x displaystyle begin aligned y mathbin dot 0 y y mathbin dot s x operatorname pred y mathbin dot x end aligned since the recursion runs over the second argument we begin with a primitive recursive definition of the reversed subtraction rsub y x x y displaystyle operatorname rsub y x x mathbin dot y its recursion then runs over the first argument so its primitive recursive definition can be obtained similar to addition as rsub ρ p 1 1 pred p 2 3 displaystyle operatorname rsub rho p_ 1 1 operatorname pred circ p_ 2 3 to get rid of the reversed argument order then define sub rsub p 2 2 p 1 2 displaystyle operatorname sub operatorname rsub circ p_ 2 2 p_ 1 2 as a computation example sub 8 1 rsub p 2 2 p 1 2 8 1 by def sub rsub 1 8 by def p 2 2 p 1 2 ρ p 1 1 pred p 2 3 s 0 8 by def rsub s pred p 2 3 0 rsub 0 8 8 by case ρ g h s pred rsub 0 8 by def p 2 3 pred ρ p 1 1 pred p 2 3 0 8 by def rsub pred p 1 1 8 by case ρ g h 0 pred 8 by def p 1 1 7 by property of pred displaystyle begin aligned operatorname sub 8 1 operatorname rsub circ p_ 2 2 p_ 1 2 8 1 text by def operatorname sub operatorname rsub 1 8 text by def circ p_ 2 2 p_ 1 2 rho p_ 1 1 operatorname pred circ p_ 2 3 s 0 8 text by def operatorname rsub s operatorname pred circ p_ 2 3 0 operatorname rsub 0 8 8 text by case rho g h s operatorname pred operatorname rsub 0 8 text by def circ p_ 2 3 operatorname pred rho p_ 1 1 operatorname pred circ p_ 2 3 0 8 text by def operatorname rsub operatorname pred p_ 1 1 8 text by case rho g h 0 operatorname pred 8 text by def p_ 1 1 7 text by property of operatorname pred end aligned converting predicates to numeric functions edit in some settings it is natural to consider primitive recursive functions that take as inputs tuples that mix numbers with truth values that is t displaystyle t for true and f displaystyle f for false citation needed or that produce truth values as outputs 8 this can be accomplished by identifying the truth values with numbers in any fixed manner for example it is common to identify the truth value t displaystyle t with the number 1 displaystyle 1 and the truth value f displaystyle f with the number 0 displaystyle 0 once this identification has been made the characteristic function of a set a displaystyle a which always returns 1 displaystyle 1 or 0 displaystyle 0 can be viewed as a predicate that tells whether a number is in the set a displaystyle a such an identification of predicates with numeric functions will be assumed for the remainder of this article predicate is zero edit as an example for a primitive recursive predicate the 1 ary function iszero displaystyle operatorname iszero shall be defined such that iszero x 1 displaystyle operatorname iszero x 1 if x 0 displaystyle x 0 and iszero x 0 displaysty...
|
