Solving Łukasiewicz μ-terms

Łukasiewicz μ-calculus was introduced by Mio and Simpson and is an extension of Łukasiewicz logic, introducing scalar multiplication and least as well as greatest fixed points. A key question is how to evaluate terms of this calculus, i.e., find the values of bound variables occurring in a term. In this paper we provide an algorithm that is single exponential in the size of the term (this takes into account the size of rationals occurring in the term and the interpretation of free variables, the number of operators as well as the number of bound variables). We also show that the solutions are polynomially bounded in the size of the input term and interpretation of free variables. The core technique used is the solution of a set of affine fixed point equations with inequalities as side conditions for which a polynomial time algorithm is given. The techniques introduced here may be of wider interest in model checking and distributive systems.