Detalhes bibliográficos
| Ano de defesa: |
2015 |
| Autor(a) principal: |
RAMOS, Arthur Freitas |
| Orientador(a): |
QUEIROZ, Ruy José Guerra Barretto de |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Universidade Federal de Pernambuco
|
| Programa de Pós-Graduação: |
Programa de Pos Graduacao em Ciencia da Computacao
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Brasil
|
| Palavras-chave em Português: |
|
| Link de acesso: |
https://repositorio.ufpe.br/handle/123456789/28831
|
Resumo: |
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. |
