Version 6 (modified by acharal, 5 years ago) |
---|

# 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

- Teygus is an implementation of lambdaProlog.
- XSB includes an implementation of HiLog.