Search

We reconsider the theory of Thompson aggregators proposed by Marinacci and Montrucchio (Marinacci and Montrucchio, 2010). We prove the existence of a Least Fixed Point (LFP) solution to the Koopmans equation. It is a recursive utility function. Our proof turns on demonstrating the Koopmans operator is a Scott continuous function when its domain is an order bounded subset of a space of bounded functions defined on the commodity space. Kleene’s Fixed Point Theorem yields the construction of the LFP by an iterative procedure. We argue the LFP solution is the Koopmans equation’s principal solution. It is constructed by an iterative procedure requiring less information (according to an information ordering) than approximations for any other fixed point. Additional distinctions between the LFP and GFP (Greatest Fixed Point) are presented. A general selection criterion for multiple solutions for functional equations and recursive methods is proposed.

We show that one can approximate the least fixed point solution for a multivariate system of monotone probabilistic max(min) polynomial equations, referred to as maxPPSs (and minPPSs, respectively), in time polynomial in both the encoding size of the system of equations and in log(1/epsilon), where epsilon > 0 is the desired additive error bound of the solution. (The model of computation is the standard Turing machine model.) We establish this result using a generalization of Newton's method which applies to maxPPSs and minPPSs, even though the underlying functions are only piecewise-differentiable. This generalizes our recent work which provided a P-time algorithm for purely probabilistic PPSs. These equations form the Bellman optimality equations for several important classes of infinite-state Markov Decision Processes (MDPs). Thus, as a corollary, we obtain the first polynomial time algorithms for computing to within arbitrary desired precision the optimal value vector for several classes of infinite-state MDPs which arise as extensions of classic, and heavily studied, purely stochastic processes. These include both the problem of maximizing and mininizing the termination (extinction) probability of multi-type branching MDPs, stochastic context-free MDPs, and 1-exit Recursive MDPs. Furthermore, we also show that we can compute in P-time an epsilon-optimal policy for both maximizing and minimizing branching, context-free, and 1-exit-Recursive MDPs, for any given desired epsilon > 0. This is despite the fact that actually computing optimal strategies is Sqrt-Sum-hard and PosSLP-hard in this setting. We also derive, as an easy consequence of these results, an FNP upper bound on the complexity of computing the value (within arbitrary desired precision) of branching simple stochastic games (BSSGs).

We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula equations. We state and prove a fixed-point theorem for Horn formula equations which is based on expressing the fixed-point computation of a minimal model of a set of Horn clauses on the object level as a formula in first-order logic with a least fixed point operator. We describe several corollaries of this fixed-point theorem, in particular concerning the logical foundations of program verification, and sketch how to generalise it to incorporate abstract interpretations., In Proceedings HCVS 2021, arXiv:2109.03988

The paper suggests a general method for proving the fact whether a certain set is p-computable or not. The method is based on a polynomial analogue of the classical Gandy’s fixed point theorem. Classical Gandy’s theorem deals with the extension of a predicate through a special operator ΓΦ(x)Ω∗ and states that the smallest fixed point of this operator is a Σ-set. Our work uses a new type of operator which extends predicates so that the smallest fixed point remains a p-computable set. Moreover, if in the classical Gandy’s fixed point theorem, the special Σ-formula Φ(x¯) is used in the construction of the operator, then a new operator uses special generating families of formulas instead of a single formula. This work opens up broad prospects for the application of the polynomial analogue of Gandy’s theorem in the construction of new types of terms and formulas, in the construction of new data types and programs of polynomial computational complexity in Turing complete languages.

International audience; Relational concept analysis (RCA) extends formal concept analysis (FCA) by taking into account binary relations between formal contexts. It has been designed for inducing description logic TBoxes from ABoxes, but can be used more generally. It is especially useful when there exist circular dependencies between objects. In this case, it extracts a unique stable concept lattice family grounded on the initial formal contexts. However, other stable families may exist whose structure depends on the same relational context. These may be useful in applications that need to extract a richer structure than the minimal grounded one. This issue is first illustrated in a reduced version of RCA, which only retains the relational structure. We then redefine the semantics of RCA on this reduced version in terms of concept lattice families closed by a fixed-point operation induced by this relational structure. We show that these families admit a least and greatest fixed point and that the well-grounded RCA semantics is characterised by the least fixed point. We then study the structure of other fixed points and characterise the interesting lattices as the self-supported fixed points.

