Menu główne
Wykłady wprowadzające do projektu Lingua
- Utworzono: sobota, 25 styczeń 2025 17:20
- Poprawiono: sobota, 29 marzec 2025 14:00
- Odsłony: 351
Wykłady wprowadzające do Projektu Lingua zostały przygotowane i wygłoszone na forum jego zespołu. Poniżej znajduje się lista tych wykładów uporządkowana w kolejności chronologicznej. Poza streszczeniami wykładów zawiera ona liki do pobrania prezentacji i odsłuchania nagrań video.
Wprowadzenie do idei projektu
Ponieważ pierwsze spotkanie grupy Lingua nie było nagrywane, podaję poniżej linki do dwóch moich krótkich wykładów i jednej rozmowy poświęconych idei i filozofii projektu.
- krótkie video-zaproszenie do projektu (ca. 4 min.) Zobacz.
- nieco pełniejsze video-zaproszenie do projektu (ca. 24 min.) Zobacz.
- rozmowa o projekcie ze scrum-masterem (ca. 55 min) Zobacz
2025 01 25 O technicznych fundamentach projektu
W wykładzie pokazuję na bardzo prostych przykładach dwie metody stanowiące fundament projektu:
- Metodę takiego projektowania języka programowania, aby istniała dla niego semantyka denotacyjna. Język jest projektowany w kolejności odwrotnej w stosunku do zwyczajowej, a mianowicie od denotacji do składni.
- Metodę konstruowania programów dającą gwarancję, że programy są funkcyjnie poprawne. Narzędzia dla takiej metody można zbudować dla języków mających semantyki denotacyjne.
2025 02 01 Podstawowe założenia o projekcie oraz trzy pierwsze warstwy denotacyjne
Wykład zaczyna się od sformułowania podstawowych założeń technicznych o języku Lingua, np. że jest silnie utypowiony, a następnie omawiam trzy pierwsze denotacyjne warstwy (algebry) języka:
- rodzaje danych, na których nasze programy będą operować, i ich konstruktory,
- typy danych rozumiane jako niezależne byty matematyczne i ich konstruktory,
- dane utypowione rozumiane jako pary składające się z danej i jej typu i ich konstruktory.
Dane utypowione stanowią szczególną kategorię elementów zwanych "wartościami". Będą one przypisywane zmiennym przy ich inicjalizacji oraz generowane przez wyrażenia w wyniku ich wykonywania.
2025 02 08 Jarzma, obiekty, klasy i stany
Stany stanowią jedno z centralnych pojęć naszego modelu, bo denotacje większości elementów naszego języka to funkcje przyjmujące stany jako argumenty i oddające bądź wartości, referencje, typy i jarzma (wyrażenia), bądź też stany (instrukcje, deklaracje i programy). To nadal dość techniczny wykład — jak poprzedni — jednakże trzeba przez niego przebrnąć, by już niedługo zacząć mówić o denotacjach. Tym razem zrezygnowałem ze streszczenia przygotowywanego przez AI, bo obawiam się, że może tylko namieszać.
2025 02 15 Stosowalność (usability) i widoczność (visibility) przedmiotów (items)
Przedmiotami w naszym modelu nazywam wartości, referencje, typy i procedury. Ich stosowalność jest opisywana (ustalana) przez mechanizm typów, a widoczność — przez mechanizm prywatności. W wykładzie omawiam podstawowe reguły stosowalności i widoczności. Ta część wykładu ma charakter raczej nieformalny. Na koniec pokazuję przykład stanu publicznego pamięci, a także stanu lokalnego dla wywołania procedury. Po wykładzie wywiązała się ciekawa dyskusja ze słuchaczami.
2025 02 22 Denotacje wyrażeń
W naszym modelu mamy trzy kategorie wyrażeń różniące się tym, jakie wyniki zwracają przy ich wyliczniu: wyrażenia wartościologiczne (zwracają wartości), wyrażenia typologiczne, jarzmowe i referencyjne. W wykładzie pokazuję czym są denotacje takich wyrażeń iraz przykłady ich kontruktorów z pominięciem jednak konstruktorów wyrażeń jarzmowych, które są technicznie dość złożone. Również po tym wykładzie wywiązała się ciekawa dyskusja, która miała swoją kontynuację na naszym serwerze Discord.
2025 03 01 Denotacje instrukcji i metody (cz.1)
Wykład składa się z dwóch części poświęconych kolejno denotacjom instrukcji i metodom.
Denotacje instrukcji są funkcjami częściowymi ze stanów w stany. W wykładzie pokazuję konstruktory denotacji instrukcji przypisania, instrukcji warunkowej i instrukcji pętli while. Pokazuję też konstruktor denotacji instrukcji warunkowej if-error służącej do obsługi błędów. Instrukcje wywołania procedur zostaną omówione w dalszych wykładach, razem z procedurami.
W wykładzie dotyczących metod wymieniam trzy ich kategorie: metody imperatywne, obiektowe i funkcyjne. Każda z takich metod może być konkretna (procedura) i abstrakcyjna (sygnatura). Omawiam też, na poziomie intuicyjnym, funkcjonowanie medod imperatywnych.
- Pobierz prezentację poświęconą instrukcjom
- Pobierz prezentację poświęconą metodom
- Zobacz video (obejmuje oba wykłady)
2025 03 22 Metody i denotacje deklaracji
Ponieważ w dniu 8 marca zapomniałem włączyć nagrywanie, a w dniu wykład się nie odbył z powodu prowadzonego przeze mnie całodzennego szkolenia gdzieindziej, w dniu 22 marca szybko powtórzyłem wykład o metodach. Następnie (też w pewnym skrócie) opowiedziałem o deklaracjach. Tym samym zakończyłem tę część wykładu, która była poświęcona modelowi denotacyjnemu. Rozdziału 7 poświęconego składni ne będę w ogóle omawiał, bo czytanie gramatyki na wykładzie byłobyh dość nudne. Tę część możecie szybko przekartkowa sami. Na kolejnym wykładzie zaję się tym co stanowi drugi filar naszej metody,m a więc zagadnieniem poprawności programów.
- Pobierz prezentację poświęconą metodom
- Pobierz prezentację poświęconą deklaracjom
- Zobacz video obejmujące oba wykłady
2025 03 29 Zbiory łańcuchowo-zupełne i relacyjny model poprawności
Zbiory łańcuchowo-zupełne to algebry o specyficznych własnościach, których elementy możde definiować równaniami stałopunktowymi postaci x = f.x. Przy pomocy takich równań definiujemy języki formalne, dziedziny denotacyjne a także wiele funkcji. Z kolei relacyjny model poprawności, to model, w którym programy są rerezentowane przez relacje binarne na stanach (abstrakcyjnych), a warunki, czyli predykaty, przez zbiory stanów. W tym modelu w bardzo prosty i elegancki sposób daje się zdefiniować pojęcia poprawoności programów, a także sformułować i udowodnić podstawowe twierdzenia o budowaniu programów poprawnych.