Uma formalização da composicionalidade do cálculo lambda-ex em Coq
Saved in:
| Main Author: | |
|---|---|
| Publication Date: | 2010 |
| Format: | Master thesis |
| Language: | por |
| Source: | Repositório Institucional da UnB |
| Download full: | http://repositorio.unb.br/handle/10482/6601 |
Summary: | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010. |
| _version_ | 1871442441529196544 |
|---|---|
| author | Barros, Flávio José Ferro |
| author_browse | Barros, Flávio José Ferro |
| author_facet | Barros, Flávio José Ferro |
| author_role | author |
| bitstream.checksum.fl_str_mv | 20b7e7f5115fdc9ff34396a6f5e6cc1f 87508fa6fda7dea75aacf50535bf4797 cf70cb41a336b352509ebba5d2c470ae |
| bitstream.checksumAlgorithm.fl_str_mv | MD5 MD5 MD5 |
| bitstream.url.fl_str_mv | http://repositorio2.unb.br/jspui/bitstream/10482/6601/1/2010_FlavioJoseFerroBarros.pdf http://repositorio2.unb.br/jspui/bitstream/10482/6601/2/license.txt http://repositorio2.unb.br/jspui/bitstream/10482/6601/3/2010_FlavioJoseFerroBarros.pdf.txt |
| collection | Repositório Institucional da UnB |
| contributor_str_mv | Moura, Flávio Leonardo Cavalcanti de |
| dc.contributor.advisor1.fl_str_mv | Moura, Flávio Leonardo Cavalcanti de |
| dc.contributor.author.fl_str_mv | Barros, Flávio José Ferro |
| dc.date.accessioned.fl_str_mv | 2011-01-26T00:28:37Z |
| dc.date.available.fl_str_mv | 2011-01-26T00:28:37Z |
| dc.date.issued.fl_str_mv | 2011-01-26 |
| dc.date.submitted.none.fl_str_mv | 2010-07-19 |
| dc.identifier.citation.fl_str_mv | BARROS, Flávio José Ferro. Uma formalização da composicionalidade do cálculo lambda-ex em Coq. 2010. vii, 61 f. Dissertação (Mestrado em Informática)-Universidade de Brasília, Brasília, 2010. |
| dc.identifier.uri.fl_str_mv | http://repositorio.unb.br/handle/10482/6601 |
| dc.language.iso.fl_str_mv | por |
| dc.rights.driver.fl_str_mv | info:eu-repo/semantics/openAccess |
| dc.source.none.fl_str_mv | reponame:Repositório Institucional da UnB instname:Universidade de Brasília (UnB) instacron:UNB |
| dc.subject.keyword.en.fl_str_mv | Linguagem de programação (Computadores) |
| dc.title.en.fl_str_mv | Uma formalização da composicionalidade do cálculo lambda-ex em Coq |
| dc.type.driver.fl_str_mv | info:eu-repo/semantics/masterThesis |
| dc.type.status.fl_str_mv | info:eu-repo/semantics/publishedVersion |
| description | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010. |
| eu_rights_str_mv | openAccess |
| format | masterThesis |
| id | UNB_a727219cf2be46e22d4e151ddf22bfb9 |
| identifier_str_mv | BARROS, Flávio José Ferro. Uma formalização da composicionalidade do cálculo lambda-ex em Coq. 2010. vii, 61 f. Dissertação (Mestrado em Informática)-Universidade de Brasília, Brasília, 2010. |
| instacron_str | UNB |
| institution | UNB |
| instname_str | Universidade de Brasília (UnB) |
| language | por |
| network_acronym_str | UNB |
| network_name_str | Repositório Institucional da UnB |
| oai_identifier_str | oai:repositorio.unb.br:10482/6601 |
| publishDate | 2010 |
| publishDateSort | 2010 |
| reponame_str | Repositório Institucional da UnB |
| repository.mail.fl_str_mv | repositorio@unb.br |
| repository.name.fl_str_mv | Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| repository_id_str | |
| spelling | Barros, Flávio José FerroMoura, Flávio Leonardo Cavalcanti de2011-01-26T00:28:37Z2011-01-26T00:28:37Z2011-01-262010-07-19BARROS, Flávio José Ferro. Uma formalização da composicionalidade do cálculo lambda-ex em Coq. 2010. vii, 61 f. Dissertação (Mestrado em Informática)-Universidade de Brasília, Brasília, 2010.http://repositorio.unb.br/handle/10482/6601Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010.Apresenta-se uma formalização das propriedades de composicionalidade do Cálculo lambda-ex em Coq. A abordagem utilizada baseia-se na lógica nominal de acordo com o trabalho desenvolvido por [3]. Mais especificamente estendemos a formalização do lambda-cálculo contida neste trabalho de forma a incluir a operação de substituição explícita do cálculo lambda-ex. Nessa abordagem, a alpha-equivalência coincide com a igualdade pré-construída de Coq, e os princípios de recursão e indução sobre classes de lambda-termos possuem tratamento específico. Escolhemos trabalhar com o cálculo lambda-ex por ser atualmente o único cálculo que satisfaz simultaneamente todas as propriedades desejáveis para um cálculo de substituições explícitas. Ele é uma extensão do lambda-x com uma regra de reescrita para composição de substituições dependentes e uma equação para comutação de substituições independentes. O cálculo lambda-ex usa um construtor unário para a substituição explicita, mas tem o mesmo poder de expressividade de cálculos com substituições simultâneas. _________________________________________________________________________________ ABSTRACTWe present a formalization of properties of compositionality of the ex-calculus in Coq. The approach is based in the nominal logic as presented in the paper [3]. More precisely, we extended a formalization of the -calculus in such a way that it now includes the explicit substitution operation of the ex-calculus. In this approach, -equivalence of -terms coincides with the Coqt’s built-in equality, and the principles of recursion and induction over classes of -terms are treated in a specific way. We chose to work with the ex-calculus because it is currently the only calculus that simultaneously satisfies all the desirable properties for a calculus of explicit substitutions. It is an extension of the x-calculus with a rewrite rule for composition of dependent substitutions and one equation for independent substitutions. The ex-calculus has a unary constructor for the explicit substitution operation, but have the same expressive power of calculi with simultaneous substitutions.Uma formalização da composicionalidade do cálculo lambda-ex em Coqinfo:eu-repo/semantics/publishedVersioninfo:eu-repo/semantics/masterThesisLinguagem de programação (Computadores)info:eu-repo/semantics/openAccessporreponame:Repositório Institucional da UnBinstname:Universidade de Brasília (UnB)instacron:UNBORIGINAL2010_FlavioJoseFerroBarros.pdf2010_FlavioJoseFerroBarros.pdfapplication/pdf454810http://repositorio2.unb.br/jspui/bitstream/10482/6601/1/2010_FlavioJoseFerroBarros.pdf20b7e7f5115fdc9ff34396a6f5e6cc1fMD51open accessLICENSElicense.txtlicense.txttext/plain1863http://repositorio2.unb.br/jspui/bitstream/10482/6601/2/license.txt87508fa6fda7dea75aacf50535bf4797MD52open accessTEXT2010_FlavioJoseFerroBarros.pdf.txt2010_FlavioJoseFerroBarros.pdf.txtExtracted texttext/plain105002http://repositorio2.unb.br/jspui/bitstream/10482/6601/3/2010_FlavioJoseFerroBarros.pdf.txtcf70cb41a336b352509ebba5d2c470aeMD53open access10482/66012023-07-14 15:56:24.244open accessoai:repositorio.unb.br:10482/6601TGljZW5zZSBncmFudGVkIGJ5IEFsbGFuIFdhbmljayBNb3R0YSAoYWxsYW5fd2FuaWNrQGhvdG1haWwuY29tKSBvbiAyMDExLTAxLTIxVDE4OjE0OjQ0WiAoR01UKToKCsOJIG5lY2Vzc8OhcmlvIGNvbmNvcmRhciBjb20gYSBsaWNlbsOnYSBkZSBkaXN0cmlidWnDp8OjbyBuw6NvLWV4Y2x1c2l2YSwKYW50ZXMgcXVlIG8gZG9jdW1lbnRvIHBvc3NhIGFwYXJlY2VyIG5vIFJlcG9zaXTDs3Jpby4gUG9yIGZhdm9yLCBsZWlhIGEKbGljZW7Dp2EgYXRlbnRhbWVudGUuIENhc28gbmVjZXNzaXRlIGRlIGFsZ3VtIGVzY2xhcmVjaW1lbnRvIGVudHJlIGVtCmNvbnRhdG8gYXRyYXbDqXMgZGU6IHJlcG9zaXRvcmlvQGJjZS51bmIuYnIgb3UgMzMwNy0yNDExLgoKTElDRU7Dh0EgREUgRElTVFJJQlVJw4fDg08gTsODTy1FWENMVVNJVkEKCkFvIGFzc2luYXIgZSBlbnRyZWdhciBlc3RhIGxpY2Vuw6dhLCBvL2EgU3IuL1NyYS4gKGF1dG9yIG91IGRldGVudG9yIGRvcwpkaXJlaXRvcyBkZSBhdXRvcik6CgphKSBDb25jZWRlIMOgIFVuaXZlcnNpZGFkZSBkZSBCcmFzw61saWEgbyBkaXJlaXRvIG7Do28tZXhjbHVzaXZvIGRlCnJlcHJvZHV6aXIsIGNvbnZlcnRlciAoY29tbyBkZWZpbmlkbyBhYmFpeG8pLCBjb211bmljYXIgZS9vdQpkaXN0cmlidWlyIG8gZG9jdW1lbnRvIGVudHJlZ3VlIChpbmNsdWluZG8gbyByZXN1bW8vYWJzdHJhY3QpIGVtCmZvcm1hdG8gZGlnaXRhbCBvdSBpbXByZXNzbyBlIGVtIHF1YWxxdWVyIG1laW8uCgpiKSBEZWNsYXJhIHF1ZSBvIGRvY3VtZW50byBlbnRyZWd1ZSDDqSBzZXUgdHJhYmFsaG8gb3JpZ2luYWwsIGUgcXVlCmRldMOpbSBvIGRpcmVpdG8gZGUgY29uY2VkZXIgb3MgZGlyZWl0b3MgY29udGlkb3MgbmVzdGEgbGljZW7Dp2EuIERlY2xhcmEKdGFtYsOpbSBxdWUgYSBlbnRyZWdhIGRvIGRvY3VtZW50byBuw6NvIGluZnJpbmdlLCB0YW50byBxdWFudG8gbGhlIMOpCnBvc3PDrXZlbCBzYWJlciwgb3MgZGlyZWl0b3MgZGUgcXVhbHF1ZXIgb3V0cmEgcGVzc29hIG91IGVudGlkYWRlLgoKYykgU2UgbyBkb2N1bWVudG8gZW50cmVndWUgY29udMOpbSBtYXRlcmlhbCBkbyBxdWFsIG7Do28gZGV0w6ltIG9zCmRpcmVpdG9zIGRlIGF1dG9yLCBkZWNsYXJhIHF1ZSBvYnRldmUgYXV0b3JpemHDp8OjbyBkbyBkZXRlbnRvciBkb3MKZGlyZWl0b3MgZGUgYXV0b3IgcGFyYSBjb25jZWRlciDDoCBVbml2ZXJzaWRhZGUgZGUgQnJhc8OtbGlhIG9zIGRpcmVpdG9zCnJlcXVlcmlkb3MgcG9yIGVzdGEgbGljZW7Dp2EsIGUgcXVlIGVzc2UgbWF0ZXJpYWwgY3Vqb3MgZGlyZWl0b3Mgc8OjbyBkZQp0ZXJjZWlyb3MgZXN0w6EgY2xhcmFtZW50ZSBpZGVudGlmaWNhZG8gZSByZWNvbmhlY2lkbyBubyB0ZXh0byBvdQpjb250ZcO6ZG8gZG8gZG9jdW1lbnRvIGVudHJlZ3VlLgoKU2UgbyBkb2N1bWVudG8gZW50cmVndWUgw6kgYmFzZWFkbyBlbSB0cmFiYWxobyBmaW5hbmNpYWRvIG91IGFwb2lhZG8KcG9yIG91dHJhIGluc3RpdHVpw6fDo28gcXVlIG7Do28gYSBVbml2ZXJzaWRhZGUgZGUgQnJhc8OtbGlhLCBkZWNsYXJhIHF1ZQpjdW1wcml1IHF1YWlzcXVlciBvYnJpZ2HDp8O1ZXMgZXhpZ2lkYXMgcGVsbyByZXNwZWN0aXZvIGNvbnRyYXRvIG91CmFjb3Jkby4KCkEgVW5pdmVyc2lkYWRlIGRlIEJyYXPDrWxpYSBpZGVudGlmaWNhcsOhIGNsYXJhbWVudGUgbyhzKSBzZXUgKHMpIG5vbWUgKHMpCmNvbW8gbyAocykgYXV0b3IgKGVzKSBvdSBkZXRlbnRvciAoZXMpIGRvcyBkaXJlaXRvcyBkbyBkb2N1bWVudG8KZW50cmVndWUsIGUgbsOjbyBmYXLDoSBxdWFscXVlciBhbHRlcmHDp8OjbywgcGFyYSBhbMOpbSBkYXMgcGVybWl0aWRhcyBwb3IKZXN0YSBsaWNlbsOnYS4KRepositório InstitucionalPUBhttps://repositorio.unb.br/oai/requestrepositorio@unb.bropendoar:2023-07-14T18:56:24Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| spellingShingle | Uma formalização da composicionalidade do cálculo lambda-ex em Coq Barros, Flávio José Ferro Linguagem de programação (Computadores) |
| status_str | publishedVersion |
| title | Uma formalização da composicionalidade do cálculo lambda-ex em Coq |
| title_full | Uma formalização da composicionalidade do cálculo lambda-ex em Coq |
| title_fullStr | Uma formalização da composicionalidade do cálculo lambda-ex em Coq |
| title_full_unstemmed | Uma formalização da composicionalidade do cálculo lambda-ex em Coq |
| title_short | Uma formalização da composicionalidade do cálculo lambda-ex em Coq |
| title_sort | Uma formalização da composicionalidade do cálculo lambda-ex em Coq |
| topic | Linguagem de programação (Computadores) |
| url | http://repositorio.unb.br/handle/10482/6601 |