Final changes in the report

Many thanks to Simon!

thesis/report/abstract.tex

@@ -1,7 +1,7 @@
 % https://tex.stackexchange.com/a/70818
 % Assumes that the two abstracts fit in one page
 \newenvironment{abstractpage}
-  {\cleardoublepage\vspace*{\fill}\thispagestyle{empty}}
+  {\cleardoublepage\vspace*{\fill}\thispagestyle{plain}}
   {\vfill\cleardoublepage}
 \newenvironment{i18nabstract}[1]
   {\bigskip\selectlanguage{#1}%

thesis/report/chapters/1-introduction.tex

@@ -5,7 +5,7 @@ \section{Introduction}
 
 In this thesis we describe the design process of a front-end for the modern proof assistant LISA. Our main focus is to preserve the same soundness standards as the existing framework while making it more expressive and interactive. The supporting source code for this project is published at the following address:
 \begin{center}
-\href{http://github.com/FlorianCassayre/master-project}{\textbf{github.com/FlorianCassayre/master-project}}\footnote{The current release is identified by commit: \code{c3499c2729730a7f807efb8676a92dcb6f8a3f8f}}
+\href{http://github.com/FlorianCassayre/master-project}{\textbf{github.com/FlorianCassayre/master-project}}\footnote{The current release is identified by commit number: \code{30b0c340e94c6e981d3115c554ab9bc97f8b8971}}
 \end{center}
 
 \subsection{LISA}
@@ -47,6 +47,6 @@ \subsection{LISA}
   \label{fig:simple-lisa-proof}
 \end{figure}
 
-A proof in this system is a directed acyclic graph of proof steps. Each such step corresponds to the application of an inference rule, and is characterized by its conclusion expressed as a sequent, and some premises. A sequent is a pair of sets of formulas, noted $\phi_1, \phi_2, ..., \phi_n \vdash \psi_1, \psi_2, ..., \psi_m$ or $\Gamma \vdash \Delta$, and can be interpreted in conventional logic as a conjunction of premises implying a disjunction of conclusions. That said, the actual semantic is controlled by the inference rules provided by the system. Proofs can optionally have ``imports'', sequents that can be used as premises, and proofs may also be nested for organization purposes. Figures \ref{fig:simple-lisa-proof-graph} and \ref{fig:simple-lisa-proof} showcase a formal proof in LISA. Notice that a directed acyclic graph can always be represented in a linear fashion, but not necessarily as a tree (unless we duplicate forward edges).
+A proof in this system is a directed acyclic graph of proof steps. Each such step corresponds to the application of an inference rule, and is characterized by its conclusion expressed as a sequent, and some premises. A sequent is a pair of sets of formulas, noted $\phi_1, \phi_2, ..., \phi_n \vdash \psi_1, \psi_2, ..., \psi_m$ or $\Gamma \vdash \Delta$, and can be interpreted in conventional logic as a conjunction of premises implying a disjunction of conclusions. That said, the actual semantic is controlled by the inference rules provided by the system. Proofs can optionally have ``imports'': sequents that are used as premises but do not come from any step. Proofs may also be nested for organization purposes. Figures \ref{fig:simple-lisa-proof-graph} and \ref{fig:simple-lisa-proof} showcase a formal proof in LISA. Notice that a directed acyclic graph can always be represented in a linear fashion, but not necessarily as a tree (unless we duplicate forward edges).
 
 Currently LISA only exists as a Scala library, therefore the proofs are described using Scala code. For further technical details about LISA, we refer the reader to the official manual \cite{Guilloud2022-2}.

thesis/report/chapters/2-background.tex

@@ -9,7 +9,7 @@ \subsection{Overview}
 
 \subsection{LCF-style framework}
 
-In 2020 I worked on designing a LCF-style framework in Scala that used the Von Neumann-Bernays-Gödel set theory (NBG) as a foundation \cite{Cassayre2020} and attempted to formalize the proofs displayed in a logic textbook \cite{Mendelson2015}. This project allowed me to explore different areas of formal methods and theorem proving such as the representation of proofs and tableaux solving strategies. One of the particularities of that framework was that formulas---and more generally theorems were strongly typed. In the lines of the Curry-Howard Correspondence, this meant that soundness could be enforced by the type checker alone. Unavoidably, this feature gets in the way when working with higher-order rules (e.g. induction) and automated strategies (e.g. tableaux). It also demonstrated that the raw LCF-style restricted the expressiveness of proofs, and that to provide more flexibility an extra layer would be needed.
+In 2020 I worked on designing a LCF-style framework in Scala that used the Von Neumann-Bernays-Gödel set theory (NBG) as a foundation \cite{Cassayre2020} and attempted to formalize the proofs displayed in a logic textbook \cite{Mendelson2015}. This project allowed me to explore different areas of formal methods and theorem proving such as the representation of proofs and tableaux solving strategies. The particularities of that framework were the possibility to recover the value of a formula from its type and the correspondence between lambda expressions and logical implications. In the lines of the \textit{Curry-Howard correspondence}, this meant that soundness could be enforced by the type checker alone. Unavoidably, this feature gets in the way when working with higher-order rules (e.g. induction) and automated strategies (e.g. tableaux). It also demonstrated that the raw LCF-style restricted the expressiveness of proofs, and that to provide more flexibility an extra layer would be needed.
 
 LISA uses the Zermelo-Fraenkel set theory (ZF, and more specifically ZFC) instead of NBG. Both axiomatizations are similar, the main difference being that NBG makes the distinction between sets and proper classes. NBG has been (independently) proven to be a conservative extension of ZFC, meaning that neither is stronger than the other. Furthermore, LISA uses sequent calculus in its deductive system, while that framework had formulas as first-class citizens.
 

thesis/report/chapters/3-framework.tex

@@ -106,7 +106,7 @@ \subsection{DSL}
 
 \input{figures/fol-erd}
 
-The major function of the DSL to assist the developer in using the first-order logic package (\autoref{fig:fol-erd}), namely to provide methods to construct objects in an intuitive way. The second aspect is to provide compile-time safety guarantees when doing so. For instance the sequent $\vdash f(a, b), c \land d$ can be written as \code{|- (f(a, b), a /\textbackslash~a)} in our Scala DSL. Scala allows custom infix operators to be defined, therefore the operators of propositional logic are straightforward to implement. The first interesting problem is about converting the tuple \code{(t1:~T1, ..., tn:~TN)} into a sequence of values of type \code{T1 {|} ...~{|} TN}. While tuples have a method to iterate over their members, this solution is unsound because it loses all type information. Instead, we rely on a mechanism offered by the language: \textit{given} instances and conversions (\autoref{lst:generic-tuples-1}).
+The major function of the DSL to assist the developer in using the first-order logic package (\autoref{fig:fol-erd}), namely to provide methods to construct objects in an intuitive way. The second aspect is to provide compile-time safety guarantees when doing so. For instance the sequent $\vdash f(a, b), c \land d$ can be written as \code{|- (f(a, b), c /\textbackslash~d)} in our Scala DSL. Scala allows custom infix operators to be defined, therefore the operators of propositional logic are straightforward to implement. The first interesting problem is about converting the tuple \code{(t1:~T1, ..., tn:~TN)} into a sequence of values of type \code{T1 {|} ...~{|} TN}. While tuples have a method to iterate over their members, this solution is unsound because it loses all type information. Instead, we rely on a mechanism offered by the language: \textit{given} instances and conversions (\autoref{lst:generic-tuples-1}).
 
 \begin{lstlisting}[language=Scala,caption={[Generic tuples (1)]{Generic tuples: converting a tuple of \code{T} into a \code{Seq[T]}.}},label={lst:generic-tuples-1}]
 trait Converter[R, S] extends (R => Seq[S])

thesis/report/chapters/4-proofs.tex

@@ -69,7 +69,7 @@ \subsection{Terminology}
   \node [block, below = of state2, text centered] (state5) {(no goals)};
   \draw [->, shorten >= 0.5mm] -- ++(0, 1.5) node[fill=white]{Prove $\vdash \neg{?a} \lor {?b} \Leftrightarrow {?a} \Rightarrow {?b}$} -- (state0);
   \draw [->, shorten >= 0.5mm] (state0.east) -- ++(1.25, 0) node[fill=white]{I.R.$\Leftrightarrow$} -- (state1);
-  \draw [->, shorten >= 0.5mm] (state1.east) -- ++(1.25, 0) node[fill=white]{Focus (2)} -- (state2);
+  \draw [->, shorten >= 0.5mm] (state1.east) -- ++(1.25, 0) node[fill=white]{Focus (1)} -- (state2);
   \draw [->, shorten >= 0.5mm] (state2.south) |- ++(0, -0.55) |- ++(-5.95, 0) node[fill=white]{I.R.$\Rightarrow$} -| (state3.north);
   \draw [->, shorten >= 0.5mm] (state3.east) -- ++(1.25, 0) node[fill=white]{I.L.$\Rightarrow$} -- (state4);
   \draw [->, shorten >= 0.5mm] (state4.east) -- ++(1.25, 0) node[fill=white]{Solve} -- (state5);

thesis/report/chapters/5-synthesis.tex

@@ -129,7 +129,7 @@ \subsubsection{Graph rewriting}
 The previous optimizations ignored the semantics of the LISA sequent calculus. Taking them into account opens up a whole new category of optimization strategies.
 For instance, consecutive \code{Rewrite} steps can be merged together assuming the first one of the two is only referenced by other rewrite steps. Similarly, fruitless instantiations can be eliminated and consecutive ones merged in some cases. These optimizations can be represented as a term rewriting system through a set of rules. These rules could in fact be as complex and granular as desired but for the sake of efficiency and because such a procedure is error-prone, we limit ourselves to cases that are likely to be produced by the front. It should be noted that the use of term rewriting rules is a convenient strategy to approach a known hard problem: finding the shortest sequent calculus proof in propositional logic \cite{Krajicek1994}.
 
-The rewriting rules that are currently in place are listed in \autoref{fig:synthesis-simplifications}. We claim that such a system always terminates. To show that we can introduce a (positive) lexicographic measure for the complexity of the proof where the first criterion is the number of steps and the second one is the sum of of the weights of each step. Rewrite steps have the lowest weights, followed by weakening steps and then all the remaining steps. Then we can see that the measure decreases strictly after any application of a rule, which implies that the system must eventually terminate.
+The rewriting rules that are currently in place are listed in \autoref{fig:synthesis-simplifications}. Due to an implementation detail in the proof checker, the rule \code{Rewrite} is slightly stronger than all of the other rules because the sequents are converted to logical implications before comparison. For convenience, \code{Rewrite} rules in our term rewriting system correspond to a weaker version of the actual kernel rules. We claim that such a system always terminates. To show that we can introduce a (positive) lexicographic measure for the complexity of the proof where the first criterion is the number of steps and the second one is the sum of of the weights of each step. Rewrite steps have the lowest weights, followed by weakening steps and then all the remaining steps. Then we can see that the measure decreases strictly after any application of a rule, which implies that the system must eventually terminate.
 
 Additionally, if we ignored the cut rules simplifications such a system would be confluent. This follows from the fact that the inputs and outputs are preserved, and that consecutive rewrite/weakening steps can be reduced to a single step in an associative way.
 

thesis/report/chapters/7-parsing-printing.tex

@@ -130,8 +130,10 @@ \subsection{Compile-time string interpolation}
 This feature has a nice application in our case: not only can we enforce interpolated variables to be terms or formulas but we can also check their type with respect to the context they appear in. For instance, in the expression \code{formula"\$a /\textbackslash\ b"}, the variable \code{a} cannot be a term (in fact, it must be a formula). In addition to terms and formulas, we may also allow the interpolation of labels which is very useful to bind names dynamically, e.g. \code{formula"\$p(s)"}. Notice that the previous expression is structurally different from \code{formula"\${p(term"s")}"}, although it results in the same formula.
 
 \begin{figure}[H]
+  \captionsetup[subfigure]{margin=0cm}
+  \centering
+  \begin{subfigure}{0.25\linewidth}
   \centering
-  \subfloat[\centering Runtime parsing \label{fig:parsing-runtime}]{
   % Runtime
   \begin{tikzpicture}[auto, on grid, node distance=1.5cm and 2cm, block/.style = {draw, fill=white, rectangle, minimum height=1cm, minimum width=2cm}, none/.style = {draw=none}]
   \node [none] (input) {$\small\code{String}\normalsize$};
@@ -144,9 +146,12 @@ \subsection{Compile-time string interpolation}
   \draw [->] (parser) -- (typer1);
   \draw [->] (typer1) -- (output);
   \end{tikzpicture}
-  }%
+  \caption{Runtime parsing}
+  \label{fig:parsing-runtime}
+  \end{subfigure}
   \qquad\qquad
-  \subfloat[\centering Compile-time parsing, with variable interpolation \label{fig:parsing-compile-time}]{
+  \begin{subfigure}{0.4\linewidth}
+  \centering
   % Compile-time
   \begin{tikzpicture}[auto, on grid, node distance=1.5cm and 2.25cm, block/.style = {draw, fill=white, rectangle, minimum height=1cm, minimum width=2cm}, none/.style = {draw=none}]
   \node [none] (input) {$\small\code{Expr[StringContext]}\normalsize$};
@@ -165,8 +170,10 @@ \subsection{Compile-time string interpolation}
   \draw [->] (typer2) -- (converter);
   \draw [->] (converter) -- (output);
   \end{tikzpicture}
-  }%
-  \caption[Parsing phases]{Phases for regular runtime parsing (\ref{fig:parsing-compile-time}) and compile-time string interpolation (\ref{fig:parsing-runtime}). \code{T} is one of \code{Sequent}, \code{Formula} or \code{Term}, depending on the interpolator that was called.}
+  \caption{Compile-time parsing, with variable interpolation}
+  \label{fig:parsing-compile-time}
+  \end{subfigure}
+  \caption[Parsing phases]{Phases for regular runtime parsing (a) and compile-time string interpolation (b). \code{T} is one of \code{Sequent}, \code{Formula} or \code{Term}, depending on the interpolator that was called.}
   \label{fig:multi-stage-parsing}
 \end{figure}
 

thesis/report/thesis.tex

@@ -14,7 +14,7 @@
 \usepackage{tikz}
 \usetikzlibrary{arrows,positioning,calc}
 \usepackage{float}
-\usepackage{subfig}
+\usepackage{subcaption}
 \usepackage{ebproof}
 \usepackage[english,french,main=english]{babel}
 \usepackage{listings}
@@ -23,14 +23,14 @@
 \usepackage[stable]{footmisc}
 \usepackage[nounderscore]{syntax}
 \usepackage{framed}
-%\usepackage{etoc} % Multiple ToCs
+\usepackage[margin=1cm]{caption}
 \usetikzlibrary{trees}
 \usepackage[style=numeric-comp]{biblatex}
 \addbibresource{bibliography.bib}
 \setlength{\columnsep}{3.25cm} % Adjust depending to the length of names in the cover
 
 % Draft
-\usepackage[firstpage]{draftwatermark}\SetWatermarkScale{2}
+%\usepackage[firstpage]{draftwatermark}\SetWatermarkScale{2}
 
 \let\oldemptyset\emptyset
 \let\emptyset\varnothing
@@ -55,7 +55,9 @@
 \newtheorem{definition}{Definition}[section]
 \newtheorem{theorem}{Theorem}
 
-\pagenumbering{gobble}
+\pagenumbering{arabic}
+
+\thispagestyle{empty}
 \input{cover}
 \newpage
 
@@ -64,7 +66,6 @@
 \addtolength{\topmargin}{-0.5cm}
 \setlength{\headsep}{0.5cm}
 
-\pagenumbering{arabic}
 \newpage
 
 \input{abstract}