Стабільність та монотонність програм щодо структурних трансформацій даних
Розглядається проблема поведінки програм щодо структурних трансформацій вхідних даних. Проведено уточнення проблеми та її
 формалізацію в рамках композиційно-номінативного підходу. Досліджено введені поняття та побудовано мову програм, які мають
 стабільну та монотонну поведінку при...
Saved in:
| Date: | 2010 |
|---|---|
| Main Authors: | , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут програмних систем НАН України
2010
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/14636 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Стабільність та монотонність програм щодо структурних трансформацій даних/ М.С. Нікітченко, Є.В. Іванов// Пробл. програмув. — 2010. — № 2-3. — С. 58-67. — Бібліогр.: 2 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860128463746236416 |
|---|---|
| author | Нікітченко, М.С. Іванов, Є.В. |
| author_facet | Нікітченко, М.С. Іванов, Є.В. |
| citation_txt | Стабільність та монотонність програм щодо структурних трансформацій даних/ М.С. Нікітченко, Є.В. Іванов// Пробл. програмув. — 2010. — № 2-3. — С. 58-67. — Бібліогр.: 2 назв. — укр. |
| collection | DSpace DC |
| description | Розглядається проблема поведінки програм щодо структурних трансформацій вхідних даних. Проведено уточнення проблеми та її
формалізацію в рамках композиційно-номінативного підходу. Досліджено введені поняття та побудовано мову програм, які мають
стабільну та монотонну поведінку при зміні структури вхідних даних.
In the article the problem of program behavior with respect to structure transformations of input data is considered. An explication and
formalization of the problem in the framework of composition-nominative approach is given. Defined notions are studied and a language of
programs having stable and monotone behavior under structure transformations is constructed.
|
| first_indexed | 2025-12-07T17:43:52Z |
| format | Article |
| fulltext |
Теоретичні та методологічні основи програмування
© М.С. Нікітченко, Є.В. Іванов, 2010
58 ISSN 1727-4907. Проблеми програмування. 2010. № 2–3. Спеціальний випуск
УДК 004.4
СТАБІЛЬНІСТЬ ТА МОНОТОННІСТЬ ПРОГРАМ
ЩОДО СТРУКТУРНИХ ТРАНСФОРМАЦІЙ ДАНИХ
М.С. Нікітченко, Є.В. Іванов
Київський національний університет імені Тараса Шевченка,
01033, Київ, вул. Володимирська, 64,
e-mail: nikitchenko@unicyb.kiev.ua, ivanov.eugen@gmail.com
Розглядається проблема поведінки програм щодо структурних трансформацій вхідних даних. Проведено уточнення проблеми та її
формалізацію в рамках композиційно-номінативного підходу. Досліджено введені поняття та побудовано мову програм, які мають
стабільну та монотонну поведінку при зміні структури вхідних даних.
In the article the problem of program behavior with respect to structure transformations of input data is considered. An explication and
formalization of the problem in the framework of composition-nominative approach is given. Defined notions are studied and a language of
programs having stable and monotone behavior under structure transformations is constructed.
Вступ
Багато мов програмування мають вбудовані операції для роботи з ієрархічними структурами даних. Такі
дані зазвичай можуть розглядатися як певні види дерев з вершинами та / або ребрами розміченими значеннями.
Часто виконання операцій суттєво залежить від характеру ієрархії (плоска, розгалужена і т. п.) даного, до якого
вони застосовані. Ця обставина відбивається на програмуванні: наприклад, програма, яка розрахована на роботу
з даними з плоскою ієрархією, може бути не придатною для роботи із даними з розгалуженою ієрархією,
і навпаки. Тому програміст має враховувати різні можливі варіанти ієрархії даних і не покладатися на те, що
обробка даних з різною ієрархією буде відбуватися потрібним для нього чином.
У деяких мовах програмування присутні засоби, що дозволяють працювати із певними класами даних, не
піклуючись про характер ієрархії в них. Для таких мов будемо казати, що програми цих мов мають стабільну
поведінку при зміні ієрархії (структури) даних. Наприклад, у мові програмування Pascal багатовимірні масиви
можуть бути описані різними способами, і кожному способу опису відповідає своя ієрархія. Так, двовимірний
масив можна описати або як матрицю (A: array [1..n, 1..m] of real), або як масив масивів (A: array [1..n] of array
[1..m] of real). За першим способом опису можна вважати, що масив є ієрархією з двома рівнями (зверху вниз):
“пара індексів”–“значення”. За другим – можна вважати, що масив є ієрархією з трьома рівнями: “перший
індекс”–“другий індекс”–“значення”. Для того, щоб звернутися до елемента масиву із заданими індексами,
необхідно пройти вниз за відповідною ієрархією. При цьому, незалежно від способу опису двовимірного
масиву, у мові Pascal дозволяється звертатися до його елементів як за нотацією A[i,j], що відповідає плоскій
ієрархії, так і за нотацією A[i][j], що відповідає розгалуженій ієрархії. Аналогічна ситуація має місце для
довільних багатовимірних масивів. Тобто програміст має можливість писати програми обробки масивів, не
піклуючись про спосіб, у який вони описані. При цьому масиви як матриці і масиви масивів можуть подаватися
в оперативній пам’яті різними структурами (це залежить від компілятора). Зауважимо, що в мовах
програмування, таких як C, C++, C# немає можливостей, аналогічних вищеописаним для мови Pascal.
Незважаючи на те, що деякі практичні мови програмування забезпечують властивість стабільності (або,
можливо, обмеженої стабільності) при структурних трансформаціях даних, теорія таких мов програмування не
є достатньо розвиненою. Дана робота має на меті зробити певний крок у розбудові зазначеної теорії. Для цього
необхідно надати формальні визначення понять ієрархічних даних, програм над ієрархічними даними,
стабільності програм при зміні ієрархії даних, побудувати і дослідити мови програм, що забезпечують їх
стабільність. Такі дослідження будемо здійснювати в рамках композиційно-номінативного підходу до
програмування [1], який надає достатньо розвинені можливості для формалізації необхідних понять.
У попередній роботі авторів над цією тематикою [2] було побудовано функціонально повну і структурно
адекватну формальну мову програм, що забезпечує їх стабільність при зміні ієрархій даних – так звану мову
SICONa (просту композиційно-номінативну мову програм з асоціативним розіменуванням). У даній роботі
досліджуються мови програм, що забезпечують більш сильну властивість, ніж стабільність, а саме –
монотонність. Змістовно, монотонність програми означає, що вона стабільна, і при розширенні вхідного даного
вихідне дане не зменшується.
Надалі будемо використовувати такі позначення:
V – множина не порожніх слів в алфавіті V ;
*( ) { | }pref u v V w V u vw – множина не порожніх префіксів слова u V ;
u v ( u v ) – слово u є префіксом (власним префіксом) слова v ;
( )f x – функція f визначена на аргументі x ;
Теоретичні та методологічні основи програмування
59
( )f x – функція f не визначена на аргументі x ;
( ) ( )f x g y – сильна рівність ( ( )f x тоді і тільки тоді, коли ( )g y , і тоді ( ) ( )f x g y );
A nB – клас (часткових) функцій з A в B , що мають скінченний графік;
)arg( f – область визначеності функції або бінарного відношення;
Af | – звуження області визначеності функції або бінарного відношення на множину A.
1. Номінативні та складноіменні дані
Для того, щоб формально визначати мови програм, будемо використовувати композиційно-номінативний
підхід [1] до визначення понять програмування. Згідно цього підходу, дані уточнюються як певні різновиди
номінативних даних (від лат. nomen – ім’я), які, неформально, є ієрархічно побудованими об’єктами на основі
відношення ім’я значення, а програми уточнюються як функції над номінативними даними, що можуть бути
отримані з базових функцій застосуванням композицій (тобто операцій над функціями). Таким чином,
розглядаючи множину функцій як носій, а композиції – як операції, отримуємо алгебру функцій (програм).
Мова програм визначається класом номінативних даних, над якими діють програми, і складом базових функцій
і композицій.
Як вищезазначено, номінативні дані є ієрархічними об’єктами. Їх можна подавати графічно у вигляді
орієнтованих дерев із дугами, розміченими іменами, і листками, розміченими значеннями, або за допомогою
текстового запису. Наприклад, запис ]]2[,1[ cba означає, що дане має дві компоненти з іменами a
і b , значення першої з яких атомарне, а значення другої саме є номінативним даним. Зауважимо, що у вигляді
номінативних даних може бути подано багато видів структур даних, у тому числі записи, файли, масиви,
реляції, бази даних тощо.
Формально, номінативні дані визначаються індуктивно на основі множини імен V та класу базових
значень (атомів) W таким чином:
0( , ) { }ND V W W – клас номінативних даних рангу нуль,
1( , ) ( , )n
k kND V W W V ND V W для 0k – клас номінативних даних рангу не більше 1k .
Тоді
0
( , ) ( , )kk
ND V W ND V W
– клас усіх номінативних даних. Класи номінативних даних різного
рангу утворюють ланцюг: ...),(),(),( 210 WVNDWVNDWVND
Згідно визначення, номінативні дані, що не є атомами (неатомарні дані), є частковими функціями на V.
При необхідності ми будемо також їх трактувати як бінарні відношення і використовувати теоретико-множинні
операції над ними.
Основними операціями над номінативними даними є унарні параметричні операції іменування і
розіменування, і бінарна операція накладання. Позначимо літерою d номінативне дане.
Іменування v з параметром v V визначається рівністю ][)( dvdv . Тобто ця операція
створює дане, у якому v (параметр операції) іменує значення d (аргумент операції).
Розіменування v з параметром v V визначається рівністю )()( vddv . Тобто ця операція
знаходить у даному d компонент з ім’ям v , що є параметром операції.
Накладання визначене тільки на неатомарних даних і задається рівністю
)arg(\)arg(1221 21
| dddddd . Тобто ця операція створює дане, в якому присутні всі компоненти другого
аргументу й ті компоненти першого, які не були перевизначені в другому.
Номінативні дані класу ),( WVND засновані на неструктурованих (простих) іменах. Проте для цілей
даної роботи необхідний клас номінативних даних, в якому можливі еквівалентні структурні перетворення,
тобто такі перетворення даного, при яких його інтуїтивний зміст залишається, а характер ієрархії імен може
змінюватися. Щоб забезпечити таку можливість, ведемо спеціальний клас номінативних даних зі складними
іменами, які задаються як конкатенації простих імен. А саме, класом даних зі складними іменами називається
клас ),(),( WVNDWVNDV .
Для деяких даних цього класу не виконується принцип однозначності структурного іменування (ОСІ).
Наприклад, у даному ]]2[,1[ yxxy доцільно вважати, що складному імені xy відповідає два значення:
1 і 2. Ми будемо розглядати підклас ),( WVNDV , для даних якого виконується принцип ОСІ. Цей підклас
назвемо класом складноіменних даних та позначимо його як ( , )NDVC V W . Перед тим, як надати формальне
визначення ( , )NDVC V W , введемо низку допоміжних визначень та позначень, в яких ),( WVNDVd :
іменний шлях в d – це послідовність імен 1 2( , ,.., )kv v v з V
+
( 1k ), така, що визначено значення
1 2( , ,.., )kd v v v шляху в d, яке задається рівністю 1 2 1 2( , ,.., ) (...(( ( ))( ))...( ))k kd v v v d v v v ; шлях називається
термінальним в d, якщо його значенням в d є дане рангу 0 (в дереві, що відповідає даному d,
термінальний шлях веде від кореня до листа дерева);
Теоретичні та методологічні основи програмування
60
( ) { | ( ) }rn d u d u – множина кореневих імен d;
( ) { | ( ) }ra d u d u W – множина атомних кореневих імен d;
0( ) { ( ) | ( ) }rn d u rn d d u W – множина неатомних кореневих імен d;
))}((|{)(0 drnuvVvVudrp – слова, які є власними префіксами кореневих імен d;
*
0( ) ( ) ( )rs d rp d rn d V – слова, які порівнюються з деяким кореневим іменем d;
операція ділення даного d на ім’я u V задається формулою
1 1 1/ [ ( ) | ( ( ) )]d u v d v v V v rn d v uv .
Формальне визначення класу складноіменних даних подається таким чином:
( , ) ( , )NDVC V W W G V W , де ( , )G V W – дані ( , ) \d NDV V W W такі, що має місце властивість: якщо для
двох деяких шляхів
1 2( , ,.., )nv v v та
1 2( , ,.., )mv v v в d виконується співвідношення 1 2 1 2... ( ... ),n mv v v pref v v v
то n m і
i iv v для всіх {1,2,.., }i n . Позначимо ( , ) ( , ) ( , )k kNDVC V W NDVC V W ND V W – дані класу
( , )NDVC V W рангу не більше k .
Змістовно, до класу ( , )NDVC V W належать дані зі складними іменами, для яких в дереві, яке відповідає
даному, немає двох шляхів від кореня (один з яких не є початком іншого), таких, що конкатенація імен вздовж
одного шляху є префіксом конкатенації імен вздовж іншого шляху. Для цих даних виконується принцип ОСІ.
Домовимося, що надалі літерою d (можливо з індексами) будуть позначатися дані класу ( , )NDVC V W ,
якщо явно не вказано інше.
Основними операціями над складноіменними даними є операція іменування, вищевизначена для
довільних номінативних даних, унарна параметрична операція асоціативного розіменування і бінарна операція
структурного накладання. Зауважимо, що іменування, застосоване до складноіменного даного, дає
складноіменне дане.
Операція асоціативного розіменування av з параметром v V аналогічна звичайному
розіменуванню, вищевведеному, але враховує складеність імен. Формально вона визначається індуктивно за
довжиною слова-параметра таким чином:
база індукції. Якщо 1v , то
( ) ( )av d d v , якщо ( )v rn d ;
( ) /av d d v , якщо ( )v rn d і /d v ;
( )av d , якщо ( )v rn d і /d v .
Індукційний перехід. Якщо 2v n , то 1( ) ( ( ))a a av d v x d для кожного ( , )d NDVC V W ,
де x V і 1
1
nv V – такі слова, що 1v xv .
Наведемо приклад дії операції асоціативного розіменування: 1])2],1[([)( yyxxy a
(тут вважається, що W}2,1{ і Vyx },{ ).
Назва операції av походить від наступної її властивості: 1 2( ) ( (..( ( )..))a a a n av d v v v d
для довільного даного ( , )d NDVC V W і довільного розкладу 1 2 1..n nv v v v v складного імені v V
на імена
1 2, ,.., nv v v V .
Операція структурного накладання також аналогічна накладанню, вищевведеному, але враховує
складеність імен. На прикладах вона діє таким чином:
],[][][ 2121 dydxdydx s , Vyx , , yx ;
][][][ 221 dxdxdxy s , тобто значення під іменем x перевизначає значення під іменами, що
є продовженнями x ;
])][([][][ 2121 dydxdxydx ss (при Wd 1 ), тобто значення під іменем xy модифікує
значення під іменем x .
Формальне визначення структурного накладання подамо індуктивно за рангом першого аргументу. Якщо
1 0( , )d NDVC V W , то
1 2 2sd d d , якщо 1d і 2 ( , ) \d NDVC V W W ;
1 2sd d , якщо 1d W або 2d W .
Індукційний перехід. Припустимо, що значення 1 2sd d вже визначено для всіх 1 2,d d , таких, що
1 ( , )kd NDVC V W . Нехай 1 1( , ) \ ( , )k kd NDVC V W NDVC V W .
Теоретичні та методологічні основи програмування
61
Тоді покладемо
1 2sd d d , де дане d визначено таким чином:
1)
2( ) ( )d u d u , якщо u є кореневим іменем в
2d і не має власного префікса, який би був кореневим
іменем в
1d , тобто
2 1( ) \ ( )u rn d rn d V ;
2)
1 2( ) ( ) ( / )sd u d u d u , якщо u є неатомним кореневим іменем в
1d і власним префіксом кореневого
імені в
2d , тобто
0 1 0 2( ) ( )u rn d rp d ;
3)
2( ) /d u d u , якщо u є атомним кореневим іменем в
1d і власним префіксом кореневого імені в
2d ,
тобто
1 0 2( ) ( )u ra d rp d ;
4)
1( ) ( )d u d u , якщо u є кореневим іменем в
1d і не порівнюється з жодним кореневим іменем з
2d ,
тобто
1 2( ) \ ( )u rn d rs d ;
5) ( )d u , в інших випадках, тобто якщо
1 2( ) ( )u rn d rn d або
1 2( ) ( )u rn d rn d V або
2 1( ) ( )u rn d rn d V .
В подальшому буде потрібна наступна лема, яку наводимо без доведення.
Лема 1 (властивості структурного накладання). Нехай
1 2sd d і u V . Тоді:
1) якщо
2( ) { }au d W , то
1 2 2( ) ( )a s au d d u d , тобто структурне накладання зберігає
атомарні значення імен з другого аргументу;
2) якщо
1 2( ) { }a su d d W і
2( )au d , то
1 1 2( ) ( )a a su d u d d , тобто структурне
накладання не створює зайвих (не пов’язаних з жодним з аргументів) атомарних значень;
3) якщо
2( )ax d , де x – перша літера u , то 1 2 1( ) ( )a s au d d u d , тобто структурне накладання
зберігає значення імен першого аргументу, що не мають спільного префікса з іменами другого.
2. Властивості складноіменних даних
Як зазначалося раніше, до даних класу ( , )NDVC V W можуть бути застосовані еквівалентні
перетворення, що зберігають їх інтуїтивний зміст, але змінюють характер ієрархії. Щоб формально визначити
цю властивість, введемо відповідне відношення еквівалентності на ( , )NDVC V W – відношення номінативної
еквівалентності. Для формального визначення номінативної еквівалентності, попередньо введемо на
( , )NDVC V W бінарне відношення номінативного включення таким чином:
якщо 1d W або
2d W , то 1 2d d тоді і тільки тоді, коли 1 2d d ;
якщо 1d W і
2d W , то 1 2d d тоді і тільки тоді, коли для кожного термінального шляху
1 2( , ,.., )kv v v в 1d існує термінальний шлях 1 2( , ,.., )lv v v в 2d , такий, що 1 2 1 2.. ..k lv v v v v v і
1 1 2 2 1 2( , ,.., ) ( , ,.., )k ld v v v d v v v .
З цього визначення випливає, що для відношення номінативного включення множина конкатенацій імен
на всіх термінальних шляхах першого даного має входити у таку ж множину другого даного, крім того і
відповідні значення мають співпадати. Легко переконатися, що відношення є передпорядком.
Номінативну еквівалентність складноіменних даних визначимо як бінарне відношення на
( , )NDVC V W , таке, що 1d 2d тоді і тільки тоді, коли 1 2d d і 2 1d d . Відношення є еквівалентністю.
На основі номінативної еквівалентності можна визначити поняття стабільності програми при зміні
ієрархії даних таким чином: програма (як функція над складноіменними даними) є (номінативно) стабільною,
якщо вона на номінативно еквівалентних вхідних даних дає номінативно еквівалентні результати (причому на
кожній парі еквівалентних даних вона визначена або не визначена одночасно). В частковому випадку, коли
результатами програми є атомарні дані, на номінативно еквівалентних даних номінативно стабільна програма
дає однакові результати.
У роботі [2] було побудовано формальну мову програм, які є номінативно стабільними. Далі побудуємо
мову програм, які задовольняють більш сильній умові – монотонності. Для цього необхідно визначити
відношення на даних, в сенсі якого програми мають бути монотонними. Таким відношенням оберемо
відношення слабкого номінативного включення, що формально визначено далі.
Введемо на ( , )NDVC V W допоміжне бінарне відношення A , вважаючи, що
якщо 1d W або 2d W , то 1 2Ad d тоді і тільки тоді, коли 1 2d d ;
якщо 1d W і 2d W , то 1 2Ad d тоді і тільки тоді, коли для кожного термінального шляху
1 2( , ,.., )kv v v в 1d , що закінчується атомом, існує термінальний шлях 1 2( , ,.., )lv v v в 2d , такий, що
1 2 1 2.. ..k lv v v v v v і 1 1 2 2 1 2( , ,.., ) ( , ,.., )k ld v v v d v v v .
Введемо на ( , )NDVC V W допоміжне бінарне відношення N , вважаючи, що
якщо 1d W або 2d W , то 1 2Nd d тоді і тільки тоді, коли 1 2d d ;
Теоретичні та методологічні основи програмування
62
якщо
1d W і
2d W , то
1 2Nd d тоді і тільки тоді, коли для всіх u V , таких, що
1( )au d W ,
виконується
2( )au d W .
Тоді введемо на ( , )NDVC V W бінарне відношення слабкого номінативного включення таким чином:
w A N . Назва відношення
w
пов’язана з тим, що відношення включається у
w
. Відмінність від
w
проявляється в тих випадках, коли значенням термінального шляху в
1d є порожнє номінативне дане, бо
тоді для відношення цей шлях в
2d також має давати порожнє дане, а для
w
такий шлях в
2d може мати
своїм значенням довільне неатомарне дане. Тобто
w
дозволяє “розширювати” порожні дані іменованими
компонентами. Наприклад, ]2,1[][ xzxyx w і ]]2,1[[][ zyxx w , але
]2,1[][ xzxyx і ]]2,1[[][ zyxx .
Лема 2. Відношення
w
є передпорядком і включає передпорядок .
Доведення цієї леми легко отримується з означення відношень, тому тут не наводиться.
3. Монотонність операцій над складноіменними даними
Встановимо монотонність операцій над складноіменними даними за відношенням передпорядку
w
.
Функції, монотонні за відношенням
w
, будемо називати номінативно монотонними.
Наведемо дві допоміжні леми без доведень.
Лема 3 (критерій відношення ). Нехай
1 2, ( , ) \d d NDVC V W W . Тоді
1 2d d тоді і тільки тоді, коли
для всіх u V , таких, що
1( ) { }au d W , виконується
2 1( ) ( )a au d u d .
Лема 4 (критерій відношення A ). Нехай 1 2, ( , ) \d d NDVC V W W . Тоді 1 2Ad d тоді і тільки тоді, коли
для всіх u V , таких, що
1( )au d W , виконується
2 1( ) ( )a au d u d .
Тепер сформулюємо властивості операцій.
Лема 5 (монотонність іменування, слабка монотонність асоціативного розіменування і ділення відносно
A
). Нехай v V . Тоді
1) якщо
1 2Ad d , то 1 2( ) ( )Av d v d ;
2) якщо 1 2Ad d ,
1( )av d і
2( )av d , то 1( )av d A 2( )av d ;
3) якщо
1 2Ad d і
2 /d v , то
1 2/ /Ad v d v .
Доведення.
1) нехай
1 2Ad d і v V . Позначимо ( ) [ ]i i ie v d v d , 1,2i . Якщо хоч одне з
1d ,
2d належить
W , то 1 2d d , тому 1 2( ) ( )Av d v d . Розглянемо випадок, коли 1d W і 2d W . Нехай 1( ,.., )nv v –
термінальний шлях в 1e , що закінчується атомом. Тоді 1v v . Оскільки 1d W , то 1n . Тоді 2( ,.., )nv v –
термінальний шлях в 1d і оскільки 1 2Ad d , то існує термінальний шлях 2( ,.., )mv v в 2d , такий, що
mn vvvv .... 22 і 2 2 1 2( ,.., ) ( ,.., )m nd v v d v v . Тоді 2( , ,.., )mv v v є термінальним шляхом в 2e і
2 2 1 2( , ,.., ) ( , ,.., )m ne v v v e v v v . Отже 1 2Ae e , тобто 1 2( ) ( )Av d v d ;
2) нехай
1 2Ad d ,
1( )av d і
2( )av d . Нехай u V і
1( ( ))a au v d W .
Тоді
1( ) ( )avu d W . Оскільки
1 2Ad d , то
2 1( ) ( ) ( ) ( )a avu d vu d за лемою 4.
Тоді
2 1( ( )) ( ( ))a a a au v d u v d . Отже 1 2( ) ( )a A av d v d за лемою 4 в силу довільності u ;
3) Нехай 1 2Ad d і 2 /d v . Тоді 1 2,d d W . Нехай 1( ,.., )nv v – термінальний шлях в 1 /d v , що
закінчується атомом. Тоді 1( ,.., )nvv v – термінальний шлях в 1d , що закінчується атомом і оскільки 1 2Ad d , то
існує термінальний шлях 1( ,.., )mv v в 2d , такий, що 1 1.. ..n mvv v v v і 1 1 2 1( ,.., ) ( ,.., )n md vv v d v v . Припустимо, що
1v v . Оскільки 1 2( )v rn d , то в 2( )rn d не існує імені, яке є продовженням v , тому 2 /d v , що суперечить
припущенню 2 /d v . Таким чином, відношення 1v v не виконується, а тому 1v v . Тоді існує слово 1v ,
таке, що 1 1vv v і )..,,( 21 mvvv є термінальним шляхом в 2 /d v , таким, що
),..,,)(/(),..,,)(/( 212211 mn vvvvdvvvvd . Отже 1 2/ /Ad v d v .
Лема доведена.
Лема 6 (монотонність іменування, слабка монотонність асоціативного розіменування і ділення відносно
N ). Нехай v V . Тоді
1) якщо 1 2Nd d , то 1 2( ) ( )Nv d v d ;
2) якщо 1 2Nd d , 1( )av d і 2( )av d , то 1( )av d N 2( )av d ;
3) якщо 1 2Nd d і 2 /d v , то 1 2/ /Nd v d v .
Теоретичні та методологічні основи програмування
63
Доведення.
1) нехай
1 2Nd d і v V . Позначимо ( ) [ ]i i ie v d v d , 1,2i . Якщо хоч одне з
1d ,
2d належить
W , то
1 2d d , тому
1 2( ) ( )Nv d v d . Розглянемо випадок, коли
1d W і
2d W . Нехай u V – слово,
таке, що
1( )au e W . Тоді або u v , або v u . Якщо u v , то
2( )u e W , бо
2d W . Якщо v u ,
то існує слово
1v V , таке, що
1vv u і
1 1 1( ) ( )a au e v d W . Оскільки
1 2Nd d , то
1 2( )av d W .
Тоді
2 1 2( ) ( )a au e v d W . Отже
1 2Ne e , тобто
1 2( ) ( )Nv d v d ;
2) нехай
1 2Nd d ,
1( )av d і
2( )av d . Нехай u V і
1( ( ))a au v d W . Тоді
1( ) ( )avu d W . Оскільки
1 2Nd d , то
2( ) ( )avu d W . Тоді
2( ( ))a au v d W . Отже
1 2( ) ( )a N av d v d в силу довільності u ;
3) нехай
1 2Nd d і
2 /d v . Тоді
1 2,d d W . Нехай u V – слово, таке, що
1( / )au d v W . Тоді
1( ) ( )avu d W і оскільки
1 2Nd d , то
2( ) ( )avu d W . Тоді
2( ( ))a au v d W . Оскільки
2 /d v ,
то
2 2( ) /av d d v , тому
2( / )au d v W . Отже
1 2/ /Nd v d v в силу довільності u .
Лема доведена.
Лема 7 (монотонність іменування, асоціативного розіменування і ділення відносно
w
).
Нехай v V . Тоді
1) якщо
1 2wd d , то 1 2( ) ( )wv d v d ;
2) якщо 1 2wd d і
1( )av d , то
2( )av d і 1( )av d w 2( )av d ;
3) якщо 1 2wd d і 2 /d v , то 1 2/ /wd v d v .
Доведення випливає безпосередньо з лем 5 і 6.
Лема 8 (монотонність структурного накладання за першим аргументом відносно
A
).
Нехай
1 1Ad d і
1 2sd d . Тоді
1 2sd d і 1 2 1 2s A sd d d d .
Доведення. Припустивши, що
1 2sd d , отримаємо 1d W або
2d W , тому 1d W (в силу того, що
1 1Ad d ) або
2d W , а отже
1 2sd d , що суперечить умові леми. Тому
1 2sd d , і достатньо довести, що
1 2 1 2s A sd d d d .
Нехай u V – таке слово, що
1 2( )a su d d W . Можливі 3 випадки:
1)
2( ) { }au d W . За лемою 1. 1),
1 2 2( ) ( )a s au d d u d і
1 2 2( ) ( )a s au d d u d ,
а отже
1 2 1 2( ) ( )a s a su d d u d d ;
2)
2( ) { }au d W . У цьому випадку існує слово
1u uV , таке, що
1 2( ) { }au d W .
Тоді за лемою 1. 1),
1 1 2( )a su d d , що суперечить припущенню 1 2( )a su d d W , оскільки u є власним
префіксом 1u . Тобто припущення 2( ) { }au d W виконуватися не може;
3) 2( )au d . За лемою 1. 2), 1 1 2( ) ( )a a su d u d d W . Оскільки 1 1Ad d ,
то
1 1( ) ( )a au d u d W за лемою 4.
Можливі такі випадки:
a)
1 2( ) { }a su d d W . У цьому випадку за лемою 1. 2), 1 2 1 1 2( ) ( ) ( )s su d d u d u d d ;
b)
1 2( ) { }a su d d W . У цьому випадку існує слово v V , таке, що
1 2( ) ( ) { }a suv d d W . Оскільки
2( ) ( )auv d , то за лемою 1. 2) отримуємо
1( ) ( ) { }auv d W ,
звідки
1( )au d W , що суперечить вищевказаній належності
1( )au d W ;
c)
1 2( )a su d d , але існує 0u – власний префікс u , такий, що
0 1 2( )a su d d . У цьому випадку
існує слово 0v , таке, що 0u є префіксом 0v і 0 1 2( ) { }a sv d d W , причому 0v є власним префіксом u .
Позначимо 1v V – слово, таке, що 0 1u v v . Якщо 0 2( )av d , то за лемою 1. 2),
0 1 0 1 2( ) ( ) { }a sv d v d d W , що суперечить вищевказаній належності 1( )au d W . Якщо ж
0 2( )av d , то існує слово *
1 0v v V , таке, що 1 2( ) { }av d W . Тоді за лемою 1. 1),
1 1 2 1 2( ) ( ) { }a s av d d v d W . Оскільки 0 1( )v pref v і 0 1 2( ) { }a sv d d W , то 1 0v v . Тоді
0 2( ) { }av d W , звідки за лемою 1. 1), 0 1 2 0 2( ) ( ) { }a s av d d v d W . Але 1 2( )a su d d W
і 0v – власний префікс u , отже отримали протиріччя. Тобто припущення даного випадку виконуватися не
може;
Теоретичні та методологічні основи програмування
64
d)
1 2( )a su d d для всіх префіксів u , зокрема
1 2( )a sx d d , де x – перша літера u . У цьому
випадку
2( )ax d , бо інакше існує слово *v xV , таке, що
2( ) { }av d W , і за лемою 1. 1),
1 2( )a sv d d , а отже
1 2( )a sx d d . Тоді за лемою 1. 3),
1 2 1( ) ( )a s au d d u d і
1 2 1( ) ( )a s au d d u d . Оскільки
1 2( )a su d d W і
1 1Ad d , то
1 2 1 2( ) ( )a s a su d d u d d .
Таким чином, у всіх можливих випадках
1 2 1 2( ) ( )a s a su d d u d d , а отже
1 2 1 2s A sd d d d
за лемою 4, в силу довільності слова u . Лема доведена.
Лема 9. Нехай
1 1wd d і 1 2sd d . Тоді
1 2sd d і
1 2 1 2s N sd d d d .
Доведення. Припустивши, що
1 2sd d , отримаємо
1d W або
2d W , тому
1d W (в силу того, що
1 1Nd d ) або
2d W , а отже
1 2sd d , що суперечить умові леми. Тому
1 2sd d , і достатньо довести, що
1 2 1 2s N sd d d d .
Нехай u V – таке слово, що
1 2( )a su d d W . Тоді існує слово *u uV , таке, що
1 2( ) { }a su d d W . Можливі 3 випадки:
1)
2( ) { }au d W . За лемою 1. 1),
1 2 2( ) ( )a s au d d u d і
1 2 2( ) ( )a s au d d u d ,
а отже
1 2 1 2( ) ( )a s a su d d u d d . Тому
1 2( )a su d d W ;
2)
2( ) { }au d W . У цьому випадку існує слово
1u uV , таке, що
1 2( ) { }au d W . Тоді за
лемою 1. 1),
1 1 2( )a su d d , що суперечить припущенню
1 2( ) { }a su d d W , оскільки u є власним
префіксом
1u . Тобто припущення
2( ) { }au d W виконуватися не може;
3)
2( )au d . За лемою 1. 2),
1 1 2( ) ( ) { }a a su d u d d W .
Якщо
1 2( )a su d d W , то оскільки
1 1Ad d , то
1( )au d W за лемою 4 і крім того, u u , бо
1 2( )a su d d W . Якщо 1 2( )a su d d , то
1( )au d W , бо 1 1Nd d . В обох випадках
1( )au d .
Можливі такі випадки:
1)
1 2( ) { }a su d d W . Оскільки u u , то
1 2( )a su d d W ;
2)
1 2( ) { }a su d d W . Якщо
1 2( )a su d d W , то u u , тому
1 2( )a su d d W . Якщо
1 2 1( ) ( )a s au d d u d , то за лемою 1. 1),
1 1 2( ) ( )a a su d u d d і оскільки 1 1Nd d ,
то
1( )au d W і
1 2( )a su d d W . Тоді
1 2( )a su d d W ;
3)
1( )au d W і
1 2( )a su d d , але існує
0u – власний префікс u , такий, що
0 1 2( )a su d d . Тоді
існує слово 0v , таке, що 0u є префіксом 0v і 0 1 2( ) { }a sv d d W , причому 0v є власним префіксом u .
Позначимо
1v V – слово, таке, що 0 1u v v . Якщо
0 2( )av d , то за лемою 1. 2),
0 1 0 1 2( ) ( ) { }a sv d v d d W , що суперечить тому, що
1( )au d . Якщо ж
0 2( )av d , то існує
слово *
1 0v v V , таке, що 1 2( ) { }av d W . Тоді за лемою 1. 1), 1 1 2 1 2( ) ( ) { }a s av d d v d W .
Оскільки 0 1( )v pref v і
0 1 2( ) { }a sv d d W , то 1 0v v . Тоді
0 2( ) { }av d W , звідки за лемою
1. 1),
0 1 2 0 2( ) ( ) { }a s av d d v d W . Але
1 2( ) { }a su d d W і
0v – власний префікс u , отже
отримали протиріччя. Тобто припущення даного випадку виконуватися не може;
4)
1 2( )a sv d d для всіх префіксів ( )v pref u , зокрема,
1 2( )a sx d d , де x – перша літера u .
У цьому випадку
2( )ax d , бо інакше існує слово *v xV , таке, що
2( ) { }av d W , і за лемою 1. 1),
1 2( )a sv d d , а отже 1 2( )a sx d d . Тоді за лемою 1. 3), 1 2 1( ) ( )a s au d d u d
і 1 2 1( ) ( )a s au d d u d . Оскільки
1 2( )a su d d і
1 1wd d , то
1 2( )a su d d – отримали протиріччя з
припущенням
1 2( )a sx d d .
В усіх можливих випадках 1 2( )a su d d W , а отже 1 2 1 2s N sd d d d в силу довільності слова u .
Лема доведена.
Лема 10 (монотонність структурного накладання за першим аргументом відносно w ). Нехай 1 1wd d
і 1 2sd d . Тоді 1 2sd d і 1 2 1 2s w sd d d d .
Доведення випливає безпосередньо з лем 8 і 9.
Лема 11 (обмежена монотонність структурного накладання за другим аргументом відносно A ). Нехай
1 2 2, , ( , ) \d d d NDVC V W W , 2 2Ad d і 2 2( ) ( )rn d rn d . Тоді 1 2 1 2s A sd d d d .
Доведемо індукцією за k , що якщо 1 ( , ) \kd NDVC V W W , 2 2, ( , ) \d d NDVC V W W , 2 2Ad d
і 2 2( ) ( )rn d rn d , то 1 2 1 2s A sd d d d .
Теоретичні та методологічні основи програмування
65
База індукції. Якщо 0k , то
1d і
1 2 2 2 1 2s A sd d d d d d .
Індукційний перехід. Припустимо, що твердження вже доведено для всіх
1 ( , ) \kd NDVC V W W . Оберемо
1 1( , ) \ ( , )k kd NDVC V W NDVC V W і
2 2,d d W , такі, що
2 2Ad d ,
2 2( ) ( )rn d rn d і доведемо, що
1 2 1 2s A sd d d d .
Нехай u V – слово, таке, що
1 2( )a su d d W . Тоді існує слово ( )v pref u , що є кореневим ім’ям
1 2sd d . Можливі такі випадки:
1) слово v не порівнюється з жодним кореневим іменем
2d . В цьому випадку
1( )v rn d (бо інакше
1 2( )( )sd d v за правилом 5 визначення операції
s ) і
1 1 2( ) ( )( )sd v d d v за правилом 4 визначення операції
s . Оскільки
2 2( ) ( )rn d rn d , то u не порівнюється з жодним кореневим іменем
2d . Тоді
1 2 1( )( ) ( )sd d v d v , звідки
1 2 1 2( ) ( )a s a su d d u d d , бо ( );v pref u
2) слово v є власним префіксом деякого кореневого імені
1v даного
2d і неатомним кореневим ім’ям в
1d . В цьому випадку
1 2 1 2( )( ) ( ) ( / )s sd d v d v d v за правилом 2 визначення операції
s . Оскільки
2 2( ) ( )rn d rn d , то
2 1( )d v і
1 2 1 2( )( ) ( ) ( / )s sd d v d v d v . Оскільки
2 /d v і
2 2Ad d , то
2 2/ /Ad v d v за
лемою 5. 3). Оскільки
2 2( ) ( )rn d rn d , то
2 2( / ) ( / )rn d v rn d v . Оскільки
1( ) ( , )kd v NDVC V W , то за
припущенням індукції, 1 2 1 2( )( ) ( )( )s A sd d v d d v . Тоді
1 2 1 2( ) ( )a s a su d d u d d за лемою 4, оскільки
( )v pref u і 1 2( )a su d d W ;
3) слово v є власним префіксом деякого кореневого імені 1v даного
2d і атомним кореневим ім’ям в
1d .
У цьому випадку 1 2 2( )( ) /sd d v d v за правилом 3 визначення операції
s . Оскільки 2 2( ) ( )rn d rn d ,
то
2 1( )d v і
1 2 2( )( ) /sd d v d v . Оскільки
2 /d v і
2 2Ad d , то
2 2/ /Ad v d v за лемою 5. 3).
Тоді
1 2 1 2( ) ( )a s a su d d u d d за лемою 4, оскільки ( )v pref u і
1 2( )a su d d W ;
4) не виконуються умови 1–3. Тоді за правилами 1 та 5 визначення операції
s ,
2 1( ) \ ( )v rn d rn d V
і 1 2 2( )( ) ( )sd d v d v . Оскільки 2 2( ) ( )rn d rn d , то
2 1( ) \ ( )v rn d rn d V . Тоді
1 2 2( )( ) ( )sd d v d v .
Оскільки ( )v pref u і 2 2Ad d , то
2 2( ) ( )a au d u d W за лемою 4.
Тоді
1 2 2 2 1 2( ) ( ) ( ) ( )s su d d u d u d u d d .
Отже в усіх випадках
1 2 1 2( ) ( )a s a su d d u d d , звідки
1 2 1 2s A sd d d d за лемою 4 в силу
довільності слова u . Індукційний перехід завершено. Лема доведена.
Лема 12. (обмежена монотонність структурного накладання за другим аргументом відносно
N
). Нехай
1 2 2, , ( , ) \d d d NDVC V W W , 2 2Nd d і 2 2( ) ( )rn d rn d . Тоді 1 2 1 2s N sd d d d .
Доведемо індукцією за k , що якщо 1 ( , ) \kd NDVC V W W , 2 2, ( , ) \d d NDVC V W W , 2 2Nd d і
2 2( ) ( )rn d rn d , то 1 2 1 2s N sd d d d .
База індукції. Якщо 0k , то 1d і 1 2 2 2 1 2s N sd d d d d d .
Індукційний перехід. Припустимо, що твердження вже доведено для всіх 1 ( , ) \kd NDVC V W W . Оберемо
1 1( , ) \ ( , )k kd NDVC V W NDVC V W і 2 2,d d W , такі, що 2 2Nd d , 2 2( ) ( )rn d rn d і доведемо, що
1 2 1 2s N sd d d d .
Нехай u V – слово, таке, що 1 2( )a su d d W . Тоді існує слово ( )v pref u , що є кореневим ім’ям
1 2sd d . Можливі такі випадки:
1) слово v не порівнюється з жодним кореневим іменем 2d . В цьому випадку 1( )v rn d (бо інакше
1 2( )( )sd d v за правилом 5 визначення операції
s ) і 1 1 2( ) ( )( )sd v d d v за правилом 4 визначення операції
s . Оскільки 2 2( ) ( )rn d rn d , то u не порівнюється з жодним кореневим іменем 2d . Тоді 1 2 1( )( ) ( )sd d v d v ,
звідки 1 2 1 2( ) ( )a s a su d d u d d , бо ( )v pref u , тому 1 2( )a su d d W ;
2) слово v є власним префіксом деякого кореневого імені 1v даного 2d і неатомним кореневим ім’ям
в 1d . У цьому випадку 1 2 1 2( )( ) ( ) ( / )s sd d v d v d v за правилом 2 визначення операції s . Оскільки
2 2( ) ( )rn d rn d , то 2 1( )d v і 1 2 1 2( )( ) ( ) ( / )s sd d v d v d v . Оскільки 2 /d v і 2 2Nd d , то 2 2/ /Nd v d v за
лемою 5. 3). Оскільки 2 2( ) ( )rn d rn d , то 2 2( / ) ( / )rn d v rn d v . Оскільки 1( ) ( , )kd v NDVC V W , то за
припущенням індукції, 1 2 1 2( )( ) ( )( )s N sd d v d d v . Тоді 1 2( )a su d d W , оскільки ( )v pref u і 2 2Nd d ;
Теоретичні та методологічні основи програмування
66
3) слово v є власним префіксом деякого кореневого імені
1v даного
2d і атомним кореневим ім’ям в
1d .
В цьому випадку
1 2 2( )( ) /sd d v d v за правилом 3 визначення операції
s . Оскільки
2 2( ) ( )rn d rn d ,
то
2 1( )d v і
1 2 2( )( ) /sd d v d v . Оскільки
2 /d v і
2 2Nd d , то
2 2/ /Nd v d v за лемою 5. 3).
Тоді
1 2( )a su d d W , оскільки ( )v pref u і
1 2( )a su d d W .
4) не виконуються умови 1–3. Тоді за правилами 1 та 5 визначення операції
s ,
2 1( ) \ ( )v rn d rn d V і
1 2 2( )( ) ( )sd d v d v . Оскільки
2 2( ) ( )rn d rn d , то
2 1( ) \ ( )v rn d rn d V . Тоді
1 2 2( )( ) ( )sd d v d v . Оскільки
( )v pref u , то
2( )au d W і оскільки
2 2Nd d , то
2( )au d W . Тоді
1 2 2( ) ( )su d d u d W .
Отже в усіх випадках
1 2( )a su d d W , звідки
1 2 1 2s N sd d d d в силу довільності слова u .
Індукційний перехід завершено. Лема доведена.
Лема 13 (обмежена монотонність структурного накладання за другим аргументом відносно
w
). Нехай
1 2 2, , ( , ) \d d d NDVC V W W ,
2 2wd d і 2 2( ) ( )rn d rn d . Тоді
1 2 1 2s w sd d d d .
Доведення випливає безпосередньо з лем 11 і 12.
Таким чином, з наведених лем випливає, що операції іменування і асоціативного розіменування
є монотонними за відношенням
w
, а операція структурного накладання монотонна за першим аргументом
і монотонна в обмеженому сенсі за другим аргументом.
4. Мова SICONT
Визначимо мову програм над складноіменними даними, яку назвемо TSICON , програми якої будуть
монотонними за відношенням
w
. Як зазначалося раніше, для цього необхідно вказати базові функції і
композиції. Оберемо деяке фіксоване значення T W , яке інтерпретується як логічна константа, і позначимо
( , ) ( , )F NDVC V W NDVC V W .
До базових функцій мови TSICON належать:
сім’я операцій іменування v з параметром v V ;
сім’я операцій асоціативного розіменування
av з параметром v V ;
функція-константа T , яка на всіх вхідних даних приймає значення T .
Як композицію мови
TSICON оберемо найпростіші композиції структурного програмування.
1. Множення – це бінарна композиція, яка за функціями ,f g F будує функцію h F (позначається
h f g ), таку, що ( ) ( ( ))h d g f d .
2. Цикл – це бінарна композиція, яка за функціями p F (умова) і g F (тіло циклу) будує функцію
h F (позначається *h p g ), таку, що
( )h d d , якщо ( )p d T ;
( )( ) ( )kh d g d , якщо ( )( ( ))kp g d T і ( )( ( ))ip g d T для всіх {1,2,.., 1}i k
(тут ( ) ( ) ( (.. ( )..))kg d g g g d – k-кратне застосування функції g до даного d );
( )h d не визначено, в інших випадках.
3. Присвоєння vAsg , залежне від параметру v V – унарна композиція на F , що задається формулою
( )( ) [ ( )]v
sAsg f d d v f d .
Тоді всі функції (програми), які виражаються в мові TSICON , складають множину
0
( , ) ( , )T T
kk
SFA V W SFA V W
, де
0 ( , ) { } { | } { | }T
aSFA V W T u u V u u V ;
1( , ) ( , ) { | , ( , )}T T T
k k kSFA V W SFA V W f g f g SFA V W
{ * | , ( , )} { ( ) | ( , ) }T v T
k kp g p g SFA V W Asg f f SFA V W v V .
Тобто ( , )TSFA V W – це функції, що можуть бути отримані з базових застосуванням композицій.
Незважаючи на простоту, мова TSICON є достатньо потужною. По-перше, як і в мові aSICON [2], в ній
можна промоделювати всі частково рекурсивні функції, тобто ця мова є функціонально повною. По-друге,
в мові aSICON можна промоделювати похідними композиціями багато композицій, що використовуються
у програмуванні – різноманітні умовні оператори, цикли тощо. Це дозволяє стверджувати, що мова TSICON
є структурно адекватною. По-третє, вона очевидно, має стислий та формальний опис. Наступна теорема
показує, що всі програми цієї мови є монотонними за відношенням w (і як наслідок, номінативно
стабільними).
Теоретичні та методологічні основи програмування
67
Теорема 1. Програми мови
TSICON є монотонними за відношенням
w
, тобто довільна функція
( , )Tf SFA V W є монотонною в такому сенсі:
якщо
1 2wd d і
1( )f d , то
2( )f d і
1 2( ) ( )wf d f d .
Доведемо індукцією за рангом
1d , що кожна функція ( , )T
kf SFA V W монотонна.
База індукції. При 0k ,
0 ( , ) { } { | } { | }T
aSFA V W T u u V u u V , тому монотонність функцій з
0 ( , )TSFA V W випливає з леми 5.
Індукційний перехід. Припустимо, що для деякого k твердження вже доведено, і доведемо його для
кожної функції з
1( , )T
kSFA V W
. Нехай
1( , ) \ ( , )T T
k kf SFA V W SFA V W .
Можливі такі випадки:
1) f g h для деяких , ( , )T
kg h SFA V W . Нехай
1 2wd d і
1( )f d . Тоді
1( )g d і за індукційним
припущенням,
2( )g d і
1 2( ) ( )wg d g d . Звідси
2 2( ) ( ( ))f d h g d і
1 1 2( ( )) ( ) ( )wh g d f d f d . Отже, функція
f монотонна;
2) *f g h для деяких , ( , )T
kg h SFA V W . Нехай
1 2wd d і
1( )f d . Тоді для деякого m Nat
виконується ( )
1 1( ) ( )mh d f d , ( )
1( ( ))mg h d T і ( )
1( ( ))ig h d T для всіх {0,1,.., 1}i m . Використовуючи m
разів монотонність функції h , отримуємо, що ( )
2( )ih d і ( ) ( )
1 2( ) ( )i i
wh d h d для {0,1,.., }i m . Із монотонності
g випливає, що ( )
2( ( ))ig h d T для всіх {0,1,.., 1}i m і ( )
2( ( ))mg h d T . Тоді за визначенням циклу,
( )
2 2 2( ) ( * )( ) ( )mf d g h d h d і
1 2( ) ( )wf d f d . Отже f монотонна;
3) ( )uf Asg g для деякого u V і ( , )kg SFA V W . Нехай
1 2wd d і
1( )f d . Тоді
1( )g d і за
монотонністю g ,
2( )g d і
1 2( ) ( )wg d g d . Крім того,
1 1 1( ) [ ( )]sf d d u g d ,
2 2 2( ) [ ( )]sf d d u g d .
Оскільки
1d W , то
2d W і
2( )f d . Оскільки
1 2( ) ( )wg d g d , то за лемою 7,
1 2[ ( )] [ ( )]wu g d u g d .
Тоді з лем 10 і 13 випливає, що
1 1 1 1 2 2 2 2( ) [ ( )] [ ( )] [ ( )] ( )s w s w sf d d u g d d u g d d u g d f d .
Отже функція f монотонна. Індукційний перехід завершено. Теорема доведена.
Наслідком отриманого результату є наступне твердження.
Теорема 2. Програми мови TSICON є номінативно стабільними за відношенням , тобто довільна
функція ( , )Tf SFA V W є стабільною в такому сенсі:
якщо
1d 2d і )( 1df або )( 2df , то обидва значення )( 1df та )( 2df визначені і )()( 21 dfdf .
Значення отриманих результатів полягає в тому, що програміст при написанні програм мови
TSICON (або подібних мов) може не займатися “ручним” узгодженням ієрархій даних між різними
компонентами програм (програмних систем), бо таке узгодження відбувається автоматично.
Висновки
У роботі побудовано та досліджено достатньо потужну формальну мову TSICON номінативно
стабільних та монотонних програм щодо структурних трансформацій даних. Така мова може стати
теоретичною основою для практичних мов програмування, які дозволять спростити процес програмування та
зробити його більш ефективним.
1. Никитченко Н.С. Композиционно-номинативный подход к уточнению понятия программы // Проблеми програмування.– 1999.–
№ 1. – C. 16–31.
2. Нікітченко М.С., Іванов Є.В. Властивості композиційно-номінативних мов програм з асоціативним розіменуванням // Матеріали
XVI Всеукраїнської наук. конф. “Сучасні проблеми прикладної математики та інформатики”. 8–9 жовтня 2009. – Львів, 2009.
– С. 157–158.
|
| id | nasplib_isofts_kiev_ua-123456789-14636 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Ukrainian |
| last_indexed | 2025-12-07T17:43:52Z |
| publishDate | 2010 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Нікітченко, М.С. Іванов, Є.В. 2010-12-27T13:52:52Z 2010-12-27T13:52:52Z 2010 Стабільність та монотонність програм щодо структурних трансформацій даних/ М.С. Нікітченко, Є.В. Іванов// Пробл. програмув. — 2010. — № 2-3. — С. 58-67. — Бібліогр.: 2 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/14636 004.4 Розглядається проблема поведінки програм щодо структурних трансформацій вхідних даних. Проведено уточнення проблеми та її
 формалізацію в рамках композиційно-номінативного підходу. Досліджено введені поняття та побудовано мову програм, які мають
 стабільну та монотонну поведінку при зміні структури вхідних даних. In the article the problem of program behavior with respect to structure transformations of input data is considered. An explication and
 formalization of the problem in the framework of composition-nominative approach is given. Defined notions are studied and a language of
 programs having stable and monotone behavior under structure transformations is constructed. uk Інститут програмних систем НАН України Теоретичні та методологічні основи програмування Стабільність та монотонність програм щодо структурних трансформацій даних Stability and monotonicity of programs with respect to structure transformations of data Article published earlier |
| spellingShingle | Стабільність та монотонність програм щодо структурних трансформацій даних Нікітченко, М.С. Іванов, Є.В. Теоретичні та методологічні основи програмування |
| title | Стабільність та монотонність програм щодо структурних трансформацій даних |
| title_alt | Stability and monotonicity of programs with respect to structure transformations of data |
| title_full | Стабільність та монотонність програм щодо структурних трансформацій даних |
| title_fullStr | Стабільність та монотонність програм щодо структурних трансформацій даних |
| title_full_unstemmed | Стабільність та монотонність програм щодо структурних трансформацій даних |
| title_short | Стабільність та монотонність програм щодо структурних трансформацій даних |
| title_sort | стабільність та монотонність програм щодо структурних трансформацій даних |
| topic | Теоретичні та методологічні основи програмування |
| topic_facet | Теоретичні та методологічні основи програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/14636 |
| work_keys_str_mv | AT níkítčenkoms stabílʹnístʹtamonotonnístʹprogramŝodostrukturnihtransformacíidanih AT ívanovêv stabílʹnístʹtamonotonnístʹprogramŝodostrukturnihtransformacíidanih AT níkítčenkoms stabilityandmonotonicityofprogramswithrespecttostructuretransformationsofdata AT ívanovêv stabilityandmonotonicityofprogramswithrespecttostructuretransformationsofdata |