Skip to main content
main-content

Über dieses Buch

This monograph develops techniques for equational reasoning in higher-order logic. Due to its expressiveness, higher-order logic is used for specification and verification of hardware, software, and mathematics. In these applica­ tions, higher-order logic provides the necessary level of abstraction for con­ cise and natural formulations. The main assets of higher-order logic are quan­ tification over functions or predicates and its abstraction mechanism. These allow one to represent quantification in formulas and other variable-binding constructs. In this book, we focus on equational logic as a fundamental and natural concept in computer science and mathematics. We present calculi for equa­ tional reasoning modulo higher-order equations presented as rewrite rules. This is followed by a systematic development from general equational rea­ soning towards effective calculi for declarative programming in higher-order logic and A-calculus. This aims at integrating and generalizing declarative programming models such as functional and logic programming. In these two prominent declarative computation models we can view a program as a logical theory and a computation as a deduction.

Inhaltsverzeichnis

Frontmatter

Chapter 1. Introduction

Abstract
This monograph develops techniques for equational reasoning in higher-order logic. Due to its expressiveness, higher-order logic is used for specification and verification of hardware, software, and mathematics. In these applications, higher-order logic provides the necessary level of abstraction for concise and natural formulations. The main assets of higher-order logic are quantification over functions or predicates and its abstraction mechanism. These allow one to represent quantification in formulas and other variable-binding constructs.
Christian Prehofer

Chapter 2. Preview

Abstract
In this chapter, we informally introduce the main concepts and outline the contributions of this work. Precise definitions are presented in later chapters. We proceed from first-order term rewriting and narrowing to higher-order unification and higher-order narrowing.
Christian Prehofer

Chapter 3. Preliminaries

Abstract
Basic definitions and results for higher-order equational reasoning are introduced in this chapter. The first sections contain general background material on reductions and orderings, followed by a brief introduction to λ-calculus. For a comprehensive treatment we refer to [HS86, Bar84].
Christian Prehofer

Chapter 4. Higher-Order Equational Reasoning

Abstract
This chapter introduces higher-order unification and term rewriting. First, Section 4.1 reviews a set of transformation rules for full higher-order pre-unification. This is followed by an important special case, higher-order patterns, where unification proceeds almost as in the first-order case.
Christian Prehofer

Chapter 5. Decidability of Higher-Order Unification

Abstract
As the known decidability results (see Section 2.6) do not cover many practical cases, we examine decidability of higher-order unification more closely, mostly considering the second-order case. An overview of the results and the corresponding sections can be found in Figure 5.1. Notice that the results only hold under the assumption that all conditions in the path to the node hold.
Christian Prehofer

Chapter 6. Higher-Order Lazy Narrowing

Abstract
This chapter discusses our main approach for solving higher-order equations: lazy narrowing. Lazy narrowing is a goal directed method for solving goals in a top-down or outside-in manner. It can be seen as a direct extension of higher-order unification by some narrowing rules. After starting with a general version of lazy narrowing, we develop refinements of lazy narrowing. Some of them also apply to equational reasoning, while the others are tailored towards functional-logic programming. In the former, we only assume terminating rewrite systems; in the latter we will in addition exploit properties of left-linear rewrite rules. Conditional equations are discussed in Section 6.4. Alternative approaches to narrowing are examined in the following chapter.
Christian Prehofer

Chapter 7. Variations of Higher-Order Narrowing

Abstract
This chapter discusses alternative approaches for solving higher-order equations by narrowing. Most of them are inspired by the different notions of first-order narrowing. Compared to lazy narrowing, for all of them new problems arise due to the higher-order case. For an overview of the approaches, we refer again to Figure 2.2.
Christian Prehofer

Chapter 8. Applications of Higher-Order Narrowing

Abstract
This section presents examples for higher-order rewriting and narrowing. Most of these applications fall into functional-logic programming, for which left-linear rewrite rules and thus Simple Systems suffice. Only the examples in Section 8.2 on program transformation and type inference go beyond programming with left-linear rules and more expressiveness is useful. For other examples on the utility of higher-order constructs, we refer to [Nip91a, MN97] for formalizing logics and λ-calculi, and for process algebras to [Po194]. Other application areas are program synthesis [Hag91b], machine learning [Har90, DW88], natural language processing [Nad87, PM90, GK96, GKL96], and theorem proving systems, for instance see [AINP90, Pau94, Gor88, CAB+86, DFH+93].
Christian Prehofer

Chapter 9. Concluding Remarks

Abstract
This work was motivated by the idea that higher-order equations can be used in practical systems for equational reasoning and functional-logic programming. Towards this goal we have first examined decidable classes of higher-order unification. We have shown that for many practical purposes, higher-order unification is not only a powerful tool, but also terminates for several classes of terms. The main restriction we need is linearity, which is common in programming. It also explains to some degree why higher-order unification in logic programming [NM88] and higher-order theorem proving [Pau94, AINP90] rarely diverges. Secondly, we have developed a framework for solving higher-order equations by narrowing. For lazy narrowing, we were able to develop many important refinements, such as normalization and eager variable elimination for normalized solutions. Of similar practical importance are the extensions to conditional equations. We have also seen that some approaches such as plain narrowing are not suitable for the higher-order case.
Christian Prehofer

Backmatter

Weitere Informationen