Add writings from 4th and 5th of May

thesis/main.tex

@@ -356,6 +356,7 @@
 
 \usepackage{amsthm}
 \newtheorem{theorem}{Theorem}[section] % Applies counting based on section number
+\newtheorem{lemma}[theorem]{Lemma} % the [theorem] is an optional argument that applies counter sharing with "theorem"
 \theoremstyle{definition} % Non-italic style for definitions
 \newtheorem{definition}[theorem]{Definition} % the [theorem] is an optional argument that applies counter sharing with "theorem"
 \newtheorem{researchquestion}{Research question} % Applies counting based on section number

thesis/sections/2_background.tex

@@ -486,7 +486,7 @@ \subsection{Port-numbering model} \label{sec:port-numbering_model}
 
 Port-numbering model (PN model) is a rather weak model of computation that inherits from the message passing model.
 In the model, nodes do not have identification.
-A distributed algorithm that executes in a port-numbering model is called as a PN-algorithm.
+A distributed algorithm that executes in a port-numbering model is called as a PN algorithm.
 
 %We can basically take any network $N$ that has the same structure as a simple undirected graph $G$.
 %Each vertex of $G$ can be one-to-one mapped (bijection) to the nodes of $N$ and vice-versa.
@@ -497,7 +497,7 @@ \subsection{Port-numbering model} \label{sec:port-numbering_model}
 The ports are numbered in an arbitrary order.
 
 All nodes are considered identical; initially they are in the same internal state.
-Every node starts the execution simultaneously following the same PN-algorithm $A$.
+Every node starts the execution simultaneously following the same PN algorithm $A$.
 The execution of $A$ is done synchronously in parallel.
 A communication round consists of following synchronous steps:
 \begin{enumerate}

thesis/sections/3_research_questions.tex

@@ -3,29 +3,28 @@
 \section{Research questions} \label{sec:research_question}
 
 There are LCL problems that cannot be solved in the PN model.
-More specifically, there exist LCL problems such that no PN-algorithm can solve it in \emph{every} graph.
-There can be multiple reasons for unsolvability, and one case we are aware of is that there exists no valid labeling for a graph.
+More specifically, there exist LCL problems such that no PN algorithm can solve it in \emph{every} PN network.
+Therefore, if an LCL problem is unsolvable in the PN model, then there exists no valid labeling to the problem for some PN network.
+We are interested in detecting the unsolvability of an LCL problem automatically.
 
 \begin{researchquestion} \label{research_question:1}
-Given an LCL problem and a graph, how can we automatically detect the non-existence of a valid labeling for the graph?
+Given an LCL problem, how can we automatically detect the unsolvability of the problem in the PN model?
 \end{researchquestion}
 
-We answer to Research question \ref{research_question:1} in Section \ref{sec:algorithm}, where we present our algorithm that can automatically detect the non-existence of a valid labeling.
+We answer to Research question \ref{research_question:1} in Section \ref{sec:algorithm}, where we present our algorithm that can automatically detect the unsolvability of an LCL problem in the PN model.
 
-In Section \ref{}, we present Theorem \ref{}, which says that an unsolvability of an LCL problem in the PN model implies that the problem is also not solvable in constant time in the LOCAL model.
+In Section \ref{sec:algorithm}, we present Theorem \ref{thm:lcl_unsolvability}, which says that an unsolvability of an LCL problem in the PN model implies that the problem is also not solvable in constant time in the LOCAL model.
 We want to know if we can prove it.
-%TODO
 
 \begin{researchquestion} \label{research_question:2}
 Can we prove that an unsolvability of an LCL problem in the PN model implies that the problem is also not solvable in constant time in the LOCAL model?
 \end{researchquestion}
 
-As our answer to Research question \ref{research_question:2}, we prove Theorem \ref{} in Section \ref{}.
-The proof is done in parts, by introducing first related lemmas and then finally proving the theorem.
-%TODO
+As our answer to Research question \ref{research_question:2}, we prove Theorem \ref{thm:lcl_unsolvability} in Section \ref{sec:algorithm:prooving_the_theorem}.
+The proof relies on multiple lemmas that we introduce in Sections \ref{sec:algorithm:from_multiple_to_simple} and \ref{sec:algorithm:from_pn_to_local}.
 
-We have implemented the algorithm that we give as an answer to Research question \ref{research_question:1} in Section \ref{sec:algorithm}, and we introduce details of the implementation in Section \ref{sec:implementation}.
-With the theorem from Research question \ref{research_question:2}, the results from the tool can be derived to non-constant lower bounds in the LOCAL model.
+We have implemented the algorithm from Section \ref{sec:algorithm} that we give as an answer to Research question \ref{research_question:1}, and we introduce details of the implementation in Section \ref{sec:implementation}.
+With Theorem \ref{thm:lcl_unsolvability}, the results from the tool can be derived to non-constant lower bounds in the LOCAL model.
 There also exists a database of upper and lower bounds of LCL problems \cite{Tereshchenko2021}, and these bounds have been computed using various tools called \emph{classifiers}.
 Our implementation is one kind of classifier, and we want to know if it can find any new lower bounds i.e. lower bounds that are higher than what is currently known about these problems.
 