In this note the proof-theoretic ordinal of the well-ordering principle for the normal functions $$\mathsf {g}$$ on ordinals is shown to be equal to the least fixed point of $$\mathsf {g}$$ . Moreover corrections to the previous paper (Arai in Arch Math Log 57:649–664, 2017) are made.

A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives rise to the coinduction principle, which states that two bisimilar elements are equal. For polynomial functors, this leads to well-known descriptions. In the present paper we look at the dual notion of "apartness". Intuitively, two elements are apart if there is a positive way to distinguish them. Phrased differently: two elements are apart if and only if they are not bisimilar. Since apartness is an inductive notion, described by a least fixed point, we can give a proof system, to derive that two elements are apart. This proof system has derivation rules and two elements are apart if and only if there is a finite derivation (using the rules) of this fact. We study apartness versus bisimulation in two separate ways. First, for weak forms of bisimulation on labelled transition systems, where silent (tau) steps are included, we define an apartness notion that corresponds to weak bisimulation and another apartness that corresponds to branching bisimulation. The rules for apartness can be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them. Next, we also study the more general categorical situation and show that indeed, apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In this analogy, we include the powerset functor, which gives a semantics to non-deterministic choice in process-theory.

We introduce the notion of a lexicographic lattice structure, namely a lattice whose elements can be viewed as stratified entities and whose ordering relation compares elements in a lexicographic manner with respect to their strata. These lattices arise naturally in many non-monotonic formalisms, such as normal logic programs, higher-order logic programs with negation, and boolean grammars. We consider functions over such lattices that may overall be non-monotonic, but retain a restricted form of monotonicity inside each stratum. We demonstrate that such functions always have a least fixed point which is also their least pre-fixed point. Moreover, we prove that the sets of pre-fixed and post-fixed points of such functions, are complete lattices. For the special case of a trivial lexicographic lattice structure whose elements essentially consist of a unique stratum, our theorem gives as a special case the well-known Knaster-Tarski fixed point theorem. Moreover, our work considerably simplifies and extends recent results on non-monotonic fixed point theory, providing in this way a useful and convenient tool in the semantic investigation of non-monotonic formalisms.

This paper shows how enhancing the representation, while fixing the logical power of computation, provides a better characterization of the computationally complex tone processes, the unbounded circumembient (UC) processes noted in Jardine (2016). Using Autosegmental Representations, we define tone-TBU associations as quantifier-free least fixed point transductions, which allow us to extend the notion of subsequentiality to the otherwise non subsequential UC processes.

International audience; We verify the partial correctness of a "local generic solver", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separation logic. The specification is simple: the solver computes the optimal least fixed point of a system of monotone equations. Although the solver relies on mutable internal state for memoization and for "spying", a form of dynamic dependency discovery, it is apparently pure: no side effects are mentioned in its specification. As auxiliary contributions, we provide several illustrations of the use of prophecy variables, a novel feature of Iris; we establish a restricted form of the infinitary conjunction rule; and we provide a specification and proof of Longley's modulus function, an archetypical example of spying.

In Hannes Leitgeb’s article What truth depends on (Leitgeb in J Philos Logic 34:155–192, 2005) the author provides a formally correct and materially adequate truth definition for the set of all grounded sentences, defined as the least fixed point of a monotone operator of semantic dependence. In this paper we will focus on the mathematical aspects of Leitgeb’s notions of dependence, grounding and truth, recasting Leitgeb’s construction in a functional setting in which we establish some new facts about these notions.

