Search

We define Sahlqvist fixed point formulas. By extending the technique of Sambin and Vaccaro we show that (1) for each Sahlqvist fixed point formula @f there exists an LFP-formula @g(@f), with no free first-order variable or predicate symbol, such that a descriptive @m-frame (an order-topological structure that admits topological interpretations of least fixed point operators as intersections of clopen pre-fixed points) validates @f iff @g(@f) is true in this structure, and (2) every modal fixed point logic axiomatized by a set @F of Sahlqvist fixed point formulas is sound and complete with respect to the class of descriptive @m-frames satisfying {@g(@f):@[email protected][email protected]}. We also give some concrete examples of Sahlqvist fixed point logics and classes of descriptive @m-frames for which these logics are sound and complete.

We show that for several classes of idempotent semirings the least fixed-point of a polynomial system of equations X = f ( X ) is equal to the least fixed-point of a linear system obtained by “linearizing” the polynomials of f in a certain way. Our proofs rely on derivation tree analysis, a proof principle that combines methods from algebra, calculus, and formal language theory, and was first used in Esparza et al. (2007) [10] , to show that Newton’s method over commutative and idempotent semirings converges in a linear number of steps. Our results lead to efficient generic algorithms for computing the least fixed-point. We use these algorithms to derive several consequences, including an O ( N 3 ) algorithm for computing the throughput of a context-free grammar (obtained by speeding up the O ( N 4 ) algorithm of Caucal et al. (2007) [7] ), and a generalization of Courcelle’s result stating that the downward-closed image of a context-free language is regular (Courcelle, 1991) [8] .

One of the most well-known induction principles in computer scienceis the fixed point induction rule, or least pre-fixed point rule. Inductive *-semirings are partially ordered semirings equipped with a star operationsatisfying the fixed point equation and the fixed point induction rule forlinear terms. Inductive *-semirings are extensions of continuous semiringsand the Kleene algebras of Conway and Kozen.We develop, in a systematic way, the rudiments of the theory of inductive*-semirings in relation to automata, languages and power series.In particular, we prove that if S is an inductive *-semiring, then so isthe semiring of matrices Sn*n, for any integer n >= 0, and that if S isan inductive *-semiring, then so is any semiring of power series S((A*)).As shown by Kozen, the dual of an inductive *-semiring may not be inductive. In contrast, we show that the dual of an iteration semiring isan iteration semiring. Kuich proved a general Kleene theorem for continuous semirings, and Bloom and Esik proved a Kleene theorem for all Conway semirings. Since any inductive *-semiring is a Conway semiringand an iteration semiring, as we show, there results a Kleene theorem applicable to all inductive *-semirings. We also describe the structureof the initial inductive *-semiring and conjecture that any free inductive*-semiring may be given as a semiring of rational power series with coefficients in the initial inductive *-semiring. We relate this conjecture torecent axiomatization results on the equational theory of the regular sets.

This paper is a comparative study of a number of (intensional-semantically distinct) least and greatest fixed point operators that natural-deduction proof systems for intuitionistic logics can be extended with in a proof-theoretically defendable way. Eight pairs of such operators are analysed. The exposition is centred around a cube-shaped classification where each node stands for an axiomatization of one pair of operators as logical constants by intended proof and reduction rules and each arc for a proof- and reduction-preserving encoding of one pair in terms of another. The three dimensions of the cube reflect three orthogonal binary options: conventional-style vs. Mendler-style, basic (“[co]iterative”) vs. enhanced (“primitive–[co]recursive”), simple vs. course-of-value [co]induction. Some of the axiomatizations and encodings are well known; others, however, are novel; the classification into a cube is also new. The differences between the least fixed point operators considered are illustrated on the example of the corresponding natural number types.

