Ścieżka do metod formalnych

Często zdarza się, że studenci rozpoczynają doktoraty z ograniczonym doświadczeniem w matematyce i formalnych aspektach informatyki. Oczywiście takim studentom bardzo trudno będzie zostać teoretycznym informatykiem, ale dobrze by było, gdyby mogli się zorientować w stosowaniu metod formalnych i czytaniu artykułów zawierających metody formalne.

Jaka jest dobra, krótkoterminowa ścieżka, którą mogą podążać rozpoczynający doktoranci, aby uzyskać ekspozycję wymaganą do przeczytania prac przy użyciu metod formalnych i ostatecznie pisania prac przy użyciu takich metod?

Jeśli chodzi o kontekst, myślę bardziej w kategoriach teorii B i weryfikacji formalnej jako rodzajów rzeczy, których powinni się nauczyć, ale także klasycznych tematów TCS, takich jak teoria automatów.

W przedmowie swojej książki „Odkrycie matematyczne, zrozumienie, uczenie się i rozwiązywanie problemów nauczania” George Pólya pisze:

Rozwiązywanie problemów jest praktyczną sztuką, taką jak pływanie, jazda na nartach lub gra na pianinie: możesz się tego nauczyć, naśladując i ćwicząc. Ta książka nie może zaoferować magicznego klucza, który otwiera wszystkie drzwi i rozwiązuje wszystkie problemy, ale oferuje dobre przykłady naśladowania i wiele okazji do ćwiczeń: jeśli chcesz nauczyć się pływać, musisz wejść do wody, a jeśli chcesz stać się rozwiązaniem problemu, musisz rozwiązać problemy.

Myślę, że nie ma krótkiej ścieżki, szczególnie do osiągnięcia stanu pisania. Wymaga praktyki, dużo tego.

Niektóre wskazówki:

Jeśli „ograniczony tło w matematyce i formalne aspekty” oznacza „nie ma dowodu pomyślany i napisany w dół”, a następnie coś jak to może być początek.

Jeśli coś w arkuszu ściągowym teoretycznej informatyki sprawia, że ​​uczeń czuje się nieswojo, wskazany byłby kurs odświeżający odpowiedni dział matematyki.

Istnieje wiele źródeł pisania matematycznego: być może notatki z wykładu z kursu z 1978 roku na Uniwersytecie Stanforda CS209. Lub ten artykuł autorstwa Paula Halmosa.

Metody formalne, takie jak Z, B, TLA, CafeObj, polegają w dużej mierze na teorii mnogości, logice, teorii kategorii, rachunku lambda i automatach do modelowania pojęć typów, danych i obliczeń.

Możesz albo przejść do obszernej monografii, takiej jak Logics of Specification Languages, autorstwa Dines Bjørner i Martina C. Hensona, red., Monographs in Theoretical Computer Science, Springer Verlag, 2008 i uczyć się, jak potrzebujesz, i korzystać z cytowanych tam referencji. Lub naucz się jednego tematu naraz:

1. Ustaw teorię
2. Logika matematyczna
3. Logika czasowa
4. Algebra uniwersalna
5. Rachunek Lambda
6. Teoria kategorii

Naprawdę uważam, że „formalne” metody nie są zbyt dobrym pomysłem do celów edukacyjnych. W tym przypadku programowanie komputera jest metodą „formalną”. Czy odnosi sukces jako narzędzie edukacyjne?

Potrzebne jest zrozumienie, intuicja i umiejętność radzenia sobie z abstrakcją. Metody formalne utrudniają to wszystko. Zamiast tego promują próbę i błąd, hackowanie, dopasowywanie wzorców, naśladowanie, koncentrację na składni. Lista jest długa.

Każdy element rygorystycznej matematyki nauczy ludzi, jak prawidłowo rozumować. Im prostsza domena, tym lepiej. Wszystko, czego nauczyłem się o rozumowaniu, którego nauczyłem się w szkole średniej, kiedy poważnie zajmowałem się geometrią euklidesową. Rachunek i algebra liniowa na uniwersytecie zrobiły resztę.

Inną atrakcyjną alternatywą jest logika filozoficzna, w której uczą ludzi, jak myśleć o wypowiedziach i rozumieć, jaka jest treść informacji i co jest tego konsekwencją. Robią to bez utopienia studentów w symbolach.

Jeśli podsumujesz wszystkich najlepszych informatyków, zdziwisz się, ilu z nich ma formalne wykształcenie filozoficzne. Tracimy to wszystko teraz, ponieważ studenci filozofii uważają teraz Informatykę za przedmiot doczesny. Zmuszenie naszych uczniów do nauki filozofii może temu przeciwdziałać. Poproś ich, aby przepracowali Historię zachodniej filozofii Bertranda Russella . To zdziała cuda.

Jeśli pracują nad teorią języka programowania, możesz też poprosić o przeczytanie Quine'a, którego uważam za „boskiego ojca” semantyki denotacyjnej. (Quine zasadniczo tworzył denotacyjną semantykę języka naturalnego w Word and Object , co było ogromnym źródłem inspiracji dla Christophera Stracheya. Ale ta książka jest dość trudna.) Edytowana kolekcja Quintessence jest dobrym źródłem pomysłów Quine'a dla początkujących.

[Uwaga dodana: Jedną z zalet filozofii nad matematyką jest to, że uczniowie widzą debatę , tzn. Widzą argument „właściwy” i argument „zły”, a eksperci wybijają niewłaściwe. W matematyce nigdy nie można dostrzec błędnego argumentu, który ogranicza jego wartość edukacyjną.]