Lem - Wkład użytkownika [pl]

Головна сторінка

2024-03-06T21:58:21Z

AnastasiiaSadlovska: /* Питання */

[[Plik:22px-English_language.svg.png]]
[[Main page]]     [[Plik:Flag of Poland.svg.png]][[ Strona główna]] 

Лотар [[Коллатц]] ( у 1937 році) мав рацію !

-------

== Карта ==
На цих сторінках ми представляємо чотири дослідницькі проєкти: Алгоритмічна логіка(з 1968), Loglan'82(з 1978), SpecVer(2007), Lem(2012).
Перші два проєкти дали багато результатів і будуть використовуватися ще багато років. 

{| class="wikitable"
|-
|♥ Дослідницький проєкт '''"Алгоритмічна логіка"''' займається відкриттям законів [[рахунок програм |рахунку програм]] і знаходить застосування у верифікації програм, тобто у доведенні істинності таких властивостей програм, як [[коректність]], відсутність циклів тощо. Мова алгоритмічної логіки дозволяє не лише виражати властивості алгоритмів (програм), а й забезпечує аксіоматизацію багатьох структур даних. Це стосується як відомих і необхідних в алгоритміці структур даних (наприклад, стеки, бінарні дерева пошуку, купи і т. д.), так і багатьох структур, що вивчаються в математиці. Можна вважати, що математика займається дослідженням, чи є дана формула <math> \alpha </math> істинною у даній структурі <math> \mathbb{A} </math>. Однак більшість структур не можна описати за допомогою аксіом, записаних у логіці першого порядку! Прийняття мови алгоритмічної логіки (або коротше, алгоритмічної мови) дозволяє представити ... 
→ '''[[Алгоритмічна логіка]]''' 
→ '''[[Media:UlotkaLogikaAlgorytmiczna.pdf| Листівка з алгоритмічної логіки]]'''

|width="50% " | ♥ Дослідницький проєкт '''"Loglan'82"''' сприяв створенню однойменної об'єктно-орієнтованої та розподіленої мови програмування. Публікація мови та розповсюдження компілятора передували дослідженням різних проблем.
Наведемо кілька прикладів: 

• Вирішення проблеми безпечного та ефективного вивільнення надлишкових об'єктів. 
• Вирішення проблеми (статичної) семантики, яка виникає, коли модулі класів можуть бути вкладеними (внутрішні класи) та розширеними (успадкування). 
• Оригінальний протокол взаємодії об'єктів процесів, які програміст може виділити в комп'ютерній мережі (alien call protocol). 
Мова Loglan була створена багато років до мов програмування C++ (1986) та Java (1995). Ці дві (та інші) мови програмування не узяли на озброєння рішень, відомих у Loglan протягом понад 30 років. Ознайомлення з Loglan може повністю змінити вашу думку про інженерію програмного забезпечення. Використовуючи знання та навички, які пропонує Loglan, ви можете значно підвищити свою кваліфікацію. 
→ '''[[Lоglan'82]]''' 
→ '''[[Media:UlotkaLoglan.pdf|Листівка Loglan'82]]''' 

|-
|♥ ''LEM'' - це назва нового дослідницького проєкту.
Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. [[специфікація LEM]]).
Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д. 
→ '''[[LЕM]]'''
|♥ Проєкт ''SpecVer'' має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer. 
→ '''[[SpеcVer]]'''
|}

{| class="wikitable"
|-
|♥ Бібліотека класів і математичних знань, корисних для програмістів. 
Візія майбутнього (ще один проєкт на роки роботи для багатьох людей).

Давайте почнемо з кількох питань: Чи можна вмістити математичні знання в комп'ютері? Чи можна вмістити інформатичні знання в комп'ютері? Дональд Кнут 70-х роках XX століття мав таку амбіцію, розпочинаючи створення своєї книги ''Мистецтво програмування''. Сьогодні, через майже 50 років, комп'ютерні знання зросли і здається неможливим, що їх можна вмістити в комп'ютері. Але, по-перше, комп'ютери тепер значно більші і швидші, ніж колись, а по-друге, існує комп'ютерна мережа (Здійснилася візія С. Лема з 50-х років). Це дозволяє нам перейти до створення ескізу концепції. 
Необхідно було б :
# Створити сховище знань, якими користуються розробники програмного забезпечення. Тут будуть знаходитися бібліотеки класів і методів, а також знання про структури даних, в яких проводяться обчислення. Це стосується як структур реляційних (алгебраїчних), що розглядаються математиками, так і структур даних, визначених і використовуваних інженерами програмного забезпечення.
# Створити мову, якою розробники програмного забезпечення будуть писати свої аргументи для (друкованих, розповсюджуваних, ...) повідомлень. Така мова повинна бути зрозумілою для людей і достатньо формалізованою, щоб була можливість комп'ютерного аналізу передставлених доказів.
# Інструмент для перевірки достовірності доказів. Буде потрібна програма proof checker, який суттєво відрізнятиметься від Mizara та йому подібних, оскільки докази будуть записані в рахунку програм (тобто в системі AL), який багатший за рахунок предикатів.
# Придумати спосіб збирання та поширення знань. Чи це має бути щось на кшталт математично-алгоритмічної пошукової системи Google?
|}

