Примитивный рекурсивный функционал

В математической логике примитивно -рекурсивные функционалы представляют собой обобщение примитивно-рекурсивных функций в теорию более высокого типа . Они состоят из набора функций всех чистых конечных типов.

Примитивно-рекурсивные функционалы важны в теории доказательств и конструктивной математике . Они являются центральной частью диалектической интерпретации интуиционистской арифметики, разработанной Куртом Гёделем .

В теории рекурсии примитивные рекурсивные функционалы являются примером вычислимости высшего типа, а примитивные рекурсивные функции являются примерами вычислимости по Тьюрингу.

Фон

У каждого примитивно-рекурсивного функционала есть тип, который говорит, какие входные данные он принимает и какой выходной результат он производит. Объект типа 0 — это просто натуральное число; ее также можно рассматривать как постоянную функцию, которая не принимает входных данных и возвращает выходные данные в виде набора N натуральных чисел.

Для любых двух типов σ и τ тип σ→τ представляет собой функцию, которая принимает входные данные типа σ и возвращает выходные данные типа τ. Таким образом, функция f ( n ) = n +1 имеет тип 0 → 0. Типы (0→0)→0 и 0→(0→0) разные; по соглашению обозначение 0→0→0 относится к 0→(0→0). На жаргоне теории типов объекты типа 0 → 0 называются функциями , а объекты, которые принимают входные данные типа, отличного от 0, называются функционалами .

Для любых двух типов σ и τ тип σ×τ представляет собой упорядоченную пару, первый элемент которой имеет тип σ, а второй элемент имеет тип τ. Например, рассмотрим функционал A , который принимает на вход функцию f от N до N и натуральное число n и возвращает f ( n ). Тогда A имеет тип (0 × (0→0))→0. Этот тип также можно записать как 0→(0→0)→0 с помощью Currying .

Множество (чистых) конечных типов — это наименьший набор типов, включающий 0 и замкнутый относительно операций × и →. Верхний индекс используется для обозначения того, что предполагается, что переменная x ^τ имеет определенный тип τ; верхний индекс может быть опущен, если тип ясен из контекста.

Определение

Примитивно-рекурсивные функционалы — это наименьшая совокупность объектов конечного типа, такая что:

• Постоянная функция f ( n ) = 0 является примитивно-рекурсивным функционалом
• Функция-преемник g ( n ) = n + 1 является примитивно-рекурсивным функционалом
• Для любого типа σ×τ функционал K( x ^σ , y ^τ ) = x является примитивно-рекурсивным функционалом
• Для любых типов ρ, σ, τ функционал

  S( р ^ρ→σ→τ , s ^ρ→σ , т ^ρ ) знак равно ( р ( т ))( s ( т ))

  является примитивно-рекурсивным функционалом

• Для любого типа τ, f типа τ и любого g типа 0→τ→τ функционал R ( f , g ) ^0→τ определяется рекурсивно как

  р ( ж , г ) (0) знак равно ж ,

  р ( ж , г )( п +1) знак равно г ( п , р ( ж , г )( п ))

  является примитивно-рекурсивным функционалом

Смотрите также

• Диалектическая интерпретация
• Функция высшего порядка
• Примитивная рекурсивная функция
• Просто напечатанное лямбда-исчисление

Рекомендации

• Джереми Авигад и Соломон Феферман (1999). Функциональная интерпретация Гёделя («Диалектика») (PDF) . в издании С. Басса, Справочник по теории доказательств, Северная Голландия. стр. 337–405.