#  $D$-completion, well-filterification and sobrification 111This work is
supported by the National Natural Science Foundation of China (No.11771134)
and by Hunan Provincial Innovation Foundation For Postgraduate (CX20200419)

Hualin Miao<EMAIL_ADDRESS>Longchun Wang<EMAIL_ADDRESS>Qingguo
Li  School of Mathematics, Hunan University, Changsha, Hunan, 410082, China
<EMAIL_ADDRESS>
###### Abstract

In this paper, we obtain some sufficient conditions for the $D$-completion of
a $T_{0}$ space to be the well-filterification of this space, the well-
filterification of a $T_{0}$ space to be the sobrification of this space and
the $D$-completion of a $T_{0}$ space to be the sobrification, respectively.
Moreover, we give an example to show that a tapered closed set may be neither
the closure of a directed set nor the closed $KF$-set, respectively. Because
the tapered closed set is a closed $WD$-set, the example also gives a negative
answer to a problem proposed by Xu. Meantime, a new direct characterization of
the $D$-completion of a $T_{0}$ space is given by using the notion of
pre-$c$-compact elements.

###### keywords:

$D$-completion , Well-filterification , Sobrification , Join continuous

###### MSC:

54B20, 06B35, 06F30

##  1 Introduction

$D$-completion, well-filterification and sobrification of a $T_{0}$ space play
a fundamental role in non-Hausdorff topological spaces. We know that the
$D$-completion of a $T_{0}$ space is contained in the well-filterification of
this space, and the well-filterification is contained in the sobrification.
But the converses of them are not necessarily true.

In [6], Keimel and Lawson verified that the $D$-completion of a $T_{0}$ space
is the sobrification of this space if the space is a $c$-space or $qc$-space.
Lawson, Wu and Xi gave the sufficient condition that the space $X$ is core-
compact for a well-filtered space $X$ to be sober in [8]. Xu and Shen proved
that every first countable well-filtered space is sober in [14]. Xi and Lawson
obtained the result that every monotone convergence space $X$ with the
property that $\mathord{\downarrow}(K\cap A)$ is a closed subset of $X$ for
any closed subset $A$ and compact saturated set $K$ is well-filtered in [12].
Therefore, naturally, there are some questions in the following:

(1) Whether the well-filterification of a first countable $T_{0}$ space $X$
coincides with the sobrification of this space;

(2) Whether the well-filterification of a second countable $T_{0}$ space
agrees with the sobrification;

(3) Whether the $D$-completion of a $T_{0}$ space $X$ with the property that
$\mathord{\downarrow}(K\cap A)$ is a closed subset of $X$ for any closed $KF$
set $A$ and compact saturated set $K$ coincides with the well-filterification.

In [10], Miao and Li proposed the concept of join-continuous poset and showed
that every core-compact join continuous dcpo is sober. They also obtain the
result that a monotone convergence space $X$ with the property that
$\mathord{\downarrow}(A\cap W)$ is a closed subset of $X$ for any irreducible
closed subset $A$ of $X$ and upper set $W$ is a sober space. Naturally, some
questions are raised below.

(4) Whether the $D$-completion of a locally compact $T_{0}$ space $X$ with the
property that $\mathord{\downarrow}(K\cap A)$ is a closed subset of $X$ for
any closed $KF$ set $A$ and compact saturated set $K$ agrees with the
sobrification;

(5) Whether the $D$-completion of a core-compact join-continuous poset $P$
coincides with the sobrification;

(6) Whether the $D$-completion of a $T_{0}$ space $X$ with the property that
$\mathord{\downarrow}(A\cap W)$ is a closed subset of $X$ for any irreducible
closed subset $A$ of $X$ and upper set $W$ coincides with the sobrification.

In [9], Liu, Li and Wu give a counterexample to show that $\mathbf{WD}(X)$ may
not agree with $\mathbf{KF}(X)$ for any $T_{0}$ space $X$, which solved the
open problem proposed by Xu in [15]. Zhang and Li provided a direct
characterization of the $D$-completion of a $T_{0}$ space using the tapered
closed subsets ([16]). We know that every directed set is a tapered set. So,
naturally there is a problem in the following.

######  Problem 1.1.

Let $X$ be a $T_{0}$ space and $A$ a tapered closed subset of $X$. Does there
exist a directed subset $D$ of $X$ such that $A=cl(D)$?

In [17], Zhao and Fan gave the $D$-completion of a poset. Keimel and Lawson
presented a standard $D$-completion of a $T_{0}$ topological space in [6].
However, both of their work do not give the concrete elements of the
$D$-completion of a poset or a $T_{0}$ space like the sobrification of the
spaces. In [16], Zhang and Li provided a direct description of the elements of
the $D$-completion of a $T_{0}$ space by continuous functions. Shall we just
characterize the $D$-completion of a $T_{0}$ space by the elements of the
space itself?

The purpose of this paper is to investigate the above questions. We give some
sufficient conditions for the $D$-completion of a $T_{0}$ space to be the
well-filterification, the well-filterification of a $T_{0}$ space to be the
sobrification and the $D$-completion of a $T_{0}$ space to be the
sobrification, respectively. For Problem 1.1, we propose a counterexample to
reveal that a tapered closed set may not be the closure of a directed set and
the closed $KF$-set, respectively. Meantime, a new direct characterization of
the $D$-completion of a $T_{0}$ space is given by using the notion of
pre-$c$-compact elements.

##  2 Preliminaries

Without further references, the posets mentioned here are all endowed with the
Scott topology.

Let $X$ be a topological space. We denote the set of all _closed sets_ of $X$
by $\Gamma(X)$ and all _open sets_ by $\mathcal{O}(X)$. If $P$ is a poset,
$\sigma(P)$ denotes the set of all _Scott open_ sets and $\Gamma(P)$ the set
of all _Scott closed_ sets. $A$ is called _$d$ -closed_ if $D\subseteq A$
implies that $\sup D\in A$ for any directed subset of $A$. $cl_{d}(A)$
represents $A$ is $d$-closed. Given a topological space $(X,\tau)$, we define
$x\leq y$ iff $x\in cl(y)$. Hence, $X$ with its specialization order is a
poset. For any set $A\subseteq X$, we denote the closure of $A$ by $cl(A)$.
The irreducible sets of $X$ are denoted by $IRR(X)$ and the irreducible closed
sets by $\mathbf{IRR}(X)$, all upper sets of $X$ by $up(X)$.

######  Definition 2.1.

([3])

(i) Let $P$ be a poset. A subset $D$ of $P$ is _directed_ provided it is
nonempty and every finite subset of $D$ has an upper bound in $D$. We denote
that $D$ is a directed subset of $P$ by $D\subseteq^{\uparrow}P$.

(ii) A poset $P$ is a _dcpo_ if every directed subset $D$ has the supremum.

######  Definition 2.2.

([4])

(i) A topological space $X$ is _locally compact_ if for every $x\in X$ and any
open neighborhood $U$ of $x$, there is a compact saturated subset $Q$ of $X$
such that $x\in\mathrm{int}(Q)$ and $Q\subseteq U$.

A set $K$ of a topological space is called _saturated_ if it is the
intersection of its open neighborhood ($K=\mathord{\uparrow}K$ in its
specialization order). If $A$ is any subset of $X$, the intersection sat$A$ of
all its open neighborhood is a saturated set called its _saturation_.

(ii) A topological space $X$ is _core-compact_ if $\mathcal{O}(X)$ is a
continuous lattice.

(iii) A topological space $X$ is said to be _first countable_ if each point
has a countable neighbourhood basis (local base). That is, for each point $x$
in $X$ there exists a sequence $N_{1},N_{2},\cdots$ of the neighbourhoods of
$x$ such that for any neighbourhood $N$ of $x$, there exists an integer $i$
with $N_{i}$ contained in $N$.

(iv) A topological space is said to be _second countable_ if its topology has
a countable base.

######  Definition 2.3.

([4]) A topological space $X$ is _sober_ if it is $T_{0}$ and every
irreducible closed subset of $X$ is the closure of a (unique) point.

######  Definition 2.4.

([3]) We shall say that a space $X$ is _well-filtered_ if for each filter
basis $\mathcal{C}$ of compact saturated sets and each open set $U$ with
$\bigcap\mathcal{C}\subseteq U$, there is a $K\in\mathcal{C}$ with $K\subseteq
U$.

For a topological space $X$, the compact saturated subsets of $X$ are denoted
by $Q(X)$. We write $\mathfrak{K}\subseteq_{flt}Q(X)$ represents that
$\mathfrak{K}$ is a filtered subfamily of $Q(X)$ and $F\subseteq_{fin}X$
represents that $F$ is a finite subset of $X$.

######  Definition 2.5.

([11]) Let $X$ be a topological space. A nonempty subset $A\in KF(X)$ if and
only if there exists $\mathfrak{K}\subseteq_{flt}Q(X)$ such that $cl(A)$ is a
minimal closed set that intersects all members of $\mathfrak{K}$. The set of
all closed $KF$-subsets of $X$ is denoted by $\mathbf{KF}(X)$.

######  Definition 2.6.

[14] A $T_{0}$ space $X$ is called _$\omega$ -well-filtered_, if for any
countable filtered family $\\{K_{i}:i<\omega\\}\subseteq Q(X)$ and
$U\in\mathcal{O}(X)$, it satisfies

$\bigcap_{i<\omega}K_{i}\subseteq U\Rightarrow\exists
i_{0}<\omega,K_{i_{0}}\subseteq U$

######  Definition 2.7.

[14] Let $X$ be a $T_{0}$ space. A nonempty subset $A\in KF_{\omega}(X)$ if
and only if there exists a countable filtered family $\mathcal{K}\subseteq
Q(X)$ such that $cl(A)$ is a minimal closed set that intersects all members of
$\mathcal{K}$. The set of all closed $KF_{\omega}$-subsets of $X$ is denoted
by $\mathbf{KF_{\omega}}(X)$.

######  Definition 2.8.

[14] A subset $A$ of a $T_{0}$ space $X$ is called a _$\omega$ -well-filtered
determined set_, $WD_{\omega}$ set for short, if for any continuous mapping
$f:X\longrightarrow Y$ to a $\omega$-well-filtered space $Y$ , there exists a
unique $y_{A}\in Y$ such that $cl(f(A))=cl(\\{y_{A}\\})$. The set of all
closed $\omega$-well-filtered determined subsets of $X$ is denoted by
$\mathbf{WD_{\omega}}(X)$.

######  Definition 2.9.

([6]) A $T_{0}$ space is a _monotone convergence space_ if and only if the
closure of every directed sets (in the specialization order) is the closure of
a unique point.

######  Definition 2.10.

([6]) A _D-completion_ of a $T_{0}$ space $X$ is a monotone convergence space
$Y$ with a topological embedding $j:X\longrightarrow Y$ and $cl_{d}(j(X))=Y$.

######  Definition 2.11.

[10] A poset $L$ is _join-continuous_ if $f_{x}$ is continuous for any $x\in
L$ where $f_{x}:(L,\sigma(L))\rightarrow up(L)$ is defined by
$f_{x}(y)=\mathord{\uparrow}x\cap\mathord{\uparrow}y$ for all $y\in L$ when
$up(L)$ is endowed with the upper Vietoris topology.

######  Definition 2.12.

[13] A subset $A$ of a $T_{0}$ space $X$ is called a _well-filtered determined
set_ , $WD$ set for short, if for any continuous mapping $f:X\longrightarrow
Y$ to a well-filtered space $Y$ , there exists a unique $y_{A}\in Y$ such that
$cl(f(A))=cl(\\{y_{A}\\})$. The set of all closed well-filtered determined
subsets of $X$ is denoted by $\mathbf{WD}(X)$.

######  Lemma 2.13.

([4]) If a topological space $X$ is second countable, then $X$ is first
countable.

######  Lemma 2.14.

([16]) The topological space of all tapered closed subsets of a $T_{0}$ space
$X$ is the standard $D$-completion of $X$.

The following construction is due to Ershov [2]. Let topological spaces $X$
and $Y_{x}$, and $x\in X$, be given. Let

$Z=\bigcup_{x\in X}Y_{x}\times\\{x\\}$

$\tau=\\{U\subseteq Z\mid(U)_{x}\in\tau({Y_{x}})~{}for~{}any~{}x\in
X~{}and~{}(U)_{X}\in\tau(X)\\}$,

where $U_{x}=\\{y\in Y_{x}\mid(y,x)\in U\\}$ for any $x\in X$ and
$(U)_{X}=\\{x\in X\mid(U)_{x}\neq\emptyset\\}.$

In this paper, the space $Z=(Z,\tau)$ is denoted by $\sum_{X}Y_{x}$. For any
subset $A\subseteq Z$, put $(A)_{x}=\\{y\in Y_{x}\mid(y,x)\in A\\}$, and
$(A)_{X}=\\{x\in X\mid(A)_{x}\neq\emptyset\\}$.

######  Lemma 2.15.

[2] Let $X$ be a $T_{0}$ space, $Y_{x}$ an irreducible $T_{0}$ space for any
$x\in X$, and $Z=\sum_{X}Y_{x}$. For all $(y_{0},x_{0}),(y_{1},x_{1})\in Z$,
we have $(y_{0},x_{0})\leq_{Z}(y_{1},x_{1})$ if and only if the following two
alternatives hold:

$(1)$ $x_{0}=x_{1}$, $y_{0}\leq_{Y_{x_{0}}}y_{1}$;

$(2)$ $x_{0}<x_{1}$ and $y_{1}=\top_{x_{1}}$ is the greatest element in
$Y_{x_{1}}$ with respect to the specialization order.

######  Lemma 2.16.

