Orientador : Cid Carvalho de Souza / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-07-28T19:54:03Z (GMT). No. of bitstreams: 1 Rodrigues_MaikolMagalhaes_M.pdf: 4069676 bytes, checksum: b0b8e4bc9cdbe5bfc3fb90f34a46b43e (MD5) Previous issue date: 2001 / Resumo: Este trabalho de mestrado procurou estudar e resolver o problema de planejamento de viagens de linhas de ônibus da região metropolitana de São Paulo. Para tanto foi proposta uma ferramenta computacional capaz de gerar automaticamente as programações de viagens para uma linha de ônibus urbano. A programação de viagens tem um grande impacto não só na qualidade do serviço prestado aos passageiros da linha mas também no custo operacional das empresas de transporte. Portanto, o problema aqui estudado é de grande relevância prática e social. Os dados de entrada incluem uma curva com a demanda horária de passageiros da linha e um conjunto de restrições operacionais relativas à frota e aos funcionários. Na saída, deve-se produzir uma tabela com os horários das viagens além da escala de serviço completa dos carros e dos funcionários que irão operar na linha. Os algoritmos propostos por essa dissertação concentram-se no desenvolvimento de heurísticas baseadas em modelos de Programação Linear Inteira para resolver o problema de programação de viagens. Estes algoritmos foram implementados como parte de uma ferramenta computacional e os resultados são comparados com as soluções adotadas atualmente pelas empresas de transportes urbano. A análise dos resultados computacionais mostra que é possível obter reduções substanciais nos custos da operação sem que com isso haja uma redução na qualidade de serviço / Abstract: This dissertation aimed at studying and solving a real world trip planning problem. The problem considered arises from the daily operation of an urban transit bus company that serves the metropolitan area of the city of São Paulo, in Brazil. In this work we present a software that automatically generates a planning for the trips of a urban bus line. The trip planning has an enormous impact not only on the quality of the service offered to the passengers but also on the operational cost of the transportation companies. Therefore, the problem tackled here is of great importance for practical and social reasons. The input data includes the hourly demand of passengers and a set of operational constraints related to the vehicles and the employees. In the output, the trip time table as well as the vehicle and the crew schedules are produced. All the proposed algorithms in this work focus on the design of heuristics based on Integer Linear Programming models for the problem. The algorithms are implemented as part of a software whose results are compared with the solutions adopted in the bus companies nowadays. The analysis of our experiments indicates that it was possible to achieve a substantial cost reduction without loss in the quality of service / Mestrado / Mestre em Ciência da Computação

Atualmente os sistemas computacionais mais sofisticados são aqueles que apresentam imagens gráficas. Devido às características de alta velocidade de processamento e excelente resultado na geração de imagens o uso da Computação Gráfica se dá em diversas áreas como a indústria, pesquisa, publicidade, entretenimento, medicina, treinamento, dentre outras. Este trabalho aborda dois assuntos clássicos na Computação Gráfica, Geometria Sólida Construtiva (CSG) e Sombras Projetadas. Ambos são muito importantes para esta linha de pesquisa da Ciência da Computação. A Geometria Sólida Construtiva é utilizada na modelagem de objetos e as sombras projetadas são necessárias para aumentar o realismo das imagens. Geometria sólida construtiva (CSG) é uma técnica para a modelagem de sólidos, que define sólidos complexos pela composição de sólidos simples (primitivas). Isso inclui também a composição de objetos já combinados, até que se chegue a um objeto mais complexo. Um fator muito importante e necessário na obtenção de imagens realistas e que deve ser considerado é a utilização de sombras, pois estas são eficazes no realismo e impressão espacial de objetos tridimensionais. As sombras estabelecem diversos níveis de profundidade na imagem, fazem uma pontuação geométrica na cena de modo a evitar que os objetos não pareçam estar flutuando no ar. Este trabalho consiste em apresentar uma proposta para a geração de sombras em objetos modelados pela Geometria Sólida Construtiva. Para tanto foram estudados os assuntos referentes à modelagem de objetos por CSG, algoritmos para a geração de sombras “bem delimitadas” e formas de gerar sombras na Geometria Sólida Construtiva. O processo de geração de sombras em cenas modeladas por CSG, através da aplicação das mesmas operações booleanas envolvidas na modelagem dos objetos, sobre as sombras nem sempre apresenta resultados corretos. Diante disso, foram investigadas outras formas de solucionar o problema. Dentre estas, uma alternativa é a realização de transformações na árvore binária CSG, através de outras operações, envolvendo o uso de complemento com operações de união e interseção, para a modelagem do objeto e geração da sombra correspondente. Com base nos estudos realizados foram implementados dois protótipos que exibem a sombra projetada de objetos modelados por CSG. Na implementação do protótipo A utilizaram-se as técnicas tradicionais de modelagem de sólidos e sombra projetada. Os resultados obtidos com este protótipo serviram de referência. No protótipo B os resultados foram obtidos através da aplicação da zona ativa das primitivas na modelagem dos objetos e a sombra é projetada durante o processo de avaliação de contornos do sólido. Os resultados obtidos com este protótipo são comparados com os resultados do protótipo A e são apresentados como forma de exibir a aplicação do método proposto.

