Submitted by Fernanda Rodrigues de Lima (fernanda.rlima@ufpe.br) on 2018-11-09T19:27:14Z
No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
DISSERTAÇÃO Arthur Freitas Ramos.pdf: 743456 bytes, checksum: cb16d9c33d78bebe371f455a60b25b34 (MD5) / Approved for entry into archive by Alice Araujo (alice.caraujo@ufpe.br) on 2019-01-25T17:02:05Z (GMT) No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
DISSERTAÇÃO Arthur Freitas Ramos.pdf: 743456 bytes, checksum: cb16d9c33d78bebe371f455a60b25b34 (MD5) / Made available in DSpace on 2019-01-25T17:02:05Z (GMT). No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
DISSERTAÇÃO Arthur Freitas Ramos.pdf: 743456 bytes, checksum: cb16d9c33d78bebe371f455a60b25b34 (MD5)
Previous issue date: 2015-07-25 / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/28831 |
| Date | 25 July 2015 |
| Creators | RAMOS, Arthur Freitas |
| Contributors | http://lattes.cnpq.br/1825502153580661, QUEIROZ, Ruy José Guerra Barretto de |
| Publisher | Universidade Federal de Pernambuco, Programa de Pos Graduacao em Ciencia da Computacao, UFPE, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.0016 seconds