[9] Let $\mathbb{N}=(N,\tau_{cof})$, where $\tau_{cof}$ denotes the cofinite
topology, and $X_{n}$ an irreducible $T_{0}$ space for every $n\in N$, such
that there are at most finitely many $X_{n}$’s that have a greatest element
under the specialization order $\leq_{X_{n}}$. Let $Z=\sum_{\mathbb{N}}X_{n}$.
Then $A$ is a $KF$-set of $Z$ iff there exists a unique $n\in\mathbb{N}$ such
that $A\subseteq X_{n}\times\\{n\\}$ and $\\{y\in X_{n}\mid(y,x)\in A\\}$ is a
$KF$-set of $X_{n}$.

######  Proposition 2.17.

([6]) For a monotone convergence space $X$. $A$ is a monotone convergence
subspace iff $A$ is a sub-dcpo of $X$ with the specialization order.

######  Theorem 2.18.

[15] Every locally compact $T_{0}$ space is a Rudin space, that is,
$\mathbf{IRR}(X)=\mathbf{KF}(X)$.

######  Theorem 2.19.

[18] Let $L$ be a dcpo. Then the following statements are equivalent:

$(1)$ $\sigma(L)$ is a continuous lattice;

$(2)$ For every dcpo or complete lattice $S$, one has $\sigma(S\times
L)=\sigma(S)\times\sigma(L)$.

######  Theorem 2.20.

[13] Let $X$ be a $T_{0}$ space. Then $\mathbf{WD}(X)$ with the lower Vietoris
topology is the well-filtered reflection of $X$.

##  3 Sufficient conditions

######  Lemma 3.1.

Let $X$ be a $T_{0}$ space. Then the following statements are equivalent:

$(1)$ If $A\in\mathbf{KF}(X)$, then $\mathord{\downarrow}(A\cap
K)\in\Gamma(X)$ for any $K\in Q(X)$;

$(2)$ $A$ is a directed closed subset of $X$.

###### Proof.

$(1)\Rightarrow(2)$ It suffices to prove that $A$ is directed. Suppose
$A\in\mathbf{KF}(X)$. Then there exists $\\{K_{i}\\}_{i\in
I}\subseteq_{flt}Q(X)$ such that $A$ is a minimal closed set that intersects
all members of $\\{K_{i}\\}_{i\in I}$ by Definition 2.5.

Claim 1: $A=\mathord{\downarrow}(A\cap K_{j})$ for any $j\in I$.

For any $i\in I$, since $\\{K_{i}\\}_{i\in I}\subseteq_{flt}Q(X)$, there
exists $r\in I$ such that $K_{r}\subseteq K_{i}\cap K_{j}$. This implies that
$\emptyset\neq A\cap K_{r}\subseteq A\cap K_{j}\cap
K_{i}\subseteq\mathord{\downarrow}(A\cap K_{j})\cap K_{i}$. Then we have
$A=\mathord{\downarrow}(A\cap K_{j})$ by the minimality of $A$.

Claim 2: $\mathord{\uparrow}x\cap K_{i}\cap A\neq\emptyset$ for any $x\in A$
and $i\in I$.

$x\in A=\mathord{\downarrow}(A\cap K_{i})$ by Claim 1. Thus
$\mathord{\uparrow}x\cap A\cap K_{i}\neq\emptyset$.

Claim 3: $A$ is directed.

Let $x,y\in A$. Then we have $\mathord{\downarrow}(\mathord{\uparrow}x\cap
A)\cap K_{i}\neq\emptyset$ by Claim 2. It follows that
$\mathord{\downarrow}(\mathord{\uparrow}x\cap A)=A$ by the minimality of $A$.
Note that $y\in A=\mathord{\downarrow}(\mathord{\uparrow}x\cap A)$, thus
$\mathord{\uparrow}y\cap\mathord{\uparrow}x\cap A\neq\emptyset$.

$(2)\Rightarrow(1)$ It remains to prove that $\mathord{\downarrow}(A\cap
K)\in\Gamma(X)$.

Claim 1: $\mathord{\downarrow}(\mathord{\uparrow}x\cap A)\in\Gamma(X)$ for any
$x\in X$.

If $\mathord{\uparrow}x\cap A=\emptyset$, then we have
$\mathord{\downarrow}(\mathord{\uparrow}x\cap A)=\emptyset\in\Gamma(X)$. Else
$\mathord{\uparrow}x\cap A\neq\emptyset$. Then $x\in A$ because $A$ is a lower
set. Obviously, $\mathord{\downarrow}(\mathord{\uparrow}x\cap A)\subseteq A$.
Conversely, $\mathord{\uparrow}a\cap\mathord{\uparrow}x\cap A\neq\emptyset$
for any $a\in A$ since $A$ is directed. So we have
$\mathord{\downarrow}(\mathord{\uparrow}x\cap A)=A\in\Gamma(X)$.

Claim 2: $\mathord{\downarrow}(K\cap A)\in\Gamma(X)$.

If $K\cap A=\emptyset$, then $\mathord{\downarrow}(K\cap
A)=\emptyset\in\Gamma(X)$. Else $K\cap A\neq\emptyset$. Pick $k\in K\cap A$.
This means that $A\subseteq\mathord{\downarrow}(\mathord{\uparrow}k\cap
A)\subseteq\mathord{\downarrow}(K\cap A)\subseteq A$ by Claim 1. Hence,
$\mathord{\downarrow}(K\cap A)=A\in\Gamma(X)$. ∎

######  Theorem 3.2.

Let $X$ be a locally compact $T_{0}$ space with the property
$\mathord{\downarrow}(K\cap A)\in\Gamma(X)$ for any $A\in\mathbf{KF}(X)$ and
$K\in Q(X)$. Then the $D$-completion of $X$ coincides with the soberification
of $X$.

###### Proof.

Let $A\in\mathbf{IRR}(X)$. It suffices to prove that $A$ is directed. By
Theorem 2.18, we have $\mathbf{IRR}(X)=\mathbf{KF}(X)$. This implies that $A$
is directed by Lemma 3.1. ∎

Theorem 3.2 gives a positive answer for the problem $(4)$ in the introduction.

######  Theorem 3.3.

Let $X$ be a $T_{0}$ space with the property $\mathord{\downarrow}(K\cap
A)\in\Gamma(X)$ for any $A\in\mathbf{KF}(X)$ and $K\in Q(X)$. If
$\mathbf{KF}(X)$ endowed with the lower Vietoris topology is the well-
filterification of $X$. Then the $D$-completion of $X$ agrees with the well-
filterification of $X$.

###### Proof.

By Lemma 2.14, we know that all tapered closed subsets of $X$ is the
$D$-completion of $X$. Note that directed closed subsets of $X$ must be
tapered. We need to prove that $A$ is a directed subset of $X$ for any tapered
closed subset $A$ of $X$. It suffices to prove that $\mathcal{D}=\\{cl(D)\mid
D\subseteq^{\uparrow}X\\}$ is a subdcpo of $\Gamma(X)$. Let
$\\{cl(D_{i})\\}_{i\in I}$ be any directed subset of $\Gamma(X)$ contained in
$\mathcal{D}$. Note that $\sup_{i\in I}cl(D_{i})=cl(\bigcup_{i\in
I}cl(D_{i}))$. We need to verify that $\sup_{i\in I}cl(D_{i})\in\mathcal{D}$.
Since $\mathcal{D}\subseteq\mathbf{KF}(X)$, we have $cl(D_{i})$ is directed
for any $i\in I$ by Lemma 3.1. It suffices to show that $\bigcup_{i\in
I}cl(D_{i})$ is a directed subset of $X$. Now let $x,y\in\bigcup_{i\in
I}cl(D_{i})$. Then there exists $\\{i_{x},i_{y}\\}\subseteq I$ such that $x\in
cl(D_{i_{x}}),y\in cl(D_{i_{y}})$. It follows that there exists $i\in I$ such
that $\\{x,y\\}\subseteq cl(D_{i_{x}})\cup cl(D_{i_{y}})\subseteq cl(D_{i})$
by the directionality of $(cl(D_{i}))_{i\in I}$. Thus there exists $z\in
cl(D_{i})\subseteq\bigcup_{i\in I}cl(D_{i})$ such that $z$ is an upper bound
of $x,y$ because $cl(D_{i})$ is a directed subset of $X$. So $\sup_{i\in
I}cl(D_{i})\in\mathcal{D}$. By Lemma 3.1, we have
$\mathbf{KF}(X)\subseteq\mathcal{D}$. Hence, the $D$-completion of $X$ agrees
with the well-filterification of $X$. ∎

We know that a monotone convergence space with the property
$\mathord{\downarrow}(K\cap A)\in\Gamma(X)$ for any $A\in\mathbf{KF}(X)$ and
$K\in Q(X)$ is a well-filtered space by [12]. So there is a problem below:

######  Problem 3.4.

Without the condition that $\mathbf{KF}(X)$ endowed with the lower Vietoris
topology is the well-filterification of $X$, whether the statement in Theorem
3.3 holds for any $T_{0}$ space $X$ with the property
$\mathord{\downarrow}(K\cap A)\in\Gamma(X)$ for any $A\in\mathbf{KF}(X)$ and
$K\in Q(X)$.

Note that Problem 3.4 actually is the problem $(3)$ in the introduction. For
this problem, we give a counterexample as follows.

######  Example 3.5.

Let $X=(\mathbb{N},\tau_{cof}),Y_{n}=(\mathbb{N},\sigma(\mathbb{N}))$ for any
$n\in X$, $Z=\sum_{X}Y_{n}$, where $\mathbb{N}$ is the set of natural numbers.
Then $\mathord{\downarrow}(K\cap A)\in\Gamma(Z)$ for any $A\in\mathbf{KF}(Z)$
and $K\in Q(Z)$, but the $D$-completion $Z^{d}$ of $Z$ does not agree with the
well-filterification $Z^{w}$ of $Z$.

###### Proof.

By Lemma 2.16 and Lemma 2.15, we have that $A$ is a directed subset of $Z$ for
any $A\in\mathbf{KF}(Z)$. This implies that $\mathord{\downarrow}(K\cap
A)\in\Gamma(Z)$ for any $A\in\mathbf{KF}(Z)$ and $K\in Q(Z)$ because of Lemma
3.1. Let $\mathcal{N}=\\{Y_{n}\times\\{n\\}\mid n\in X\\}$. Note that
$Y_{n}\times\\{n\\}\subseteq^{\mathord{\uparrow}}Z$ for any $n\in X$. It
follows that $\mathcal{N}\subseteq Z^{w}$.

Claim 1: $\mathcal{A}$ is compact in $Z^{w}$ for any
$\mathcal{A}\subseteq\mathcal{N}$.

Let $\\{U_{i}\\}_{i\in I}\subseteq\mathcal{O}(Z)$ with
$\mathcal{A}\subseteq\bigcup_{i\in I}\diamondsuit U_{i}$. Pick
$Y_{n_{0}}\times\\{n_{0}\\}\in\mathcal{A}\subseteq\bigcup_{i\in I}\diamondsuit
U_{i}$. So there exists $i_{n_{0}}\in I$ such that
$Y_{n_{0}}\times\\{n_{0}\\}\in\diamondsuit U_{i_{n_{0}}}$.
$(U_{i_{n_{0}}})_{X}\in\tau_{cof}$ since $U_{i_{n_{0}}}$ is open in $Z$. Let
$B=X\backslash(U_{i_{n_{0}}})_{X},C=\\{n\in X\mid
Y_{n}\times\\{n\\}\in\mathcal{A},Y_{n}\times\\{n\\}\cap
U_{i_{n_{0}}}=\emptyset\\}$. Note that $B$ is finite and $C\subseteq B$. Then
there exists finitely many members of $\\{\diamondsuit U_{i}\\}_{i\in I}$ to
cover $\mathcal{A}$.

Let $\mathcal{A}_{n}=\mathcal{N}\backslash\\{Y_{i}\times\\{i\\}\mid
i\in\\{1,2,\cdots n\\}\\}$. Thus
$\\{\mathord{\uparrow}_{Z^{w}}\mathcal{A}_{n}\\}_{n\in
X}\subseteq_{flt}Q(Z^{w})$ by Claim 1.

Since $Z^{w}$ is well-filtered, we have $\bigcap_{n\in
X}\mathord{\uparrow}_{Z^{w}}\mathcal{A}_{n}\neq\emptyset$. Choose
$B\in\bigcap_{n\in X}\mathord{\uparrow}_{Z^{w}}\mathcal{A}_{n}$, i.e., $B\in
Z^{w}$.

Claim 2: $(B)_{X}$ is infinite.

Suppose not, if $(B)_{X}$ is finite. Let $n_{1}=\max{(B)_{X}}$. Since
$B\in\bigcap_{n\in
X}\mathord{\uparrow}_{Z^{w}}\mathcal{A}_{n}\subseteq\mathord{\uparrow}_{Z^{w}}\mathcal{A}_{n_{1}}$,
we have $\mathord{\downarrow}_{Z^{w}}B\cap\mathcal{A}_{n_{1}}\neq\emptyset$.
Then there exists $n_{2}>n_{1}$ such that
$Y_{n_{2}}\times\\{n_{2}\\}\in\mathord{\downarrow}_{Z^{w}}B\cap\mathcal{A}_{n_{1}}$,
which contradicts $n_{2}\notin(B)_{X}$.

By Lemma 2.15, $B$ is not directed. This implies that $B$ is not a tapered
closed subset of $Z$ by the proof of Theorem 3.3. Thus $B\in Z^{w}\backslash
Z^{d}$, that is, the $D$-completion $Z^{d}$ of $Z$ does not agree with the
well-filterification $Z^{w}$ of $Z$.

∎

######  Lemma 3.6.

Let $L$ be a poset. Then the following statements are equivalent:

$(1)$ $\sigma(L)$ is a continuous lattice;

