Языки логического программирования

Модель Бэкуса алгебры программ: алгебра программ

Показывать лекцию целиком

Алгебра программ

Простота форм модели Бэкуса, заключающаяся в их регулярности и свободе от контекста, способствует построению системы регулярных преобразований, сохраняющих смысл программ, и потому названа Бэкусом алгеброй программ. Область значений этой алгебры - класс функций в модели Бэкуса, а операциями алгебры являются формы. Например, f*(g*h) есть формула в алгебре программ, а результат "вычисления" этого выражения зависит от значений переменных f,\ g,\ h. При их интерпретации это вполне определенные функции. Например, при интерпретации f -> id, g -> id, h -> id

f*(g*h) = id.

В алгебре программ с программами-выражениями можно обращаться так же, как в обычной алгебре - с формулами, уравнениями, неравенствами. И этим умением можно упрощать программы, доказывать их эквивалентность (значит, и корректность).

Основой алгебры программ является серия законов. Например,

(f, g)*h = ((f*h), (g*h)).

К законам можно относиться как к аксиомам и теоремам. Будем относиться к нижеследующим 6 законам как к аксиомам.

  • (f1,..., fn)*g = (f1*g,..., fn*g)
  • Af*(g1,..., gn) = (f*g1,..., f*gn)
  • /f*(g1,..., gn) = f*(g1, /f*(g2,..., gn) (n >= 2), /f*g = g
  • (f1*1,..., fn*n)*(g1,..., gn) = (f1*g1,..., fn*gn)
  • appendl*(f*g, Af*h) = Af*appendl*(g, h)
  • A(f*g) = Af*Ag
    •

    Для обоснования той или иной аксиомы достаточно показать, что применение к любым данным формы в левой части равенства совпадает с применением к этим же данным формы в правой части равенства. Обоснуем для примера аксиому 1o. Для любых данных x (атом, неопределенность <?> или непустой кортеж):

    (f1,..., fn)*g : x =(f1,..., fn) : (g : x) =
  = <f1 : (g : x),..., fn : (g : x)> = <f1*g : x,..., fn*g : x> =

    = (f_1*g,..., f_n*g) : x, что и требовалось. Обоснования остальных аксиом мы оставляем читателю.

    В формулировках теорем принято продукцию обозначать двойной стрелкой ( $$\Rightarrow$$ ). Приведем и докажем теорему, которая нам потребуется в дальнейшем.

    Теорема 1.

    pair  not*null*1 => appendl*((1*1, 2), distr*(t1*1, 2)) = distr

    Условие теоремы читается так:

    Верно следующее равенство форм для любых аргументов, представляющих собой кортеж из 2 элементов с первым непустым элементом:

    appendl*((1*1, 2), distr*(t1*1, 2)) = distr.

    Доказательство.

    Рассмотрим 2 случая:

  • 1-й элемент кортежа-аргумента x - атом или неопределенность <?>.
  • 1-й элемент кортежа-аргумента x - любой непустой кортеж.
    •

  • distr : <x, y> = <?> (из определения функции distr ).

    t1*1:<x, y> =<?> (из определения функции distr ).

    Поэтому и правая, и левая форма равенства дают неопределенность <?>.

  • x=<x1,..., xn> (n >= 1).
appendl*((1*1, 2), distr*(t1*1, 2)) : <x, y> =
= appendl*((1*1, 2):<x, y>, distr*(t1*1, 2):<x, y>) =
= appendl*<<1:x, y>, distr:<t1:x, y>>) =

    2a) Если t1:x = <>, то

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

    2b) Если $$t1:x \ne <>$$, то

    = appendl:<<x1, y>, <<x2, y>,..., <xn, y>>> =
= distr:<x, y>.
    •

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

    Рассмотрим теперь пример построения программы умножения матриц и преобразования этой программы с целью ее улучшения.

    Упражнения

  • Обоснуйте все аксиомы алгебры программ.
  • Является ли верным следующее утверждение: revers*revers=id, где revers - функция, определенная в упражнении 4.8.1?
    •
    Предыдущее занятие Следующее занятие
    Вернуться к учебному плану
    ^