Back to Search Start Over

Tipo identidade como o tipo de caminhos computacionais

Authors :
RAMOS, Arthur Freitas
QUEIROZ, Ruy José Guerra Barretto de
Source :
Repositório Institucional da UFPE, Universidade Federal de Pernambuco (UFPE), instacron:UFPE
Publication Year :
2015
Publisher :
Universidade Federal de Pernambuco, 2015.

Abstract

CAPES O presente trabalho tem como objetivo o estudo de uma entidade computacional conhecida como caminhos computacionais. Proposta originalmente por QUEIROZ; OLIVEIRA (2011) como ’sequências de reescritas’, a ideia é que os caminhos computacionais funcionam como os termos do tipo identidade da Teoria dos Tipos de Martin-Löf’. Esse trabalho expande essa ideia, mostrando uma formalização completa do tipo identidade a partir dos caminhos computacionais. É mostrado que os caminhos computacionais tornam o tipo identidade uma entidade muito mais intuitiva e simples, quando comparado com a abordagem tradicional. Um outro foco desse trabalho é o estudo das propriedades matemáticas dos caminhos computacionais. Em particular, o interesse é em explorar a relação entre os caminhos e a teoria das categorias. Especificamente, é provado que os caminhos computacionais são capazes de induzir uma estrutura algébrica conhecida como grupóide. Esse resultado está de acordo com os resultados obtidos por HOFMANN; STREICHER (1994), que mostram que a abordagem tradicional do tipo identidade induzem um modelo de grupóide. The current work aims to study a computational entity known as computational paths. Originally proposed by QUEIROZ; OLIVEIRA (2011) as ’sequence of rewrites’, the idea is that computational paths are terms of Martin-Löf’s identity type. This work expands this idea, showing a complete formalization of the identity type using computational paths. It is shown that computational paths makes the identity type a much simpler and more intuitive entity, when compared to the tradional approach. Another focus of this work is the study of the mathematical properties of computational paths. In particular, the main aim is the relation between computational paths and category theory. Specifically, this work shows that computational paths are capable of inducing an algebraic structure known as groupoid. This results is on a par with the one obtained by HOFMANN; STREICHER (1994), which shows that the traditional approach of the identity type also induces a grupoid model.

Details

Language :
Portuguese
Database :
OpenAIRE
Journal :
Repositório Institucional da UFPE, Universidade Federal de Pernambuco (UFPE), instacron:UFPE
Accession number :
edsair.od......3056..c9ed79e87ababc1af9c6580c2090a5da