Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Moura, Flávio Leonardo Cavalcanti de | - |
Autor(es): dc.creator | Carvalho Segundo, Washington Luís Ribeiro de | - |
Data de aceite: dc.date.accessioned | 2024-07-22T12:16:30Z | - |
Data de disponibilização: dc.date.available | 2024-07-22T12:16:30Z | - |
Data de envio: dc.date.issued | 2011-05-11 | - |
Data de envio: dc.date.issued | 2011-05-11 | - |
Data de envio: dc.date.issued | 2011-05-11 | - |
Data de envio: dc.date.issued | 2010-07-13 | - |
Fonte completa do material: dc.identifier | http://repositorio.unb.br/handle/10482/7685 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/capes/800079 | - |
Descrição: dc.description | Dissertação (mestrado) - Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010. | - |
Descrição: dc.description | O cálculo גex representa uma solução importante dentro da classe de cálculos de substituições explícitas que lidam com “nomes”, em oposição aqueles que codificam suas variáveis por índices. Delia Kesner obteve, através de um conjunto de provas construtivas, demonstrações das importantes propriedades do גex. Dentre elas, destacamos a PSN, isso é, a Preservação da Normalização Forte, cuja demonstração faz uso de uma estratégia de redução perpétua, que permitiu uma caracterização indutiva do conjunto SN גex. Estendemos a especificação em Coq, já realizada para o cálculo ג, de B. Aydemir et al, e que utiliza lógica nominal para construção de princípios de indução e recursão _-estrutural. Dessa forma nossa especificação inclui a substituição explícita (s[x=t]) na gramática de termos. Avançamos definindo os sistemas de reescrita e as relações de redução do גex, e concluímos por formalizar alguns resultados para o cálculo, a saber: a FC (Composição Completa), a SIM (Simulação de um passo da β-redução) e ainda outros que caminham para a formalização da PSN. _______________________________________________________________________________ ABSTRACT | - |
Descrição: dc.description | The גex-calculus represents an important solution among all the class of explicit substitutions calculi that deal with "names", as opposed to those that encode variables by indices. Delia Kesner developed the proofs, through a set of constructive ones, of important properties of the _ex calculus. Among them, we highlight the PSN property, that is, the Preservation of Strong Normalization, whose proof uses a perpetual reduction strategy which allowed an inductive characterization of the set SN גex. We extended the specifi cation already done in Coq for the -calculus by B. Aydemir et al, using nominal logic to build principles of ג -structural induction and recursion. In this way our specification includes the explicit substitution (s[x=t]) in the grammar of the terms. We go foward by de_ning the rewriting systems and the reduction relations for the ג ex and we conclude by formalizing some results for this calculus, as follows: The FC (Full Composition), SIM (Simulation of One Step of β -Reduction) and others that go in the direction of the formalization of the PSN. | - |
Formato: dc.format | application/pdf | - |
Direitos: dc.rights | Acesso Aberto | - |
Palavras-chave: dc.subject | Verificação formal | - |
Palavras-chave: dc.subject | Cálculos de substituições explícitas | - |
Palavras-chave: dc.subject | Cálculo ג | - |
Palavras-chave: dc.subject | Cálculo ex | - |
Título: dc.title | Verificação de propriedades do cálculo גex em Coq | - |
Aparece nas coleções: | Repositório Institucional – UNB |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: