Primitive recursive functional: Difference between revisions
Added See also section |
No edit summary |
||
Line 1: | 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. |
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]]. |
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. |
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: | Line 7: | ||
== Background == |
== Background == |
||
Every primitive recursive functional has a type, which |
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 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: | Line 41: | ||
| title = Gödel's functional ("Dialectica") interpretation |
| title = Gödel's functional ("Dialectica") interpretation |
||
| url = http://math.stanford.edu/~feferman/papers/dialectica.pdf |
| url = http://math.stanford.edu/~feferman/papers/dialectica.pdf |
||
| author = Jeremy Avigad and Solomon Feferman |
| author = [[Jeremy Avigad]] and [[Solomon Feferman]] |
||
| publisher = in S. Buss ed., The Handbook of Proof Theory, North-Holland |
| publisher = in S. Buss ed., The Handbook of Proof Theory, North-Holland |
||
| year = 1999 |
| year = 1999 |
Revision as of 01:12, 17 February 2021
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
- 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.