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 Studies in Mathematics
Hellenica World - Scientific Library
Retrieved from "http://en.wikipedia.org/"
All text is available under the terms of the GNU Free Documentation License