Back to Search
Start Over
Tipo identidade como o tipo de caminhos computacionais
- 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.
- Subjects :
- Teoria da computação
Teoria dos tipos
Subjects
Details
- Language :
- Portuguese
- Database :
- OpenAIRE
- Journal :
- Repositório Institucional da UFPE, Universidade Federal de Pernambuco (UFPE), instacron:UFPE
- Accession number :
- edsair.od......3056..c9ed79e87ababc1af9c6580c2090a5da