Let 
be an equivariant relation. We show that under a certain assumption on 
, for every 
, if there exists a witness 
such that 
holds, then there also exists one with small support. We show an application to extending homomorphisms.
Category Archives: posts
Orbit finiteness vs. number of supported elements
A set is orbit finite if and only if the number of its elements supported by 
atoms grows polynomially with .
The colored open question closed
A question in my recent post Automorphisms vs color-preserving automorphisms in Fraisse classes has been answered negatively by Mikołaj. The counterexample Fraisse class is the age of the structure 
, the rational numbers with the ternary ‘cyclic order’ relation 
defined by:
![\[T(x, y, z) \iff x<y<z \ \lor \ z<x<y \ \lor \ y<z<x.\]](https://atoms.mimuw.edu.pl/wp-content/ql-cache/quicklatex.com-cde928718d51666d7943a367f1bef972_l3.svg "Rendered by QuickLaTeX.com")
I am about to reformulate the question slightly, in order to make refutation harder;)
A stronger Kleene theorem
This post continues the discussion on the Kleene theorem from here. The previous post gave a notion of regular expressions that had the same expressive power as nondeterministic automata. The idea was that a star corresponds to a graph where the set of vertices had one orbit, and where the edges where labelled by simpler regular expressions. In the case without atoms, such a graph is necessarily a self loop, which corresponds to the standard Kleene star. This post is about a stronger requirement: instead of saying that the graph has one orbit of vertices, we say that it has one orbit of edges.
Normalization of pp-formulas
Classicaly, primitive positive formulas form the smallest fragment of first-order logic which is closed under conjunction and existential quantification. Pp-formulas can be turned in to a normal form 
– this is due to Skolemization, i.e. the fact that 
can be turned into 
. In this case, Skolemization is a consequence of the axiom of finite choice.
We show that in the world with atoms, not every orbit-finite pp-formula can be converted into an equivalent one in prenex form. This is another demonstration of the failure of the axiom of choice.
This raises the question: what is the appropriate notion of a pp-formula, which does have normal forms?
The Rum Conjecture is refuted
A conjecture I posted a while ago, concerning reachability of states in automata with atoms after a Brzozowski phase, has been refuted by Mikołaj Bojańczyk.
A Kleene Theorem with Atoms
Standard alphabets beyond equality atoms
In this post, I try to give a characterization of standard alphabets (i.e. alphabets where Turing machines determinize) which works for many choices of atoms.
Theorem. Assume that the atoms are oligomorphic, have a decidable first-order theory, and for every one can compute the number of orbits of -tuples of atoms. The following conditions are equivalent for every orbit finite set 
.
- Turing machines over input alphabet determinize
- There exists a function
which is computable by a deterministic Turing machine, and such that two words are in the same orbit if and only if they have the same image under 
.
Existence of least supports for Fraisse atoms
In Automata theory in nominal sets (Thm. 9.3), we provided a necessary and sufficient criterion for the existence of least finite supports for arbitrary atoms. It was not clear whether the criterion could be significantly simplified for Fraisse atoms. I show that it cannot be made as simple as we originally conjectured.
Derived alphabets
We study a derivation quasi-order between between alphabets. Whenever is derived from 
and is non-standard then is non-standard too. We identify also a class of minimal non-standard alphabets wrt. the quasi-order.