Primitive recursive functional: Difference between revisions

Revision as of 09:32, 27 April 2017

Revision as of 01:12, 17 February 2021

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 tellssays 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''.

Line 41:

| 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