Unificación y Correspondencia de Orden Superior.
Author: Carlos C. Martínez
May 2002
Abstract::
The goal of this article is to summarize basic issues concerning with Higher Order Unification (H.O.U.) and its related decision problem in the context of Simply Typed Lambda-Calculus. Firstly, we motivate unification in its more general sense, by considering the following definition below. After introducing unification, we present the Simply Typed Lambda-Calculus and mention a few remarks on its expressive power, and finally refer to some classical results on H.O.U problems, such as undecidability of third order unification.
Definition:: (Unification)
Given a formal system S, its unification problem is stated as: Given two terms U, V in S, is there a sigma substitution such that sigma (U) = sigma (V).
Background::
Automating higher order logic was first addressed in the early ‘60 by J.A. Robinson, the complexity of the problem appeared when higher order unification was shown to be undecidable in 1972 independently by G. Huet and C. Lucchesi. An important case of unification is pattern matching or simple as matching, where Huet’s semi decision algorithm turn out to be decidable generating.
© 2012 Carlos C. Martínez | Generated by webgen