International Journal of Foundations of Computer Science

A nonempty set C of vertices of a graph G is a star-cutset if G\C is disconnected and some vertex in C is adjacent to all the remaining vertices in C. A graph G is unbreakable if neither G nor its complement Ḡ contains a star-cutset. In this note we present a new characterization of unbreakable graphs.

This paper starts by setting the ground for a lambda calculus notation that strongly mirrors the two fundamental operations of term construction, namely abstraction and application. In particular, we single out those parts of a term, called items in the paper, that are added during abstraction and application. This item notation proves to be a powerful device for the representation of basic substitution steps, giving rise to different versions of β-reduction including local and global β-reduction. In other words substitution, thanks to the new notation, can be easily formalised as an object language notion rather than remaining a meta language one. Such formalisation will have advantages with respect to various areas including functional application and the partial unfolding of definitions. Moreover our substitution is, we believe, the most general to date. This is shown by the fact that our framework can accommodate most of the known reduction strategies, which range from local to global. Finally, we show how the calculus of substitution of Abadi et al., can be embedded into our calculus. We show moreover that many of the rules of Abadi et al. are easily derivable in our calculus.

The computational problem of model checking for circumscription of first-order formulae is studied. It is shown that there is a universal first-order formula whose circumscription has coNP-complete model checking problem. This answers a question raised by P.H. Kolaitis and C.H. Papadimitriou.

This paper proves that “promise classes” are so fragilely structured that they do not robustly (i.e. with respect to all oracles) possess Turinghard sets even in classes far larger than themselves. In particular, this paper shows that FewP does not robustly possess Turing hard sets for UP∩coUP and IP∩coIP does not robustly possess Turing hard sets for ZPP. It follows that ZPP, R, coR, UP∩coUP, UP, FewP∩coFewP, FewP, and IP∩coIP do not robustly possess Turing complete sets. This both resolves open questions of whether promise classes lacking robust downward closure under Turing reductions (e.g., R, UP, FewP) might robustly have Turing complete sets, and extends the range of classes known not to robustly contain many-one complete sets.

Some special sets of ω-words, namely, the sets that can be obtained by catenating nonempty finite sets of words, an infinite number of times, are considered. A condition for the equality of two such sets of ω-words is obtained.