$(2)$ For every dcpo or complete lattice $S$, one has $\sigma(S\times
L)=\sigma(S)\times\sigma(L)$.

###### Proof.

The proof is similar to Theorem 2.19. ∎

######  Theorem 3.7.

Let $L$ be a core-compact and join continuous poset. Then the $D$-completion
of $L$ coincides with the soberification of $L$.

###### Proof.

Let $A$ be a irreducible closed subset of $X$. Then it suffices to prove that
$A$ is directed. Define $F:(L\times L,\sigma(L\times L))\longrightarrow up(L)$
by $F(x,y)=\mathord{\uparrow}x\cap\mathord{\uparrow}y$ for any $(x,y)\in
L\times L$.

Claim 1: $F$ is continuous.

Let $U\in\sigma(L)$. We need to prove that $F^{-1}(\Box U)$ is Scott open in
$L\times L$. It suffices to prove that $F^{-1}(\Box U)$ is Scott open when
$F^{-1}(\Box U)\neq\emptyset$. Obviously, $F^{-1}(\Box
U)=\mathord{\uparrow}(F^{-1}(\Box U))$. Now let $\\{(x_{i},y_{i})\\}_{i\in I}$
be any directed subset of $L\times L$ such that $\sup_{i\in I}(x_{i},y_{i})$
exists in $L\times L$ with $\sup_{i\in I}(x_{i},y_{i})=(\sup_{i\in
I}x_{i},\sup_{i\in I}y_{i})\in F^{-1}(\Box U)$. This implies that
$\mathord{\uparrow}\sup_{i\in I}x_{i}\cap\mathord{\uparrow}\sup_{i\in
I}y_{i}\in\Box U$. So we have $f_{\sup_{i\in I}x_{i}}(\sup_{i\in
I}y_{i})\in\Box U$. It follows that $\sup_{i\in I}y_{i}\in f_{\sup_{i\in
I}x_{i}}^{-1}(\Box U)$ is Scott open in $L$ because $L$ is join continuous.
This implies that there exists $i_{0}\in I$ such that $y_{i_{0}}\in
f_{\sup_{i\in I}x_{i}}^{-1}(\Box U)$. Thus
$\mathord{\uparrow}y_{i_{0}}\cap\mathord{\uparrow}\sup_{i\in I}x_{i}\in\Box
U$. Then we have $\sup_{i\in I}x_{i}\in f_{y_{i_{0}}}^{-1}(\Box U)$. By the
join continuity of $L$, there exists $i_{1}\in I$ such that $x_{i_{1}}\in
f_{y_{i_{0}}}^{-1}(\Box U)$. Thus there exists $i\in I$ such that
$(x_{i},y_{i})$ is an upper bound of
$\\{(x_{i_{0}},y_{i_{0}}),(x_{i_{1}},y_{i_{1}})\\}$ because
$\\{(x_{i},y_{i})\\}_{i\in I}$ is directed. Therefore, $(x_{i},y_{i})\in
F^{-1}(\Box U)$. Hence, $F$ is continuous.

Claim 2: $A$ is a directed subset of $X$.

By Lemma 3.6 and Claim 1, we have $F:\sigma(L)\times\sigma(L)\longrightarrow
up(L)$ is continuous. Let $\\{x,y\\}\subseteq A$. We need to prove that
$\mathord{\uparrow}x\cap\mathord{\uparrow}y\cap A\neq\emptyset$. Suppose not,
if $\mathord{\uparrow}x\cap\mathord{\uparrow}y\cap A=\emptyset$. It follows
that $\mathord{\uparrow}x\cap\mathord{\uparrow}y\subseteq\Box(X\backslash A)$,
that is, $F((x,y))\in\Box(X\backslash A)$. This implies that there exists
$\\{U,V\\}\subseteq\sigma(L)$ such that $(x,y)\in U\times V\subseteq
F^{-1}(\Box(X\backslash A))$ by the continuity of $F$. Notice that $x\in A\cap
U$, $y\in A\cap V$. We have $A\cap U\cap V\neq\emptyset$ since $A$ is
irreducible. Pick $z\in A\cap U\cap V$. Hence $(z,z)\in U\times V\subseteq
F^{-1}(\Box(X\backslash A))$. This means that
$z\in\mathord{\uparrow}z\cap\mathord{\uparrow}z\subseteq(X\backslash A)$,
which contradicts $z\in A$. So $A$ is directed.

∎

For the problem $(5)$ mentioned in the introduction, we give a positive answer
by Theorem 3.7.

######  Corollary 3.8.

Let $L$ be a core-compact poset with the property that
$\mathord{\downarrow}(K\cap A)\in\Gamma(L)$ for any $A\in\mathbf{IRR}(L)$ and
$K\in Q(L)$. Then the $D$-completion of $L$ agrees with the soberification of
$L$.

###### Proof.

The proof is similar to Theorem 3.7. ∎

In contrast to Theorems 3.2 and Corollary 3.8, we raise the following
question.

######  Problem 3.9.

Whether the statement in Corollary 3.8 holds for arbitrary core-compact
topological spaces $X$ with the property that $\mathord{\downarrow}(K\cap
A)\in\Gamma(X)$ for any $A\in\mathbf{IRR}(X)$ and $K\in Q(X)$.

######  Proposition 3.10.

Let $X$ be a second countable space. Then the well-filterification of $X$
coincides with the soberification of $X$.

###### Proof.

It suffices to prove that the well-filterification of $X$ is second countable
by Theorem 4.1 in [14]. Let $\mathcal{B}$ be a countable basis of $X$,
$\mathcal{U}=\\{\diamondsuit U\mid U\in\mathcal{B}\\}$. Since $\mathcal{U}$ is
countable, we only need to prove that $\mathcal{U}$ is a basis of the well-
filterification of $X$. Let $A\in\mathbf{WD}(X)$, $V\in\mathcal{O}(X)$,
$A\in\diamondsuit V$. Then $A\cap V\neq\emptyset$. Pick $x\in A\cap V$. This
implies that there exists $U\in\mathcal{B}$ such that $x\in U\subseteq V$. It
follows that $A\in\diamondsuit U\subseteq\diamondsuit V$. ∎

We give a positive answer for the problem $(2)$ in the introduction by Theorem
3.10.

######  Lemma 3.11.

Let $X$ be a $T_{0}$ space, $X^{s}$ the soberification of $X$. For each
ordinal $\beta$, define

$(1)$ $X_{\beta+1}=\\{x\in X^{s}\mid\exists
F\in\mathbf{KF}(X_{\beta}),cl_{X^{s}}(F)=\mathord{\downarrow}_{X^{s}}x\\}$;

$(2)$ $X_{\beta}=\bigcup_{\gamma<\beta}X_{\gamma}$ for a limit ordinal
$\beta$.

Then there exists an ordinal $\alpha_{X}$ such that
$X_{\alpha_{X}}=X_{\alpha_{X}+1}$ and the $\omega$-well-filtered reflection is
$X_{\alpha_{X}}$ endowed with the lower Vietoris topology.

###### Proof.

The proof is similar to Proposition 3.8 in [11]. ∎

######  Theorem 3.12.

Let $X$ be a first countable space. Then the well-filterification of $X$
agrees with the soberification of $X$.

###### Proof.

By Theorem 4.1 in [14], we only need to prove that the $\omega$-well-
filterification of $X$ is first countable. There exists an ordinal
$\alpha_{X}$ such that $X_{\alpha_{X}}=X_{\alpha_{X}+1}$ and the
$\omega$-well-filtered reflection is $X_{\alpha_{X}}$ endowed with the lower
Vietoris topology by Lemma 3.11. We want to prove that $X_{\alpha}$ endowed
with the lower Vietoris topology is first countable for any ordinal
$\alpha\leq\alpha_{X}$. We use induction on $\alpha$. For $\alpha=0$,
$X_{0}=\\{\mathord{\downarrow}x\mid x\in X\\}$. Then $X$ and $X_{0}$ are
homeomorphic. This implies that $X_{0}$ is first countable. Let $\alpha$ be
such that $\alpha+1\leq\alpha_{X}$, and let $X_{\alpha}$ be first countable.

Claim 1: $X_{\alpha+1}$ is first countable.

Let $A\in X_{\alpha+1}$. Then there exists
$\mathcal{F}\in\mathbf{KF}(X_{\alpha})$ such that
$cl_{X^{s}}(\mathcal{F})=\mathord{\downarrow}_{X^{s}}A$. Since
$\mathcal{F}\in\mathbf{KF}(X_{\alpha})$, there exists
$(\mathcal{K}_{n})_{n\in\mathbb{N}}\subseteq Q(X_{\alpha})$ such that
$\mathcal{F}$ is a minimal closed set that intersects all members of
$\\{\mathcal{K}_{n}\mid n\in\mathbb{N}\\}$. Pick
$A_{n}\in\mathcal{F}\cap\mathcal{K}_{n}$ for any $n\in\mathbb{N}$. It follows
that $\mathcal{F}=cl_{X_{\alpha}}(\mathcal{A})$ from the minimality of
$\mathcal{F}$, where $\mathcal{A}=\\{A_{n}\mid n\in\mathcal{N}\\}$. We want to
prove that $cl_{X^{s}}(\mathcal{F})=cl_{X^{s}}(\mathcal{A})$. Since
$cl_{X^{s}}(\mathcal{F})\cap
X_{\alpha}=\mathcal{F}=cl_{X_{\alpha}}(\mathcal{A})=cl_{X^{s}}(\mathcal{A})\cap
X_{\alpha}$, we have $\mathcal{F}\subseteq cl_{X^{s}}(\mathcal{A})$. So
$cl_{X^{s}}(\mathcal{F})\subseteq cl_{X^{s}}(\mathcal{A})$. Conversely, note
that $A_{n}\in\mathcal{K}_{n}\subseteq X_{\alpha}$ for any $n\in\mathbb{N}$.
Hence, $\mathcal{A}\subseteq cl_{X^{s}}(\mathcal{A})\cap
X_{\alpha}=cl_{X^{s}}(\mathcal{F})\cap X_{\alpha}$. This implies that
$\mathcal{A}\subseteq cl_{X^{s}}(\mathcal{F})$. Therefore,
$cl_{X^{s}}(\mathcal{F})=cl_{X^{s}}(\mathcal{A})$. Because $X_{\alpha}$ is
first countable, there exists a countable neighborhood basis
$\mathcal{B}_{n}=\\{\diamondsuit U\cap X_{\alpha}\mid\diamondsuit U\cap
X_{\alpha}\in\mathcal{B}_{n}\\}$ of $A_{n}$ for any $n\in\mathbb{N}$. Let
$\mathcal{B}_{A}=\\{\diamondsuit U\cap X_{\alpha+1}\mid\diamondsuit U\cap
X_{\alpha}\in\bigcup_{n\in\mathbb{N}}\mathcal{B}_{n}\\}$. Note that
$\mathcal{B}_{A}$ is countable. We only need to prove that $\mathcal{B}_{A}$
is a countable neighborhood basis of $A$ in $X_{\alpha+1}$. Let
$V\in\mathcal{O}(X)$ with $A\in\diamondsuit V\cap X_{\alpha+1}$. It follows
that $\mathcal{A}\cap\diamondsuit V\neq\emptyset$ since
$\mathord{\downarrow}_{X^{s}}A=cl_{X^{s}}(\mathcal{F})=cl_{X^{s}}(\mathcal{A})$.
Choose $A_{n}\in\mathcal{A}\cap\diamondsuit V\cap X_{\alpha}$. Then there
exists $\diamondsuit U\cap X_{\alpha}\in\mathcal{B}_{n}$ such that
$A_{n}\in\diamondsuit U\cap X_{\alpha}\subseteq\diamondsuit V\cap X_{\alpha}$.
We need to prove that $U\subseteq V$. Suppose not, if $U\nsubseteq V$, then
there exists $u\in U\cap(X\backslash V)$. This implies that
$\mathord{\downarrow}u\in\diamondsuit U\cap X_{\alpha}\subseteq\diamondsuit
V$. Thus $u\in V$, which contradicts $u\in X\backslash V$. So
$A\in\diamondsuit U\cap X_{\alpha+1}\subseteq\diamondsuit V\cap X_{\alpha+1}$.

Suppose now that $\alpha\leq\alpha_{X}$ is a limit ordinal and $X_{\beta}$ is
first countable for any $\beta<\alpha$. By definition of $X_{\alpha}$, we have
$X_{\alpha}=\bigcup_{\beta<\alpha}X_{\alpha}$.

Claim 2: $X_{\alpha}$ is first countable.

For any $A\in X_{\alpha}$, there exists $\beta<\alpha$ such that $A\in
X_{\beta}$. We have that there exists a countable neighborhood basis
$\mathcal{B}=\\{\diamondsuit U\cap X_{\beta}\mid\diamondsuit U\cap
X_{\beta}\in\mathcal{B}\\}$ of $A$ in $X_{\beta}$ since $X_{\beta}$ is first
countable. It suffices to prove that $\mathcal{B}_{A}=\\{\diamondsuit U\cap
X_{\alpha}\mid\diamondsuit U\cap X_{\beta}\in\mathcal{B}\\}$ is a countable
neighborhood basis of $A$ in $X_{\alpha}$. It is obvious that
$\mathcal{B}_{A}$ is countable. Now let $V\in\mathcal{O}(X)$ with $A\in
X_{\alpha}\cap\diamondsuit V$. Then $A\in\diamondsuit V\cap X_{\beta}$. It
follows that there exists $\diamondsuit U\cap X_{\beta}\in\mathcal{B}$ such
that $A\in\diamondsuit U\cap X_{\beta}\subseteq\diamondsuit V\cap X_{\beta}$.
Similar to the proof of Claim 1, we have $U\subseteq V$. So $A\in\diamondsuit
U\cap X_{\alpha}\subseteq\diamondsuit V\cap X_{\alpha}$. This proves that
$X_{\alpha}$ endowed with the lower Vietoris topology is first countable for
any ordinal $\alpha\leq\alpha_{X}$. Hence, the $\omega$-well-filtered
reflection $X_{\alpha_{X}}$ of $X$ is first countable.

