Правила - подстановка
Cтраница 2
Наиболее общие грамматики типа 0 не накладывают никаких ограничений на правила подстановки. Применительно к языкам программирования они обладают излишней общностью. [16]
При разборе сверху вниз существенным является порядок, в котором проверяются правила подстановки. Сначала необходимо проверять более сложные правила. В противном случае могло бы оказаться, что в некотором правиле подстановки, таком, как ( целое без знака):: ( цифра) ( цифра) ( целое без знака), вторая возможность никогда не проверялась, поскольку если она имеет место, то всегда имеет место и первая, так что анализатор никогда не достиг бы второй альтернативы. [17]
Грамматика представляет собой формальную конструкцию, содержащую образования трех типов: терминальные или первичные символы, нетерминальные символы и правила подстановок или порождающие правила. Грамматика может использоваться либо в порождающем, либо в анализирующем режиме. Когда грамматика используется в порождающем режиме, она позволяет конструировать строки терминальных символов путем последовательного применения правил подстановок. Строка терминальных символов, построенная с помощью данной грамматики в порождающем режиме, называется предложением. Множество всех предложений, которые могут быть построены с помощью данной грамматики, называется языком этой грамматики. [18]
Вывод, в котором в качестве исходных формул используются только тождественно истинные формулы исчисления высказываний, а в качестве прочих вспомогательных средств - только правила подстановки вместо формульных переменных без аргументов, правило повторения и схема заключения, мы называем выводом средствами исчисления высказываний или при помощи средств исчисления высказываний. [19]
Необходимо изменить правила переходов между состояниями ( сравните с реализацией вызовов по имени, описанной в тексте главы) и семантическую функцию cval, определяющую правила подстановки для р - н б-редукции. В остальном доказательство аналогично приведенному в тексте главы. [20]
 |
Удачное применение алгоритма-построителя LR ( 1 для грамматики Р. [21] |
Обобщая, можно сказать, что если в множестве конфигураций представлено более одного возможного исхода ( или полностью расширенное и частично расширенное правило подстановки, как в приведенном ранее1случае, или два или более различных расширенных правила подстановки), то либо множества правых контекстов, ассоциируемых с ними, должны быть непересекающимися, либо грамматика не будет LR ( k) для этого к. Если они непересекающиеся, мы просто добавляем соответствующие признаки к рассматриваемому состоянию и продолжаем процесс. Для частично расширенных правил переносим терминальные k головы остальной части правила вправо от курсора и прибавляем правый контекст. [22]
Затем, как и в ранее рассмотренных формализмах, в формализме К, ввиду осуществимости возвратного переноса подстановок в исходные формулы, имеется возможность исключить с помощью схем формул формульные переменные и сделать ненужными правила подстановки. [23]
Напомним, что правила вывода арифметики, по определению, совпадают с правилами вывода расширенного исчисления предикатов, которые в свою очередь отличаются от правил исчисления предикатов только тем, что в связи с введением термов расширены правила подстановки. Следовательно, нам достаточно доказать утверждение теоремы для всех правил вывода расширенного исчисления предикатов. [24]
Поэтому каждая квазирекурсивная функция одного аргумента вычислима в некотором формализме, определяемом - если взять за основу расширенное понятие терма - заданием некоторой системы равенств между термами ( играющих роль исходных формул) и трех упоминавшихся правил вывода: правила подстановки терма вместо индивидной переменной, схемы замены и схемы перестановки. [25]
Действительно, вычисление значения такого терма t может быть формализовано посредством вывода, который от рекурсивных равенств, участвующих в рекурсивном построении t, ведет к равенству t m, где т - значение этого терма При этом используются аксиома равенства ( J2), правила подстановки и средства исчисления высказываний. [26]
Введем сначала следующее определение: Мы будем говорить, что формула 23 выводима из формулы 91, если 91 - 23 есть формула и формула S3 выводима из совокупности всех выводимых формул исчисления предикатов и формулы 91 посредством применения всех правил исчисления предикатов, причем оба правила связывания квантором, правила подстановки вместо переменных предикатов и вместо свободных предметных переменных должны применяться только к таким переменным предикатам или предметам, которые в формулу 91 не входят. [27]
Правила подстановок языков, основанных на лямбда-исчислении, ставят перед проектировщиком вычислительных машин серьезные проблемы. Берклинг [3] разработал модифицированное лямбда-исчисление с тремя видами применений, в котором нет необходимости переименовывать переменные. [28]
Формальные параметры указываются в описании подпрограммы, а фактические - в обращении к ней. Правила подстановки фактических параметров определяются языком программирования. [29]
Совместимость, в описанном выше смысле, гарантирует работоспособность операций присваивания. Кроме того, что очень важно, она определяет правила подстановки значений или переменных в вызовы процедур и функций. [30]
Страницы: 1 2 3