Details

Um estudo comparativo sobre unificaçao de ordem superior em cálculos de substituições explícitas

by Cavalcanti de, Flávio Leonardo

Abstract (Summary)
Neste trabalho estudamos unificação e matching de ordem superior em cálculos de substituições explícitas. Em particular comparamos o algoritmo de Huet para o ?-cálculo simplesmente tipado com o método desenvolvido por Dowek, Hardin e Kirchner para o ?s-cálculo e concluímos que existe uma correspondência estrutural entre as derivações realizadas por estes métodos para um dado problema. Para formalizar esta comparação, adaptamos o algoritmo de Huet para a notação à la de Bruijn, já que esta é a notação utilizada pelos cálculos de substituições explícitas aqui tratados e, introduzimos as noções de árvore de unificação e pseudo-cozimento. Adicionalmente, mostramos que unificação no ?s-cálculo e no ?se-cálculo podem gerar árvores de derivação iguais no sentido que, os dois métodos de unificação sempre podem utilizar regras de unificação "correspondentes" para um dado problema. Esta comparação é feita utilizando-se duas funções T e L que traduzem termos dos ?se-cálculo para o ?s-cálculo e vice-versa, respectivamente, mostrando que uma dada regra de unificação pode ser utilizada no ?s-cálculo para um problema P se, e somente se a regra "correspondente" pode ser utilizada no ?se-cálculo para a tradução de P. Em seguida, utilizamos as idéias desenvolvidas em unificação para construir uma aplicação específica de um caso restrito de unificação conhecido como matching. Apresentamos um algoritmo que decide uma classe especial de problemas de segunda ordem no ?s-cálculo. O estudo comparativo aqui apresentado é importante para uma melhor compreensão dos métodos de unificação utilizados em sistemas computacionais baseados no ?-cálculo, e do papel dos cálculos de substituições explícitas em unificação de ordem superior. Além disto, a noção de pseudo-cozimento aqui introduzida pode ser útil na implementação de versões mais eficientes dos métodos de unificação desenvolvidos para cálculos de substituições explícitas já que esta combina a noção de pré-cozimento usual com as regras de unificação.
This document abstract is also available in English.
Bibliographical Information:

Advisor:Mauricio Ayala Rincon

School:Universidade de Brasília

School Location:Brazil

Source Type:Master's Thesis

Keywords: substituições explícitas unificação de ordem superior

ISBN:

Date of Publication:03/23/2006

© 2009 OpenThesis.org. All Rights Reserved.