@@ -41,5 +40,5 @@ \section{Research questions} \label{sec:research_question}
 \end{researchquestion}
 
 As an answer to Research questions \ref{research_question:3} and \ref{research_question:4}, we present the results from our implementation in Section \ref{sec:results}.
-The results will include new problem classifications, execution time statistics and ... \todo{}.
+The results will include new problem classifications, execution time statistics and ... \todo{Complete these after results are done.}.
 %TODO

thesis/sections/5_algorithm.tex

@@ -2,11 +2,35 @@
 
 \section{Algorithm} \label{sec:algorithm}
 
+%% Draft how this whole section should look like.
+%% Then after that, spread these comments to their correct positions.
+%%
+% - Tell about this section 5
+% - First, we want to answer to RQ1,  or how we can autom. detect the unsolvability of an LCL problem.
+%   - For this, we first define what is solvability
+%   - Then we define what is unsolvability (its complement)
+%   - Lemma: LCL is not solvable in PN, if there exists a network that no algorithm can solve
+%     - !Mention! that this is only one case where problem is unsolvable. There does not really have to be one network that is not solvable with any algorithm. The other option would be that for each algorithm, there is some network in which the problem is not solvable.
+%   - Lemma: If LCL is not solvable in graph G, then the problem is also not solvable in any PN network N that has G as its underlying graph
+%     - Proof: We proof by contradiction. We assume that PI is not solvable in G, and PI is solvable in some N that has G as its underlying graph. This means that there exists a valid labeling for N, therefore there must exist a valid labeling for G. This is contradicting with the assumption that PI is not solvable in G.
+%   - We show the algorithm that finds graphs (counterexamples) and explain the algorithm.
+% - Second, we show our theorem: if an LCL problem is unsolvable in the PN model, then the problem is also not solvable in constant time in the LOCAL model.
+%   - We introduce some lemmas in the following subsections
+%   - 
+
+%
+%
+%
+
+
+
+
+\todo{I could say something about Research questions \ref{research_question:1} and \ref{research_question:2}}
 In this section, we will introduce the basic idea of an essential algorithm that is used in the actual implementation discussed in section \ref{sec:implementation}.
-The algorithm's purpose is to find a proof that a given LCL problem $\Pi$ is impossible to solve in PN model.
+The algorithm's purpose is to find a proof that a given LCL problem $\Pi$ is impossible to solve in the PN model.
 Here we specifically allow PN networks to have multiple connections.
-Later in Section \ref{sec:algorithm:theorems:a} we show that the unsolvability of a problem $\Pi$ in PN networks (with multiple connections) implies that it is also impossible to solve $\Pi$ in \emph{simple} PN networks (without multiple connections).
-Finally, in Section \ref{sec:algorithm:theorems:b} we show that the unsolvability of $\Pi$ in \emph{simple} PN networks implies that $\Pi$ is not solvable in constant time ($\mathcal{O}(1)$) in the LOCAL model.
+Later in Section \ref{sec:algorithm:from_multiple_to_simple} we show that the unsolvability of a problem $\Pi$ in PN networks (with multiple connections) implies that it is also impossible to solve $\Pi$ in \emph{simple} PN networks (without multiple connections).
+Finally, in Section \ref{sec:algorithm:from_pn_to_local} we show that the unsolvability of $\Pi$ in \emph{simple} PN networks implies that $\Pi$ is not solvable in constant time ($\mathcal{O}(1)$) in the LOCAL model.
 
 First we start with defining the meaning of solvability of an LCL problem.
 %TODO These definitions and theorems might have a better place under section 2 background.
@@ -21,21 +45,21 @@ \section{Algorithm} \label{sec:algorithm}
 
 The Definitions \ref{def:lcl_solvability} and \ref{def:lcl_solvability:contrapositive} are equivalent. The latter one might be more difficult to understand, but the way it is phrased, easily leads us to the following Theorem:
 
-\begin{theorem} \label{thm:lcl_unsolvability}
+\begin{lemma} \label{lem:lcl_unsolvability}
     An LCL problem $\Pi$ is not solvable in PN model, if there exists a PN network $N$ such that no PN algorithm $A$ can solve the $\Pi$ in $N$.
-\end{theorem}
+\end{lemma}
 \begin{proof}
     Let $\Pi$ be an LCL problem.
     Let $N$ be a PN network such that no PN algorithm $A$ can solve $\Pi$ in $N$.
     Therefore, no PN algorithm $A$ can find a solution to $\Pi$ in all PN networks.
