-
From Tractatus to Later Writings and Back -- New Implications from the Nachlass
Authors:
Ruy J. G. B. de Queiroz
Abstract:
As a celebration of the \emph{Tractatus} 100th anniversary it might be worth revisiting its relation to the later writings. From the former to the latter, David Pears recalls that ``everyone is aware of the holistic character of Wittgenstein's later philosophy, but it is not so well known that it was already beginning to establish itself in the \emph{Tractatus}" (\emph{The False Prison}, 1987). Fr…
▽ More
As a celebration of the \emph{Tractatus} 100th anniversary it might be worth revisiting its relation to the later writings. From the former to the latter, David Pears recalls that ``everyone is aware of the holistic character of Wittgenstein's later philosophy, but it is not so well known that it was already beginning to establish itself in the \emph{Tractatus}" (\emph{The False Prison}, 1987). From the latter to the former, Stephen Hilmy's (\emph{The Later Wittgenstein}, 1987) extensive study of the \emph{Nachlass} has helped removing classical misconceptions such as Hintikka's claim that ``Wittgenstein in the \emph{Philosophical Investigations} almost completely gave up the calculus analogy." Hilmy points out that even in the \emph{Investigations} one finds the use of the calculus/game paradigm to the understanding of language, such as ``in operating with the word" (Part I, §559) and ``it plays a different part in the calculus". Hilmy also quotes from a late (1946) unpublished manuscript (MS 130) ``this sentence has use in the calculus of language"), which seems to be compatible with ``asking whether and how a proposition can be verified is only a particular way of asking `How do you mean?'." Central in this back and forth there is an aspect which seems to deserve attention in the discussion of a semantics for the language of mathematics which might be based on (normalisation of) proofs and/or Hintikka/Lorenzen game-dialogue: the explication of consequences. Such a discussion is substantially supported by the use of the open and searchable \emph{The Wittgenstein Archives at the University of Bergen}. These findings are framed within the discussion of the meaning of logical constants in the context of natural deduction style rules of inference.
△ Less
Submitted 21 April, 2023;
originally announced April 2023.
-
The Theory of an Arbitrary Higher $λ$-Model
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
Abstract:
One takes advantage of some basic properties of every homotopic $λ$-model (e.g.\ extensional Kan complex) to explore the higher $βη$-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher $λ$-terms, whose equality rules would be…
▽ More
One takes advantage of some basic properties of every homotopic $λ$-model (e.g.\ extensional Kan complex) to explore the higher $βη$-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher $λ$-terms, whose equality rules would be contained in the theory of any $λ$-homotopic model.
△ Less
Submitted 26 April, 2023; v1 submitted 13 November, 2021;
originally announced November 2021.
-
Solving Homotopy Domain Equations
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
Abstract:
In order to get $λ$-models with a rich structure of $\infty$-groupoid, which we call "homotopy $λ$-models", a general technique is described for solving domain equations on any cartesian closed $\infty$-category (c.c.i.) with enough points. Finally, the technique is applied in a particular c.c.i., where some examples of homotopy $λ$-models are given.
In order to get $λ$-models with a rich structure of $\infty$-groupoid, which we call "homotopy $λ$-models", a general technique is described for solving domain equations on any cartesian closed $\infty$-category (c.c.i.) with enough points. Finally, the technique is applied in a particular c.c.i., where some examples of homotopy $λ$-models are given.
△ Less
Submitted 9 September, 2022; v1 submitted 2 April, 2021;
originally announced April 2021.
-
Towards a Homotopy Domain Theory
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
Abstract:
An appropriate framework is put forward for the construction of $λ$-models with $\infty$-groupoid structure, which we call \textit{homotopic $λ$-models}, through the use of an $\infty$-category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and $λ$-calculus, in the sense that the concept of proof (path) of equality of…
▽ More
An appropriate framework is put forward for the construction of $λ$-models with $\infty$-groupoid structure, which we call \textit{homotopic $λ$-models}, through the use of an $\infty$-category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and $λ$-calculus, in the sense that the concept of proof (path) of equality of $λ$-terms is raised to \textit{higher proof} (homotopy).
△ Less
Submitted 26 October, 2022; v1 submitted 29 July, 2020;
originally announced July 2020.
-
Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system
Authors:
Tiago M. L. Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
We use a labelled deduction system ( LND$_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which allowed us to carry out in homotopic theory an approach using the concept of computational paths. From this, we show that the computational paths can be used to perform the proofs of the $LND_{EQ}-TRS_{2}$ rewriting system…
▽ More
We use a labelled deduction system ( LND$_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which allowed us to carry out in homotopic theory an approach using the concept of computational paths. From this, we show that the computational paths can be used to perform the proofs of the $LND_{EQ}-TRS_{2}$ rewriting system.
△ Less
Submitted 17 November, 2023; v1 submitted 13 July, 2020;
originally announced July 2020.
-
Capivara: A decentralized package version control using Blockchain
Authors:
Felipe Zimmerle da N. Costa,
Ruy J. Guerra B. de Queiroz
Abstract:
Distributed consensus and Blockchains are popular among the cryptocurrencies where no one except the coins users, owns the data and transactions. No different to open source repositories, where the data belongs to the users. In this work it is presented a manner of having a repository for software packages in a Blockchain with distributed consensus, supported by the idea of the also demonstrated p…
▽ More
Distributed consensus and Blockchains are popular among the cryptocurrencies where no one except the coins users, owns the data and transactions. No different to open source repositories, where the data belongs to the users. In this work it is presented a manner of having a repository for software packages in a Blockchain with distributed consensus, supported by the idea of the also demonstrated proof-of-download.
△ Less
Submitted 30 July, 2019;
originally announced July 2019.
-
An alternative approach to the calculation of fundamental groups based on labeled natural deduction
Authors:
Tiago M. L. de Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
In this work, we use a labelled deduction system based on the concept of computational paths (sequence of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We use a labelled deduction system based on the concept of computational paths (se…
▽ More
In this work, we use a labelled deduction system based on the concept of computational paths (sequence of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We use a labelled deduction system based on the concept of computational paths (sequence of rewrites) to obtain some results of algebraic topology and with support of the Seifet-Van Kampen Theorem we will calculate, in a way less complex than the one made in mathematics \cite{Munkres} and the technique of homotopy type theory \cite{hott}, the fundamental group of Klein Blottle $\mathbb{K}^2$, of the Torus $\mathbb{T}^2$ and Two holed Torus $\mathbb{M}_2=\mathbb{T}^2\# \mathbb{T}^2$ (the connected sum two torus).
△ Less
Submitted 19 June, 2019;
originally announced June 2019.
-
A Topological Application of Labelled Natural Deduction
Authors:
Tiago M. L. Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We then proceed to show the main result here: using this system to obtain the calculation of th…
▽ More
We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We then proceed to show the main result here: using this system to obtain the calculation of the fundamental group of the circle, of the torus and the real projective plane.
△ Less
Submitted 9 May, 2021; v1 submitted 19 June, 2019;
originally announced June 2019.
-
The $\infty$-groupoid generated by an arbitrary topological $λ$-model
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
Abstract:
The lambda calculus is a universal programming language. It can represent the computable functions, and such offers a formal counterpart to the point of view of functions as rules. Terms represent functions and this allows for the application of a term/function to any other term/function, including itself. The calculus can be seen as a formal theory with certain pre-established axioms and inferenc…
▽ More
The lambda calculus is a universal programming language. It can represent the computable functions, and such offers a formal counterpart to the point of view of functions as rules. Terms represent functions and this allows for the application of a term/function to any other term/function, including itself. The calculus can be seen as a formal theory with certain pre-established axioms and inference rules, which can be interpreted by models. Dana Scott proposed the first non-trivial model of the extensional lambda calculus, known as $ D_\infty$, to represent the $λ$-terms as the typical functions of set theory, where it is not allowed to apply a function to itself. Here we propose a construction of an $\infty$-groupoid from any lambda model endowed with a topology. We apply this construction for the particular case $D_\infty$, and we see that the Scott topology does not provide enough information about the relationship between higher homotopies. This motivates a new line of research focused on the exploration of $λ$-models with the structure of a non-trivial $\infty$-groupoid to generalize the proofs of term conversion (e.g., $β$-equality, $η$-equality) to higher-proofs in $λ$-calculus.
△ Less
Submitted 17 January, 2021; v1 submitted 13 June, 2019;
originally announced June 2019.
-
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths
Authors:
Tiago Mendonça Lucena de Veras,
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the equality between two terms of the same type as a collection of homotopical paths between points of the same space. Since this is only a semantical interpretation, the addition of paths to the syntax of homotopy t…
▽ More
One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the equality between two terms of the same type as a collection of homotopical paths between points of the same space. Since this is only a semantical interpretation, the addition of paths to the syntax of homotopy type theory has been recently proposed by De Queiroz, Ramos and De Oliveira . In these works, the authors propose an entity known as `computational path', proposed by De Queiroz and Gabbay in 1994, and show that it can be used to formalize the identity type. We have found that it is possible to use these computational paths as a tool to achieve one central result of algebraic topology and homotopy type theory: the calculation of fundamental groups of surfaces. We review the concept of computational paths and the $LND_{EQ}-TRS$, which is a term rewriting system proposed by De Oliveira in 1994 to map redundancies between computational paths. We then proceed to calculate the fundamental group of the circle, cylinder, M{ö}bius band, torus and the real projective plane. Moreover, we show that the use of computational paths make these calculations simple and straightforward, whereas the same result is much harder to obtain using the traditional code-encode-decode approach of homotopy type theory.
△ Less
Submitted 17 May, 2018; v1 submitted 3 April, 2018;
originally announced April 2018.
-
On the Use of Computational Paths in Path Spaces of Homotopy Type Theory
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira,
Tiago Mendonça Lucena de Veras
Abstract:
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is i…
▽ More
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is indeed equal to $b$. Based on that, a proof of equality can be seen as a sequence of substitutions and rewrites, also known as a `computational path'. One interesting fact is that it is possible to rewrite computational paths using a set of reduction rules arising from an analysis of redundancies in paths. These rules were mapped by De Oliveira in 1994 in a term rewrite system known as $LND_{EQ}-TRS$. Here we use computational paths and this term rewrite system to work with path spaces. In homotopy type theory, the main technique used to define path spaces is the code-encode-decode approach. Our objective is to propose an alternative approach based on the theory of computational paths. We believe this new approach is simpler and more straightforward than the code-encode-decode one. We then use our approach to obtain two important results of homotopy type theory: the construction of the path space of the naturals and the calculation of the fundamental group of the circle.
△ Less
Submitted 2 March, 2018;
originally announced March 2018.
-
Sequentialization for full N-Graphs via sub-N-Graphs
Authors:
Ruan V. B. Carvalho,
Lais S. Andrade,
Anjolina G. de Oliveira,
Ruy J. G. B. de Queiroz
Abstract:
Since proof-nets for MLL- were introduced by Girard (1987), several studies have appeared dealing with its soundness proof. Bellin & Van de Wiele (1995) produced an elegant proof based on properties of subnets (empires and kingdoms) and Robinson (2003) proposed a straightforward generalization of this presentation for proof-nets from sequent calculus for classical logic. In 2014 it was presented a…
▽ More
Since proof-nets for MLL- were introduced by Girard (1987), several studies have appeared dealing with its soundness proof. Bellin & Van de Wiele (1995) produced an elegant proof based on properties of subnets (empires and kingdoms) and Robinson (2003) proposed a straightforward generalization of this presentation for proof-nets from sequent calculus for classical logic. In 2014 it was presented an extension of these studies to obtain a proof of the sequentialization theorem for the fragment of N-Graphs with conjunction, disjunction and negation connectives, via the notion of sub-N-Graphs. N-Graphs is a symmetric natural deduction calculus with multiple conclusions that adopts Danos-Regnier's criterion and has defocussing switchable links. In this paper, we present a sequentization for full propositional classical N-Graphs, showing how to find a split node in the middle of the proof even with a global rule for discharging hypothesis.
△ Less
Submitted 1 March, 2018;
originally announced March 2018.
-
Explicit Computational Paths
Authors:
Arthur Freitas Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is i…
▽ More
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$, whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that establishes that $a$ is indeed equal to $b$. Based on that, a proof of equality can be seen as a sequence of substitutions and rewrites, also known as a `computational path'. One interesting fact is that it is possible to rewrite computational paths using a set of reduction rules arising from an analysis of redundancies in paths. These rules were mapped by De Oliveira in 1994 in a term rewrite system known as $LND_{EQ}-TRS$. Here we use computational paths and this term rewrite system to develop the main foundations of homotopy type theory, i.e., we develop the lemmas and theorems connected to the main types of this theory, types such as products, coproducts, identity type, transport and many others. We also show that it is possible to directly construct path spaces through computational paths. To show this, we construct the natural numbers and the fundamental group of the circle, showing results connected to these structures.
△ Less
Submitted 25 April, 2018; v1 submitted 16 September, 2016;
originally announced September 2016.
-
Formalization of context-free language theory
Authors:
Marcus V. M. Ramos,
Ruy J. G. B. de Queiroz,
Nelma Moreira,
José Carlos Bacelar Almeida
Abstract:
Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of fundamental results related to context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless…
▽ More
Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of fundamental results related to context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols inaccessible symbols, empty rules and unit rules) and the existence of a Chomsky Normal Form for context-free grammars.
△ Less
Submitted 30 October, 2015;
originally announced October 2015.
-
Formalization of the pum** lemma for context-free languages
Authors:
Marcus V. M. Ramos,
Ruy J. G. B. de Queiroz,
Nelma Moreira,
José Carlos Bacelar Almeida
Abstract:
Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pum** Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pum** Lemma for context-free languages.
Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pum** Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pum** Lemma for context-free languages.
△ Less
Submitted 15 October, 2015;
originally announced October 2015.
-
On Computational Paths and the Fundamental Groupoid of a Type
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina de Oliveira
Abstract:
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computational paths can be seen as the grounds on which the propositional equality between two computational objects stand. Using computational paths and categorical semantics, we take any type $A$ of type theory and construct a…
▽ More
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computational paths can be seen as the grounds on which the propositional equality between two computational objects stand. Using computational paths and categorical semantics, we take any type $A$ of type theory and construct a groupoid for this type. We call this groupoid the fundamental groupoid of a type $A$, since it is similar to the one obtained using the homotopical interpretation of the identity type. The main difference is that instead of being just a semantical interpretation, computational paths are entities of the syntax of type theory. We also expand our results, using computational paths to construct fundamental groupoids of higher levels.
△ Less
Submitted 21 September, 2015;
originally announced September 2015.
-
Formalization of simplification for context-free grammars
Authors:
Marcus V. M. Ramos,
Ruy J. G. B. de Queiroz
Abstract:
Context-free grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of the fact that general context-free grammars generate languages that can be also generated by simpler and equivalent context-free grammars. Namely, useless symbol elimination, inacc…
▽ More
Context-free grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of the fact that general context-free grammars generate languages that can be also generated by simpler and equivalent context-free grammars. Namely, useless symbol elimination, inaccessible symbol elimination, unit rules elimination and empty rules elimination operations were described and proven correct with respect to the preservation of the language generated by the original grammar.
△ Less
Submitted 15 October, 2015; v1 submitted 7 September, 2015;
originally announced September 2015.
-
Formalization of closure properties for context-free grammars
Authors:
Marcus V. M. Ramos,
Ruy J. G. B. de Queiroz
Abstract:
Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and the Coq proof assistant. The results obtained so far include the representation of context-free grammars, the description of algorithms for some operations on…
▽ More
Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and the Coq proof assistant. The results obtained so far include the representation of context-free grammars, the description of algorithms for some operations on them (union, concatenation and closure) and the proof of related theorems (e.g. the correctness of these algorithms). A brief survey of related works is presented, as well as plans for further development.
△ Less
Submitted 10 June, 2015;
originally announced June 2015.
-
On the Groupoid Model of Computational Paths
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences or rewrites', computational paths are taken to be terms of the identity type of Martin Löf's Intensional Type Theory, since these paths can be seen as the grounds on which the propositional equality between two computational objects stand. Fro…
▽ More
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences or rewrites', computational paths are taken to be terms of the identity type of Martin Löf's Intensional Type Theory, since these paths can be seen as the grounds on which the propositional equality between two computational objects stand. From this perspective, this work aims to show that one of the properties of the identity type is present on computational paths. We are referring to the fact that that the identity type induces a groupoid structure, as proposed by Hofmann \& Streicher (1994). Using categorical semantics, we show that computational paths induce a groupoid structure. We also show that computational paths are capable of inducing higher categorical structures.
△ Less
Submitted 8 September, 2016; v1 submitted 8 June, 2015;
originally announced June 2015.
-
Context-Free Language Theory Formalization
Authors:
Marcus Vinícius Midena Ramos,
Ruy J. G. B. de Queiroz
Abstract:
Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different tools are being increasingly used in order to accelerate and simplify proof checking. Context-free language theory is a well-established area of mathematics, relevant to computer science foundatio…
▽ More
Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different tools are being increasingly used in order to accelerate and simplify proof checking. Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This proposal aims at formalizing parts of context-free language theory in the Coq proof assistant. This report presents the underlying theory and general characteristics of proof assistants, including Coq itself, discusses its use in relevant formalization projects, presents the current status of the implementation, addresses related projects and the contributions of this work. The results obtained so far include the formalization of closure properties for context-free grammars (under union, concatenation and closure) and the formalization of grammar simplification. Grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory, and the formalization refers to the fact that general context-free grammars generate languages that can be also generated by simpler and equivalent context-free grammars. Namely, useless symbol elimination, inaccessible symbol elimination, unit rules elimination and empty rules elimination operations were described and proven correct with respect to the preservation of the language generated by the original grammar.
△ Less
Submitted 30 April, 2015;
originally announced May 2015.
-
On the Identity Type as the Type of Computational Paths
Authors:
Arthur F. Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
We introduce a new way of formalizing the intensional identity type based on the fact that a entity known as computational paths can be interpreted as terms of the identity type. Our approach enjoys the fact that our elimination rule is easy to understand and use. We make this point clear constructing terms of some relevant types using our proposed elimination rule. We also show that the identity…
▽ More
We introduce a new way of formalizing the intensional identity type based on the fact that a entity known as computational paths can be interpreted as terms of the identity type. Our approach enjoys the fact that our elimination rule is easy to understand and use. We make this point clear constructing terms of some relevant types using our proposed elimination rule. We also show that the identity type, as defined by our approach, induces a groupoid structure. This result is on par with the fact that the traditional identity type induces a groupoid, as exposed by Hofmann \& Streicher (1994).
△ Less
Submitted 18 April, 2015;
originally announced April 2015.
-
Sequences of Rewrites: A Categorical Interpretation
Authors:
Arthur Ramos,
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
In Martin-Löf's Intensional Type Theory, identity type is a heavily used and studied concept. The reason for that is the fact that it's responsible for the recently discovered connection between Type Theory and Homotopy Theory. The main problem with identity types, as originally formulated, is that they are complex to understand and use. Using that fact as motivation, a much simpler formulation fo…
▽ More
In Martin-Löf's Intensional Type Theory, identity type is a heavily used and studied concept. The reason for that is the fact that it's responsible for the recently discovered connection between Type Theory and Homotopy Theory. The main problem with identity types, as originally formulated, is that they are complex to understand and use. Using that fact as motivation, a much simpler formulation for the identity type was proposed by Queiroz & Gabbay (1994) and further developed by de Queiroz & de Oliveira (2013). In this formulation, an element of an identity type is seen as a sequence of rewrites (or computational paths). Together with the logical rules of this new entity, there exists a system of reduction rules between sequence of rewrites called LND_{EQS}-RWS. This system is constructed using the labelled natural deduction (i.e. Prawitz' Natural Deduction plus derivations-as-terms) and is responsible for establishing how a sequence of rewrites can be rewritten, resulting in a new sequence of rewrites. In this context, we propose a categorical interpretation for this new entity, using the types as objects and the rules of rewrites as morphisms. Moreover, we show that our interpretation is in accordance with some known results, like that types have a groupoidal structure. We also interpret more complicated structures, like the one formed by a rewrite of a sequence of rewrites.
△ Less
Submitted 15 February, 2015; v1 submitted 5 December, 2014;
originally announced December 2014.
-
Propositional equality, identity types, and direct computational paths
Authors:
Ruy J. G. B. de Queiroz,
Anjolina G. de Oliveira
Abstract:
In proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactical details (such as, e.g., change of bound variables). When setting up a proof theory for equality one is faced with a rather unexpected situation where there may not be a unique canonical proof of an equality statement.…
▽ More
In proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactical details (such as, e.g., change of bound variables). When setting up a proof theory for equality one is faced with a rather unexpected situation where there may not be a unique canonical proof of an equality statement. Indeed, in a (1994--5) proposal for the formalisation of proofs of propositional equality in the Curry--Howard style, we have already uncovered such a peculiarity. Totally independently, and in a different setting, Hofmann & Streicher (1994) have shown how to build a model of Martin-Löf's Type Theory in which uniqueness of canonical proofs of identity types does not hold. The intention here is to show that, by considering as sequences of rewrites and substitution, it comes a rather natural fact that two (or more) distinct proofs may be yet canonical and are none to be preferred over one another. By looking at proofs of equality as rewriting (or computational) paths this approach will be in line with the recently proposed connections between type theory and homotopy theory via identity types, since elements of identity types will be, concretely, paths (or homotopies).
△ Less
Submitted 5 August, 2013; v1 submitted 10 July, 2011;
originally announced July 2011.
