The Regular Expression Descriptions of Unifier Set in the Typed λ-Calculus

Article type: Research Article

Authors: Zaionc, Marec^{; *}

Affiliations: Department of Computer and Information Sciences, University of Alabama at Birmingham, University Station, Birmingham, Alabama 35294, U.S.A.

Note: [*] Research described in this paper was partially done while author was at Jagiellonian University, Krakow (Poland).

Abstract: λ-language over simple type structure is considered. We investigate unification problem such that number of elementary substitutions in a potentially infinite matching tree introduced by Huet is finite (compare [8]). The substitutions are generated using term grammar technique. Such a grammar consists of productions which are on the form; nonterminal variable of certain type produces a term of the same type. The most interesting is the case when matching tree is infinite and includes an infinite number of most general unifiers. We will show an interesting property of the infinite unification trees from examined class: for every infinite branch there is a node which occurs earlier in this tree. It means that there are some fragments which are repeated in this tree. Therefore the set of most general unifiers which are represented by terminal nodes can be described by regular expression over finite alphabet. Regular expression are constructed as a solution of linear language equalities. For every problem from this class the set of unifiers is described by some language. This language can be approximated by regular languages.

Keywords: typed λ-calculus, unification, infinite trees, regular expressions, matching trees

DOI: 10.3233/FI-1987-10304

Journal: Fundamenta Informaticae, vol. 10, no. 3, pp. 309-322, 1987