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

В математической логике примитивно рекурсивный функционал (англ. primitive recursive functional) — это обобщение понятия примитивно рекурсивной функции на многомерную теорию типов.

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

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

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

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

Если $\sigma$ и $\tau$ — типы, то тип $\sigma \to \tau$ имеют функции с аргументом типа $\sigma$ и результатом типа $\tau$. Таким образом, функция $f\colon 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\colon \sigma$). В случае, когда тип ясен из контекста, индекс может быть опущен.

Определение

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

• Константу ${\mathsf {0}}$ типа $0$.
• Функцию инкремента ${\mathsf {N}}\colon 0\to 0$ с семантикой ${\mathsf {N}}(x)=x+1$; часто обозначается также ${\mathsf {Sc}}$ или просто штрихом ($x'$).
• ${\mathsf {K}}_{\sigma \tau }\colon \sigma \to \tau \to \sigma$ — набор комбинаторов постоянных функций для всевозможных типов $\sigma$ и $\tau$; ${\mathsf {K}}_{\sigma \tau }(x^{\sigma },y^{\tau })=x$.
• ${\mathsf {S}}_{\rho \sigma \tau }\colon (\rho \to \sigma \to \tau )\to (\rho \to \sigma )\to \rho \to \tau$ — набор комбинаторов «совместного применения»; ${\mathsf {S}}(f,g,x)=f(x,g(x))$.
• ${\mathsf {R}}_{\tau }\colon \tau \to (0\to \tau \to \tau )\to 0\to \tau$ — операторы примитивной рекурсии;${\begin{cases}{\mathsf {R}}(f,g)({\mathsf {0}})=f\\{\mathsf {R}}(f,g)({\mathsf {N}}(x))=g(x,{\mathsf {R}}(f,g)(x))\end{cases}}$.
• Композицию $s(t)\colon \sigma$ примитивно рекурсивных функционалов $s^{\tau \to \sigma }$ и $t^{\tau }$.

См. также

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

Литература

• Avigad, J. Gödel's Functional („Dialectica“) Interpretation / J. Avigad, S. Feferman // Handbook of Proof Theory / edited by Samuel R. Buss. — The Netherlands : Elsevier Science B. V., 1998. — P. 337–405. — (Studies in logic and the foundation of mathematics ; vol. 137). — ISBN 0-444-89840-9.