== Питання ==
Про функціональне програмування і тому подібне.
# Не розумію: мене переконують перейти на функціональне програмування. Що я від цього отримаю? Кажуть, у функціональному програмуванні відсутні побічні ефекти та операції присвоєння. І що з того? Чи існують інструменти для вираження властивостей, таких як: a) Обчислення буде закінчене, b) Набір визначень не містить протиріч, c) Результати будуть правильними, i т.д.
# У 1943 році Стівен Коул Кліні довів, що будь-яку рекурсивну функцію в розумінні Гьоделя-Гербранда можна виразити оператором мінімуму ефективного <math>\mu</math>. Чи це не означає, що в області натуральних (цілих) чисел функціональне програмування та програмування за допомогою операцій while i ін. визначають один і той самий набір обчислюваних функцій?
# Чи можна у функціональному програмуванні описати синтаксис такого класу програм, що обчислення будуть закінчені? Для ітераційного програмування (тобто структурного) такий критерій існує.
# Я прочитав такий вислів: ''Якби який-небуть тиран заборонив використання процедур та функцій, тоді вся інформатика зазнала б краху. Вони настільки важливі, що важко уявити програмування без використання процедур та функцій.'' Як це стосується теореми Кліні? тези Черча-Тюрінга?
# Вартість? Розглянемо послідовність Фібоначчі. Яка найкраща вартість обчислення n-го виразу цієї послідовності?
Щодо керування пам'яттю (збір сміття, висячі референції).
# Чи варто довільно вирішувати про відкидання інструкції, яка видаляє об'єкт?

Головна сторінка

2024-03-06T21:56:29Z

AnastasiiaSadlovska: Tłumaczenie Pytań

[[Plik:22px-English_language.svg.png]]
[[Main page]]     [[Plik:Flag of Poland.svg.png]][[ Strona główna]] 

Лотар [[Коллатц]] ( у 1937 році) мав рацію !

-------

== Карта ==
На цих сторінках ми представляємо чотири дослідницькі проєкти: Алгоритмічна логіка(з 1968), Loglan'82(з 1978), SpecVer(2007), Lem(2012).
Перші два проєкти дали багато результатів і будуть використовуватися ще багато років. 

{| class="wikitable"
|-
|♥ Дослідницький проєкт '''"Алгоритмічна логіка"''' займається відкриттям законів [[рахунок програм |рахунку програм]] і знаходить застосування у верифікації програм, тобто у доведенні істинності таких властивостей програм, як [[коректність]], відсутність циклів тощо. Мова алгоритмічної логіки дозволяє не лише виражати властивості алгоритмів (програм), а й забезпечує аксіоматизацію багатьох структур даних. Це стосується як відомих і необхідних в алгоритміці структур даних (наприклад, стеки, бінарні дерева пошуку, купи і т. д.), так і багатьох структур, що вивчаються в математиці. Можна вважати, що математика займається дослідженням, чи є дана формула <math> \alpha </math> істинною у даній структурі <math> \mathbb{A} </math>. Однак більшість структур не можна описати за допомогою аксіом, записаних у логіці першого порядку! Прийняття мови алгоритмічної логіки (або коротше, алгоритмічної мови) дозволяє представити ... 
→ '''[[Алгоритмічна логіка]]''' 
→ '''[[Media:UlotkaLogikaAlgorytmiczna.pdf| Листівка з алгоритмічної логіки]]'''

|width="50% " | ♥ Дослідницький проєкт '''"Loglan'82"''' сприяв створенню однойменної об'єктно-орієнтованої та розподіленої мови програмування. Публікація мови та розповсюдження компілятора передували дослідженням різних проблем.
Наведемо кілька прикладів: 

• Вирішення проблеми безпечного та ефективного вивільнення надлишкових об'єктів. 
• Вирішення проблеми (статичної) семантики, яка виникає, коли модулі класів можуть бути вкладеними (внутрішні класи) та розширеними (успадкування). 
• Оригінальний протокол взаємодії об'єктів процесів, які програміст може виділити в комп'ютерній мережі (alien call protocol). 
Мова Loglan була створена багато років до мов програмування C++ (1986) та Java (1995). Ці дві (та інші) мови програмування не узяли на озброєння рішень, відомих у Loglan протягом понад 30 років. Ознайомлення з Loglan може повністю змінити вашу думку про інженерію програмного забезпечення. Використовуючи знання та навички, які пропонує Loglan, ви можете значно підвищити свою кваліфікацію. 
→ '''[[Lоglan'82]]''' 
→ '''[[Media:UlotkaLoglan.pdf|Листівка Loglan'82]]''' 

|-
|♥ ''LEM'' - це назва нового дослідницького проєкту.
Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. [[специфікація LEM]]).
Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д. 
→ '''[[LЕM]]'''
|♥ Проєкт ''SpecVer'' має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer. 
→ '''[[SpеcVer]]'''
|}

