Рекурсивные функции, типы и произвольное число аргументов

[arseniiv]

Приведу здесь определения, чтобы не было неоднозначности, хотя это вещи и известные, т. к. задача зависит от одной из деталей. $\mathbb N,\mathbb N^+,\mathbb N'$ ниже — неотрицательные и положительные целые числа и $\mathbb N\cup\{\bot\},\bot\notin\mathbb N$ соответственно.

Рассмотрим систему вывода термов вида $\ldots:n, n\in\mathbb N$ с аксиомами $O:0$, $S:1$ и $I^n_m:n$ для всевозможных $m,n\in\mathbb N^+,m\leqslant n$ и правилами вывода

$$\frac{f:m, \quad g_1,\ldots,g_m:n}{C(f,g_1,\ldots,g_m):n}\,\mathsf C_m,m\in\mathbb N^+ \qquad \frac{b:n, \quad s:n+2}{R(b,s):n+1}\,\mathsf R \qquad \frac{m:n+1}{M(m):n}\,\mathsf M.$$

Нетрудно показать, что для каждого $t$, для которого выводимо $t:n$, не выводимо никакого $t:m, m\ne n$. Это можно исправить, введя правило

$$\frac{f:m}{C(f):n}\,\mathsf C_0.$$

Пусть $Tt = \{ n\in\mathbb N : {\vdash t:n} \}$. Можно заметить, что $T\ldots$ бывает всего нескольких видов — $\varnothing,\{n\},\mathbb N+n$.

Назначим правила для вычисления выводимых термов — опять же всё вполне стандартно, только $[t]\in\bigcup\limits_{n\in Tt}(\mathbb N'^n\to\mathbb N')$ будет функцией, принимающей возможно разное число аргументов;

$$[O]() = 0, \qquad [S](n) = (n\ne\bot)\mathrel? n+1 :\bot, \qquad [I^n_m](x_1,\ldots,x_n) = (\bot\notin\{x_1,\ldots,x_n\})\mathrel? x_m :\bot,$$

$$[C(f,\vec g)](\vec x) = (\bot\notin\{y_1,\ldots,y_m\})\mathrel? f(\vec y) :\bot\text{, где }y_i = g_i(\vec x),$$

$$[R(b,s)](0,\vec x) = b(\vec x), \qquad [R(b,s)](n+1,\vec x) = s(n,[R(b,s)](n,\vec x),\vec x), \qquad [R(b,s)](\bot,\vec x) = \bot,$$

$$[M(m)](\vec x) = (0\in\{ m(a,\vec x) : a\in\mathbb N \})\mathrel? \min((a\in\mathbb N\mapsto m(a,\vec x))^{-1}\{0\}) :\bot.$$

Опишите вычислительные свойства термов $t$, для которых $Tt$ бесконечно, и по каким конкретно причинам введение правила вывода $\mathsf C_0$ было излишним.

[arseniiv]

Ладно, ввиду скорее всего неинтересности темы даже для тех, кто мало знаком с темой, сам отвечу.

(Ответ)

Такие термы $t$ имеют одно общее свойство: для каждого из них существует число $k\in\mathbb N$ такое, что для любого $n$ значение $[t](x_1,\ldots,x_n)$ не зависит от значений $x_i, i\geqslant k$ (ещё бы оно зависело!). Эти термы вообще бы были константными, не будь $\mathsf R$, позволяющего добавлять аргумент, от положительности которого можно ввести зависимость.

Правило $\mathsf C_0$ известно избыточно, потому что $n$-местную константу можно рекурсивно построить с помощью $\mathsf R$ из нульместной. Интересности же, которые оно вносит в систему типов (можно переформулировать все правила вывода в виде $t : A$, где $A$ — что-нибудь из $\varnothing,\{n\},\mathbb N+n$, введя на этих типах частичный порядок и операции ${}\pm1$), из предыдущего оказываются неинтересными. Так что плюсов от него нет. (Кроме того, подход к определениям, используемый Манином в нескольких местах (хотя бы в «Вычислимом и невычислимом»), ещё лучше: у нас сразу есть многоместный ноль и всего одно правило для композиции (значения функций — в $\mathbb N^k$).)