A mathematical foundation of reflexion?

[Brian T. Rice]

At 02:42 AM 1/7/00 +0100, Massimo Dentico wrote:
>>From "Draft of ECOOP ^Ñ99 Banquet Speech", Peter Wegner
>(http://www.cs.brown.edu/people/pw/papers/ecoop99_speech.pdf)
>
>------------------------------------------------------------------
>[...]
>
>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
>developed earlier.
>
>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
>called coinduction.
>
>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
>(http://www.cs.brown.edu/people/pw/papers/bcj1.pdf)
>
>-- 
>Massimo Dentico

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.
	Brian