ГОСТ Р 56271-2014
В частности, пример (1) допускается в нерекурсивных механизмах, а пример (2) не допускается.
Обычно множество имен N разделяют на множество примитивных имен Ри множество определенных имен
О. N =PuD. Pr-D = 0. При этом не существует определений шаблонов для имен из Р. в то время как любое имя в
D должно иметь определение.
Если механизм шаблона работает путем повторной замены ссылок (на определенные имена леD) на тело
определения п, это означает, что любой вход вконечном счете (в результате большого конечного числа шагов) при
водит к чему-то, что содержит только имена из Р. тоесть примитивные имена. Видно, что результат не зависит от
порядка, в котором расширяются полученные определенные имена.
Можно видеть, что оценка шаблона путемего расширения непротиворечива саксиоматической точки зрения.
Для каждого определения шаблона:
N[x.y....y-*p
где тело Ь— это комплексный термин, возможно содержащий х.у..... определим аксиому
5
Vx,y,....iV(x.y....}<->fr
и соберем все указанные аксиомы во множество Ах. Теперь, если s — это результат повторного расширения всех
определенных имен в t. то справедливо:
Yxl =s = t
Из аксиоматического прочтения определений шаблонов следует, что расширение s семантически эквива
лентно оригинальному члену Г®. Это можно доказать по индукции, рассматривая шаги расширений и повторные
приложения леммы подстановки.
Следует очень внимательно относиться к аргументам шаблонов: если допустимы аргументы «более высоко
го порядка» (то есть имеются аргументы, которые используются в расширении как функции), то циклы могут по
явиться неожиданно. Например, после определения:
SelfApp(x):=x(x)
использование расширения SelfApp(SelfApp) приводит к зацикливанию, что уничтожает все достоинства
рассматриваемого механизма. Если исключать аргументы более высокого порядка не хочется, то нужно подобрать
для аргументов соответствующую систему типов, исключающуюданную проблему.
С другой стороны, рекурсивные механизмы шаблонов ограничений на зависимость «>» не накладывают. В
частности, можно использовать рекурсивные определения вида (2), рассмотренные выше. Очевидным преиму
ществом здесь является возможность представить комплексные свойства, например, транзитивное замыкание.
Недостатки:
- нет гарантии, что выход вконкретном оконечном устройстве не зависит от порядка расширения:
- можно получить полный по Тьюрингу механизм, то есть кетипированное лямбда-исчисление. Программи
ровать с шаблонами тоже можно. Настоящий программист всегда с этим справится. Правда, механизм шаблонов —
плохой язык программирования: его трудно понять, в нем часто ошибаются. Мета-программирование шаблонов на
языке C++ — типовой пример.
Е.З Прочив технические вопросы
Меры предосторожности для нерекурсивных механизмов шаблонов:
- гложетоказаться интерсным использование тела шаблона, не являющегося правильным (действительным)
членом. Например, определение
& :=л
позволяет использовать предпочтительный символ в качестве связующего элемента. Если расширение имеет вид
строки, то это реально сработает. Однако это сильно затрудняет анализ системы определений шаблона:
- в контексте первого порядка аргументы шаблона не квантифицируются в теле определения:
f(x):=Vx.p<x)
это недопустимо и не имеет смысла;
- реализация должна обеспечить переименование связанных переменных при необходимости. Для шаблона:
f(x):=Vx.p(x.y),
реализация ((у) не сводится к:
vy.p(y.y).
Это известно как захват переменной. Этого можно избежать, например, путем переименования связанных
переменных:
V/.p(y.y).
5
Если это есть шаблоны формул, то можно взять <-* вместо =.
6
Обратное не обязательно верно, так как из Ах может следовать много отношений, которые нельзя дока
зать только путем расширения шаблона.
80