∎

We give a positive answer by Theorem 3.12 to the problem $(1)$ in the
introduction.

######  Theorem 3.13.

Let $X$ be a $T_{0}$ space with the property $\mathord{\downarrow}(A\cap
W)\in\Gamma(X)$ for any $A\in\mathbf{IRR}(X)$ and $W\in up(X)$. Then the
$D$-completion of $X$ coincides with the soberification of $X$.

###### Proof.

Let $A\in\mathbf{IRR}(X)$. It suffices to prove that $A$ is directed. For any
$x,y\in A$, we need to prove that
$\mathord{\uparrow}x\cap\mathord{\uparrow}y\cap A\neq\emptyset$. Suppose not,
$\mathord{\uparrow}x\cap\mathord{\uparrow}y\cap A=\emptyset$. Let
$B=\mathord{\downarrow}(\mathord{\uparrow}x\cap A)$. Then
$\mathord{\downarrow}(X\backslash B)\in\Gamma(X)$. It follows that
$A=(B\cup(X\backslash B))\cap A=(B\cap A)\cup((X\backslash B)\cap
A)=B\cup((X\backslash B)\cap A)\subseteq
B\cup\mathord{\downarrow}((X\backslash B)\cap A)$. Thus $A\subseteq B$ or
$A\subseteq\mathord{\downarrow}((X\backslash B)\cap A)$. But $y\in
A\cap(X\backslash B)$ and $\mathord{\uparrow}x\cap A\cap(X\backslash
B)=\emptyset$ implies that $A\nsubseteq B$ and
$A\nsubseteq\mathord{\downarrow}((X\backslash B)\cap A)$, which contradicts
$A\subseteq B$ or $A\subseteq\mathord{\downarrow}((X\backslash B)\cap A)$. ∎

For the problem $(6)$ in the introduction, we give a positive answer by
Theorem 3.13.

##  4 A counterexample

In the following, we construct an example to give a negative answer to Problem
1.1. It also can answer Xu’s problem ([15]).

Figure 1: A tapered non-directed-determined poset.

######  Example 4.1.

Let $L=\mathbb{N}\times\mathbb{N}\times(\mathbb{N}\cup\infty)$, where
$\mathbb{N}$ is the set of natural numbers. We define an order $\leq$ on $L$
as follows:

$(n_{1},i_{1},j_{1})\leq(n_{2},i_{2},j_{2})$ if and only if:

$\bullet$ $n_{1}=n_{2},i_{1}=i_{2},j_{1}\leq j_{2}$;

$\bullet$ $n_{1}=n_{2},i_{2}=j_{2}=j_{1},i_{1}\leq i_{2}$;

$\bullet$ $n_{2}=n_{1}+1,j_{1}\leq i_{2},j_{2}=\infty$.

$L$ can be easily depicted as in Figure 1. Then $L$ is tapered closed in
$(L,\sigma(L))$, but $L\notin\mathbf{KF}(L)$ and $L\notin\\{cl(D)\mid
D\subseteq^{\uparrow}L\\}$.

###### Proof.

Claim 1: $L$ is tapered closed.

Let $A_{n}=\\{(n,i,j)\mid(i,j)\in\mathbb{N}\times(\mathbb{N}\cup\infty)\\}$.
Note that $\bigcup_{i=1}^{n}A_{i}=cl(A_{n}\backslash\max A_{n})$ for any
$n\in\mathbb{N}$ and $A_{n}\backslash\max A_{n}\subseteq^{\uparrow}L$. Hence,
$\bigcup_{i=1}^{n}A_{i}$ is tapered closed. Let
$B_{n}=\bigcup_{i=1}^{n}A_{i}$. It follows that
$\\{B_{n}\\}_{n\in\mathbb{N}}\subseteq^{\mathord{\uparrow}}\Gamma(L)$. Then we
have $L=\sup_{n\in\mathbb{N}}B_{n}$ is tapered closed.

Claim 2: $L\notin\\{cl(D)\mid D\subseteq^{\uparrow}L\\}$.

Suppose not, if there exists a directed subset $D$ of $L$ such that $cl(D)=L$.
We need to prove that $(D)_{\mathbb{N}}=\\{n\in\mathbb{N}\mid A_{n}\cap
D\neq\emptyset\\}$ is infinite. Assume $(D)_{\mathbb{N}}$ is finite. Let
$n_{0}=\max(D)_{\mathbb{N}}$. Then we have
$D\subseteq\bigcup_{i\in(D)_{\mathbb{N}}}A_{i}\subseteq\bigcup_{i=1}^{n_{0}}A_{i}=B_{n_{0}}$.
So $L=cl(D)\subseteq B_{n_{0}}$, which contradicts $B_{n_{0}}\subsetneqq L$.
Thus $(D)_{\mathbb{N}}$ is infinite. Let $n_{1}\in(D)_{\mathbb{N}}$. Pick
$(n_{1},i_{1},j_{1})\in D\cap A_{n_{1}}$. By the infiniteness of
$(D)_{\mathbb{N}}$, there exists $m\in(D)_{\mathbb{N}}$ such that $m\geq
n_{1}+2$. Choose $(m,i_{m},j_{m})\in D\cap A_{m}$. Obviously,
$\mathord{\uparrow}(n_{1},i_{1},j_{1})\subseteq A_{n_{1}}\cup A_{n_{1}+1}$ and
$\mathord{\uparrow}(m,i_{m},j_{m})\subseteq A_{m}\cup A_{m+1}$,
$(A_{n_{1}}\cup A_{n_{1}+1})\cap(A_{m}\cup A_{m+1})=\emptyset$. It follows
that
$\mathord{\uparrow}(n_{1},i_{1},j_{1})\cap\mathord{\uparrow}(m,i_{m},j_{m})=\emptyset$,
which contradicts that $D$ is directed.

Claim 3: $(K)_{\mathbb{N}}=\\{n\in\mathbb{N}\mid K\cap A_{n}\neq\emptyset\\}$
is finite for any $K\in Q(L)$.

Suppose not, if $(K)_{\mathbb{N}}$ is infinite. For any
$n\in(K)_{\mathbb{N}}$, pick $(n,i_{n},j)\in K\cap A_{n}$, Then
$(n,i_{n},\infty)\in K\cap A_{n}$. Let $F\subseteq_{fin}(K)_{\mathbb{N}}$,
$B_{F}=\\{\bigcup_{n\in(K)_{\mathbb{N}}\backslash
F}\mathord{\downarrow}(n,i_{n},\infty)\\}$. We need to verify that
$B_{F}\in\Gamma(L)$. Now let $D\subseteq^{\mathord{\uparrow}}B_{F}$. If $D$ is
finite, then $\sup D\in D\subseteq B_{F}$. Else, there exists a unique
$n\in(K)_{\mathbb{N}}$ such that
$D\subseteq\mathord{\downarrow}(n,i_{n},\infty)$. This implies that $\sup
D\in\mathord{\downarrow}(n,i_{n},\infty)\subseteq B_{F}$.
$\mathord{\downarrow}B_{F}=B_{F}$ is obvious. Note that $B_{F}\cap
K\neq\emptyset$ for any $F\subseteq_{fin}(K)_{\mathbb{N}}$. So we have
$K\cap\bigcap_{F\subseteq_{fin}(K)_{\mathbb{N}}}B_{F}\neq\emptyset$.
Therefore, there exists $(n,i,j)\in
K\cap\bigcap_{F\subseteq_{fin}(K)_{\mathbb{N}}}B_{F}$. Since
$(K)_{\mathbb{N}}$ is infinite, we have $m\in(K)_{\mathbb{N}}$ such that
$m\geq n+2$.

We now distinguish two cases:

Case 1, $n+1\in(K)_{\mathbb{N}}$: Then
$(n,i,j)\in\bigcap_{F\subseteq_{fin}(K)_{\mathbb{N}}}B_{F}\subseteq
B_{\\{n,n+1\\}}\cap A_{n}$, which contradicts $B_{\\{n,n+1\\}}\cap
A_{n}=\emptyset$.

Case 2, $n+1\notin(K)_{\mathbb{N}}$: Then
$(n,i,j)\in\bigcap_{F\subseteq_{fin}(K)_{\mathbb{N}}}B_{F}\subseteq
B_{\\{n\\}}\cap A_{n}$, which contradicts $B_{\\{n\\}}\cap A_{n}=\emptyset$.

Claim 4: $L\notin\mathbf{KF}(L)$.

Suppose not, $L\in\mathbf{KF}(L)$, then there exists $\\{K_{i}\\}_{i\in
I}\subseteq_{flt}Q(L)$ such that L is a minimal closed set that intersects all
members of $\\{K_{i}\\}_{i\in I}$ by Definition 2.5. Pick $i_{0}\in I$.
$(K_{i_{0}})_{\mathbb{N}}$ is finite by Claim 3. Now let
$m_{0}=\max(K_{i_{0}})_{\mathbb{N}}$. This implies that $K_{i_{0}}\subseteq
B_{m_{0}}$. We need to prove that $B_{m_{0}}\cap K_{i}\neq\emptyset$ for any
$i\in I$. For any $i\in I$, there exists $j\in I$ such that $K_{j}\subseteq
K_{i}\cap K_{i_{0}}$ because $\\{K_{i}\\}_{i\in I}$ is filter. It follows that
$\emptyset\neq K_{j}=B_{m_{0}}\cap K_{j}\subseteq B_{m_{0}}\cap K_{i}$. So
$L=B_{m_{0}}$ by the minimality of $L$, which contradicts $L\neq B_{m_{0}}$.

∎

Figure 2: Certain relations among some kinds of subsets of a $T_{0}$ space.

######  Example 4.2.

Let $J$ be Johnstone’s Example. Then $J\in\mathbf{KF}(J)$, but $J$ is not a
tapered closed set.

######  Remark 4.3.

By Example 4.1 and 4.2, we know that there is no relation between the tapered
closed subsets and the closed $KF$-subsets of a $T_{0}$ space $X$.

Figure 2 below shows certain relations among some kinds of subsets of a
$T_{0}$ space.

##  5 A direct characterization for $D$-completion

Let $P$ be a poset,
$\mathcal{H}=\\{\mathcal{D}\subseteq\Gamma(P)\backslash\emptyset\mid,\forall
A\in\mathcal{D},\forall a\in
A,\mathord{\downarrow}a\in\mathcal{D},cl_{d}(\mathcal{D})=\mathcal{D}\\}$ and
$A,B\in\Gamma(P)$. We say that $A~{}\mathrm{is}~{}\mathrm{beneath}~{}B$
denoted by $A\prec B$, if for every $\mathcal{D}\in\mathcal{H}$, the relation
$B\subseteq\sup\mathcal{D}$ always implies that $A\in\mathcal{D}$.

Notice that the relation which we define above is not an auxiliary relation
because the elements of $\mathcal{H}$ may not be lower sets.

######  Definition 5.1.

Let $P$ be a poset. An element $A$ of $\Gamma(P)$ is called _pre-C-compact_ if
$A\prec A$. We use $\mathcal{K}(\Gamma(P))$ to denote the set of all the
pre-$C$-compact elements of $P$.

Ho and Zhao introduce _C-continuous_ posets and $C$-compact elements in [19].
They proved that the $C$-compact elements of a poset $P$ are co-primes. They
find that the $C$-compact elements of $\Gamma(P)$ are more than the elements
of the $D$-completion of the posets. Now we want to find a way to reduce the
$C$-compact elements of $P$ such that they are equal.

######  Definition 5.2.

[19] Let $P$ be a poset and $x,y\in P$. We say that $x$ is beneath $y$,
denoted by $x\prec y$, if for every nonempty Scott closed set $C\subseteq P$
for which $\sup C$ exists, the relation $y\leq\sup C$ always implies that
$x\in C$. An element $x$ of a poset $P$ is called $C$-compact if $x\prec x$.

The pre-$C$-compact elements are $C$-compact by Definition 5.2. The following
example reveals that $C$-compact elements may not be pre-$C$-compact.

######  Example 5.3.

Let $J=\mathbb{N}\times(\mathbb{N}\cup\\{\infty\\})$, that is Johnstone’s
example. The partial order is
$(m,n)\leq(a,b)~{}\mathrm{iff}~{}\mathrm{either}~{}m=a~{}\mathrm{and}~{}n\leq
b~{}\mathrm{or}~{}b=\infty~{}\mathrm{and}~{}n\leq a$. That $J$ is $C$-compact
have been proved in Remark 5.3 of [19]. We now show that $J$ is not
pre-$C$-compact. Let $\mathcal{D}=\\{\mathord{\downarrow}x\mid x\in J\\}$.
Note that $\mathcal{D}\in\mathcal{H}$ and $\sup\mathcal{D}=J$ but
$J\not\in\mathcal{D}$.

The following proposition reveals some order-theoretic properties of the
lattice $(\Gamma(P),\subseteq)$ for an arbitrary poset $P$.

######  Proposition 5.4.

Let P be a poset. Then for any $\mathcal{D}\in\mathcal{H}$,
$\sup_{\Gamma(P)}\mathcal{D}=\bigcup\mathcal{D}$.

###### Proof.

