Uma formalização da composicionalidade do cálculo lambda-ex em Coq
AUTOR(ES)
Flávio José Ferro Barros
DATA DE PUBLICAÇÃO
2010
RESUMO
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.
ASSUNTO(S)
confluência ciencia da computacao cálculos de substituições explícitas cálculo lambda-ex composicionalidade
Documentos Relacionados
- Verificação de propriedades do cálculo גex em Coq
- Uma formalização da mão invisível
- Uma formalização da teoria de reescrita em linguagem de ordem superior
- Uma formalização matematica do comportamento das membranas excitaveis
- Formalização da comunicação de conhecimentos probabilísticos em sistemas multiagentes : uma abordagem baseada em lógica probabilística