{
  "id": "enwiki-001365279734",
  "slug": "primitive-recursive-functional",
  "title": "Primitive recursive functional",
  "qid": "",
  "lead": "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.",
  "body": "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. 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. 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",
  "categories": [
    "20476433",
    "26868936"
  ],
  "license": "CC BY-SA 4.0",
  "source_uri": "https://en.wikipedia.org/w/index.php?oldid=1365279734",
  "content_hash": "",
  "created_at": null,
  "updated_at": 1784625860.0,
  "claims": [],
  "contradictions": [],
  "confidence": 0.6,
  "csl": {
    "id": "enwiki-001365279734",
    "type": "webpage",
    "title": "Primitive recursive functional",
    "author": [
      {
        "family": "Anticloud FZ LLE",
        "literal": "Anticloud FZ LLE"
      }
    ],
    "container-title": "encyclopegia.org",
    "publisher": "Anticloud FZ LLE",
    "publisher-place": "Dubai, United Arab Emirates",
    "URL": "https://encyclopegia.org/a/primitive-recursive-functional",
    "issued": {
      "date-parts": [
        [
          2026,
          11,
          15
        ]
      ]
    },
    "accessed": {
      "date-parts": [
        [
          2026,
          11,
          15
        ]
      ]
    },
    "license": "CC BY-SA 4.0",
    "DOI": "eo1:enwiki-001365279734",
    "isBasedOn": "https://en.wikipedia.org/w/index.php?oldid=1365279734",
    "note": "Immutable snapshot enwiki-001365279734"
  }
}