Primitivní rekurzivní funkce - Primitive recursive functional

v matematická logika, primitivní rekurzivní funkcionály jsou zobecněním primitivní rekurzivní funkce na vyšší teorie typů. Skládají se z kolekce funkcí ve všech čistě konečných typech.

Primitivní rekurzivní funkcionály jsou důležité v teorie důkazů a konstruktivní matematika Jsou ústřední součástí Výklad dialektiky intuitivní aritmetiky vyvinuté Kurt Gödel.

v teorie rekurze, primitivní rekurzivní funkcionály jsou příkladem vypočítatelnosti vyššího typu, protože primitivní rekurzivní funkce jsou příklady Turingovy vypočítatelnosti.

Pozadí

Každá primitivní rekurzivní funkcionalita má typ, který říká, jaké vstupy přijímá a jaký výstup produkuje. Objekt typu 0 je jednoduše přirozené číslo; lze ji také zobrazit jako konstantní funkci, která nepřijímá žádný vstup a vrací výstup v sadě N přirozených čísel.

Pro libovolné dva typy σ a τ představuje typ σ → τ funkci, která převezme vstup typu σ a vrátí výstup typu τ. Tedy funkce F(n) = n+1 je typu 0 → 0. Typy (0 → 0) → 0 a 0 → (0 → 0) jsou různé; podle konvence se zápis 0 → 0 → 0 vztahuje k 0 → (0 → 0). V žargonu teorie typů se nazývají objekty typu 0 → 0 funkce a objekty, které přijímají vstupy jiného typu než 0, se nazývají funkcionáři.

Pro jakékoli dva typy σ a τ představuje typ σ × τ uspořádaný pár, jehož první prvek má typ σ a druhý prvek má typ τ. Zvažte například funkční A bere jako vstupy funkci F z N na Na přirozené číslo na vrátí se F(n). Pak A má typ (0 × (0 → 0)) → 0. Tento typ lze také zapsat jako 0 → (0 → 0) → 0, podle Kari.

Sada (čistého) konečné typy je nejmenší sbírka typů, která obsahuje 0 a je uzavřena pod operacemi × a →. Horní index se používá k označení, že proměnná X^τ předpokládá se, že má určitý typ τ; horní index může být vynechán, pokud je typ jasný z kontextu.

Definice

Primitivní rekurzivní funkcionály jsou nejmenší kolekce objektů konečného typu, která:

• Konstantní funkce F(n) = 0 je primitivní rekurzivní funkce
• Funkce nástupce G(n) = n + 1 je primitivní rekurzivní funkce
• Pro jakýkoli typ σ × τ je funkční K (X^σ, y^τ) = X je primitivní rekurzivní funkce
• Pro všechny typy ρ, σ, τ je funkční

  S (r^{ρ → σ → τ},s^{ρ → σ}, t^ρ) = (r(t))(s(t))

  je primitivní rekurzivní funkce

• Pro jakýkoli typ τ a F typu τ a jakékoli G typu 0 → τ → τ, funkční R(F,G)^{0 → τ} definován rekurzivně jako

  R(F,G)(0) = F,

  R(F,G)(n+1) = G(n,R(F,G)(n))

  je primitivní rekurzivní funkce

Viz také

• Výklad dialektiky
• Funkce vyššího řádu
• Primitivní rekurzivní funkce
• Jednoduše zadaný lambda kalkul

Reference

• Jeremy Avigad a Solomon Feferman (1999). Gödelova funkční interpretace („Dialectica“) (PDF). v S. Buss ed., The Handbook of Proof Theory, North-Holland. 337–405.