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

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

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

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

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

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

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

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

Определение

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

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

См. также

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

Литература

• Avigad, J. / 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 .