RE: [Axiom-developer] Consistency (was Lazy Evaluation)

[Page, Bill]

On Thursday, June 23, 2005 5:12 PM Bob McElrath wrote:
> ...
> Circular dependencies, however, deserve more thought.  This could
> break lazy re-evaluation logic.  But, is there any *sensible*
> document with circular dependencies?  I would call a circular
> dependency a "bug". (one which an intelligent front-end could warn
> the user about)
>

Jon Barwise and Lawrence Moss (see previous email refering to their
book "Vicious Circles"), disagree strongly with your opinion and
demontrate many cases where circular definitions do make sense
and are very efficent formal descriptions of some phenomena or
idea. Unfortunately Jon Barwise died in ca. 2000. 

I think calling a circular dependency a "bug" is not so different
from those people who would claim that doing mathematics on a
computer is impossible because it easy to show that there are
many more real numbers than there are integers and computers only
have finite memory so they can not even represent all the integers!
I know some people who have even argued that this problem demonstrates
that artifical intellegence is impossible because obviously human
beings (mathematicans) can reason effectively about real numbers.
And we believe that we use them all the time in physics and in
engineering. But in using computer algebra systems we know that
this argument about fundamental limitations of the ability of
computers is wrong. It is quite possible to write programs
which manipulate and appear to reason about infinite objects.

Many of the things (not all) that can be described in a circular
manner turn out to be infinite objects, in fact what mathematicians
might call *very big* objects (in a specific technical sense).

Here is another plug for book and a very useful review paper:

http://cogprints.org/336/
http://page.axiom-developer.org/zope/Plone/refs/articles/akman-vicious.pdf/v
iew

"To a greater or lesser degree, every scientific advance marks some
departure from the common sense that preceded it." These words of
Irving M. Copi (Copi, 1979, p.195) apparently summarize the nature
of Vicious Circles in the most concise fashion. Following the steps
of Aczel's ground-breaking monograph (Aczel, 1988) which marked a
departure from the `common sense' that is attributed to classical set
theory, this new book (abbreviated as VC in the sequel) of Jon Barwise
and Larry Moss not only offers an introduction to the revolutionary
and fascinating topic of non-wellfounded sets (a.k.a. hypersets) but
also becomes the most authoritative source for any serious researcher
(mathematician, philosopher, or computer scientist alike) who wants
to understand and further pursue this timely topic."

And in a footnote the reviewer write:

"It is hard to tell why circularity has always been regarded with
doubt in mathematical circles. One reason may be that circular
arguments or structures are thought to be diffcult to grasp, most
probably due to our educational make-up in linear thinking. On a
more personal note: I tend to think that popular works such as
Escher's drawings may have helped to create the illusion that
circularity invites nonsense."

> Here is some discussion on this from the smv language (some kind
> of formal verification tool)
>
> http://www.cis.ksu.edu/santos/smv-doc/language/node17.html
>

"There are cases where a combinational [i.e. circular] loop
``makes sense'', in that there is always a solution of the
equations. In this case, the order in which signals are evaluated
may be conditional on the values of some signals. For example,
take the following system:

        x := c ? y : 0;
        y := ~c ? x : 1;

If c is false, then we may first evaluate x, then y, obtaining
x = 0, then y = 0. On the other hand, if c is true, we may
first evaluate y, then x, obtaining y = 1, then x = 1. The
existence of conditional schedules such as this is difficult
to determine, since it may depend on certains states (or signal
values) being ``unreachable''. For example, if we have

        x := c ? y : 0;
        y := d ? x : 1;

it may be the case that c and d are never true at the same time,
in which case x and y can always be evaluated in some order.
Loops of this kind do sometimes occur in hardware designs
(especially in buses and ring-structured arbiters). The
expected approach to this problem is require the user to
provide constraints on the order of evaluation (so that the
program can be compiled), and to verify that these constraints
always have a solution."

I think these examples are good ones and are probably similar
to many of the kinds of circularities that are found in Axioms
algebra library. I think it is easy to see that there is nothing
"fundamentally wrong" with these definitions and that it
should be possible in principle to use such statements as
reliable specifications for a program. Of course this does not
necessarily mean that compiling such specifications into a
runnable program is going to be easy. On the other hand there
seem to quite a large number of cases where a "fixed point"
iteration procedure starting from some inconsistent partial
solution, will necessarily lead to the unique and real
solution. Specifically, I think that this is the case in the
case of the Axiom library.

Regards,
Bill Page.