Solving higher-order equations : from logic to programming
著者
書誌事項
Solving higher-order equations : from logic to programming
（Progress in theoretical computer science）
Birkhäuser, c1998
大学図書館所蔵 件 / 全13件
-
該当する所蔵館はありません
- すべての絞り込み条件を解除する
注記
Includes bibliographical references and index
内容説明・目次
- 巻冊次
-
ISBN 9780817640323
内容説明
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.
目次
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.
- 巻冊次
-
ISBN 9783764340322
内容説明
This monograph develops techniques for equational reasoning and declarative programming based on higher-order logic. The author presents a framework for the full integration of declarative programming models and shows its application. On the technical side, he integrates the main results of both worlds. The book presents completeness results as common in logic programming and also generalizes evaluation strategies found in current functional programming languages to this setting. The book includes a thorough introduction to higher-order equational logic, higher-order rewriting, and unification. This followed by a stepwise development from general equational reasoning toward effective methods for declarative programming in higher-order logic and lambda-calculus. Another important, complementing, result shows that higher order unification, the basic inference engine in logic programming, is decidable for programming applications. The text is aimed at researchers and advanced students in computer science and mathematics with interests in declarative programming, symbolic computation, term rewriting, equational reasoning, and theorem proving.
It can provide a firm basis for a variety of graduate course in logic and theoretical computer science.
目次
- Higher-order equational reasoning
- decidability of higher-order unification
- higher-order lazy narrowing
- variations of higher-order narrowing
- applications of higher-order narrowing.
「Nielsen BookData」 より