Abstract Data Types
The theme of this paper is the interaction between recursion-theoretic and algebraic properties of abstract data types. We show that any "algebra with semicomputable inequality which has a nonunit computable $V$-behaviour has a final algebra specification by a finite set of equations and possibly using additional function symbols. For any computable algebra there is a finite set of equations specifying it under both the initial and final algebra semantics. All recursively enumerable degrees of unsolvability arise both in final and initial algebras." (My quotes here are not from the paper, but instead from the summary on by H. Jürgensen on Math Reviews).
Of the three papers above, the last is probably the most interesting.
We exhibit an initial specification of the rational numbers equipped with addition, subtraction, multiplication, greatest integer function, and absolute value. Our specification uses only the sort of rational numbers. It uses one hidden function; that function is unary. But it does not use an error constant, or extra (hidden) sorts, or conditional equations. All of our work is elementary and self-contained. Discrete Mathematics and Theoretical Computer Science Volume 4, no. 2 (2001), pp. 291-300. Here is the paper at the DMTCS site.
Abstract State Machines
Coalgebra
We present a generalization of
modal logic to logics which are interpreted
on coalgebras of functors on sets.
Each coalgebraic logic is determined by a functor on sets
satisfying a few properties, and the formulas of
each logic are interpreted on coalgebras of that functor.
Among the logics obtained are a certain fragment of infinitary
modal logic as well as versions of natural
logics associated with various classes of transition systems,
including probabilistic
transition systems.
The end of the paper argues that
the formulas of coalgebraic logics can be viewed
as approximations to the elements of a final coalgebra.
The basic idea of generalizing modal logic to coalgebras
has been pursued by many other people. In most cases, the
work has been more specific than in the orginial paper.
And by considering a smaller class of functors, better results
have been obtained. For more in this area, one should see
papers by Alexandru Baltag, Bart Jacobs, Alexander Kurz,
Dirk Pattinson, Martin Rossiger, and others.
The last sections
of "Coalgebraic Logic"
appear with lots of blank spaces due to
a bug in the printing process, and they re-appear in the same
journal: 99 (1999) no. 1-3, 241-259.
You can get it here as a
postscript
file.
This paper gives a new foundation to the topics above,
using final coalgebras instead of domains or metric spaces.
The subject certainly could have been studied from that
angle all along.
This paper is a more developed version of the last one.
It takes much more background, but the results are also much
better.
It shows how to solve and study recursive program schemes using
coalgebra and (especially) Elgot algebras. The work also includes
treatments of implictly defined functions in other areas of mathematics.
The current version of this paper
is available from the web site of
Stefan Milius,
and the paper will appear as well in the proceedings of
the first meeting on
Algebra and Coalgebra in Computer Science (CALCO),
to be held at the
University of Wales, Swansea, from
September 3-6, 2005.
This paper connects coalgebra with a long discussion in
the foundations of game theory on the modeling of type spaces.
We argue that type spaces are coalgebras, that universal
type spaces are final coalgebras, and that the modal logics
already proposed in the economic theory literature are closely
related to those in recent work in coalgebraic modal logic.
In the other direction, the categories of interest in this
work are usually measurable spaces or compact (Hausdorff) topological
spaces.
A coalgebraic version of the
construction of the universal type space
due to Heifetz and Samet is generalized for some
functors in those categories.
Since the concrete categories of interest
have not been explored so deeply in
the coalgebra literature, we have some new results.
We show that every functor on the category of measurable spaces
built from constant functors, products, coproducts, and
the probability measure functor has a final coalgebra.
Moreover, we construct this final coalgebra from the relevant
version of coalgebraic modal logic. Specifically, we consider
the set of theories of points in all coalgebras and endow
this set with a sigma-algebra and coalgebra structure; the main
result is the finality of this space.
This
is the journal version of the paper above. It also has a logical
represenatation of
the final coalgebras of all functors on Sets
built from the identity and constant functors
using products, coproducts, functions from a fixed set, and
the functor of discrete probability measures.
This paper is a contribution to the
study of uniformity conditions
for endofunctors on sets initiated in
Peter Aczel's 1988 book and pursued
later in papers of others.
The main results
have been
that the "usual" functors on sets are uniform
in some sense, and that assuming the Anti-Foundation Axiom
AFA, a
uniform functor has the property that its greatest fixed point
is a final coalgebra whose structure is the identity map.
We propose a notion of uniformity whose definition involves
notions from recent work in coalgebraic recursion theory such
as completely iterative monads and completely iterative algebras
(CIAs),
This simplifies many calculations and makes the definition
of uniformity more natural than it had been.
We also present several new results,
including one which could be called a
Paranoia Theorem:
For a uniform functor H, the entire universe is a CIA: the structure is
the inclusion of HV into the universe V itself.
Some papers in the section on
Recursion/Corecursion
are also
relevant to coalgebra.
Grammar Formalisms
As its title suggests, this paper gives some completeness
results for the Rounds-Kasper logics of feature structures.
As in
many modal completeneness results, the proofs use canonical models.
The topic of these papers is Stratified Feature Logic,
a formalization of relational grammar which incorporates
extensions of feature logic.
These last papers make the proposal of using evolving algebras
in the description of syntactic formalisms. The contain
many examples of different formalisms rendered dynamically.
Graphs
There is a countable graph which isometrically embeds
every countable graph. This paper discusses this and
some related material from a model-theoretic point of view.
In addition to some positive results on universal graphs,
this paper also shows some negative ones. For example,
there is no countable planar graph which is universal
with respect to one-to-one graph homomorphisms. If we
drop the 'one-to-one', then the Four Color Theorem tells
us that K4 is universal. So the result here indicates a
way in which the 4CT can't be improved.
For each n there's a countable graph of diameter n
which isometrically embeds all countable graphs of diameter n.
This short paper shows that the Johnson graphs J(n,3) satisfy
a distance extension property called I3, provided that
n is at least 6. No finite graphs with I3 were known up
to this point. We also use a random method to construct graphs
with I3 and local versions of the Pk properties studied
in connection with the Rado universal graph.
[postscript]
Hypersets
This paper gives a connection of hypersets with
domain theory. The model of that paper gave rise
to the axiomatic theory of partial sets mentioned
in the paper above.
This is a survey paper about set theory and circularity.
If you are interested in the topic of hypersets, you might also
like to see a
book
on it.
Manifesto
My main purposes in this essay are to introduce applied logic
as a research area, to situate it in a broader context,
to make the case that it is a significant
and worthwhile enterprise, and to detail
some of its research areas.
These are my main overt purposes. But my "covert"
purpose is to write something that might open new doors
for young students with interests in logic. In my
younger days I remember the excitement I felt from
subjects at the borders of mathematics, computer
science, and linguistics. It was not until many years
later that I began to think more explicitly
about the "politics" of what
I and many others have been doing. I think it would
have helped me to ponder a manifesto or two
along the way, even in my high school or college days.
So my hope about this article is that somewhere, sometime,
somebody will pick it up and . . .
Modal Logic
These papers present a logical system in which
formulas are evaluated at pointed sets. The modalities
include shrinking the set around the point, and moving
the point inside the set. The idea is to get a decidable
core language for the kind of reasoning that goes on in
elementary topology.
Of these two papers, the first is a preliminary
version, and the second contains the full proofs
and much more other information.
This paper shows that the correspondence theory can be
re-worked to deal with models modulo bisimulation rather
than frames. The overall idea is to pass from
finitary modal logic to infinitary modal logic and
from Kripke models to their strongly extensional
quotients.
This paper constructs logical languages which are
interpreted on coalgebras of functors on sets. The languages
generalize a fragment of infinitary modal logic (the fragment
contains of the characterizers of the bisimulation classes
of arbitrary models. A result in the paper gives the characterization
result for coalgebraic logic, assuming a uniformity condition on
the functor.
This last group of papers present logical systems in which various
group-level
epistemic actions are incorporated into the object language. That is, we
consider the standard modeling of knowledge among a set of agents
by multi-modal Kripke structures. One might want to consider actions
that take place, such as announcements to groups privately,
announcements with suspicious outsiders, wiretapping, etc.
In our system, such actions
correspond to additional modalities in the object language. That
is, we do not add machinery on top of model
but we reify aspects of the machinery in the logical language.
In addition to a useful semantics, we also have completeness/decidability
results for all the logics of this type. And we have
expressive power results, such as the following: A logical
system with the ability to reason about common knowledge
and public announcements is less expressive than one
with the ability to reason about common knowledge,
public announcements, and private announcements.
Here is a guide to the papers above.
The 2000 paper with Alexandru Baltag and Slawomir Solecki
is a very concrete presentation of some logical systems for
dynamic epistemic logic. It is superceded by several other papers,
mostly because of improvements in the overall syntax. (Some readers
might still prefer the 2000 version, since it is shorter to read.)
The paper "Logics for Epistemic Programs" presents logical systems
with a more standard syntax. It also discusses a large number of
examples. There is a paper on the completeness theorems for
these logics that will be done shortly. The paper with Joseph Miller
shows that it is not possible to iterate epistemic actions
such as announcements and remain decidable.
Specifically, we show that three fragments of logic of iterated
relativization (announcements) and transitive closure are
$\Sigma^1_1$-complete. Of these,
two fragments do not include transitive closure. We also show that the
question of whether a sentence in these fragments has a finite (tree)
model is $\Sigma^0_1$-complete. These results go via reduction to problems
concerning domino systems.
Natural Language Semantics
Quantum Logic
Recursion and Corecursion
My Ph.D. dissertation. The idea is to extend
set recursion by adding the power set operation as a
primitive. This gives a countable family of set theoretic
operations which are considered "recursive"; the family
contains practically all operations studied concretely
in set theory. The work goes on to study degree theory
and also to get equiconsistency results between
recursion theory and set theory.
My advisor is
Professor Yiannis N. Moschovakis
of the
UCLA Mathematics Department.
This paper is about the logic FLR0, originally proposed
by Moschovakis. The paper presents a general logical system
for reasoning about recursion.
This paper draws connections between hypersets
and the logic of recursion. It also presents a new
logical system which is complete for reasoning about
circularly defined sets.
[Abstract |
postscript
]
This paper develops a theory of substitution and
recursion for parametrically defined objects in final
coalgebras. It also develops the theory of uniform
functors on sets. In so doing, it shows how to do
some of the mathematics of the book
Vicious Circles
in a more elegant and general way.
This paper is concerned with the equational logic
of corecursion, that is of definitions involving
final coalgebra maps. The framework for our
study is iteration
theories, recently
re-introduced as models of
the FLR_0 fragment of Moschovakis' Formal Language of
Recursion. We present a new class of iteration theories
derived from final coalgebras.
We also study the valid equations in the semantics,
and prove the relevant completeness theorem. This is
actually a new proof of the well-known completeness
theorem for fixed point equations in general settings.
The last few papers in this group are also related to
Coalgebra.
Situation Theory