اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدRelation lifting, with an application to the many-valued cover modality
31
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the powerset monad on categories, one is the preservation by T of exactness of certain squares. Both characterisations are generalisations of the classical results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.
قيم البحث
اقرأ أيضاً
We revisit two well-established verification techniques, $k$-induction and bounded model checking (BMC), in the more general setting of fixed point theory over complete lattices. Our main theoretical contribution is latticed $k$-induction, which (i)
generalizes classical $k$-induction for verifying transition systems, (ii) generalizes Park induction for bounding fixed points of monotonic maps on complete lattices, and (iii) extends from naturals $k$ to transfinite ordinals $kappa$, thus yielding $kappa$-induction. The lattice-theoretic understanding of $k$-induction and BMC enables us to apply both techniques to the fully automatic verification of infinite-state probabilistic programs. Our prototypical implementation manages to automatically verify non-trivial specifications for probabilistic programs taken from the literature that - using existing techniques - cannot be verified without synthesizing a stronger inductive invariant first.
Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete
implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.
This paper shows how to transform explosive many-valued systems into paraconsistent logics. We investigate especially the case of three-valued systems showing how paraconsistent three-valued logics can be obtained from them.
We develop a categorical compositional distributional semantics for Lambek Calculus with a Relevant Modality, which has a limited version of the contraction and permutation rules. The categorical part of the semantics is a monoidal biclosed category
with a coalgebra modality as defined on Differential Categories. We instantiate this category to finite dimensional vector spaces and linear maps via quantisation functors and work with three concrete interpretations of the coalgebra modality. We apply the model to construct categorical and concrete semantic interpretations for the motivating example of this extended calculus: the derivation of a phrase with a parasitic gap. The effectiveness of the concrete interpretations are evaluated via a disambiguation task, on an extension of a sentence disambiguation dataset to parasitic gap phrases, using BERT, Word2Vec, and FastText vectors and Relational tensors
The logics RL, RP, and RG have been obtained by expanding Lukasiewicz logic L, product logic P, and Godel--Dummett logic G with rational constants. We study the lattices of extensions and structural completeness of these three expansions, obtaining r
esults that stand in contrast to the known situation in L, P, and G. Namely, RL is hereditarily structurally complete. RP is algebraized by the variety of rational product algebras that we show to be Q-universal. We provide a base of admissible rules in RP, show their decidability, and characterize passive structural completeness for extensions of RP. Furthermore, structural completeness, hereditary structural completeness, and active structural completeness coincide for extensions of RP, and this is also the case for extensions of RG, where in turn passive structural completeness is characterized by the equivalent algebraic semantics having the joint embedding property. For nontrivial axiomatic extensions of RG we provide a base of admissible rules. We leave the problem open whether the variety of rational Godel algebras is Q-universal.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
