Source author record

Anjolina G. de Oliveira

Anjolina G. de Oliveira appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science math.CT

Catalog footprint

What is connected

4works

2topics

3close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2016arXiv

On the Groupoid Model of Computational Paths

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.

preprint2015arXiv

On the Identity Type as the Type of Computational Paths

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).

preprint2015arXiv

Sequences of Rewrites: A Categorical Interpretation

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.

preprint2013arXiv

Propositional equality, identity types, and direct computational paths

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).