Abstract
By permitting function and predicate symbols to be variables and by replacing first-order terms by simply typed lambda -terms, a higher-order extension to first-order Horn clauses can be described. To be complete in principle, a logic-programming language based on this extension must incorporate higher order unification. Although this is a more complex operation than first-order unification, its availability as a primitive makes certain kinds of programming tasks easier. This aspect is illustrated by presenting some programs in a higher-order version of Prolog called lambda Prolog that manipulate objects, such as formulas and programs, whose representation requires structures containing abstractions or bound variables. It is shown how a simple natural deduction theorem prover may be implemented in lambda Prolog and how some simple program transformers for a functional programming language may be written in this language.
Original language | English (US) |
---|---|
Title of host publication | Unknown Host Publication Title |
Publisher | IEEE |
Pages | 379-388 |
Number of pages | 10 |
ISBN (Print) | 0818607998 |
State | Published - 1987 |