Walther recursion

Last updated

In computer programming, Walther recursion (named after Christoph Walther) is a method of analysing recursive functions that can determine if the function is definitely terminating, given finite inputs. It allows a more natural style of expressing computation than simply using primitive recursive functions.

Christoph Walther is a German computer scientist, known for his contributions to automated theorem proving. He is Professor emeritus at Darmstadt University of Technology.

In computability theory, primitive recursive functions are a class of functions that are defined using composition and primitive recursion – described below – as central operations. They are a strict subset of those µ-recursive functions which are also total functions. Primitive recursive functions form an important building block on the way to a full formalization of computability. These functions are also important in proof theory.

Since the halting problem cannot be solved in general, there must still be programs that terminate, but which Walther recursion cannot prove to terminate. Walther recursion may be used in total functional languages in order to allow a more liberal style of showing primitive recursion.

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running or continue to run forever.

Total functional programming is a programming paradigm that restricts the range of programs to those that are provably terminating.

See also

BlooP and FlooP are simple programming languages designed by Douglas Hofstadter to illustrate a point in his book Gödel, Escher, Bach. BlooP is a non-Turing-complete programming language whose main control flow structure is a bounded loop. All programs in the language must terminate, and this language can only express primitive recursive functions.

In computer science, a termination analysis is program analysis which attempts to determine whether the evaluation of a given program will definitely terminate. Because the halting problem is undecidable, termination analysis cannot be total. The aim is to find the answer "program does terminate" whenever this is possible. Without success the algorithm working on the termination analysis may answer with "maybe" or continue working infinitely long.

Related Research Articles

In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive. All primitive recursive functions are total and computable, but the Ackermann function illustrates that not all total computable functions are primitive recursive.

In mathematics and computer science, mutual recursion is a form of recursion where two mathematical or computational objects, such as functions or data types, are defined in terms of each other. Mutual recursion is very common in functional programming and in some problem domains, such as recursive descent parsers, where the data types are naturally mutually recursive.

Recursion process of repeating items in a self-similar way

Recursion occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathematics and computer science, where a function being defined is applied within its own definition. While this apparently defines an infinite number of instances, it is often done in such a way that no loop or infinite chain of references can occur.

In mathematical logic and computer science, the general recursive functions or μ-recursive functions are a class of partial functions from natural numbers to natural numbers that are "computable" in an intuitive sense. In computability theory, it is shown that the μ-recursive functions are precisely the functions that can be computed by Turing machines(this is one of the theorems that supports Church–Turing thesis). The μ-recursive functions are closely related to primitive recursive functions, and their inductive definition (below) builds upon that of the primitive recursive functions. However, not every μ-recursive function is a primitive recursive function—the most famous example is the Ackermann function.

Computability theory, also known as recursion theory, is a branch of mathematical logic, of computer science, and of the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since expanded to include the study of generalized computability and definability. In these areas, recursion theory overlaps with proof theory and effective descriptive set theory.

In computer science, divide and conquer is an algorithm design paradigm based on multi-branched recursion. A divide-and-conquer algorithm works by recursively breaking down a problem into two or more sub-problems of the same or related type, until these become simple enough to be solved directly. The solutions to the sub-problems are then combined to give a solution to the original problem.

In computability theory, the μ-operator, minimization operator, or unbounded search operator searches for the least natural number with a given property. Adding the μ-operator to the five primitive recursive operators makes it possible to define all computable functions.

Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm, in the sense that a function is computable if there exists an algorithm that can do the job of the function, i.e. given an input of the function domain it can return the corresponding output. Computable functions are used to discuss computability without referring to any concrete model of computation such as Turing machines or register machines. Any definition, however, must make reference to some specific model of computation but all valid definitions yield the same class of functions. Particular models of computability that give rise to the set of computable functions are the Turing-computable functions and the μ-recursive functions.

In computability theory, a machine that always halts, also called a decider or a total Turing machine, is a Turing machine that eventually halts for every input.

In software, a stack overflow occurs if the call stack pointer exceeds the stack bound. The call stack may consist of a limited amount of address space, often determined at the start of the program. The size of the call stack depends on many factors, including the programming language, machine architecture, multi-threading, and amount of available memory. When a program attempts to use more space than is available on the call stack, the stack is said to overflow, typically resulting in a program crash.

In computability theory, course-of-values recursion is a technique for defining number-theoretic functions by recursion. In a definition of a function f by course-of-values recursion, the value of f(n+1) is computed from the sequence .

Recursion (computer science) method in computer science

Recursion in computer science is a method of solving a problem where the solution depends on solutions to smaller instances of the same problem. The approach can be applied to many types of problems, and recursion is one of the central ideas of computer science.

The power of recursion evidently lies in the possibility of defining an infinite set of objects by a finite statement. In the same manner, an infinite number of computations can be described by a finite recursive program, even if this program contains no explicit repetitions.

In computer science and recursion theory the McCarthy Formalism (1963) of computer scientist John McCarthy clarifies the notion of recursive functions by use of the IF-THEN-ELSE construction common to computer science, together with four of the operators of primitive recursive functions: zero, successor, equality of numbers and composition. The conditional operator replaces both primitive recursion and the mu-operator.

Terminator, a research project at Microsoft Research, is an automated program analyzer that aims to find whether a program can run infinitely. It supports nested loops and recursive functions, pointers and side-effects, and function-pointers as well as concurrent programs. Like all programs for termination analysis it tries to solve the halting problem for particular cases, since the general problem is undecidable. It provides a solution which is sound, meaning that when it states that a program does always terminate, the result is dependable.

In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some invariant conditions, thereby ensuring its termination. A loop variant whose range is restricted to the non-negative integers is also known as a bound function, because in this case it provides a trivial upper bound on the number of iterations of a loop before it terminates. However, a loop variant may be transfinite, and thus is not necessarily restricted to integer values.

References

<i>Artificial Intelligence</i> (journal) Journal published by Elsevier

Artificial Intelligence is a scientific journal on artificial intelligence research. It was established in 1970 and is published by Elsevier. The journal is abstracted and indexed in Scopus and Science Citation Index. The 2009 Impact Factor for this journal is 3.036 and the 5-Year Impact Factor is 4.277.

Massachusetts Institute of Technology University in Massachusetts

The Massachusetts Institute of Technology (MIT) is a private research university in Cambridge, Massachusetts. The Institute is a land-grant, sea-grant, and space-grant university, with an urban campus that extends more than a mile alongside the Charles River. Founded in 1861 in response to the increasing industrialization of the United States, MIT adopted a European polytechnic university model and stressed laboratory instruction in applied science and engineering. It has since played a key role in the development of many aspects of modern science, engineering, mathematics, and technology, and is widely known for its innovation and academic strength, making it one of the most prestigious institutions of higher learning in the world.

David A. McAllester is an American computer scientist who is Professor and former Chief Academic Officer at the Toyota Technological Institute at Chicago. He received his B.S., M.S., and Ph.D. degrees from the Massachusetts Institute of Technology in 1978, 1979, and 1987 respectively. His PhD was supervised by Gerald Sussman. He served on the faculty of Cornell University for the academic year of 1987-1988 and on the faculty of MIT from 1988 to 1995. He was a member of technical staff at AT&T Labs-Research from 1995 to 2002. He has been a fellow of the American Association of Artificial Intelligence since 1997. He has authored over 100 refereed publications.