Recursive definition

From Wikipedia, the free encyclopedia
(Redirected from Inductive definition)
Jump to navigation Jump to search

Template:Short description

File:KochFlake.svg
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!Script error: No such module "Check for unknown parameters". is defined by the rules

0!=1.(n+1)!=(n+1)n!.

This definition is valid for each natural number Template:Mvar, 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!Script error: No such module "Check for unknown parameters"., starting from n = 0Script error: No such module "Check for unknown parameters". and proceeding onwards with n = 1, 2, 3Script error: No such module "Check for unknown parameters". 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 Template:Tmath of natural numbers is:

  1. 0 is in Template:Tmath
  2. If an element n is in Template:Tmath then n + 1Script error: No such module "Check for unknown parameters". is in Template:Tmath
  3. Template:Tmath 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, …} Script error: No such module "Check for unknown parameters". 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 + 1Script error: No such module "Check for unknown parameters". whenever it holds of Template:Mvar, then the property holds of all natural numbers (Aczel 1977:742).

Form of recursive definitions

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)Script error: No such module "Check for unknown parameters". (i.e., base case) is given, and that for n > 0Script error: No such module "Check for unknown parameters"., an algorithm is given for determining f(n)Script error: No such module "Check for unknown parameters". in terms of Template:Mvar, f(0),f(1),,f(n1) (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

Let Template:Mvar be a set and let a0Script error: No such module "Check for unknown parameters". be an element of Template:Mvar. If Template:Mvar is a function which assigns to each function Template:Mvar mapping a nonempty section of the positive integers into Template:Mvar, an element of Template:Mvar, then there exists a unique function h:+A such that

h(1)=a0h(i)=ρ(h|{1,2,,i1}) for i>1.

Examples of recursive definitions

Elementary functions

Addition is defined recursively based on counting as

0+a=a,(1+n)+a=1+(n+a).

Multiplication is defined recursively as

0a=0,(1+n)a=a+na.

Exponentiation is defined recursively as

a0=1,a1+n=aan.

Binomial coefficients can be defined recursively as

(a0)=1,(1+a1+n)=(1+a)(an)1+n.

Prime numbers

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 Template:Mvar by this definition requires knowing the primality of every integer between 2 and Template:Mvar, which is well defined by this definition. That last point can be proved by induction on Template:Mvar, 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

The even numbers can be defined as consisting of

  • 0 is in the set Template:Mvar of non-negative evens (basis clause),
  • For any element Template:Mvar in the set Template:Mvar, x + 2Script error: No such module "Check for unknown parameters". is in Template:Mvar (inductive clause),
  • Nothing is in Template:Mvar unless it is obtained from the basis and inductive clauses (extremal clause).

Well formed formula

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

  1. pScript error: No such module "Check for unknown parameters". is a wff if pScript error: No such module "Check for unknown parameters". is a propositional variable.
  2. ¬ pScript error: No such module "Check for unknown parameters". is a wff if pScript error: No such module "Check for unknown parameters". is a wff.
  3. (p • q)Script error: No such module "Check for unknown parameters". is a wff if pScript error: No such module "Check for unknown parameters". and qScript error: No such module "Check for unknown parameters". 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:

  • (pq)Script error: No such module "Check for unknown parameters". is a wff, because the propositional variables pScript error: No such module "Check for unknown parameters". and qScript error: No such module "Check for unknown parameters". are wffs and Script error: No such module "Check for unknown parameters". is a logical connective.
  • ¬ (pq)Script error: No such module "Check for unknown parameters". is a wff, because (pq)Script error: No such module "Check for unknown parameters". is a wff.
  • p ∧ ¬ q)Script error: No such module "Check for unknown parameters". is a wff, because ¬ pScript error: No such module "Check for unknown parameters". and ¬ qScript error: No such module "Check for unknown parameters". are wffs and Script error: No such module "Check for unknown parameters". is a logical connective.

Recursive definitions as logic programs

Script error: No such module "Labelled list hatnote". 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

Notes

<templatestyles src="Reflist/styles.css" />

  1. Script error: No such module "Citation/CS1".
  2. Script error: No such module "citation/CS1".
  3. For a proof of Recursion Theorem, see On Mathematical Induction (1960) by Leon Henkin.
  4. Script error: No such module "citation/CS1".
  5. Denecker, M., Ternovska, E.: A logic of nonmonotone inductive definitions. ACM Trans. Comput. Log. 9(2), 14:1–14:52 (2008)
  6. Warren, D.S. and Denecker, M., 2023. A better logical semantics for prolog. In Prolog: The Next 50 Years (pp. 82-92). Cham: Springer Nature Switzerland.

Script error: No such module "Check for unknown parameters".

References

  • Script error: No such module "citation/CS1".
  • Script error: No such module "citation/CS1".
  • Script error: No such module "citation/CS1".

Template:Defining