A mathematical foundation of reflexion?
Mon, 10 Jan 2000 18:28:37 +0100
"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.
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
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"
and "A Categorical Primer", Chris Hillman
Not cited here, from the F.I.S. Group WebSite - http://www.fis.lv/
these Scientific Proceedings:
"The Arrow Manifesto: Towards software engineering based on
comprehensible yet rigorous graphical specification"
"Humans, Computers, Specifications: The Arrow Logic of
Information System Engineering"
A riview on "TAC - Theory and Applications of Categories"
Paul Taylor (http://hypatia.dcs.qmw.ac.uk/author/TaylorP/) have
applied Category Theory to interpret the semantics of a simple
An Exact Interpretation of While, I
An Exact Interpretation of While, II
and in this thesis to type theory and polymorphism:
"Recursive Domains, Indexed Category Theory and Polymorphism"
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  and his Data Types as Lattices paper ,
together with the work of Smyth and Plotkin on recursive domain
equations  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  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
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
Does your conjecture make any nontrivial statement about
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.