Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userThe Fixed-Point Theory of Strictly Contracting Functions on Generalized Ultrametric Semilattices
128
0
0.0
(
0
)
Added by
EPTCS
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We introduce a new class of abstract structures, which we call generalized ultrametric semilattices, and in which the meet operation of the semilattice coexists with a generalized distance function in a tightly coordinated way. We prove a constructive fixed-point theorem for strictly contracting functions on directed-complete generalized ultrametric semilattices, and introduce a corresponding induction principle. We cite examples of application in the semantics of logic programming and timed computation, where, until now, the only tool available has been the non-constructive fixed-point theorem of Priess-Crampe and Ribenboim for strictly contracting functions on spherically complete generalized ultrametric semilattices.
rate research
Read More
Graph polynomials which are definable in Monadic Second Order Logic (MSOL) on the vocabulary of graphs are Fixed-Parameter Tractable (FPT) with respect to clique-width. In contrast, graph polynomials which are definable in MSOL on the vocabulary of hypergraphs are fixed-parameter tractable with respect to tree-width, but not necessarily with respect to clique width. No algorithmic meta-theorem is known for the computation of graph polynomials definable in MSOL on the vocabulary of hypergraphs with respect to clique-width. We define an infinite class of such graph polynomials extending the class of graph polynomials definable in MSOL on the vocabulary of graphs and prove that they are Fixed-Parameter Polynomial Time (FPPT) computable, i.e. that they can be computed in time $O(n^{f(k)})$, where $n$ is the number of vertices and $k$ is the clique-width.
Implementations of artificial neural networks (ANNs) might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are barely interpretable. Here, we develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference, to obtain adversarial cases and validate coverage methods in a multi-layer perceptron (MLP). We exploit incremental BMC based on interval analysis to compute boundaries from a neurons input. Then, the latter are propagated to effectively find a neurons output since it is the input of the next one. This paper describes the first bit-precise symbolic verification framework to reason over actual implementations of ANNs in CUDA, based on invariant inference, therefore providing further guarantees about finite-precision arithmetic and its rounding errors, which are routinely ignored in the existing literature. We have implemented the proposed approach on top of the efficient SMT-based bounded model checker (ESBMC), and its experimental results show that it can successfully verify safety properties, in actual implementations of ANNs, and generate real adversarial cases in MLPs. Our approach was able to verify and produce adversarial examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods. Although our verification time is higher than existing approaches, our methodology can consider fixed-point implementation aspects that are disregarded by the state-of-the-art verification methodologies.
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.
We establish two fixed point theorems for certain mappings of contractive type. The first result is concerned with the case where such mappings take a nonempty, closed subset of a complete metric space $X$ into $X$, and the second with an application of the continuation method to the case where they satisfy the Leray-Schauder boundary condition in Banach spaces.
Let $D$ be a bounded domain in a complex Banach space. According to the Earle-Hamilton fixed point theorem, if a holomorphic mapping $F : D mapsto D$ maps $D$ strictly into itself, then it has a unique fixed point and its iterates converge to this fixed point locally uniformly. Now let $mathcal{B}$ be the open unit ball in a complex Hilbert space and let $F : mathcal{B} mapsto mathcal{B}$ be holomorphic. We show that a similar conclusion holds even if the image $F(mathcal{B})$ is not strictly inside $mathcal{B}$, but is contained in a horosphere internally tangent to the boundary of $mathcal{B}$. This geometric condition is equivalent to the fact that $F$ is asymptotically strongly nonexpansive with respect to the hyperbolic metric in $mathcal{B}$.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
