The Size of the Giant Joint Component in a Binomial Random Double Graph

We study the joint components in a random 'double graph' that is obtained by superposing red and blue binomial random graphs on $n$~vertices. A joint component is a maximal set of vertices that supports both a red and a blue spanning tree. We show that there are critical pairs of red and blue edge densities at which a giant joint component appears. In contrast to the standard binomial graph model, the phase transition is first order: the size of the largest joint component jumps from $O(1)$ vertices to $\Theta(n)$ at the critical point. We connect this phenomenon to the properties of a certain bicoloured branching process.

Rewriting with generalized nominal unification

We consider matching, rewriting, critical pairs and the Knuth–Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. We utilize atom-variables instead of atoms to formulate and rewrite rules on constrained expressions, which is an improvement of expressiveness over previous approaches. Nominal unification and nominal matching are correspondingly extended. Rewriting is performed using nominal matching, and computing critical pairs is done using nominal unification. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is $$\prod _2^p$$ -complete. We prove that the adapted Knuth–Bendix confluence test is applicable to a nominal rewrite system with atom-variables, and thus that there is a decidable test whether confluence of the ground instance of the abstract rewrite system holds. We apply the nominal Knuth–Bendix confluence criterion to the theory of monads and compute a convergent nominal rewrite system modulo alpha-equivalence.

Critical Pair Analysis in Nominal Rewriting

Nominal rewriting (Fernández, Gabbay & Mackie, 2004;Fernández & Gabbay, 2007) is a framework that extendsfirst-order term rewriting by a binding mechanismbased on the nominal approach (Gabbay & Pitts, 2002;Pitts, 2003). In this paper, we investigate confluenceproperties of nominal rewriting, following the study oforthogonal systems in (Suzuki et al., 2015), but herewe treat systems in which overlaps of the rewrite rulesexist. First we present an example where choice ofbound variables (atoms) of rules affects joinability ofthe induced critical pairs. Then we give a detailedproof of the critical pair lemma, and illustrate someof its applications including confluence results fornon-terminating systems.

Finitary -adhesive categories

Finitary$\mathcal{M}$-adhesive categories are$\mathcal{M}$-adhesive categories with finite objects only, where$\mathcal{M}$-adhesive categories are a slight generalisation of weak adhesive high-level replacement (HLR) categories. We say an object is finite if it has a finite number of$\mathcal{M}$-subobjects. In this paper, we show that in finitary$\mathcal{M}$-adhesive categories we not only have all the well-known HLR properties of weak adhesive HLR categories, which are already valid for$\mathcal{M}$-adhesive categories, but also all the additional HLR requirements needed to prove classical results including the Local Church-Rosser, Parallelism, Concurrency, Embedding, Extension and Local Confluence Theorems, where the last of these is based on critical pairs. More precisely, we are able to show that finitary$\mathcal{M}$-adhesive categories have a unique$\mathcal{E}$-$\mathcal{M}$factorisation and initial pushouts, and the existence of an$\mathcal{M}$-initial object implies we also have finite coproducts and a unique$\mathcal{E}$′-$\mathcal{M}$pair factorisation. Moreover, we can show that the finitary restriction of each$\mathcal{M}$-adhesive category is a finitary$\mathcal{M}$-adhesive category, and finitarity is preserved under functor and comma category constructions based on$\mathcal{M}$-adhesive categories. This means that all the classical results are also valid for corresponding finitary$\mathcal{M}$-adhesive transformation systems including several kinds of finitary graph and Petri net transformation systems. Finally, we discuss how some of the results can be extended to non-$\mathcal{M}$-adhesive categories.