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. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
