A mathematical foundation of reflexion?
Brian T. Rice
Thu, 06 Jan 2000 22:17:12 -0800
At 02:42 AM 1/7/00 +0100, Massimo Dentico wrote:
>>From "Draft of ECOOP ^Ñ99 Banquet Speech", Peter Wegner
>There is abundant evidence that interactive services over time
>cannot be expressed by algorithms, but this result is difficult to
>prove theoretically. My colleague Dina Goldin and I have pursued
>two principal approaches towards this end, by machine models and
>mathematical models. Persistent Turing machines are a minimal
>extension of Turing machines that express interactive behavior by
>multi-tape machines with a persistent worktape preserved between
>interactions. Non-well-founded sets are an extension of
>traditional sets that provide a mathematical model of streams and
>interactive computing in terms of circular reasoning. The
>**mathematics of circular reasoning** was discovered only in the
>1980s and is comprehensively presented for the fitrst time in the
>1995 book Vicious Circles by Barwise and Moss. I will not try to
>explain non-well-founded set theory in a banquet speech, but will
>say a little about the intuitions that underlie **circular
>reasoning** and the reasons that it was not discovered and
>The key intuition is that the class of things that a finite agent
>can observe is greater than the class of things that an agent can
>construct. We can formalize this intuition by showng that the
>class of things that an agent can construct is enumerable, while
>the set of situation that an agent can observe is nonenumerable.
>Moreover, we can show that constructible sets can be specified by
>induction, while observable sets require a stronger inference rule
>Bertrand Russell in the 1900s and Hilbert and Godel in the 1920s
>made a fundamental mathematical mistake in assuming that induction
>was the strongest form of definition and reasoning. They were
>misled by the paradoxes of set theory and mitskenly thought that
>**circular reasoning** needed to describe observation processes
>was inconsistent. In fact, **circular reasoning** is consistent
>and allows stronger forms of definiton and reasoning than is
>possible through induction. Though induction is sufficient to
>describe construction processes stronger forms of reasoning are
>needed to express observation processes. Turing machines turn out
>to be the strongest form of computation possible by inductive
>reasoning but are not strong enough to express interactive
>computations of finite agents that observe an incompletely known
>environment, which are modeled by **circular reasoning**.
>See also: "Interaction, Computability, and Church^Òs Thesis", Peter
>Wegner, Dina Goldin, chapter 3. Mathematical Models of Interaction
I just got done doing an extensive amount of research just because of
reading that book, "Vicious Circles". It turns out to be, in my opinion,
an excellent source of formallization for some of my current work with
Arrow. Although hypersets are self-referential, the key part of the idea
that allows for better reflective principles is the coinduction principle
that allows a formalization of the difference between an interaction via a
stream and a stirctly non-interactive computation. To me, this relates
directly to continuations in Lisp, and therefore by extension, allows for a
partial answer to Fare's question in "Lambda-Calculus and Non-Determinism".
At any rate, I'm currently working really hard to put together my theory
into a professional and completely formalized form, although if you really
understand these ideas, you'll see that one formalism just won't cut it.
The results should be interesting, and I'm going to post results to my home
directory in various formats for you to comment on.
At any rate, my idea for arrow concerns the development of model theory for
information systems, and strongly centers around the notion of
interactivity. By the way, there are quite a few papers that discuss
extending model theory due to the types of reasoning in "Vicious Circles".
So, yes, I completely agree that this is an excellent way to enhance our
ideas of reflection.
Thanks ever so much for the links to those papers.