Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas,
Departamento de Ciência da Computação, 2012. / Submitted by Alaíde Gonçalves dos Santos (alaide@unb.br) on 2013-04-26T15:53:16Z
No. of bitstreams: 1
2012_FabioHenriquedaSilva.pdf: 552243 bytes, checksum: e64f674891aeafd428d4d66fd0fe9706 (MD5) / Approved for entry into archive by Guimaraes Jacqueline(jacqueline.guimaraes@bce.unb.br) on 2013-07-29T13:03:08Z (GMT) No. of bitstreams: 1
2012_FabioHenriquedaSilva.pdf: 552243 bytes, checksum: e64f674891aeafd428d4d66fd0fe9706 (MD5) / Made available in DSpace on 2013-07-29T13:03:08Z (GMT). No. of bitstreams: 1
2012_FabioHenriquedaSilva.pdf: 552243 bytes, checksum: e64f674891aeafd428d4d66fd0fe9706 (MD5) / Os cálculos de Substituições Explícitas (CSEs) são variações do cálculo λ que especificam de maneira concreta a operação de substituição, definida de maneira implícita no cálculo λ. Estes cálculos estendem a linguagem do cálculo λ de maneira a atomizar os passos envolvidos numa aplicação concreta da operação de substituição. Este trabalho abordará a propriedade de expansibilidade em alguns CSEs que podemos dizer que seja uma investigação do passado de um termo. Esta propriedade é interessante quando este passado nos revela um termo puro, ou seja, um termo pertencente à linguagem do cálculo λ Para isso fez-se necessário estudar várias outras propriedades, como a simulação da regra β do cálculo λ, a correção da regra (B) no λ? -cálculo e, a propriedade de Projeção do λ?-cálculo e do λσ-cálculo. O objetivo é estudar o problema de expansão no lambda sigma-cálculo, e para isso observamos os resultados de Ariel Arbiser no lambda upsilon-cálculo, em que o Teorema de Scott foi uma ferramenta crucial. _______________________________________________________________________________________ ABSTRACT / Calculi of Explicit Substitutions (CSEs) are variants of the λ calculus which specify concretely the substitution operation, defined implicitly in the λ calculus. These calculi extend the language of λ calculus in order to atomize the steps involved in the practical application of replacement operation. This work will discuss the expansion property in some CSEs, that it is an investigation of the past of a term. This property is interesting when it discloses a past term pure, i.e. a term belonging to the language of λ calculus. For this it was necessary to study several other properties, such as the simulation of rule β of λ calculus, the correction of the rule (B) in λ?-calculus and the property projection of λ?-calculus and the λσ-calculus. The goal is to study the expansion problem in the λσ-calculus and verify the aplication of the results of Ariel Arbiser in the λ?-calculi, in which the Scott Theorem was a crucial tool.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.unb.br:10482/13737 |
| Date | 29 November 2012 |
| Creators | Silva, Fábio Henrique da |
| Contributors | Ventura, Daniel Lima, Ayala-Rincón, Mauricio |
| 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 UnB, instname:Universidade de Brasília, instacron:UNB |
| Rights | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data., info:eu-repo/semantics/openAccess |
Page generated in 0.0021 seconds