| 12345678910111213141516 |
- \chapter{Zakończenie} \label{chap:zakonczenie}
- Rozdział przedstawia podsumowanie pracy, zwłaszcza rozdziału \ref{chap:wykonanie}.
- \section{Zwycięstwa i wkład} \label{sec:dokonania}
- Twierdzenia opisane w rozdziale \ref{chap:wykonanie}, a zatem: \ref{thm:kern-subgroup}, \ref{thm:quotient-group-is--a-group}, \ref{thm:II-1-1}, \ref{thm:II-1-2}, \ref{thm:cosets-norm-eq},\ref{thm:hom-induces-ideal}, \ref{thm:quotient-ring-is-a-ring}, \ref{thm:II-2-1}, \ref{thm:impotent-lemma} oraz opis pod-struktur (\ref{sec:pod-struktury}) są według mojej wiedzy pierwszą ich formalizacją w Agdzie, a zatem stanowią wkład do obecnego stanu badań nad komputerowym sprawdzaniem dowodów matematycznych.
- \section{Porażki i problemy otwarte}
- Praca w pierwotnym założeniu mała dotyczyć sprawdzania twierdzeń z zakresu teorii ciał. Nie udało się tego zrobić z powodów opisanych w (\ref{sec:wielomiany}). Jedyny lemat ściśle z zakresu teorii ciał to trywialny lemat \ref{thm:impotent-lemma}. Otwartym problemem pozostaje reprezentacja wielomianów spełniająca wymagania opisane w (\ref{subsec:ograniczenia-implementacyjne}).
- \section{Możliwości rozwoju}
- Twierdzeń wymienionych w (\ref{sec:dokonania}) nie ma w biliotece standardowej Agdy, a sama praca wykorzystuje struktury i twierdzenia dostępne w bibliotece standardowej Agdy; stąd praca mogła by być do niej dołączona i przysłużyć się innym użytkownikom biblioteki standardowej.
- Praca zawiera formalizację fragmentu podręcznika ``A course in constructive algebra'' \cite{algebra}, formalizacja może być kontunuowana z wykorzystaniem twierdzen i struktur skonstruowanych w tej pracy.
- \section{Przemyślenia na temat formalizacji twierdzeń}
- Anders M\"{o}rtberg w swojej pracy magisterskiej \cite{magfailed} napisał: ``The process of converting constructive proofs into computer programs is difficult. The reason is that many things are left out in the mathematical arguments.''. Zgadzam się z drugim zdaniem --- na przykład twierdzenie dotyczące grup ilorazowych (\ref{sec:grupa-ilorazowa}) opisane w \cite{algebra} nie podaje chociażby dlaczego zakłada się że grupa musi być normalna (dowód jest pominięty). Natomiast nie zgadzam się z pierwszym zdaniem: myślę że napisanie wyżej wymienionego dowodu w Agdzie jest łatwiejsze niż wymyślenie go samemu bez wsparcia komputera (M\"{o}rtberg w swojej pracy nie korzystał z języka zależnie typowanego, a zatem też nie miał wspomagania). Kompilator gwarantuje poprawność dowodu\footnote{Zakładając że sam kompilator jest poprawny} przez co nie marnuje się czasu na wnioskowanie oparte na błędnych założeniach, a możliwość użycia edytora/IDE (\href{https://www.gnu.org/software/emacs/}{Emacs'a}) pozwala szybko znajdować, czytać i używać potrzebnych twierdzeń. Te zalety sprawiają, że programiści bez wykształcenia matematycznego mogą pisać poprawne dowody używając dobrze znanych sobie narzędzi (języki programowania, IDE).
|