{| class="wikitable"
|-
|♥ Бібліотека класів і математичних знань, корисних для програмістів. 
Візія майбутнього (ще один проєкт на роки роботи для багатьох людей).

Давайте почнемо з кількох питань: Чи можна вмістити математичні знання в комп'ютері? Чи можна вмістити інформатичні знання в комп'ютері? Дональд Кнут 70-х роках XX століття мав таку амбіцію, розпочинаючи створення своєї книги ''Мистецтво програмування''. Сьогодні, через майже 50 років, комп'ютерні знання зросли і здається неможливим, що їх можна вмістити в комп'ютері. Але, по-перше, комп'ютери тепер значно більші і швидші, ніж колись, а по-друге, існує комп'ютерна мережа (Здійснилася візія С. Лема з 50-х років). Це дозволяє нам перейти до створення ескізу концепції. 
Необхідно було б :
# Створити сховище знань, якими користуються розробники програмного забезпечення. Тут будуть знаходитися бібліотеки класів і методів, а також знання про структури даних, в яких проводяться обчислення. Це стосується як структур реляційних (алгебраїчних), що розглядаються математиками, так і структур даних, визначених і використовуваних інженерами програмного забезпечення.
# Створити мову, якою розробники програмного забезпечення будуть писати свої аргументи для (друкованих, розповсюджуваних, ...) повідомлень. Така мова повинна бути зрозумілою для людей і достатньо формалізованою, щоб була можливість комп'ютерного аналізу передставлених доказів.
# Інструмент для перевірки достовірності доказів. Буде потрібна програма proof checker, який суттєво відрізнятиметься від Mizara та йому подібних, оскільки докази будуть записані в рахунку програм (тобто в системі AL), який багатший за рахунок предикатів.
# Придумати спосіб збирання та поширення знань. Чи це має бути щось на кшталт математично-алгоритмічної пошукової системи Google?
|}

== Питання ==
Про функціональне програмування і тому подібне.
# Не розумію: мене переконують перейти на функціональне програмування. Що я від цього отримаю? Кажуть, у функціональному програмуванні відсутні побічні ефекти та операції присвоєння. І що з того? Чи існують інструменти для вираження властивостей, таких як: a) Обчислення буде закінчене, b) Набір визначень не містить протиріч, c) Результати будуть правильними, itp.
# У 1943 році Стівен Коул Кліні довів, що будь-яку рекурсивну функцію в розумінні Гьоделя-Гербранда можна виразити оператором мінімуму ефективного <math>\mu</math>. Чи це не означає, що в області натуральних (цілих) чисел функціональне програмування та програмування за допомогою операцій while i ін. визначають один і той самий набір обчислюваних функцій?
# Чи можна у функціональному програмуванні описати синтаксис такого класу програм, що обчислення будуть закінчені? Для ітераційного програмування (тобто структурного) такий критерій існує.
# Я прочитав такий вислів: ''Якби який-небуть тиран заборонив використання процедур та функцій, тоді вся інформатика зазнала б краху. Вони настільки важливі, що важко уявити програмування без використання процедур та функцій.'' Як це стосується теореми Кліні? тези Черча-Тюрінга?
# Вартість? Розглянемо послідовність Фібоначчі. Яка найкраща вартість обчислення n-го виразу цієї послідовності?
Щодо керування пам'яттю (збір сміття, висячі референції).
# Чи варто довільно вирішувати про відкидання інструкції, яка видаляє об'єкт?

Plik:UlotkaLogikaAlgorytmiczna.pdf

2024-03-05T23:43:33Z

AnastasiiaSadlovska: AnastasiiaSadlovska przesłano nową wersję pliku „Plik:UlotkaLogikaAlgorytmiczna.pdf“

Plik:UlotkaLoglan.pdf

2024-03-05T23:40:18Z

AnastasiiaSadlovska: AnastasiiaSadlovska przesłano nową wersję pliku „Plik:UlotkaLoglan.pdf“

Plik:UlotkaLoglan.pdf

2024-03-05T23:36:49Z

AnastasiiaSadlovska: AnastasiiaSadlovska przesłano nową wersję pliku „Plik:UlotkaLoglan.pdf“

Plik:UlotkaLogikaAlgorytmiczna.pdf

2024-03-05T23:35:42Z

AnastasiiaSadlovska: AnastasiiaSadlovska przesłano nową wersję pliku „Plik:UlotkaLogikaAlgorytmiczna.pdf“

Plik:UlotkaLogikaAlgorytmiczna.pdf

2024-03-05T23:32:28Z

AnastasiiaSadlovska: AnastasiiaSadlovska przesłano nową wersję pliku „Plik:UlotkaLogikaAlgorytmiczna.pdf“

Plik:UlotkaLogikaAlgorytmiczna.pdf

2024-03-05T23:31:01Z

AnastasiiaSadlovska: AnastasiiaSadlovska przesłano nową wersję pliku „Plik:UlotkaLogikaAlgorytmiczna.pdf“

Головна сторінка

2024-03-04T23:55:49Z

AnastasiiaSadlovska: Tłumaczenie 'Wizja przyszłości'

Головна сторінка

2024-03-04T23:11:29Z

AnastasiiaSadlovska: /* Мапа */

Головна сторінка

2024-03-04T22:51:34Z

AnastasiiaSadlovska:

Головна сторінка

2024-03-04T22:51:19Z

AnastasiiaSadlovska: Tłumaczenie LEM i SpecVer

[[Plik:22px-English_language.svg.png]]
[[Main page]]     [[Plik:Flag of Poland.svg.png]][[ Strona główna]] 

Лотар [[Коллатц]] ( у 1937 році) мав рацію !

-------

[[Plik:22px-English_language.svg.png]]
[[Main page]]     [[Plik:Flag of Poland.svg.png]][[ Strona główna]] 

