Strona główna: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Nie pokazano 107 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 1: Linia 1:
<p style="text-align: right;">[[Plik:22px-English_language.svg.png]]
+
<p style="text-align: left;">[[Plik:22px-English_language.svg.png]]
 
[[Main page]]  </p>
 
[[Main page]]  </p>
 +
<big><big><span style="color: Red">These pages are under permanent  (re)construction.</span></big></big><br />
 +
 +
UWAGA! nowy i jeszcze "ciepły" wynik -- Lothar  Collatz w roku 1937 miał rację !
 +
Pierwsza wersja dowodu. http://lem12.uksw.edu.pl/images/2/24/Na_twierdzenie_Collatza.pdf
  
 +
-------
 +
Materiały do seminarium 26 maja 2020: http://lem12.uksw.edu.pl/wiki/Plik:SlajdyPawel26maj.pdf<br />
 +
Artykuł o programie: http://lem12.uksw.edu.pl/images/5/5c/NPawel.pdf<br />
 +
 +
== 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.
+
Dwa pierwsze projekty przyniosły wiele wyników i będą stosowane przez wiele lat.<br />
{|class="wikitable"
+
|-
+
 
|♥ Projekt ''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 ...<br />
+
{| class="wikitable"
'''[[Logika Algorytmiczna]]'''
+
|-  
|♥ Projekt Loglan'82 zaowocował sformułowaniem języka programowania obiektowego na wiele lat przed powstaniem języków C++ i Java. Co więcej, Loglan zawiera wiele rozwiązań nieznanych w innych językach programowania.<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 />
'''[[Loglan'82]]'''
+
'''[[Logika Algorytmiczna]]''' <br />
 +
→ '''[[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:<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 />
 +
→ '''[[Media:UlotkaLoglan.pdf|ulotka Loglan'82]]'''<br />
 +
 
|-
 
|-
 
|♥ LEM jest nazwą nowego projektu badawczego.
 
|♥ 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]]).
 
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.<br />
 
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.<br />
'''[[LEM]]'''
+
'''[[LEM]]'''
|♥ Projekt SpecVer ma potwierdzić przydatność  stosowania praw logiki algorytmicznej w inżynierii oprogramowania. LEM może okazać się przydatny w pracach  projektu SpecVer.<br />
+
|♥ 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.<br />
'''[[SpecVer]]'''
+
'''[[SpecVer]]'''
 
|}
 
|}
 +
 +
{|  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ł 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?

Wersja z 21:02, 28 lip 2021

22px-English language.svg.png Main page

These pages are under permanent (re)construction.

UWAGA! nowy i jeszcze "ciepły" wynik -- Lothar Collatz w roku 1937 miał rację ! Pierwsza wersja dowodu. http://lem12.uksw.edu.pl/images/2/24/Na_twierdzenie_Collatza.pdf


Materiały do seminarium 26 maja 2020: http://lem12.uksw.edu.pl/wiki/Plik:SlajdyPawel26maj.pdf
Artykuł o programie: http://lem12.uksw.edu.pl/images/5/5c/NPawel.pdf

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 ...

Logika Algorytmiczna
ulotka Logika Algorytmiczna

♥ 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
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

♥ 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 :

  1. 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.
  2. 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.
  3. 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,
  4. 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.

  1. 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.
  2. 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?
  3. 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.
  4. 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?
  5. 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)

  1. Czy warto arbitralnie decydować o odrzuceniu instrukcji usuwającej obiekt?