Note that each member of $\mathcal{H}$ is a Scott-closed subset of $P$. So to
prove the equation, it suffices to show that $\bigcup\mathcal{D}\in\Gamma(P)$.
Obviously, $\bigcup\mathcal{D}$ is a lower set. Now Let $D$ be any directed
subset of $P$ contained in $\bigcup\mathcal{D}$ such that $\sup D$ exists in
$P$. We want to prove that $\sup D\in C$ for some $C\in\mathcal{D}$. First
note that $\mathcal{C}=\\{\mathord{\downarrow}d~{}|~{}d\in D\\}$ is a directed
subset of $\Gamma(P)$. Moreover, $\mathcal{C}\subseteq\mathcal{D}$ by the
definition of $\mathcal{D}$. Since $\mathcal{D}$ is a $d$-closed set, so
$\sup\mathcal{C}\in\mathcal{D}$. But $\sup\mathcal{C}$ is precisely
$\mathord{\downarrow}\sup D$. Hence $\sup D\in C$ for some $C\in\mathcal{D}$.
∎

######  Proposition 5.5.

Let $P$ be a poset. If $A\in\mathcal{K}(\Gamma(P))$, then $A$ is an
irreducible closed set.

###### Proof.

Suppose $A$ is pre-$C$-compact and $B,C\in\Gamma(P)$, $A\subseteq B\cup C$.
Let $\mathcal{D}=\mathord{\downarrow}\\{B,C\\}$. Then
$\mathcal{D}\in\mathcal{H}$ and $\sup\mathcal{D}=B\cup C$. Hence,
$A\in\mathcal{D}$, so $A\subseteq B$ or $A\subseteq C$. ∎

######  Lemma 5.6.

Let $P$ be a poset and $D$ be a directed subset of $P$. Then
$cl(D)\in\mathcal{K}(\Gamma(P))$.

###### Proof.

Let $\mathcal{D}\in\mathcal{H}$. Suppose $cl(D)\subseteq\sup\mathcal{D}$. Then
by Proposition 5.4, $D\subseteq\sup\mathcal{D}$ and
$\\{\mathord{\downarrow}d~{}|~{}d\in D\\}$ is a directed subset of
$\mathcal{D}$. Hence, $cl(D)=\sup\\{\mathord{\downarrow}d~{}|~{}d\in
D\\}\in\mathcal{D}$. ∎

######  Corollary 5.7.

Let $P$ be a poset. Then for each $x\in P$,
$\mathord{\downarrow}x\prec\mathord{\downarrow}x$ holds.

######  Theorem 5.8.

For any poset $P$, $\mathcal{K}(\Gamma(P))$ is a dcpo with the inclusion
order.

###### Proof.

Let $(A_{i})_{i\in I}$ be a directed subset in $\mathcal{K}(\Gamma(P))$. It
suffices to show that $\sup_{i\in I}A_{i}\prec\sup_{i\in I}A_{i}$. Suppose
$\mathcal{D}\in\mathcal{H}$ with $\sup_{i\in I}A_{i}\subseteq\sup\mathcal{D}$.
Then $A_{i}\subseteq\sup\mathcal{D}$ for all $i\in I$. Since
$A_{i}\in\mathcal{K}(\Gamma(P))$, it follows that $A_{i}\prec A_{i}$ and so
$A_{i}\in\mathcal{D}$. Because $\mathcal{D}$ is $d$-closed, this implies that
$\sup_{i\in I}A_{i}\in\mathcal{D}$. ∎

We write $\hat{P}=\mathcal{K}(\Gamma(P))$ with the relative topology of
$\Gamma(P)$.

######  Proposition 5.9.

Let $P$ be a poset. Then $\hat{P}$ is a monotone convergence space.

###### Proof.

It is easy to prove by Proposition 2.17. ∎

######  Lemma 5.10.

Let $P$ be a poset. If $A\subseteq P$ is tapered and closed, then
$A\in\mathcal{K}(\Gamma(P))$.

###### Proof.

Assume $P^{\vee}$ is the set of all tapered closed subsets and $A\in
P^{\vee}$, then $(P^{\vee},j)$ is the $D$-completion of $P$ by Lemma 2.14.
Define $f:P\rightarrow\mathcal{K}(\Gamma(P))$ by $f(x)=\mathord{\downarrow}x$
for all $x\in P$. Then, immediately, $f$ is continuous. As $(P^{\vee},j)$ is
the $D$-completion of $P$, it follows that there exists a unique continuous
map $\hat{f}:P^{\vee}\rightarrow\mathcal{K}(\Gamma(P))$ s.t. $f=\hat{f}\circ
j$. Thus sup$f(A)=\hat{f}(A)$ by Theorem 3.10 (2) of [19]. We need to prove
$A\in\mathcal{K}(\Gamma(P))$. Suppose not, $A\notin\mathcal{K}(\Gamma(P))$.
Since $\mathord{\downarrow}a\leq A$ for any $a\in A$ and $\hat{f}$ is
continuous, we have
$\mathord{\downarrow}a=\hat{f}(\mathord{\downarrow}a)\leq\hat{f}(A)=\sup
f(A)$. Hence, $A\varsubsetneqq\sup f(A)$, i.e. $\sup f(A)\cap A^{c}\neq{\O}$.
So we have $\sup f(A)\in\diamondsuit(A^{c})$. Because $\hat{f}$ is continuous,
this implies $\hat{f}^{-1}(\diamondsuit(A^{c}))$ is open in $P^{\vee}$ and
$A\in\hat{f}^{-1}(\diamondsuit(A^{c}))$. Hence, there exists $U\in\sigma(P)$
such that $A\in\diamondsuit U\subseteq\hat{f}^{-1}(\diamondsuit(A^{c}))$. This
means that $A\cap U\neq\emptyset$, then there exists $a\in A\cap U$ such that
$\mathord{\downarrow}a\in\diamondsuit
U\subseteq\hat{f}^{-1}(\diamondsuit(A^{c}))$, that is
$\hat{f}(\mathord{\downarrow}a)=\mathord{\downarrow}a\in\diamondsuit(A^{c})$
which contradicts $a\in A$. Thus we have shown the Lemma. ∎

######  Theorem 5.11.

Let $P$ be a poset. Then $\mathcal{K}(\Gamma(P))=cl_{d}(\eta(P))$ where
$\eta:P\rightarrow\Gamma(P)$ is defined by $\eta(x)=\mathord{\downarrow}x$ for
all $x\in P$, i.e. $(\hat{P},\eta)$ is the $D$-completion of $P$.

###### Proof.

For any $x\in P$, $\eta(x)=\mathord{\downarrow}x\in\mathcal{K}(\Gamma(P))$ by
Corollary 5.7. Then $\eta(P)\subseteq\mathcal{K}(\Gamma(P))$. We have shown
that $\mathcal{K}(\Gamma(P))$ is a subdcpo of $\Gamma(P)$, so
$cl_{d}(\eta(P))\subseteq\mathcal{K}(\Gamma(P))$.

Conversely, note that $cl_{d}(\eta(P))\in\mathcal{H}$ and $\sup
cl_{d}(\eta(P))=P$. If $A\in\mathcal{K}(\Gamma(P))$, then $A\subseteq\sup
cl_{d}(\eta(P))$. This implies $A\in cl_{d}(\eta(P))$ since $A\prec A$. ∎

From the proof of Theorem 5.11, we have the following:

######  Corollary 5.12.

Let $P$ be a poset. Then the pre-C-compact elements are exactly the tapered
closed sets.

######  Definition 5.13.

Let $(X,\tau)$ be a topological space. $X$ is called _determined by its
directed subsets_ if $\tau=\\{U\subseteq X~{}\mid cl(D)\cap
U\neq\emptyset~{}\mathrm{implies}~{}D\cap U\neq\emptyset\\}$ for all directed
subsets with respect to the order of specialization.

The following two theorems have the similar proof to that of posets.

######  Theorem 5.14.

Let $X$ be a topological space. Suppose $X$ is determined by its directed
subsets, then we can get $(\mathcal{K}(\Gamma(X)),\eta)$ is the $D$-completion
of $X$, where $\eta:X\rightarrow\Gamma(X)$ is defined by
$\eta(x)=\mathord{\downarrow}x$ for all $x\in X$.

######  Theorem 5.15.

Suppose $X$ is a topological space. Define
$\mathcal{H}=\\{\mathcal{D}\subseteq\Gamma(X)\mid\forall
A\in\mathcal{D},\forall a\in
A,\mathord{\downarrow}a\in\mathcal{D},cl_{d}(\mathcal{D})=\mathcal{D},cl({\bigcup\mathcal{D}})=\bigcup\mathcal{D}\\}$.
Then $(\mathcal{K}(\Gamma(X)),\eta)$ is the $D$-completion of $X$.

######  Corollary 5.16.

A topological space $X$ is a monotone convergence space if and only if for any
$A\in\mathcal{K}(\Gamma(X))$, there exists a unique point $x$ in $X$, such
that $A=\mathord{\downarrow}x$.

##  6 Reference

## References

  * [1] Y. Ershov.  On $d$-Spaces.  Theoretical Computer Science, 224 (1999): 59-72.
  * [2] Y. Ershov.  The $d$-rank of a topological space.  Algebra and Logic, 56 (2017): 98-107.
  * [3] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, D. S. Scott.  Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications.  Cambridge University Press, 2003.
  * [4] J. Goubault-Larrecq.  Non-Hausdorff Topology and Domain Theory, volume 22 of New Mathematical Monographs.  Cambridge University Press, 2013.
  * [5] R. Heckmann, K. Keimel  Quasicontinuous Domains and the Smyth Powerdomain.  Electronic Notes in Theoretical Computer Science, 298 (2013): 215-232.
  * [6] K. Keimel, J. D. Lawson.  $D$-completions and the $d$-topology.  Annals of Pure and Applied Logic 159 (2007): 292-306.
  * [7] J. D. Lawson.  Stably compact space.  Mathematical Structures in Computer Science, 21 (2011): 125-169.
  * [8] J. D. Lawson, G. Wu, X. Xi.  Well-filtered spaces, compactness, and the lower topology.  Houston Journal of Mathematics, 46 (2020): 283-294
  * [9] B. Liu, Q. Li, G. Wu.  Well-filterifications of topological spaces.  Topology and its Applications, 279 (2020): 107245.
  * [10] H. Miao, Z. Yuan, Q. Li.  A discussion of well-filterness and sobriety.  Topology and its applications, (2020), DOI: 10.1016/j.topol.2020.107450.
  * [11] C. Shen, X. Xi, X. Xu, D. Zhao.  On well-filtered reflections of $T_{0}$ space.  Topology and its Applications, 267 (2019): 106869.
  * [12] X. Xi, J. D. Lawson.  On well-filtered spaces and ordered sets.  Topology and its Applications, 228 (2017): 139-144.
  * [13] X. Xu and C. Shen, X. Xi, D. Zhao.  On $T_{0}$ spaces determined by well-filtered spaces.  Topology and its Applications, 282 (2020): 107323.
  * [14] X. Xu, C. Shen.  First countability, $\omega$-well-filtered spaces and reflections.  Topology and its Applications, 279 (2020): 107-255.
  * [15] X. Xu, D. Zhao.  On topological Rudin’s lemma, well-filtered spaces and sober spaces.  Topology and its Applications, 272 (2020): 107080.
  * [16] Z. Zhang, Q. Li.  A direct characterization of monotone convergence space completion.  Topology and its Applications, 230 (2017): 99-104.
  * [17] D. Zhao, T. Fan.  Dcpo-completion of posets.  Theoretical Computer Science, 411 (2010): 2167-2173.
  * [18] X. Jia.  Meet-continuity and locally compact sober dcpos. PhD thesis.  University of Birmingham, 2018.
  * [19] W. Ho, D. Zhao.  Lattices of Scott-closed sets.  Commentationes Mathematicae Universitatis Carolinae, 50 (2009): 297-314.


# A Declarative Validator for GSOS Languages

Matteo Cimini University of Massachusetts Lowell
Lowell, MA, USA<EMAIL_ADDRESS>
###### Abstract

Rule formats can quickly establish meta-theoretic properties of process
algebras. It is then desirable to identify domain-specific languages (DSLs)
that can easily express rule formats. In prior work, we have developed Lang-n-
Change, a DSL that includes convenient features for browsing language
definitions and retrieving information from them. In this paper, we use Lang-
n-Change to write a validator for the GSOS rule format, and we augment Lang-n-
Change with suitable macros on our way to do so. Our GSOS validator is
concise, and amounts to a few lines of code. We have used it to validate
several concurrency operators as adhering to the GSOS format. Moreover, our
code expresses the restrictions of the format declaratively.

##  1 Introduction

After creating a process algebra, the job of a language designer is not
finished yet. Ideally, the language designer would strive to prove that the
process algebra at hand affords the desired properties. Depending on the
process algebra, it may be interesting to establish whether bisimilarity is a
congruence, whether the language is deterministic, or whether some of its
operators satisfy certain algebraic laws such as commutativity and
associativity, to name a few.

The field of _language validation_ aims at developing methods and tools that
take a language definition as input, apply a static analysis on it, and
establish whether some property holds for the language. In the context of
concurrency theory, language validation has been best expressed with _rule
formats_ [35] over Structural Operational Semantics (SOS) specifications [37].
Rule formats state that if the rules that have been used to write the SOS
specification of a language conform to some syntactic restrictions then some
semantic property is guaranteed to hold. This approach has been applied to
automatically derive the congruence of strong bisimilarity [13, 27, 26, 41],
of weak bisimilarity [24, 12, 22], and to establish algebraic laws of
operators [19, 5, 36, 6], as well as deriving global properties such as
determinism [2] and bounded nondeterminism [23], and has also been applied to
probabilistic transitions [20, 29, 10] and contexts with binders [42, 7, 21],
to name a few applications.

It is then desirable to identify suitable domain-specific languages (DSLs)
that make it easier for designers of rule formats to express their formats and
automatically test them. This allows them to quickly test their new ideas, do
so on a suite of several process algebras at once, and have a path to rapidly
prototyping new formats. These tests are helpful for debugging a new rule
format while designers are still crafting a theoretical result.

