Welcome to Higher Order Prolog with Extensional Semantics

Hopes is a prototype interpreter for a higher-order PROLOG-like language. The syntax of the language extends that of PROLOG by supporting higher-order constructs (such as higher-order predicate variables, partial application and lambda terms). In particular, the syntax allows clauses (and queries) that contain uninstantiated predicate variables. The interpreter implements a higher-order top-down SLD-resolution proof procedure described in this paper. In the case of uninstantiated predicate variables, the proof procedure will systematically (and in a sophisticated way) investigate all finite instantiations of these variables.

In other words, Hopes has all the advantages of a higher-order system but continues to keep the flavor of classical Prolog programming.

Getting Started with the Interpreter

To checkout the source from the darcs repository you should execute

darcs get http://code.haskell.org/hopes hopes

To compile the source you must install the cabal package and execute

make

Features

  • Can write first-order programs like ordinary Prolog.
  • Higher-Order Variables: Can be passed as arguments and called like ordinary predicates.
  • Partial Applications: Predicates can be applied only to some of their arguments.
  • Lambda Abstractions: Support of anonymous predicate definition using lambda abstractions.
  • Existential Higher-Order Variables: Can query a variable relation and generate an appropriate extensional binding.

Examples

In order to gain some intuition behind logic programming in HOPES some simple examples are given.

The ordered predicate is the simple second-order predicate that holds if the relation R is an ordering of the list.

ordered(R, []).
ordered(R, [X]).
ordered(R, [X, Y| Z]):- R(X,Y), ordered(R, [Y|Z]).

The popular map predicate:

map(R, [], []).
map(R, [X|Xs], [Y|Ys]) :- R(X, Y), map(R, Xs, Ys).

Other Higher Order Logic Systems