Strona główna: Różnice pomiędzy wersjami
(→Pytania) |
|||
(Nie pokazano 25 wersji utworzonych przez 2 użytkowników) | |||
Linia 1: | Linia 1: | ||
<p style="text-align: left;">[[Plik:22px-English_language.svg.png]] | <p style="text-align: left;">[[Plik:22px-English_language.svg.png]] | ||
− | [[Main page]] </p> | + | [[Main page]] [[Plik:ukrainian_language.png|22px]] |
+ | [[Головна сторінка]] | ||
+ | [[Page d'accueil]] </p> | ||
+ | |||
+ | |||
+ | |||
<big><big><span style="color: Red">These pages are under permanent (re)construction.</span></big></big><br /> | <big><big><span style="color: Red">These pages are under permanent (re)construction.</span></big></big><br /> | ||
+ | Lothar [[Collatz]] (<small>w roku 1937</small>) miał rację ! | ||
+ | |||
+ | ------- | ||
+ | |||
+ | == Mapa == | ||
Na tych stronach przedstawiamy cztery projekty badawcze: Logika Algorytmiczna(od 1968), Loglan'82(od 1978), SpecVer(2007), Lem(2012). | 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.<br /> | Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat.<br /> | ||
Linia 42: | Linia 52: | ||
# obmyśleć sposób gromadzenia i udostępniania wiedzy. Czy ma to być swego rodzaju wyszukiwarka Google matematyczno-algorytmiczna? | # obmyśleć sposób gromadzenia i udostępniania wiedzy. Czy ma to być swego rodzaju wyszukiwarka Google matematyczno-algorytmiczna? | ||
|} | |} | ||
− | |||
− | |||
== Pytania == | == Pytania == | ||
− | # Nie rozumiem: jestem namawiany do programowania funkcyjnego. Co na tym zyskam? Powiadają, w programowaniu funkcyjnym nie ma efektów ubocznych, ani instrukcji przypisania. No | + | Na programowanie funkcyjne i temu podobne. |
− | Czy istnieją narzędzia do wyrażenia własności takich jak: | + | # 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? | # 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? |
Aktualna wersja na dzień 19:45, 25 kwi 2024
Main page
Головна сторінка
Page d'accueil
These pages are under permanent (re)construction.
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.
♥ Projekt badawczy Logika Algorytmiczna zajmuje się odkrywaniem praw 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 ... |
♥ 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. |
♥ 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. |
♥ 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 |
♥ 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 :
|
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?