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

# Welcome to Higher Order Prolog with Extensional Semantics

HOPES is a prototype interpreter written in Haskell for the definitorial higher order PROLOG. The interpreter implements a higher order proof procedure with extensional semantics.

For more information about the formal definition of the language and its semantics you should consult this paper.

## 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.