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