Authors
Ulrich Kühler, Claus-Peter Wirth
Title
Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving
Bibtex Entry
In
Long Version:
SEKI-Report SR-1996-11
Full paper: Format: ps.gz.
Short version:
8th RTA 1997, LNCS 1232, pp. 38--52, Springer.
Full paper: Format: ps.gz.
Copyright Owner
Long Version:
SEKI
Short version:
Springer
Abstract
We propose a specification language for the formalization of data types with partial or non-terminating operations as part of a rewrite-based logical framework for inductive theorem proving. The language requires constructors for designating data items and admits positive/negative conditional equations as axioms in specifications. The (total algebra) semantics for such specifications is based on so-called data models. We present admissibility conditions that guarantee the unique existence of a distinguished data model with properties similar to those of the initial model of a usual equational specification. Since admissibility of a specification requires confluence of the induced rewrite relation, we provide an effectively testable confluence criterion which does not presuppose termination.
Keywords
Algebraic specification, partial operations, conditional rewriting, confluence, inductive theorem proving