Конспект установочных лекций по комплексному курсу Информатика, Теория информации




Описание значений выражений - часть 2


I[t]
 ) переводит в однозначную нормальную форму. Далее предполагается, что терм t с I[t] =
 не обладает никаким терминальным вычислением.

Для СПТ устанавливалось, что правила подстановок термов в АПТ могут применяться на любом месте. В противоположность этому для описания операционной семантики ЯП мы применяем такую концепцию подстановки термов, при которой выбор места применения определяется индивидуально. В последующем в выражениях ЯП должно быть целенаправленно установлено, на каком месте выражения ЯП должно быть возможно применение правила. Общая концепция применения ППТ на любом месте была бы неэффективной, так как при известных обстоятельствах благодаря этому упрощались бы термы, значение которых для вычисления результата на самом деле не используется. Однако существенно, что свободное применение правил на любом месте для определенных элементов ЯП приводило бы к незавершающимся вычислениям, тогда как целенаправленное управление применением может гарантировать завершение вычислений. В ЯП обычно встречаются выражения, чье вычисление завершается успешно, т.е. которые имеют значение

, хотя они содержат подвыражения, для которых существуют незавершающиеся вычисления, т.е. значение которых =
. Общая концепция безусловного применения неизбежно ведет для таких выражений к существованию незавершающихся вычислений.

Поэтому мы нуждаемся в ограниченном понятии применения ППТ. Эти правила должны применяться не в любом месте терма, а только при определенных условиях на подтерм. Для этой цели мы будем применять условные ППТ. Благодаря этому достигается более тонкое управление вычислением значения, т.е. выбор места применения правил в аппликативном выражении ЯП. Говорят также об управляемом потоке.

Пример (управляемое вычисление для нестрогих функций). Мы рассматриваем нестрогую функцию соr (условную or), которая соответствует последовательной дизъюнкции с функциональностью

fеt соr = (bool, bool) bool и таблицей значений:

соr       L           О       

L          L           L         L




Содержание  Назад  Вперед