This survey exhibits various algorithms to decide the question if a given ordered set P has the fixed point property resp. if P has a fixed point free order-preserving self-map. While a depth-first search algorithm for a fixed point free map is easily written it is also quite inefficient. We discuss a reduction algorithm by Xia which can be used to speed up the search for a fixed point free self-map. The ideas used in creating this algorithm show close connections to two problems: the decision whether an ordered set has a fixed point free automorphism and the decision whether a given r-partite graph has an r-clique. The latter two problems are shown to be NP-complete using the work of Goddard, Lubiw and Williamson. The problem to decide whether a given finite ordered set has a fixed point free order-preserving self-map has recently been shown to be NP-complete, thus showing that the above close connection is not by accident.Retraction theorems leading to dismantling algorithms are another approach to the problem. We present the classical dismantling procedure by Rival and extensions by Fofanova, Li, Milner, Rutkowski and the author. These theorems give a polynomial algorithm to decide if an ordered set has the fixed point property for some nice classes of ordered sets (height 1, width 2), and structural insights for other classes (chain-complete ordered sets with no infinite antichains, sets of (interval) dimension 2). The related issue of uniqueness of cores gives an insight into Birkhoff's problem regarding cancellation of exponents. Walker's relational fixed point property for which the analogous problem has a very satisfying solution also is discussed.Another variation on the retraction theme is the use of algebraic topology in deriving fixed point theorems initiated by Baclawski and Björner and continued for example by Constantin and Fournier. After a primer on the basic concepts of (integer) homology we present their retraction/dismantling procedures, which always prove acyclicity of the associated simplicial complex and then the fixed point property via a Lefschetz-type fixed point theorem. Differences and similarities with the above combinatorial procedures are pointed out. The main problem in making these results accessible to entirely combinatorial proofs is the lack of a combinatorial/discrete analogue of the continuous concept of a weak (resp. deformation) retract. We also present a class of ordered sets without the fixed point property, such that all proper retracts have the fixed point property. This class is induced via triangulations of n-spheres. Finally, we include an indication how methods developed for work on the fixed point property can be used in other areas. For example, the arguments by Abian, Brown and Pelczar to prove that in a chain-complete ordered set existence of a point P with P ⩽ f(P) implies existence of a fixed point have recently found application to analysis in the work of Carl, Heikkilä, Lakhshmikantham and others.

Infinite behavior of nondeterministic finite-state automata running over infinite trees or more generally over elements of an arbitrary algebraic structure is characterized by a calculus of fixed point terms interpreted in powerset algebras. These terms involve the least and greatest fixed point operators and disjunction as the only logical operation. A tight correspondence is established between a hierarchy of Rabin indices of automata and a hierarchy induced by alternation of the least and greatest fixed point operators. It is shown that, in the powerset algebra of trees constructed from a set of functional symbols, the fixed point hierarchy is infinite unless all the symbols are unary (i.e. trees are words). It is also shown that an interpretation of a closed fixed point term in any powerset algebra can be factorized through the interpretation of this term in the powerset algebra of trees, from which it is deduced that the question whether a term denotes always ∅ can be answered in polynomial time.

The greatest fixed point of a set functor is proved to be (a) a metric completion and (b) a CPO-completion of finite iterations. For each (possibly infinitary) signature Σ the terminal Σ-coalgebra is thus proved to be the coalgebra of all Σ-labelled trees; this is the completion of the set of all such trees of finite depth. A set functor is presented which has a fixed point but does not have a greatest fixed point. A sufficient condition for the existence of a greatest fixed point is proved: the existence of two fixed points of successor cardinalities.

We discuss the temporal logic “USF”, involving Until, Since and the fixed point operator ϑ of Gabbay, with semantics over the natural numbers. We show that any formula not involving Until is equivalent to one without nested fixed point operators. We then prove that USF has expressive power matching that of the monadic second-order logic S1S. The proof shows that any USF-formula is equivalent to one with at most two nested fixed point operators — i.e., no branch of its formation tree has more than two ϑ's. We then axiomatise USF and prove that it is decidable, with PSPACE-complete satisfiability problem. Finally, we discuss an application of these results to the executable temporal logic system “MetateM”.

