SIMILARITY AND BISIMILARITY FOR
		    COUNTABLE NON-DETERMINISM AND
			HIGHER-ORDER FUNCTIONS

		  Søren B. Lassen & Corin Pitcher
			      (HOOTS II)
				   
We show that certain variants of similarity and bisimilarity are
compatible for a higher-order functional programming language with
countable non-determinism.  This work extends results of Howe and Ong
for languages with bounded non-determinism.

We extend a higher-order functional programming language with a
construct that can choose any natural number, but cannot diverge.  The
relations of interest on the language are lower (may) similarity,
upper (must) similarity, convex (may and must) similarity, and
bisimilarity.  The forms of similarity correspond to the different
constructions on preorders that are used to characterise the lower,
upper and convex powerdomains.  Bisimilarity reflects the possibility
of convergence or divergence in either direction.

Howe's original compatibility proof for lower similarity does extend
to the language.  However, the presence of the must converge
(equivalently, cannot diverge) judgement in the definitions of upper
similarity, convex similarity, and bisimilarity makes their
compatibility proofs more difficult than that of lower similarity.
The solutions proposed by Howe and Ong do not apply directly to a
language with countable non-determinism.

In this talk we show that it is possible to characterise the must
converge predicate inductively, via a collection of infinitary rule
schema.  The closure ordinal of the functional associated with the
rule schema is \omega for bounded non-determinism, but increases to
\omega^{CK}_1 (the least non-recursive ordinal) for countable
non-determinism.  We give the compatibility proofs for upper
similarity, convex similarity and bisimilarity in terms of this
inductive characterisation.

We also present some preliminary results about syntactic
\omega-continuity and \omega^{CK}_1-continuity in the presence of
bounded and countable non-determinism.