Orientador: Ricardo Dahab / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto da Computação / Made available in DSpace on 2018-08-02T03:39:47Z (GMT). No. of bitstreams: 1 Miranda_RogerioAlbertoni_M.pdf: 2899328 bytes, checksum: d0afff8b4bc78bf95a3670fb021de8ec (MD5) Previous issue date: 2002 / Resumo: Sistemas de chave pública tem sua segurança depositada sobre um problema matemático unanimemente considerado difícil pela comunidade científica. De modo geral, a dificuldade do problema cresce exponencialmente no número de bits das chaves utilizada por tal sistema. Sistemas criptográficos baseados em curvas elípticas, propostos em 1985 a partir de idéias matemáticas conhecidas desde o século XIX, são sistemas que permitem que níveis desejáveis de segurança sejam obtidos com valores muito pequenos de chave, quando comparados com outros sistemas de chave pública como RSA e ElGamal. Por isso, eles têm despertado um progressivo interesse, especialmente para aplicações com sérias restrições de recurso, tal como é o caso de smart cards, handhelds, telefones celulares, aplicações web, etc. Nesta dissertação, apresentamos e discutimos cada um dos elementos que compõem um sistema criptográfico baseado em curvas elípticas, dando ênfase na descrição detalhada dos critérios de seleção de um conjunto de algoritmos eficientes para as operações aritméticas envolvidas, a partir de diversas contribuições na literatura relacionada. Também descrevemos cada um dos passos de nossa implementação de um ECC completo e analisamos os resultados finais obtidos a partir desta implementação / Mestrado / Mestre em Ciência da Computação

Orientador : Maria Beatriz Felgar de Toledo / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-03T07:47:45Z (GMT). No. of bitstreams: 1 Almeida_HudoRodriguesde_M.pdf: 4932798 bytes, checksum: 8ec72a7d06fd010d7b6a55baf11da594 (MD5) Previous issue date: 2002 / Resumo: Esta dissertação propõe uma arquitetura para um sistema de gerenciamento de workflows que atenda aos requisitos de aplicações para o desenvolvimento de projetos. São considerados modos mais flexíveis para troca de informações entre usuários que trabalham no mesmo projeto, no contexto de uma transação de grupo. Em sistemas de workflow tradicionais, a troca de informações é realizada através de parâmetros entre tarefas. O modelo proposto permite a troca de resultados intermediários entre usuários de uma transação de grupo. Além disso, o sistema garante a execução confiável de processos mesmo quando falhas ocorrem. Finalmente, um protótipo foi implementado sobre uma plataforma distribuída baseada em CORBA / Abstract: This dissertation proposes an architecture for a workflow management system that meets the requirements of project development applications. More flexible modes for information exchange between users that work on the same project are considered, in the context of a group transaction. In traditional workflow systems, the information exchange is achieved by parameter passing between tasks. The proposed model allows the exchange of intermediary results between users within a group transaction. Moreover, the system guarantees the reliable execution of processes even when failures occur. Finally, a prototype has been implemented on a CORBA-based distributed platform / Mestrado / Mestre em Ciência da Computação

