Abstract:
Rice's theorem tells us that no non-trivial property of the behavior of a Turing machine can be decided by looking at the machine itself. This situation changes completely when we consider weaker models of computation. Consider for example finite automata. Their behaviors are the languages they accept presented in a form of a tree. Rabin's theorem implies that all monadic second-order logic (MSOL) properties of behaviors of automata can be decided by looking at automata. Muchnik's transfer theorem says even more: for every MSOL property of behaviors, the set of automata whose behavior satisfies the property is MSOL definable. It turns out that the same is true for a much richer computation model which is the simply-typed lambda-calculus with fixpoint operators; in a slogan: the MSOL transfer theorem holds for evaluation.

In this talk we will see these results in a larger context. Rabin's theorem states that the MSOL theory of the full binary tree is decidable. Thanks to the technique of interpretation, many other interesting theories can be reduced to the MSOL theory of the binary tree, for example: Presburger arithmetic, Skolem arithmetic, the first order theory of countable well-founded orders. Muchnik's theorem coupled with interpolation gives us an even more powerful tool. Among others, it allows to obtain decidability of the MSOL theory of all graphs in the pushdown hierarchy.

Simply typed lambda-calculus with fixpoints is an abstraction of higher-order functional programs. It faithfully models the control in such programs but abstracts from data: all constants are non-interpreted. In particular, terms of this calculus can encode finite automata so that an evaluation of a term gives the behavior of the automaton it encodes. In this way, transfer theorem for evaluation generalizes Muchnik's theorem. It allows us to obtain even more decidable theories, and creates a link between language theory, verification, and semantics.