-    According to the definition \ref{def:lcl_solvability:contrapositive}, this is equivalent with $\Pi$ being unsolvable.
+    According to Definition \ref{def:lcl_solvability:contrapositive}, this is equivalent with $\Pi$ being unsolvable.
 \end{proof}
 
-As the Theorem \ref{thm:lcl_unsolvability} shows us, to show that a problem $\Pi$ is unsolvable, it is enough to find a counterexample, a PN network $N$ in which the problem $\Pi$ cannot be solved.
+As the Theorem \ref{lem:lcl_unsolvability} shows us, to show that a problem $\Pi$ is unsolvable, it is enough to find a counterexample, a PN network $N$ in which the problem $\Pi$ cannot be solved.
 To show that, it is enough to find an underlying graph $G$ of $N$ in which the problem $\Pi$ cannot be solved.
-\begin{theorem} \label{thm:problem_unsolvability_in_graphs}
+\begin{lemma} \label{thm:problem_unsolvability_in_graphs}
     If a problem $\Pi$ is not solvable in graph $G$, then $\Pi$ is also not solvable in any PN network $N$ that has $G$ as its underlying graph.
-\end{theorem}
+\end{lemma}
 \begin{proof}
 \todo{Complete proof} %TODO complete proof
 \end{proof}
@@ -89,8 +113,15 @@ \section{Algorithm} \label{sec:algorithm}
 %TODO talk about networks and graphs. In the above text they are refered as if they were the same thing.
 %TODO Do we need to talk about trees and how these biregular multigraphs relate to them? 'Informally, the idea is to prove negative results for the case in which "we are in the middle of a very large tree, far away from the leaves".'
 
+
+\todo{Check if this is good place for the theorem.}%TODO
+\todo{Also modify other text so that it fits here.}%TODO
+\begin{theorem} \label{thm:lcl_unsolvability}
+    If an LCL problem is unsolvable in the PN model, then the problem is also not solvable in constant time in the LOCAL model.
+\end{theorem}
+
 In the following sections, we will prove that if an LCL problem $\Pi$ is not solvable in PN network $N$ with multiple connections, then it is not solvable in constant time in the LOCAL model.
-We have divided the proofs into multiple theorems and grouped them under two different sections, Section \ref{sec:algorithm:theorems:a} and Section \ref{sec:algorithm:theorems:b}.
+We have divided the proofs into multiple theorems and grouped them under two different sections, Section \ref{sec:algorithm:from_multiple_to_simple} and Section \ref{sec:algorithm:from_pn_to_local}.
 The dependencies of theorems are shown in the Figure \ref{fig:algorithm:theorem_dependency}.
 \footnote{Where should I put these theorems? Do they fit under Section \ref{sec:algorithm}?}
 
@@ -111,7 +142,7 @@ \section{Algorithm} \label{sec:algorithm}
     \caption{A dependency graph of the following theorems.\label{fig:algorithm:theorem_dependency}}
 \end{figure}
 
-\subsection{Theorems A? From multiple connections to simple networks} \label{sec:algorithm:theorems:a}
+\subsection{Theorems A? From multiple connections to simple networks} \label{sec:algorithm:from_multiple_to_simple}
 \todo{Fix section title}
 In this section we show that if an LCL problem is not solvable in PN networks with multiple connections, then the problem is also not solvable in simple PN networks.
 We try to split this into couple of theorems and at the end utilize the shown theorems to show this to be true.
@@ -252,7 +283,7 @@ \subsection{Theorems A? From multiple connections to simple networks} \label{sec
     Therefore, the problem $\Pi$ is not solvable in simple PN network $N_1$ that is a lift of $N_2$.
 \end{proof}
 
-\subsection{Theorems B? From PN to LOCAL} \label{sec:algorithm:theorems:b}
+\subsection{Theorems B? From PN to LOCAL} \label{sec:algorithm:from_pn_to_local}
 \todo{Fix section title}
 
 \begin{theorem} \label{thm:lcl_unsolvability:5}
@@ -262,4 +293,13 @@ \subsection{Theorems B? From PN to LOCAL} \label{sec:algorithm:theorems:b}
 \end{theorem}
 \begin{proof}
     \todo{Complete this proof} %TODO Complete this proof
-\end{proof}
+\end{proof}
+
+
+\subsection{Proving the theorem} \label{sec:algorithm:prooving_the_theorem}
+Now that all the groundwork has been done in the prior sections, we can prove Theorem \ref{thm:lcl_unsolvability}.
+The proof is also our answer to Research Question \ref{research_question:2}.
+\begin{proof}[Proof of Theorem \ref{thm:lcl_unsolvability}]
+    Here is the proof.
+    \todo{}
+\end{proof}