From 127d1fbc9a60b38104d4842b615d5674930c346b Mon Sep 17 00:00:00 2001 From: Mysaa Date: Wed, 16 Aug 2023 22:23:39 +0200 Subject: [PATCH] Added a bit more bibliography --- ZOL2.lagda | 2 +- report/Bilibibio.bib | 68 +++++++++++++++++++++++++++++++++++++------- report/M1Report.tex | 22 +++++++------- report/header.tex | 2 +- 4 files changed, 71 insertions(+), 23 deletions(-) diff --git a/ZOL2.lagda b/ZOL2.lagda index 0132bb0..1ac55d1 100644 --- a/ZOL2.lagda +++ b/ZOL2.lagda @@ -42,7 +42,7 @@ module ZOL2 where Pf : (Γ : Con) → For Γ → Prop ℓ⁴ -- Action on morphisms _[_]p : {Γ Δ : Con} → {F : For Γ} → Pf Γ F → (σ : Sub Δ Γ) → Pf Δ (F [ σ ]f) - -- Equalities below are useless because Pf Γ F is in prop + --# Equalities below are useless because Pf Γ F is in prop -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Pf Γ F} -- → prf [ id {Γ} ]p ≡ prf -- []p-∘ : {Γ Δ Ξ : Con}{α : Sub Ξ Δ}{β : Sub Δ Γ}{F : For Γ}{prf : Pf Γ F} diff --git a/report/Bilibibio.bib b/report/Bilibibio.bib index 8f55507..05c0f05 100644 --- a/report/Bilibibio.bib +++ b/report/Bilibibio.bib @@ -1,13 +1,3 @@ -@article{RedFreeNorm1995, - doi = {10.1007/3-540-60164-3_27}, - url = {https://doi.org/10.1007\%2F3-540-60164-3_27}, - year = 1995, - publisher = {Springer Berlin Heidelberg}, - pages = {182--199}, - author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher}, - title = {Categorical reconstruction of a reduction free normalization proof}, - booktitle = {Category Theory and Computer Science} -} @article{NBE2016, title={Normalisation by Evaluation for Dependent Types}, author={Thorsten Altenkirch and Ambrus Kaposi}, @@ -39,3 +29,61 @@ author = {Uemura, T.}, year = {2021}, } + +@article{logicalFramework1993, + author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon}, + title = {A Framework for Defining Logics}, + year = {1993}, + issue_date = {Jan. 1993}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = {40}, + number = {1}, + issn = {0004-5411}, + url = {https://doi.org/10.1145/138027.138060}, + doi = {10.1145/138027.138060}, + abstract = {The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-Lo¨f's system of arities. The treatment of rules and proofs focuses on his notion of a judgment. Logics are represented in LF via a new principle, the judgments as types principle, whereby each judgment is identified with the type of its proofs. This allows for a smooth treatment of discharge and variable occurence conditions and leads to a uniform treatment of rules and proofs whereby rules are viewed as proofs of higher-order judgments and proof checking is reduced to type checking. The practical benefit of our treatment of formal systems is that logic-independent tools, such as proof editors and proof checkers, can be constructed.}, + journal = {J. ACM}, + month = {jan}, + pages = {143–184}, + numpages = {42}, + keywords = {formal systems, interactive theorem proving, proof checking, typed lambda calculus} +} + +@article{hoffmann1999, + author = {Hofmann, Martin}, + title = {Semantical Analysis of Higher-Order Abstract Syntax}, + year = {1999}, + isbn = {0769501583}, + publisher = {IEEE Computer Society}, + address = {USA}, + abstract = {A functor category semantics for higher-order abstract syntax is proposed with the following aims: relating higher-order and first order syntax, justifying induction principles, suggesting new logical principles to reason about higher-order syntax}, + booktitle = {Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science}, + pages = {204}, + series = {LICS '99} +} + +@article{fioreMahmoud2013secondorder, + title={Second-Order Algebraic Theories}, + author={Marcelo Fiore and Ola Mahmoud}, + year={2013}, + eprint={1308.5409}, + archivePrefix={arXiv}, + primaryClass={cs.LO} +} +@article{RedFreeNorm1995, + doi = {10.1007/3-540-60164-3_27}, + url = {https://doi.org/10.1007\3-540-60164-3_27}, + year = 1995, + publisher = {Springer Berlin Heidelberg}, + pages = {182--199}, + author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher}, + title = {Categorical reconstruction of a reduction free normalization proof}, + booktitle = {Category Theory and Computer Science} +} + + + + + + diff --git a/report/M1Report.tex b/report/M1Report.tex index e839a4e..a3908a2 100644 --- a/report/M1Report.tex +++ b/report/M1Report.tex @@ -25,15 +25,13 @@ In the first place, I was supposed to do this internship in Nottingham (UK) with Thorsten Altenkirsh. But, because of administrative issues, I was not able to go there, and Thorsten Altenkirsh contacted Ambrus Kaposi in Budapest, whose university agreed to accept me. Therefore, I went to Budapest and I did the internship under the physical supervision of Ambrus Kaposi, and the remote supervision of Thorsten Altenkirsch. - The original subject of the internship was \enquote{Developing a simplified account of normalization by evaluation using the theory of categories with families}. But there was a lot to do, starting with learning how to use Agda. - \subsection{Introduction to the problem} - What we call a \enquote{logic} is a set of definitions containing formulas and a notion of provability of those formulæ, plus a set of operators/equalities to construct or reduce these proofs. I have studied the most common logical frameworks, that is, Propositional Logic, First-Order Logic with an infinitary operator, and Predicate Logic. For each of those logics, one can define a notion of \emph{model}. A model of a certain kind of logic is something that implements all of the logic's definitions, operators, and equalities. From all of those models, one can extract the \emph{initial model}, also called \emph{syntax}. It is the smallest of all models, which means that for any model of that logic, we have a morphism from the syntax to this model. + What we call a \enquote{logic} or \enquote{logical framework} is a set of definitions containing formulas and a notion of provability of those formulæ, plus a set of operators/equalities to construct or reduce these proofs \cite{logicalFramework1993}. I have studied the most common logical frameworks, that is, Propositional Logic, First-Order Logic with an infinitary operator, and Predicate Logic. For each of those logics, one can define a notion of \emph{model}. A model of a certain kind of logic is something that implements all of the logic's definitions, operators, and equalities. From all of those models, one can extract the \emph{initial model}, also called \emph{syntax}. It is the smallest of all models, which means that for any model of that logic, we have a morphism from the syntax to this model. Then, our goal is for each logic to prove the completeness of a specific class of models. Completeness can be stated as such: \enquote{For any formula, if it is provable in all models of the specified class, then it has a proof in the syntax}. \subsection{Motivation} - Ambrus is currently studying Second-Order Generalized Algebraic Theories (or SOGAT) and he is trying to state a better definition than that first defined in Taichi Uemura's thesis \cite{UemuraThesis2021}. He also wants to write a paper with examples to show why they are useful, and adding some examples for different frameworks of logic can help with that. + Ambrus is currently studying Second-Order Generalized Algebraic Theories (or SOGAT) and he is trying to state a better definition than that first defined in Taichi Uemura's thesis \cite{UemuraThesis2021}. He also wants to write a paper with examples to show why they are useful, and adding some examples for different frameworks of logic can help with that. Having a completeness proof in this (categorical) higher order setting \cite{hoffmann1999} can help. \subsection{Structure of this report} @@ -98,7 +96,7 @@ With those context extensions, we also have to add a way to extend substitutions (which are the morphisms from the base category). We do that by adding a \emph{comma} operator that takes a substitution and a proof and which extends the goal of the substitution. (If we see a proof context as a list of formulæ and a proof substitution as a list of proofs, the action of the comma operator is simply to add one proof to the list). We also need to be able to extract the proof and the base substitution from a substitution into an extended context (called \emph{weakening} operation). Therefore, we add two $\pi$ projections that extract the data from the substitution. We also need some equalities, that are saying that $(\AgdaField{$\pi_p¹$} , \AgdaField{$\pi_p²$})$, and $\AgdaField{$,_p$}$ are reciprocal, plus one equality saying that the comma operator also transposes the substitution. But as both \AgdaField{Pf} and \AgdaField{Sub} are in \Prop{}, those equations are unneeded. \begin{tcolorbox} - \agda{agda/ZOL-5.tex} + \agda{agda/ZOL-6.tex} \end{tcolorbox} The last step is to add the constructors of our objects into the algebra. We write them directly as they were presented in the SOGAT, except for the new \AgdaField{Con} parameter that we need to add to everything. We also need to add one equation for each constructor saying that the constructors do respect substitutions. And we don't add any for \AgdaField{Pf} constructors as they are unneeded as \AgdaField{Pf} are in \AgdaPrimitive{Prop}. @@ -106,18 +104,18 @@ The only one we cannot translate directly is the $\rightarrow^+$ from the \lam{} constructor from the SOGAT. To translate this \emph{locally representable application}, we transform the parameter of the arrow into a context extension of the appropriate type. Therefore, a function $\Pf\; A \rightarrow^+ \Pf\; B$ becomes a proof $\Pf\; (\Gamma \:\AgdaField{$\triangleright_p$}\, A)\; B$ (except that we have to transform B that is a $\For\;\Gamma$ into a $\For\;(\Gamma \:\AgdaField{$\triangleright_p$}\, A)$, using the \emph{weakening} substitution $\AgdaField{$\pi_p¹$}\;\AgdaField{id}\;:\;\AgdaField{Sub}\;\Gamma\;(\Gamma \:\AgdaField{$\triangleright_p$}\, X)$ for any Γ-formula $X$) \begin{tcolorbox} - \agda{agda/ZOL-8.tex} - \agdasep \agda{agda/ZOL-9.tex} \agdasep - \agda{agda/ZOL-11.tex} + \agda{agda/ZOL-10.tex} + \agdasep + \agda{agda/ZOL-12.tex} \end{tcolorbox} We now have completed our definition of a model for Propositional Logic, in the SOGAT setting. In the meantime, we will define (categorical) morphisms between models. They are composed of mappings for every sort of the GAT, plus equations for the categorical objects (terminal object, identity, and composition), for the action of the functors on morphisms ($[]f$ and $[]p$), and finally equations to say that the constructors are also transported by the morphism. A lot of those equations are not written because \AgdaField{Pf} and \AgdaField{Sub} are in \Prop{}. \begin{tcolorbox} - \agda{agda/ZOL-13.tex} + \agda{agda/ZOL-14.tex} \agdasep - \agda{agda/ZOL-15.tex} + \agda{agda/ZOL-16.tex} \end{tcolorbox} \subsection{Finding a strict syntax} @@ -197,7 +195,7 @@ This works because, in the universal model, a context is a map from contexts of the syntax to \AgdaPrimitive{Prop} (because the category is posetal). \begin{center} - \begin{tikzpicture}[thick, scale=5] + \begin{tikzpicture}[thick, scale=3] \node at (-1,0) (nI) {$\mathcal{I}$}; \node at (1,0) (nU) {$\mathcal{U}$}; @@ -265,6 +263,8 @@ You can notice that we have only worked with negative fragments of logic (i.e. without disjunction) because then, Kripke models would not have been sufficient to make the completeness proof. This is another way to extend the work done during this internship. + During the internship, i also studied different forms of normalization proofs (i.e. saying that if we have a proof of $A$ in $\Gamma$ then we have a \emph{normal} proof of $A$ in $\Gamma$) using different wide subcategories of $\bCon$. One of those normalizations was exactly completeness. We will try to study a formalization for other logical frameworks of this \enquote{generalized normalization proof} \cite{RedFreeNorm1995}. + \section{First-order logic (or Predicate Logic)} In this part, we will try to implement the same as we did for Propositional Logic, but this time for Predicate Logic. We again work in a simpler layout where we don't have function symbols and only have one binary relation \AgdaField{R}. And again, adding other relations and function symbols does not add a lot of new interesting content, but makes everything less readable and more complex to use. diff --git a/report/header.tex b/report/header.tex index 0264dcb..7915f63 100644 --- a/report/header.tex +++ b/report/header.tex @@ -35,7 +35,7 @@ \usepackage{mathtools} \usepackage{textgreek} -\usepackage{geometry} +\usepackage[textheight=0.75\paperheight]{geometry} \usepackage{csquotes} \usepackage[lighttt]{lmodern}