Simpson, A.K., A characterisation of the least-fixed-point operator by dinaturality, Theoretical Computer Science 118 (1993) 301-314. The paper addresses the question of when the least-fixed-point operator, in a Cartesian-closed category of domains, is characterised as the unique dinatural transformation from the exponentiation bifunctor to the identity functor. We give a sufficient condition on a Cartesian-closed full subcategory of the category of algebraic cpos for the characterisation to hold. The condition is quite mild, and the least-fixed-point operator is so characterised in many of the most commonly used categories of domains. By using retractions, the characterisation extends to the associated cartesianclosed categories of continuous cpos. However, dinaturality does not always characterise the leastfixed-point operator. We show that in Cartesian-closed full subcategories of the category of continuous lattices the characterisation fails.

The author develops a theory of disjunctive logic programming, with negations allowed to appear both in the head of a clause and in the body. As such programs can easily contain inconsistent information (with respect to the intuitions of two-valued logic), this means that the formalism allows reasoning about systems that are intuitively inconsistent but yet have models (in nonclassical model theory). Such an ability is important because inconsistencies may occur very easily during the design and development of deductive databases and/or expert systems. The author also develops a theory of disjunctive deductive databases that (perhaps) contain inconsistent information. The author shows how to associate, with any such database, an operator that maps multivalued-model states to multivalued-model states. It is shown that this operator has a least fixed point which is identical to the set of all variable-free disjunctions that are provable from the database under consideration. A procedure to answer queries to such databases is devised. Soundness and completeness results are proved. The techniques introduced are fairly general. However, the results are applicable to databases that are quantitative in nature. >

After a simple and convenient generalization of the notion of continuous functions and continuous lattices we answer the following question: when for a given element x of a complete lattice there is a least continuous function having x as a least fixed point? The minimal continuous functions having x as a least fixed point are characterized through a correspondence with maximal ascending sequences converging to x .

The aim of this paper is to compare two approaches to the semantics of programming languages: the least fixed point approach, and the unique fixed point approach. Briefly speaking, we investigate here the problem of existence of extensions of algebras with the unique fixed point property to ordered algebras with the least fixed point property, that preserve the fixed point solutions. We prove that such extensions always exist, the construction of a free extension is given. It is also shown that in some cases there is no ‘faithful’ extension, i.e. some elements of a carrier are always collapsed.

LCF is the logic of computable (read ‘continuous’) functionals, where continuity means the preservation of sups ⊔neωxn of ω-chains 〈x〉neω in ω-cpo's P with least element ⊥. Most important sups have the form μxf(x) = ⊔neωfn (⊥) and are given continuously by the least fixed point operator Y. Consequently, Scotts induction axiom (∀f)[R(f, ⊥)^ ∀x[R(f, x) → R(f, f(x))] → R (f, Yf)] is valid for certain relations R ⊆ [ P → P ] × P , such as those satisfying the condition (*): (∀f) {x:R(f, x)} is closed under ω-sups. Given a relation R, we ask whether the obviously sufficient condition (*) is also necessary for R to satisfy Scott's induction axiom. Our main result shows that (*) is not a necessary condition, even for sets X ⊆ P (where R(f, x) ↔ x e X). As a consequence of certain definability and effectiveness aspects of the main result, we also show that some rather interesting classes of ω-cpo's can be finitely axiomatized in the language of LCF.

Udgivelsesdato: February We propose a method to axiomatize by equations the least prefixed point of an order preserving function. We discuss its domain of application and show that the Boolean modal μ-calculus has a complete equational axiomatization. The method relies on the existence of a “closed structure” and its relationship to the equational axiomatization of Action Logic is made explicit. The implication operation of a closed structure is not monotonic in one of its variables; we show that the existence of such a term that does not preserve the order is an essential condition for defining by equations the least prefixed point. We stress the interplay between closed structures and fixed point operators by showing that the theory of Boolean modal μ-algebras is not a conservative extension of the theory of modal μ-algebras. The latter is shown to lack the finite model property.

