Logo - springer
Slogan - springer

Birkhäuser - Birkhäuser Computer Science | Solving Higher-Order Equations - From Logic to Programming

Solving Higher-Order Equations

From Logic to Programming

Prehofer, Christian

1998, IX, 188 p.

A product of Birkhäuser Basel
Available Formats:

Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.

You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.

After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.


(net) price for USA

ISBN 978-1-4612-1778-7

digitally watermarked, no DRM

Included Format: PDF

download immediately after purchase

learn more about Springer eBooks

add to marked items


Hardcover version

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-0-8176-4032-3

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days

add to marked items


Softcover (also known as softback) version.

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-1-4612-7278-6

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days

add to marked items

  • About this book

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.

Content Level » Research

Keywords » Hardware - Program Analysis - Theorem Proving - Variable - calculus - computer - computer science - declarative programming - functional programming - logic - program transformation - programming - verification

Related subjects » Birkhäuser Computer Science - Birkhäuser Mathematics

Table of contents 

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.

Popular Content within this publication 



Read this Book on Springerlink

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Mathematical Applications in Computer Science.

Additional information