13. Неперервні відображення.Теореми про найменшу нерухому точку (Кнастер-Тарський-Кліні); теорема про неперервність оператора нерухомої точки.

Визначення на властивості неперервних відображень

Визначення 5.6.Відображення :D D,задане наЧВМ , – неперервне за Гейне, якщо для будь-якого ланцюга з D виконується рівність

1. .

Зауваження 5.4.Поняття неперервного відображення узагальнюється для відображень типу  : DR, (де (D, _D) та (R, _R) – ЧВМ) наступним чином. Нехай – ланцюг в D. Тоді   – неперервне, якщо .

Визначення 5.7.Відображення :D D–монотонне, якщо

2. .

Неперервні відображення є монотонними.

Лема 5.1. Нехай – ЧВМ та :DD – неперервне відображення, тоді – монотонне.

Доведення

Нехай є ланцюг , всі елементи якого, крім d₀, дорівнюють d₁. Тоді з визначення ланцюга та неперервності випливає, що

3. 

Оскільки , то . Це означає, що є мажорантою . Тому ._▄

14. Теореми про найменшу нерухому точку

Теорема 5.1 (Кнастер-Тарський-Кліні)

Нехай D – ω-область, :DD – неперервне відображення, задане на цій області. Тоді існує найменша нерухома точка , яка позначається та для якої справедлива наступна формула:

(),

(КТК)

де , , i.

Доведення теореми складається з трьох тверджень:

1. Доведення факту, що множина { }_i є ланцюг (тому її супремум існує).

2. Доведення того, що є нерухомою точкою φ.

3. Доведення, що є найменшою з нерухомих точок φ.

Почнемо з першого твердження. Розглянемо послідовність .

Доведемо методом математичної індукції, що це – ланцюг.

База індукції. Оскільки  – найменший елемент D, то .

Індуктивний крок. Треба довести, що з випливає . Дійсно, за монотонністю φ маємо

.

Отже – ланцюг.

Перейдемо до другого твердження. За неперервністю :

.

Остання рівність випливає з того, що , а найменший елемент не впливає на супремум. Отже, – нерухома точка φ.

Доведемо тепер останнє твердження, що – найменша нерухома точка (ННТ).

Нехай b також нерухома точка, тобто . Маємо, що . За монотонністю φ . Аналогічно, для всіх i. Тому . Отже, – найменша з нерухомих точок._▄

15. Теорема про не перерв. оператора нерухомої точки

Теорема 5.3 (неперервність lfp). Якщо – -область, то відображення - неперервне, тобто .

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

4. .

Спочатку доведемо, що . Оскільки , то за лемою 5.10 для довільного , а отже .

Тепер доведемо, що . Для цього покажемо, що – нерухома точка для (тобто, ). Дійсно

.Позначимо , . Неважко довести, що засновки леми 5.2 виконуються, тому

= .

Оскільки – найменша нерухома точка, то вона менша за будь-яку нерухому точку для . Тому .

Отже ми довели, що . _▄

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

14. Методи формальної семантики мов програмування (композиційна, натуральна, денотаційна, аксіоматична).

Методи формальної семантики.

Формальная семантика — это изучение семантики, или интерпретации, формальных и естественных языков путём их формального описания в математических терминах.

Формальный язык может быть задан без какой-либо интерпретации. Это достигается заданием множества символов (также называемого алфавитом) и множества правил вывода (также называемого формальной грамматикой), которые определяют, какие строки символов являются правильно построенными формулами. При добавлении правил преобразования и принятии некоторых предложений за аксиомы (что вместе называется дедуктивной системой), формируется логическая система. Интерпретация — это задание смысла её символам и значений истинности её предложениям.

Условия истинности различных предложений, которые могут присутствовать в аргументах, зависят от их смысла, поэтому добросовестные учёные не могут полностью обойтись без какого-либо описания смысла этих предложений. Семантика логики описывает различные подходы к пониманию и определению тех частей смысла, которые представляют интерес. Как правило, интерес с точки зрения логики представляет не само по себе предложение, а оно же в пропозиционной, идеализированной форме, подходящей для логических преобразований.