Most studies of fixed points involve their existence or construction. Our interest is in their equational properties. We study certain equational properties of the fixed-point operation in computationally interesting cartesian closed categories. We prove that in most of the poset categories that have been used in semantics, the least fixed-point operation satisfies four identities we call the Conway identities. We show that if %plane1D;49E; 0 is a sub-ccc of any ccc %plane1D;49E; with a fixed-point operation satisfying these identities, then there is a simple normal form for the morphisms in the least sub-ccc of %plane1D;49E; containing %plane1D;49E; 0 closed under the fixed-point operation. In addition, the standard functional completeness theorem is extended to Conway ccc's.

The denotational semantics of a deterministic timed system can be described by a function F : (T → V) → (T → V) with T partially ordered. The semantics of a feedback loop then is usually defined by a special (unique) fixed point of F but it is not always obvious that such a fixed point exists. This paper proves that every function F in the very general class of strictly causal functions has a unique fixed point.

We provide a direct and modular translation from the temporal logics $CTL$, $ETL$, $FCTL$ ($CTL$ extended with the ability to express fairness) and the Modal $\mu$-calculus to Monadic inf-Datalog with built-in predicates. We call it inf-Datalog because the semantics we provide is a little different from the conventional Datalog least fixed point semantics, in that some recursive rules (corresponding to least fixed points) are allowed to unfold only finitely many times, whereas others (corresponding to greatest fixed points) are allowed to unfold infinitely many times. We characterize the fragments of Monadic inf-Datalog that have the same expressive power as Modal Logic (resp. $CTL$, alternation-free Modal $\mu$-calculus and Modal $\mu$-calculus). Our translation is interesting because it is direct and succinct. Moreover the fragments of Monadic inf-Datalog that we have exhibited have very simple syntactic characterizations as subsets of what we call Modal inf-Datalog programs.

Monadic least fixed point logic MLFP is a natural logic whose expressiveness lies between that of first-order logic FO and monadic second-order logic MSO. In this paper, we take a closer look at the expressive power of MLFP. Our results are: (1) MLFP can describe graph properties beyond any fixed level of the monadic second-order quantifier alternation hierarchy. (2) On strings with built-in addition, MLFP can describe at least all languages that belong to the linear time complexity class DLIN. (3) Settling the question whether addition-invariant MLFP = addition-invariant MSO on finite strings or, equivalently, settling the question whether MLFP = MSO on finite strings with addition would solve open problems in complexity theory: "=" would imply that PH = PTIME whereas "≠" would imply that DLIN ≠ LINH. Apart from this we give a self-contained proof of the previously known result that MLFP is strictly less expressive than MSO on the class of finite graphs.

In this paper we consider the complexity of some problems arising in a fixed point model of trust in large-scale distributed systems, based on the notion of trust structures introduced by Carbone, Nielsen and Sassone; a set of trust levels with two distinct partial orderings. In the trust model, a global trust state exists as the least fixed point of a collection of local policy functions of nodes in the network.We first show that it is possible to efficiently compute a single component of the global trust state using a simple, robust and totally asynchronous distributed algorithm. We complement this with a lower bound which shows that, if the policies are unrestricted then communication and time linear in the number of distinct trust levels is required in the worst case.We then consider the notion of distributed proof carrying requests previously introduced as a means of safely approximating the global trust state without computing its exact value. We present a new result that enables us to give a continuum of proof carrying protocols, the previously known protocol being one extreme of this. The theorem allows us to generate protocols that can prove all possible trust values (previously, it was only possible to prove trust values representing ‘not too much bad behaviour’). However, we show that such a general protocol may not be efficient — it is NP-hard to construct an approximately minimal size proof in our model, and in the worst case the nodes must communicate almost as much data as if they were to compute the global trust state from scratch. The implications of our negative results are that it may be necessary to restrict the policy language in order to efficiently implement a fixed point model of trust in a distributed network.