اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدDeduction as Reduction
160
0
0.0
(
0
)
تأليف
Dominique Duval
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Deduction systems and graph rewriting systems are compared within a common categorical framework. This leads to an improved deduction method in diagrammatic logics.
قيم البحث
اقرأ أيضاً
In this short paper, using category theory, we argue that logical rules can be seen as fractions and logics as limit sketches.
We propose a categorical foundation for the connection between pure and mixed states in quantum information and quantum computation. The foundation is based on distributive monoidal categories. First, we prove that the category of all quantum chann
els is a canonical completion of the category of pure quantum operations (with ancilla preparations). More precisely, we prove that the category of completely positive trace-preserving maps between finite-dimensional C*-algebras is a canonical completion of the category of finite-dimensional vector spaces and isometries. Second, we extend our result to give a foundation to the topological relationships between quantum channels. We do this by generalizing our categorical foundation to the topologically-enriched setting. In particular, we show that the operator norm topology on quantum channels is the canonical topology induced by the norm topology on isometries.
In this paper we consider the two major computational effects of states and exceptions, from the point of view of diagrammatic logics. We get a surprising result: there exists a symmetry between these two effects, based on the well-known categorical
duality between products and coproducts. More precisely, the lookup and update operations for states are respectively dual to the throw and catch operations for exceptions. This symmetry is deeply hidden in the programming languages; in order to unveil it, we start from the monoidal equational logic and we add progressively the logical features which are necessary for dealing with either effect. This approach gives rise to a new point of view on states and exceptions, which bypasses the problems due to the non-algebraicity of handling exceptions.
In a deduction system with some propositions and some known relations among these propositions, people usually care about the minimum of propositions by which all other propositions can be deduced according to these known relations. Here we call it a
minimizing deduction system. Its common solution is the guess and determine method. In this paper we propose a method of solving the minimizing deduction system based on MILP. Firstly, we introduce the conceptions of state variable, path variable and state copy, which enable us to characterize all rules by inequalities. Then we reduce the deduction problem to a MILP problem and solve it by the Gurobi optimizer. As its applications, we analyze the security of two stream ciphers SNOW2.0 and Enocoro-128v2 in resistance to guess and determine attacks. For SNOW 2.0, it is surprising that it takes less than 0.1s to get the best solution of 9 known variables in a personal Macbook Air(Early 2015, Double Intel Core i5 1.6GHZ, 4GB DDR3). For Enocoro-128v2, we get the best solution of 18 known variables within 3 minutes. Whats more, we propose two improvements to reduce the number of variables and inequalities which significantly decrease the scale of the MILP problem.
In this paper we propose a complete axiomatization of the bisimilarity distance of Desharnais et al. for the class of finite labelled Markov chains. Our axiomatization is given in the style of a quantitative extension of equational logic recently pro
posed by Mardare, Panangaden, and Plotkin (LICS 2016) that uses equality relations $t equiv_varepsilon s$ indexed by rationals, expressing that `$t$ is approximately equal to $s$ up to an error $varepsilon$. Notably, our quantitative deduction system extends in a natural way the equational system for probabilistic bisimilarity given by Stark and Smolka by introducing an axiom for dealing with the Kantorovich distance between probability distributions. The axiomatization is then used to propose a metric extension of a Kleenes style representation theorem for finite labelled Markov chains, that was proposed (in a more general coalgebraic fashion) by Silva et al. (Inf. Comput. 2011).
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