The paper is concerned with a line of research that plumbs the scope of constructive theories. The object of investigation here is Feferman’s intuitionistic theory of explicit mathematics augmented by the monotone fixed point principle which asserts that every monotone operation on classifications (Feferman’s notion of set) possesses a least fixed point. To be more precise, the new axiom not merely postulates the existence of a least solution, but, by adjoining a newfunctional constant to the language, it is ensured that a fixed point is uniformly presentable as a function of the monotone operation. The strength of the classical non-uniform version, MID, was investigated in [6] whereas that of the uniform version was determined in [16, 17] and shown to be that of subsystems of second order arithmetic based on \( \varPi_{2}^{1} \)-comprehension. This involved a rendering of \( \varPi_{2}^{1} \)-comprehension in terms of fixed points of non-monotonic \( \varPi_{1}^{1} \)-operators and a proof-theoretic interpretation of the latter in specific operator theories that can be interpreted in explicit mathematics with the uniform monotone fixed point principle. The intent of the current paper is to show that the same strength obtains when the underlying logic is taken to be intuitionistic logic.

In this paper, we study common fixed point properties for a family of mappings. We present the extensions of Caristi's fixed point theorem and Markov–Kakutani fixed point theorem for a family of set-valued mappings.

The fact that every combinator has a fixed point is at the heart of the λ -calculus as a model of computation. We consider several aspects of such phenomenon; our specific, perhaps eccentric, point of view focuses on problems and results that we consider worthy of further investigations. We first consider the relation with self application, in comparison with the opposite view, which stresses the role of coding, unifying the first and the second fixed point theorems. Then, we consider the relation with the diagonal argument, a relation which is at the origin of the fixed point theorem itself. We also review the Recursion Theorem, which is considered a recursion theoretic version of the fixed point theorem. We end considering systems of equations which are related to fixed points.

In this work, we introduce new concepts of G-monotone sequences, G-bounded and Gτ-compact nonempty subsets of the set of vertices of a weighted digraph G, where τ is a sequential convergence. We also provide an application to metric fixed point theory.

The purpose of this paper is to give some fixed point results for mappings involving generalized $$(\psi ,\varphi )$$ -contractions via rational expressions in the setup of partially ordered b-metric spaces. Our main results extend, generalize and enrich several well known comparable results in the recent literature. Moreover, some examples and an application to integral equation are given here to illustrate the usability of the obtained results.

We first prove one of the most basic inequalities on a b-metric space. And then we prove some fixed point theorems. We also consider two similar conditions; one implies the Cauchyness on sequences but the other does not.

[EN] We introduce and study a general concept of multiple fixed point for mappings defined on partially ordered distance spaces in the presence of a contraction type condition and appropriate monotonicity properties. This notion and the obtained results complement the corresponding ones from [M. Choban, V. Berinde, A general concept of multiple fixed point for mappings defined on spaces with a distance, Carpathian J. Math. 33 (2017), no. 3, 275--286] and also simplifies some concepts of multiple fixed point considered by various authors in the last decade or so., This second author acknowledges the support provided by the Deanship of Scientific Research at King Fahd University of Petroleum and Minerals for funding this work through the projects IN151014 and IN141047.

In 1970, a qualitative xed point technique useful to model the recursive specications in denotational semantics was developed by means of the celebrated Kleene's xed point theorem. Later on, in 1994 and 1995, quantitative counterparts of the aforesaid technique, but now based on generalized versions of Banach fixed point theorem, were obtained in such a way that the spirit of Kleene's technique was preserved. These new techniques are able to provide a measure of the informa- tion content degree and this fact has constituted an advantage with respect to the qualitative techniques. The main purpose of this paper is to discern the relationship between the afore mentioned qualitative and quantitative fixed point techniques. In particular, we clarify what is the additional real contribution of the quantitative fixed point techniques with respect to the qualitative ones.Key words: Partial order, quasi-metric, partial metric, complete, fixed point, denotational semantics, algorithmic complexity, fixed point.

The aim of this paper is to present a fuzzification of Tarski's fixed point theorem without the assumption of transitivity. For this purpose a new structure – the so called L-complete propelattice, which generalizes complete lattices and completely lattice L-ordered sets, is introduced. Our results show that for L-fuzzy isotone maps on L-complete propelattices a variant of Tarski's fixed point theorem holds. Especially, the set of fixed points is nonempty and of a certain structure.

