Funkcjonalność rekurencyjna prymitywna - Primitive recursive functional

W logice matematycznej , że prymitywne rekurencyjne Funkcjonały są uogólnieniem funkcji pierwotnie rekurencyjnych w wyższej teorii typów . Składają się ze zbioru funkcji we wszystkich czystych typach skończonych.

Prymitywne funkcjonały rekurencyjne są ważne w teorii dowodu i matematyce konstruktywnej . Stanowią centralną część interpretacji intuicjonistycznej arytmetyki Dialectica opracowanej przez Kurta Gödla .

W teorii rekurencji prymitywne funkcje rekurencyjne są przykładem obliczalności wyższego typu, ponieważ pierwotne funkcje rekurencyjne są przykładami obliczalności Turinga.

tło

Każda prymitywna funkcja rekurencyjna ma typ, który mówi, jakiego rodzaju dane wejściowe przyjmuje i jaki typ danych wyjściowych generuje. Obiekt typu 0 jest po prostu liczbą naturalną; można go również postrzegać jako funkcję stałą, która nie pobiera danych wejściowych i zwraca wynik w zbiorze N liczb naturalnych.

Dla dowolnych dwóch typów σ i τ, typ σ → τ reprezentuje funkcję, która przyjmuje dane wejściowe typu σ i zwraca dane wyjściowe typu τ. Zatem funkcja f ( n ) = n +1 jest typu 0 → 0. Rodzaje (0 → 0) → 0 i 0 → (0 → 0) są różne; umownie notacja 0 → 0 → 0 odnosi się do 0 → (0 → 0). W żargonie teorii typów obiekty typu 0 → 0 nazywane są funkcjami, a obiekty, które przyjmują dane wejściowe typu innego niż 0, nazywane są funkcjonałami .

Dla dowolnych dwóch typów σ i τ, typ σ × τ reprezentuje uporządkowaną parę, której pierwszy element ma typ σ, a drugi element ma typ τ. Na przykład, rozważmy, że funkcja A przyjmuje jako dane wejściowe funkcję f od N do N oraz liczbę naturalną n i zwraca f ( n ). Wtedy A ma typ (0 × (0 → 0)) → 0. Ten typ można również zapisać jako 0 → (0 → 0) → 0 przez Currying .

Zbiór (czystych) typów skończonych jest najmniejszym zbiorem typów, który zawiera 0 i jest zamykany w ramach operacji × i →. Indeks górny służy do wskazania, że zakłada się, że zmienna x τ ma określony typ τ; indeks górny można pominąć, gdy typ jest jasny z kontekstu.

Definicja

Prymitywne funkcjonały rekurencyjne to najmniejszy zbiór obiektów typu skończonego, który:

  • Funkcja stała f ( n ) = 0 jest prymitywnym funkcjonałem rekurencyjnym
  • Następująca funkcja g ( n ) = n + 1 jest prymitywnym funkcjonałem rekurencyjnym
  • Dla dowolnego typu σ × τ, funkcjonał K ( x σ , y τ ) = x jest prymitywnym funkcjonałem rekurencyjnym
  • Dla wszystkich typów ρ, σ, τ, funkcjonał
    S ( r ρ → σ → τ , s ρ → σ , t ρ ) = ( r ( t )) ( s ( t ))
    jest prymitywną funkcją rekurencyjną
  • Dla dowolnego typu τ i f typu τ oraz dowolnego g typu 0 → τ → τ, funkcjonał R ( f , g ) 0 → τ zdefiniowany rekurencyjnie jako
    R ( f , g ) (0) = f ,
    R ( f , g ) ( n +1) = g ( n , R ( f , g ) ( n ))
    jest prymitywną funkcją rekurencyjną

Zobacz też

Bibliografia

  • Jeremy Avigad i Solomon Feferman (1999). Funkcjonalna interpretacja Gödla („Dialectica”) (PDF) . w S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405.