Лотар [[Коллатц]] ( у 1937 році) мав рацію !

-------

== Мапа ==
На цих сторінках ми представляємо чотири дослідницькі проєкти: Алгоритмічна логіка(з 1968), Loglan'82(з 1978), SpecVer(2007), Lem(2012).
Перші два проєкти дали багато результатів і будуть використовуватися ще багато років. 

{| class="wikitable"
|-
|♥ Дослідницький проєкт '''"Алгоритмічна логіка"''' займається відкриттям законів [[рахунок програм |рахунку програм]] і знаходить застосування у верифікації програм, тобто у доведенні істинності таких властивостей програм, як [[коректність]], відсутність циклів тощо. Мова алгоритмічної логіки дозволяє не лише виражати властивості алгоритмів (програм), а й забезпечує аксіоматизацію багатьох структур даних. Це стосується як відомих і необхідних в алгоритміці структур даних (наприклад, стеки, бінарні дерева пошуку, купи і т. д.), так і багатьох структур, що вивчаються в математиці. Можна вважати, що математика займається дослідженням, чи є дана формула <math> \alpha </math> істинною у даній структурі <math> \mathbb{A} </math>. Однак більшість структур не можна описати за допомогою аксіом, записаних у логіці першого порядку! Прийняття мови алгоритмічної логіки (або коротше, алгоритмічної мови) дозволяє представити ... 
→ '''[[Алгоритмічна логіка]]''' 
→ '''[[Media:UlotkaLogikaAlgorytmiczna.pdf| Листівка з алгоритмічної логіки]]'''

|width="50% " | ♥ Дослідницький проєкт '''"Loglan'82"''' сприяв створенню однойменної об'єктно-орієнтованої та розподіленої мови програмування. Публікація мови та розповсюдження компілятора передували дослідженням різних проблем.
Наведемо кілька прикладів: 

• Вирішення проблеми безпечного та ефективного вивільнення надлишкових об'єктів. 
• Вирішення проблеми (статичної) семантики, яка виникає, коли модулі класів можуть бути вкладеними (внутрішні класи) та розширеними (успадкування). 
• Оригінальний протокол взаємодії об'єктів процесів, які програміст може виділити в комп'ютерній мережі (alien call protocol). 
Мова Loglan була створена багато років до мов програмування C++ (1986) та Java (1995). Ці дві (та інші) мови програмування не узяли на озброєння рішень, відомих у Loglan протягом понад 30 років. Ознайомлення з Loglan може повністю змінити вашу думку про інженерію програмного забезпечення. Використовуючи знання та навички, які пропонує Loglan, ви можете значно підвищити свою кваліфікацію. 
→ '''[[Lоglan'82]]''' 
→ '''[[Media:UlotkaLoglan.pdf|Листівка Loglan'82]]''' 

|-
|♥ LEM - це назва нового дослідницького проєкту.
Метою цього проєкту є вивчення можливості створення мови програмування з певними визначеними характеристиками (див. [[специфікація LEM]]).
Мова LEM має ґрунтуватися на досягненнях проекту Loglan'82 та використовувати найкращі аспекти об'єктно-орієнтованих мов програмування новіших поколінь: Java, C++, C#, Python і т.д. 
→ '''[[LЕM]]'''
|♥ Проєкт SpecVer має на меті підтвердити корисність застосування законів алгоритмічної логіки в інженерії програмного забезпечення. Мова LEM може виявитися корисною в роботі проєкту SpеcVer. 
→ '''[[SpеcVer]]'''
|}

Головна сторінка

2024-03-04T00:20:42Z

AnastasiiaSadlovska:

Головна сторінка

2024-03-04T00:11:08Z

