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

Примитивно рекурсивный функционал (Шаблон:Lang-en) — обобщение понятия примитивно рекурсивной функции на многомерную теорию типов.

Примитивно рекурсивные функционалы играют важную роль в теории доказательств и конструктивной математике и составляют ядро гедёлевской «диалектической» интерпретации интуиционистской арифметики.

С токи зрения теории вычислимости, примитивно рекурсивные функционалы представляет собой пример вычислимости в типах высших размерностей, а обыкновенные примитивно рекурсивные функции — вычислимости по Тьюрингу.

Общие сведения

Каждый примитивно рекурсивный функционал имеет тип, указывающий, что функционал получает на вход, и что производит в качестве результата. Тип $0$ имеют натуральные числа; их можно трактовать как константные функции без аргументов со значением из множества $\mathbb{N}$ (множества натуральных чисел).

Если $\sigma$ и $\tau$ — типы, то тип $\sigma \to \tau$ имеют функции с аргументом типа $\sigma$ и результатом типа $\tau$. Таким образом, функция $f:x\mapsto x+1$ имеет тип $0\to 0$. Типы $(0\to 0)\to 0$ и $0\to (0\to 0)$ различны; запись $0\to 0\to 0$ обозначает $0\to (0\to 0)$. На жаргоне теории типов, объект «стрелочного» типа $\sigma \to 0$ называется функцией, если тип его аргумента $0$, и функционалом в противном случае.

Из двух типов $\sigma$ и $\tau$ можно построить $\sigma \times \tau$ — тип упорядоченных пар, в которых первый компонент имеет тип $\sigma$, а второй — тип $\tau$. Например, рассмотрим функционал $A$, который принимает на вход натуральное число $n$ и функцию $f$ из $\mathbb{N}$ в $\mathbb{N}$, и возвращает $f(n)$. Тогда $A$ имеет тип $(0\times (0\to 0))\to 0$; с помощью каррирования этот тип можно записать как $0\to (0\to 0)\to 0$.

Множество (чистых) конечных типов  — это наименьшее множество, содержащее $0$ и замкнутое относительно операций $\to$ и $\times$. Верхний индекс над переменной (например, $x^{\sigma }$) означает предположение о типе этой переменной (т.е. предположение, что $x:\sigma$). В случае, когда тип ясен из контекста, индекс может быть опущен.

Определение

Множество примитивно рекурсивных функционалов определяется индуктивно как наименьшее множество объектов конечного типа, содержащее:

• Константу $\mathrm{𝟢}$ типа $0$.
• Функцию инкремента $𝖭:0\to 0$ с семантикой $𝖭(x)=x+1$; часто обозначается также $𝖲𝖼$ или просто штрихом ($x^{\prime }$).
• ${𝖪}_{\sigma \tau }:\sigma \to \tau \to \sigma$ — набор комбинаторов постоянных функций для всевозможных типов $\sigma$ и $\tau$; ${𝖪}_{\sigma \tau }(x^{\sigma },y^{\tau })=x$.
• ${𝖲}_{\rho \sigma \tau }:(\rho \to \sigma \to \tau )\to (\rho \to \sigma )\to \rho \to \tau$ — набор комбинаторов «совместного применения»; $𝖲(f,g,x)=f(x,g(x))$.
• ${𝖱}_{\tau }:\tau \to (0\to \tau \to \tau )\to 0\to \tau$ — операторы примитивной рекурсии;$\{\begin{array}{c}𝖱(f,g)(\mathrm{𝟢})=f\\ 𝖱(f,g)(𝖭(x))=g(x,𝖱(f,g)(x))\end{array}$.
• Композицию $s(t):\sigma$ примитивно рекурсивных функционалов $s^{\tau \to \sigma }$ и $t^{\tau }$.

См. также

• D-интерпретация («диалектическая» интерпретация)
• Функция высшего порядка
• Примитивно рекурсивная функция
• Просто типизированное лямбда-исчисление

Литература

• Шаблон:Публикация