Quasi-decompositions and quasidirect products of Hilbert algebras

A quasi-decomposition of a Hilbert algebra A is a pair (C, D) of its subalgebras such that (i) every element a ∈ A is a meet c ∧ d with c ∈ C, d ∈ D, where c and d are compatible (i.e., c → d = c → (c ∧ d)), and (ii) d → c = c (then c is uniquely defined). Quasi-decompositions are intimately related to the so-called triple construction of Hilbert algebras, which we reinterpret as a construction of quasidirect products. We show that it can be viewed as a generalization of the semidirect product construction, that quasidirect products has a certain universal property and that they can be characterised in terms of short exact sequences. We also discuss four classes of Hilbert algebras and give for each of them conditions on a quasi-decomposition of an arbitrary Hilbert algebra A under which A belongs to this class.

$$H^1$$-conforming finite element cochain complexes and commuting quasi-interpolation operators on Cartesian meshes

A finite element cochain complex on Cartesian meshes of any dimension based on the $$H^1$$ H 1 -inner product is introduced. It yields $$H^1$$ H 1 -conforming finite element spaces with exterior derivatives in $$H^1$$ H 1 . We use a tensor product construction to obtain $$L^2$$ L 2 -stable projectors into these spaces which commute with the exterior derivative. The finite element complex is generalized to a family of arbitrary order.

Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security

Most existing program verifiers check trace properties such as functional correctness, but do not support the verification of hyperproperties, in particular, information flow security. In principle, product programs allow one to reduce the verification of hyperproperties to trace properties and, thus, apply standard verifiers to check them; in practice, product constructions are usually defined only for simple programming languages without features like dynamic method binding or concurrency and, consequently, cannot be directly applied to verify information flow security in a full-fledged language. However, many existing verifiers encode programs from source languages into simple intermediate verification languages, which opens up the possibility of constructing a product program on the intermediate language level, reusing the existing encoding and drastically reducing the effort required to develop new verification tools for information flow security. In this paper, we explore the potential of this approach along three dimensions: (1) Soundness: We show that the combination of an encoding and a product construction that are individually sound can still be unsound, and identify a novel condition on the encoding that ensures overall soundness. (2) Concurrency: We show how sequential product programs on the intermediate language level can be used to verify information flow security of concurrent source programs. (3) Performance: We implement a product construction in Nagini, a Python verifier built upon the Viper intermediate language, and evaluate it on a number of challenging examples. We show that the resulting tool offers acceptable performance, while matching or surpassing existing tools in its combination of language feature support and expressiveness.

The Hahn Embedding Theorem for a Class of Residuated Semigroups

Hahn’s embedding theorem asserts that linearly ordered abelian groups embed in some lexicographic product of real groups. Hahn’s theorem is generalized to a class of residuated semigroups in this paper, namely, to odd involutive commutative residuated chains which possess only finitely many idempotent elements. To this end, the partial lexicographic product construction is introduced to construct new odd involutive commutative residuated lattices from a pair of odd involutive commutative residuated lattices, and a representation theorem for odd involutive commutative residuated chains which possess only finitely many idempotent elements, by means of linearly ordered abelian groups and the partial lexicographic product construction is presented.

SIMBOLIKHAJI: Studi Deskriptif Analitik pada Orang Bugis

<p>As stated by Berger, Hajj as religious practice is attached to cultural<br />context and meaning dialecticism. The difference of hajj symbol as cultural<br />product construction from others laid on its transcendence and its<br />religious dimension. Its cultural meaning has also changed overtime.<br />This change can be looked on the newly hajj interpretation which has<br />deviated from its true meaning written in Islamic texts, and implicated<br />to the current Buginese community social and cultural practice and<br />inter relation. As the symbol of hajj relatively attached more to the female<br />hajj, the number of female hajj, as its implication, is more higher<br />than male hajj.</p>

Growth series of crossed and two-sided crossed products of cyclic groups

We recall that the two-sided crossed product of finite cyclic groups is actually a generalization of the crossed product construction of the same type of groups (cf. [10]). In this paper, by considering the crossed and two-sided crossed products obtained from both finite and infinite cyclic groups, we first present the complete rewriting systems and normal forms of elements over crossed products. (We should note that the complete rewriting systems and normal forms of elements over two-sided crossed products have been recently defined in [10]). In the crossed product case, we will consider their presentations that were given in [2]. As a next step, by using the normal forms of elements of these two products, we calculate the growth series of the crossed product of different combinations of finite and infinite cyclic groups as well as the growth series of two-sided crossed product of finite cyclic groups.