In 1970, D.S. Scott gave applications of Kleene’s fixed point theorem to describe the meaning of recursive denotational specifications in programming languages. Later on, in 1994, S.G. Matthews and, in 1995, M.P. Schellekens gave quantitative counterparts of the Kleene fixed point theorem which allowed to apply partial metric and quasi-metric fixed point techniques to denotational semantics and asymptotic complexity analysis of algorithms in the spirit of Scott. Recently, in 2005, J.J. Nieto and R. Rodríguez-López made an in-depth study of how to reconcile order-theoretic and metric fixed point techniques in the classical metric case with the aim of providing the existence and uniqueness of solutions to first-order differential equations admitting only the existence of a lower solution. Motivated by the aforesaid fixed point results we prove a partial quasi-metric version, when the specialization order is under consideration, of the fixed point results of Nieto and Rodríguez-López in such a way that the results of Matthews and Schellekens can be retrieved as a particular case.

We show that a discrete fixed point result of Jachymski (Fixed Point Theory Appl 1:31–36, 2004) is equivalent to the classical Banach contraction mapping principle.

In this work, we generalize the classical fixed-point logics using relations instead of operators in order to capture the notion of nondeterminism. The basic idea is that we use loops in a relation instead of fixed-points of a function, that is, X is a fixed-point of the relation R in case the pair (X,X) belongs to R . We introduce the notion of initial fixed-point of an inflationary relation R and the associated operator rifp. We denote by RIFP the first-order logic with the inflationary relational fixed-point operator rifp and show that it captures the polynomial hierarchy using a translation to second-order logic. We also consider the fragment RIFP1 with the restriction that the rifp operator can be applied at most once. We show that RIFP1 captures the class NP and compare our logic with the nondeterministic fixed-point logic proposed by Abiteboul, Vianu and Vardi in [S. Abiteboul, M. Vardi, and V. Vianu. Fixpoint logics, relational machines, and computational complexity. Journal of the ACM, 44-1:30–56, 1997].

Recently, Wardowski (Fixed Point Theory Appl. 2012:94, 2012) introduced a new concept of F-contraction and proved a fixed point theorem which generalizes the Banach contraction principle. Following this direction of research, in this paper, we present some new fixed point results for F-expanding mappings, especially on a complete G-metric space.

The split common fixed-point problem is an inverse problem that consists in finding an element in a fixed-point set such that its image under a linear transformation belongs to another fixed-point set. In this paper, we propose a new algorithm for the split common fixed-point problem that does not need any priori information of the operator norm. Under standard assumptions, we establish a weak convergence theorem of the proposed algorithm.

A set of sufficient conditions which guarantee the existence of a point x⋆ such that f(x⋆) = x⋆ is called a "fixed point theorem". Possibly hundreds of such theorems exist in the literature. About twenty of them are explicitly mentioned in Wikipedia where they are named after well-known mathematicians and economists. Fixed point theorems are among most useful ones in applied mathematics, especially in economics and game theory. Particularly important theorem in these areas is Kakutani's fixed point theorem which ensures existence of fixed point for point-to-set mappings, e.g., [2, 3, 4]. John Nash developed and applied Kakutani's ideas to prove the existence of (what became known as)"Nash equilibrium" for finite games with mixed strategies for any number of players. This work earned him a Nobel Prize in Economics that he shared with two mathematicians. Nash's life was dramatized in the movie "Beautiful Mind" in 2001. In this paper, we approach the system f(x) = x differently. Instead of studying existence of its solutions our objective is to determine conditions which are both necessary and sufficient that an arbitrary point x⋆ is a fixed point, i.e., that it satises f(x⋆) = x⋆. The existence of solutions for continuous function f of the single variable is easy to establish using the Intermediate Value Theorem of Calculus. However, characterizing fixed points x⋆, i.e., providing answers to the question of finding both necessary and sufficient conditions for an arbitrary given x⋆ to satisfy f(x⋆) = x⋆, is not simple even for functions of the single variable. It is possible that constructive answers do not exist. Our objective is to find them. Our work may require some less familiar tools. One of these might be the "quadratic envelope characterization of zero-derivative point" recalled in the next section. The results are taken from the author's current Research project "Studying the Essence of Fixed Points". They are believed to be original. The author has received several feedbacks on the preliminary report and on parts of the project which can be seen on Internet [9].

