Языки программирования. Практический сравнительный анализ



Языки программирования. Практический сравнительный анализ - стр. 76


Другими словами, равенство, которое написано справа от знака "->->", выполнено для класса объектов, удовлетворяющих условию, выписанному слева от "->->" (т.е. для пар с непустой первой компонентой).

Доказательство. Идея : слева и справа от знака равенства получается тот же результат для любого объекта из выделяемого условием класса.

Случай 1. x - атом или <?> .

          distr : (x,y) = <?>.         (см. опр distr)

          t1 * 1 : (x,y) = <?>.        (опр t1).

И так как все функции сохраняют <?>, получаем утверждение теоремы.

Случай 2. х = <x1, ... ,xn>   (т.е. x - кортеж). Тогда

       appendl * ((1 * 1,2),distr * (t1 * 1,2)) : <x,y> =

         = appendl:<<1:x,y>, distr:<t1:x,y>> =

Если t1:x = <>  [<> обозначает "пусто"], то

         = appendl:<<x1,y>,<>> = <<x1,y>> = distr:<x,y> .

Если t1:x /= <>, то

         = appendl:<<x1,y>,<<x2,y>, ... ,<xn,y>>> =

         = distr:<x,y>.

Что и требовалось доказать.

2.5.2. Эквивалентность двух программ перемножения матриц

Наша ближайшая цель - продемонстрировать применение алгебры программ для доказательства эквивалентности двух нетривиальных программ. Одна из них - программа ММ, при создании которой мы совершенно игнорировали проблему эффективности (в частности, расхода памяти исполнителя). Вторая - программа MMR, которую мы создадим для решения той же задачи (перемножения матриц), но позаботимся теперь о рациональном использовании памяти исполнителя. Естественно, MMR получится более запутанной. Уверенность в ее правильности (корректности) будет, конечно, более высокой, если удастся доказать ее эквивалентность ММ, при создании которой именно правильность (концептуальная ясность) и была основной целью.

Естественно считать ММ точной формальной спецификацией задачи перемножения матриц (т.е. определением функции "перемножение матриц").


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