The full version of the paper is available at arXiv:1106.0425.

We convert these rules into rewrite rules, which permits building up an interpretation of PDL through terms in an algebra which admits operators of infinite arity. It is shown that each program corresponds to an essentially unique irreducible tree, which in turn is assigned a natural transformation of a suitable functor, serving as the programm's interpretation. Some technical problems have to be overcome by the observation that the interpretation of the indefinite interpretation requires a base space which is closed under the well-known Souslin operation from set theory. This is in particular inconvenient when the state space is assumed to be Polish: these spaces are closed under this operation only if they are finite. Hence previous results on the coalgebraic interpretation of modal logics are difficult to apply. The paper discusses the expressivity of these models and relates properties like logical and behavioral equivalence or bisimilarity to the corresponding properties of a Kripke model for a closely related non-dynamic logic of the Hennessy-Milner type.

Research funded in part by Deutsche Forschungsgemeinschaft, grant DO 263/12-1, Koalgebraische Eigenschaften stochastischer Relationen

In the solid domain of 3D objects in R

We study the visual hull in the solid domain which allows the notion of partial visual hull. It captures the imprecision in the input polyhedral scenes and outputs the exact information about what points are definitely inside/outside the visual hull. The partial visual hull algorithm maintains the same computational complexity as the classical method and generates a partial visual hull which converges to the classical visual hull as the input converges to an exact value. We show the Hausdorff and the Scott continuity of the domain-theoretic construction in the Solid domain of the projective 3 space P

- for every ordinal $i$ we have $A_{i+1} = FA_{i}$

- for $j \le i$ we have $A_{j+1;i+1} = FA_{j;i}$

- for limit $i$ the cone $(A_i; (A{j,i})_{j

Let us consider the $\kappa$-bounded powerset functor $P^{\kappa}$, where $\kappa$ is an infinite regular cardinal. The most interesting cases are $P^{\omega}$ and $P^{\omega_1}$ , the finite powerset and countable powerset functors respectively.

The final sequence of $P^{\kappa}$ (and of other functors) was studied in [Wor05]. It was shown that $A_{\kappa,\kappa+1}$ is an injection, and hence $A_{j,i}$ is an injection for all $j \ge\kappa$. Finally, since $P^{\kappa}$ preserves intersections, the sequence stabilizes at $\kappa+\omega$.

The map $A_{j,i}$ is not injective for $j < \kappa$, because the kernel of $p_j$ is the $j$th approximant to bisimilarity, see e.g. [Sta09].

But which connecting maps are surjective? [Wor05] answers this for $P^{\omega}$.

2. Each projection $p_{i}$, for $i <\omega$, is surjective.

However, the question for general $\kappa$ remained open. We report progress as follows.

1. The final sequence for $P^{\kappa}$ does not stabilize until $\kappa+\omega$.

2. Suppose $\kappa > \omega_1$. Then the projection $p_i$ is surjective for all countable $i$.

This fully answers the surjectivity question for the countable powerset functor. In the case of $\kappa>\omega_1$ it remains open whether $p_i$ is surjective for all $i <\kappa$.

[Sta09] Sam Staton. Relating coalgebraic notions of bisimulation. In Proceedings, CALCO, volume 5728 of LNCS, 2009.

[Wor05] James Worrell. On the nal sequence of a nitary set functor. Theoretical Computer Science, 338(1-3):184-199, June 2005.

Supported by EPSRC Advanced Research Fellowship EP/E056091/1

Here "mic" stands for "minimally inconsistent".

There is a standard assignment of ordinals to nodes in well-founded trees and then to well-founded trees. We assign ordinals $||n||$ to nodes $n$ of a non-empty well-founded countable tree $\tau$ by:

$||n|| = 0$ if $n$ is a leaf

$||n|| = sup{||n'|| + 1 | n' is a child of n} otherwise

The ordinal $||\tau||$ of such a tree $\tau$ is defined to be the ordinal of its root. The ordinals obtained in this way are exactly the countable ones. If $\tau\to D^o$ is a mic tree then $||\tau|| > 0$. Combining these ordinals with mic trees we can first define coherence degrees of domains and then of categories of domains. The coherence degree $coh(D)$ of a Scott domain $D$ is defined by:

$$coh(D) = sup{||\tau||+1 | there is a mic tree \tau\to D, with \tau well-founded and countable}$$

For example, the $n$-coherent domains are those with coherence degree $n$ (for $n \neq 1$).

Every Scott domain has coherence degree $\le\omega_1$, and there is a non-trivial Scott domain with every such ordinal (except for 1).

Next, the coherence degree $coh(C)$ of a full subcategory $C$ of Dom, the category of Scott domains, is defined by:

$$coh(C) = sup{coh(D) + 1|D \in Ob(C)}$$

We have $coh(C)\le\omega_1 + 1$, but not = 2. (The case $coh(C) = 0$ is when $C$ has no objects.)

Let $Dom_\kappa$ be the full subcategory of all domains with coherence degree $<\kappa$ (for $\tau\le\omega_1 + 1$, but not = 0, 2); it has coherence degree $\kappa$. Let $Dom^f_\kappa$ be the full subcategory of all domains with finitely many points with coherence degree $<\kappa$ (for $\tau\le\omega$, but not = 0, 2); it has coherence degree $\kappa$. We discuss the following conjecture:

(The trivial ones are those with at most one object.)

References

[Jun90] Achim Jung, The Classification of Continuous Domains (Extended Abstract), Proc. 5th LICS, 35-40, 1990.

[Plo78] Gordon D. Plotkin, T^omega as a Universal Domain, J. Comput. Syst. Sci., 17(2), 209-236, 1978.

[Sco76] Dana S. Scott, Data Types as Lattices, SIAM J. Comput., 5(3), 522-587, 1976.

[Sco82] Dana S. Scott, Domains for Denotational Semantics, Proc. 9th ICALP, LNCS, 140, 577-613, 1982.

[Smy83] Michael B. Smyth, The Largest Cartesian Closed Category of Domains, Theor. Comput. Sci., 27, 109-119, 1983.

P(X) =

P

L(X) =

We can understand these monads as arising from algebraic theories. Following Plotkin and Power [2] we can in turn understand the algebraic theories as theories of computational effects. The finite-non-empty powerset monad P

Some references

[1] P. Freyd. Numerology in topoi. Theory Appl. of Categ., 16(19):522-528, 2006.

[2] G. D. Plotkin and J. Power. Notions of computation determine monads. In Proc. FOSSACS'02, volume 2303 of Lecture Notes in Comput. Sci., pages 342-356, 2002.

[3] D. Sangiorgi. A theory of bisimulation for the pi-calculus. In Proc. CONCUR'93, volume 715 of Lecture Notes in Comput. Sci., pages 127-142, 1993.

Research partly supported by ERC grant Events, Causality and Symmetry.

[AJ94] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symbolic Logic, 59:543-574, 1994.

[Tan97] A.M. Tan. Full completeness for models of linear logic. PhD thesis, University of Cambridge, 1997.

I will show how to overcome these two problems, using bases with just intersections rather than unions too. The key idea is a weakening of the roundedness conditions.

These weaker conditions are satisfied by interval arithmetic and preserved by composition and lambda-abstraction. The outcome is that we may translate the ASD language for topology into familiar styles of logic, functional and interval programming. Moreover, lamdda-abstractions become closures in the usual way.

Last modified: Fri Sep 2 2011