Skip navigation
Use este identificador para citar ou linkar para este item: http://repositorio.unb.br/handle/10482/7685
Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
2010_WashingtnLuisRibeirodeCarvalhoSegundo.pdf516,71 kBAdobe PDFVisualizar/Abrir
Título: Verificação de propriedades do cálculo גex em Coq
Autor(es): Carvalho Segundo, Washington Luís Ribeiro de
Orientador(es): Moura, Flávio Leonardo Cavalcanti de
Assunto: Verificação formal
Cálculos de substituições explícitas
Cálculo ג
Cálculo ex
Data de publicação: 11-Mai-2011
Referência: CARVALHO SEGUNDO, Washington Luís Ribeiro de. Verificação de propriedades do cálculo גex em Coq. 2010. 71 f. Dissertação(Mestrado em Informática)-Universidade de Brasília, Brasília, 2010.
Resumo: 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
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.
Unidade Acadêmica: Instituto de Ciências Exatas (IE)
Departamento de Ciência da Computação (IE CIC)
Informações adicionais: Dissertação (mestrado) - Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010.
Programa de pós-graduação: Programa de Pós-Graduação em Informática
Aparece nas coleções:Teses, dissertações e produtos pós-doutorado

Mostrar registro completo do item Visualizar estatísticas



Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.