Strona główna: Różnice pomiędzy wersjami
Z Lem
| (Nie pokazano 85 wersji utworzonych przez 2 użytkowników) | |||
| Linia 1: | Linia 1: | ||
| − | <p style="text-align: | + | <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 /> | ||
| − | < | + | Nie lękajcie się rachunku programów, bo przed nim kolosalna przyszłość!<br /> |
| + | |||
| + | Lothar [[Collatz]] (<small>w roku 1937</small>) miał rację ! | ||
| + | |||
| + | ------- | ||
| + | |||
| + | |||
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. | + | Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat.<br /> |
| + | |||
| + | |||
{| class="wikitable" | {| class="wikitable" | ||
|- | |- | ||
| − | |♥ Projekt ''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 ...<br /> | + | |♥ 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 ...<br /> |
→ '''[[Logika Algorytmiczna]]''' <br /> | → '''[[Logika Algorytmiczna]]''' <br /> | ||
→ '''[[Media:UlotkaLogikaAlgorytmiczna.pdf| ulotka Logika Algorytmiczna]]''' | → '''[[Media:UlotkaLogikaAlgorytmiczna.pdf| ulotka Logika Algorytmiczna]]''' | ||
| − | |width="50% " | ♥ | + | |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:<br /> |
| + | • 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. <br /> | ||
→ '''[[Loglan'82]]'''<br /> | → '''[[Loglan'82]]'''<br /> | ||
| − | → '''[[Media:UlotkaLoglan.pdf|ulotka Loglan'82]]''' | + | → '''[[Media:UlotkaLoglan.pdf|ulotka Loglan'82]]'''<br /> |
| + | |||
|- | |- | ||
|♥ LEM jest nazwą nowego projektu badawczego. | |♥ LEM jest nazwą nowego projektu badawczego. | ||
| Linia 24: | Linia 41: | ||
|} | |} | ||
| − | Wizja przyszłości(jeszcze jeden projekt na lata dla wielu osób).<br /> | + | {| class="wikitable" |
| + | |- | ||
| + | |♥ Biblioteka klas i wiedzy matematycznej przydatnej programistiom. <br /> | ||
| + | Wizja przyszłości (jeszcze jeden projekt na lata pracy dla wielu osób).<br /> | ||
| − | 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ł | + | 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 : | |
| − | # magazyn wiedzy z jakiej korzystają twórcy oprogramowania. Znajdą się w nim biblioteki klas i metod i ponadto . | + | # 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. | # 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 | + | # 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? | # 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? | ||
Aktualna wersja na dzień 18:04, 3 paź 2024
Main page 
Головна сторінка
Page d'accueil
These pages are under permanent (re)construction.
Nie lękajcie się rachunku programów, bo przed nim kolosalna przyszłość!
Lothar Collatz (w roku 1937) miał rację !
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?
