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: |