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

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

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

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

Общие сведенияПравить

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

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

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

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

ОпределениеПравить

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

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