A function in intension is a finite program or formal construction description. Its associated function in extension is the partial or total input-output map it denotes. A Gödel number records the description rather than identifying all descriptions with the same extension.
A function in extension is a function specified by its domain and the value at each input in that domain. Distinct functions in intension can have this same extension. Properties of the extension of an arbitrary program are semantic properties, to which Rice theorem applies when the property is nontrivial.
A total binary-valued function is diagonally noncomputable if it differs from each defined diagonal value in an effective enumeration of partial computable functions. Nonbinary diagonal outputs are automatically different. No such function is computable: its own program index would contradict the defining condition. Choosing the opposite bit at every defined binary diagonal value proves existence without supplying a computable procedure.
A bounded simulation records whether a specified deterministic program has halted, with a specified output, within a given finite number of steps. This is a primitive recursive predicate of the program code, input and time bound. Peano arithmetic can verify genuine finite computation certificates and prove that two different outputs cannot both be the first halting output.
A set is productive when a partial computable function returns an element of outside any computably enumerable subset supplied by its index. The function must halt for every index of a subset of , including finite subsets. Productive sets are not computably enumerable.
Uniformly diagonalize against the formula expressing membership in to obtain a sentence saying that its own code is not in . If every enumerated sentence is true, this new sentence cannot be enumerated, and hence is true. Its code is a computable new element of arithmetic truth outside .
Kolmogorov complexity measures the length of a shortest effective description of an object. Fixing an optimal description machine gives an invariant quantity up to an additive machine-dependent constant. Plain Kolmogorov complexity is especially convenient for counting descriptions shorter than a binary string.
For a fixed optimal description machine , the plain Kolmogorov complexity of a binary string is the minimum length of a finite program producing it. The admissible programs need not satisfy a prefix restriction. There are at most descriptions shorter than , which is the counting fact behind the existence of incompressible strings.
A binary string is incompressible relative to a fixed optimal description machine when its plain Kolmogorov complexity is at least its length. A counting argument gives at least one such string at each length, and their set is immune.
If an infinite computably enumerable family contained only incompressible strings, select its first enumerated string of length at least . This is a total computable selection rule, and its selected string has a description of length encoding the threshold. For large that is shorter than the selected string. This contradiction proves immunity.
A description machine is a partial computable map from finite binary programs to finite binary outputs. It is optimal if, for every other description machine , there is a constant such that . Encoding an interpreter index in a fixed prefix gives the constant-overhead descriptions used in incompressibility arguments.
A decision problem for which no algorithm terminates with the correct yes-or-no answer on every input. For example, if the diagonal halting set had a decision algorithm, a program could halt on its own code exactly when that algorithm says it does not halt, producing a contradiction. An undecidable decision problem may still admit a partial procedure that terminates on every yes-instance.
A finite-injury priority construction orders countably many requirements so that each has finitely many predecessors. A strategy may discard lower-priority strategies' current witnesses and restraints when it acts. If each requirement acts finitely often after its last such initialization, induction on priority shows that every requirement is injured only finitely often and eventually has a stable strategy. The Friedberg–Muchnik theorem is a central example.
A priority restraint protects finitely many oracle answers by requiring lower-priority enumerations to avoid positions below a numerical bound. Higher-priority action can cancel the priority restraint by initializing its owner. After the last such injury, the protected computation is permanent.
An oracle computation queries only finitely many positions. If the oracle remains unchanged below its use, the same computation has the same output. In a finite-injury priority construction, a successful requirement imposes this bound on lower priorities; the induction that higher priorities stop acting then makes the disagreement permanent.
To prevent a Turing functional from computing the indicator function of an enumerated set , reserve a permanently unique fresh witness . On observing a convergent computation with oracle use , enumerate into if the answer is zero; otherwise keep it out. Restrain subsequent lower-priority enumerations into below . Higher-priority actions may initialize this strategy and retire its witness, but witnesses are never reused. In a finite-injury priority construction, mathematical induction on priority shows that the final computation, if observed, remains correct as a computation from the final oracle and disagrees with at . If no computation is ever observed after the final initialization, the final oracle computation diverges, since any convergent computation uses only finitely many eventually stable oracle bits.
There are computably enumerable sets with and . A finite-injury priority construction alternates requirements preventing oracle programs for from computing and programs for from computing . Each requirement uses a private witness, enumerates it when the opposing computation gives zero, and restrains the oracle segment preserving that disagreement. Verification inducts on priority. Both degrees are noncomputable and strictly below the halting degree, resolving Post problem.
The incomparable-degree formulation is stated in Steffen Lempp's notes, section 1.1.
An injury discards a strategy's current witness or restraint when a higher-priority action changes its assumptions. Finite injury means that each strategy experiences only finitely many such resets. The final uninjured strategy must still be checked to satisfy its requirement; finite injury alone is not the conclusion.
A set is Turing-reducible to when an oracle machine with membership oracle computes the characteristic function of . Unlike a many-one reduction, it may make adaptive queries and reverse or combine oracle answers.
Build an infinite oracle as an increasing union of finite binary strings. With the diagonal halting set as an oracle, decide whether some finite extension makes a specified Turing functional halt with a binary output at a fresh input. In a yes case, preserve that finite computation and commit the opposing set's bit to the opposite value. In a no case, no subsequent infinite extension can yield a characteristic-function value there. Length growth makes the resulting sets computable in the halting oracle.
A Turing functional is a partial computation performed by an oracle machine, viewed as a function of both the oracle and input . Oracle programs admit an effective enumeration. Every convergent computation inspects only a finite part of its oracle, recorded by its oracle use.
The use of a convergent oracle computation is one more than its largest queried position, or zero if there are no queries. Preserving the oracle below this number preserves the computation. This finite dependence supplies the restraints in a finite-injury priority construction.
The Turing degree of a set is its equivalence class under mutual Turing reducibility. Degrees inherit the partial order induced by Turing reducibility. The Friedberg–Muchnik theorem gives incomparable degrees represented by computably enumerable sets.
There are incomparable Turing degrees strictly between the computable degree and the degree of the diagonal halting set. An oracle-assisted finite-extension construction alternately defeats each Turing functional in the two directions. Since the sets are computable in the halting oracle, their degrees are at most ; incomparability makes them nonzero and strictly below . This theorem does not require the constructed sets to be computably enumerable. The Friedberg–Muchnik theorem supplies that stronger conclusion.
Post problem asks whether a computably enumerable set can have a Turing degree strictly between the computable degree and the degree of the halting problem. The Friedberg–Muchnik theorem answers yes by constructing two incomparable computably enumerable degrees.
The Church–Turing thesis asserts that every effectively calculable function is computable by a formal model equivalent to a Turing machine. It identifies an informal notion of effective procedure with a mathematical class rather than stating a theorem within one formal system.
A pairing function is a computable bijection from to whose inverse coordinate functions are also computable. Iterating it gives computable encodings of every fixed finite tuple of nonnegative integers.
A pairing function whose forward map and two inverse coordinate functions are primitive recursive functions. For example, the Cantor pairing function has such inverses: find the diagonal index by bounded minimization over integers at most the encoded value, then recover by subtraction. It enables finite tuples to be decoded within a primitive recursive construction.
The bracket enumerates the positive integers not divisible by . Every positive integer has exactly one decomposition into a power of times such an integer, so this formula is a bijection from to . Subtracting one in the codomain includes zero without requiring a trailing-zero convention for its decimal representation. For the inverse, write with , then .
A register machine has finitely many states and finitely many addressed registers, together with instructions that inspect and modify register contents and change state. A computed partial function is defined by the contents at the halt state.
In a string register machine, appends to register ; branches according to whether its final letter is ; tests emptiness; and branches to when empty, or deletes the final letter and branches to otherwise.
A machine computes the characteristic function of a language when it halts on every input with the one-letter output for inputs in and for inputs outside .
Two string registers can recognize by storing one marker per and removing one per . A machine with only its input register cannot: two different terminal -block lengths eventually reach the same state and remaining prefix, forcing equal outputs for one member and one nonmember.
To recognize words ending in a fixed symbol , test the final input letter, choose one of two erasing loops, and append after the accepting loop or after the rejecting loop. The empty word follows the rejecting branch.
Replace the original halt state by a continuation state that tests whether its one-letter output is or , removes it, appends the other symbol, and enters a new halt state. This computes the complement language without changing termination behavior.
Primitive recursive functions are generated by zero, successor, and projections under composition and primitive recursion.
For a decidable coding of finite construction trees, the codes of arity- primitive recursive functions in intension are decidable. Check initial-function tags, then verify the child arities at each composition and recursion node. This is a terminating finite syntax check, distinct from asking whether an arbitrary program's extension happens to be primitive recursive.
Enumerate all valid unary primitive recursive functions in intension by their decidable codes , and interpret each extension . The function is a total computable function, since each finite construction terminates. If it were primitive recursive, some would equal , giving . Repeated extensions in the syntax enumeration do not affect this argument.
A valid finite construction expression from the initial functions of recursion theory by function composition in recursion theory and primitive recursion. Its extension is a primitive recursive function. The construction grammar supplies both a decidable syntax and a total computable interpreter, but no uniformly primitive recursive interpreter for all valid codes.
For a fixed effective machine coding, the predicate that program on input halts within steps is primitive recursive. Code finite configurations, iterate a total single-step function by primitive recursion, and test for the halt state. This supplies a bounded simulation even though the unrestricted halting problem is undecidable.
Search over the finite interval for the least witness to a primitive recursive predicate, with an explicitly chosen default if there is none. The result is a primitive recursive function, by scanning this finite interval using primitive recursion. This differs from unbounded minimization, which may fail to terminate.
The predecessor function on the nonnegative integers is and . This is a primitive recursive function by primitive recursion from the zero and projection functions.
The initial functions are the zero function, the successor function, and all coordinate projections.
The successor function is
The functions generated from the initial functions using composition alone are exactlyfor a constant . Structural induction proves necessity, and iterating the successor function on zero or a projection proves sufficiency.
To prove a property of every primitive recursive function, prove it for the zero, successor, and projection functions, then prove that it is preserved by composition and by primitive recursion. This is structural induction on the finite construction of the function.
The initial functions are total, composition preserves totality, and ordinary induction on the recursion argument shows that primitive recursion applied to total functions is total. Structural induction therefore proves that every primitive recursive function is total.
The graph of every primitive recursive has a formulain the language of ordered rings, where every quantifier inside is bounded. Composition uses existentially quantified intermediate values, while primitive recursion uses a boundedly checked code for the finite sequence of intermediate values.
The Gödel beta function codes finite sequences by remainders:Choosing sufficiently large and divisible by the relevant small integers makes the moduli pairwise coprime, so the Chinese remainder theorem codes any prescribed finite sequence.
The graph of the factorial function has a fixed-length first-order formula in the language of ordered rings interpreted on the natural numbers. A remainder code records , , and for every . Uniqueness of remainders proves ; sufficiently large pairwise-coprime moduli and the Chinese remainder theorem supply a code for every input. Formula length is independent of the input variable's value, although substituting a numeral adds its encoding length.
In a primitive recursion, an existential representation of the step function may need a different witness tuple at every time. Code each coordinate of the finite witness array by a separate beta-function code pair. All row witnesses then have bounded remainder quantifiers under the bounded time quantifier, while the finitely many code pairs remain in the outer unrestricted existential block.
A set is computably enumerable when a program halts precisely on its members. Equivalently, it is the domain of a partial computable function or some algorithm lists its elements.
A computably enumerable set is simple when its complement of a set is an immune set: the complement is infinite and contains no infinite computably enumerable subset. Equivalently, it is coinfinite and meets every infinite computably enumerable set. A simple set is not decidable.
Enumerate all computably enumerable sets as . For each , once a witness appears in , enumerate one such witness into and never act for again. Every infinite supplies a witness. Only requirements can put numbers into , so at least numbers in that interval stay outside . Thus is a simple set. The proof uses a numerical bound rather than an infinitude test.
An immune set is infinite but contains no infinite computably enumerable subset. Thus its infinitude cannot be witnessed by any effective infinite listing that stays entirely inside the set. Finite strings can be treated as natural-number codes for this definition.
Every nonempty computably enumerable set is the range of a primitive recursive function . Choose , decode using a primitive recursive pairing function, and output if the recognizing machine halts within steps, or otherwise. The bounded halting predicate makes this function primitive recursive, and every member of occurs for a sufficiently large bound. The empty set is excluded because such a function is total.
A set is computable when an algorithm decides membership for every input and always halts. Equivalently, both the set and its complement are computably enumerable.
For a nonempty set of words, the following are equivalent: is computably enumerable, is the domain of a partial computable function, is the range of a partial computable function, and is the range of a total computable function. The nonempty hypothesis is needed only for the last formulation, since the range of a total function cannot be empty.
Kleene recursion gives programs access to their own effective descriptions: every computable transformation of program indices has a semantic fixed point.
Two sets have the same many-one degree when each many-one reduces to the other.
A staged-enumeration reduction controls an output language by enumerating more elements at each simulation stage and changing behavior when a source computation halts.
An index set is a set of program codes whose membership depends only on the partial function or enumerable language computed, rather than the code's syntax.
An extensional program property gives identical answers to all codes computing the same object.
Every nontrivial extensional property of partial computable functions or computably enumerable languages is undecidable.
For a nonempty set of words, the propertyis a nontrivial extensional property of unary partial computable functions: the nowhere-defined function fails it, while any total constant function with value in satisfies it. The Rice theorem therefore makes its index set undecidable.
The cofinite index set contains codes whose enumerable language has finite complement.
The padding lemma produces infinitely many syntactically distinct program indices for the same computed function or language.
Dovetailing interleaves finite stages of multiple computations so that every computation that halts is eventually observed.
The S-m-n theorem says that fixed inputs can be compiled into program codes by a total computable transformation. For every , there is a total computable such thatwhenever either side is defined.
A partial function is computable when a program returns its value on every input in its domain and runs forever on inputs outside its domain.
For every partial computable function , there are total primitive recursive functions such thatHere is zero exactly on codes of valid halting computation histories for the chosen program and input, and extracts the final output. Coding finite configurations and finite histories makes checking every local step a bounded primitive recursive operation. If a computation halts, some history code passes and every passing code has the same output; if it does not halt, none passes. This is the usual normal-form version with the program index fixed; a universal predicate can also retain that index as an input.
For a partial function , unbounded minimization definesas the least at which is zero, provided the preceding required computations are defined. If no such is found, is undefined. Closing the primitive recursive functions under this operation gives the partial recursive functions.
For a theory of arithmetic and a program index , the function is provably total in when proves its canonical totality sentenceIf is recursively axiomatized, the indices of its provably total functions form a computably enumerable set.
For a program code , input , and time bound , the truncated computation simulates program on for at most steps and reports either its output or that no halt occurred within the bound. This is a total computable function of .
The arithmetical hierarchy classifies sets by alternating blocks of number quantifiers over computable predicates.
A bounded quantifier has the form or , where the term does not contain . It ranges over a finite initial segment in the standard natural numbers.
An arithmetic bounded formula uses only quantifiers bounded by arithmetic terms, such as and , with the bound not containing the quantified variable. Existential bounded representation of a primitive recursive function places all unrestricted existential variables in a single outer block.
A set is in exactly when it is the domain of a partial computable function. Equivalently, there is a computable predicate such that
A set is in when membership can be written with one universal block followed by one existential block over a computable predicate. Equivalently, in the word-function formulation, there is a partial computable such that
For an effective enumeration of computably enumerable languages , the totality problem isIt is -complete: a condition maps effectively to a program whose domain is .
If all indices of total computable functions could be enumerated as , thenwould be total and computable. Some would index , giving . Thus the totality problem is not computably enumerable.
Lambda calculus forms terms from variables, abstraction, and application, and computes by substitution.
A lambda term is a variable, an abstraction , or an application , formed recursively from lambda terms and .
A lambda abstraction binds the variable in the lambda term . In the simply typed lambda calculus, if under , the abstraction has type ; this is the implication introduction rule under the Curry-Howard correspondence.
The untyped lambda calculus forms terms from variables, abstraction, and application without assigning types.
A lambda term has head normal form when it beta-reduces to a term with a variable at the head. The argument terms need not be in beta-normal form. A term with no head normal form cannot be beta-equivalent to a Church numeral.
Articles were limited to the first 100 out of 131 total.
Articles by others on the same topic
Computability theory, also known as recursive function theory, is a branch of mathematical logic and computer science that deals with the question of what it means for a function to be computable. It explores the limits of what can be algorithmically solved and examines the characteristics of functions, problems, or decision-making processes that can be effectively computed by mechanical means, such as algorithms or theoretical models like Turing machines.