= 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 [http://en.wikipedia.org/wiki/Prolog 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 [http://arxiv.org/abs/1106.3457 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 ==

 * [http://teyjus.cs.umn.edu/ Teygus] is an implementation of [http://www.lix.polytechnique.fr/~dale/lProlog/ lambdaProlog].
 * [http://xsb.sourceforge.net/index.html XSB] includes an implementation of [http://www.cs.stonybrook.edu/~kifer/TechReports/hilog.pdf HiLog].