Solving Higher-Order Equations

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.

Contenu

1 Introduction.- 2 Preview.- 2.1 Term Rewriting.- 2.2 Narrowing.- 2.3 Narrowing and Logic Programming.- 2.4 ?-Calculus and Higher-Order Logic.- 2.5 Higher-Order Term Rewriting.- 2.6 Higher-Order Unification.- 2.7 Decidability of Higher-Order Unification.- 2.8 Narrowing: The Higher-Order Case.- 2.8.1 Functional-Logic Programming.- 2.8.2 Conditional Narrowing.- 3 Preliminaries.- 3.1 Abstract Reductions and Termination Orderings.- 3.2 Higher-Order Types and Terms.- 3.3 Positions in ?-Terms.- 3.4 Substitutions.- 3.5 Unification Theory.- 3.6 Higher-Order Patterns.- 4 Higher-Order Equational Reasoning.- 4.1 Higher-Order Unification by Transformation.- 4.2 Unification of Higher-Order Patterns.- 4.3 Higher-Order Term Rewriting.- 4.3.1 Equational Logic.- 4.3.2 Confluence.- 4.3.3 Termination.- 5 Decidability of Higher-Order Unification.- 5.1 Elimination Problems.- 5.2 Unification of Second-Order with Linear Terms.- 5.2.1 Unifying Linear Patterns with Second-Order Terms.- 5.2.2 Extensions.- 5.3 Relaxing the Linearity Restrictions.- 5.3.1 Extending Patterns by Linear Second-Order Terms.- 5.3.2 Repeated Second-Order Variables.- 5.4 Applications and Open Problems.- 5.4.1 Open Problems.- 6 Higher-Order Lazy Narrowing.- 6.1 Lazy Narrowing.- 6.2 Lazy Narrowing with Terminating Rules.- 6.2.1 Avoiding Lazy Narrowing at Variables.- 6.2.2 Lazy Narrowing with Simplification.- 6.2.3 Deterministic Eager Variable Elimination.- 6.2.4 Avoiding Reducible Substitutions by Constraints.- 6.3 Lazy Narrowing with Left-Linear Rules.- 6.3.1 An Invariant for Goal Systems: Simple Systems.- 6.3.2 A Strategy for Call-by-Need Narrowing.- 6.3.3 An Implementational Model.- 6.4 Narrowing with Normal Conditional Rules.- 6.4.1 Conditional Rewriting.- 6.4.2 Conditional Lazy Narrowing with Terminating Rules.- 6.4.3 Conditional Lazy Narrowing with Left-Linear Rules.- 6.5 Scope and Completeness of Narrowing.- 6.5.1 Oriented versus Unoriented Goals.- 7 Variations of Higher-Order Narrowing.- 7.1 A General Notion of Higher-Order Narrowing.- 7.2 Narrowing on Patterns with Pattern Rules.- 7.3 Narrowing Beyond Patterns.- 7.4 Narrowing on Patterns with Constraints.- 8 Applications of Higher-Order Narrowing.- 8.1 Functional-Logic Programming.- 8.1.1 Hardware Synthesis.- 8.1.2 Symbolic Computation: Differentiation.- 8.1.3 A Functional-Logic Parser.- 8.1.4 A Simple Encryption Problem.- 8.1.5 "Infinite" Data-Structures and Eager Evaluation.- 8.1.6 Functional Difference Lists.- 8.1.7 The Alternating Bit Protocol.- 8.2 Equational Reasoning by Narrowing.- 8.2.1 Program Transformation.- 8.2.2 Higher-Order Abstract Syntax: Type Inference.- 9 Concluding Remarks.- 9.1 Related Work.- 9.1.1 First-Order Narrowing.- 9.1.2 Other Work on Higher-Order Narrowing.- 9.1.3 Functional-Logic Programming.- 9.1.4 Functional Programming.- 9.1.5 Higher-Order Logic Programming.- 9.2 Further Work.- 9.2.1 Implementation Issues.- 9.2.2 Other Extensions.