-quasiminimal enumeration degrees.
The notion of solvability in the call-by-value λ-calculus is defined and completely characterized, both from an operational and a logical point of view. The operational characterization is given through a reduction machine, performing the classical β-reduction, according to an innermost strategy. In fact, it turns out that the call-by-value reduction rule is too weak for capturing the solvability property of terms. The logical characterization is given through an intersection type assignment system,...
We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We show how the result can be used to prove the inherent ambiguity of languages of infinite trees. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded...
We introduce Oberwolfach randomness, a notion within Demuth’s framework of statistical tests with moving components; here the components’ movement has to be coherent across levels. We show that a ML-random set computes all -trivial sets if and only if it is not Oberwolfach random, and indeed that there is a -trivial set which is not computable from any Oberwolfach random set. We show that Oberwolfach random sets satisfy effective versions of almost-everywhere theorems of analysis, such as the...
We study the succinctness of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic least fixed point logic, which in turn is non-elementarily more succinct than monadic datalog. Succinctness...
We study the succinctness of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic least fixed point logic, which in turn is non-elementarily more succinct than monadic datalog. Succinctness...