FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic

Authors: Florian Bruse, Martin Lange and Etienne Lozes

Paper Information

Title:Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
Authors:Florian Bruse, Martin Lange and Etienne Lozes
Proceedings:PARIS Contributed papers
Editors: Alexis Saurin, David Baelde and Radu Calinescu
Keywords:modal fixpoint logic, lambda calculus, fixpoint alternation
Abstract:

ABSTRACT. Higher-Order Fixpoint Logic (HFL) is an extension of the modal mu-calculus by a typed lambda calculus. As in the mu-calculus, whether the nesting of least and greatest fixpoints increases expressive power is an important question. It is known that at low type theoretic levels, the fixpoint alternation hierarchy is strict. We present classes of structures over which the alternation hierarchy of HFL-formulas at low type level collapses into the alternation-free fragment, albeit at increase in type level by one.

Pages:4
Talk:Jul 07 11:45 (Session 26L: Contributed talks)
Paper: