DOC PREVIEW
Higher-Order Logic Programming as Constraint Logic Programming

This preview shows page 1-2-3 out of 9 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Higher-Order Logic ProgrammingasConstraint Logic ProgrammingSpiro MichaylovDepartment of Computer and Information ScienceThe Ohio State UniversityColumbus, OH 43210-1277, [email protected] PfenningSchool of Computer ScienceCarnegie Mellon UniversityPittsburgh, PA 15213-3891, [email protected] logic programming (HOLP) languages are particularly useful for various kinds of meta-programming and theorem proving tasks because of the logical support for variable binding via λ-abstraction. They have been used for a wide range of applications including theorem proving, program-ming language interpretation, type inference, compilation, and natural language parsing. Despite theirutility, current language implementations have acquired a well-deserved reputation for being inefficient.In this paper we argue that HOLP languages can reasonably be viewed as Constraint Logic Program-ming (CLP) languages, and show how this can be expected to lead to more practical implementationsby applying the known principles for the design and implementation of practical CLP systems.1 IntroductionHigher-order logic programming (HOLP) languages [17] typically use a typed λ-calculus as their domainof computation. In the case of λProlog [18] it is the simply-typed λ-calculus, while in the case of Elf[22] it is a dependently typed λ-calculus. These languages are particularly useful for various kinds of meta-programming and theorem proving tasks because of the logical support for variable binding via λ-abstraction.They have been used for a wide range of applications including theorem proving [3], programming languageinterpretation [5, 13], type inference [21], compilation [6], and natural language parsing [20]. Despite theirutility, current language implementations have acquired a well-deserved reputation for being inefficient. Inthis paper we argue that HOLP languages can reasonably be viewed as Constraint Logic Programming (CLP)languages [8]. Measurements with an instrumented Elf interpreter confirm that such a view can producepractical benefits, as the known principles for the design and implementation of practical CLP systems [9, 12]are directly applicable to making implementations of HOLP languages more efficient.The core domain of the languages we consider is the set of typed λ-expressions, where abstractionand application are the only interpreted operations and equality is the only relation (interpreted as βηα-convertibility). There are other features of these languages that distinguish them from the CLP languagescheme as defined in [8], for example, higher-order predicates, dependent or polymorphic types, modules,embedded implication and universal quantification. Many of these features have been addressed in a satis-factory way in ongoing implementation projects at Duke and IRISA/INRIA in Rennes. Surveys and furtherreferences to the design of these implementations can be found in [11] and [1]. In this paper we will concen-trate on the issues related to the view of higher-order logic programming as constraint logic programmingwhich, we believe, has the most fundamental impact on expected execution speed.2 Solving Equations Between Typed λ-ExpressionsFull unification in higher-order languages is clearly impractical, due to the non-existence of minimal completesets of most-general unifiers [7]. Therefore, work on λProlog has used Huet’s algorithm for pre-unification [7],where so-called flex-flex pairs (which are always unifiable) are maintained as constraints, rather than beingincorporated in an explicit parametric form. Yet, even pre-unifiability is undecidable, and sets of mostgeneral pre-unifiers may be infinite. While undecidability has not turned out to be a severe problem, thelack of unique most general unifiers makes it difficult to accurately predict the run-time behavior of λPrologprograms that attempt to take advantage of full higher-order pre-unification. It can result in thrashing whencertain combinations of unification problems have to be solved by extensive backtracking. Moreover, in astraightforward implementation, common cases of unification incur a high overhead compared to first-orderunification. These problems have led to a search for natural, decidable subcases of higher-order unificationwhere most general unifiers exist. Miller [15] has suggested a syntactic restriction (Lλ)toλProlog, easilyextensible to related languages [23], where most general unifiers are unique modulo βηα-equivalence.Miller’s restriction has many attractive features. Unification is deterministic and thrashing behavior dueto unification is avoided. Higher-order unification in its full power can be implemented if some additionalcontrol constructs (when) are available [16].However, our empirical analysis [14] suggests that this solution is unsatisfactory, since it has a detrimen-tal effect on programming methodology, and potentially introduces a new efficiency problem. Object-levelvariables are typically represented by meta-level variables, which means that object-level capture-avoidingsubstitution can be implemented via meta-level β-reduction. The syntactic restriction to Lλprohibits thisimplementation technique, and hence a new substitution predicate must be programmed for each objectlanguage. Not only does this make programs harder to read and reason about, but a substitution predicatewill be less efficient than meta-language substitution. This is not to diminish the contribution that Lλhasmade to our understanding of higher-order logic programming. As we will describe below, it forms the basisfor our approach to the implementation of HOLP languages.3 A Practical Approach to Constraint Logic ProgrammingThe generality of the CLP scheme allows languages to be defined that raise two important implementationproblems:• High overhead for frequently-occurring simple constraints.It has been observed [9, 12] that the constraints that occur most frequently in the execution of pro-grams in many CLP systems are relatively simple. However, the generality needed to solve the morecomplicated, but rarely occurring constraints tends to introduce overheads for solving all constraints.Ideally, it should be possible to solve the simple constraints without incurring this overhead.• Some constraints may be too hard to solve or solve efficiently.For many seemingly desirable domains, the required decision algorithms simply do not exist. For others,the decision problem may


Higher-Order Logic Programming as Constraint Logic Programming

Download Higher-Order Logic Programming as Constraint Logic Programming
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Higher-Order Logic Programming as Constraint Logic Programming and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Higher-Order Logic Programming as Constraint Logic Programming 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?