Редукційне програмування функцій, заданих операціями підсумовування

Як відомо, функції, які задані операціями підсумовування

, (1)

де – довільна функція дійсних змінних та натуральної змінної , досить поширені у чисельному аналізі.

З метою композиційного конструювання коректних програм обчислення цих функцій введемо до розгляду іменні функції, які використовуються у процесі програмування. Нехай

– D -іменна -функція, яка іменній множині зіставляє значення ;

– D -іменна -функція, яка іменній множині зіставляє значення ;

- D -іменний предикат, який іменній множині зіставляє значення . Використовуючи ці функції, можна сконструювати коректні програми обчислення (1). Покажемо, що має місце таке твердження.

Теорема 1. Для обчислення функції (1) в елементарній програмній логіці виводиться коректна програма з оракулами (схема програм), що має вигляд

І:= 0; S:= ;

while do (I:=I+ 1; S:=S+ ) (2)

Доведення теореми проведемо шляхом безпосередньої побудови методом редукцій виводу в елементарній програмній логіці програми з оракулами (2), користуючись композиційною технологією програмування.

За характеристичну візьмемо таку властивість функції (1): її значення збігається із значенням такого члена першої із системи двох послідовностей, визначеної системою двох рекурентних співвідношень першого порядку

(3)

при j> 0 та початкових значеннях , для якого предикат приймає значення false коли , значення true, коли .

Згідно до композиційної технології програмування, знайдемо спочатку функціональну структуру програми. Аналіз характеристичної властивості функції (1) показує, що функціональною структурою може бути (D,W)-іменна функція , яка іменній множині зіставляє іменну множину , де

таку, що іменний предикат іменній множині зіставляє false, коли , та значення true, коли .

Композиційна структура програми, в розробленні якої полягає другий етап композиційного програмування, здобувається розкладанням функції, яка задає функціональну структуру програми, на більш прості функції за допомогою відповідних композицій. За останні оберемо композиції структурного програмування, до яких належать аплікація, розгалуження та циклування.

Щоб розкласти функцію F, яка задає функціональну структуру програми, за допомогою обраних композицій, продовжимо аналіз характеристичної властивості функції (1). Неважко зрозуміти, що при розкладанні функції F має бути використана композиція типу циклування, наприклад, while_do. Але застосувати цю ком позицію зразу на першому етапі розкладання функції F неможливе, бо знайти редукцію цієї функції природним шляхом не вдається. Тут під редукцією іменної функції F слід розуміти таку іменну функцію G для якої G;F=F, де «;» позначає композицію аплікації. Тому спробуємо, як це завжди роблять у таких випадках, розкласти спочатку функцію F, використовуючи композицію аплікації. З цією метою розглянемо функцію , де , такий член послідовності, а , , що предикат приймає значення false, коли та значення true, коли . Ця послідовність є першою в системі двох послідовностей, визначеній системою двох рекурентних співвідношень першого порядку

(4)

для та початковими значеннями .

Легко побачити, що при та система послідовностей, яка визначається системою рекурентних співвідношень (4), збігається з системою послідовностей, яка визначається системою рекурентних співвідношень (3) при вказаних початкових значеннях. Отже, при та для будь-яких припустимих значень значення функції збігається зі значенням функції :

= .

Введемо до розгляду (D,W)-іменну функцію , яка іменній множині

(5)

зіставляє іменну множину

, (6)

Тоді, зважаючи на сказане раніше, функцію F можна записати у вигляді:

(7)

Якщо для функції знайдеться редукція , то вона може бути представлена у вигляді: while P do , де Р – придатний предикат.

Покажемо, що (D,W)-іменна функція

, є редукцією функції . Для цього пересвідчимось, що виконується визначальна властивість редукції: .

Нехай задана іменна множина (5). Її образ відносно функції є

. (8)

Але згідно з означенням функції ,

Отже іменна множина (8), на яку функцією перетворюються іменна множина (5), збігається з іменною множиною (6), на яку та ж сама множина (5) перетворюється функцією

Таким чином, функція дійсно є редукцією функції . Тоді останню можна зобразити у вигляді:

while P do

Легко зрозуміти, що за Р можна обрати предикат . Це випливає з характеристичної властивості функції .

Беручи до уваги, що функція F, яка нас цікавить, зображувана у вигляді (7), можна зробити останній крок її розкладання, здобувши композиційну структуру цієї функції

while do ( ).

Ця композиційна структура, очевидно, являє собою програму з оракулами (2), що обчислює функцію (1). Безпосередньо з побудови програми випливає її коректність. Теорему доведено.

Нехай – D -іменна -функція, яка іменній множині зіставляє значення ;

Тоді аналогічно теоремі 1 доводиться наступне твердження.

Теорема 2. Для обчислення функції

, де ,

в елементарній програмній логіці виводиться коректна програма з оракулами (схема програм), що має вигляд

while do ()

Нехай функція визначається рівністю

(9)

де та – такі функції дшйсних аргументів та натуральних значень, що для всіх .

Нехай далі , та D -іменні -функції, які іменній множині зіставляють значення , та відповідно.

Нехай нарешті, - D -іменний предикат, який іменній множині зіставляє значення . Тоді має місце таке твердження.

Теорема 3. Для обчислення функції, яка визначається рівністю (9) в елементарній програмній логіці виводиться коректна програма оракулами (схема програм), що має такий вигляд

; ;

while do .

Доведення теореми аналогічно доведенню теореми 1. Характерною особливістю програм, наведених у теоремах 1-3, є відносність, яка проявляється у входженні до них іменних функцій , , , , які відповідають функціям , ,
, , та . Тому вони являють собою не конкретні програми, а програми з оракулами (схеми програм). Конкретні програми дістаються з цих схем замінами вказаних відносних функцій конкретними функціями.

Таким чином, теореми 1-3 дозволяють діставати коректні програми обчислення різних скінчених сум шляхом заміни схем програм довільних функцій, що до неї входять, відповідними конкретними функціями. Здобуті при цьому програми є коректні за способом своєї побудови. Так, наприклад, сконструйовану вище програму обчислення суми можна дістати зі схеми програм теореми 2, поклавши в ній . Цим самим гарантується коректність цієї програми.

Перейдемо тепер до розгляду питання композиційного конструювання методом редукцій коректних схем програм обчислення функцій, заданих операціями мультиплікування.