diff --git a/CITATION.cff b/CITATION.cff index 8dd561f..ae5a004 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -4,7 +4,7 @@ authors: - family-names: "Cassayre" given-names: "Florian" orcid: "https://orcid.org/0000-0001-5784-8051" -title: "A front-end for LISA" +title: "A front-end for the LISA proof assistant" version: 1.0.0 doi: 10.5281/zenodo.6645113 date-released: 2022-06-24 diff --git a/README.md b/README.md index be657a3..2eb02a7 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,7 @@ This repository hosts the work related to my Master Project (PDM) at [LARA](https://lara.epfl.ch/w/). This includes source code, writeup and any other significant resource related to the project. -Project title: ***A Proof System for LISA*** +Project title: ***A front-end for the LISA proof assistant*** Dates: **21.02.2022** to **24.06.2022** diff --git a/thesis/report/abstract.tex b/thesis/report/abstract.tex index cdc7655..62fe129 100644 --- a/thesis/report/abstract.tex +++ b/thesis/report/abstract.tex @@ -11,10 +11,10 @@ \begin{abstractpage} \begin{i18nabstract}{english} % Don't forget to update the translation if you make any changes here! - We propose a front-end framework for the novel proof assistant LISA. The two systems are based on Gentzen's sequent calculus with first-order logic and are implemented in the Scala programming language. Our framework supports different proof styles and provides a declarative language for tactics. The usage of tactics is facilitated thanks to a parameter inference system. The proofs written in our framework can then be translated into the trusted kernel for verification. We demonstrate that our framework simplifies the process of writing formal proofs for LISA, and that it is suitable for an interactive use. We also introduce other relevant components for LISA such as a strongly typed programming interface, a two-way parser and printer, and a proof simplifier. + We propose a front-end framework for the novel proof assistant LISA. The two systems are based on Gentzen's sequent calculus with first-order logic and are implemented in the Scala programming language. Our framework supports different proof styles and provides a declarative language for tactics. The usage of tactics is facilitated thanks to a parameter inference system. The proofs written in our framework can be translated into the trusted kernel for verification. We demonstrate that our framework simplifies the process of writing formal proofs for LISA, and that it is suitable for an interactive usage. We also introduce other relevant components for LISA such as a strongly typed programming interface, a two-way parser and printer, and a proof simplifier. \end{i18nabstract} \begin{i18nabstract}{french} - Nous proposons un cadriciel pour le nouvel assistant de preuve LISA. Les deux systèmes sont basés sur le calcul des séquents de Gentzen en utilisant la logique du premier ordre, et sont implémentés dans le langage de programmation Scala. Notre système prend en charge différents styles de preuve et apporte un langage déclaratif pour les tactiques. L'utilisation des tactiques est facilitée grâce à un système d'inférence des paramètres. Les preuves écrites dans ce cadre peuvent ensuite être traduites vers le noyau de confiance pour y être vérifiées. Nous montrons que notre cadre permet de simplifier le processus d'écriture de démonstrations formelles pour LISA, et qu'il est adapté à une utilisation interactive. Nous présentons d'autres composantes clés pour LISA, telles qu'une interface de programmation fortement typée, un analyseur syntactique ains qu'un système d'impression élégante, et un simplificateur de preuves. + Nous proposons un cadriciel pour le nouvel assistant de preuve LISA. Les deux systèmes sont basés sur le calcul des séquents de Gentzen en utilisant la logique du premier ordre, et sont implémentés dans le langage de programmation Scala. Notre système prend en charge différents styles de preuve et apporte un langage déclaratif pour les tactiques. L'utilisation des tactiques est facilitée par un système d'inférence des paramètres. Les preuves écrites dans ce cadre peuvent ensuite être traduites vers le noyau de confiance pour y être vérifiées. Nous montrons que notre cadre permet de simplifier le processus d'écriture de démonstrations formelles pour LISA, et qu'il est adapté à une utilisation interactive. Nous présentons d'autres composantes clés pour LISA, telles qu'une interface de programmation fortement typée, un analyseur syntactique ains qu'un système d'impression élégante, et un simplificateur de preuves. \end{i18nabstract} \end{abstractpage} diff --git a/thesis/report/bibliography.bib b/thesis/report/bibliography.bib index e81bcba..7c2f47d 100644 --- a/thesis/report/bibliography.bib +++ b/thesis/report/bibliography.bib @@ -227,3 +227,10 @@ @book{Appel1989 year={1989}, publisher={American Mathematical Soc.} } + +@phdthesis{Ayers2021, + title={A Tool for Producing Verified, Explainable Proofs}, + author={Ayers, Edward}, + year={2021}, + school={University of Cambridge} +} diff --git a/thesis/report/chapters/1-introduction.tex b/thesis/report/chapters/1-introduction.tex index 924063c..1891a60 100644 --- a/thesis/report/chapters/1-introduction.tex +++ b/thesis/report/chapters/1-introduction.tex @@ -1,18 +1,16 @@ \section{Introduction} \label{sec:introduction} -A proof assistant is a piece of software that can assist a user in writing a particular type of proofs, one that can be verified by a machine. Proofs following this format are desirable because it suffices to show that the verification procedure is sound to automatically and irrefutably judge them. Computer-assisted theorem proving can also leverage the computational capabilities offered by machines, one of the most famous example being the proof of the \textit{four-color conjecture} \cite{Appel1989}. However, the greatest strength of proof assistants might also be their greatest weakness: they are often complex systems, which correctness is difficult to demonstrate and therefore are prone to bugs in their implementation. +A proof assistant is a piece of software that can assist a human user in writing a particular type of proofs, one that can be verified by a machine. Proofs following this format are desirable because it suffices to show that the verification procedure is sound to automatically and irrefutably judge any of them. Computer-assisted theorem proving can also leverage the computational capabilities offered by machines, one of the most famous example being the proof of the \textit{four-color conjecture} \cite{Appel1989}. However, the greatest strength of proof assistants might also be their greatest weakness: they are often complex systems, whose correctness is difficult to demonstrate and therefore are prone to bugs in their implementation. They also suffer from a lack of understandability, both in terms of the underlying theories used and of the proofs produced, which results in a low adoption rate by mathematicians \cite{Ayers2021}. -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 introducing an interactive component. - -The supporting source code for this project is published at the following address: +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}} \end{center} \subsection{LISA} -LISA\footnote{\textbf{L}ISA \textbf{I}s \textbf{S}ets \textbf{A}utomated} is an ongoing project conducted at the lab for automated reasoning and analysis (LARA), EPFL. It is a library built on top of sequent calculus and set theory that enables the formalization of mathematical proofs \cite{Guilloud2022-2}. +LISA\footnote{\textbf{L}ISA \textbf{I}s \textbf{S}ets \textbf{A}utomated} is an ongoing project conducted at the Lab for Automated Reasoning and Analysis (LARA), EPFL. It is a library built on top of sequent calculus and set theory that enables the formalization of mathematical proofs \cite{Guilloud2022-2}. \begin{figure}[H] $$ @@ -38,17 +36,17 @@ \subsection{LISA} \infer2[Right $\Leftrightarrow$]{\vdash \neg{?a} \lor {?b} \Leftrightarrow {?a} \Rightarrow {?b}} \end{prooftree} $$ - \caption[Proof tree (1)]{An example of a proof in sequent calculus. Here it proves the tautology $\neg{?a}\lor{?b}\Leftrightarrow{?a}\Rightarrow{?b}$. The question mark indicates a schema, essentially a variable such that the statement holds true for any value. The inference used at every step is indicated.} + \caption[Proof tree (1)]{An example of a proof in sequent calculus. This proof demonstrates the tautology $\neg{?a}\lor{?b}\Leftrightarrow{?a}\Rightarrow{?b}$. The question mark indicates a schema, namely a variable that can later be instantiated. The inference rule used at every step is indicated on the right.} \label{fig:simple-lisa-proof-graph} \end{figure} \begin{figure}[H] \centering \input{figures/proof-mini.lisa} - \caption[Proof in LISA]{A representation of the proof of \autoref{fig:simple-lisa-proof-graph} in LISA. Each step is assigned an index, import are represented with negative indices. The indentation corresponds to the level of the proof: subproofs are indented further down. The second column states what rule is used, along with the premises it relies upon. The third column is the conclusion of that step. The last column contains parameters to disambiguate the application of the rule.} + \caption[Proof in LISA]{A representation of the proof of \autoref{fig:simple-lisa-proof-graph} in LISA. Each step is assigned an index, and import are represented with negative indices. Scoping within the proof is possible and determined by the indentation level: subproofs are indented further down. The second column states what rule is used, along with the premises it uses. The third column is the conclusion of that step. The last column contains parameters to disambiguate the application of the rule.} \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 along with its linear representation. Notice that a directed acyclic graph can always be represented in a linear fashion, but not necessarily as a tree (without having to inline leaves). +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). 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}. diff --git a/thesis/report/chapters/2-background.tex b/thesis/report/chapters/2-background.tex index 19f5594..b62fe84 100644 --- a/thesis/report/chapters/2-background.tex +++ b/thesis/report/chapters/2-background.tex @@ -1,18 +1,18 @@ \section{Background} \label{sec:background} -Attempts at formalizing logic and mathematics are numerous, and one can observe that successful systems are often the result of an iterative process \cite{Paulson2019, Harrison2014, Asperti2007}. In this section we describe the history of proof assistants, and we present my past contributions to the field. +Attempts at formalizing logic and mathematics are numerous, and one can observe that successful systems are often the result of an iterative process \cite{Paulson2019, Harrison2014, Asperti2007}. In this section we describe the history of proof assistants, and we present our past contributions to the field. \subsection{Overview} -Historically, proof assistants focused mainly on automating the process of demonstrating assertions rather than providing tools to assist the user in doing so; which is objectively a simpler task \cite{Harrison2014}. It is only later that designs have leaned towards user-centered systems with ideas such as the Edinburgh LCF, and subsequent work on metalogic and tactics \cite{Milner1984}. Usability gradually improved, as progress was made in the areas of higher-order logic, type systems and unification \cite{Paulson2019}. The proof assistants that are currently available vary in designs, however different systems often share a set of similar features. Coq and Isabelle/HOL are two examples of widely adopted systems that have a vast repertoire of proven theorems \cite{Yushkovskiy2018}. Both support forward and backward reasoning, and are expressive enough to write procedures such as tactics. Their main differences boil down to the underlying theory and the implementation of their kernel \cite{Barras1999, Wenzel2021}. Coq is based on the calculus of constructions, while Isabelle/HOL relies on higher-order logic. +Historically, proof assistants consisted mainly on automating the process of demonstrating assertions rather than providing tools to assist the user in doing so; which is objectively a simpler task \cite{Harrison2014}. It is only later that designs have leaned towards user-centered systems with ideas such as the Edinburgh LCF, and subsequent work on metalogic and tactics \cite{Milner1984}. Usability gradually improved, as progress was made in the areas of higher-order logic, type systems and unification \cite{Paulson2019}. The proof assistants that are currently available vary in designs, however different systems often share a set of similar features. Coq and Isabelle/HOL are two examples of widely adopted systems that have a vast repertoire of proven theorems \cite{Yushkovskiy2018}. Both support forward and backward reasoning, and are expressive enough to write procedures such as tactics. Their main differences boil down to the underlying theory and the implementation of their verifier \cite{Barras1999, Wenzel2021}: Coq is based on the calculus of constructions, while Isabelle/HOL relies on higher-order logic. -\subsection{LCF-like framework} +\subsection{LCF-style framework} -In 2020 I worked on designing a LCF-like 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 in theorem proving such as the representation of proofs and tableaux solving strategies. One of the particularity of that framework was that formulas and more generally theorems were strongly typed. In the lines of the Curry-Howard Correspondence, this meant that the soundness could be enforced by the type checker alone. Naturally 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 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. 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. 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. \subsection{LISA} -Before starting this thesis I contributed to the design of LISA late 2021, notably by maintaining the codebase, reviewing and testing the proof checker, and exploring the design of third-party tools for LISA. This LISA project then ramified itself into several sub-projects, including this very thesis. The topic of projects lead by other persons include: formalization of other theories such as Peano's arithmetic, proof space exploration using deep learning methods, and interoperability with other tools, for example Stainless \cite{Kuncak2021}. During the period of the thesis I continued to occasionally work on LISA as it continued its maturation process. Some components and ideas designed in this front-end framework were integrated in LISA, and eventually the full framework strives to become a module of LISA. +Late 2021 before starting working on this thesis, I contributed to the design of LISA, notably by maintaining the codebase, reviewing and testing the proof checker, and exploring the design of third-party tools for LISA. This LISA project then ramified itself into several sub-projects, including this very thesis. The topic of projects lead by other persons include: formalization of other theories such as Peano's arithmetic, proof space exploration using deep learning methods, translation of natural language sentences into formal statements, and interoperability with other tools, for example Stainless \cite{Kuncak2021}. During the period of the thesis I continued to occasionally work on LISA as it proceeded further in its maturation process. Some components and ideas designed in this front-end framework were integrated in LISA. Eventually we are aiming to integrate the full framework proposed in this thesis as a module of LISA. diff --git a/thesis/report/chapters/3-framework.tex b/thesis/report/chapters/3-framework.tex index 60703b3..cd75800 100644 --- a/thesis/report/chapters/3-framework.tex +++ b/thesis/report/chapters/3-framework.tex @@ -1,11 +1,11 @@ \section{The framework} \label{sec:framework} -The work of this thesis is designated as ``a front-end for LISA''. The term ``front-end'' is generally used for layered architectures to outline a layer that is the closest to the end user. Though, what is understood as a user can vary depending on the context. In our case, we understand front-end as a programmatic interface for the user of LISA. More precisely, we were interested in designing a framework that depended on the LISA kernel and strove to provide a higher-level interface to construct and organize proofs. The use of an indefinite article in our designation is to emphasize the fact that such a layer is by essence guided by opinionated design choices (independent of LISA). +The work of this thesis is designated as ``a front-end for LISA''. The term ``front-end'' is generally used for layered architectures to outline a layer that is the closest to the user. Often this corresponds to some kind of interface, though what is understood as a user and an interface can vary depending on the context. In our case, we understand front-end as a programmatic interface for the end-user of LISA. More precisely, we were interested in designing a framework that depended on the LISA kernel and strove to provide a higher-level interface to develop proofs. The use of an indefinite article in our designation is to emphasize the fact that such a layer is by essence guided by opinionated design choices. -One could wonder about the necessity of relying on an existing system. The fundamental reason is to keep the core of the system sufficiently small and simple enough that it could be understood, reasoned about and perhaps formally proved by another system. We refer to this part as the \textbf{kernel} of LISA. The constraint over the complexity of the kernel gives us better reasons to trust it regarding its soundness. On the other side, the front-end does not make such claims and can thus be made arbitrarily more sophisticated. The only requirement is for the front-end to be able to reconstruct all of its proofs in the kernel, such that one could check them with the same level of confidence as if they were initially written there. We define soundness as the property for a proof in the front to have the same meaning as one in the kernel. By the requirement, soundness thus relies on the only assumption that statements in the front are logically equivalent to statements in the kernel. As a consequence such a system would satisfy the (informal) De Bruijn criterion, in the sense that the underlying proofs can be checked by a reasonably simple procedure (the kernel). +One could wonder about the necessity of relying on an existing system. The fundamental reason is to keep the core of the system sufficiently small and simple enough that it could be understood, reasoned about and perhaps formally proved by another system. We refer to this part as the \textbf{kernel} of LISA. The constraint on the complexity of the kernel gives us better reasons to trust its correctness. On the other side, the front-end does not make such claims and can thus be made arbitrarily more sophisticated. The only requirement is for the front-end to be able to reconstruct all of its proofs in the kernel, such that one could check them with the same level of confidence as if they were initially written there. We define soundness as the property for a proof in the front to have the same meaning as one in the kernel, and to be valid there. By the requirement, soundness thus relies on the only assumption that statements in the front are logically equivalent to statements in the kernel. As a consequence such a system would satisfy the De Bruijn criterion, in the sense that the underlying proofs can be checked by a reasonably simple procedure: the kernel. -Another aspect of the front is that despite its dependency on the kernel, it does not expose it to the user. Instead, it redefines most of its components and provides mappings for uni or bi-directional translations. The motivation is two-fold. First of all, it allows us to extend the existing functionality. Practically, for example, it was decided that the kernel would not provide schematic connectors as they were not strictly needed. However the front requires such a functionality for its rules and it is not possible to emulate them at low cost, consequently we implement this functionality in the front. Alternatively we can also strengthen some of its features, for instance by representing sequents as indexed sequences rather than sets. Additionally we can redefine the method \code{toString} on all of our classes. Secondly, it allows us to enrich the DSL and bring type safety guarantees. Some types in the kernel are (purposely) weak and require runtime checks to ensure safety. This aspect contributes to building a strong framework and is compatible with the mid-term objective of having LISA exist as a Scala library. +Another aspect of the front is that despite its dependency on the kernel, it does not expose it to the user. Instead, it redefines most of its components and provides mappings for uni or bi-directional translations. The motivation is two-fold. First of all, it allows us to extend the existing functionality. Practically, for example, it was decided that the kernel would not provide schematic connectors as they were not strictly needed. However the front requires such a functionality to represent its pattern variables and it is not possible to emulate them at low cost. Consequently we implement this functionality in the front and provide conversions. We can also strengthen some of the kernel features, for instance by representing sequents as indexed sequences rather than sets. We may additionally redefine the method \code{toString} on all of our classes. Secondly, it allows us to enrich the language and bring type safety guarantees. Some types in the kernel are (purposely) weak and require runtime checks to ensure safety. This aspect contributes to building a strong framework and is compatible with the mid-term objective of having LISA exist as a Scala library. \begin{figure}[H] \centering @@ -42,11 +42,11 @@ \section{The framework} \label{fig:front-kernel} \end{figure} -Finally, the interaction between the front and the kernel is relatively limited as the front handles its own state independently (\autoref{fig:front-kernel}). The common ground between the two are justified statements (axioms, theorems, definitions), which means that such objects can be converted back and forth. Whenever a theorem is proven in the front, it is translated to the kernel and checked for consistency. The front obtains the mirror of that justified statement and can be quite certain about its correctness. +The interaction between the front and the kernel is relatively limited as the front handles its own state independently (\autoref{fig:front-kernel}). The common ground between the two are justified statements (axioms, theorems, definitions), which means that such objects can be converted back and forth. Whenever a theorem is proven in the front, it is translated to the kernel and checked for consistency. The front obtains the mirror of that justified statement and can be quite certain about its correctness. This enables full compatibility with LISA, making it possible to lift theorems that were not proven in the front. \subsection{Language and tools} -The implementation was done in Scala version 3\footnote{Also known as Dotty: \href{https://dotty.epfl.ch}{dotty.epfl.ch}.}. The choice of version was a requirement, following the decision to upgrade LISA from version 2 to 3: because this project does not work directly on the LISA codebase, but instead depends on it as a library, both versions must be the same. Regarding the version, it turns out that some of the features implemented in this project would not have had an equivalent encoding in the older version, which lets us to confidently argue that Scala version 3 is an appropriate language for the design of DSL\footnote{DSL: domain specific language} libraries. +The implementation was done in Scala version 3\footnote{Also known as Dotty: \href{https://dotty.epfl.ch}{dotty.epfl.ch}.}. The choice of version was a requirement, following the decision to upgrade LISA from version 2 to 3. Since this project does not work directly on the LISA codebase but instead depends on it as a library, both versions must be the same. Regarding the version, it turns out that some of the features implemented in this project would not have had an equivalent encoding in the older version, which lets us to confidently argue that Scala version 3 is an appropriate language for the design of DSL\footnote{DSL: domain specific language} libraries. During the implementation, eight bugs were discovered in different areas of the Dotty compiler. All the issues that could be minimized and reproduced were reported\footnote{ \href{https://github.com/lampepfl/dotty}{github.com/lampepfl/dotty}: @@ -94,7 +94,7 @@ \subsection{Structure} \node at (6, -4.8) {\parbox{7cm}{\hspace*{0pt}\hfill(utilities that only rely on the kernel)}}; \node at (6, -5.4) {\parbox{7cm}{\hspace*{0pt}\hfill(older experiments)}}; \end{tikzpicture} - \caption[Source code packages structure]{Structure of the packages in the source code. The reader is invited to begin its study with the package \code{example}, which presents a collection of examples giving an overview of the framework.} + \caption[Source code packages structure]{Structure of the packages in the source code. The reader is invited to review the package \code{example}, which contains a collection of examples giving an overview of the framework.} \label{fig:packages} \end{figure} @@ -102,11 +102,11 @@ \subsection{Structure} \subsection{DSL} -Our framework introduces its own DSL\footnote{DSL: Domain-Specific Language, a custom language designed for a particular purpose.} implemented in Scala, which we briefly explain in this section. +Our framework introduces its own DSL\footnote{DSL: Domain-Specific Language, a custom language designed for a particular purpose.} implemented in Scala. In this section we briefly describe it and explain in more details two interesting problems. \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}), and provide the said compile-time safety guarantees. For instance the sequent $\vdash f(a, b), c \land d$ can be written as \code{|- (f(a, b), a /\textbackslash~a)} in Scala. Scala enables custom infix syntaxes, so 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), 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}). \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]) @@ -134,9 +134,9 @@ \subsection{DSL} (1, "2"): Seq[Int] // error \end{lstlisting} -The idea is to inductively deconstruct the tuple at compilation-time, using the polymorphic helper trait \code{Converter} and its \textit{given} implementations. If such an instance is successfully obtained, then the value can be successfully converted into a sequence thanks to the \code{Conversion} instance. With this method the types are preserved and we obtain a representation as a sequence of values which we can work with at runtime. +The idea is to inductively deconstruct the tuple at compilation-time, using the polymorphic helper trait \code{Converter} and its \textit{given} implementations. If such an instance can be constructed, then the value can be converted into a sequence thanks to the \code{Conversion} instance. With this method the types are preserved and we obtain a representation of the tuple as a sequence of values which we can work with at runtime. -The second problem we encountered was about checking the arguments when applying labels, namely ensuring that the correct number of arguments is passed. Labels represent unapplied functions, predicates or connectors, and they store information about the expected arity. A naive solution would be to manually encode common arities, but it is not satisfactory. The solution we adopted was once again a generic one (\autoref{lst:generic-tuples-2}). +The second problem we encountered was about checking the arguments when applying labels, namely ensuring that the correct number of arguments is passed with respect to the label's arity. Labels represent unapplied functions, predicates or connectors, and they store information about the expected arity. A naive solution would be to manually encode common arities, but it is not satisfactory. The solution we adopted was once again a generic one (\autoref{lst:generic-tuples-2}) that works for any arity. \begin{lstlisting}[language=Scala,caption={[Generic tuples (2)]{Generic tuples: enforcing correct function application arity. The type \code{HTuble} represents an homogeneous tuple, \code{Label} is a function label and \code{Applied} is an applied function.}},label={lst:generic-tuples-2}] type Arity = Int & Singleton @@ -162,6 +162,6 @@ \subsection{DSL} l2(a, a, a) // error \end{lstlisting} -The type \code{Arity} is defined as the intersection between the primitive \code{Int} type and the special \code{Singleton} synthetic type, which enforces a type to be the same as the value it models. For example the singleton type of the literal value \code{1} would be the literal type \code{1}. We constrain labels to specify their arity as this precise type, in order for us to use this information later. We then introduce the constructive type alias \code{HTuple} representing an heterogeneous tuple of arity \code{N} and for which all the members are of type \code{T}. Then, an \code{apply} method is added to the label taking an heterogeneous tuple as its own argument, representing the arguments passed to this label. The arity of the tuple is naturally the one specified by the label. Optionally we can protect the regular constructor of \code{Apply} to protect it from unsound usage. +The type \code{Arity} is defined as the intersection between the primitive \code{Int} type and the special \code{Singleton} synthetic type, which enforces a type to be the same as the value it models. For example the singleton type of the literal value \code{1} would be the literal type \code{1}. We constrain labels to express their arity in terms of this precise type, in order for us to use this information later. We then introduce the recursively defined type alias \code{HTuple} representing an homogeneous tuple of arity \code{N} and for which all the members are of type \code{T}. Then, an \code{apply} method is added to the label taking an homogeneous tuple as its own argument, representing the arguments passed to this label. The arity of the tuple is naturally the one specified by the label. Optionally we can protect the regular constructor of \code{Apply} to protect it from unsound usage. -The DSL also supports string interpolation which we chose to describe later, in \autoref{sec:parsing-printing-string-interpolation}. +The DSL also supports string interpolation which we describe later, in \autoref{sec:parsing-printing-string-interpolation}. diff --git a/thesis/report/chapters/4-proofs.tex b/thesis/report/chapters/4-proofs.tex index 5976b09..45f7b63 100644 --- a/thesis/report/chapters/4-proofs.tex +++ b/thesis/report/chapters/4-proofs.tex @@ -1,32 +1,34 @@ \section{Proofs} \label{sec:proofs} -LCF-like proof systems are notorious for the simplicity of their implementation, which makes them desirable foundational systems [citation needed]. However they also become a limiting factor in terms of usability, assuming they are used bare (that is without an overlay). For example incomplete proofs cannot be constructed, despite being useful in practice. Another example, which is a consequence of the former: proofs must be constructed in the forward direction only, meaning that the conclusion is dictated by the final construction (the last step) instead of being stated in advance as it is often done with pen and paper proofs. +LCF-like proof systems are notorious for the simplicity of their implementation, which makes them desirable foundational systems \cite{Paulson2019}. However they also become a limiting factor in terms of usability, assuming they are used bare (that is without an overlay). For example incomplete proofs cannot be constructed, despite being useful in practice. Another example, which is a consequence of the former: proofs must be constructed in the forward direction only, meaning that the conclusion is dictated by the final construction (the last step) instead of being stated in advance as it is often done with pen and paper proofs. + +\subsection{Terminology} \begin{definition}[Justified statement] -A \textbf{justified statement} is a sequent that is understood to be true within a theory. Axioms, theorems and definitions are examples of justified statements. +A \textbf{justified statement} of a theory is a sequent that is accepted by that theory. Axioms, theorems and definitions are examples of justified statements. \end{definition} -In LISA and in our system, sequents are the base logical construct. They carry a meaning that is at least as strong as formulas because any formula $\mathcal{F}$ can be encoded as $\vdash \mathcal{F}$. That is how axiomatic formulas are encoded. +In LISA and in our system, sequents are the base meta logical construct. They carry a meaning that is at least as strong as formulas because any formula $\mathcal{F}$ can be encoded as $\vdash \mathcal{F}$. This is also how axiomatic formulas are encoded. \begin{definition}[Theory] A \textbf{theory} (or \textbf{environment}) is a global context that contains a set of justified statements. It is constructed with an initial set of axioms and can be used to translate proofs into theorems and definitions. \end{definition} -The concept of theories is a formalization of mathematical theories. Namely it is a context with some axioms and definitions that one can use without proving. In our framework, axioms must be defined in advance (it is not possible to add more later). This provides more control over the critical parts of the system, in particular it ensures that an instance of a theory will have exactly those axioms and not more. Theorems can be obtained by providing a proof that depends on other justified statements of this theory. Definitions require a proof of uniqueness. These aspects are similar to the kernel's \code{RunningTheory}. Remark that a theory is stateful as one can always add more definitions to it. +The concept of theories is a formalization of mathematical theories. Namely it is a context with some axioms and definitions that one can use without proving. In our framework, axioms must be defined in advance (it is not possible to add more later). This provides more control over the critical parts of the system, in particular it ensures that an instance of a theory will have exactly those axioms and not more. Theorems can be obtained by providing a proof that depends on other justified statements of this theory. Definitions require a proof of uniqueness. These aspects are similar to the kernel's \code{RunningTheory}. Remark that a theory is stateful as one is allowed to add more definitions to it. \begin{definition}[Proof direction] A \textbf{forward proof} is a proof where the conclusion of each proof step is a justified statement. -A \textbf{backward proof} is a forward proof with the proof steps reversed. +A \textbf{backward proof} is a forward proof reversed, but for which only the final conclusion is a justified statement. \end{definition} -Forward proofs are conservative: when moving from one state to another the environment becomes strictly more rich. It is not the case for backward proofs, as it is possible to end up with proof states that are (provably) unprovable. One can observe that kernel proofs can easily be adapted to satisfy the forward reasoning definition, by transforming every proof step into an ordered sequence of proofs having one proof step. Moreover one can also see that forward and backward proofs are dual of each other. Backward proofs motivate the introduction of the following concepts, inspired by existing frameworks. +Forward proofs are conservative: when moving from one state to another the environment becomes strictly more rich. It is not the case for backward proofs, as it is possible to end up with proof states that are unprovable (and provably so). One can observe that kernel proofs can easily be adapted to satisfy the definition of forward reasoning, by transforming a proof having $n$ steps into $n$ proofs of one step and as many justified statements. Moreover one can also notice that valid forward and backward proofs are dual of each other. Backward proofs motivate the introduction of the following concepts, inspired by existing frameworks. \begin{definition}[Proof mode] The \textbf{proof mode} is a contextualized representation of a backward proof. \end{definition} -The proof mode is stateful: commands can be applied to update the internal state. The history of commands is also stored and is used to later generate the kernel proof. +The proof mode is stateful: commands can be applied to update the internal state. The history of commands is also stored and is used to later produce a kernel proof. \begin{definition}[Proof goal] In proof mode, a \textbf{proof goal} corresponds to a sequent that remains to be proven. @@ -38,11 +40,11 @@ \section{Proofs} In proof mode, the \textbf{proof state} is a stack of proof goals. \end{definition} -To enter proof mode it is required to provide an initial proof goal that will serve as an initial state to this proof mode. A statement is said to be proven once the proof state becomes empty, or in other words once all proof goals have been eliminated. Thus, proof modes with empty proof states should produce a valid kernel proof. +To enter proof mode it is required to provide an initial proof goal that will serve as an initial state to this proof mode. A statement is said to be proven once the proof state becomes empty, or in other words once all proof goals have been eliminated. Thus, proof modes having an empty proof state should produce a valid kernel proof. -Regarding the representation of the proof state as a stack, it is motivated by the fact that the order of the goals is arbitrary as it does not affect the realization of the proof. With that model in mind, the \textbf{current goal} naturally refers to the goal at the top of the stack. Therefore, by convention it is natural to choose to push new goals to the top of the stack since those are most likely to be proven next by the user. +Regarding the representation of the proof state as a stack, it is motivated by the fact that the order of the goals is arbitrary as does not affect the realization of the proof. With that model in mind, the \textbf{current goal} intuitively refers to the goal at the top of the stack. Therefore, by convention it is natural to choose to push new goals to the top of the stack since those are the most likely to be proven next by the user. -\begin{lstlisting}[language=Scala,caption={[Tactical proof]{Example of a tactical proof.}},label={lst:proof-interaction},captionpos=b] +\begin{lstlisting}[language=Scala,caption={[Backward proof]{Example of a backward proof.}},label={lst:proof-interaction},captionpos=b] val theorem: Theorem = { val p = ProofMode(sequent"|- (!?a \/ ?b) <=> (?a => ?b)") @@ -72,7 +74,7 @@ \section{Proofs} \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); \end{tikzpicture} - \caption[Tactical proof interaction]{Representation of the interaction of the tactical proof from \autoref{lst:proof-interaction}. The boxes represent the successive proof states and the edges correspond to the tactics applied.} + \caption[Tactical proof interaction]{Representation of the interaction of the backward proof from \autoref{lst:proof-interaction}. The boxes represent the successive proof states and the transitions correspond to the tactics applied.} \label{fig:proof-interaction} \end{figure} @@ -82,7 +84,7 @@ \subsection{Tactics} A \textbf{tactic} is a partial function that maps parameters and proof states to proof states and partial kernel proofs. \end{definition} -Informally, a tactic transforms a proof state into a new state, and the result of this transformation has a representation in terms of kernel proof steps. The former describes how the state evolves in the front while the latter does the synchronization with the kernel. +Informally, a tactic transforms a proof state into a new proof state, and the result of this transformation has a representation in terms of kernel proof steps. The former describes how the state evolves in the front while the latter does the synchronization with the kernel. Both are stored in the proof mode following a successful application of the tactic. Tactics can be categorized into more specific functions, for instance most tactics only work on a single goal by replacing it by zero or more new goals. Other tactics may only reorganize the proof, for instance by reordering goals. @@ -122,15 +124,15 @@ \subsection{Rules} \end{prooftree} $$ } - \caption[Correspondence between front rules and kernel steps]{Correspondence between front rules and kernel steps. The framed sequents represent the corresponding input and output of the rule.} + \caption[Correspondence between front rules and kernel steps]{Correspondence between a front rule and its kernel steps. The framed sequents represent the corresponding input and output of the rule.} \label{fig:example-rule} \end{figure} -Rule are by themselves not tactics, however a rule can be instantiated to obtain a tactic. In fact, since rules are made of patterns they could be applied in different ways on a same context. The parameters are there disambiguate the application of that rule. For instance they specify what formula of the sequent correspond to what pattern, and what variable assignment should be used. In proof mode, we are therefore trying to match the conclusion pattern of a rule against a proof goal. Successfully applying a rule replaces the current goal by a number of goals equal to the number of premises of that rule. Any formula that does not appear in the pattern will appear as is the new goals. Formally, an instantiated rule with premises $\vec{\phi_1} \vdash \vec{\psi_1}; ...; \vec{\phi_n} \vdash \vec{\psi_n}$ and conclusion $\vec{\phi_0} \vdash \vec{\psi_0}$ applied on a goal $\Gamma, \vec{\phi_0} \vdash \vec{\psi_0}, \Delta$ will replace this goal by the new goals $\Gamma, \vec{\phi_1} \vdash \vec{\psi_1}, \Delta; ...; \Gamma, \vec{\phi_n} \vdash \vec{\psi_n}, \Delta$. +Rule are by themselves not tactics, however a rule can be instantiated to obtain a tactic. In fact, since rules are made of patterns they could be applied in different ways on a same context. The parameters are needed to disambiguate the application of that rule. For instance they specify what formula of the sequent correspond to what pattern, and what variable assignment should be used. In proof mode, we are therefore trying to match the conclusion pattern of a rule against a proof goal. Successfully applying a rule replaces the current goal by a number of goals equal to the number of premises of that rule. Any formula that does not appear in the pattern will appear as is in the new goals. Formally, an instantiated rule with premises $\Sigma_1 \vdash \Pi_1 \hspace{0.5em} ; \hspace{0.5em} ... \hspace{0.5em} ; \hspace{0.5em} \Sigma_n \vdash \Pi_n$ and conclusion $\Sigma_0 \vdash \Pi_0$ applied on a goal $\Gamma, \Sigma_0 \vdash \Pi_0, \Delta$ will replace it by the new goals $\Gamma, \Sigma_1 \vdash \Pi_1, \Delta \hspace{0.5em} ; \hspace{0.5em} ... \hspace{0.5em} ; \hspace{0.5em} \Gamma, \Sigma_n \vdash \Pi_n, \Delta$. -Rules may also be applied forward in a very similar fashion: this time we are matching the premises against a sequence of justified statements, to obtain a new justified statement. Using the same notation as previously, justifications $\Gamma_1, \vec{\phi_1} \vdash \vec{\psi_1}, \Delta_1; ...; \Gamma_n, \vec{\phi_n} \vdash \vec{\psi_n}, \Delta_n$ will generate the new theorem $\Gamma_1 \cup ... \cup \Gamma_n, \vec{\phi_0} \vdash \vec{\psi_0}, \Delta_1 \cup ... \cup \Delta_n$. In practice, since the front stores sequents as pairs of indexed sequences of formulas, the union operation is a concatenation operation followed by the removal of duplicate formulas. +Rules may also be applied forward in a very similar fashion: this time we are matching the premises against a sequence of justified statements, to obtain a new justified statement. Using the same notation as previously, justifications $\Gamma_1, \Sigma_1 \vdash \Pi_1, \Delta_1 \hspace{0.5em} ; \hspace{0.5em} ... \hspace{0.5em} \hspace{0.5em} ; \hspace{0.5em} \Gamma_n, \Sigma_n \vdash \Pi_n, \Delta_n$ will generate the new theorem $\Gamma_1, ..., \Gamma_n, \Sigma_0 \vdash \Pi_0, \Delta_1, ..., \Delta_n$. In practice, since the front stores sequents as pairs of indexed sequences of formulas, the union operation is a concatenation operation followed by the removal of duplicate formulas. -Most of the kernel's proof steps can be translated into rules, and several kernel proof steps can be represented by a single rule. \autoref{fig:example-rule} shows an example rule and its translation in the kernel. The explanation on how patterns are matched against values can be found in \autoref{sec:matching}. +Most of the kernel's proof steps can be translated into rules, and several kernel proof steps can be represented by a single rule. \autoref{fig:example-rule} shows an example rule and its translation in the kernel. The specification for the matching of patterns against values can be found in \autoref{sec:matching}. \subsection{Tactics combinators} @@ -150,7 +152,7 @@ \subsection{Tactics combinators} \label{tab:tactics-combinators} \end{table} -These combinators make it possible to conveniently write simple routines, for instance a propositional solver (\autoref{lst:solver-combinators}). Remark that this particular procedure is deterministic and runs in exponential time in the worst case. The argument for the former is a proof by induction on the structure of the goal, while the argument for the latter is a pathological case (e.g. a sequence of conjunctions on the right side). More efficient heuristics could be used to slightly improve the runtime and the length of the proofs, however as per \cite{Krajicek1994} there exists tautologies that cannot be proven in less than an exponential number of LISA's sequent calculus steps (even with the cut rule). +These combinators make it possible to conveniently write simple routines, for instance a propositional solver (\autoref{lst:solver-combinators}). Remark that this particular procedure is deterministic and runs in exponential time in the worst case. The argument for the former is a proof by induction on the structure of the goal, while the argument for the latter is a pathological case (e.g. a sequence of conjunctions on the right side). More efficient heuristics could be used to slightly improve the runtime and the length of the proofs, however as per \cite{Krajicek1994} there exists tautologies that cannot be proven in less than an exponential number of LISA's sequent calculus steps, even if the cut rule was used. \begin{lstlisting}[language=Scala,caption={[Propositional solver]{A propositional solver written using exclusively rules and tactic combinators.}},label={lst:solver-combinators},captionpos=b] val autoProp = (introHypo @@ -181,15 +183,52 @@ \subsection{Justifications} val theorem = p.asTheorem() \end{lstlisting} -At line 5, the tactic \code{justificationInst} takes a justification as parameter and performs all the necessary rewrites and instantiations. Here we pass it a theorem of the form $\vdash \neg({?s} \in \emptyset)$ (lines 6-9); which matches with the current goal $\vdash \neg(\emptyset \in \emptyset), {?a}$. ${?s}$ is instantiated to $\emptyset$, and ${?a}$ is removed as part of a weakening step. +At line 5, the tactic \code{justificationInst} takes a justification as parameter and performs all the necessary rewrites and instantiations. Here we pass it a theorem of the form $\vdash \neg({?s} \in \emptyset)$ (lines 6-9); which matches against the current goal $\vdash \neg(\emptyset \in \emptyset), {?a}$. ${?s}$ is instantiated to $\emptyset$, and ${?a}$ is removed as part of a weakening step. \subsection{Proof-level state transformations} Because the proof mode is meant to be interactive, it implements commands to interact with the history, for instance to cancel an applied tactic or to restart the proof. While these features aren't particularly sophisticated they provide an interface for interactivity; the most primitive example of such an interface being the REPL\footnote{REPL: Read-Eval-Print Loop, a generic term to describe an environment that can interpret code interactively.}. +\begin{figure}[H] + \centering + \begin{tikzpicture}[box/.style = {draw, rectangle, minimum width=2cm, minimum height=0.75cm}, label/.style = {fill=white, inner sep=1,outer sep=1}, node distance = 1cm and 0.5cm] + \node[box, densely dotted] (mutator) {Proof-level mutator}; + \node[box, below left = of mutator] (cancel) {Cancel}; + \node[box, below = of mutator] (reset) {Reset}; + \node[box, densely dotted, below right = of mutator] (tactic) {Tactic}; + \node[box, densely dotted, below left = of reset] (tactic-goal) {Tactic goal}; + \node[box, right = of tactic-goal] (focus) {Focus}; + \node[box, right = of focus] (repeat) {Repeat}; + \node[box, right = of repeat] (fallback) {Fallback}; + \node[box, right = of fallback] (combine) {Sequence}; + \node[box, draw=none, right = of combine] (ellipsis-1) {...}; + \node[box, densely dotted, below = of tactic-goal] (tactic-functional) {Tactic functional}; + \node[box, right = of tactic-functional] (tactic-justify) {Tactic justify}; + \node[box, below = of tactic-functional] (rule) {Applied rule}; + \node[box, right = of rule] (solver) {Solver}; + \node[box, draw=none, right = of solver] (ellipsis-3) {...}; + \draw (cancel) |- ($(reset)!0.5!(mutator)$); + \draw[->] (reset) -- (mutator); + \draw (tactic) |- ($(reset)!0.5!(mutator)$); + \draw[<-] (tactic) -- ++(0, -0.9) -| (tactic-goal); + \draw (focus) -- ++(0, 0.87); + \draw (repeat) -- ++(0, 0.87); + \draw (fallback) -- ++(0, 0.87); + \draw (combine) -- ++(0, 0.87); + \draw (tactic) ++(0, -0.9) -| (ellipsis-1); + \draw[->] (tactic-functional) -- (tactic-goal); + \draw (tactic-justify) |- ($(tactic-functional)!0.5!(tactic-goal)$); + \draw[->] (rule) -- (tactic-functional); + \draw (solver) -- ++(0, 0.88); + \draw (ellipsis-3) |- ($(rule)!0.5!(tactic-functional)$); + \end{tikzpicture} + \caption[Hierarchy of tactics]{Hierarchy of tactics and relation with proof-level mutators.} + \label{fig:front-tactic} +\end{figure} + \subsection{Mixing proof styles} -Our framework allows both forward and backward to be used. The most common use case is to transform a justification to eliminate a goal. Some rules are also more commonly used in a mode than another. For example, instantiation rules are more intuitively understood when used forward while weakening rules are more naturally used backward. +Our framework allows both forward and backward to be used. The most common use case is to transform a justification to eliminate a goal. Some rules are also more commonly used in a mode than another. For example, instantiation rules are more intuitively understood when used forward while weakening rules are generally used backward. \begin{figure}[H] \centering diff --git a/thesis/report/chapters/5-synthesis.tex b/thesis/report/chapters/5-synthesis.tex index f9f02bc..e85b955 100644 --- a/thesis/report/chapters/5-synthesis.tex +++ b/thesis/report/chapters/5-synthesis.tex @@ -1,19 +1,19 @@ \section{Proof synthesis} \label{sec:synthesis} -\subsection{Front-end proof to kernel proof} - In the front a backward proof is characterized by an initial proof goal and a sequence of tactics to apply such that they eventually reduce the goal to nil. Forward proofs in the front are much more concise as they are the result of a single step; e.g. a forward rule application. As stated in the requirements, we would like to be able to translate these two proofs into kernel proofs. We describe how this process works in this section. Note that since we are not that much interested in the final shape of the proof, it is not strictly speaking a one-to-one translation but rather a synthesis (or a reconstruction) process. Such a relaxation allows us for instance to optimize the proof. +\subsection{Front-end proof to kernel proof} + For backward proofs the first step is to reverse the order of the tactics and successive states. This is necessary as kernel proofs must be constructed forward; any changes to existing steps would require a complete reorganization of the proof. At the same time, we should also label each distinct proof goal as they will either represent an individual proof step or an import in the final kernel proof. This mechanism is achieved thanks to the \textbf{shadow proof state}, which associates identifiers to the goals in the proof state. That way, when a proof goal is transformed into subgoals we can recover the ids of the premises and the current step. Similarly, when proof goals are reordered we should update the shadow state accordingly to reflect the new order. -Then, we can proceed with the reconstruction of the kernel proof. Recall that the tactics are listed in reverse order. The result of applying the tactic is a partial kernel proof that should be included as is in the reconstruction. The imports of this partial proof are updated to the corresponding steps in the final proof, and the partial proof is appended to the final proof. This partial proof can then be referred to as a single step with index equal to the size of the final proof minus one. +Then, we can proceed with the reconstruction of the kernel proof. Recall that the tactics are listed in reverse order. The result of applying the tactic is a partial kernel proof that should be included as is in the reconstruction. The imports of this partial proof are updated to the corresponding steps in the final proof, and the partial proof is appended to the final proof. This partial proof can then be referred to as a single step whose index is equal to the size of the final proof minus one. \subsection{Optimizations} The front can translate its high-level proof representation into kernel proofs. The exported proofs are mainly intended for the proof checker rather than human readers. Regardless, we would like the generated proofs to be reasonably concise and easily verifiable. We could imagine that a larger proof base might take a non-negligible amount of time to be fully checked. Moreover these proofs would have to be shipped to the end users, taking up disk space, and the verification would also have to be performed on every host machine. -We identified that the following factors would impact negatively the complexity (computational complexity of verifying the proof) and the size (entropy of the representation of the proof): +We identified that the following factors would have a negative impact on complexity (computational complexity of verifying the proof) and size (entropy of the representation of the proof): \begin{itemize} \item Total number of proof steps @@ -24,13 +24,11 @@ \subsection{Optimizations} The front provides some efforts to minimize some of these factors. However, because of its versatility and complexity we should not fully rely on it. For that reason it makes sense to design optimization techniques that work directly on kernel proofs. -This general problem happens to relate to the area of compiler optimizations, in particular kernel proofs could be thought of as a sequence of static single assignments, where each value would be a call to some function taking previously computed values as arguments (the premises). - -We implement and describe a few techniques in the following sub-sections. +This general problem happens to relate to the area of compiler optimizations, in particular kernel proofs could be thought of as a sequence of static single assignments, where each value would be a call to some function taking previously computed values as arguments (the premises). We describe and implement a few techniques in the following sub-sections. \subsubsection{Dead branches elimination} -Recalling that proof in LISA is a directed acyclic graph, we can notice that it does not enforce the graph to be connected. Furthermore we can observe that a proof acts as a blackbox taking some premises and returning a conclusion. All the individual proof steps are not available from outside of that proof. Therefore, a proof that is a disconnected graph will not carry more information, and can by essence be simplified. +Recalling that a proof in LISA is a directed acyclic graph, we can realize that it does not enforce the graph to be connected. Furthermore we can observe that a proof acts as a blackbox taking some premises and returning a conclusion: apart from the conclusion no proof steps can be referenced outside of that proof. Therefore, a proof that is a disconnected graph will be longer but will not carry more information, and can by essence be simplified. \begin{definition}[Dead branches] A proof step or an import is said to be dead if it is different than the conclusion and all the steps that reference it as a premise are also dead. @@ -40,7 +38,7 @@ \subsubsection{Dead branches elimination} Finally we can just iterate over the proof steps in the order in which they appear and remove the ones that are marked as dead. The premises should be remapped accordingly; i.e. if a step is removed then all the indices that follow should be decreased by one. This can be done in a single pass by storing the new mapping in a hash map. -Note that this procedure should be applied recursively on children subproofs first, otherwise we would have to run the procedure several times (precisely, a number proportional to the depth of the proof). This gives without surprise a linear-time algorithm. +Note that this procedure should be applied recursively on children subproofs first, otherwise we would have to run the procedure several times (precisely, a number proportional to the depth of the proof). This yields without any surprise a linear-time algorithm. \begin{figure}[H] \centering @@ -62,16 +60,15 @@ \subsubsection{Dead branches elimination} \draw [thick] (5.25,-0.75) rectangle (9.75,0.75); \node [label={[shift={(7.5,0.75)}](4)}] {}; \end{tikzpicture} - \caption[Dead branch elimination]{Example of applying the dead branch elimination procedure on a proof. Each node represents a proof step or an import; the rectangle represents a subproof step. The nodes in gray are part of dead branches. (3) and ($4_{-1}$) are dead because they are not referenced by any other step. (2) is dead because it is only referenced by (3) and ($4_{-2}$), which are dead. In this situation we can remove the steps (2), (3) along with the import ($4_{-2}$).} + \caption[Dead branch elimination]{Example of applying the dead branch elimination procedure on a proof. Each node represents a proof step or an import; the rectangle represents a subproof step. The nodes in gray are part of dead branches. (3) and ($4_{-1}$) are dead because they are not referenced by any other step. (2) is dead because it is only referenced by (3) and ($4_{-2}$), which are dead. In this situation we can safely remove the steps (2), (3) along with the import ($4_{-2}$).} \label{fig:synthesis-dead-branches} \end{figure} \subsubsection{Proof flattening} -A synthesis procedure can make use of subproofs for its own convenience, for instance to dynamically remap premises of an existing proof. Nested subproofs could potentially lead to arbitrarily deep proofs, which is totally valid but can affect the readability and the performances. - -This motivates the need of a procedure that can ``flatten'' a proof by inlining all the occurrences of subproofs. +A synthesis procedure can make use of subproofs for its own convenience, for instance to dynamically remap premises of an existing proof. Nested subproofs could potentially lead to arbitrarily deep proofs, which are totally valid but can affect the readability and the performances of the checking process. +This motivates the need of a procedure that can ``flatten'' a proof by inlining all occurrences of subproofs. \begin{figure}[H] \centering @@ -130,9 +127,9 @@ \subsubsection{Proof flattening} \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 heuristic to approach a generally hard problem: finding the shortest sequent calculus proof in propositional logic is a known hard problem \cite{Krajicek1994}. +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 terminate. For that we 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}. 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. diff --git a/thesis/report/chapters/6-matching.tex b/thesis/report/chapters/6-matching.tex index 8378bdf..071de66 100644 --- a/thesis/report/chapters/6-matching.tex +++ b/thesis/report/chapters/6-matching.tex @@ -3,9 +3,9 @@ \section{Matching} Matching is the process of finding an assignment for a pattern such that when this pattern is instantiated with that assignment, the result equals the target value. Namely, given two terms $\phi$ and $\psi$, we are looking for a substitution $\sigma$ such that $\phi[\sigma] = \psi$. Matching can be seen as a special case of a more general problem called unification $\phi[\sigma] = \psi[\sigma]$, because the patterns appear only on one side \cite{Knight1989}. -Most programming languages that implement pattern matching, such as Scala, disallow the reuse of pattern variables. These kinds of patterns are referred to as linear. On the other hand, non-linear patterns allow variables to appear multiple times. In that case the usually implied semantic is that all the occurrences of the same variable should be pairwise equal. +Most programming languages that implement pattern matching, such as Scala, disallow the reuse of pattern variables. These kinds of restricted patterns are referred to as linear. On the other hand, non-linear patterns allow variables to appear multiple times. In that case the usually implied semantic is that all the occurrences of the same variable should be pairwise equal. -In this framework we relax the notion of equality for non-linear pattern variables by allowing them to be equivalent with respect the equivalence checker implemented in LISA: the orthocomplemented bisemilattices (OCBSL) equivalence checker \cite{Guilloud2022}. This leads to an ambiguity in the assignment because by construction a variable can only be assigned a single value; thus not only will the resulting assignment may not lead to an instantiation that is structurally equal to the target, but it is also unclear which assigned value to choose. To address these ambiguities, we define deterministic rules that are not necessarily practical but are required to exhibit consistent behavior over different execution contexts. +In this framework we relax the notion of equality for non-linear pattern variables by allowing them to be equivalent with respect the equivalence checker implemented in LISA: the orthocomplemented bisemilattices (OCBSL) equivalence checker \cite{Guilloud2022}. This leads to an ambiguity in the assignment because by construction a variable can only be assigned a single value; thus not only may the resulting assignment not lead to an instantiation that is structurally equal to the target, but it is also unclear which assigned value to choose. To address these ambiguities, we define deterministic rules that are not necessarily intended to be practical but are required to exhibit consistent behavior over different execution contexts. \subsection{Terminology} @@ -15,7 +15,7 @@ \subsection{Terminology} A \textbf{tree} refers to either a term, a formula or a sequent. \end{definition} -The type of a tree is known and gives its nature (term, formula or sequent). +The type of a tree is known and indicates its nature (term, formula or sequent). \begin{definition}[Pattern variable and constant] A \textbf{pattern variable} is a term or a formula represented as a schema or a bound/free variable. @@ -41,7 +41,7 @@ \subsection{Terminology} \subsection{Specification} -The goal is to find an assignment for the sequence of patterns such that when it is instantiated it becomes equivalent to the sequence of values. Each pattern is matched against the value located at the same index in the sequence. The matching is successful if all the patterns can be resolved without reaching a contradiction. The matching fails if a contradiction is reached, or if the problem is under-constrained (solution space is infinite). If a solution is returned, then it should always be a superset of the provided partial assignment. By default the partial assignment is the empty set. +The goal is to find an assignment for the sequence of patterns such that when it is instantiated it becomes equivalent to the sequence of values. Each pattern is matched against the value located at the same index in the sequence. The matching is successful if all the patterns can be resolved without reaching a contradiction. The matching fails if a contradiction is reached, or if the problem is under-constrained (solution space is infinite, or problem is ill-posed). If a solution is returned, then it should always be a superset of the provided partial assignment. By default the partial assignment is the empty set. Because the procedure can also be used to rename bound variables, the pattern should not declare a bound variable more than once. Moreover, no free variable can reuse the name of a bound variable, regardless the scope. Apart from these restrictions, all pattern variables can appear any number of times in the pattern. In addition, pattern variables can appear as arguments of other pattern variables (without any limitation on the depth). @@ -96,7 +96,7 @@ \subsection{Specification} \item By specifying the predicate, the problem is transformed into the matching of $t = u$ against pattern ${?x} = u$ (where ${?x}$ is a fresh variable). \item The first pattern/value pair is the same as (7), however the second pair adds the necessary constraint to reduce the problem to (8). \item The problem is under-constrained because the argument contains an unresolved variable. -\item Similar to (10), the variable is resolved while handling the second pair unlocking the first one. In addition, both branches are factored because they are equivalent. +\item Similarly to (10), the variable is resolved while handling the second pair unlocking the first one. In addition, both branches are factored because they are equivalent. \item This example showcases the renaming of bound/free variables. \item Here ${?a}$ is a variable that should match a constant. However the formula $y = u$ depends on the bound variable $y$, and thus cannot match that pattern. \item This is a fix for (14): the bound variable appears as an argument of the predicate variable. @@ -110,21 +110,21 @@ \subsubsection{Preliminary checks} \subsubsection{Fresh names} -Schemas and variables have a different meaning depending whether they appear in the pattern or in the value. One of the requirements was to avoid extending the first order logic package with new datatypes. To disambiguate both meanings there are two options. The first one consists of defining a new intermediate representation that is exclusive to patterns. The alternative approach is to rename schemas and variable in such a way that we can distinguish them from each other. The second option was chosen as the implementation is significantly shorter. +Schemas and variables have a different meaning depending whether they appear in the pattern or in the value. One of the requirements was to avoid extending the first order logic package with new datatypes. To disambiguate both meanings there are two options. The first one consists of defining a new intermediate representation that is exclusive to patterns. The alternative approach is to rename schemas and variable in such a way that we can distinguish them from each other. The second option was chosen not only because its implementation is significantly shorter, but because it also simplified some use cases as schemas were designed to be instantiated. -The first step of the algorithm is therefore to list all schemas and variables on both sides, and then to rename all schemas and pattern variables by freshly generated identifiers. The mapping should be kept because we will use it to restore the original names at the end. The mapping also serves as a predicate to determine whether a name is a pattern variable or a constant. +The first step of the algorithm is therefore to list all schemas and variables on both sides, and then to rename them by freshly generated identifiers. The mapping between the original names and the fresh ones should be kept because we will use it to restore the names at the end. The mapping also serves as a predicate to determine whether a name is a pattern variable or a constant. \subsubsection{Constraints collection} -Pattern variables can appear as arguments of other pattern variables, which does not make it possible to solve the constraints in a single traversal. Instead, we decompose the problem into different phases, which can be mutually recursive. The first one of these is the constraints enumeration. A constraint is a triplet consisting of a pattern variable, its arguments and a target value. In this phase we traverse the pattern and value trees at the same time, in pre-order. As long as the pattern is constant, the only task done by this procedure is to ensure that both sides are structurally equal. When a pattern variable is encountered, a constraint is returned and the traversal stops for this branch. At any point, if a contradiction is detected, it is transferred back to the first caller in order to halt the procedure; we further refer to that as a \textbf{failure}. +Pattern variables can appear as arguments of other pattern variables, which does not make it possible to solve the constraints in a single traversal. Instead, we decompose the problem into different phases, which can be mutually recursive. The first one of these being the constraints collection phase. A constraint is a triplet consisting of a pattern variable, its arguments and a target value. In this phase we traverse the pattern and value trees at the same time, in pre-order. As long as a pattern node is constant, the only liability of this procedure is to ensure that both sides are structurally equal. When a pattern variable is encountered, a constraint is returned and the traversal stops for this branch. At any point, if a contradiction is detected, it is transferred back to the first caller in order to halt the procedure; we further refer to that as a \textbf{failure}. \subsubsection{Pattern to value matching} -At this point we have not determined to what value each pattern corresponded to. This information may be provided explicitly but may as well be omitted. This is essentially an instance of a bipartite matching problem, however one that we cannot easily solve efficiently. The reason is because the pattern to value matching cannot be considered independent, therefore we cannot construct the bipartite graph efficiently. The solution we adopted was to enumerate all possible bipartite matching in a lazy manner, and then call the constraints resolution on each such matching until a valid solution is found. We argue that in practice the cost associated to this solution is not high as the number of premises and conclusions in a sequent remains low. +At this point we have not determined to what value each pattern corresponded to. This information may be provided explicitly but may as well be omitted. This can be seen as an instance of a bipartite matching problem, however one that we cannot easily solve efficiently. The reason is because the pattern to value matching cannot be considered independent, therefore we cannot construct the bipartite graph efficiently. The solution we adopted was to enumerate all possible bipartite matching instances in a lazy manner, and then call the constraints resolution on each such matching until a valid solution is found. We argue that in practice the cost associated to this solution is not high as the number of premises and conclusions in a sequent remains low. \subsubsection{Constraints resolution} -After collecting the constraints the objective of the next phase is to attempt to resolve them. We say that a constraint is resolved as soon as the pattern variable it represents has been assigned a value in this context, and that value is compatible with the constraint's. For that, the constraints are processed in the order they appear; by assumption these constraints were listed in pre-order. However, not all constraints can be immediately solved: sometimes the resolution of a constraint may unlock another constraint. Therefore while there remains unsolved constraints the procedure picks the first constraints that can be solved. If none exists, that means the problem is under-constrained and the procedure returns a failure. Although the current implementation of the resolution phase does not create additional constraints, other implementations that may want to return a result for under-constrained instances has the possibility to produce and return additional constraints. In that case the new constraints are inserted at the same position in the sequence. +After collecting the constraints the objective of the next phase is to attempt to resolve them. We say that a constraint is resolved as soon as the pattern variable it represents has been assigned a value in this context, and that value is compatible with the constraint's. For that, the constraints are processed in the order they appear; by assumption these constraints were listed in pre-order. However, not all constraints can be immediately solved: sometimes the resolution of a constraint may unlock another constraint. Therefore while there remains unsolved constraints the procedure picks the first constraints that can be solved. If none exists, that means the problem is under-constrained and the procedure returns a failure. Although the current implementation of the resolution phase does not create additional constraints, other implementations that may want to return a result for under-constrained instances has the possibility to produce and return such additional constraints. In that case the new constraints are inserted at the same position in the sequence. In this phase a constraint can be solved if and only if all the pattern variables in the pattern's arguments have been assigned a value with respect to the current context. As a consequence, all constraints represented by nullary schemas or variables can be solved immediately. @@ -132,11 +132,11 @@ \subsubsection{Constraints resolution} If the pattern variable is already assigned a value, we instantiate this assignment with the instantiated arguments and compare it against the value for equivalence. If we cannot prove that they are equivalent we return a failure, otherwise we do not do anything and carry on. -If the pattern variable does not have an assigned value we must assign one to it. If applicable we generate fresh schemas for the arguments of this assignment. We then apply a greedy factoring algorithm to replace all occurrences of the instantiated arguments by their associated schema. Again, we traverse the tree in pre-order to satisfy the specification, and then find the first instantiated argument that is equivalent to this node. The factoring procedure cannot fail: an special case could be that no value is factored, however it is still a valid solution. +If the pattern variable does not have an assigned value we must assign one to it. If applicable we generate fresh schemas for the arguments of this assignment. We then apply a greedy factoring algorithm to replace all occurrences of the instantiated arguments by their associated schema. Again, we traverse the tree in pre-order to satisfy the specification, and then find the first instantiated argument that is equivalent to this node. The factoring procedure cannot fail: a special case could be that no value is factored, however that is still a valid solution. \subsubsection{Conclusion} -If all the constraints have been solved, we can return that solution after restoring the original pattern variable names. +If all the constraints have been solved, we can return the assignment as a solution after restoring the original pattern variable names. \subsection{Analysis} @@ -147,12 +147,12 @@ \subsection{Analysis} {a \equiv b} \implies {x[a \mapsto b] \equiv x} \tag{\textsc{Substitution}} \end{gather} -It is easy to see that these properties hold for logical equivalence. For the substitution property of OCBSL equivalence, because $a \equiv b$, both $a$ and $b$ reduce to a common normal form $n$. Therefore $x[a \mapsto b] \equiv x$ is the same problem as $x[a \mapsto b][\{a, b\} \mapsto n] \equiv x[\{a, b\} \mapsto n]$ which is a tautology. For transitivity we have that $\{x, y\}$ have a normal form $n_1$, $\{y, z\}$ a normal form $n_2$, $\{x, z\}$ a normal form $n_3$. Because $y$ has a normal form equal to $n_1$ and $n_2$ it must be the case that $n_1 = n_2$; therefore $n_1 = n_2 = n_3$. +It is easy to see that these properties hold for logical equivalence. For the substitution property of OCBSL equivalence, since $a \equiv b$, both $a$ and $b$ reduce to a common normal form $n$. Therefore $x[a \mapsto b] \equiv x$ is the same problem as $x[a \mapsto b][\{a, b\} \mapsto n] \equiv x[\{a, b\} \mapsto n]$ which is a logical tautology. For transitivity we have that $\{x, y\}$ have a normal form $n_1$, $\{y, z\}$ a normal form $n_2$, $\{x, z\}$ a normal form $n_3$. Because $y$ has a normal form equal to $n_1$ and $n_2$ it must be the case that $n_1 = n_2$; therefore $n_1 = n_2 = n_3$. It should be noted that in any case, $x \equiv y \implies x \Leftrightarrow y$. Therefore, even though a resolved pattern may not be checked for equivalence (e.g. if a weaker or alternative checker is used), it is still expected to be logically equivalent. \subsection{Limitations and extensions} -The procedure is by design incomplete, i.e. there are problem instances where a matching (as we defined it) exists but would not be found. For instance, the pattern ${?a} \land b$ matches the value $b \land a$ but despite being OCBSL equivalent, it would not be detected by the algorithm. This issue could be solved relatively easily at an exponential cost by enumerating all the equivalent formulas and calling matching on them. We suspect this problem to be solvable in polynomial time, as an extension of OCBSL. +The procedure is by design incomplete, i.e. there are problem instances where a matching (as we defined it) exists but would not be found. For instance, the pattern ${?a} \land b$ matches the value $b \land a$ but despite being OCBSL equivalent, it would not be detected by the algorithm. This issue could be solved relatively easily at an exponential cost by enumerating all the equivalent formulas and calling matching on them. We suspect this problem to be solvable in polynomial time, as an extension of OCBSL, but we could not come up with an algorithm to demonstrate it. \subsection{Applications} diff --git a/thesis/report/chapters/7-parsing-printing.tex b/thesis/report/chapters/7-parsing-printing.tex index 7c97816..851d628 100644 --- a/thesis/report/chapters/7-parsing-printing.tex +++ b/thesis/report/chapters/7-parsing-printing.tex @@ -3,7 +3,7 @@ \section{Parsing and printing} \subsection{Grammar} -At the time of writing this thesis, LISA does not have a formalized concrete syntax grammar for its language but rather a simple printer that is used to display proofs in a more readable way. In this project I defined a grammar for the first-order logic language with sequents of the front-end (\autoref{fig:grammar}). The grammar is designed to be unambiguous so that we could use it for serialization/persistence later on, and is as close as possible to the original printer of LISA. The main challenge in designing a grammar for our language is due to the fact that the distinction between terms and formulas is made early on, in other words it is not possible to construct ill-typed trees. This subtlety opens the door to potential ambiguities where it is unclear if a node should be interpreted as a term or a formula. The front-end avoids thanks to a carefully designed grammar and a type checker that serves at the same time as a resolver. +At the time of writing this thesis, LISA does not have a formalized concrete syntax grammar for its language but rather a simple printer that is used to display proofs in a more readable way. In this project I defined a grammar for the first-order logic language with sequents of the front-end (\autoref{fig:grammar}). Unlike the former printer, the grammar is designed to be unambiguous so that we could use it for serialization/persistence later on, and is as close as possible to the original printer of LISA. The main challenge in designing a grammar for our language is due to the fact that the distinction between terms and formulas is made early on, in other words it is not possible to construct ill-typed trees. This subtlety opens the door to potential ambiguities where it is unclear if a node should be interpreted as a term or a formula. The front-end avoids this issue thanks to a carefully designed grammar and a type checker that resolves an intermediate representation into well-typed trees. \begin{figure}[H] \centering @@ -49,13 +49,13 @@ \subsection{Grammar} ((( `;')* `...') | ) \end{grammar} \end{framed} - \caption[BNF grammar]{BNF grammar for the front. The rules for precedence are the usual ones. The current system uses an extended syntax which simply adds convenient aliases for common symbols in set theory (empty, singleton and pair sets, constants, etc.).} + \caption[BNF grammar]{BNF grammar for the front. The precedence of operators is the usual one. The current system uses an extended syntax, not shown here, which simply adds convenient aliases for common symbols of set theory (empty, singleton and pair sets, constants, etc.).} \label{fig:grammar} \end{figure} \subsection{Parsing} -A parser for this grammar was written using \code{scala-parser-combinators} \cite{Moors2008}, a recursive-descent parsing library for Scala. The parser alone is not sufficient to generate the final trees; an intermediate phase called \textbf{resolution} performs type checking and resolves the intermediate representation into its final form. The procedure is dictated by the rules listed in \autoref{fig:typing-rules}. Given the type of the top-level term, we can recover all the remaining types in the tree and thus reconstruct the final representation of the tree. +A parser for this grammar was written using \code{scala-parser-combinators} \cite{Moors2008}, a recursive-descent parsing library for Scala. The parser alone is not sufficient to generate the final trees; an intermediate phase called \textbf{resolution} performs type checking and resolves the intermediate representation into its final form. The procedure is dictated by the rules listed in \autoref{fig:typing-rules}. Given the type of the top-level term, we can show by induction that it is possible to recover all the remaining types in the tree, and thus reconstruct the final representation of the tree. \begin{figure}[H] \centering @@ -81,7 +81,7 @@ \subsection{Parsing} \frac{}{\Gamma, x \vdash x: \mathcal{T}} \tag{\textsc{Variable}} \end{gather} \end{framed} - \caption[Type inference rules]{Type inference rules. $\mathcal{T}$, $\mathcal{F}$ and $\mathcal{S}$ represent term, formula and sequent types respectively. The metasymbol $x$ represents identifiers, while $t$ represents parsed terms. An optional question mark symbol can precede identifiers. It can be shown that given a top-level formula, it is always possible to unambiguously type all the children terms.} + \caption[Type inference rules]{Type inference rules. $\mathcal{T}$, $\mathcal{F}$ and $\mathcal{S}$ represent term, formula and sequent types respectively. The meta symbol $x$ represents identifiers, while $t$ represents parsed terms. An optional question mark symbol can precede identifiers. Given a well-formed top-level formula, it is always possible to unambiguously type all the children terms.} \label{fig:typing-rules} \end{figure} @@ -116,18 +116,18 @@ \subsection{Parsing} \subsection{Compile-time string interpolation} \label{sec:parsing-printing-string-interpolation} -While the parser was originally designed for runtime usage, it can also be used by the compiler at compilation-time. This is possible thanks to the fact that the Scala 3 allows multi-stage metaprogramming. That enables the user to manipulate values (\code{T}), expressions for these values (\code{Expr[T]}) or even expressions of expressions for these values (\code{Expr[Expr[T]]}); all within the same program. +While the parser was originally designed for runtime usage, it can also be used by the compiler at compilation-time. This is possible thanks to the fact that the Scala 3 allows multi-stage metaprogramming. The user can manipulate values (\code{T}), expressions for these values (\code{Expr[T]}) or even expressions of expressions for these values (\code{Expr[Expr[T]]}); all within the same program. -The idea was to exploit this mechanism to guarantee safe parsing at compile-time. Thus, if the user attempts to parse an invalid string literal, the compiler would raise an error. The implementation of that feature is relatively straight forward and is done within a macro. First we extract the string literal value from the expression, then we call our parser on it and finally convert the resulting tree to an expression (that is, in the meta-level converting \code{T} to \code{Expr[T]}). The last step requires defining conversion methods for all ADT members. +The idea was to exploit this mechanism to guarantee safe parsing at compile-time. Thus, if the user attempts to parse an invalid string literal, the compiler would raise a type error. The implementation of that feature is relatively straight forward and is done within a macro. First we extract the string literal value from the expression, then we call our parser on it and finally convert the resulting tree to an expression (at the meta-level, that is converting a \code{T} to an \code{Expr[T]}). The last step requires defining conversion methods for all ADT members. -It turns out we can do better than that. Scala offers a feature called string interpolators which additionally allows variables to be ``inserted'' within the string literal (\autoref{fig:string-interpolation-general}). Moreover, it only works on string literals thus guaranteeing the recovery of the value at compile-time. +It turns out we can do better than that. Scala offers a feature called \textit{string interpolator} which additionally allows variables to be ``inserted'' within the string literal (\autoref{fig:string-interpolation-general}). Moreover, it only works on string literals thus guaranteeing the recovery of the value at compile-time. \begin{lstlisting}[language=Scala,caption={[String interpolation general example]{Simple demonstration of the string interpolation mechanism in Scala. The \code{s} interpolator simply calls \code{toString} on each variable passed and concatenates all the parts together.}},label={fig:string-interpolation-general},captionpos=b] val s1: String = "world" val s2: String = s"Hello $s1!" // Hello world! \end{lstlisting} -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 express names dynamically, e.g. \code{formula"\$p(s)"}. Notice that the previous expression is structurally different from \code{formula"\${p(term"s")}"}, although it leads to the same formula. +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] \centering @@ -170,7 +170,7 @@ \subsection{Compile-time string interpolation} \label{fig:multi-stage-parsing} \end{figure} -To implement this feature, we must execute the different parsing phases separately (\autoref{fig:multi-stage-parsing}). One can observe that in a well-formed interpolator, tokens (as output by the lexer) cannot possibly overlap different string parts. That property let us to do lexing on each string part independently. From this step we can then identify all the potentially taken identifiers allowing us to safely create fresh ones. Then, all the variables are replaced by fresh schemas; still represented as tokens at this point. Finally, we can proceed to the parsing and type checking phases. The first type checking phase will assign types to all of our fresh schemas, while the second will ensure that these assigned types agree with the Scala types of the interpolated variables. A disagreement or an error at an earlier phase is mapped to a positioned Scala type error. Finally all that is left to do is substitute those schemas by their actual value, and convert the value into an expression tree. Notice that we cannot do that at compilation-time as we don't have access to the variables' values: only their type. But this makes sense: types model the range of allowed values, the rest of the information is to be discovered at runtime. Therefore the tree should be constructed at compilation-time, while the final substitution can only happen at runtime. +To implement this feature, we must execute the different parsing phases separately (\autoref{fig:multi-stage-parsing}). One can observe that in a well-formed interpolator, tokens (as output by the lexer) cannot possibly overlap different string parts. That property let us do lexing on each string part independently. From this step we can then identify all the potentially taken identifiers allowing us to safely create fresh ones. Then, all the variables are replaced by fresh schemas; still represented as tokens at this point. Finally, we can proceed to the parsing and type checking phases. The first type checking phase will assign types to all of our fresh schemas, while the second will ensure that these assigned types agree with the Scala types of the interpolated variables. A disagreement or an error at an earlier phase is mapped to a positioned Scala type error. Finally all that is left to do is substitute those schemas by their actual value, and convert the value into an expression tree. Notice that we cannot do that at compilation-time as we don't have access to the variables' values: only their type. But this makes sense: types model the range of allowed values, the rest of the information is to be discovered at runtime. Therefore the tree should be constructed at compilation-time, while the final substitution must happen at runtime. We also studied the possibility of implementing \code{unapply} macros for pattern matching, which could be useful in a tactic language. We concluded that the implementation would be somewhat similar to \code{apply}. We could also make use of the matcher, for instance when matching partial sequents. However, the support for inlining on string interpolators \code{unapply} is currently only partial\footnote{\href{https://github.com/lampepfl/dotty/issues/8577}{github.com/lampepfl/dotty/issues/8577}}. diff --git a/thesis/report/chapters/8-future-work.tex b/thesis/report/chapters/8-future-work.tex index 243de88..cb1f18b 100644 --- a/thesis/report/chapters/8-future-work.tex +++ b/thesis/report/chapters/8-future-work.tex @@ -1,19 +1,19 @@ \section{Future work} \label{sec:future-work} -While the original goal of this framework was to propose an opinionated front-end for LISA, we do not exclude the possibility of integrating some useful components directly into LISA (as is, or in a refined version). That includes all the logic for bidirectional parsing and printing (possibly with macros), proof utilities and optimization routines, and a matcher or unifier. It should also be decided whether it would be worth strengthening the kernel to provide support for schematic connectors, which are as we have shown essential elements for unification tasks. +While the original goal of this framework was to propose an opinionated front-end for LISA, we do not exclude the possibility of integrating some useful components directly into LISA (as is, or in a refined version). That includes all the logic for bidirectional parsing and printing (possibly with macros), proof utilities and optimization routines, and the matcher. It should also be decided whether it would be worth strengthening the kernel to provide support for schematic connectors, which are as we have shown essential elements for unification tasks. Similarly, we should also decide on the future of free/bound variables, as they could very well be represented by nullary functions. The following subsections expose known limitations of the framework, how they could be addressed and finally a selected list of potential ramifications that could be explored as a sequel to this project. \subsection{Limitations} -Despite our efforts and the previous iterations, we have discovered a few limitations in the current version of the system and present them here along with a hint for a potential fix. +Despite our efforts and the previous iterations, we have discovered a few limitations in the current version of the system and present them here. Unlike the kernel, the front does not have an explicit error reporting system when writing proofs. This means that if a tactic is incorrectly applied the result of the optional will be empty but will not indicate the reason. This lack hinders the usability of the framework as it is more difficult to debug the construction of proofs. The reason for such absence is because we have not yet been able to unify the tactic arguments APIs in an elegant way, thus postponing the implementation of such a mechanism. Similarly, the matcher does not have error reporting either; the various possible failure are all encoded as an empty option. The framework is also missing the implementation of more pre-defined tactics, which would make the framework more practical. The difficulty is to identify what are the most common sequences of steps when writing proofs, and to come up with a way to factor them out into tactics. -Finally, although Scala 3 provides an indisputably more powerful language to write DSLs, we have observed that the compiler was still not entirely stable. This lead us to the discovery of several compiler bugs, and sometimes required us to adapt our code around the bogus components. These unstable behaviors can unfortunately affect the end user as our framework relies heavily on these newer features. However, we are confident that these problems will eventually fade away thanks to the fast-paced ongoing work on the compiler. +Finally, although Scala 3 provides an indisputably more powerful language to write DSLs, we have observed that the compiler was still not entirely stable. This lead us to the discovery of several compiler bugs, and sometimes required us to adapt our code around the bogus components. These unstable behaviors can unfortunately affect the end user as our framework relies heavily on these newer features. However, we are confident that the problems will eventually fade away thanks to the fast-paced ongoing work on the compiler. \subsection{Next steps} diff --git a/thesis/report/chapters/9-conclusion.tex b/thesis/report/chapters/9-conclusion.tex index 3a98cf4..7b4fa95 100644 --- a/thesis/report/chapters/9-conclusion.tex +++ b/thesis/report/chapters/9-conclusion.tex @@ -1,6 +1,6 @@ \section{Conclusion} \label{sec:conclusion} -In this project we explored the implementation of a front-end for LISA. We demonstrated the feasibility and practicality of mixing backward and forward proof styles. We introduced a concept of tactics, and we focused on the implementation of rules which provide a scalable interface to represent compound proof steps. We implemented a general matching procedure that can be used to infer most of the parameters when applying rules. We showed that our procedure was applicable to other use cases, such as the instantiation of justifications. On top of that, we also significantly improved the tooling which LISA can directly benefit from: a type safe DSL, a two-way parser/printer and various utilities to work with kernel proofs. Overall, our work was focused on interactivity and usability, and to that extent we have succeeded in producing a framework that was usable in a REPL environment. We exposed the limitations we have encountered or accidentally introduced, and provided ideas to solve them. +In this project we explored the implementation of a front-end for LISA. We argued that such a layered structure was a crucial design aspect to build a sound proof assistant. We demonstrated the feasibility and practicality of mixing backward and forward proof styles, and observed that it significantly helped users to write proofs. We introduced a concept of tactics, and we focused on the implementation of rules which provide a scalable interface to represent compound proof steps. We implemented a general matching procedure that can be used to infer most of the parameters when applying rules. We showed that our procedure was applicable to other use cases, such as the instantiation of justifications. On top of that, we also significantly improved the tooling which LISA can directly benefit from: a type safe DSL, a two-way parser/printer and various utilities to work with kernel proofs. Overall, our work was focused on interactivity and usability, and to that extent we have succeeded in producing a framework that was usable in a REPL environment. We exposed the limitations we have encountered or accidentally introduced, and provided ideas to solve them. -I would like to personally thank Viktor and Simon for giving me the opportunity to work on the early version of LISA, and later for the supervision of this thesis. I would also like to thank all of the members of the LARA laboratory for the rich discussions and precious advice I received from them. +I would like to personally thank Viktor and Simon for giving me the opportunity to contribute early on to the design of LISA, and later for supervising this thesis. I would also like to thank all of the members of the LARA laboratory for the rich discussions and precious advice they shared. diff --git a/thesis/report/figures/fol-erd.tex b/thesis/report/figures/fol-erd.tex index 2833479..65d620b 100644 --- a/thesis/report/figures/fol-erd.tex +++ b/thesis/report/figures/fol-erd.tex @@ -104,6 +104,6 @@ \draw [oone to many] (formula.north) ++(-0.6, 0) |- ++(0, 0.75) |- ++(1.2, 0) -| ++(0, -0.75); \draw [one to nmany] (term.north) ++(-0.6, 0) |- ++(0, 0.75) |- ++(1.2, 0) -| ++(0, -0.75); \end{tikzpicture} - \caption[First-order logic relationships]{First-order logic relationships presented in \textit{crow's foot notation}. Each relation corresponds to at least one syntactic combinator.} + \caption[First-order logic relationships]{First-order logic relationships presented in \textit{crow's foot} notation. Each relation corresponds to at least one syntactic combinator.} \label{fig:fol-erd} \end{figure}