Primitive recursive functional: Difference between revisions

Revision as of 20:01, 14 February 2011

Revision as of 12:05, 5 May 2014

Line 1:

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.

Line 7:

== 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→00→0. The types (0→00→0)→0→0 and 0→0→(0→00→0) are different; by convention, the notation 0→0→00→0→0 refers to 0→0→(0→00→0). In the jargon of type theory, objects of type 0→00→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→00→0))→0→0. This type can also be written as 0→0→(0→00→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 ==

Line 20:

* 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→τ→τ0→τ→τ, the functional ''R''(''f'',''g'')^{0→τ0→τ} defined recursively as

*::''R''(''f'',''g'')(0) = ''f'',

*::''R''(''f'',''g'')(''n''+1) = ''g''(''n'',''R''(''f'',''g'')(''n''))