Program Transformation with Abstract Relation Algebras.

摘要

Our objective is to satisfy two seemingly opposing constraints on program design. We want to begin a program as an obvious formal specification but also insist upon efficient execution. Our approach is to find expressive, model independent program constructs with algebraic properties that can show logical equivalence between a clear specification and an efficient program. Our solution is an implementation of some of the relations, relation operators, and equations that comprise Tarski's Q-relation algebra. The key to this solution is a single operator for linear recursions that satisfies two equations. The first merges recursions and the second propagates constraints for early pruning of the nonproductive branches of the computation tree. Keywords: Logic programming; Functional programming; Organizational reasoning. (KR)