Orientador: Elnatan Chagas Ferreira / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-07-25T08:50:41Z (GMT). No. of bitstreams: 1 Sousa_AntonioHeronaldode_D.pdf: 9476626 bytes, checksum: 6fc4c287239d7216bd6d55c7a1e61b23 (MD5) Previous issue date: 1999 / Resumo: Este trabalho apresenta um estudo sobre a viabilidade de se utilizar novas metodologias de engenharia de software em ambientes microcontrolados. É abordado o uso da programação orientada a objetos, juntamente com a programação visual, na construção de linguagens mais acessíveis e mais produtivas para a programação de microcontroladores. Como resultado, foi proposto um protótipo de uma linguagem, chamada 0++. Esta linguagem se caracteriza por utilizar, em conjunto, estruturas gráficas e estruturas textuais para melhor representar dados e algoritmos. Além disso, ela foi projetada para combinar as características de reusabilidade da programação orientada a objetos e a acessibilidade da programação visual. Ela permite o desenvolvimento de aplicações usando estruturas visuais orientadas a objetos, a fim de melhorar a qualidade e acessibilidade de informações trocadas no desenvolvimento de software para sistemas microcontrolados...Observação: O resumo, na íntegra, poderá ser visualizado no texto completo da tese digital / Abstract: This thesis presents a feasibility investigation about use of new engineering software methodologies in microcontroller systems. The approach is to use object oriented programming paradigm with visual programming to build a more productive microcontroller programming language. It was developed a microcontroller programming language, called 0++. The main feature of this language is to use, at the same time, graphical structures and text to represent data and procedures. Also, it was designed to combine the reusability of object-oriented programming and the accessibility of visual programming. It allows the development of applications using visual object-oriented structures in order to improve quality and accessibility of information exchange in microcontroller systems software design...Note: The complete abstract is available with the full electronic digital thesis or dissertations / Doutorado / Doutor em Engenharia Elétrica

Submitted by Marco Antônio de Ramos Chagas (mchagas@ufv.br) on 2017-02-02T12:40:52Z No. of bitstreams: 1 texto completo.pdf: 4553880 bytes, checksum: df41256758e1eed020511478d544566b (MD5) / Made available in DSpace on 2017-02-02T12:40:52Z (GMT). No. of bitstreams: 1 texto completo.pdf: 4553880 bytes, checksum: df41256758e1eed020511478d544566b (MD5) Previous issue date: 2016-11-23 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Neste trabalho avaliou-se a ocorrência de erros de arredondamento decorrentes do uso de aritmética de ponto-flutuante em algoritmos de simplificação geométrica 2D e 3D. Erros de arredondamento podem fazer com que algoritmos produzam resultados topologicamente inconsistentes, isto ́e, resultados que violam alguma característica crucial do modelo original. Foram mostradas situações em que inconsistências ocorrem, mesmo em algoritmos projetados para evitá-las. Visando contornar este problema, dois métodos foram propostos: EPLSimp, para simplificação de linhas, e UGSimp para simplificação de malhas triangulares. Em ambos os métodos, testes preemptivos para verificação de inconsistência topológica foram realizados utilizando-se núumeros racionais de precisão múltipla, em vez de números de ponto-flutuante. O uso de números racionais não gera erros de arredondamento, entretanto o uso de precisão múltipla implica em um aumento no tempo de execução dos algoritmos. Para compensar esta redução de desempenho, os algoritmos foram implementados com o paradigma de computação paralela. Como resultado, temos dois métodos de simplificação isentos de erros de arredondamento por ponto- flutuante. Testes mostraram um ganho considerável no tempo de execução com as implementações paralelas. / In this work, we evaluated the occurrence of round-off errors on floating-point arith- metic for the problem of 2D and 3D geometric simplification. Round-off errors may lead algorithms to produce topologically inconsistent results, that is, results that fail to preserve crucial features of the original model. Some algorithms are designed to avoid such inconsistencies, however, they are usually implemented with floating- point arithmetic. Even these algorithms may fail to output topologically consistent results due to round-off errors. In order to overcome this issue, two methods were proposed: EPLSimp for polyline simplification, and UGSimp, for triangular mesh simplification. On both methods, preemptive tests are carried out to detect and pre- vent topological inconsistencies. Such tests use multiple precision rational numbers instead of floating-point numbers. The use of rational numbers does not present round-off errors. Nevertheless, it causes an increase on the execution time of the algorithms. To compensate for this performance loss, both algorithms were imple- mented using a parallel computing paradigm. As result, the methods presented do not output topologically inconsistent models. Tests have shown a considerable performance gain with parallel implementations of the proposed approaches.

