Замечание по поводу Третьего Манифеста

Хотя парадокс Эпименида по своей сути слишком прост для иллюстрации этого факта, в общем случае идея «предикатов, ссылающихся на предикаты» в реляционной терминологии соответствует отношениям, значениями атрибутов которых являются отношения (relation-valued attributes, RVA). В частности, непосредственно самоссылащийся предикат – т.е. предикат, включающий прямую ссылку на самого себя – соответствует отношению некоторого типа T, содержащему атрибут того же типа T. Такой тип отношения T называется рекурсивно определенным типом. В [4] по этому поводу говорится следующее:

<цитата>

Открытым остается вопрос о том, можно ли определять тип отношения рекурсивно, напрямую или косвенно, в терминах его же самого. Более точно, пусть RELATION{H} является типом отношения, и пусть S(1), S(2), ... – это последовательность множеств, определяемая следующим образом:

S(1) = {t : t является типом некоторого атрибута в {H}}

S(i) = {t : t является типом некоторого компонента в некотором возможном представлении некоторого скалярного типа или типом некоторого атрибута некоторого типа отношения в S(i-1) }

(i > 1)

Если существует некоторое n (n > 0) такое, что RELATION{H} – элемент S(n), то этот тип RELATION{H} является рекурсивно определенным. (Это определение нуждается в небольшом расширении, если поддерживается наследование типов, но эта деталь нас здесь не задевает.) Таким образом, открытый вопрос состоит в том, следует ли допускать рекурсивно определяемые типы. Наша модель не настолько зависит от ответа на этот вопрос, чтобы мы чувствовали себя обязанными уделить ему отдельное внимание; однако в данной книге мы следуем Принципу осторожного проектирования [3] и полагаем (там, где это существенно), что такие типы не допускаются.

</цитата>

Мне кажется, что аргументы, представленные в настоящей статье, делают желательным усиление приведенной позиции. Более точно, теперь я полагаю, что рекурсивно определяемые типы отношений следует явно запретить.
Вот что следует из этой позиции:

Примите к сведению, что я не призываю полностью запретить RVA. Я говорю об этом потому, что многие люди критиковали Третий Манифест за поддержку RVA на том основании, что допущение таких отношений выводит нас в сферу логики второго (или более высокого) порядка. Последнее утверждение, по-видимому, является верным, но никто еще не смог продемонстрировать какую-либо конкретную проблему, порождаемую этим фактом (т.е. только этим фактом) – по крайней мере, никто не продемонстрировал такую проблему нам, авторам [4].
В приведенной выше цитате из [4] говорится, что в этой книге мы полагаем, что рекурсивно определяемые типы не допускаются. Однако в описанном в этой же книге языке Tutorial D определение таких типов допускается (возможно, косвенным образом). Вот простой пример:

VAR RX BASE RELATION { A1 INTEGER, A2 SAME_TYPE_AS ( RX ) };

Более сложный пример:

VAR RX BASE RELATION { A1 INTEGER, A2 SAME_TYPE_AS ( RY ) };
VAR RY BASE RELATION { A3 INTEGER, A4 SAME_TYPE_AS ( RX ) };

Поэтому, возможно, языку Tutorial D в том виде, в котором он описывается в [4], свойственно отсутствие разрешимости. Однако я полагаю, что можно было бы создать реализацию, в которой бы отвергалась любая попытка использования этой «возможности» путем предотвращения (желательно, во время компиляции) любой попытки определения (напрямую или косвенным образом) типа T с использованием его же самого – примерно так же, как система должна предотвращать любую попытку определения ограничения, при вычислении которого во время определения не может быть получено значение TRUE.