Unfortunately, literature does not offer any DSL that has been specifically
designed for expressing rule formats. In this paper, we focus on an existing
DSL called Lang-n-Change [31, 33], which has been created for purposes other
than language validation but whose operations can be repurposed to write rule
formats. Lang-n-Change is a DSL for expressing language transformations, that
is, the input is a language definition and transformation instructions, and
the output is a modification of the language given as input. Consider the
typing rule of function application below on the left and its version with
subtyping on the right.

${\vbox{\hbox{\hbox{\small\small{(t-app)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
82.81047pt\vbox{\hbox{\hskip-82.81047pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\;e_{\\_}1:T_{\\_}1\to
T_{\\_}2$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\;e_{\\_}2:T_{\\_}1$}}}}\vbox{}}}\over\hbox{\hskip
37.9752pt\vbox{\vbox{}\hbox{\hskip-37.97519pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\;e_{\\_}1\;e_{\\_}2:T_{\\_}2$}}}}}}$}}}\quad\Longrightarrow\quad{\vbox{\hbox{\hbox{\small\small{(t-app')}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
124.52098pt\vbox{\hbox{\hskip-124.52097pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\;e_{\\_}1:T_{\\_}{11}\to
T_{\\_}2$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\;e_{\\_}2:T_{\\_}{12}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
T_{\\_}{12}<:T_{\\_}{11}$}}}}}\vbox{}}}\over\hbox{\hskip
37.9752pt\vbox{\vbox{}\hbox{\hskip-37.97519pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\;e_{\\_}1\;e_{\\_}2:T_{\\_}2$}}}}}}$}}}$

(t-app’) is a transformation of (t-app). Lang-n-Change provides linguistic
features to express such a transformation. For example, Lang-n-Change can
express the test that detects that $T_{\\_}1$ has been used twice in (t-app)
and assigns new distinct variables $T_{\\_}{11}$ and $T_{\\_}{12}$ to those
occurrences. Lang-n-Change also includes the operation for creating the
premise $T_{\\_}{12}<:T_{\\_}{11}$. Lang-n-Change has been applied to several
case studies that automatically transform SOS specifications, such as adding
subtyping [31, 17], pattern-matching [33], references [33], gradual typing
[32], as well as automatically deriving big-step semantics from small-step
style [31], and CK machines [17].

To express language transformations, Lang-n-Change offers fine-grained
operations for browsing SOS rules, their premises, and other components of the
language. In this paper, we explore the idea of using Lang-n-Change to express
rule formats. The idea is to devise a language transformation that ultimately
_does not_ modify the language in input, but that uses the operations of Lang-
n-Change to test the syntactic constraints prescribed by the rule formats, and
throw a runtime error when they are not met. We have written a checker for the
GSOS format [13] using Lang-n-Change. This is a well-known rule format, which
can establish the congruence of bisimilarity of many process algebras with
common operators. To better express some of the tests that are prescribed by
this format, we have augmented Lang-n-Change with suitable macros. These are
not extensions to the core language, nor to its evaluator. These are parsed
away into ordinary operations of Lang-n-Change.

We have used our tool to validate common concurrency operators that are known
to adhere to the GSOS format, such as the CCS parallel operator [30], the
synchronous parallel composition from CSP [28], and the projection operator of
ACP [11]. (Section 4 provides a complete list of our tests.) In total, we have
validated 18 concurrency operators. We have also performed a series of
negative tests. More specifically, we have given to our tool languages as
input that do not adhere to the GSOS format, and we confirm that our tool
rejects them, indeed.

Our GSOS validator amounts to 6 lines of code, which makes for a very concise
validator. Also, our code expresses the GSOS syntactic restrictions
declaratively. The work in this paper provides some evidence that Lang-n-
Change can be a useful tool for expressing rule formats.

The paper is organized as follows. Section 2 provides an overview of Lang-n-
Change. Section 3 presents our new macros and our GSOS validator. Section 4
discusses our evaluation. Section 5 discusses related work, and Section 6
concludes the paper.

##  2 Overview on Lang-n-Change

We repeat the relevant background on Lang-n-Change [31, 33] in this section.
Fig. 1 shows the tool pipeline of Lang-n-Change. The input consists of two
elements: A language definition and a language transformation. The output is
either a language definition, or an error message.

Language TransformationLanguage DefinitionLang-n-ChangeLanguage
DefinitionError Message Figure 1: Tool pipeline of Lang-n-Change

#### What Language Definitions?

Lang-n-Change works with languages defined in SOS. The input is a textual
representation of transition system specifications for SOS (with negative
transitions) [14]. The following is an example language that is input to Lang-
n-Change: A process algebra with the prefix operator, the interleaving
operator, and the sequence operator.

⬇

Label L ::= (a) | (b) | (c)

Process P ::= (null) | (a P) | (b P) | (c P) | (par P P) | (sequence P P)

(a P) \--(a)--> P.

(par P1 P2) \--(a)--> (par P1’ P2) <== P1 \--(a)--> P1’.

(par P1 P2) \--(a)--> (par P1 P2’) <== P2 \--(a)--> P2’.

(sequence P1 P2) \--(a)--> (sequence P1’ P2) <== P1 \--(a)--> P1’.

(sequence P1 P2) \--(a)--> P2’ <== P2 \--(a)--> P2’ /\ P1 -/-(a)-->

/\ P1 -/-(b)\-->

/\ P1 -/-(c)\-->.

... rest of the rules (same as the rules above but for the other labels)

That is, a grammar declares processes and labels, and a series of inference
rules define labeled transitions. Intuitively, <== means “provided that”, and
the formulae after that symbol are the premises of the rule. A formula such as
“P2 -/-(a)--->” means that $P_{\\_}2$ does not perform an $a$-transition. This
syntax does not present any novelty compared to other textual representations
for SOS, and is indeed inspired by the syntax employed in the Ott tool [39].

Some remarks on our example language: The GSOS format only works with a finite
set of labels [13]. For simplicity, we have chosen the set of actions
$\\{a,b,c\\}$. Moreover, the uniform setting for operators in GSOS is that of
a function symbol applied to processes. This is typically accommodated as
shown above: A prefix operator for each action.

#### What Language Transformations?

The following is the subset of the syntax of Lang-n-Change that is relevant to
this paper111We refer the reader to [31] and [33] for the syntax of Lang-n-
Change..

$\begin{array}[]{l@{\;\;}lcl}\text{\sf Expression}&e&::=&x\mid\textit{str}\mid
t\mid[e\;\ldots\;e]\mid\mathtt{head}\;e\mid\mathtt{tail}\;e\mid e@e\mid
e-e\mid\mathtt{map}(e,e)\mid e(e)\\\
&&&\mid\mathtt{rules}\mid\mathtt{premises}\mid\mathtt{conclusion}\mid\mathtt{self}\\\
&&&\mid{e}[p]:\;e\mid\mathtt{uniquefy}(e)\Rightarrow(x,x):e\mid\mathtt{getVars}(e)\\\
&&&\mid\mathtt{if}\;b\;\mathtt{then}\;e\;\mathtt{else}\;e\mid\mathtt{skip}\mid\mathtt{error}\;str\\\
\text{\sf Boolean Expr.}&b&::=&e=e\mid\mathtt{isVar}(e)\mid
b\;\mathtt{and}\;b\mid b\;\mathtt{or}\;b\mid\mathtt{not}\;b\\\ \text{\sf
Pattern}&p&::=&x\mid[p\;\ldots\;p]\mid predname\;p\mid opname\;p\mid
x\;p\end{array}$

We assume a set of operator names OpName ranged over by _opname_. OpName
contains elements such as $\mathtt{par}$, and $\mathtt{sequence}$, for
example. We also assume a set of predicate names PredName ranged over by
_predname_. PredName contains elements such as $\longrightarrow$ and
$\centernot\longrightarrow$. Lang-n-Change accommodates formulae uniformly in
abstract syntax
$(predname\;\mathit{arg}_{\\_}1\;\ldots\;\mathit{arg}_{\\_}n)$, as it does not
make assumptions on the language. Yet, the tool still reads transitions such
as $P\longrightarrow^{a}P^{\prime}$ with syntax P ---(a)---> P’ for the
convenience of users (see the example language above).

_Expression_ is the main syntactic category. Given an SOS specification, i.e.,
a language $\mathcal{L}$, and given an expression $e$, $e$ contains the
operations that will be applied to $\mathcal{L}$. Expressions can be
variables, strings (str), terms ($t$) (such as (par P1 P2) and (sequence P1
P2)), and lists with ordinary operations for extracting the head and the tail
of lists, appending two lists ($e~{}@~{}e$), and performing list difference
($e\;-\;e$). Expressions can also be maps $\mathtt{map}(e_{\\_}1,e_{\\_}2)$,
where $e_{\\_}1$ and $e_{\\_}2$ are lists. The first element of $e_{\\_}1$ is
the key of the first element of $e_{\\_}2$, and so on for the rest of the
elements222This schema is motivated in [31]. For example, it quickly maps
$T_{\\_}i$ to $T_{\\_}i^{\prime}$ from conclusions of subtyping rules such as
the conclusions $T_{\\_}1\to T_{\\_}2<:T_{\\_}1^{\prime}\to T_{\\_}2^{\prime}$
and $T_{\\_}1\times T_{\\_}2<:T_{\\_}1^{\prime}\times T_{\\_}2^{\prime}$..
Given a map $m$, $m(k)$ retrieves the value in $m$ associated with the key
$k$.

Lang-n-Change includes the special keywords $\mathtt{rules}$,
$\mathtt{premises}$, $\mathtt{conclusion}$, and $\mathtt{self}$. The keyword
$\mathtt{rules}$ returns a list with all the inference rules of the language
given as input. We shall describe the other keywords in the context of the
following operator.

The _selector operator_ ${e_{\\_}1}[p]:\;e_{\\_}2$ selects one by one the
elements of the list $e_{\\_}1$ that satisfy the pattern $p$ and executes the
body $e_{\\_}2$ for each of them. The selector returns a list with the values
produced by each evaluation of $e_{\\_}2$. The keyword $\mathtt{self}$, when
used in $e_{\\_}2$, returns the element of the list $e_{\\_}1$ that has been
selected at that iteration. A _pattern_ $p$ can be a variable, can attempt to
match a list (pattern $[p\;\ldots\;p]$), to match a formula that uses a
specific predicate name (pattern $\textit{predname}\;p$), to match a term with
a specific top-level operator (pattern $\textit{opname}\;p$), or can attempt
to match a formula or term with an unspecified top-level name (pattern
$x\;p$). As typical with pattern-matching, the variables that are used in the
pattern $p$ are bound in $e_{\\_}2$, and are instantiated at runtime. To make
an example, let us consider
${\mathtt{rules}}[P\longrightarrow^{L}P^{\prime}]:\;e_{\\_}2$ being executed
for the example language above (with prefix, $\mathtt{par}$, and
$\mathtt{sequence}$). $\mathtt{rules}$ evaluates to a list with all the rules
of the language. When the list contains rules, the pattern of the selector is
applied to match the conclusions of these rules. Therefore, the pattern
$P\longrightarrow^{L}P^{\prime}$ selects all the reduction rules. The first
iteration of $e_{\\_}2$ is executed with $P=\texttt{(a P)}$, $L=\texttt{(a)}$,
and $P^{\prime}=\texttt{P}$, and so on. (Notice that there is no clash between
pattern variables and the metavariables of rules, as they are separate in
Lang-n-Change.) For the convenience of programmers, simply writing
${\mathtt{rules}}[\longrightarrow]:\;e$ selects the rules that define
$\longrightarrow$ without specifying a full pattern. Also, $e[p]$ is a
shorthand for $e[p]:\mathtt{self}$, i.e., a list of the elements selected by
the pattern. Therefore, $\mathtt{rules}[\longrightarrow]$ simply selects all
reduction rules. The keyword $\mathtt{premises}$ can be used when the selector
operator works on rules, and returns the list of premises of the selected
rule. For example, ${\mathtt{rules}}[\longrightarrow]:\;\mathtt{premises}$
returns a list where each element is the list of premises of a rule such as
$[[],[\texttt{P1 ---(a)---> P1'}],[\texttt{P2 ---(a)---> P2'}],\ldots]$ in our
example process algebra. Similarly, the keyword $\mathtt{conclusion}$ returns
the conclusion of the selected rule.

$\mathtt{uniquefy}(e_{\\_}1)\Rightarrow(x,y):e_{\\_}2$ takes a list $e_{\\_}1$
of formulae, and returns a version of these formulae where multiple
occurrences of a metavariable have been assigned distinct metavariables. The
computation continues by executing $e_{\\_}2$. The list of new formulae is
passed to $e_{\\_}2$ as $x$. $\mathtt{uniquefy}$ also computes a map that
summarizes the changes that have been made to the original list of formulae
$e_{\\_}1$. This map is passed to $e_{\\_}2$ as $y$. This operation is useful
for transformations such as that of (t-app) into (t-app’) that we have
described in Section 1. Suppose that $l$ contains the list of premises of
(t-app), then
$\mathtt{uniquefy}(l)\Rightarrow(\emph{newPremises},\emph{mapOfChanges}):e$
will execute $e$ where _newPremises_ is the list
$[\Gamma\vdash\;e_{\\_}1:T_{\\_}{11}\to
T_{\\_}2,\Gamma\vdash\;e_{\\_}2:T_{\\_}{12}]$ and mapOfChanges is the map
$\\{T_{\\_}1\mapsto[T_{\\_}{11},T_{\\_}{12}]\\}$, which denotes that the
occurrences of $T_{\\_}1$ have been split into $T_{\\_}{11}$ and
$T_{\\_}{12}$333$\mathtt{uniquefy}$ can be used in a more fine-grained style,
as shown in [31], but we do not need that style in this paper..

