Primitive recursive functional

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 says 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

* {{cite book
, title = Gödel's functional ("Dialectica") interpretation
, url = http://math.stanford.edu/~feferman/papers/dialectica.pdf
, author = Jeremy Avigad and Solomon Feferman
, publisher = in S. Buss ed., The Handbook of Proof Theory, North-Holland
, year = 1999
, pages = 337–405

Proof theory
Computability theory