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)
In this work we study higher-order unification via explicit substitutions calculi.In particular, we compare Huet?s algorithm for the simply typed ¸-calculus withthe method developed by Dowek, Hardin and Kirchner for the ¸¾-calculus andwe conclude that there exists a structural correspondence between the derivationsin these two methods for a given unification problem. In order to formalize thiscomparison, we adapt Huet?s algorithm for de Bruijn?s notation since this is thenotation used by the explicit substitutions calculi considered here. In addition, weintroduce the notions of unification trees and pseudo-precooking.In addition, we show that unification in both ¸¾- and ¸se-calculus may generateidentical derivation trees in the sense that, both unification methods can alwaysapply ?corresponding? rules for a given unification problem. This comparison isdone by introducing the functions T and L that convert terms from the ¸se-calculusto the ¸¾-calculus and vice-versa, respectively, and proving that a unification rulecan be applied in the ¸¾-calculus for a problem P, if and only if, we can apply the?corresponding? rule of the ¸se-calculus to the translation of P.We use the ideas developed for unification to build an specific application for aparticular case of unification called matching. We present an algorithm that decidesa special class of second order problems in the ¸¾-calculus.The comparative study presented here is important for a better understandingof the unification methods used in computational systems based on the ¸-calculus,as well as the role of explicit substitutions in the higher-order unification and shedsome light on implementational questions. Moreover, the new notion of pseudoprecookingcan be useful for optimizing implementations of the unification methodsdeveloped for explicit substitutions calculi since it combines the usual notion ofprecooking with applications of the unification rules.
This document abstract is also available in Portuguese.
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 matematica aplicada matemática


Date of Publication:03/23/2006

© 2009 All Rights Reserved.