Hubbry Logo
Recursive definitionRecursive definitionMain
Open search
Recursive definition
Community hub
Recursive definition
logo
8 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Recursive definition
Recursive definition
Recursive definition
View on Wikipedia
from Wikipedia
Four stages in the construction of a Koch snowflake. As with many other fractals, the stages are obtained via a recursive definition.

In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set (Aczel 1977:740ff). Some examples of recursively definable objects include factorials, natural numbers, Fibonacci numbers, and the Cantor ternary set.

A recursive definition of a function 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 factorial function n! is defined by the rules

This definition is valid for each natural number n, because the recursion eventually reaches the base case of 0. The definition may also be thought of as giving a procedure for computing the value of the function n!, starting from n = 0 and proceeding onwards with n = 1, 2, 3 etc.

The recursion theorem states that such a definition indeed defines a function that is unique. The proof uses mathematical induction.[1]

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 ⁠⁠ of natural numbers is:

  1. 0 is in ⁠⁠
  2. If an element n is in ⁠⁠ then n + 1 is in ⁠⁠
  3. ⁠⁠ is the smallest set satisfying (1) and (2).

There are many sets that satisfy (1) and (2) – for example, the set {0, 1, 1.649, 2, 2.649, 3, 3.649, …} satisfies the definition. However, condition (3) specifies the set of natural numbers by removing the sets with extraneous members.

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 of the natural number 0 (or 1), and the property holds of n + 1 whenever it holds of n, then the property holds of all natural numbers (Aczel 1977:742).

Form of recursive definitions

[edit]

Most recursive definitions have two foundations: a base case (basis) and an inductive clause.

The difference between a circular definition and a recursive definition is that a recursive definition must always have base cases, cases that satisfy the definition without 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., closer to those base cases that terminate the recursion) — a rule also known as "recur only with a simpler case".[2]

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 infinite regress.

That recursive definitions are valid – meaning that a recursive definition identifies a unique function – is a theorem of set theory known as the recursion theorem, the proof of which is non-trivial.[3] Where the domain of the function is the natural numbers, sufficient conditions for the definition to be valid are that the value of f(0) (i.e., base case) is given, and that for n > 0, an algorithm is given for determining f(n) in terms of n, (i.e., inductive clause).

More generally, recursive definitions of functions can be made whenever the domain is a well-ordered set, using the principle of transfinite recursion. 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 James Munkres' Topology. However, a specific case (domain is restricted to the positive integers instead of any well-ordered set) of the general recursive definition will be given below.[4]

Principle of recursive definition

[edit]

Let A be a set and let a0 be an element of A. If ρ is a function which assigns to each function f mapping a nonempty section of the positive integers into A, an element of A, then there exists a unique function such that

Examples of recursive definitions

[edit]

Elementary functions

[edit]

Addition is defined recursively based on counting as

Multiplication is defined recursively as

Exponentiation is defined recursively as

Binomial coefficients can be defined recursively as

Prime numbers

[edit]

The set of prime numbers can be defined as the unique set of positive integers satisfying

  • 2 is a prime number,
  • any other positive integer is a prime number if and only if it is not divisible by any prime number smaller than itself.

The primality of the integer 2 is the base case; checking the primality of any larger integer X by this definition requires knowing the primality of every integer between 2 and X, which is well defined by this definition. That last point can be proved by induction on X, 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.

Non-negative even numbers

[edit]

The even numbers can be defined as consisting of

  • 0 is in the set E of non-negative evens (basis clause),
  • For any element x in the set E, x + 2 is in E (inductive clause),
  • Nothing is in E unless it is obtained from the basis and inductive clauses (extremal clause).

Well formed formula

[edit]

The notion of a well-formed formula (wff) in propositional logic is defined recursively as the smallest set satisfying the three rules:

  1. p is a wff if p is a propositional variable.
  2. ¬ p is a wff if p is a wff.
  3. (p • q) is a wff if p and q are wffs and • is one of the logical connectives ∨, ∧, →, or ↔.

The definition can be used to determine whether any particular string of symbols is a wff:

  • (p ∧ q) is a wff, because the propositional variables p and q are wffs and ∧ is a logical connective.
  • ¬ (p ∧ q) is a wff, because (p ∧ q) is a wff.
  • (¬ p ∧ ¬ q) is a wff, because ¬ p and ¬ q are wffs and ∧ is a logical connective.

Recursive definitions as logic programs

[edit]
See also: Definition § Logic programs

Logic programs can be understood as sets of recursive definitions.[5][6] For example, the recursive definition of even number can be written as the logic program: 

even(0).
even(s(s(X))) :- even(X).

Here :- represents if, and s(X) represents the successor of X, namely X+1, as in Peano arithmetic.

The logic programming language Prolog uses backward reasoning to solve goals and answer queries. For example, given the query ?- even(s(s(0))) it produces the answer true. Given the query ?- even(s(0)) it produces the answer false.

