Object Variables

Appeared in Volume 9/2, May 1996

Keywords: variables.

pjr@cs.uq.edu.au
Peter Robinson
19th February 1996

Previous postings to comp.lang.prolog about writing a predicate to carry out term substitution (substitute/4) have hinted at some of the problems that arise when using Prolog to represent substitutions, object-variables and quantifiers. One of the key questions is "How do I represent object-variables?".

There appear to be two options for representing object-variables in Prolog:

(a) as Prolog variables (logically this means, as variables ranging over the objects in the semantics which are object variables); or

(b) as some data structure e.g. atoms.

The problem with (a) is that Prolog is untyped: Prolog variables can be bound to any term and this is almost certainly not what is wanted for representations of object-variables.

Consider, for example, a definition of a predicate substitute(T, X, Term, NewTerm) which is supposed to replace free occurrences of X in Term by T to give NewTerm.

My conjecture is that no matter how substitute/4 is written (within reason) the following queries would give different answers.

?- substitute(b, X, f(a,X), T), X = a.
?- X = a, substitute(b, X, f(a,X), T).

The problem with (b) is that we might want to unify terms containing object variables. For example, consider a theorem prover with a generalization rule

rule(generalization, T, forall(x, T)).

and a query:

?- rule(generalization, p(y), forall(y, p(y)).

The intent is that this should succeed but it is not clear how this could work if object variables are represented by some data structure.

A Plug for Using Qu-Prolog

Qu-Prolog is an extended Prolog designed primarily as an implementation and tactic language of interactive theorem provers. It does not have a lavish supply of types, but it does have a second class of variables (called object variables, a convenient abuse of language) that range over the real object variables (which are semantic objects - a subset of the objects over which ordinary Prolog and Qu-Prolog variables range).

Qu-Prolog has representations for quantifiers, substitutions, and object-level variables. The unification algorithm is appropriately extended and includes substitution evaluation.

The object language of Qu-Prolog is a full higher order language that includes quantified terms and object variables.

Syntactically, object variables have the same form as atoms but are distinguished by declaration. So, for example, if x is declared as an object variable then this also declares the infinite class x1, x2, ... as object variables.

One of the postings on this subject referred to using substitutions for implementing beta-reduction.

As an example, here is a Qu-Prolog program for lambda-evaluation. This example also illustrates some of Qu-Prolog's support for higher-order notations.

?- obvar_prefix(x).	% declare x, x1, x2,... as object variables

?- op(500, quant, lambda).	% declare lambda as a quantifier
?- op(800, xfx, =>).	% single reduction
?- op(800, xfx, =>*). 	% zero or more reductions

% a recogniser for lambda terms
lambda_term(x).	% object variables are lambda terms
lambda_term(A(B)) :-	% application
    lambda_term(A),
    lambda_term(B).
lambda_term(lambda x A) :-
    lambda_term(A).

% lambda evaluation
A =>* C :- A => B, B =>* C, !.
A =>* A.
(lambda x A)(B) => [B/x]A.	% beta rule - [B/x] represents a substitution
A(B) => C(B) :- A => C.
A(B) => A(C) :- B => C.
lambda x A => lambda x B :- A => B.
lambda x A(x) => A :- x not_free_in A.	% eta rule (optional)

Note, for example, that the query

?- lambda_term(x1).

succeeds by unifying x1 and x (of the program) and that

?- lambda x1 x1 = lambda x2 x2.

succeeds without instantiation (alpha-equivalence).

Qu-Prolog has been in serious use for some years as the implementation language of an interactive theorem prover (Ergo) which is now getting used in industrial trials of the development of formally verified software. Thus, for example, Qu-Prolog has a seriously useable level of performance. A bonus, necessary for this class of work, is that Qu-Prolog does do occurs checking (unless it can detect that none is necessary).

For more information on Qu-Prolog please contact me.

Peter J Robinson
Dept. of Computer Science
The Univ. of Queensland
Queensland 4072, Australia
Email: pjr@cs.uq.edu.au
Tel: +61 7 365 3461
Fax: +61 7 365 1999