- •М. С. Нікітченко теорія програмування Частина 1
- •1. Формалізація простої мови програмування
- •1.1. Неформальний опис простої мови програмування
- •1.2. Формальний опис синтаксису мови sipl
- •1.3. Формальний опис семантики мови sipl
- •1.3.2. Функції
- •1.3.3. Композиції
- •1.3.4. Програмні алгебри
- •1.3.5. Визначення семантичних термів
- •1.3.6. Побудова семантичного терму програми
- •1.3.7. Обчислення значень семантичних термів
- •1.3.8. Загальна схема формалізації мови sipl
- •1.4. Властивості програмної алгебри
- •2. Розвиток основних понять програмування
- •2.1. Аналіз словникових визначень поняття програми
- •2.2. Розвиток поняття програми з гносеологічної точки зору
- •2.3. Розвиток основних понять програмування
- •2.3.1 Початкова тріада понять програмування
- •2.3.2. Тріада прагматичності програм
- •2.3.3. Тріада основних понять програмування
- •2.3.4. Пентада основних понять програмування
- •2.4. Розвиток основних програмних понять
- •2.4.1. Тріада основних програмних понять
- •Малюнок 2.7. Програма як діалектичне заперечення проблеми
- •2.4.2. Пентада основних програмних понять
- •2.5. Сутнісні та семіотичні аспекти програм
- •2.6. Програми і мови
- •2.7. Пентада програмних понять процесного типу
- •3. Формалізація програмних понять
- •3.1. Теоретико-функціональна формалізація
- •3.2. Класи функцій
- •3.3. Програмні системи
- •3.4. Рівні конкретизації програмних систем
- •4. Синтактика: формальні мови та граматики
- •4.1. Розвиток понять формальної мови та породжуючої граматики
- •4.2. Визначення основних понять формальних мов
- •4.3. Операції над формальними мовами
- •4.4. Породжуючі граматики
- •4.5. Приклад породжуючої граматики та її властивості
- •4.6. Ієрархія граматик Хомського
- •4.7. Автоматні формалізми сприйняття мов
- •4.7.1. Машини Тьюрінга
- •4.7.2. Еквівалентність машин Тьюрінга та породжуючих граматик
- •4.7.3. Лінійно-обмежені автомати
- •4.7.4. Магазинні автомати
- •4.7.5. Скінченні автомати
- •4.8. Методи подання синтаксису мов програмування
- •4.8.1. Нормальні форми Бекуса–Наура
- •4.8.2. Модифіковані нормальні форми Бекуса–Наура
- •4.8.3. Синтаксичні діаграми
- •4.9. Властивості контекстно-вільних граматик
- •4.9.1. Видалення несуттєвих символів
- •4.9.2. Видалення -правил
- •4.9.3. Нормальна форма Хомського
- •4.9.4. Нормальна форма Грейбах
- •4.9.5. Рекурсивні нетермінали
- •4.10. Властивості контекстно-вільних мов
- •4.11. Операції над формальними мовами
- •4.12. Дерева виводу
- •4.13. Однозначні та неоднозначні граматики
- •4.14. Розв’язні та нерозв’язні проблеми кв-граматик та мов
- •4.15. Рівняння в алгебрах формальних мов
- •5. Теорія рекурсії (теорія найменшої нерухомої точки)
- •5.1. Рекурсивні визначення та рекурсивні рівняння
- •5.2. Частково впорядковані множини, границі ланцюгів та -області
- •5.3. Неперервні відображення
- •5.4. Теореми про нерухомі точки
- •5.5. Конструювання похідних -областей
- •5.6 Властивості оператора найменшої нерухомої точки
- •5.7. Застосування теорії ннт
- •5.7.1. Уточнення синтаксису мов програмування
- •5.7.2. Семантика мов програмування
- •5.7.3. Рекурсивні розширення мови sipl
1.3.4. Програмні алгебри
Побудовані композиції дозволяють стверджувати, що отримано алгебру функцій (програмну алгебру)
A_Prog =<FNA, FNB, FNAB, FA, FB, FS; Sn, ASx, , IF, WH, x, id>.
Функції іменування x та накладання не включені до переліку операцій цієї алгебри, тому що вони представлені композицією присвоєння. Також не включаємо функції-константи , які мають специфічну природу. Разом із тим до переліку композицій включено функції (нуль-арні композиції) розіменування та тотожна функція. Це пояснюється тим, що вказані нуль-арні композиції мають не предметну (специфічну) природу, а логічну (загальнозначущу), що дозволяє розглядати їх саме як загальні композиції (нехай і нуль-арні), а не як специфічні функції. Втім, цей розподіл є досить умовним.
id
Рисунок 1.4. Алгебра функцій (програмна алгебра)
Наведена алгебра (рис. 1.4) в своїх основах містить багато «зайвих» функцій, які не можуть бути породжені в мові SIPL. Аналіз мови дозволяє стверджувати (цей факт буде доведено пізніше в теоремі 1.1), що функції, які задаються мовою SIPL, породжуються в алгебрі A_Prog з наступних базових функцій:
add, sub, mult FNA;
or, neg FNB;
eq, gr FNAB;
FA (nInt).
Підалгебру алгебри A_Prog, породжену наведеними базовими функціями, назвемо функціональною алгеброю мови SIPL і позначимо A_SIPL.
Зауважимо, що всі функції алгебри A_SIPL є однозначними (детермінованими) функціями. Це випливає з того, що всі базові функції є однозначними, а композиції зберігають цю властивість. Прохання до читача довести цю властивість самостійно.
Формули для обчислення композицій та функцій алгебри A_Prog подамо у наступній таблиці (тут f – n-арна функція, fa, g1,…, gn – номінативні арифметичні функції, fb – номінативний предикат, fs, fs1, fs2 – біномінативні функції, st – стан, n – число).
Таблиця 1.5
Композиція
|
Формула обчислення |
Ім’я формули |
Суперпозиція |
(Sn(f, g1,…, gn))( st)=f(g1(st),…, gn(st)) |
AF_S |
Присвоєння |
ASx (fa)(st)=st [x fa(st)] |
AF_AS |
Послідовне виконання |
fs1fs2(st)=fs2(fs1(st)) |
AF_SEQ |
Умовний оператор |
|
AF_IF |
Цикл |
WH(fb,fs)(st)=stn, де st0=st, st1=fs(st0), st2=fs(st1), …, stn=fs(stn-1), причому fb(st0)=true, fb(st1)=true,…, fb(stn-1)=true, fb(stn)=false. |
AF_WH |
Функція розіменування |
x(st)=st(x) |
AF_DNM |
Тотожна функція |
id(st)=st |
AF_ID |
Зауваження 1.6. Наведені формули слід тлумачити з урахуванням частковості функцій. А саме, якщо значення однієї з функцій, що фігурує у формулі, не є визначеним, то і результат не буде визначеним. Так, для формули fs1fs2(st)=fs2(fs1(st)) вважаємо, що коли fs1(st) або fs2(fs1(st)) не визначені, то і результат не є визначеним.
Для роботи з частковими функціями використовують наступні позначення:
fs(st) – значення fs на st не визначене,
fs(st) – значення fs на st визначене,
fs(st)=r –значення fs на st визначене і дорівнює r.
З урахуванням частковості, формулу для послідовного виконання можна записати у наступному вигляді:
fs1fs2(st)=
Формула для умовного оператора буде мати вигляд
Інші формули можуть бути переписані аналогічним чином. Наведений вигляд формули зберігають і у випадку багатозначних (недетермінованих) функцій. Правда, тут такі функції розглядати не будемо.
Зазначимо, що наведені формули можна було б записувати із вживанням сильної рівності, яка задає невизначеність лівої частини при невизначеності правої.■
Побудована алгебра A_SIPL дозволяє тепер формалізувати семантику програм мови SIPL, задаючи їх функціональними виразами (семантичними термами) алгебри A_SIPL.