Головна сторінка: Różnice pomiędzy wersjami
Z Lem
(Tłumaczenie LEM i SpecVer) |
m (→Питання) |
||
| (Nie pokazano 4 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
| Linia 3: | Linia 3: | ||
| − | Лотар [[Коллатц]] (<small> у 1937 році</small>) мав рацію ! | + | Лотар [[Коллатц]] (<small> у 1937 році</small>) мав рацію ! |
------- | ------- | ||
| − | + | == Карта == | |
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | + | ||
| − | = | + | |
На цих сторінках ми представляємо чотири дослідницькі проєкти: Алгоритмічна логіка(з 1968), Loglan'82(з 1978), SpecVer(2007), Lem(2012). | На цих сторінках ми представляємо чотири дослідницькі проєкти: Алгоритмічна логіка(з 1968), Loglan'82(з 1978), SpecVer(2007), Lem(2012). | ||
Перші два проєкти дали багато результатів і будуть використовуватися ще багато років.<br /> | Перші два проєкти дали багато результатів і будуть використовуватися ще багато років.<br /> | ||
| Linia 37: | Linia 29: | ||
|- | |- | ||
| − | |♥ LEM - це назва нового дослідницького проєкту. | + | |♥ ''LEM'' - це назва нового дослідницького проєкту. |
Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. [[специфікація LEM]]). | Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. [[специфікація LEM]]). | ||
Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д.<br /> | Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д.<br /> | ||
→ '''[[LЕM]]''' | → '''[[LЕM]]''' | ||
| − | |♥ Проєкт SpecVer має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer.<br /> | + | |♥ Проєкт ''SpecVer'' має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer.<br /> |
→ '''[[SpеcVer]]''' | → '''[[SpеcVer]]''' | ||
|} | |} | ||
| + | |||
| + | {| class="wikitable" | ||
| + | |- | ||
| + | |♥ Бібліотека класів і математичних знань, корисних для програмістів. <br /> | ||
| + | Візія майбутнього (ще один проєкт на роки роботи для багатьох людей). | ||
| + | |||
| + | Давайте почнемо з кількох питань: Чи можна вмістити математичні знання в комп'ютері? Чи можна вмістити інформатичні знання в комп'ютері? Дональд Кнут 70-х роках XX століття мав таку амбіцію, розпочинаючи створення своєї книги ''Мистецтво програмування''. Сьогодні, через майже 50 років, комп'ютерні знання зросли і здається неможливим, що їх можна вмістити в комп'ютері. Але, по-перше, комп'ютери тепер значно більші і швидші, ніж колись, а по-друге, існує комп'ютерна мережа (Здійснилася візія С. Лема з 50-х років). Це дозволяє нам перейти до створення ескізу концепції. <br /> | ||
| + | Необхідно було б : | ||
| + | # Створити сховище знань, якими користуються розробники програмного забезпечення. Тут будуть знаходитися бібліотеки класів і методів, а також знання про структури даних, в яких проводяться обчислення. Це стосується як структур реляційних (алгебраїчних), що розглядаються математиками, так і структур даних, визначених і використовуваних інженерами програмного забезпечення. | ||
| + | # Створити мову, якою розробники програмного забезпечення будуть писати свої аргументи для (друкованих, розповсюджуваних, ...) повідомлень. Така мова повинна бути зрозумілою для людей і достатньо формалізованою, щоб була можливість комп'ютерного аналізу передставлених доказів. | ||
| + | # Інструмент для перевірки достовірності доказів. Буде потрібна програма proof checker, який суттєво відрізнятиметься від Mizara та йому подібних, оскільки докази будуть записані в рахунку програм (тобто в системі AL), який багатший за рахунок предикатів. | ||
| + | # Придумати спосіб збирання та поширення знань. Чи це має бути щось на кшталт математично-алгоритмічної пошукової системи Google? | ||
| + | |} | ||
| + | |||
| + | == Питання == | ||
| + | Про функціональне програмування і тому подібне. | ||
| + | # Не розумію: мене переконують перейти на функціональне програмування. Що я від цього отримаю? Кажуть, у функціональному програмуванні відсутні побічні ефекти та операції присвоєння. І що з того? Чи існують інструменти для вираження властивостей, таких як: <br /> a) Обчислення буде закінчене, <br /> b) Набір визначень не містить протиріч, <br /> c) Результати будуть правильними, i т.д. | ||
| + | # У 1943 році Стівен Коул Кліні довів, що будь-яку рекурсивну функцію в розумінні Гьоделя-Гербранда можна виразити оператором мінімуму ефективного <math>\mu</math>. Чи це не означає, що в області натуральних (цілих) чисел функціональне програмування та програмування за допомогою операцій while i ін. визначають один і той самий набір обчислюваних функцій? | ||
| + | # Чи можна у функціональному програмуванні описати синтаксис такого класу програм, що обчислення будуть закінчені? Для ітераційного програмування (тобто структурного) такий критерій існує. | ||
| + | # Я прочитав такий вислів: ''Якби який-небуть тиран заборонив використання процедур та функцій, тоді вся інформатика зазнала б краху. Вони настільки важливі, що важко уявити програмування без використання процедур та функцій.'' Як це стосується теореми Кліні? тези Черча-Тюрінга? | ||
| + | # Вартість? Розглянемо послідовність Фібоначчі. Яка найкраща вартість обчислення n-го виразу цієї послідовності? | ||
| + | Щодо керування пам'яттю (збір сміття, висячі референції). | ||
| + | # Чи варто довільно вирішувати про відкидання інструкції, яка видаляє об'єкт? | ||
Aktualna wersja na dzień 22:58, 6 mar 2024
Лотар Коллатц ( у 1937 році) мав рацію !
Карта
На цих сторінках ми представляємо чотири дослідницькі проєкти: Алгоритмічна логіка(з 1968), Loglan'82(з 1978), SpecVer(2007), Lem(2012).
Перші два проєкти дали багато результатів і будуть використовуватися ще багато років.
| ♥ Дослідницький проєкт "Алгоритмічна логіка" займається відкриттям законів рахунку програм і знаходить застосування у верифікації програм, тобто у доведенні істинності таких властивостей програм, як коректність, відсутність циклів тощо. Мова алгоритмічної логіки дозволяє не лише виражати властивості алгоритмів (програм), а й забезпечує аксіоматизацію багатьох структур даних. Це стосується як відомих і необхідних в алгоритміці структур даних (наприклад, стеки, бінарні дерева пошуку, купи і т. д.), так і багатьох структур, що вивчаються в математиці. Можна вважати, що математика займається дослідженням, чи є дана формула [math] \alpha [/math] істинною у даній структурі [math] \mathbb{A} [/math]. Однак більшість структур не можна описати за допомогою аксіом, записаних у логіці першого порядку! Прийняття мови алгоритмічної логіки (або коротше, алгоритмічної мови) дозволяє представити ... |
♥ Дослідницький проєкт "Loglan'82" сприяв створенню однойменної об'єктно-орієнтованої та розподіленої мови програмування. Публікація мови та розповсюдження компілятора передували дослідженням різних проблем.
Наведемо кілька прикладів: • Вирішення проблеми безпечного та ефективного вивільнення надлишкових об'єктів. |
| ♥ LEM - це назва нового дослідницького проєкту.
Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. специфікація LEM).
Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д. |
♥ Проєкт SpecVer має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer. → SpеcVer |
♥ Бібліотека класів і математичних знань, корисних для програмістів. Візія майбутнього (ще один проєкт на роки роботи для багатьох людей). Давайте почнемо з кількох питань: Чи можна вмістити математичні знання в комп'ютері? Чи можна вмістити інформатичні знання в комп'ютері? Дональд Кнут 70-х роках XX століття мав таку амбіцію, розпочинаючи створення своєї книги Мистецтво програмування. Сьогодні, через майже 50 років, комп'ютерні знання зросли і здається неможливим, що їх можна вмістити в комп'ютері. Але, по-перше, комп'ютери тепер значно більші і швидші, ніж колись, а по-друге, існує комп'ютерна мережа (Здійснилася візія С. Лема з 50-х років). Це дозволяє нам перейти до створення ескізу концепції.
|
Питання
Про функціональне програмування і тому подібне.
- Не розумію: мене переконують перейти на функціональне програмування. Що я від цього отримаю? Кажуть, у функціональному програмуванні відсутні побічні ефекти та операції присвоєння. І що з того? Чи існують інструменти для вираження властивостей, таких як:
a) Обчислення буде закінчене,
b) Набір визначень не містить протиріч,
c) Результати будуть правильними, i т.д. - У 1943 році Стівен Коул Кліні довів, що будь-яку рекурсивну функцію в розумінні Гьоделя-Гербранда можна виразити оператором мінімуму ефективного [math]\mu[/math]. Чи це не означає, що в області натуральних (цілих) чисел функціональне програмування та програмування за допомогою операцій while i ін. визначають один і той самий набір обчислюваних функцій?
- Чи можна у функціональному програмуванні описати синтаксис такого класу програм, що обчислення будуть закінчені? Для ітераційного програмування (тобто структурного) такий критерій існує.
- Я прочитав такий вислів: Якби який-небуть тиран заборонив використання процедур та функцій, тоді вся інформатика зазнала б краху. Вони настільки важливі, що важко уявити програмування без використання процедур та функцій. Як це стосується теореми Кліні? тези Черча-Тюрінга?
- Вартість? Розглянемо послідовність Фібоначчі. Яка найкраща вартість обчислення n-го виразу цієї послідовності?
Щодо керування пам'яттю (збір сміття, висячі референції).
- Чи варто довільно вирішувати про відкидання інструкції, яка видаляє об'єкт?
