A mathematical foundation of reflexion?

[Massimo Dentico]

"Brian T. Rice" wrote:
 
> 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

Thank  you for your timely reply, Brian,  and sorry for the delay,
but  my  big problem is my bad knowledge of english (and for  this
reason  is  impossible for me to partecipate to the discussion  in
real-time  on IRC). Moreover my mathematical background  is  quite
limited.

I  am   taking an interest  in your work  since  your paper   "The
Arrow  System":   intuitively your approach  seem very  promising,
but   I  need a more deep  understanding. Now I'm trying to  learn
some  basic stuff on the subjects of Category Theory   and   Arrow
Logic.   Searching on the net for tutorials and other  material  I
have   discovered  that  Category Theory  attract  more  and  more
attention in the field of Computer Science.

I'm reading (very very slowly) these papers:

the already cited on these list

"A Crash Course in Arrow Logic"
- ftp://ftp.phil.uu.nl:21/pub/logic/PREPRINTS/preprint107.ps.Z

and "A Categorical Primer", Chris Hillman
- http://www.math.washington.edu/~hillman/PUB/categorical.ps

Not cited here, from the F.I.S. Group WebSite - http://www.fis.lv/
these Scientific Proceedings:
- http://www.fis.lv/ru.koi8/english/science.html

"The  Arrow Manifesto:  Towards  software engineering   based   on
comprehensible yet rigorous graphical specification"
- ftp://ftp.md.chalmers.se/pub/users/diskin/MANIFEST/arrfest.ps

"Humans,    Computers,   Specifications:   The  Arrow   Logic   of
Information System Engineering"
- ftp://ftp.md.chalmers.se/pub/users/diskin/PAPERS-DB/casys99.ps

A riview on "TAC - Theory and Applications of Categories"
- http://tac.mta.ca/tac/

Paul  Taylor  (http://hypatia.dcs.qmw.ac.uk/author/TaylorP/)  have
applied  Category Theory to interpret the semantics  of  a  simple
imperative language:

An Exact Interpretation of While, I
- http://hypatia.dcs.qmw.ac.uk/data/T/TaylorP/while-1987-II.ps.gz

An Exact Interpretation of While, II
- http://hypatia.dcs.qmw.ac.uk/data/T/TaylorP/while-1987-II.ps.gz

and in this thesis to type theory and polymorphism:

"Recursive Domains, Indexed Category Theory and Polymorphism"
- http://hypatia.dcs.qmw.ac.uk/data/T/TaylorP/thesis.ps.gz

This is an excerpt from the "Introduction", p. vi:
==================================================================
It  will be apparent that I consider myself a Mathematician rather
than  a Logician (I shall avoid the question as to whether I am  a
Computer Scientist), in the sense that it is tangible mathematical
objects  (models)  which interest me and not the  manipulation  of
syntax.  In fact syntactic discussion of polymorphic languages  is
decidedly   thin  in  this  work.  As  regards  the  "denotational
semantics" of programming languages, I lost (or rather, suspended)
my  faith in the applicability of these techniques some two  years
ago;  my interest in the subject is in the remarkable mathematical
behaviour of categories of domains.

I  have  perhaps  been less than courteous to some  of  its  other
practitioners. I apologise for this. However it would appear  that
Scott's   original  P[omega(?)  symbol]  and  D[infinite   symbol]
constructions [1972] and his Data Types as Lattices paper  [1976],
together  with  the work of Smyth and Plotkin on recursive  domain
equations [1978] account for most of what has been done as far  as
semantics, i.e. the provision of mathematical objects in which  to
explain things, is concerned. I am of the belief that Chapter V of
the present work is the first model of a type-of-types since 1976.
Moreover I further claim that it is the first (ever) to attempt to
explain its own existence (I cannot help but regard V in [omega(?)
symbol] as an accident). This in no way detracts from the value of
the  [1976]  paper,  indeed it is a veritable goldmine  containing
many  nuggets of which I personally have very little understanding
and which are sure to lead to many further major contributions  to
the subject.

I  should also like to offer a piece of friendly advice to  anyone
who  might  attempt in the future to study Domain  Theory.  It  is
this.

   Does  your  conjecture  make  any  nontrivial  statement  about
   finite posets?
   If so, then it's false: look for the counter example.

On  the other hand the remarkable fact about categories of domains
is  that  we seem never to have to worry about questions of  size;
indeed  this  (the fact that the function-space  of  a  continuous
lattice  is essentially no bigger than the given lattice) is  what
led Scott into the subject in the first place. In other words, the
existence of a type-of-types is no particular surprise.
==================================================================

It's truly hard for me to understand these papers with a precedent
little  exposure  to  first-order  logic,  naive  set  theory  and
elementary algebra, but I'm always available to learn. So links to
introductory papers are welcome.

--
Massimo Dentico