Orientador: Fernando Antonio Campos Gomide / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-20T16:32:11Z (GMT). No. of bitstreams: 1 Oliveira_MarcoAntonioAssfalkde_M.pdf: 6234787 bytes, checksum: 1efbc34436bca796b24e8197ce2e35cb (MD5) Previous issue date: 1995 / Resumo: A navegação autônoma de veículos é um exemplo bem conhecido e típico de problemas de controle autônomo. Este tipo de controle envolve um ambiente muito complexo e desestruturado. A grande quantidade de parâmetros descarta o uso de um modelo matemático do ambiente. Por isso, o controle autônomo exige métodos de controle que se adaptam constantemente ao ambiente e que utilizam informações locais. O uso de tais métodos incorre em duas considerações: localidade (situ.atedness) e o problema da referência (frame-of-reference). A primeira questão está relacionada com a complexidade do ambiente de operação, a qual não permite a previsão do comportamento global do ambiente. Assim, o agente autônomo deverá ser capaz de agir baseado em informações parciais, provenientes de sua situação local. O segundo problema está ligado ao conhecimento utilizado no projeto do agente (conhecimento a priori). Este conhecimento pré-inserido limita a adaptabilidade do agente ao impor tanto o ponto de vista do projetista (o qual é baseado em sensores e modos de processamento bem diferentes dos do agente) quanto o conhecimento limitado sobre o ambiente deste projetista. Ambos os problemas são resolvidos pelo uso de um método de controle adaptativo e localizado. As propostas mais promissoras provém da área de computação flexível. Computação flexível engloba um conjunto de métodos, desde teoria dos sistemas nebulosos a sistemas evolucionários. Os paradigmas principais são as redes neurais, sistemas nebulosos e um conjunto de métodos conhecido como raciocínio probabilístico. Este último inclui sistemas evolucionários, teoria da complexidade e teoria do caos, entre outros. O poder da computação flexível vem da simbiose de seus múltiplos métodos. Estes sistemas híbridos oferecem as vantagens dos seus componentes e compensam mutuamente as falhas destes componentes. As características mais interessantes incluem auto-organização, processamento de informações imprecisas e capacidade de aprendizagem. Neste trabalho propomos um método de controle autônomo que combina uma rede neural, teoria de sistemas nebulosos e um algoritmo genético. A sinergia destes três paradigmas de computação oferece uma estrutura computacional paralela e robusta com fácil inserção/extração de conhecimento e capaz de aprendizagem não-supervisionada. O método proposto foi aplicado ao problema de navegação autônoma de veículos em um ambiente simulado. Os resultados demonstram que as limitações observadas podem ser atribuídas à quantidade e tipo de conhecimento utilizado na escolha dos parâmetros (Sensores e representação de conhecimento). O método de navegação em si provou ser robusto e confiável, desenvolvendo comportamentos com desempenho comparável aos de um agente projetado heuristicamente. O desenvolvimento futuro deste trabalho será focalizado na investigação de métodos auto-organizados para reconhecimento dos dados ambientais relevantes e nos problemas de otimização do conhecimento a priori e da sensibilidade do método de aprendizagem às especificações dos sensores. Estas pesquisas têm por objetivo libertar o agente de limitações impostas pelo projetista e aumentar a adaptabilidade do agente / Abstract: Autonomous vehicle navigation is a well-known and typical example of an autonomous control problem. This type of control problem involves a very complex, unstructured environment. The great amount of parameters preclude the use of a mathematical model of the environment. Thus, autonomous control demands constantly adapting, locally situated control methods, giving rise to two fundamental design issues: situatedness and frame-of-knowledge. The first deals with the impossibility of predicting the global behaviour of the environment. Instead the autonomous agent must be able to act upon local and limited data. The latter problem refers to the knowledge used in the design of an agent (a priori knowledge). Such pre-installed experience limits the agent's adaptability by imposing the designer's point of view (based on sensors and processing modes far different from those of the agent) and limited knowledge of the environment. Both issues are addressed by implementing an adaptive locally-aware control method. Qne of the most promising approaches comes from the 80ft computing field. Soft computing involves a spectrum of methods, ranging from fuzzy system theory to evolutionary systems. The main bulwarks are neural networks, fuzzy systems and a number of methods known as probabilistic reasoning. The latter includes evolutionary systems, cellular automata, complexity theory and chaos theory, among others. The power and promise of soft computing emerge from the symbiosis of its many paradigms. These hybrid synergetic systems offer the strengths of their components while cross-compensating the components' drawbacks. The most interesting features include auto-organization, imprecise data handling and unsupervised learning capabilities. In this work we propose an autonomous control method that combines a neural- network, fuzzy system theory and a genetical algorithm. The synergy of these three soft computing paradigms offers a parallel robust computing structure with easily extractable/insertable knowledge and capable of unsupervised learning. The proposed method was applied to the autonomous vehicle navigation problem in a simulated environment. The results show that most of the limitations are due to the amount and type of knowledge used in the choice of the vehicle parameters (sensors and knowledge representation). The navigation method itself proved to be robust and reliabJe, deveJoping behaviours comparable to those of a hand-crafted agent. Future work will focus on the issues of the optimum a priori knowledge levels, the sensivity of the learning method to sensor specifications, and on the development of self-organizing methods for relevant environment data recognition. These efforts are geared towards freeing the agent from human-imposed limiting factors while enhancing its adaptability / Mestrado / Mestre em Engenharia Elétrica

