**David Lee Winston Miller's**

**(half-baked & probably unoriginal)**

**Invertibility Theory**

Introduction

NOTE: Under construction. Very, very tentative! Also, the literature
has not been searched for similar theories. This page only represents a
*theory*. I have not PROVEN the claims below. I only suspect that
they may be true and propose them for discussion. A proof or counter example
may be fairly easy to come up with--I haven't given it time for either.
Or, the facts may suggest that the theory must be fine-tuned. Regardless
of the outcome, I think Cantor's Diagonal Argument should be useful in
this subject**-- this is my main point**. (It may also be useful
in relation to other CLP languages like CLP(

In any event, I suspect that if the theory is correct, then someone
has already proven it and stated more elegantly! (and recognized its possible
relation to other Constraint Logic Programming languages). *If you know
of such literature, or have comments, your input would be most appreciated.*
This theory was inspired by, and naturally extents from, my graduate studies
under Dr. Roger Cavallo
and Dr. Jorge Novillo
but *I'm* responsible for the thus-far half-baked aspect of this idea.
I sometimes worry that when students have "ideas" they are really
planted by their professors. (Intentionally sometimes, and at other times
because professors occasionally cook up their ideas while teaching). To
the extent that we student are correct in our "ideas", they are
sometimes not really our own. (I learned about the beauty of invertibility
in Dr. Novillo's Prolog class and
first proposed the idea of this paper in a discussion in Dr. Cavallo's
Special Topics class after Dr. Cavallo exposed me to Cantor's Diagonal
Argument. The paper also reflects some concepts gained in Dr. Cavallo's
Formal Methods class.)

Ideally, Prolog predicates should be invertible
(except in rare cases for which instantiation testing is important.) Beautifully
constructed invertible predicates are easily reused in programs and can
be flexibly used in queries. You don't have to worry about the input-output
assumptions that the programmer made. In its best, most *fundamental*
form, you can think of Prolog not a functional language but rather as a
relational language where arguments are not restricted to input or output
roles. That's what I find to be so beautiful about Prolog. (And if you
agree, I think that you will find the concept behind CLP(** R**)
to be more attractive because Prolog often fall's short of what we may
wish it to be. I haven't used CLP(

Unfortunately, from the code that I've seen, invertibility is rarely achieved. In my limited reading, I haven't seen a lot on the subject. So, here's a rather off-the-cuff attempt at furthering invertibility:

Theory of Invertibility

Let **p** be a Prolog predicate with arguments **A ^{1}**,

Let **D ^{i}** be the domain (or should I say range when speaking
of a relation, as opposed to a function?) associated with argument

Let **s ^{i}** be an element of the domain

Provided that clauses of **p** make no test for instantiation^{2}
and provided that clauses of **p** execute only "fundamental"^{3}
Prolog code:

If **p** is called with uninstantiated arguments and it happens that
the sequence of solutions (outputted by Prolog) enumerates the state space
{(**s ^{1}**,

Note that I do not claim here that it is necessary that the solutions
be instantiated. However, uninstantiated variables in the solution will
not be so general as to "cover" space not covered by **R**
(appropriately constrained) and will be general enough to cover the space
covered by **R** subject to the constraints specified.

Example: **two_ints**. ("Two Integers"--Produces the possible
pairs of positive integers.)

__Solutions of two predicates when "called" with
uninstantiated arguments:__

(For clarity, the solution is shown differently than normally presented as output by Prolog.)

?**two_ints_not_invertible**(A,B).

`A= 0 1 2 3 4 5 . . .`

`B= 0 0 0 0 0 0 . . .`

If you call this predicate with an instantiated integer for argument B,
you'll probably get a correct sequence of solutions. However, the sequence
of solutions when called with uninstantiated arguments (shown above) indicates
that this predicate *might* not be invertible. The sequence doesn't
cover the state space of the relation. If we think in terms of Cantor's
Diagonal Argument, we can see why:

(It appears doubtful that this predicate will ever produce, for example,
the solution A=2, B=2 if both A and B are uninstantiated. It is even questionable
that the predicate will function properly if we call it with A=2 --it will
probably generate the same sequence shown, skipping the first two states.)

?**two_ints_invertible**(A,B).

`A= 0 0 1 0 1 2 0 1 2 3 . . .`

`B= 0 1 0 2 1 0 3 2 1 0 . . .`

This predicate appears to be invertible. Again, we think in terms of Cantor's Diagonal Argument to show that the entire state space of the relation is "covered":

Summary

If the clauses of **p** make no test for instantiation, and it is
proven that the sequence of solutions (for a predicate called with uninstantiated
arguments) will be such that no solution will be missed, then **p**
is invertible. A further requirement, for invertibility to be guaranteed,
is that only "fundamental" code be employed--however, this requirement
may be dropped or simplified in the future if the requirement is shown
to be unnecessarily restrictive.

An unscientific rational for the theory might be expressed as follows:
*If a predicate can successfully enumerate its entire state space, it
would appear that it could also enumerate a smaller portion of it.*
However as logical as that sounds, we know that we can, using tests for
instantiation, make such a predicate fail under certain conditions. (For
instance, we could program one of the above example predicates to fail
if one argument is instantiated when the other is not.) For this reason,
we require more than a Diagonal Argument for proof of invertibility.

Notes

1. Note that Cantor's Diagonal Argument
proves that the reals are not denumerable. Invertibility probably cannot
be guaranteed via *this* theory if reals or any other nondenumerable
set constitutes the domain of an argument. (On the other hand, it may be
constructive to note that reals are generally expressed on computers as
finite numbers and that reals are always expressed in some finite fashion.)

2. Many built-in operators and predicates test for instantiation.

3. The term "fundamental" needs
to be explained of course. A predicate that employs simple matching is
an example of "fundamental" Prolog code. There are probably other
examples of Prolog code that would qualify. An example of code that would
not qualify as "fundamental" Prolog code would be any code that
tests for instantiation. (More specifically, "unfundamental"
code would at least include code that has the possibility of failing a
goal due to the fact that an argument--or combination of arguments--was
uninstantiated.) Of course, this leaves a lot of Prolog control operators
and predicates to be properly categorized as "fundamental" or
"unfundamental". "Fundamental" Prolog code is defined
here as the operators or predicates for which this theory holds. Any proof
of this theory might be constructed to prove (or disprove) the theory for
one predicate at a time. However, a more general approach, broadly defining
"fundamental" (with a proof for such a class of Prolog code),
may be possible. I suspect that most (if not all) control operators will
fail to fall in the "fundamental" class. I also suspect that
data classification predicates will also fail to be "fundamental".
In fact, I suspect, few Prolog constructs will qualify. (If this is frustrating,
we may find ourselves rebuilding Prolog or exploring other CLP languages
such as CLP(** R**).) However, an important point is that, with
proper knowledge, many predicates can be beautifully constructed such that
they are guaranteed to be invertible.

(It may be that when a predicate that makes no test for instantiation is "called" with uninstantiated arguments, and it happens that the sequence of solutions enumerate the solution state space intended to be covered by the predicate, then the predicate can be deemed invertible without having to check that the code is limited to "fundamental" constructs. This remains to be determined. For now, we will require "fundamental" code to be used, with the hope that we can ease invertibility insurance requirements in the future.)

4. By invertible I mean that the predicate
may be "called" with any combination of instantiated and uninstantiated
arguments resulting in a sequence of solutions (outputted by Prolog) that
enumerates the state space appropriately constrained (or unconstrained)
by the arguments. (The sequence of solutions will only "cover"
the states that represent valid solutions, and will not "cover"
any other states.) In addition, we require that invertible predicates *eventually*
terminate once additional solutions are no longer possible.

Copyright 1996, David Lee Winston Miller. This document may be reproduced provided that it is duplicated in its entirety including all links, credits and copyright notices.