Ph.D.
Solving Higher-Order Equations\: From Logic to Programming
Author(s): Christian Prehofer
Year: 1995
Publisher: Technical Report TUM-I9508
Editor:
CR Classification:
CR General Terms:
Keywords:
Abstract:We present methods for higher-order equational reasoning which aim for the integration of higher-order functional and logic programming. The underlying computation rule for this integration, called narrowing, is lifted to the higher-order case. We develop several notions of higher-order narrowing and give first completeness results. Higher-order narrowing employs higher-order unification instead of first-order unification as in logic programming. Although undecidable in general, we show that second-order unification as required for functional-logic programming is decidable. We further introduce several refinements for narrowing which utilize properties of functional programs\: left-linearity and convergence, which entails uniqueness of normal forms. These refinements can be combined to a narrowing strategy which generalizes call-by-need as in functional programming. This forms a new basis for higher-order functional-logic programming with functional programs, possibly with conditions.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@phdthesis{ TUM-I9508,
author = {Christian Prehofer},
title = {Solving Higher-Order Equations\: From Logic to Programming},
type = {PHDrep},
school = {Technische Univerit\"at M\"unchen},
year = {1995},
url = {http://www4.informatik.tu-muenchen.de/reports/TUM-I9508.html},
abstract = {We present methods for higher-order equational reasoning which aim for the integration of higher-order functional and logic programming. The underlying computation rule for this integration, called narrowing, is lifted to the higher-order case. We develop several notions of higher-order narrowing and give first completeness results. Higher-order narrowing employs higher-order unification instead of first-order unification as in logic programming. Although undecidable in general, we show that second-order unification as required for functional-logic programming is decidable. We further introduce several refinements for narrowing which utilize properties of functional programs\: left-linearity and convergence, which entails uniqueness of normal forms. These refinements can be combined to a narrowing strategy which generalizes call-by-need as in functional programming. This forms a new basis for higher-order functional-logic programming with functional programs, possibly with conditions. },
CRClassification = {},
CRGenTerms = {}
}
]]>