До становления современной логики, в Органоне Аристотеля, а именно в работеОб истолковании были заданы основы понимания и значения логики. Введение кванторов должно было решить проблему общности множеств, не решаемую в рамках субъектно-предикатного анализа Аристотеля, хотя в логике термов появляется новый интерес, а именно попытки построить исчисление в духе силлогистики Аристотеля, но используя свойства общности кванторов из современной логики.

Основными современными подходами к семантике для формальных языков являются:

Модельно-теоретическая семантика, архетип семантики теории истинности Альфреда Тарского, основанной на его Т-схеме, является одной из ключевых концепций модельной теории. Это один из наиболее распространённых подходов. Основная его идея в том, что смысл различных частей утверждения задаются всевозможными способами рекурсивного задания

группы функций интерпретации, отображающих предложения на некоторые заранее заданные математические множества. Так, интерпретация логики предикатов первого порядка задаётся отображением термов в универсум, и отображение предикатов в значения истинности «истина» и «ложь». На модельно-теоретической семантике основан подход в теории смысла под названием семантика условной Истины, который впервые был предложен Дональдом Девидсоном. Семантика Крипке по сути вносит некоторые дополнения к семантике Тарского.

Доказательно-теоретическая семантика связывает смысл утверждений с ролями, которые они играют в рассуждении. Герхард Гентцен, Дэг Превитц и Майкл Даммет считаются основателями этого подхода. На него

сильно повлияла поздняя философия Людвига Витгенштейна, особенно его афоризм «смысл — это применение».

Семантика значений истинности (также известная как подстановочная квантификация) была предложена Рутом Баркан Маркусом для модальных логик в начале 1960-х и затем продвигалась Данном, Белнапом и Лебланом в качестве стандартной логики первого порядка. Джеймс Гарсон получил некоторые результаты в областях адекватности интенсиональных логик, снабжённых такой семантикой. Условия истинности квантифицированных формул задаются исключительно в терминах истинности, без использования множеств (отсюда и название).

Игровая семантика недавно была возрождена Яакко Хинтикка для логик (конечной) частично покрытой квантификации, которые изначально исследовались Леоном Хенкиным.

Вероятностная семантика — естественное обобщение семантики значений истинности, созданное Филдом.

Лингвисты редко применяли формальные семантики до тех пор, пока Ричард Монтегю не показал как можно воспринимать английский (или любой другой естественный язык) как формальный язык. Его вклад в лингвистическую семантику, известный как грамматика Монтегю, представляет основу для того, что лингвисты называют формальной семантикой.

15. Формальні методи розробки програм.

Формальні методи програмування. Формальні методи (англ. Formal methods) — у комп'ютерних науках, побудовані на математиці методи написання специфікацій, розробки та перевірки (англ. verification) програмного забезпечення та комп'ютерного обладнання. Цей підхід особливо важливий для вбудованих систем, для яких важливими є надійність або безпека, для захисту від помилок у процесі розробки. Застосування формальних методів особливо ефективне на ранніх етапах написання вимог та специфікацій, але, вони також можуть застосовуватися для повністю формальної розробки реалізації (наприклад, програми).

Формальні методи може бути застосовано на декількох рівнях: Рівень 0 Написання формальної специфікації та неформалізована розробка, на її основі, програмного забезпечення. Такий підхід, також, має назву спрощені формальні методи. Він може бути найоптимальнішим підходом з погляду витрат у багатьох випадках.

Рівень 1

Формальний підхід до розробки та перевірки програмного забезпечення може використовуватись для формальнішої реалізації програми. Наприклад, може виконуватись доведення властивостей або уточнення (англ. refinement) із формальної специфікації в програмі. Такий підхід найоптимальніший у вбудованих системах, які повинні мати високий рівень безпеки або надійності.

Рівень 2

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

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

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

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

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

Прип щення (англ. Assertion) (варіанти перекладу терміну: твердження, пересвідчення) в програмуванні — конструкція в мові програмування яка описує певне припущення щодо властивостей змінних або стану програми.Це припущення зазвичай повенне бути істинним. Більшість мов програмування використовують ці припущення для перевірки таких коректності даних і виконання, а деякі використовують їх для документування. Якщо припущення не виконується, це може вказувати на наявність помилки в програмі