Статті в журналах з теми "Complete equational theories"
Щоб переглянути інші типи публікацій з цієї теми, перейдіть за посиланням: Complete equational theories.
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Ознайомтеся з топ-19 статей у журналах для дослідження на тему "Complete equational theories".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Переглядайте статті в журналах для різних дисциплін та оформлюйте правильно вашу бібліографію.
1
Hölldobler, Steffen. "Conditional equational theories and complete sets of transformations." Theoretical Computer Science 75, no. 1-2 (1990): 85–110. http://dx.doi.org/10.1016/0304-3975(90)90063-n.
2
Cerna, David M., and Temur Kutsia. "Higher-order pattern generalization modulo equational theories." Mathematical Structures in Computer Science 30, no. 6 (May 20, 2020): 627–63. http://dx.doi.org/10.1017/s0960129520000110.
Анотація:
AbstractWe consider anti-unification for simply typed lambda terms in theories defined by associativity, commutativity, identity (unit element) axioms and their combinations and develop a sound and complete algorithm which takes two lambda terms and computes their equational generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of such generalizations contains finitely many elements. We define the notion of optimal solution and investigate special restrictions of the problem for which the optimal solution can be computed in linear or polynomial time.
3
Fages, François, and Gérard Huet. "Complete sets of unifiers and matchers in equational theories." Theoretical Computer Science 43 (1986): 189–200. http://dx.doi.org/10.1016/0304-3975(86)90175-1.
4
ÉSIK, Z. "THE POWER OF THE GROUP-IDENTITIES FOR ITERATION." International Journal of Algebra and Computation 10, no. 03 (June 2000): 349–73. http://dx.doi.org/10.1142/s0218196700000145.
Анотація:
It has been shown that the axioms of iteration theories capture the equational properties of iteration in several different models related to computer science. Iteration theories are axiomatizable by the Conway identities and the group-identities corresponding to the finite (simple) groups. In this paper we provide a complete analysis of these identities by giving a concrete description of the free theories in the variety axiomatized by the Conway identities and any given subcollection of the group-identities. It follows that when the group-identities are effectively given, the equational theory of the variety is decidable.
5
Ésik, Z. "Equational properties of fixed-point operations in cartesian categories: An overview." Mathematical Structures in Computer Science 29, no. 06 (May 24, 2019): 909–25. http://dx.doi.org/10.1017/s0960129518000361.
Анотація:
AbstractSeveral fixed-point models share the equational properties of iteration theories, or iteration categories, which are cartesian categories equipped with a fixed point or dagger operation subject to certain axioms. After discussing some of the basic models, we provide equational bases for iteration categories and offer an analysis of the axioms. Although iteration categories have no finite base for their identities, there exist finitely based implicational theories that capture their equational theory. We exhibit several such systems. Then we enrich iteration categories with an additive structure and exhibit interesting cases where the interaction between the iteration category structure and the additive structure can be captured by a finite number of identities. This includes the iteration category of monotonic or continuous functions over complete lattices equipped with the least fixed-point operation and the binary supremum operation as addition, the categories of simulation, bisimulation, or language equivalence classes of processes, context-free languages, and others. Finally, we exhibit a finite equational system involving residuals, which is sound and complete for monotonic or continuous functions over complete lattices in the sense that it proves all of their identities involving the operations and constants of cartesian categories, the least fixed-point operation and binary supremum, but not involving residuals.
6
Amy, Matthew. "Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes." Electronic Proceedings in Theoretical Computer Science 384 (August 23, 2023): 127–41. http://dx.doi.org/10.4204/eptcs.384.8.
7
Mordido, Andreia, and Carlos Caleiro. "Probabilistic logic over equations and domain restrictions." Mathematical Structures in Computer Science 29, no. 06 (March 8, 2019): 872–95. http://dx.doi.org/10.1017/s096012951800035x.
Анотація:
AbstractWe propose and study a probabilistic logic over an algebraic basis, including equations and domain restrictions. The logic combines aspects from classical logic and equational logic with an exogenous approach to quantitative probabilistic reasoning. We present a sound and weakly complete axiomatization for the logic, parameterized by an equational specification of the algebraic basis coupled with the intended domain restrictions.We show that the satisfiability problem for the logic is decidable, under the assumption that its algebraic basis is given by means of a convergent rewriting system, and, additionally, that the axiomatization of domain restrictions enjoys a suitable subterm property. For this purpose, we provide a polynomial reduction to Satisfiability Modulo Theories. As a consequence, we get that validity in the logic is also decidable. Furthermore, under the assumption that the rewriting system that defines the equational basis underlying the logic is also subterm convergent, we show that the resulting satisfiability problem is NP-complete, and thus the validity problem is coNP-complete.We test the logic with meaningful examples in information security, namely by verifying and estimating the probability of the existence of offline guessing attacks to cryptographic protocols.
8
ÉSIK, ZOLTÁN. "Equational axioms associated with finite automata for fixed point operations in cartesian categories." Mathematical Structures in Computer Science 27, no. 1 (April 8, 2015): 54–69. http://dx.doi.org/10.1017/s0960129515000031.
Анотація:
The axioms of iteration theories, or iteration categories, capture the equational properties of fixed point operations in several computationally significant categories. Iteration categories may be axiomatized by the Conway identities and identities associated with finite automata. We show that the Conway identities and the identities associated with the members of a subclass $\mathcal{Q}$ of finite automata is complete for iteration categories iff for every finite simple group G there is an automaton Q ∈ $\mathcal{Q}$ such that G is a quotient of a group in the monoid M(Q) of the automaton Q. We also prove a stronger result that concerns identities associated with finite automata with a distinguished initial state.
9
Aguirre, Alejandro, and Lars Birkedal. "Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice." Proceedings of the ACM on Programming Languages 7, POPL (January 9, 2023): 33–60. http://dx.doi.org/10.1145/3571195.
Анотація:
Developing denotational models for higher-order languages that combine probabilistic and nondeterministic choice is known to be very challenging. In this paper, we propose an alternative approach based on operational techniques. We study a higher-order language combining parametric polymorphism, recursive types, discrete probabilistic choice and countable nondeterminism. We define probabilistic generalizations of may- and must-termination as the optimal and pessimal probabilities of termination. Then we define step-indexed logical relations and show that they are sound and complete with respect to the induced contextual preorders. For may-equivalence we use step-indexing over the natural numbers whereas for must-equivalence we index over the countable ordinals. We then show than the probabilities of may- and must-termination coincide with the maximal and minimal probabilities of termination under all schedulers. Finally we derive the equational theory induced by contextual equivalence and show that it validates the distributive combination of the algebraic theories for probabilistic and nondeterministic choice.
10
Carette, Titouan, Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. "Completeness of Graphical Languages for Mixed State Quantum Mechanics." ACM Transactions on Quantum Computing 2, no. 4 (December 31, 2021): 1–28. http://dx.doi.org/10.1145/3464693.
Анотація:
There exist several graphical languages for quantum information processing, like quantum circuits, ZX-calculus, ZW-calculus, and so on. Each of these languages forms a †-symmetric monoidal category (†-SMC) and comes with an interpretation functor to the †-SMC of finite-dimensional Hilbert spaces. In recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of how to extend these languages beyond pure quantum mechanics to reason about mixed states and general quantum operations, i.e., completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map that allows one to get rid of a quantum system, an operation that is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction , which transforms any †-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction, we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However, this construction fails for some fringe cases like Clifford+T quantum mechanics, as the category does not have enough isometries.
11
Choudhury, Vikraman, Jacek Karwowski, and Amr Sabry. "Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages." Proceedings of the ACM on Programming Languages 6, POPL (January 16, 2022): 1–32. http://dx.doi.org/10.1145/3498667.
Анотація:
The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections. Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.
12
Alfanur, Farah, and Yasuo Kadono. "EMPIRICAL STUDY OF PURCHASE INTENTION AND BEHAVIOR OF E-COMMERCE CONSUMERS IN INDONESIA." MALAYSIAN E COMMERCE JOURNAL 5, no. 1 (November 16, 2021): 20–28. http://dx.doi.org/10.26480/mecj.01.2021.20.28.
Анотація:
E-commerce in Indonesia is currently growing as consumers make an increasing number of online purchases, making the competition fiercer between e-commerce business players in the country. Despite this growth, e-commerce in Indonesia faces challenges remaining to their development such as a gap in internet penetration between rural and urban areas. To win the competition among all e-commerce businesses and face the existing challenges, it is necessary to determine the best strategy to retain current consumers along with getting more and more consumers. Thus, this study aims to better understand the behavior of e-commerce consumers in Indonesia by developing a structural model of purchase intention and behavior based on an adaptation of the unified theory of acceptance and use of technology 2 (UTAUT2) model, with input from other relevant theories and interviews conducted in the country. Data from questionnaires completed by 400 e-commerce consumers are analyzed using covariance-based structural equational modeling (CB-SEM). The CB-SEM analysis finds that purchase intention is significantly influenced by these six factors: facilitating conditions, perceived website quality, security, convenience, economic reasons, and social influence. Furthermore, purchase intention significantly influences the purchase behavior of consumers. Conversely, three factors considered in the study are found not to significantly influence purchase intention: hedonic motivation, variety, and delivery factors. These results help e-commerce businesses to consider important factors when determining key factors influencing consumer purchase intentions and behavior.
13
Ikebuchi, Mirai. "A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods." Logical Methods in Computer Science Volume 18, Issue 3 (September 21, 2022). http://dx.doi.org/10.46298/lmcs-18(3:36)2022.
Анотація:
It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given equational theory (or term rewriting systems), using homological algebra. Their method is an analog of Squier's homology theory on string rewriting systems. In this paper, we develop the homology theory for term rewriting systems more and provide a better lower bound under a stronger notion of equivalence than their equivalence. The author also implemented a program to compute the lower bounds, and experimented with 64 complete TRSs.
14
Szabo, Peter, and Jörg Siekmann. "E-Unification based on Generalized Embedding." Mathematical Structures in Computer Science, March 24, 2022, 1–20. http://dx.doi.org/10.1017/s0960129522000019.
Анотація:
Abstract Ordering is a well-established concept in mathematics and also plays an important role in many areas of computer science, where quasi-orderings, most notably well-founded quasi-orderings and well-quasi-orderings, are of particular interest. This paper deals with quasi-orderings on first-order terms and introduces a new notion of unification based on a special quasi-order, known as homeomorphic tree embedding. Historically, the development of unification theory began with the central notion of a most general unifier based on the subsumption order. A unifier $\sigma$ is most general, if it subsumes any other unifier $\tau$ , that is, if there is a substitution $\lambda$ with $\tau=_{E}\sigma\lambda$ , where E is an equational theory and $=_{E}$ denotes equality under E. Since there is in general more than one most general unifier for unification problems under equational theories E, called E-Unification, we have the notion of a complete and minimal set of unifiers under E for a unification problem $\varGamma$ , denoted as $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ . This set is still the basic notion in unification theory today. But, unfortunately, the subsumption quasi-order is not a well-founded quasi-order, which is the reason why for certain equational theories there are solvable E-unification problems, but the set $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ does not exist. They are called type nullary in the unification hierarchy. In order to overcome this problem and also to substantially reduce the number of most general unifiers, we extended the well-known encompassment order on terms to an encompassment order on substitutions (modulo E). Unification under the encompassment order is called essential unification and if $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ exists, then the complete set of essential unifiers $e\mathcal{U}\Sigma_{E}(\Gamma)$ is a subset of $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ . An interesting effect is that many E-unification problems with an infinite set of most general unifiers (under the subsumption order) reduce to a problem with only finitely many essential unifiers. Moreover, there are cases of an equational theory E, for which the complete set of most general unifiers does not exist, the minimal and complete set of essential unifiers however does exist. Unfortunately again, the encompassment order is not a well-founded quasi-ordering either, that is, there are still theories with a solvable unification problem, for which a minimal and complete set of essential unifiers does not exist. This paper deals with a third approach, namely the extension of the well-known homeomorphic embedding of terms to a homeomorphic embedding of substitutions (modulo E). We examine the set of most general, minimal, and complete E-unifiers under the quasi-order of homeomorphic embedment modulo an equational theory E, called $\varphi U\Sigma_{E}(\Gamma)$ , and propose an appropriate definitional framework based on the standard notions of unification theory extended by notions for the tree embedding theorem or Kruskal’s theorem as it is called. The main results are that for regular theories the minimal and complete set $\varphi\mathcal{U}\Sigma_{E}(\Gamma)$ always exists. If we restrict the E-embedding order to pure E-embedding, a well-known technique in logic programming and term rewriting where the difference between variables is ignored, the set $\varphi_{\pi}\mathcal{U}\Sigma_{E}(\Gamma)$ always exists and it is even finite for any theory E.
15
AFFELDT, REYNALD, JACQUES GARRIGUE, DAVID NOWAK, and TAKAFUMI SAIKAWA. "A trustful monad for axiomatic reasoning with probability and nondeterminism." Journal of Functional Programming 31 (2021). http://dx.doi.org/10.1017/s0956796821000137.
Анотація:
Abstract The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a nontrivial interface, which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories, and that we integrate in a framework for monadic equational reasoning.
16
Ésik, Zoltán. "Continuous Additive Algebras and Injective Simulations of Synchronization Trees." BRICS Report Series 7, no. 25 (January 25, 2000). http://dx.doi.org/10.7146/brics.v7i25.20153.
Анотація:
<p>The (in)equational properties of the least fixed point operation on<br />(omega-)continuous functions on (omega-)complete partially ordered sets are<br />captured by the axioms of (ordered) iteration algebras, or iteration<br />theories. We show that the inequational laws of the sum operation in<br />conjunction with the least fixed point operation in continuous additive<br />algebras have a finite axiomatization over the inequations of ordered<br />iteration algebras. As a byproduct of this relative axiomatizability <br />result, we obtain complete infinite inequational and finite implicational<br />axiomatizations. Along the way of proving these results, we give a <br />concrete description of the free algebras in the corresponding variety of<br />ordered iteration algebras. This description uses injective simulations of <br />regular synchronization trees. Thus, our axioms are also sound and<br />complete for the injective simulation (resource bounded simulation) of<br />(regular) processes.</p><p><br />Keywords: equational logic, fixed points, synchronization trees, simulation.</p>
17
Dahlqvist, Fredrik, and Renato Neves. "The syntactic side of autonomous categories enriched over generalised metric spaces." Logical Methods in Computer Science Volume 19, Issue 4 (December 18, 2023). http://dx.doi.org/10.46298/lmcs-19(4:31)2023.
Анотація:
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear {\lambda}-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear {\lambda}-theories based on this V-equational system form a category that is equivalent to a category of autonomous categories enriched over 'generalised metric spaces'. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. We additionally show that this syntax-semantics correspondence extends to the affine setting. We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing.
18
Bacci, Giorgio, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. "Propositional Logics for the Lawvere Quantale." Electronic Notes in Theoretical Informatics and Computer Science Volume 3 - Proceedings of... (November 23, 2023). http://dx.doi.org/10.46298/entics.12292.
Анотація:
Lawvere showed that generalised metric spaces are categories enriched over $[0, \infty]$, the quantale of the positive extended reals. The statement of enrichment is a quantitative analogue of being a preorder. Towards seeking a logic for quantitative metric reasoning, we investigate three $[0,\infty]$-valued propositional logics over the Lawvere quantale. The basic logical connectives shared by all three logics are those that can be interpreted in any quantale, viz finite conjunctions and disjunctions, tensor (addition for the Lawvere quantale) and linear implication (here a truncated subtraction); to these we add, in turn, the constant $1$ to express integer values, and scalar multiplication by a non-negative real to express general affine combinations. Quantitative equational logic can be interpreted in the third logic if we allow inference systems instead of axiomatic systems. For each of these logics we develop a natural deduction system which we prove to be decidably complete w.r.t. the quantale-valued semantics. The heart of the completeness proof makes use of the Motzkin transposition theorem. Consistency is also decidable; the proof makes use of Fourier-Motzkin elimination of linear inequalities. Strong completeness does not hold in general, even (as is known) for theories over finitely-many propositional variables; indeed even an approximate form of strong completeness in the sense of Pavelka or Ben Yaacov -- provability up to arbitrary precision -- does not hold. However, we can show it for theories axiomatized by a (not necessarily finite) set of judgements in normal form over a finite set of propositional variables when we restrict to models that do not map variables to $\infty$; the proof uses Hurwicz's general form of the Farkas' Lemma.
19
Ésik, Zoltán, and Hans Leiß. "Greibach Normal Form in Algebraically Complete Semirings." BRICS Report Series 9, no. 46 (December 5, 2002). http://dx.doi.org/10.7146/brics.v9i46.21761.
Анотація:
We give inequational and equational axioms for semirings with a fixed-point operator and formally develop a fragment of the theory of context-free languages. In particular, we show that Greibach's normal form theorem depends only on a few equational properties of least pre-fixed-points in semirings, and elimination of chain- and deletion rules depend on their inequational properties (and the idempotency of addition). It follows that these normal form theorems also hold in non-continuous semirings having enough fixed-points.