ART

In mathematical logic, the primitive recursive functionals are a generalization of primitive recursive functions into higher type theory. They consist of a collection of functions in all pure finite types.

The primitive recursive functionals are important in proof theory and constructive mathematics They are a central part of the Dialectica interpretation of intuitionistic arithmetic developed by Kurt Gödel.

In recursion theory, 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.

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

See also

Dialectica interpretation
Higher-order function
Primitive recursive function
Simply typed lambda calculus

References
Jeremy Avigad and Solomon Feferman (1999). Gödel's functional ("Dialectica") interpretation (PDF). in S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405.

 

Undergraduate Texts in Mathematics

Graduate Texts in Mathematics

Graduate Studies in Mathematics

Mathematics Encyclopedia

World

Index

Hellenica World - Scientific Library

Retrieved from "http://en.wikipedia.org/"
All text is available under the terms of the GNU Free Documentation License