A Type-Directed Negation Elimination

TL;DR

This paper extends negation elimination techniques from the modal mu-calculus to the higher-order modal fixed point logic (HFL), providing a quadratic-size transformation procedure that is linear when variable count is fixed.

Contribution

It introduces a method for negation elimination in HFL, generalizing previous results and offering size-efficient transformations.

Findings

Quadratic worst-case size for negation elimination in HFL

Linear size transformation when variable count is fixed

Extension of well-formedness and negation normal form concepts to HFL

Abstract

In the modal mu-calculus, a formula is well-formed if each recursive variable occurs underneath an even number of negations. By means of De Morgan's laws, it is easy to transform any well-formed formula into an equivalent formula without negations -- its negation normal form. Moreover, if the formula is of size n, its negation normal form of is of the same size O(n). The full modal mu-calculus and the negation normal form fragment are thus equally expressive and concise. In this paper we extend this result to the higher-order modal fixed point logic (HFL), an extension of the modal mu-calculus with higher-order recursive predicate transformers. We present a procedure that converts a formula into an equivalent formula without negations of quadratic size in the worst case and of linear size when the number of variables of the formula is fixed.