Русская Википедия:Примитивно рекурсивный функционал
В математической логике примитивно рекурсивный функционал (Шаблон:Lang-en) — это обобщение понятия примитивно рекурсивной функции на многомерную теорию типов.
Примитивно рекурсивные функционалы играют важную роль в теории доказательств и конструктивной математике и составляют ядро гедёлевской «диалектической» интерпретации интуиционистской арифметики.
С токи зрения теории вычислимости, примитивно рекурсивные функционалы представляет собой пример вычислимости в типах высших размерностей, а обыкновенные примитивно рекурсивные функции — вычислимости по Тьюрингу.
Общие сведения
Каждый примитивно рекурсивный функционал имеет тип, указывающий, что функционал получает на вход, и что производит в качестве результата. Тип <math>0</math> имеют натуральные числа; их можно трактовать как константные функции без аргументов со значением из множества <math>\mathbb{N}</math> (множества натуральных чисел).
Если <math>\sigma</math> и <math>\tau</math> — типы, то тип <math>\sigma \to \tau</math> имеют функции с аргументом типа <math>\sigma</math> и результатом типа <math>\tau</math>. Таким образом, функция <math>f \colon x \mapsto x + 1</math> имеет тип <math>0 \to 0</math>. Типы <math>(0 \to 0) \to 0</math> и <math>0 \to (0 \to 0)</math> различны; запись <math>0 \to 0 \to 0</math> обозначает <math>0 \to (0 \to 0)</math>. На жаргоне теории типов, объект «стрелочного» типа <math>\sigma \to 0</math> называется функцией, если тип его аргумента <math>0</math>, и функционалом в противном случае.
Из двух типов <math>\sigma</math> и <math>\tau</math> можно построить <math>\sigma \times \tau</math> — тип упорядоченных пар, в которых первый компонент имеет тип <math>\sigma</math>, а второй — тип <math>\tau</math>. Например, рассмотрим функционал <math>A</math>, который принимает на вход натуральное число <math>n</math> и функцию <math>f</math> из <math>\mathbb{N}</math> в <math>\mathbb{N}</math>, и возвращает <math>f(n)</math>. Тогда <math>A</math> имеет тип <math>(0 \times (0 \to 0)) \to 0</math>; с помощью каррирования этот тип можно записать как <math>0 \to (0 \to 0) \to 0</math>.
Множество (чистых) конечных типов — это наименьшее множество, содержащее <math>0</math> и замкнутое относительно операций <math>\to</math> и <math>\times</math>. Верхний индекс над переменной (например, <math>x^\sigma</math>) означает предположение о типе этой переменной (т.е. предположение, что <math>x \colon \sigma</math>). В случае, когда тип ясен из контекста, индекс может быть опущен.
Определение
Множество примитивно рекурсивных функционалов определяется индуктивно как наименьшее множество объектов конечного типа, содержащее:
- Константу <math>\mathsf{0}</math> типа <math>0</math>.
- Функцию инкремента <math>\mathsf{N} \colon 0 \to 0</math> с семантикой <math>\mathsf{N}(x) = x + 1</math>; часто обозначается также <math>\mathsf{Sc}</math> или просто штрихом (<math>x'</math>).
- <math>\mathsf{K}_{\sigma\tau} \colon \sigma \to \tau \to \sigma</math> — набор комбинаторов постоянных функций для всевозможных типов <math>\sigma</math> и <math>\tau</math>; <math>\mathsf{K}_{\sigma\tau} (x^\sigma, y^\tau) = x</math>.
- <math>\mathsf{S}_{\rho\sigma\tau} \colon (\rho \to \sigma \to \tau) \to (\rho \to \sigma) \to \rho \to \tau</math> — набор комбинаторов «совместного применения»; <math>\mathsf{S} (f, g, x) = f(x, g(x))</math>.
- <math>\mathsf{R}_\tau \colon \tau \to (0 \to \tau \to \tau) \to 0 \to \tau</math> — операторы примитивной рекурсии;<math>\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}</math>.
- Композицию <math>s(t) \colon \sigma</math> примитивно рекурсивных функционалов <math>s^{\tau \to \sigma}</math> и <math>t^\tau</math>.
См. также
- D-интерпретация («диалектическая» интерпретация)
- Функция высшего порядка
- Примитивно рекурсивная функция
- Просто типизированное лямбда-исчисление
Литература