Orientadores: Shusaburo Motoyama, Claudio Kirner / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-17T11:53:47Z (GMT). No. of bitstreams: 1 Silva_JorgeLuize_D.pdf: 9332250 bytes, checksum: 7333ab47e718273c0c4a589b6727c50a (MD5) Previous issue date: 1992 / Resumo: Este trabalho teve como objetivo analisar e desenvolver Programação a Fluxo de Dados Tolerante a Falhas em um computador paralelo estruturado recursivamente (CPER). O CPER é uma máquina paralela que possui uma estrutura básica constituída de N Elementos de Processamento (EP), interligados através de um barramento paralelo de alta velocidade, correspondendo ao barramento nível 1. Várias destas estruturas básicas interligadas através de um outro barramento constitui a estrutura do barramento nível 2. O uso recursivo desta mesma regra irá compor a estrutura hierárquica do CPER, que permite expansão, flexibilidade e alto grau de Tolerância a Falhas. Entretanto esta arquitetura pode não ser eficiente, se não utilizarmos conceitos de programação paralela. Propusemos então a Programação a Fluxo de Dados na estrutura hierárquica do CPER. Inicialmente apresentamos o hardware do CPER, e suas estruturas de alto desempenho. Em seguida, mostramos como o CPER opera para executar programas a fluxo de dados de forma dinâmica e mostramos também uma solução de software para garantir Tolerância a Falhas na programação a fluxo de Dados. Finalmente apresentamos um simulador (FDsim), e uma análise estocástica, que tiveram como objetivo mostrar viabilidade e eficiência da máquina paralela proposta / Abstract: In this work is analyzed the fault tolerant data flow processing in a computer based on hierarchical parallel buses. In this architecture, a set of N processors, each one called processing element (PE), are interconnected to a bus constituting a basic structure or cluster. The set of the buses of these basic structures correspond to the parallel buses leveI 1. Several basic structures of level 1 are interconnected to a bus constituting a cluster for the parallel buses leveI 2. The same idea can be recursively used to get parallel buses leveI M. This computer architecture based on hierarchical parallel buses permits the expansion flexibility and is highly fault tolerant computer. However, this architecture may not be efficient. If it is not utilized parallel programming concept. In this work we proposed the data flow processing for the execution of the programs in hierarchical parallel buses machine. First of alI, it is proposed hardware solution to get high throughput for inter-clusters and inter-Ievels communications in hierarchical parallel buses machine. FOllowing, it is discussed how the parallel buses computer can work as a dynamic data flow machine and it is proposed software solution to get fault tolerant processing. Finally, a software simulation is carried out to show the feasibility and efficiency of proposed parallel buses machine / Doutorado / Doutor em Engenharia Elétrica

