This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/20259
Description
Title
Semantic unification for convergent systems
Author(s)
Mitra, Subrata
Issue Date
1994
Doctoral Committee Chair(s)
Dershowitz, Nachum
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Language
eng
Abstract
Equation solving is the process of finding a substitution of terms for variables that makes two terms equal in a given theory, while semantic unification is the process that generates a basis set of such unifying substitutions. A simpler variant of the problem is semantic matching, where the substitution is made in only one of the terms. Semantic unification and matching constitute an important component of theorem proving and programming language interpreters.
In this thesis we formulate a unification procedure based on a system of transformation rules that looks at goals in a lazy, top-down fashion, and prove its soundness and completeness for equational theories described by convergent rewrite systems (finite sets of equations that compute unique output values when applied from left-to-right to input values).
We consider different variants of the system of transformation rules. We describe syntactic restrictions on the equations under which simpler sets of transformation rules are sufficient for generating a complete set of semantic matchings. We show that our first-order unification procedure, with slight modifications, can be used to solve the satisfiability problem in combinatory logic together with a convergent set of algebraic axioms, resulting in a complete higher-order unification procedure for the given algebra. We also provide transformation rules to handle situations where some of the function symbols additionally satisfy the equivalences of associativity and commutativity.
"Termination of a system of directed equations is essential for proving existence and uniqueness of normal forms. Furthermore, termination is essential for simplification in theorem provers. We provide a simple restriction on the well-known ""recursive path ordering"" which can be used for proving termination of extended rewriting, modulo the axioms of associativity and commutativity."
Finally, we formulate various syntactic and semantic conditions on the given equations and the goal which result in decidability of semantic matching. We also investigate decidable cases of semantic unification.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