$\mathtt{getVars}(e)$ returns the list of metavariables that are used in $e$
after it has been evaluated. We also have an if-statement, and a
$\mathtt{skip}$ operation that does not perform any operation. When
$\mathtt{if}$ has no $\mathtt{else}$ branch, as in
$\mathtt{if}\;b\;\mathtt{then}\;e$, it means
$\mathtt{if}\;b\;\mathtt{then}\;e\;\mathtt{else}\;\mathtt{skip}$. Error
$\mathtt{error}$ throws a runtime error and carries a string as error message.
The boolean conditions of the if-statement can check for syntactic equality,
whether $e$ is a metavariable with $\mathtt{isVar}(e)$, and can combine these
checks with boolean operations.

We do not discuss here the type checker of Lang-n-Change, which has been
presented in [31] and can reject, for example, ${e}[p]:\;e^{\prime}$ when $e$
is not a list, and other type errors.

##  3 A GSOS Validator

#### The GSOS Rule Format

We recall the GSOS format [13]. The following is the shape for GSOS rules:

$\inference{\\{x_{\\_}i\longrightarrow^{l_{\\_}{ij}}y_{\\_}{ij}\mid i\in
I,1\leq j\leq
m_{\\_}i\\}~{}\cup~{}\\{x_{\\_}j\centernot\longrightarrow^{l^{\prime}_{\\_}{jk}}\mid
j\in J,1\leq k\leq n_{\\_}j\\}}{(op\;x_{\\_}1\ldots
x_{\\_}h)\longrightarrow^{l}t}$

Notice that $x$s and $y$s are metavariables for metavariables, so that some
relation can be stated among different metavariables. In other words, $x$s and
$y$s all denote metavariables such as $P$, $P_{\\_}1$, $P_{\\_}2$, and so on.
We have that $x_{\\_}i$ and $y_{\\_}i$ are all distinct. $I$ and $J$ are
subsets of $\\{1,\dots,h\\}$, that is, $x$s in the premises come from the
conclusion, and each of them can be the subject of positive premises multiple
times, as well as the subject of negative premises multiple times. The
metavariables that occur in $t$ can only come from $x$s and $y$s, Finally,
labels $l$s are constants.

A rule that conforms to these restrictions is a GSOS rule. For example, all
the rules of the example process algebra in the previous section (with prefix,
$\mathtt{par}$, and $\mathtt{sequence}$) are GSOS rules.

Consider the following rule, which defines the behavior of the replication
operator.

$\qquad\quad\inference{(P\mid\;!P)\longrightarrow^{a}P^{\prime}}{!P\longrightarrow^{a}P^{\prime}}$

This rule is not a GSOS rule because the source of the premise is
$(P\mid\;!P)$ rather than a variable.

The following is a classic result of the meta-theory of SOS: If all the rules
of the language are GSOS rules then bisimilarity is a congruence for the
language [13].

###  3.1 New Macros for Lang-n-Change

We define the following macros in Lang-n-Change.

  * •

$e\;\mathtt{must\;match}\;p_{\\_}1\mid p_{\\_}2\mid\ldots\mid
p_{\\_}n\;\mathtt{otherwise}\;e^{\prime}\triangleq\mathtt{if}\;\mathtt{not}((e-e[p_{\\_}1]-e[p_{\\_}2]\ldots-e[p_{\\_}n])=[])\;\mathtt{then}\;e^{\prime}$.

Here, $e$ is a list. The idea is that each element of $e$ must match one of
the patterns $p_{\\_}1,p_{\\_}2,\ldots,p_{\\_}n$, otherwise we execute
$e^{\prime}$. To do that, we progressively subtract from $e$ its sublists
filtered by the patterns and check that the resulting list is empty. This
macro is useful to check that premises and conclusions have the correct shape.
We use this same “empty list”-test to check whether a list is a sublist of
another with: $e\;\mathtt{sublistOf}\;e^{\prime}\triangleq(e-e^{\prime})=[]$.
This macro is useful to check that the metavariables being used in some part
of the rule all come from the correct list of metavariables.

  * •

$\mathtt{match}\;e\;\mathtt{with}\;p\to
e^{\prime}\;\mathtt{otherwise}\;e^{\prime\prime}\triangleq\mathtt{if}\;[e][p]=[]\;\mathtt{then}\;e^{\prime\prime}\;\mathtt{else}\;e^{\prime}$.

Here, we check that $e$ matches the pattern $p$ and, if that is the case, we
execute $e^{\prime}$, otherwise we execute $e^{\prime\prime}$. To do so, we
create the list with only one element $[e]$ and use the selector to filter it
by pattern $p$. If the resulting list is empty then the pattern $p$ does not
succeed for $e$444[32] used this method for a simpler version of this macro..
When we omit “$\to e^{\prime}$” in this macro, it means “$\to\mathtt{skip}$”.
When we omit “$\mathtt{otherwise}\;e^{\prime\prime}$”, it means
“$\mathtt{otherwise}\;\mathtt{skip}$”. This macro is useful to check a pattern
for one element, as opposed to a list as above, and to specify a
$\mathtt{then}$\- versus $\mathtt{otherwise}$-reaction.

  * •

The following macros are useful to quickly access sources and targets of
transition formulae:

$\displaystyle\mathtt{premises.LTsources}$
$\displaystyle~{}\triangleq~{}(\mathtt{premises[\text{{$P\;$---$L$--->$\;P^{\prime}$]:$P$}}})~{}@~{}(\mathtt{premises[\text{{$P\;$--/-$L$--->]:$P$}}})$
$\displaystyle\mathtt{premises.LTtargets}$
$\displaystyle~{}\triangleq~{}\mathtt{premises[\text{{$P\;$---$L$--->$\;P^{\prime}$]:$P^{\prime}$}}}$
$\displaystyle\mathtt{conclusion.LTsource}$
$\displaystyle~{}\triangleq~{}\mathtt{head~{}([conclusion][\text{{$P\;$---$L$--->$\;P^{\prime}$]:$P$}}})$
$\displaystyle\mathtt{conclusion.LTtarget}$
$\displaystyle~{}\triangleq~{}\mathtt{head~{}([conclusion][\text{{$P\;$---$L$--->$\;P^{\prime}$]:$P^{\prime}$}}})$

Notice that $\mathtt{premises.LTsources}$ extracts the sources of both
positive and negative labeled transition formulae. “$\mathtt{LT}$” in
$\mathtt{LTsources}$ stands for labeled transition. We also have introduced
the analogous macros for (unlabeled) transitions $P\longrightarrow P$ such as
$\mathtt{Tsources}$, $\mathtt{Ttargets}$, and so on. We do not think that
these are ad-hoc macros in the context of language design. Labeled and
(unlabeled) transitions are so common that it is reasonable to have operations
that say, for example, “ _handle this premise as a labeled transition formula
and return its source_ ”. When a formula of another shape is given,
$\mathtt{premises.LTsources}$ and $\mathtt{premises.LTtargets}$ return an
empty list, and $\mathtt{head}$ fails at runtime for
$\mathtt{conclusion.LTsource}$ and $\mathtt{conclusion.LTtarget}$.

  * •

$\mathtt{distinctVars}(e)\;\mathtt{otherwise}\;e^{\prime}\triangleq$

$\mathtt{uniquefy}([(\emph{pname}\;e)])\Rightarrow(\emph{new},\emph{m}):\mathtt{if}\;\mathtt{not}(\emph{m}=\mathtt{map}([],[]))\;\mathtt{then}\;e^{\prime}$

Here, $e$ is a list of metavariables. We create the formula
$(\emph{pname}\;e)$ with an unused predicate name _pname_ just so we can pass
it to $\mathtt{uniquefy}$. If $m$ is the empty map $\mathtt{map}([],[])$ then
$\mathtt{uniquefy}$ did not detect any metavariable as being used more than
once, i.e., all metavariables in $e$ are distinct. $\mathtt{distinctVars}$
executes $e^{\prime}$ otherwise.

###  3.2 A GSOS Validator in Lang-n-Change

We now use Lang-n-Change to write a GSOS validator. We divide our task into
$5$ parts. These are $5$ checks that are meant to be performed in the order
they appear, i.e., first Part 1, then Part 2, and so on. They all return
$\mathtt{skip}$ if their corresponding check succeeds, otherwise they throw a
runtime error. Thanks to the operations of Lang-n-Change and our macros, these
checks are easy to read, and we may omit commenting on some of them. Below, we
use $\mathit{math}$ font for Lang-n-Change pattern variables.

  * •

Part 1: All premises are positive or negative transition formulae, and they
use constant labels.

⬇

rules[\-->]: premises must match $\mathit{P}\;$\--($\mathit{op}$ [])-->$\;\mathit{P^{\prime}}$ | $\mathit{P}\;$-/-($\mathit{op}$ [])-->

otherwise error msg

where $\texttt{{msg}}=$ “Premises must be either positive labeled transitions
or negative labeled transitions, and their label must be a constant”. A
constant is a term with a top-level operator and an empty list as arguments.

  * •

Part 2: All conclusions are transition formulae that use a constant label, and
are defined for an operator applied to metavariables as arguments. (Part 4
will check later that these metavariables are distinct, as they also need to
be distinct from $y$s.)

⬇

rules[\-->]: match conclusion with
($\mathit{op_{1}}~{}Ps\;$)--($\mathit{op_{2}}$ [])-->$\;\mathit{P^{\prime}}$
->

$\mathit{Ps}$[$\mathit{P}$]: if not(isVar($\mathit{P}$)) then error msg1

otherwise error msg2

where $\texttt{{msg}}_{\\_}1=$ “The operator that is the subject of the
conclusion must have all metavariables as arguments”, and
$\texttt{{msg}}_{\\_}2=$ “Conclusion formulae must be positive labeled
transitions with a constant label and must apply to an operator”.

  * •

Part 3: Sources of premises must come from $x$s of the conclusion, and $y$s
must be metavariables.

⬇

rules[\-->]:

if not(premises.LTsources sublistOf getVars(conclusion.LTsource))

then error msg1

else premises.LTtargets[$\mathit{P}$]: if not(isVar($\mathit{P}$)) then error
msg2

where $\texttt{{msg}}_{\\_}1=$ “Sources of premises must be arguments of the
operator in the source of the conclusion”, and $\texttt{{msg}}_{\\_}2=$
“Targets of premises must be metavariables”. Here,
$\mathtt{premises.LTsources}$, $\mathtt{conclusion.LTsource}$, and
$\mathtt{premises.LTtargets}$ are used after Part 1 and Part 2 have checked
that we do have labeled transition formulae.

  * •

Part 4: $x$s in the source of the conclusion, and $ys$ in the premises must
all be distinct.

⬇

rules[\-->]:

distinctVars (getVars(conclusion.LTsource) @ premises.LTtargets)

otherwise error msg

where $\texttt{{msg}}=$ “The arguments of the operator in the source of the
conclusion and the targets of the premises must all be distinct
metavariables”.

  * •

Part 5: Metavariables in the target of the conclusion come from $x$s and $y$s.

⬇

rules[\-->]:

if not(getVars(conclusion.LTtarget)

sublistOf

(getVars(conclusion.LTsource) @ premises.LTtargets))

then error msg

where $\texttt{{msg}}=$ “The metavariables in the target of the conclusion
must come from the source of the conclusion or from the targets of premises”.

##  4 Evaluation

We have implemented the macros that we have described in this paper [15]555The
flagship implementation of Lang-n-Change is that of [33] but it uses a syntax
that is more verbose than the one firstly proposed in [31]. We have then
implemented a lightweight evaluator of the Lang-n-Change DSL. The flagship
implementation of Lang-n-Change remains that of [33].. More precisely, we have
not changed the core language of Lang-n-Change, but we have added those
constructors to the surface language for the convenience of programmers. These
constructors are simply _parsed away_.

We have created a collection of test cases for our GSOS validator. We have
defined a base language definition with only the prefix operator $l.P$. This
language serves as a base to which we have added other features. Starting from
this, we have created one language for each of the following concurrency
operators: the interleaving parallel operator of CCS [30] (without process
communication), the full parallel operator with communication of CCS [30], the
synchronous parallel composition from CSP [28], the external choice of CCS,
the internal choice of CSP, projection of ACP [11], hiding of CSP, left merge
operator, the rename operator of CCS, the restriction operator of CCS, the
“hourglass” operator from [3], signaling [9], the disrupt operator, the
interrupt operator, the sequence operator ;, the priority operator, and a
while-loop operator. These operators are known to satisfy the GSOS
restrictions.

Our repo contains 18 concurrency operators, and we confirm that our GSOS
validator successfully executes the checks of Section 3.2 (Part 1–5) on all
these languages. That is, our tool validates the above-mentioned operators as
adhering to the GSOS format. We have also performed a series of negative
tests. Specifically, we have created languages that do not conform to the GSOS
restrictions described in Section 3. We confirm that our GSOS validator fails
in these cases and provide the corresponding error message.

Most of the checks of Section 3.2 can be written in one line despite having
presented them in multiple lines for readability. Overall, we could write a
GSOS validator in 6 lines of Lang-n-Change code. This is a remarkably concise
validator. Moreover, we believe that our code expresses the syntactic
restrictions of the GSOS format declaratively. The website of our tool reports
on all our tests [15].

##  5 Related Work

We are not aware of domain-specific languages that have been designed to
express rule formats.

