Skip to content

Home

Jump to bottom
Angelos Charalambidis edited this page Oct 28, 2013 · 8 revisions

HOPES

Hopes (Higher-order Prolog with extensional semantics) 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 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).

The closure predicate denotes the transitive closure of a relation R

closure(R, X, Y) :- R(X, Y).
closure(R, X, Y) :- R(X, Z), closure(R, Z, Y).

then, if we assume the existence of the predicate parent that holds if the first argument is a parent of the second argument, we can define the predicate descendant as follows.

descendant(X, Y) :- closure(parent, X, Y).

Extensional Semantics

To understand the importance of this extension, consider the following axiom for bands (musical ensembles):

band(B):- singer(S), B(S), drummer(D), B(D), guitarist(G), B(G).

This says that a band is a group that has at least a singer, a drummer, and a guitarist. Suppose that we also have a database of musicians:

singer(sally).
singer(steve).
drummer(dave).
guitarist(george).
guitarist(grace).

Our extensional higher-order language allows the query

?- band(B).

At first sight a query like this seems impractical if not impossible to implement. Since a band is a set, bands can be very large and there can be many, possibly uncountably infinitely many of them. In existing intensional systems such queries fail since the program does not provide any information about any particular band.

However, in an extensional context the finitary behavior of the predicates of our language, saves us. If the predicate band declares a relation to be a band, then it must have examined only finitely many members of the relation. Therefore we can enumerate the bands by enumerating finite bands, and this collection is countable (in this particular example it is actually finite).

Other Higher Order Logic Systems

Clone this wiki locally