2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Рекурсивные функции, типы и произвольное число аргументов
Сообщение13.12.2016, 18:52 
Заслуженный участник


27/04/09
28128
Приведу здесь определения, чтобы не было неоднозначности, хотя это вещи и известные, т. к. задача зависит от одной из деталей. $\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$ было излишним.

 Профиль  
                  
 
 Re: Рекурсивные функции, типы и произвольное число аргументов
Сообщение16.12.2016, 20:41 
Заслуженный участник


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

(Ответ)

Такие термы $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$).)

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 2 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group