Files in this item



application/pdf8924945.pdf (3MB)Restricted to U of Illinois
(no description provided)PDF


Title:Proofs and computations in conditional equational theories
Author(s):Sivakumar, G.
Doctoral Committee Chair(s):Dershowitz, Nachum
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Science
Abstract:Conditional equations arise naturally in the algebraic specification of data types. They also provide an elegant computational paradigm that cleanly combines logic and functional programming. In this thesis, we study how to do proofs and computations in conditional equational theories, using rewriting techniques.
We examine different formulations of conditional equations as rewrite systems and compare their expressive power. We identify a class of "decreasing" systems for which most of the basic notions (like rewriting and computing normal forms) are decidable. We then study how to determine if a conditional rewrite system is "confluent." We settle negatively the question whether "joinability of critical pairs" is, in general, sufficient for confluence of terminating conditional systems. We also prove two positive results for systems having critical pairs and arbitrarily big terms in conditions.
We discuss "completion" methods to generate convergent conditional rewrite systems equivalent to a given set of conditional equations. Finally, we study equation solving methods and formulate a goal-directed approach that improves prior methods and detects more unsatisfiable equations.
Issue Date:1989
Rights Information:Copyright 1989 Sivakumar, G.
Date Available in IDEALS:2011-05-07
Identifier in Online Catalog:AAI8924945
OCLC Identifier:(UMI)AAI8924945

This item appears in the following Collection(s)

Item Statistics