AnastasiiaSadlovska: tłumaczenie o logicę informatycznej i Loglan`82

Головна сторінка

2024-03-03T17:52:41Z

AnastasiiaSadlovska: Pierwsze elementy strony

Strona główna

2024-03-03T17:43:21Z

AnastasiiaSadlovska:

[[Plik:22px-English_language.svg.png]]
[[Main page]]    [[Plik:ukrainian_language.png|22px]]
[[Головна сторінка]] 

<big><big>These pages are under permanent (re)construction.</big></big> 

Lothar [[Collatz]] (w roku 1937) miał rację !

-------

== Mapa ==
Na tych stronach przedstawiamy cztery projekty badawcze: Logika Algorytmiczna(od 1968), Loglan'82(od 1978), SpecVer(2007), Lem(2012).
Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat. 

{| class="wikitable"
|-
|♥ Projekt badawczy ''Logika Algorytmiczna'' zajmuje się odkrywaniem praw [[rachunek programów |rachunku programów]] i znajduje zastosowanie w weryfikacji programów tzn. w dowodzeniu prawdziwości takich własności programów jak [[poprawność]], niezapetlanie się i in. Język logiki algorytmicznej pozwala nie tylko wyrażać własności algorytmów(programów) ale także umożliwia aksjomatyzacje wielu struktur danych. Zarówno tych znanych i niezbędnych w algorytmice np. stosy, drzewa binarnych poszukiwań, kopce, etc. jak i wielu struktur badanych w matematyce. Można uznać, że matematyka zajmuje się badaniem, czy dana formuła <math> \alpha </math> jest prawdziwa w danej strukturze <math> \mathbb{A} </math>. Ale większośc struktur nie daje sie opisać przy pomocy aksjomatów zapisanych w języku pierwszego rzędu! Przyjęcie języka logiki algorytmicznej (krócej, języka algorytmicznego) umożliwia podanie ... 
→ '''[[Logika Algorytmiczna]]''' 
→ '''[[Media:UlotkaLogikaAlgorytmiczna.pdf| ulotka Logika Algorytmiczna]]'''

|width="50% " | ♥ Projekt badawczy '''Loglan'82''' wniósł język programowania obiektowego i rozproszonego o tej samej nazwie. Opublikowanie języka i dystrybucja kompilatora poprzedzone zostały badaniami problemów badawczych. Wymieńmy dla przykładu: 
• Rozwiązanie problemu bezpiecznej i efektywnej dealokacji niepotrzebnych obiektów.
• Rozwiązanie problemu (statycznej) semantyki jaki pojawia się gdy moduły klas mogą być zagnieżdżane (klasy wewnętrzne) i rozszerzane (dziedziczenie).
• Oryginalny protokół współpracy obiektów procesów, jakie programista może alokować w sieci komputerowej (protokół ''alien call''). Język Loglan powstał wiele lat przed językami C++(1986) i Java(1995). Te dwa (oraz inne) języki programowania nie przyswoiły sobie rozwiązań znanych w Loglanie od ponad 30 lat. Zapoznanie się z Loglanem może całkowicie zmienić Twój pogląd na inżynierię oprogramowania. Wykorzystując wiedzę i umiejętności oferowane przez Loglan możesz w znaczący sposób podnieść swoje kwalifikacje. 
→ '''[[Loglan'82]]''' 
→ '''[[Media:UlotkaLoglan.pdf|ulotka Loglan'82]]''' 

|-
|♥ LEM jest nazwą nowego projektu badawczego.
Celem tego projektu jest zbadanie czy można stworzyć język programowania o pewnych określonych cechach (zob. [[specyfikacja LEM]]).
Język LEM ma oprzeć się na osiągnięciach projektu Loglan'82 i wykorzystać to co dobre w językach programowania obiektowego nowszych generacji: Java, C++, C#, python etc. 
→ '''[[LEM]]'''
|♥ Projekt SpecVer ma potwierdzić przydatność stosowania praw logiki algorytmicznej w inżynierii oprogramowania. Język LEM może okazać się przydatny w pracach projektu SpecVer. 
→ '''[[SpecVer]]'''
|}

{| class="wikitable"
|-
|♥ Biblioteka klas i wiedzy matematycznej przydatnej programistiom. 
Wizja przyszłości (jeszcze jeden projekt na lata pracy dla wielu osób). 

Zacznijmy od paru pytań: Czy można zawrzeć wiedzę matematyczną w komputerze? Czy można zawrzeć wiedzę informatyczną w komputerze? D. Knuth w latach 70-tych XX wieku miał taką ambicję rozpoczynając tworzenie swojej ''The Art of Programming''. Dziś po prawie 50 latach wiedza informatyczna rozrosła się i wydaje się niemozliwym, by można ją było zawrzeć w komputerze. A jednak, po pierwsze komputery są znacznie większe i znacznie szybsze niż kiedyś, po drugie istnieje sieć komputerowa. (Spełniła sie wizja S. Lema z lat 50-tych). Pozwala to nam przejść do szkicowania koncepcji:
Należałoby :
# stworzyć magazyn wiedzy z jakiej korzystają twórcy oprogramowania. Znajdą się w nim biblioteki klas i metod i ponadto wiedza o strukturach danych w jakich przeprowadzane są obliczenia. Dotyczy to zarówno struktur relacyjnych (algebraicznych) rozpatrywanych przez matematyków jak i struktur danych definiowanych i wykorzystywanych przez inżynierów oprogramowania.
# stworzyć język w jakim twórcy oprogramowania będą zapisywac swoje argumenty na rzecz wygłaszanych (drukowanych, rozpowszechnianych, ...) komunikatów, Język taki powinien być czytelny dla ludzi i na tyle sformalizowany by możliwa była komputerowa analiza przedstawianych dowodów.
# narzędzie do weryfikacji poprawności dowodów. Potrzebny będzie proof checker, ale istotnie inny od Mizara i jemu podobnych, ponieważ dowody będą zapisywane w rachunku programów (tj. systemie AL) bogatszym od rachunku predykatów,
# obmyśleć sposób gromadzenia i udostępniania wiedzy. Czy ma to być swego rodzaju wyszukiwarka Google matematyczno-algorytmiczna?
|}

== Pytania ==
Na programowanie funkcyjne i temu podobne.
# Nie rozumiem: jestem namawiany do programowania funkcyjnego. Co na tym zyskam? Powiadają, w programowaniu funkcyjnym nie ma efektów ubocznych, ani instrukcji przypisania. No i co z tego? Czy istnieją narzędzia do wyrażenia własności takich jak: a) obliczenie będzie skończone, b) zestaw definicji nie zawiera sprzeczności, c) wyniki będa poprawne, itp.
# W r. 1943 S.C. Kleene udowodnił, że każda funkcja rekurencyjna w sensie Goedla-Herbranda jest wyrażalna przez operator minimum efektywnego <math>\mu</math>. Czy nie ozncza to tyle, że w dziedzinie liczb naturalnych (całkowitych) programowanie funkcyjne i programowanie za pomoca operacji while i in. definiuja ten sam zbiór ffunkcji obliczalnych?
# Czy w programowaniu funkcyjnym można opisać składnię takiej klasy programów, że obliczenia będą skończone? Dla programowania iteracyjnego (alias strukturalne) jest takie kryterium.
# Przeczytałem nastepujące zdania: ''Gdyby jakiś tyran zabronił stosowania procedur i funkcji, wówczas cała informatyka by padła. Są one tak ważnym narzędziem, że trudno sobie wyobrazić programowanie bez stosowania procedur i funkcji. '' Jak to się ma do twierdzenia Kleenego? do tezy Turinga-Churcha?
# Koszt? Weźmy pod uwagę funkcję (ciąg) Fibonacciego. Jaki jest najlepszy koszt obliczenia n-tego wyrazu tego ciągu?
W sprawie zarządzania pamięcią (odśmiecanie, wiszące referencje)
# Czy warto arbitralnie decydować o odrzuceniu instrukcji usuwającej obiekt?

Main page

2024-03-03T17:42:22Z

AnastasiiaSadlovska:

[[Plik:Flag of Poland.svg.png]][[ Strona główna]]
    [[Plik:ukrainian_language.png|22px]]
[[Головна сторінка]] 

Collatz conjecture is [http://lem12.uksw.edu.pl/images/3/37/CollatzConjecturebecomesTheorem20Nov23.pdf '''Collatz theorem'''] 

These pages are about four research programs that are intertwined each other. Two of projects have quite a history:
{| class="wikitable"
|-
|♥ ''Algorithmic Logic'' - also <big>program calculus</big>. Its aim is to study the laws of reasoning about programs, 
♥ '''[[Media:LeafletAlgorithmicLogic.pdf| Leaflet on Algorithmic Logic]]'''

[[Algorithmic Logic]]
|♥ Loglan'82- it is an object programming language that offers solutions of many problems of importance; 
• Problem of safe and efficient dealocation of not used objects. • Problem of static semantics of modules of classes that can be nested and extended. • An original protocol of communicating objects of processes. (''alien call'' protocols).
designed more than 30 years ago. 
♥ [[Loglan'82 project]] 
[[Media:LeafletLoglan.pdf|♥ have a look at a leaflet Loglan ]]
|-
|♥ LEM - a project that is aimed at a new programming language and environment, The language LEM is to apply the results of Loglan'82 project and to adapt the achievements of object programming languages of younger generations such as Java, C++, C#, Python, etc.
LEM may turn out to be useful in the works of another larger project ''SpecVer'' 

[[LEM]]
|♥ SpecVer - the project .
SpecVer project is to bring an environment for software engineers and mathematicians. 

[[SpecVer]]
|}

Main page

2024-03-03T17:36:28Z

AnastasiiaSadlovska:

[[Plik:Flag of Poland.svg.png]][[ Strona główna]] 
[[Plik:ukrainian_language.png|22px]]
[[Головна сторінка]] 

Collatz conjecture is [http://lem12.uksw.edu.pl/images/3/37/CollatzConjecturebecomesTheorem20Nov23.pdf '''Collatz theorem'''] 

These pages are about four research programs that are intertwined each other. Two of projects have quite a history:
{| class="wikitable"
|-
|♥ ''Algorithmic Logic'' - also <big>program calculus</big>. Its aim is to study the laws of reasoning about programs, 
♥ '''[[Media:LeafletAlgorithmicLogic.pdf| Leaflet on Algorithmic Logic]]'''

[[Algorithmic Logic]]
|♥ Loglan'82- it is an object programming language that offers solutions of many problems of importance; 
• Problem of safe and efficient dealocation of not used objects. • Problem of static semantics of modules of classes that can be nested and extended. • An original protocol of communicating objects of processes. (''alien call'' protocols).
designed more than 30 years ago. 
♥ [[Loglan'82 project]] 
[[Media:LeafletLoglan.pdf|♥ have a look at a leaflet Loglan ]]
|-
|♥ LEM - a project that is aimed at a new programming language and environment, The language LEM is to apply the results of Loglan'82 project and to adapt the achievements of object programming languages of younger generations such as Java, C++, C#, Python, etc.
LEM may turn out to be useful in the works of another larger project ''SpecVer'' 

[[LEM]]
|♥ SpecVer - the project .
SpecVer project is to bring an environment for software engineers and mathematicians. 

[[SpecVer]]
|}

Main page

2024-03-03T17:35:35Z

AnastasiiaSadlovska: Wycofano edycje użytkownika AnastasiiaSadlovska (dyskusja). Autor przywróconej wersji to AndrzejSalwicki.

[[Plik:Flag of Poland.svg.png]][[Strona_główna]] 
Collatz conjecture is [http://lem12.uksw.edu.pl/images/3/37/CollatzConjecturebecomesTheorem20Nov23.pdf '''Collatz theorem'''] 

These pages are about four research programs that are intertwined each other. Two of projects have quite a history:
{| class="wikitable"
|-
|♥ ''Algorithmic Logic'' - also <big>program calculus</big>. Its aim is to study the laws of reasoning about programs, 
♥ '''[[Media:LeafletAlgorithmicLogic.pdf| Leaflet on Algorithmic Logic]]'''

[[Algorithmic Logic]]
|♥ Loglan'82- it is an object programming language that offers solutions of many problems of importance; 
• Problem of safe and efficient dealocation of not used objects. • Problem of static semantics of modules of classes that can be nested and extended. • An original protocol of communicating objects of processes. (''alien call'' protocols).
designed more than 30 years ago. 
♥ [[Loglan'82 project]] 
[[Media:LeafletLoglan.pdf|♥ have a look at a leaflet Loglan ]]
|-
|♥ LEM - a project that is aimed at a new programming language and environment, The language LEM is to apply the results of Loglan'82 project and to adapt the achievements of object programming languages of younger generations such as Java, C++, C#, Python, etc.
LEM may turn out to be useful in the works of another larger project ''SpecVer'' 

[[LEM]]
|♥ SpecVer - the project .
SpecVer project is to bring an environment for software engineers and mathematicians. 

[[SpecVer]]
|}

Main page

2024-03-03T17:34:22Z

AnastasiiaSadlovska: Dodanie ukraińskiej flagi

[[Plik:Flag of Poland.svg.png]][[ Strona główna]] 
[[Plik:ukrainian_language.png|22px]]
[[Головна сторінка]] 
Collatz conjecture is [http://lem12.uksw.edu.pl/images/3/37/CollatzConjecturebecomesTheorem20Nov23.pdf '''Collatz theorem'''] 

These pages are about four research programs that are intertwined each other. Two of projects have quite a history:
{| class="wikitable"
|-
|♥ ''Algorithmic Logic'' - also <big>program calculus</big>. Its aim is to study the laws of reasoning about programs, 
♥ '''[[Media:LeafletAlgorithmicLogic.pdf| Leaflet on Algorithmic Logic]]'''

[[Algorithmic Logic]]
|♥ Loglan'82- it is an object programming language that offers solutions of many problems of importance; 
• Problem of safe and efficient dealocation of not used objects. • Problem of static semantics of modules of classes that can be nested and extended. • An original protocol of communicating objects of processes. (''alien call'' protocols).
designed more than 30 years ago. 
♥ [[Loglan'82 project]] 
[[Media:LeafletLoglan.pdf|♥ have a look at a leaflet Loglan ]]
|-
|♥ LEM - a project that is aimed at a new programming language and environment, The language LEM is to apply the results of Loglan'82 project and to adapt the achievements of object programming languages of younger generations such as Java, C++, C#, Python, etc.
LEM may turn out to be useful in the works of another larger project ''SpecVer'' 

[[LEM]]
|♥ SpecVer - the project .
SpecVer project is to bring an environment for software engineers and mathematicians. 

[[SpecVer]]
|}

Strona główna

2024-03-03T17:30:26Z

AnastasiiaSadlovska: Dodanie flagi

[[Plik:22px-English_language.svg.png]]
[[Main page]] 
[[Plik:ukrainian_language.png|22px]]
[[Головна сторінка]] 

<big><big>These pages are under permanent (re)construction.</big></big> 

Lothar [[Collatz]] (w roku 1937) miał rację !

-------

== Mapa ==
Na tych stronach przedstawiamy cztery projekty badawcze: Logika Algorytmiczna(od 1968), Loglan'82(od 1978), SpecVer(2007), Lem(2012).
Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat. 

{| class="wikitable"
|-
|♥ Projekt badawczy ''Logika Algorytmiczna'' zajmuje się odkrywaniem praw [[rachunek programów |rachunku programów]] i znajduje zastosowanie w weryfikacji programów tzn. w dowodzeniu prawdziwości takich własności programów jak [[poprawność]], niezapetlanie się i in. Język logiki algorytmicznej pozwala nie tylko wyrażać własności algorytmów(programów) ale także umożliwia aksjomatyzacje wielu struktur danych. Zarówno tych znanych i niezbędnych w algorytmice np. stosy, drzewa binarnych poszukiwań, kopce, etc. jak i wielu struktur badanych w matematyce. Można uznać, że matematyka zajmuje się badaniem, czy dana formuła <math> \alpha </math> jest prawdziwa w danej strukturze <math> \mathbb{A} </math>. Ale większośc struktur nie daje sie opisać przy pomocy aksjomatów zapisanych w języku pierwszego rzędu! Przyjęcie języka logiki algorytmicznej (krócej, języka algorytmicznego) umożliwia podanie ... 
→ '''[[Logika Algorytmiczna]]''' 
→ '''[[Media:UlotkaLogikaAlgorytmiczna.pdf| ulotka Logika Algorytmiczna]]'''

|width="50% " | ♥ Projekt badawczy '''Loglan'82''' wniósł język programowania obiektowego i rozproszonego o tej samej nazwie. Opublikowanie języka i dystrybucja kompilatora poprzedzone zostały badaniami problemów badawczych. Wymieńmy dla przykładu: 
• Rozwiązanie problemu bezpiecznej i efektywnej dealokacji niepotrzebnych obiektów.
• Rozwiązanie problemu (statycznej) semantyki jaki pojawia się gdy moduły klas mogą być zagnieżdżane (klasy wewnętrzne) i rozszerzane (dziedziczenie).
• Oryginalny protokół współpracy obiektów procesów, jakie programista może alokować w sieci komputerowej (protokół ''alien call''). Język Loglan powstał wiele lat przed językami C++(1986) i Java(1995). Te dwa (oraz inne) języki programowania nie przyswoiły sobie rozwiązań znanych w Loglanie od ponad 30 lat. Zapoznanie się z Loglanem może całkowicie zmienić Twój pogląd na inżynierię oprogramowania. Wykorzystując wiedzę i umiejętności oferowane przez Loglan możesz w znaczący sposób podnieść swoje kwalifikacje. 
→ '''[[Loglan'82]]''' 
→ '''[[Media:UlotkaLoglan.pdf|ulotka Loglan'82]]''' 

|-
|♥ LEM jest nazwą nowego projektu badawczego.
Celem tego projektu jest zbadanie czy można stworzyć język programowania o pewnych określonych cechach (zob. [[specyfikacja LEM]]).
Język LEM ma oprzeć się na osiągnięciach projektu Loglan'82 i wykorzystać to co dobre w językach programowania obiektowego nowszych generacji: Java, C++, C#, python etc. 
→ '''[[LEM]]'''
|♥ Projekt SpecVer ma potwierdzić przydatność stosowania praw logiki algorytmicznej w inżynierii oprogramowania. Język LEM może okazać się przydatny w pracach projektu SpecVer. 
→ '''[[SpecVer]]'''
|}

{| class="wikitable"
|-
|♥ Biblioteka klas i wiedzy matematycznej przydatnej programistiom. 
Wizja przyszłości (jeszcze jeden projekt na lata pracy dla wielu osób). 

Zacznijmy od paru pytań: Czy można zawrzeć wiedzę matematyczną w komputerze? Czy można zawrzeć wiedzę informatyczną w komputerze? D. Knuth w latach 70-tych XX wieku miał taką ambicję rozpoczynając tworzenie swojej ''The Art of Programming''. Dziś po prawie 50 latach wiedza informatyczna rozrosła się i wydaje się niemozliwym, by można ją było zawrzeć w komputerze. A jednak, po pierwsze komputery są znacznie większe i znacznie szybsze niż kiedyś, po drugie istnieje sieć komputerowa. (Spełniła sie wizja S. Lema z lat 50-tych). Pozwala to nam przejść do szkicowania koncepcji:
Należałoby :
# stworzyć magazyn wiedzy z jakiej korzystają twórcy oprogramowania. Znajdą się w nim biblioteki klas i metod i ponadto wiedza o strukturach danych w jakich przeprowadzane są obliczenia. Dotyczy to zarówno struktur relacyjnych (algebraicznych) rozpatrywanych przez matematyków jak i struktur danych definiowanych i wykorzystywanych przez inżynierów oprogramowania.
# stworzyć język w jakim twórcy oprogramowania będą zapisywac swoje argumenty na rzecz wygłaszanych (drukowanych, rozpowszechnianych, ...) komunikatów, Język taki powinien być czytelny dla ludzi i na tyle sformalizowany by możliwa była komputerowa analiza przedstawianych dowodów.
# narzędzie do weryfikacji poprawności dowodów. Potrzebny będzie proof checker, ale istotnie inny od Mizara i jemu podobnych, ponieważ dowody będą zapisywane w rachunku programów (tj. systemie AL) bogatszym od rachunku predykatów,
# obmyśleć sposób gromadzenia i udostępniania wiedzy. Czy ma to być swego rodzaju wyszukiwarka Google matematyczno-algorytmiczna?
|}

== Pytania ==
Na programowanie funkcyjne i temu podobne.
# Nie rozumiem: jestem namawiany do programowania funkcyjnego. Co na tym zyskam? Powiadają, w programowaniu funkcyjnym nie ma efektów ubocznych, ani instrukcji przypisania. No i co z tego? Czy istnieją narzędzia do wyrażenia własności takich jak: a) obliczenie będzie skończone, b) zestaw definicji nie zawiera sprzeczności, c) wyniki będa poprawne, itp.
# W r. 1943 S.C. Kleene udowodnił, że każda funkcja rekurencyjna w sensie Goedla-Herbranda jest wyrażalna przez operator minimum efektywnego <math>\mu</math>. Czy nie ozncza to tyle, że w dziedzinie liczb naturalnych (całkowitych) programowanie funkcyjne i programowanie za pomoca operacji while i in. definiuja ten sam zbiór ffunkcji obliczalnych?
# Czy w programowaniu funkcyjnym można opisać składnię takiej klasy programów, że obliczenia będą skończone? Dla programowania iteracyjnego (alias strukturalne) jest takie kryterium.
# Przeczytałem nastepujące zdania: ''Gdyby jakiś tyran zabronił stosowania procedur i funkcji, wówczas cała informatyka by padła. Są one tak ważnym narzędziem, że trudno sobie wyobrazić programowanie bez stosowania procedur i funkcji. '' Jak to się ma do twierdzenia Kleenego? do tezy Turinga-Churcha?
# Koszt? Weźmy pod uwagę funkcję (ciąg) Fibonacciego. Jaki jest najlepszy koszt obliczenia n-tego wyrazu tego ciągu?
W sprawie zarządzania pamięcią (odśmiecanie, wiszące referencje)
# Czy warto arbitralnie decydować o odrzuceniu instrukcji usuwającej obiekt?

Plik:Ukrainian language.png

2024-03-03T17:18:07Z

AnastasiiaSadlovska: