Pw. 2.7. Вычислительная схема _-:

Терм со свободными идентификаторами определяет вычислительную схему. Схемы можно найти (в несколько иной форме) во многих местах в управлении. Например, есть схемы для начисления зарплаты.

Если в терме определенные идентификаторы встречаются многократ­но, то вместо схем типа дерева получают "Наsse"-диаграммь1 (т. е. ацик­лические ориентированные графы).

Пример (схема с многократно применяемым промежуточным резуль­татом). Терм (х - у) * (х + у) обладает схемой, показанной на рис. 2.8.



Рис.2.8. Вычислительная схема

Термы могут использоваться в системах замены термов для представле­ния алгоритмов.

2.3. Алгоритмы как системы подстановки термов

Наиболее наглядный метод описания алгоритмов как системы текстовых замен предлагают системы подстановки термов. Как было показано в предыдущем разделе, имеет место: термы могут строиться над заданной сигнатурой по определенным, четким правилам. К сигнатуре и термам над нею могут быть заданы интерпретации над вычислительной структу­рой, т. е. над алгеброй. Как и в случае булевских термов, возникает ин-4)ормационная система, при которой термы выступают как представле­ния. Через интерпретацию задается семантическая эквивалентность на гермах. Правила преобразования термов могут тогда быть определены так, что термы всегда будут переводиться в семантически эквивалентные термы.

Множества правил для алгоритмов могут быть предъявлены в форме системы подстановки термов. Специальная структура термов, которая получается из их построения, может использоваться для задания правил подстановок и их применения.

2.3.1. Правила подстановки термов

Для заданной сигнатуры  и заданного семейства Х множеств идентификаторов пара (t, r) термов t, r одинакового типа с (свободными) идентификаторами из Х называется подстановкой термов (правилом подстановки термов - ППТ) или также схемой подстановки термов. Правило записывается в виде t  г.

В большинстве случаев для ППТ требуется, чтобы все идентификато­ры, встречающиеся в г, также входили в t. Если в t и г заменяют опреде­ленные идентификаторы Х1, ..., Xn на термы t1, ..., tn подходящих типов, то получают экземпляр (частный, конкретный случаи) правила. Соот­ветственно

t [ t1/X1, ..., tn/Xn ]  r [ t1/X1, .... tn/Xn]

называется экземпляром правила t  г. Если t и г - основные термы, то экземпляр называется полным.

Пример (экземпляры правил подстановок термов). Для правила

pred (succ (x))  х примерами экземпляров являются:

pred (succ (zero))  zero, pred (succ (succ (у)))  succ (у).

Из правила получаются шаги подстановки термов благодаря тому, что правило применяется к любому подтерму имеющегося терма.

Пусть t —> г есть экземпляр правила. Пусть задан терм с, в котором встречается свободный идентификатор х; тогда

С [t/Х]  С [r/Х]

называется (безусловным) применением правила (к. терму c[t/x]). Tepм t называется редексом, а вхождение х в с - местом применения.

Пример (применение правила замены термов). К терму

succ (succ (pred (succ (zero)))) может быть применено правило предыдущего примера. Это дает:

succ (succ (pred (succ (zero)))) —> succ (succ (zero)).

Аналогом алгоритмов в виде подстановки текстов являются алгоритмы в виде систем подстановки термов (алгоритмы подстановки термов - АПТ).

2.3.2. Система подстановки термов

Множество (в общем случае конечное) R правил подстановки термов на сигнатуре  называется системой подстановки термов (СПТ) над . Если для последовательности термов ti (0 <= i <= n) справедливо для i=0,...,n-l:

(*). ti, —> ti+1 есть применение правила из системы подстановки термов R, то последовательность термов является вычислением в R для to.

Терм t называется терминальным для системы R, если не существует герма г такого, что t г

есть применение правила из R.

Если в вычислении, заданном с помощью термов ti 0 <= i <= n, терм tn является терминальным, то вычисление называется терминированным (завершающимся), a tn -результатом или выходом вычисления для входа to.

Бесконечная последовательность (ti)iN термов, удовлетворяющих приведенному выше условию (*), называется нетерминированным (незавершающимся) вычислением R для to. Система R называется в общем случае терминированной, если не существует незавершающихся вычислений.

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

Пример (СПТ для вычислительной структуры BOOL). Ниже символы

функций