The program can be used not only to check whether a query is true, but also to generate answers that are true. For example: 

?- even(X).
X = 0
X = s(s(0))
X = s(s(s(s(0))))
X = s(s(s(s(s(s(0))))))
.....

Logic programs significantly extend recursive definitions by including the use of negative conditions, implemented by negation as failure, as in the definition: 

even(0).
even(s(X)) :- not(even(X)).

See also

[edit]

Notes

[edit]

References

[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Recursive definition

View on Grokipedia
from Grokipedia
A recursive definition, also termed an inductive definition, is a foundational method in and for specifying the elements of a set, the values of a function, or terms in a by establishing initial conditions and rules that generate subsequent elements from prior ones. This approach ensures that complex structures are built systematically from simpler components, avoiding circularity through a well-ordered progression. The structure of a recursive definition typically includes a base case, which defines the simplest or initial elements—such as f(0)=1f(0) = 1 for the function or the ϵ\epsilon for the set of all strings over an —and one or more recursive steps, which describe how to derive new elements, like f(n+1)=(n+1)⋅f(n)f(n+1) = (n+1) \cdot f(n) or appending a to an existing string. An extremal clause often accompanies these to stipulate that only elements constructed in a finite number of steps belong to the defined object, preventing . Common examples illustrate its versatility: the natural numbers can be defined with base case 0∈N0 \in \mathbb{N} and recursive step if n∈Nn \in \mathbb{N}, then n+1∈Nn+1 \in \mathbb{N}; the uses F(0)=0F(0) = 0, F(1)=1F(1) = 1, and F(n)=F(n−1)+F(n−2)F(n) = F(n-1) + F(n-2) for n≥2n \geq 2; and sets like palindromes over an include the and single letters as base cases, with recursive construction yxyyxy where xx and yy are prior palindromes. Recursive definitions underpin for proofs, enable the formalization of data types in , and form the basis for recursive functions in , where they distinguish primitive recursive functions—computable via bounded loops—from more general recursively enumerable ones. They also apply to geometric objects like fractals and binary trees, where self-similar patterns emerge from repeated application of rules.

Fundamentals

Definition

A recursive definition provides a way to specify mathematical objects, such as sets, sequences, or functions, by referring to the object itself in a structured manner that begins with simple initial elements and builds complexity through repeated application of rules. This approach allows for the precise characterization of infinite structures without enumerating every element explicitly, relying instead on a foundational simplicity that expands iteratively. Formally, a recursive definition—also known as an inductive definition—comprises a base that identifies the initial or simplest objects belonging to the defined collection, and one or more inductive s that describe how to generate additional objects from those already established. The base ensures a starting point, while the inductive s provide the mechanism for extension, guaranteeing that every object in the collection can be derived through finite applications of these rules. This structure is fundamental in areas like and logic, where it enables the definition of complex entities like the natural numbers or well-formed expressions. Recursive definitions differ from circular definitions, which merely restate the term being defined without providing new information and thus lead to unresolved , such as equating a solely to itself. In contrast, recursive definitions are acyclic and well-founded: they progress strictly from simpler cases to more complex ones, anchored by the base clause to prevent endless looping and ensure every instance terminates in a finite derivation. This foundational progression aligns with principles like , which justifies the completeness of such definitions. In general, for a function ff defined on a well-ordered domain, the recursive form specifies f(x)=g(x)f(x) = g(x) when xx belongs to a base set BB, and otherwise f(x)=h(f(y1),…,f(yk))f(x) = h(f(y_1), \dots, f(y_k)) for some hh and arguments y1,…,yky_1, \dots, y_k that are strictly simpler than xx under the given ordering. This ensures that or always reduces to the base case through a finite chain of dependencies, avoiding ambiguity or non-termination.

Principle of Recursive Definition

The principle of recursive definition ensures that, in an appropriate mathematical domain, a specification consisting of base clauses and inductive rules uniquely determines an object satisfying those clauses. In set theory, this is formalized by the recursion theorem, which states that for a well-founded and set-like relation RR on a class CC, and a class function F:C×V→VF: C \times V \to V, there exists a unique class function G:C→VG: C \to V such that for all x∈Cx \in C, G(x)=F(x,G↾pred⁡R(x))G(x) = F(x, G \upharpoonright \operatorname{pred}_R(x)), where pred⁡R(x)\operatorname{pred}_R(x) denotes the set of RR-predecessors of xx. This theorem applies particularly when the base case specifies values for minimal elements under RR, with inductive steps building upon prior values. The applicability of this principle requires the domain to be equipped with a well-founded partial order, ensuring no infinite descending chains exist and thereby preventing circular or ill-defined dependencies in the . A relation RR is well-founded if every nonempty subclass of CC has an RR-minimal element, and it is set-like if the predecessor set pred⁡R(x)\operatorname{pred}_R(x) is a set for each x∈Cx \in C. These conditions, satisfied by structures like the ordinals under membership or arbitrary well-ordered sets, guarantee that the recursive process terminates and yields a coherent . The uniqueness of GG follows from transfinite induction: supposing two functions G1G_1 and G2G_2 both satisfy the recursion equation, their agreement on predecessors implies equality at any minimal point of difference, leading to a contradiction otherwise. For existence, one constructs GG via transfinite iteration: define approximations on the RR-closed subsets of CC by assigning values to minimal elements using FF and previously defined portions, proceeding up to the ordinal rank of the relation. Alternatively, in domains forming complete partial orders (such as power sets under inclusion), the recursive definition corresponds to the least fixed point of the monotonic operator induced by FF, obtained as the supremum of the iterated applications starting from the bottom element.

Base Case and Inductive Step

In a recursive definition, the base case establishes the foundational values or memberships for the simplest or initial elements of the domain, preventing infinite regression and providing a starting point for the definition. For instance, in defining a function ff over non-negative integers, the base case might specify f(0)=1f(0) = 1, assigning a concrete value to the minimal input without relying on prior computations. This component ensures that the definition is grounded and applicable to the most elementary instances, such as the in structural definitions or the zeroth term in sequences. The inductive step, also known as the recursive step, provides rules for extending the to more complex elements by expressing them in terms of previously defined simpler ones. This step outlines how to construct or compute values for larger inputs using outputs from smaller ones, such as f(n)=n⋅f(n−1)f(n) = n \cdot f(n-1) for n>0n > 0, where the value at nn depends directly on the value at n−1n-1. It enables the progressive buildup of the entire structure, ensuring that every element in the domain can be reached through finite applications of the rules. The base case and inductive step are interdependent, with the base anchoring the process to avoid circularity and the inductive step driving expansion toward greater complexity. Without a solid base, the inductive step cannot initiate , leading to stagnation; conversely, an inductive step without connection to the base fails to propagate values effectively. This mirrors the principle of recursive definition, where the base halts descent and the step ascends systematically. Common pitfalls in formulating these components include incomplete base cases, which can result in undefined values for certain elements and render the overall inapplicable or lead to non-termination in computations. For example, omitting a base case for all initial conditions might cause attempts to evaluate the function to loop indefinitely without resolution. Similarly, overbroad inductive steps can introduce by allowing multiple interpretations or inconsistent derivations for the same element, undermining the definition's uniqueness and clarity.

Mathematical Examples

Arithmetic Operations

In the axiomatic foundation of natural numbers, as established by the , basic arithmetic operations are defined recursively using the SS, which maps each nn to its immediate successor S(n)S(n). This approach ensures that the operations are constructed from primitive notions without circularity, relying solely on the axioms governing the natural numbers, zero, and induction. Addition is defined recursively as follows: for any natural numbers mm and nn, m+0=m,m + 0 = m, m+S(n)=S(m+n).m + S(n) = S(m + n). This definition, introduced by , specifies the base case where adding zero leaves the first argument unchanged and the inductive step where adding the successor of nn is equivalent to taking the successor of the sum with nn. builds upon in a similar recursive manner: for any natural numbers mm and nn, m⋅0=0,m \cdot 0 = 0, m⋅S(n)=m+(m⋅n).m \cdot S(n) = m + (m \cdot n). Here, the base case sets the product with zero to zero, while the inductive step treats multiplication by the successor as adding mm to the product with nn, effectively defining multiplication as repeated addition. Dedekind formalized this in his foundational work on the nature of numbers. Exponentiation extends this pattern by iterating multiplication: for any natural numbers mm and nn, m0=1,m^0 = 1, mS(n)=m⋅(mn).m^{S(n)} = m \cdot (m^n). The base case establishes that any number raised to the power of zero is one, and the inductive step computes the power with the successor as the product of mm and the power with nn, representing exponentiation as repeated multiplication. This recursive structure, also due to Dedekind, underpins the hierarchy of arithmetic operations within Peano arithmetic. These definitions exemplify the principle of recursive definition by providing a base case and an inductive rule that references the operation on smaller inputs, allowing all values to be derived systematically from the without presupposing the operations themselves. incorporated and axiomatized these recursive constructions in his treatise, solidifying their role in formal arithmetic.

Sequences and Sets

Recursive definitions are commonly used to define sequences in mathematics, where each term depends on previous terms. One classic example is the factorial sequence, which counts the number of permutations of nn distinct objects. The factorial of a non-negative integer nn, denoted n!n!, is defined recursively as follows: the base case is 0!=10! = 1, and for n>0n > 0, the inductive step is n!=n×(n−1)!n! = n \times (n-1)!. This definition generates the sequence 1, 1, 2, 6, 24, 120, and so on, building each value from the prior one through multiplication. Another prominent sequence defined recursively is the , which appears in various natural phenomena such as plant branching patterns. It is specified by the base cases F(0)=0F(0) = 0 and F(1)=1F(1) = 1, with the recursive rule F(n)=F(n−1)+F(n−2)F(n) = F(n-1) + F(n-2) for n>1n > 1. This produces the terms 0, 1, 1, 2, 3, 5, 8, 13, 21, and continues indefinitely, where each term is the sum of the two preceding ones. The recursive structure highlights the sequence's self-similar growth properties. Recursive definitions also apply to sets, generating their members through base elements and rules that incorporate existing members. For the set of even non-negative integers, denoted EE, the base case is 0∈E0 \in E, and the inductive step states that if n∈En \in E, then n+2∈En+2 \in E. This construction ensures E={0,2,4,6,… }E = \{0, 2, 4, 6, \dots \}, capturing all non-negative even numbers without including odds, as the recursive addition of 2 preserves parity from the base. The set of prime numbers, PP, can similarly be defined inductively as the smallest set of positive s greater than 1 satisfying: 2 is prime (base case), and for any n>2n > 2, n∈Pn \in P if nn is not divisible by any prime p∈Pp \in P with p<np < n. This recursive characterization builds P={2,3,5,7,11,… }P = \{2, 3, 5, 7, 11, \dots \} by checking divisibility against previously identified primes, ensuring each new member is the smallest not factored by smaller ones in the set. Such definitions emphasize the generative nature of recursion in set theory, distinguishing primes from composites through successive verification.

Structural Definitions

Recursive definitions excel at modeling hierarchical or self-similar structures in mathematics, where complex objects are built by nesting simpler instances of the same type, enabling precise descriptions of entities like trees and ordinals that defy linear enumeration. This approach contrasts with sequential definitions by emphasizing composition over iteration, capturing the intrinsic nesting that defines such structures. A prominent example is the binary tree, a fundamental hierarchical structure used to represent ordered data with branching. Formally, a binary tree is defined recursively as follows:
  • It is either empty (null), or
  • It consists of a root node containing a data element and two pointers: one to a left binary subtree and one to a right binary subtree, where each subtree is itself a binary tree.
This definition ensures that every non-empty binary tree decomposes into a root and two potentially smaller binary trees, embodying self-similarity at every level. Another illustrative case is the Ackermann function, which demonstrates deeply nested recursion to define a total computable function that grows faster than any primitive recursive function, highlighting the power of structural recursion for hyper-exponential growth. The function A(m,n)A(m, n) is defined with base cases and an inductive step: A(0,n)=n+1,A(m,0)=A(m−1,1)for m>0,A(m,n)=A(m−1,A(m,n−1))for m>0, n>0.\begin{align*} A(0, n) &= n + 1, \\ A(m, 0) &= A(m-1, 1) \quad \text{for } m > 0, \\ A(m, n) &= A(m-1, A(m, n-1)) \quad \text{for } m > 0, \, n > 0. \end{align*} This nested application in the inductive clause creates a hierarchical tree, where each evaluation branches into further recursive calls, originally introduced by in 1928 to exemplify non-primitive recursive functions. In , the natural numbers are constructed as von Neumann ordinals via a recursive that builds the number system from the , forming a hierarchical chain of sets where each successor embeds the previous structure. Specifically:
  • 0=∅0 = \varnothing,
  • For any ordinal α\alpha, the successor is α+1=α∪{α}\alpha + 1 = \alpha \cup \{\alpha\}.
This yields 1={∅}1 = \{\varnothing\}, 2={∅,{∅}}2 = \{\varnothing, \{\varnothing\}\}, and so on, with the finite ordinals corresponding to the numbers N\mathbb{N}; the recursion extends transfinitely to define all ordinals, ensuring well-ordered sets without cycles.

Logical Applications

Well-Formed Formulas

In propositional logic, well-formed formulas (wffs) are syntactically valid expressions defined recursively to capture the structure of the language precisely. The base case consists of atomic formulas, which are the propositional variables such as [p](/page/P′′)[p](/page/P′′), [q](/page/Q)[q](/page/Q), or [r](/page/R)[r](/page/R). These atomic elements form the foundation upon which more complex formulas are built through recursive application of logical connectives. The inductive step specifies that if ϕ\phi and ψ\psi are well-formed formulas, then so are the negated formula ¬ϕ\neg \phi, the conjunction (ϕ∧ψ)(\phi \land \psi), the disjunction (ϕ∨ψ)(\phi \lor \psi), and the implication (ϕ→ψ)(\phi \to \psi). No other strings qualify as wffs except those generated by finite applications of these rules. The inclusion of parentheses in compound expressions ensures balanced nesting and resolves ambiguities in operator precedence, allowing recursive construction of arbitrarily complex yet unambiguous syntactic objects. This recursive approach extends naturally to predicate logic, where the language incorporates quantifiers and relations over objects. Atomic formulas here are formed by applying an n-ary predicate symbol PP to exactly n terms t1,…,tnt_1, \dots, t_n, respecting the predicate's arity to maintain syntactic validity; for example, if PP is binary, P(t1,t2)P(t_1, t_2) is well-formed. The connectives operate recursively on these and other wffs as in the propositional case. Additionally, if AA is a and xx is a variable, then the universal quantification ∀xA\forall x A and the ∃xA\exists x A are well-formed formulas. Parentheses continue to enforce proper recursive nesting around quantified and connected subformulas, ensuring that the entire syntax of predicate logic is defined without ambiguity and supports the formal expression of properties and relations.

Predicate Logic Constructs

In , terms are fundamental syntactic objects that denote elements of the , defined recursively to ensure a structured and unambiguous formation. The base cases consist of all variables and constant symbols in the language. For an n-ary function symbol ff and terms t1,…,tnt_1, \dots, t_n, the expression f(t1,…,tn)f(t_1, \dots, t_n) qualifies as a term, allowing complex terms to be built inductively from simpler ones. Nothing beyond these rules counts as a term, preventing ill-formed expressions and guaranteeing that every term can be decomposed into its atomic components via repeated application of the inverse operations. Atomic formulas extend this recursive structure to express basic assertions about terms, forming the atoms from which compound formulas are assembled. Specifically, for an n-ary predicate symbol PP and terms t1,…,tnt_1, \dots, t_n, the expression P(t1,…,tn)P(t_1, \dots, t_n) is an atomic formula, capturing relational among domain elements. Equality provides another primitive: if t1t_1 and t2t_2 are terms, then t1=t2t_1 = t_2 is an atomic formula. This recursive reliance on terms ensures atomic formulas precisely delineate the simplest propositions, such as membership or ordering relations in mathematical structures. Axiomatic systems in employ recursive definitions to generate from via iterative application of inference rules, yielding the deductive closure of the axiom set. exemplifies this: given theorems ψ→ϕ\psi \to \phi and ψ\psi, the rule infers ϕ\phi as a new theorem, with the process repeating indefinitely on derived results. Other rules, like , further expand this closure, ensuring all logically entailed statements are systematically producible. This recursive mechanism underpins the completeness of axiomatic proofs, as articulated in Hilbert-style systems. The Herbrand universe embodies recursive term generation in a parameter-free context, comprising all ground terms (variable-free) derivable from the language's constants and function symbols. Its construction begins with the constant symbols—if none exist, an arbitrary constant is adjoined—and closes under : for terms t1,…,tnt_1, \dots, t_n already in the universe and an n-ary function ff, f(t1,…,tn)f(t_1, \dots, t_n) is added. This exhaustively enumerates the "individuals" available for interpretation in Herbrand models, central to reducing in .

Computational Uses

Recursive Algorithms

In , a recursive function is defined as one that solves a problem by calling itself with a smaller or simpler instance of the same problem, typically until a base case is reached where no further occurs. This approach mirrors the inductive step in mathematical , allowing complex computations to be broken down into repeated applications of simpler operations. For instance, the algorithm partitions an around a and recursively sorts the subarrays on either side, with the base case being an empty or single-element that requires no sorting. Tail recursion occurs when the recursive call is the final operation in the function, with no subsequent computations performed on the returned value, enabling compilers or interpreters to optimize the recursion into an iterative loop and avoid from deep call chains. This optimization is particularly valuable in languages like Scheme, where tail calls are guaranteed to be efficient, transforming what would otherwise be linear space usage into constant space. Mutual recursion involves two or more functions that invoke each other in a cyclic manner to solve interdependent subproblems, such as determining whether a number is even or odd by alternating calls between helper functions. A classic example is the pair of functions isEven(n) and isOdd(n), where isEven(0) returns true as the base case, isEven(n) otherwise calls isOdd(n-1), and isOdd(n) symmetrically calls isEven(n-1) with isOdd(0) false; this mutual structure elegantly captures parity without direct . The time and space complexity of recursive algorithms is analyzed using recursion trees or master theorems, where time complexity reflects the total work across all recursive levels and space complexity accounts for the maximum depth of the call stack. For linear recursion, such as computing a factorial by successive multiplication, the time complexity is O(n) due to n recursive calls each performing constant work, while space complexity is also O(n) from the stack frames; in contrast, balanced divide-and-conquer recursion like quicksort averages O(n log n) time but can reach O(n^2) in the worst case. These analyses highlight how recursion depth influences resource usage, often favoring tail-recursive variants for efficiency in practice.

Logic Programs

In , recursive definitions are foundational to expressing computations declaratively through Horn clauses, which are logical formulas consisting of a single positive literal (the head) and a conjunction of literals (the body), enabling the definition of predicates via recursive rules. This approach, pioneered in the development of languages like , treats programs as sets of such clauses where arises naturally in defining relations or functions, contrasting with by focusing on what holds true rather than how to compute it step-by-step. For instance, the parity of natural numbers can be defined recursively using clauses like even(0). as a base case and even(s(X)) :- odd(X). along with odd(s(X)) :- even(X)., where s denotes the , allowing the system to infer evenness or oddness through unfolding the recursion. Definite clause grammars (DCGs) extend this recursive framework specifically for language parsing and analysis, representing context-free grammars as Horn clauses augmented with arguments to track state, such as positions in input strings. In a DCG, non-terminals are defined recursively; for example, a simple for arithmetic expressions might include rules like expr(Xs, Ys, X + Z) --> expr(Xs, Ws, X), ['+'], term(Ws, Ys, Z). and base cases for terms, enabling the parser to build parse trees by recursively descending into substructures while consuming the input. This recursive structure directly mirrors the inductive definitions of formal languages, facilitating both recognition and generation tasks in a unified logical setting. The evaluation of these recursive definitions in logic programs relies on SLD (Selective Linear Definite clause) , an mechanism that systematically derives facts from clauses by selecting literals for resolution in a linear fashion, ensuring completeness for programs under fair computation strategies. SLD resolution unfolds recursive predicates by repeatedly applying rules until base cases are reached or failure occurs, with to explore alternatives, thus computing the least Herbrand model of the program. A classic example is the relation, defined by base clause ancestor(X, Y) :- parent(X, Y). and recursive clause ancestor(X, Z) :- parent(X, Y), [ancestor](/page/Ancestor)(Y, Z)., where querying ancestor(A, B) triggers SLD to traverse the recursively until terminating at direct . This mechanism guarantees that recursive definitions are both sound and complete in their declarative interpretation, provided the recursion is well-founded to avoid infinite loops.

Proof Techniques

Mathematical Induction

Mathematical induction is a fundamental proof technique that leverages the recursive structure of the natural numbers to establish properties for all elements in an infinite set. The principle states that if a property P(n)P(n) holds for the base case n=0n = 0 (or n=1n = 1, depending on the formulation), and if the assumption that P(k)P(k) holds implies P(k+1)P(k+1) for any natural number kk, then P(n)P(n) holds for all natural numbers nn. This method is particularly suited to recursive definitions, as the natural numbers themselves are recursively defined via a base element (0) and a successor function. For recursively defined sets beyond the naturals, such as trees or lists, structural induction extends this principle. In structural induction, one proves a property ϕ(x)\phi(x) for all elements xx in the set by first verifying ϕ\phi on the base elements, then showing that if ϕ\phi holds for the components used in a constructor rule, it holds for the resulting structure. This mirrors the recursive construction of the set, ensuring the property propagates through all generated elements. A classic application involves proving properties of recursively defined functions, such as the sum of the first nn natural numbers. Define S(0)=0S(0) = 0 and S(n)=S(n−1)+nS(n) = S(n-1) + n for n≥1n \geq 1; to show S(n)=n(n+1)2S(n) = \frac{n(n+1)}{2}, verify the base case S(0)=0=0⋅12S(0) = 0 = \frac{0 \cdot 1}{2}, then assume it holds for kk and confirm for k+1k+1: S(k+1)=S(k)+(k+1)=k(k+1)2+(k+1)=(k+1)(k+2)2.S(k+1) = S(k) + (k+1) = \frac{k(k+1)}{2} + (k+1) = \frac{(k+1)(k+2)}{2}. By , the formula holds for all n≥0n \geq 0. When recursive definitions involve multiple branches or dependencies on several prior cases, strong induction provides a more flexible approach. Strong induction assumes the property holds for all values up to kk to prove it for k+1k+1, making it ideal for functions like the Fibonacci sequence where each term depends on the two preceding ones. This variant, sometimes called complete induction, is equivalent in power to standard induction but aligns naturally with complex recursive structures.

Well-Foundedness and Termination

A well-founded order on a set is a strict partial order with no infinite descending chains, meaning that every non-empty has a minimal element. For example, the natural numbers under the usual less-than relation form a well-founded order, as any descending must terminate at zero. In recursive definitions, termination is guaranteed when the recursion proceeds along a well-founded order, such that each recursive call reduces the argument according to a measure that respects this order. For instance, in tree recursion where the size of subtrees decreases, the well-foundedness of the relation ensures the process halts after finitely many steps. This condition prevents infinite computation by ensuring that the recursion depth is bounded by the order's structure. Noetherian induction extends this to partial orders, allowing proofs of properties over well-founded sets by assuming the property holds for all smaller elements and verifying it for minimal ones. It generalizes standard to arbitrary well-founded relations, such as those in algebraic structures. A common pitfall in recursive definitions arises when the base case is omitted or the measure does not decrease, leading to non-termination; for example, defining f(n)=f(n−1)f(n) = f(n-1) for positive integers nn without a base case results in an .

Historical Context

Origins in Set Theory

In his 1888 treatise Was sind und was sollen die Zahlen?, Richard Dedekind provided a foundational recursive construction of the natural numbers within set theory by defining them as a "simply infinite system." He introduced the concept of a chain, which is the minimal closure of a base element under an injective mapping φ that excludes the base from its image, thereby generating the numbers recursively: starting from 1, each subsequent element is the successor via φ, ensuring an infinite sequence isomorphic to the naturals. This approach abstracted the natural numbers from any specific realization, emphasizing structural properties and enabling rigorous proofs of arithmetic via induction on these chains. Dedekind's method resolved foundational issues in arithmetic by grounding it in set-theoretic recursion, proving that every infinite set contains such a subsystem. Giuseppe Peano's 1889 work Arithmetices principia, nova methodo exposita formalized the natural numbers through axioms featuring a successor function S, which implicitly supports recursive definitions by stipulating that every natural number except zero is the successor of a unique predecessor. The axioms include: zero is a natural number; S is a function from naturals to naturals; S is injective; zero is not in the image of S; and the induction axiom ensures closure under properties holding for zero and successors. This framework allows arithmetic operations like addition and multiplication to be defined recursively—for instance, addition as x + 0 = x and x + S(y) = S(x + y)—providing a deductive basis for number theory without circularity. Peano's successor-based recursion influenced later axiomatizations, bridging arithmetic and logic. Gottlob Frege's 1879 Begriffsschrift introduced an early recursive syntax for logical expressions, modeling logic on arithmetic through a tree-like notation that builds complex formulas from atomic contents via recursive application of operators. The system distinguishes judgeable contents (propositions) from incomplete expressions (functions), allowing recursive decomposition: for example, a proposition like "A is a" can be parsed with "A" as argument and "is a" as unary function, or vice versa, with binary connectives like conditionals applied recursively to form nested structures. Quantification is handled recursively via a "concavity" stroke binding variables over scopes, enabling the expression of generality in a formally precise, hierarchical manner. This recursive syntactic framework laid groundwork for modern predicate logic, treating logical forms as built iteratively from primitive elements. Ernst Zermelo's 1908 axiomatization of , published in "Untersuchungen über die Grundlagen der Mengenlehre," incorporated the axiom schema of separation (Aussonderung), a restricted form of comprehension that enables recursive definitions by forming subsets from existing sets based on definite properties. Separation states that for any set A and property φ, the collection {x ∈ A | φ(x)} is a set, allowing iterative construction of sets without paradoxes by bounding comprehension to prior sets. Later refinements by and in the 1920s added the , which ensures that the image of a set under a definable function is itself a set, facilitating transfinite recursion—for example, defining ordinal numbers recursively through successor and limit stages. Together, these axioms in Zermelo-Fraenkel (ZF) provide the set-theoretic foundation for recursive hierarchies, underpinning much of modern mathematics.

Key Developments in Logic and Computing

In 1931, introduced primitive recursive functions as a key component in his proof of the first incompleteness theorem, demonstrating that formal systems capable of expressing basic arithmetic are inherently incomplete by encoding syntactic properties arithmetically using these functions. Gödel defined primitive recursive functions through composition and primitive recursion schemes starting from basic functions like successor and projection, showing they suffice to represent the provability relation within Peano arithmetic, thereby revealing undecidable propositions. Building on this foundation, and independently formalized the notion of in 1936, equating it with recursive functions to resolve Hilbert's . Church's λ-calculus provided a system for defining functions via abstraction and application, proving that λ-definable functions coincide with Gödel-Herbrand recursive functions, thus establishing a based on . Concurrently, Turing introduced Turing machines as abstract devices that compute exactly the partial recursive functions, linking mechanical processes to and showing the unsolvability of the . Their work, known as the Church-Turing thesis, posited that all effectively computable functions are recursive, bridging logic and the emerging field of computing. Stephen Kleene advanced recursion theory in 1936 by developing a comprehensive framework for partial recursive functions, culminating in the normal form , which asserts that every partial recursive function can be expressed in a standardized μ-recursive form using a universal primitive recursive predicate T and a primitive recursive extraction function U. This enabled the enumeration of all partial recursive functions and formalized their , providing a cornerstone for later developments in and automata. Kleene's contributions clarified the structure of , distinguishing total from partial functions and influencing the analysis of algorithmic processes. His 1938 work further built on this foundation. In 1960, John McCarthy pioneered practical recursive programming with , the first language designed explicitly around recursive functions of symbolic expressions, enabling direct implementation of λ-calculus abstractions for list processing and symbolic computation. McCarthy's system treated code as data through S-expressions, supporting recursive definitions like eval and apply, which facilitated applications and marked the transition from theoretical to programmable constructs in early computing. This innovation influenced subsequent paradigms, where recursion underpins rule-based inference.

References

  1. https://ocw.mit.edu/courses/6-042j-mathematics-for-computer-science-spring-2015/mit6_042js15_session10.pdf
  2. https://www.math.fsu.edu/~pkirby/mad2104/SlideShow/s4_3.pdf
  3. https://people.math.sc.edu/dw7/class_webpages/Math174/Chapter%203/Section%203.3.pdf
  4. https://math.libretexts.org/Bookshelves/Combinatorics_and_Discrete_Mathematics/Elementary_Foundations:_An_Introduction_to_Topics_in_Discrete_Mathematics_(Sylvestre)/11:_Recurrence_and_induction/11.04:_Inductive_definitions
  5. https://cburch.com/csbsju/cs/160/notes/29/0.html
  6. http://people.umass.edu/partee/726_04/lectures/Lecture9_Induction.pdf
  7. https://fa.ewi.tudelft.nl/~hart/onderwijs/set_theory/Jech/Kunen-1980-Set_Theory.pdf
  8. https://plato.stanford.edu/entries/recursive-functions/
  9. https://homepages.inf.ed.ac.uk/rmayr/Ch5.pdf
  10. https://www.cs.yale.edu/homes/aspnes/classes/202/notes.pdf
  11. https://pages.cs.wisc.edu/~paton/readings/Old/fall01/RECURSION.html
  12. https://archive.org/details/cu31924001586282
  13. https://archive.org/details/arithmeticespri00peangoog
  14. https://csc151.cs.grinnell.edu/readings/recursion-over-numbers.html
  15. https://www3.cs.stonybrook.edu/~skiena/113/lectures/lecture14/lecture14.html
  16. http://courses.ics.hawaii.edu/ReviewICS141/morea/recursion/RecursiveDefinitions-QA.pdf
  17. https://mathresearch.utsa.edu/wiki/index.php?title=Recursion
  18. https://eng.libretexts.org/Bookshelves/Computer_Science/Programming_and_Computation_Fundamentals/Mathematics_for_Computer_Science_(Lehman_Leighton_and_Meyer)/01%3A_Proofs/06%3A_Recursive_Data_Types/6.01%3A_Recursive_Definitions_and_Structural_Induction
  19. http://cslibrary.stanford.edu/110/BinaryTrees.html
  20. https://plato.stanford.edu/entries/recursive-functions/ackermann-peter.html
  21. https://plato.stanford.edu/entries/set-theory/
  22. https://www.math.ucla.edu/~ynm/114l.1.21s/pl.pdf
  23. https://sites.oxy.edu/traiger/logic/primer/chapter2/wffs-PL.html
  24. https://www.cs.toronto.edu/~axgao/cs245_s18/slides/lec02_prop_syntax_sol.pdf
  25. https://www3.cs.stonybrook.edu/~cse371/lec13.pdf
  26. https://scholar.harvard.edu/files/yxiang/files/handout_2_propositional-logic-2014.pdf
  27. https://builds.openlogicproject.org/content/first-order-logic/syntax-and-semantics/syntax.pdf
  28. http://people.umass.edu/partee/726_06/lectures/Lecture9_Model_theory.pdf
  29. https://mathworld.wolfram.com/HerbrandUniverse.html
  30. https://dl.acm.org/doi/10.1145/367177.367199
  31. https://academic.oup.com/comjnl/article-abstract/5/1/10/395338
  32. https://www.doc.ic.ac.uk/~rak/papers/IFIP74.pdf
  33. https://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf
  34. https://cgi.di.uoa.gr/~takis/pereira-warren.pdf
  35. https://www.doc.ic.ac.uk/~rak/papers/sl.pdf
  36. https://www.ling.ohio-state.edu/~pollard/680/chapters/induction.pdf
  37. https://engineering.purdue.edu/~relation/surf/files/induction-discussion.pdf
  38. https://donaldlab.cs.duke.edu/Teaching/discretemath/Online/handouts/induction/index.shtml
  39. https://www.cs.princeton.edu/courses/archive/spr99/cs126/comments/09recursion.html
  40. http://ramanujan.math.trinity.edu/rdaileda/teach/s20/m3326/lectures/strong_induction_handout.pdf
  41. https://www.cs.tulane.edu/~zzheng3/teaching/cmps2170/fall18/slides/induction.pdf
  42. https://cecchetti.sites.cs.wisc.edu/cs704/2024fa/notes/lec05-wf-induction.pdf
  43. https://people.engr.tamu.edu/andreas-klappenecker/cpsc289-f08/noetherian_induction.pdf
  44. https://www.cl.cam.ac.uk/teaching/1819/DiscMath/AddWFI.pdf
  45. https://lamport.azurewebsites.net/pubs/recursive-ops.pdf
  46. https://rg1-teaching.mpi-inf.mpg.de/autrea-ss10/script/lecture3.pdf
  47. https://plato.stanford.edu/entries/dedekind-foundations/
  48. https://plato.stanford.edu/entries/peano-arithmetic/
  49. https://raw.githubusercontent.com/mdnahas/Peano_Book/master/Peano.pdf
  50. https://plato.stanford.edu/entries/frege-logic/
  51. https://plato.stanford.edu/entries/zermelo-set-theory/
  52. https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/church.pdf
  53. https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
  54. https://www-formal.stanford.edu/jmc/recursive.pdf
Add your contribution
Related Hubs
User Avatar
No comments yet.