In mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

, the primitive recursive functionals are a generalization of primitive recursive functions into higher type theory

Type theory

In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...

. They consist of a collection of functions in all pure finite types.

The primitive recursive functionals are important in proof theory

Proof theory

Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...

 and constructive mathematics They are a central part of the Dialectica interpretation

Dialectica interpretation

In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic...

 of intuitionistic arithmetic developed by Kurt Gödel

Kurt Gödel

Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...

.

In recursion theory

Recursion theory

Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...

, the primitive recursive functionals are an example of higher-type computability, as primitive recursive functions are examples of Turing computability.

Background

Every primitive recursive functional has a type, which tells what kind of inputs it takes and what kind of output it produces. An object of type 0 is simply a natural number; it can also be viewed as a constant function that takes no input and returns an output in the set N of natural numbers.

For any two types σ and τ, the type σ→τ represents a function that takes an input of type σ and returns an output of type τ. Thus the function f(n) = n+1 is of type 0→0. The types (0→0)→0 and 0→(0→0) are different; by convention, the notation 0→0→0 refers to 0→(0→0). In the jargon of type theory, objects of type 0→0 are called functions and objects that take inputs of type other than 0 are called functionals.

For any two types σ and τ, the type σ×τ represents an ordered pair, the first element of which has type σ and the second element of which has type τ. For example, consider the functional A takes as inputs a function f from N to N, and a natural number n, and returns f(n). Then A has type (0 × (0→0))→0. This type can also be written as 0→(0→0)→0, by Currying

Currying

In mathematics and computer science, currying is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument...

.

The set of (pure) finite types is the smallest collection of types that includes 0 and is closed under the operations of × and →. A superscript is used to indicate that a variable x^τ is assumed to have a certain type τ; the superscript may be omitted when the type is clear from context.

Definition

The primitive recursive functionals are the smallest collection of objects of finite type such that:

• The constant function f(n) = 0 is a primitive recursive functional
• The successor function g(n) = n + 1 is a primitive recursive functional
• For any type σ×τ, the functional K(x^σ, y^τ) = x is a primitive recursive functional
• For any types ρ, σ, τ, the functional

  S(r^ρ→σ→τ,s^ρ→σ, t^ρ) = (r(t))(s(t))

  is a primitive recursive functional

• For any type τ, and f of type τ, and any g of type 0→τ→τ, the functional R(f,g)^0→τ defined recursively as

  R(f,g)(0) = f,

  R(f,g)(n+1) = g(n,R(f,g)(n))

  is a primitive recursive functional