Orientador: Marcio Luiz de Andrade Netto / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-18T14:25:22Z (GMT). No. of bitstreams: 1 Rosa_JoaoLuisGarcia_M.pdf: 10533866 bytes, checksum: eff7483f9919f4d2a0a8d1da0a8ad44d (MD5) Previous issue date: 1993 / Resumo: Esta dissertação de mestrado é sobre Processamento de Linguagem Natural (PLN). O PLN consiste de uma série de tarefas que a máquina deve executar para analisar um texto. Na literatura existem vários trabalhos em diversas abordagens. Este trabalho faz uma combinação de abordagens baseadas em lógica e de abordagens conexionistas. O trabalho proposto tem três partes. A primeira parte faz a análise sintática de frases da língua portuguesa. É baseada em lógica. A segunda parte faz a análise semântica, ou a verificação do significado das palavras numa frase. Isto é feito através de redes neurais artificiais, que "aprendem" a representação binária das palavras (suas microcaracterísticas semânticas). Esta abordagem é chamada de conexionismo. Sua grande vantagem é a habilidade de generalização, ou seja, a rede é capaz de reconhecer uma palavra, mesmo que esta não tenha sido mostrada a ela. A terceira, e última, parte deste trabalho trata da utilização de redes recorrentes para análise de frases. Este tipo de rede serve para "ligar" as palavras em uma frase, pois a rede recorrente tem memória. Ela é capaz de "lembrar" da última palavra vista numa seqüência. É útil para ligar as palavras em uma sentença, por exemplo, o sujeito com o objeto, o objeto com o complemento, etc. Isto torna a frase uma entidade única a ser analisada / Abstract: This dissertation is about Natural Language Processing (NLP). NLP consists of a series of tasks the machine should carry out in analysing a texto In literature, there are papers having different approaches. This work combines two approaches: based on logic and connectionism. The proposed work is divided in three parts. The first makes the parsing, or the syntactic analysis of sentences in the Portuguese language, based on logic. The second part takes care of the semantic analysis, or the verification of the meaning of words in a sentence. This is achieved through artificial neural networks that "Iearn" the binary representation of the words (their semantic microfeatures). This approach is called connectionism. Its major advantage is the ability of generalizing, i. e., it is able to recognize a word even it is not presented to the nets. The third, and last, part of this work is about the use of recurrent networks in text analysis. This kind of network is to "Iink" the words in a sentence because the recurrent net is given memory, which makes it able to "remember" the last word seen in a sequence. This is useful to link the words in a sentence like the subject to the object, the object to the complement, etc. This makes a sentence an entire item to be analysed. / Mestrado / Mestre em Engenharia Elétrica

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.