The theory of countable partially ordered sets (posets) is developed within a weak subsystem of second order arithmetic. We within $$\mathsf {RCA_0}$$RCA0 give definitions of notions of the countable order theory and present some statements of countable lattices equivalent to arithmetical comprehension axiom over $$\mathsf {RCA_0}$$RCA0. Then we within $$\mathsf {RCA_0}$$RCA0 give proofs of Knaster---Tarski fixed point theorem, Tarski---Kantorovitch fixed point theorem, Bourbaki---Witt fixed point theorem, and Abian---Brown maximal fixed point theorem for countable lattices or posets. We also give Reverse Mathematics results of the fixed point theory of countable posets; Abian---Brown least fixed point theorem, Davis' converse for countable lattices, Markowski's converse for countable posets, and arithmetical comprehension axiom are pairwise equivalent over $$\mathsf {RCA_0}$$RCA0. Here the converses state that some fixed point properties characterize the completeness of the underlying spaces.

The split common fixed point problem is an inverse problem that consists in finding an element in a fixed point set such that its image under a bounded linear operator belongs to another fixed-point set. In this paper, we propose a new algorithm for this problem that is completely different from the existing algorithms. Moreover, our algorithm does not need any prior information of the operator norm. Under standard assumptions, we establish a weak convergence theorem of the proposed algorithm and a strong convergence theorem of its variant.

Co-design problems in the field of robotics involve the tradeoff of “resources” usage, such as cost, execution time, and energy, with mission performance, under recursive constraints that involve energetics, mechanics, computation, and communication. This letter shows that a large class of codesign problems have a common structure, as they are described by two posets, representing functionality, and resources. The codesign constraints can be expressed as two maps in opposite directions between the two posets. Finding the most resource-economical feasible solution is equivalent to finding the least fixed point of the composition of those two maps. If the two maps are monotone, results from order theory allow concluding uniqueness and systematically deriving an optimal design or a certificate for infeasibility.

We show that one can approximate the least fixed point solution for a multivariate system of monotone probabilistic polynomial equations in time polynomial in both the encoding size of the system of equations and in log(1=), where > 0 is the desired additive error bound of the solution. (The model of computation is the standard Turing machine model.) We use this result to resolve several open problems regarding the computational complexity of computing key quantities associated with some classic and well studied stochastic processes, including multi-type branching processes and stochastic context-free grammars.

In this paper, we present some triple fixed point theorems in partially ordered multiplicative metric spaces depended on another function. Our results generalise the results of [6] and [5].

This paper offers a computational characterization of tone-to-TBU association processes using a restricted least-fixed point logic. Crucially, least fixed point logics allow recursive definitions which capture output-oriented processes. The added requirement that these definitions are quantifier-free ensures that they are inherently local, a restriction that is well-motivated for phonological processes in general. The typology developed here distinguishes between possible and impossible tone mappings, capturing a wider range of attested tone mappings (left-to-right, right-to-left, edge-in, quality-sensitive) than previous rule-based or optimization approaches, while also explaining why certain unattested mapping patterns (for example center-out association) are impossible. This thus represents a strong first approximation of a definition for output-based local functions over non-linear structures

The closure ordinal of a \(\mu \)-calculus formula \(\varphi (x)\) is the least ordinal \(\alpha \), if it exists, such that, in any model, the least fixed point of \(\varphi (x)\) can be computed in at most \(\alpha \) many steps, by iteration of the meaning function associated with \(\varphi (x)\), starting from the empty set. In this paper we focus on closure ordinals of the two-way modal \(\mu \)-calculus. Our main technical contribution is the construction of a two-way formula \(\varphi _n\) with closure ordinal \(\omega ^n\) for an arbitrary \(n\in \omega \). Building on this construction, as our main result we define a two-way formula \(\varphi _\alpha \) with closure ordinal \(\alpha \) for an arbitrary \(\alpha

The humble \(\dagger \) (“dagger”) is used to denote two different operations in category theory: Taking the adjoint of a morphism (in dagger categories) and finding the least fixed point of a functional (in categories enriched in domains). While these two operations are usually considered separately from one another, the emergence of reversible notions of computation shows the need to consider how the two ought to interact.

We extend Alternation-Free Least Fixed Point Logic to be based on Belnap logic, while maintaining the close correspondence between static analysis and model checking pioneered by Bernhard Steffen, and opening up for handling access control policies central to the construction of secure IT systems.