There are only a few tools that validate rule formats. PREG Axiomatizer [4]
includes a checker for the GSOS format in around four hundred lines of Maude
code666We are thankful to Eugen-Ioan Goriac for kindly providing this
estimation in private communications via email, and also for clarifying that
such a GSOS checker is originally a part of PREG Axiomatizer rather than Meta
SOS. Notice that if we did not count the code for parsing, the checker is
estimated to be around 150 lines of Maude code.. Besides the format checks,
this part implements methods for retrieving information from languages. For
example, it implements functions for retrieving rules, searching premises, and
obtaining the variables used in formulae, to name a few. As it turns out,
these are functionalities that most language tools [40, 18, 25, 16, 38] need
to use. It appears that each tool makes use of a specific programming
language, stores languages as a data type of such programming language, and
reimplements these retrieval functions. This is an issue that Lang-n-Change
can alleviate by providing a DSL for expressing them concisely and
declaratively. It would be interesting to embed Lang-n-Change into programming
languages so that implementors can call its primitives.

Meta SOS [8] implements rule formats other than the GSOS format, hence a
direct comparison is not possible. The tool of Mousavi and Reniers [34]
provides a GSOS validator in Maude, and adopts a different implementation
approach than [4]. Process algebras are provided as Maude rewriting rules. The
tool then makes use of Maude introspective reflective features to explore the
shape of rules, premises, and so on. Language designers can certainly use this
approach to express their next rule formats, but it requires familiarity with
Maude, with its reflective library, and with a very particular style of meta-
programming that can have a steep learning curve. Some practitioners may find
the linguistic features of Lang-n-Change more intuitive and accessible.

##  6 Conclusion

Rule formats can quickly establish meta-theoretic properties of process
algebras. It is then desirable to identify DSLs that can easily express rule
formats and automatically test them. In this paper, we have observed that
Lang-n-Change offers convenient operations to interrogate operational
semantics. We have created macros on top of Lang-n-Change to better express
some of the checks that often occur in rule formats. We have then used Lang-n-
Change and our macros to implement the GSOS rule format. Overall, we have
written a full GSOS validator with only 6 lines of code, and we have used it
to validate several concurrency operators. Moreover, our code expresses the
GSOS restrictions declaratively.

In the future, we would like to apply our approach to other rule formats [35].
Several formats, including tyft, ntyft, path and panth [27, 26, 41], check for
distinct variables, impose a specific shape for transition formulae, and
retrieve sources and targets for analysis. We believe that Lang-n-Change and
our macros can be useful in those cases. However, there are possibly
challenging aspects of our approach. For example, there may be operations that
Lang-n-Change does not implement yet, and whose need may be discovered at the
attempt of capturing other rule formats. We have encountered an instance of
this scenario when using Lang-n-Change to automatically add references to
certain pure functional languages [33]. This endeavor requires lifting the
shape of reduction rules from $e\longrightarrow e$ to $e;\mu\longrightarrow
e;\mu$, where $\mu$ is the heap. In that occasion we have extended Lang-n-
Change with an operator called $\mathtt{lift}$ to specify the change of shape
for relations. That is, we have added a new operator that Lang-n-Change
lacked. (This operator turned out to be useful also for automating gradual
typing in [32], and it is therein described.) Another challenge is that Lang-
n-Change presents some limitations. For example, a characteristic of the GSOS
rule format is that its checks remain “local” and confined to the rule that
has been selected for analysis. Some rule formats, instead, need to maintain a
more global view on the process algebra at hand. An example is the rule format
that establishes the commutativity of operators (modulo bisimilarity) [36],
which compares multiple rules at the same time. Lang-n-Change seems to be best
suited to select one rule at a time. We will explore developing other DSLs, if
other linguistic designs are more suitable.

Our tool is publicly available, and all our tests are documented at its GitHub
repo [15].

## References

  * [1]
  * [2] Luca Aceto, Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi & Michel A. Reniers (2009): _Rule Formats for Determinism and Idempotence_.  In: Proceedings of the Third IPM International Conference on Fundamentals of Software Engineering, FSEN’09, Springer-Verlag, Berlin, Heidelberg, pp. 146–161, 10.1007/978-3-642-11623-08.
  * [3] Luca Aceto, Bard Bloom & Frits Vaandrager (1994): _Turning SOS Rules into Equations_.  Information and Computation 111(1), pp. 1–52, 10.1006/inco.1994.1040.
  * [4] Luca Aceto, Georgiana Caltais, Eugen-Ioan Goriac & Anna Ingolfsdottir (2011): _PREG Axiomatizer – A Ground Bisimilarity Checker for GSOS with Predicates_.  In Andrea Corradini, Bartek Klin & Corina Cîrstea, editors: International Conference on Algebra and Coalgebra in Computer Science (CALCO 2011), Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 378–385, 10.1007/978-3-642-22944-227.
  * [5] Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, Mohammad Reza Mousavi & Michel A. Reniers (2011): _SOS rule formats for zero and unit elements_.  Theoretical Computer Science 412(28), pp. 3045–3071, 10.1016/j.tcs.2011.01.024.
  * [6] Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza Mousavi & Michel A. Reniers (2012): _Rule formats for distributivity_.  Theoretical Computer Science 458, pp. 1–28, 10.1016/j.tcs.2012.07.036.
  * [7] Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir & Yolanda Ortega-Mallén (2019): _Rule Formats for Nominal Process Calculi_.  Logical Methods in Computer Science 15(4), 10.23638/LMCS-15(4:2)2019.
  * [8] Luca Aceto, Eugen-Ioan Goriac & Anna Ingólfsdóttir (2013): _Meta SOS - A Maude Based SOS Meta-Theory Framework_.  In Johannes Borgström & Bas Luttik, editors: Proceedings Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics, EXPRESS/SOS 2013, Buenos Aires, Argentina, 26th August, 2013, EPTCS 120, pp. 93–107, 10.4204/EPTCS.120.8.
  * [9] J. C. M. Baeten & J. A. Bergstra (1992): _Process Algebra with Signals and Conditions_.  In Manfred Broy, editor: Programming and Mathematical Method, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 273–323, 10.1007/978-3-642-77572-713.
  * [10] Falk Bartels (2002): _GSOS for probabilistic transition systems: (extended abstract)_.  Electronic Notes in Theoretical Computer Science 65(1), pp. 29–53, 10.1016/S1571-0661(04)80358-X.  CMCS’2002, Coalgebraic Methods in Computer Science (Satellite Event of ETAPS 2002).
  * [11] J.A. Bergstra & J.W. Klop (1984): _Process algebra for synchronous communication_.  Information and Control 60(1), pp. 109–137, 10.1016/S0019-9958(84)80025-X.
  * [12] Bard Bloom (1995): _Structural operational semantics for weak bisimulations_.  Theoretical Computer Science 146(1), pp. 25–68, 10.1016/0304-3975(94)00152-9.
  * [13] Bard Bloom, Sorin Istrail & Albert R. Meyer (1995): _Bisimulation Can’t Be Traced_.  Journal of the ACM 42(1), pp. 232–268, 10.1145/200836.200876.
  * [14] Roland Bol & Jan Friso Groote (1996): _The Meaning of Negative Premises in Transition System Specifications_.  Journal of the ACM 43(5), pp. 863–914, 10.1145/234752.234756.
  * [15] Matteo Cimini (2022): _GSOS-Validator_.  https://github.com/mcimini/gsos-validator.
  * [16] Matteo Cimini, Dale Miller & Jeremy G. Siek (2020): _Extrinsically typed operational semantics for functional languages_.  In: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, November 16-17, 2020, pp. 108–125, 10.1145/3426425.3426936.
  * [17] Matteo Cimini & Benjamin Mourad (2021): _Language Transformations in the Classroom_.  In Ornela Dardha & Valentina Castiglioni, editors: Proceedings Combined 28th International Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics, EXPRESS/SOS 2021, and 18th Workshop on Structural Operational SemanticsParis, France (online event), 23rd August 2021, EPTCS 339, pp. 43–58, 10.4204/EPTCS.339.6.
  * [18] Matteo Cimini & Jeremy G. Siek (2016): _The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems_.  In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’16, Association for Computing Machinery, New York, NY, USA, pp. 443–455, 10.1145/2837614.2837632.
  * [19] Sjoerd Cranen, MohammadReza Mousavi & Michel A. Reniers (2008): _A Rule Format for Associativity_.  In Franck van Breugel & Marsha Chechik, editors: CONCUR 2008 - Concurrency Theory, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 447–461, 10.1007/978-3-540-85361-935.
  * [20] Pedro R. D’Argenio, Matias David Lee & Daniel Gebler (2015): _SOS rule formats for convex and abstract probabilistic bisimulations_.  In Silvia Crafa & Daniel Gebler, editors: Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, EXPRESS/SOS 2015, Madrid, Spain, 31st August 2015, EPTCS 190, pp. 31–45, 10.4204/EPTCS.190.3.
  * [21] Marcelo Fiore & Sam Staton (2009): _A congruence rule format for name-passing process calculi_.  Information and Computation 207(2), pp. 209–236, 10.1016/j.ic.2007.12.005.
  * [22] Wan J. Fokkink (2000): _Rooted Branching Bisimulation as a Congruence_.  Journal of Computer and System Sciences 60(1), pp. 13–37, 10.1006/jcss.1999.1663.
  * [23] Wan J. Fokkink & Thuy Duong Vu (2003): _Structural operational semantics and bounded nondeterminism_.  Acta Informatica 39, pp. 501–516, 10.1007/s00236-003-0111-1.
  * [24] Rob J. van Glabbeek (2005): _On Cool Congruence Formats for Weak Bisimulations_.  In Dang Van Hung & Martin Wirsing, editors: Theoretical Aspects of Computing – ICTAC 2005, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 318–333, 10.1007/1156064721.
  * [25] Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann & Mira Mezini (2015): _Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers_.  In: 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), Onward! 2015, ACM, New York, NY, USA, pp. 137–150, 10.1145/2814228.2814239.
  * [26] Jan Friso Groote (1993): _Transition system specifications with negative premises_.  Theoretical Computer Science 118(2), pp. 263–299, 10.1016/0304-3975(93)90111-6.
  * [27] Jan Friso Groote & Frits Vaandrager (1992): _Structured operational semantics and bisimulation as a congruence_.  Information and Computation 100(2), pp. 202–260, 10.1016/0890-5401(92)90013-6.
  * [28] C. A. R. Hoare (1978): _Communicating Sequential Processes_.  Communications of the ACM 21(8), pp. 666–677, 10.1145/359576.359585.
  * [29] Ruggero Lanotte & Simone Tini (2009): _Probabilistic Bisimulation as a Congruence_.  ACM Transactions on Computational Logic 10(2), pp. 9:1–9:48, 10.1145/1462179.1462181.
  * [30] Robin Milner (1980): _A Calculus of Communicating Systems_.  Lecture Notes in Computer Science 92, Springer Berlin Heidelberg, Berlin, Heidelberg, 10.1007/3-540-10235-3.
  * [31] Benjamin Mourad & Matteo Cimini (2020): _A Calculus for Language Transformations_.  In: 46th International Conference on Current Trends in Theory and Practice of Informatics (SOFSEM 2020), Springer, pp. 547–555, 10.1007/978-3-030-38919-2_44.
  * [32] Benjamin Mourad & Matteo Cimini (2020): _A Declarative Gradualizer with Language Transformations_.  In Olaf Chitil, editor: IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages, Virtual Event / Canterbury, UK, September 2-4, 2020, ACM, pp. 44–54, 10.1145/3462172.3462190.
  * [33] Benjamin Mourad & Matteo Cimini (2020): _System Description: Lang-n-Change - A Tool for Transforming Languages_.  In Keisuke Nakano & Konstantinos Sagonas, editors: Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings, Lecture Notes in Computer Science 12073, Springer, pp. 198–214, 10.1007/978-3-030-59025-3_12.
  * [34] Mohammad Reza Mousavi & Michel A. Reniers (2006): _Prototyping SOS Meta-theory in Maude_.  Electronic Notes in Theoretical Computer Science 156(1), pp. 135–150, 10.1016/j.entcs.2005.09.030.  Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005).
  * [35] Mohammad Reza Mousavi, Michel A. Reniers & Jan F. Groote (2007): _SOS formats and meta-theory: 20 years after_.  Theoretical Computer Science 373(3), pp. 238–272, 10.1016/j.tcs.2006.12.019.
  * [36] MohammadReza Mousavi, Michel Reniers & Jan Friso Groote (2005): _A syntactic commutativity format for SOS_.  Information Processing Letters 93(5), pp. 217–223, 10.1016/j.ipl.2004.11.007.
  * [37] Gordon D. Plotkin (2004): _A structural approach to operational semantics_.  Journal of Logic and Algebraic Programming 60-61, pp. 17–139, 10.1016/j.jlap.2004.05.001.
  * [38] Michael Roberson, Melanie Harries, Paul T. Darga & Chandrasekhar Boyapati (2008): _Efficient Software Model Checking of Soundness of Type Systems_.  In Gail E. Harris, editor: Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, OOPSLA ’08, Association for Computing Machinery, New York, NY, USA, pp. 493–504, 10.1145/1449764.1449803.
  * [39] Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar & Rok Strniša (2010): _Ott: Effective tool support for the working semanticist_.  Journal of Functional Programming 20(1), pp. 71–122, 10.1017/S0956796809990293.
  * [40] Andrei Stefănescu, Daejun Park, Shijiao Yuwen, Yilong Li & Grigore Roşu (2016): _Semantics-based program verifiers for all languages_.  In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, pp. 74–91, 10.1145/2983990.2984027.
  * [41] C. Verhoef (1994): _A congruence theorem for structured operational semantics with predicates and negative premises_.  In Bengt Jonsson & Joachim Parrow, editors: CONCUR ’94: Concurrency Theory, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 433–448, 10.1007/978-3-540-48654-132.
  * [42] Axelle Ziegler, Dale Miller & Catuscia Palamidessi (2006): _A Congruence Format for Name-passing Calculi_.  Electronic Notes in Theoretical Computer Science 156(1), pp. 169–189, 10.1016/j.entcs.2005.09.032.  Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005).