Przemebra/praca-magisterska/wstep.tex

\chapter{Wst\texorpdfstring{ę}{e}p} \label{chap:wstep}

\section{Sformułowanie celu pracy} \label{sec:cel-pracy}
Celem pracy jest komputerowe sprawdzenie poprawności twierdzeń z zakresu algebry \cite{algebra} (opisanych w rozdziale (\ref{sec:podstawy-algebry})) przez zapisanie ich jako zależnie typowane programy komputerowe w języku programowania Agda \cite{agdafoundation} (opisanym w rozdziale (\ref{sec:podstawy-agdy})).

\subsection{Zadasność celu}
Sprawdzenie poprawności dodowów matematycznych jest podatne na ludzki błąd.
Ograniczenia możliwości poznawczych człowieka sprawiają, że nie ma pewności co do poprawności twierdzenia po sprawdzeniu go przez skończoną liczbą matematyków. Może zaistnieć następujący scenariusz:
\begin{enumerate}
\item pewien matematyk dowodzi twierdzenie \(\mathcal{T}\),
\item twierdzenie \(\mathcal{T}\) przechodzi recencję naukową i zostaje opublikowane,
\item przez następnych kilka lat dziesiątki innych matematyków powołują się na \(\mathcal{T}\) w swoich pracach,
\item ktoś znajduje błąd w dowodzie \(\mathcal{T}\),
\item wszystkie twierdzenia powołujące się na \(\mathcal{T}\) są unieważnione.\footnote{Do artykułów i książek publikuje się erraty, czyli wykazy błędów.}
\end{enumerate}

\section{Organizacja pracy}
Rozdział \ref{chap:wstep} jest wstępem do pracy, zawiera sformułowanie celu (\ref{sec:cel-pracy}) oraz przegląd obecnie istniejących rozwiązań i narzędzi przydatnych do osiągnięcia celu (\ref{sec:przeglad}).
Rozdział \ref{chap:podstawy-teoretyczne} zawiera podstawy teoretyczne potrzebne do przejścia od ``ręcznego'' sprawdzania dowodów matematycznych do komputerowego, w szczególności: \begin{enumerate}
\item charakterystykę matematyki klasycznej (\ref{sec:matematyka-klasyczna}),
\item różnice między matematyką klasyczną i konstruktywistyczną (\ref{sec:matematyka-konstruktywistyczna}),
\item opis teorii typów {\PerMartinLofDopelniacz} (\ref{sec:pml}),
\item różnice między konstrukcją kompilatora języka prosto typowanego i języka z typami zależnymi (\ref{sec:kompilatory}).
\end{enumerate}
Ponadto rozdział zawiera opis podstaw algebry potrzebnych w dalszej częsci pracy (\ref{sec:podstawy-algebry}) i podstaw języka Agda (\ref{sec:podstawy-agdy}). Rozdział \ref{chap:wykonanie} zawiera spis sprawdzonych twierdzeń oraz sposoby ich sprawdzenia, a rozdział \ref{chap:zakonczenie} zawiera podsumowanie pracy.

\section{Przegląd istniejących rozwiązań i narzędzi} \label{sec:przeglad}
Sprawdzenie poprawności dowodów matematycznych można wspomagać komputerowo (szczegółowy opis sposobu znajduje się w rozdziale \ref{chap:podstawy-teoretyczne}).

\subsection{Systemy wspomagające dowodzenie}
System wspomagający dowodzenie twierdzeń to program komputerowy pozwalający użytkownikowi na zapis wyrażeń i formuł matematycznych oraz pomagający przy przeprowadzaniu ich dowodu \cite{proof-assistant-wiki}. Podstawą systemów wspierających dowodzenie twierdzeń są kompilatory języków zależnie typowanych, sposób ich działania jest opisany w (\ref{sec:kompilatory}). Lista nie jest kompletna, zawiera kilka wybranych, popularnych systemów.

\subsubsection{Coq} \label{subsec:coq}
\href{https://coq.inria.fr}{Coq} \cite{coq} jest systemem wspomagającym dowodzenie wydanym w 1989r. przez \href{https://www.inria.fr}{INRIA}\footnote{ Nadowowy instutut badań nad informatyką i automatyką (fr. \emph{Institut national de recherche en informatique et en automatique})} .
Coq posiada funkcjonalność automatycznego poszukiwania fragmentów dowodów, poszukiwanie definiuje się przez specjalny język taktyk \footnote{\href{https://coq.inria.fr/refman/coq-tacindex.html}{Spis taktyk dla w Coq'u}}. Podstawę teoretyczną Coq'a stanowi rachunek konstruktorów \cite{calculus-of-constructions} \footnote{W nowszych wersjach: rachunek indukcyjnych konstruktorów}.
\subsubsection{Lean}
\href{https://leanprover.github.io}{Lean} \cite{lean} to język rozwijany przez Microsoft Research od 2013r., który w założeniu ma ``zmniejszyć przepaść między interaktywnym i automatycznym dowodzeniem przez umieszczenie odpowiednich narzędzi i metod w zrębach, które wspierają interakcję z użytkownikiem i konstukcję w pełni wyspecyfikowanych, aksjomatycznych dowodów''\footnote{Cytat za \href{https://leanprover.github.io/about/}{oficjalną stroną Lean'a}}.

\subsubsection{Agda}
\href{https://wiki.portal.chalmers.se/agda/pmwiki.php}{Agda} \cite{agdafoundation} to zależnie typowany funkcyjny język programowania oraz system wspomagający dowodzenie używany w tej pracy, jego opis znajduje się w (\ref{sec:podstawy-agdy}).

% wincyj? HOL , Isabelle?

\subsection{Zbiory dowodów}
\subsubsection{Unimath}
Projekt \cite{UniMath} rozwijany w Coq'u (\ref{subsec:coq}) od 2014r., ``mający na celu sformalizowanie sporej częsci matematyki (...)'' \footnote{Cytat za \href{https://github.com/UniMath/UniMath/blob/master/README.md}{repozytorium UniMath}}. Zawiera, między innymi, formalizację algebry, topologii i teorii kategorii.

\subsubsection{Agda-stdlib}
Standardowa biblioteka Agdy \cite{agdastdlib}, ta praca bazuje na niej. Opis wykorzystywanych części jest w (\ref{sec:podstawy-algebry}).

\subsubsection{Math (Agda)}
Biblioteka napisana w Agdzie \cite{agdaslabe}, częściowo powielająca bibliotekę standardową.