# Response to Moffat’s Comment on “Towards Meaningful Statements in IR
Evaluation: Mapping Evaluation Measures to Interval Scales”

Marco Ferrante, Nicola Ferro, Norbert Fuhr Department of Mathematics “Tullio
Levi-Civita”, University of Padua, Italy (email:
ferrante@math.unipd.it)Department of Information Engineering, University of
Padua, Italy (email: ferro@dei.unipd.it)Faculty of Engineering, University of
Duisburg-Essen, Germany (email<EMAIL_ADDRESS>
###### Abstract

Moffat recently commented on our previous work published in the IEEE Access
journal. Our work focused on how laying the foundations of our evaluation
methodology into the representational theory of measurement can improve our
knowledge and understanding of the evaluation measures we daily use in
Information Retrieval (IR) and how it can shed light on the different types of
scales adopted by our evaluation measures; we also provided evidence, through
extensive experimentation, on the impact and effect of the different types of
scales on the subsequent statistical analyses, as well as on the impact of
departing from their assumptions. Moreover, we investigated, for the first
time in IR, the concept of _meaningfulness_ , intended as a specific sort of
invariance of the experimental statements and inferences you draw, and
proposed it as a way to ensure more valid and generalizabile results.

Moffat’s comments build on: (i) misconceptions about the representational
theory of measurement, such as what an interval scale actually is and what
axioms it has to comply with; (ii) they totally miss the central concept of
_meaningfulness_. Therefore, we reply to Moffat’s comments by properly framing
them in the representational theory of measurement and in the concept of
_meaningfulness_.

All in all, we can only reiterate what we said several times: the goal of this
research line is to theoretically ground our evaluation methodology – and IR
is a field where it is extremely challenging to perform any theoretical
advances – in order to aim for more robust and generalizable inferences –
something we currently lack in the field. Possibly there are other and better
ways to achieve this objective and these proposals could emerge from an open
discussion in the field and from the work of others. On the other hand,
reducing everything to a contrast on what is (or pretend to be) an interval
scale or whether all or none evaluation measures are interval scales may be
more a barrier from than a help in progressing towards this goal.

##  1 Introduction

We write this response in reply to Moffat’s comment [20] on our paper “Towards
Meaningful Statements in IR Evaluation: Mapping Evaluation Measures to
Interval Scales” [12].

We hope that this response will help to clarify some misunderstandings about
the _representational theory of measurement_ [17, 19, 26], in general, and the
notion of _meaningfulness_ [21] in particular – misconceptions central to
Moffat’s comment and leading to somehow fallacious arguments. We also hope
that this response will contribute to a _constructive and informed discussion_
in the field about these themes, which are often faced just as a contrast of
opinions.

Information Retrieval (IR) is an highly experimental field by nature and by
necessity, where we suffer from a lack of _generalizability_ of our results
and, consequently, the (almost) impossibility of _predicting_ the performance
of our systems. There is already some agreement on the need for “a better
understanding of the assumptions and user perceptions underlying different
metrics, as a basis for judging about the differences between methods” and on
the fact that “the assumptions underlying our algorithms, evaluation methods,
datasets, tasks, and measures should be identified and explicitly formulated.
Furthermore, we need strategies for determining how much we are departing from
these assumptions in new cases and how much this impacts on system
performance” [13]. In this respect, our work adheres to the representational
theory of measurement and proceeds step-by-step along its lines, in order to
understand and check assumptions and deviations as well as their implications
and consequences.

We welcome very much the comment by Moffat, as an exemplar way: (i) to open
the discussion to the community; (ii) to keep a written record of the
arguments, record which, today, helps researchers in taking informed decisions
and, in the future, will remain useful to motivate adopted approaches or to
further revise them; and, (iii) to have a transparent and frank exchanges of
views on a somewhat heartfelt topic. On the other hand, we would very much
prefer all of this not to be framed as a contrast between, in Moffat’s words,
“a bleak picture of past decades of IR evaluation” and “a more optimistic view
of IR evaluation and IR measurement”, because this rhetoric is apt to fuel
oppositions, leaving everything unchanged, rather than to tackle the real
issue, perhaps to favor the formulation of alternative and better solutions,
and to make overall progress.

The paper is organized as follows: Section 2 summarizes the main arguments in
Moffat’s comment; Section 3 introduces preliminary notions on the
representation theory of measurement and on _meaningfulness_ in order to set a
proper stage for the discussion; Section 4 provides our response to Moffat’s
main arguments; finally, Section 5 reports some concluding remarks.

##  2 Main Arguments by Moffat

As Moffat’s comment does not refer to any specific part of our paper to which
we could answer, we will start from his text instead, considering his main
arguments by directly quoting them. We also limit ourselves to the very major
arguments, avoiding to enter in too low level or too technical details,
because this would make our response too long, less clear, and of little use
to a researcher who wants to form their opinion or to contribute new ideas.

MA1

“If you do know where the numbers came from and why they have the values that
they do, and are confident that those values can be justified in reference to
the real world attribute that the mapping is designed to represent, then those
numbers may be used in your analysis and interpretation of that real world
equivalence” [20, p. 105570]

_MA1.1_

“While care needs to be exercised when choosing the metric that best fits the
user experience for any particular IR application […] once that match has been
decided, the values calculated by the effectiveness metric may be used as
simple numbers “that don’t remember where they came from” [18]; that is,
without regard to their origins in a categorical-scale SERP dataset” [20, p.
105576]

MA2

“Via a sequence of examples we have presented our view that all IR
effectiveness metrics can be considered to be interval scale measurements,
provided only that the mapping from SERP categories to numeric scores has a
real-world basis (an external validity) and can be motivated as corresponding
to the underlying usefulness of each SERP, as experienced by an identified
cohort of users as they carry out some identified search task” [20, p. 105576]

_MA2.1_

“There can be no ambiguity: RR is an interval scale measurement for those
users” [20, p. 105573]

_MA2.2_

“Any argument that RR – or any other metric – is an unsuitable categorical to
numeric mapping for measuring IR system effectiveness for some cohort of users
or some type of search task must be justified based on rhetoric about user
perceptions of SERP usefulness, or on observational data that measures SERP
usefulness via some agreed surrogate. Arguments against IR effectiveness
metrics cannot be based solely upon statements about the non-uniformity of the
intervals between the available measurement points” [20, pp. 105573–105574]

_MA2.3_

“We argue that most current IR metrics are well-founded, and, moreover, that
those metrics are more meaningful in their current form than in the proposed
“intervalized” versions” [20, p. 105564]

MA3

“We believe that intervalization should regarded with scepticism. There is no
requirement in Steven’s typology that interval scales be restricted to uniform
distances between the available measurement points; the requirement is simply
that the ratio between pairs of intervals be indicative of the corresponding
difference in the underlying attribute” [20, p. 105574]

_MA3.1_

“We have argued that the proposed intervalization of current IR effectiveness
metrics is neither required nor helpful. If the raw metric value is indeed a
defensible measurement of SERP usefulness and corresponds to the user’s
experience when they are presented with a member of that SERP category, then
equi-intervalizing those measurements via a different categorical to numeric
mapping must of necessity distort and alter any findings that arise, and thus
risk masking what would otherwise be valid conclusions. And if the raw metric
is not a defensible measurement of SERP usefulness for the search task at
hand, then equi-intervalizing its scores is unlikely to improve the situation”
[20, p. 105576]

_MA3.2_

“Moreover, altering the categorical to numeric mapping used to assign score to
SERPs changes the relativities being measured, and thus affects the outcome of
any subsequent arithmetic” [20, p. 105574]

##  3 Preliminaries on Measurement and Meaningfulness

Although we spent quite some effort to explain the following concepts in our
original article [12], as well as in previous and more formal work [10],
providing detailed discussion, references, and examples, we summarize here the
main concepts needed to articulate our response. In doing so, we also opt for
quoting as many passages as possible directly from the foundational works in
the area of measurement, in order to plainly report third party research,
without any additional interpretation on our side.

An introductory presentation of the concepts described below can be found in
general textbooks about measurement, such as Hand [15], or textbooks about
software metrics, such as Fenton and Bieman [7]. For a historical overview of
the evolution of the theory of measurement and its concepts, you can refer to
Díez [5, 6].

###  3.1 Measurement and Scales

“When measuring some attribute of a class of objects or events, we associate
numbers […] with objects in such a way that the properties of the attribute
are faithfully represented as numerical properties” [17, p. 1].

Suppose we aim at measuring the _length_ of rods. In the real world, we can
compare rods to determine which one is longer, i.e. we have a comparison
relation $\succ$ among rods; we can also concatenate rods together, i.e. we
have a concatenation operation $\circ$ among rods.

“A _relational structure_ is a set with one or more relations on that set”
[17, p. 8].

So, in our example, we have a set of rods $A$, a binary relation $a\succ b$ to
compare them, and a ternary relation $c=a\circ b$ to concatenate them.
Overall, $\langle A,\succ,\circ\rangle$ is an empirical relational structure
over the set of rods; it is called empirical because it exists in the real
world.

“The numerical assignment $\phi$ is a _homomorphism_ in the sense that it
sends $A$ into $\mathbb{R^{+}}$, $\succ$ into $>$, and $\circ$ into $+$ in
such a way that $>$ preserves the properties of $\succ$ and $+$ the properties
of $\circ$” [17, p. 8], where the properties are [17, p. 4]:

  1. 1.

$a\succ b$ if and only if $\phi(a)>\phi(b)$;

  2. 2.

$\phi(a\circ b)=\phi(a)+\phi(b)$.

These small excerpts from Krantz et al. [17], the first volume of the landmark
three-volume series on the foundations and mathematical formalization of
measurement, provide us with an intuitive understanding of the basic idea
behind the measurement theory: we use numbers as proxies of attributes of real
world objects, provided that the relations and operations among those numbers
keep corresponding to the relations and operations among real world objects.

This is formulated mathematically by saying that the assignment $\phi$, which
is called a _scale_ , is, in general, a homomorphism. Note that the
homomorphism is used because $\phi(a)=\phi(b)$ does not necessarily mean that
the rods $a$ and $b$ are the same rod but just that they have the same length.
However, if we consider the equivalence relation $\sim$ on $A$, then the
empirical relational structure $\langle A/{\sim},\succeq,\circ\rangle$ on the
quotient set $A/{\sim}$ becomes an _isomorphism_ to the numerical relational
structure $\langle\mathbb{R}^{+},\geq,+\rangle$. This further underlines the
_bijective_ nature of the correspondence between real world objects and
numbers, as well as their relations and operations.

The theory of measurement moves a further step forward and asks and additional
question: “Given a set of rods, a comparison relation $\succ$, and a
concatenation operation $\circ$, what assumptions concerning $\succ$ and
$\circ$ are necessary and/or sufficient to construct a real-valued function
$\phi$ that is order preserving and additive?” [17, p. 8]. Therefore, we have
to seek for characteristics of the real world objects, expressed in the form
of axioms, which guarantee the existence of a numerical scale $\phi$ with the
desired properties. More specifically, “a _representation theorem_ asserts
that if a given relational structure satisfies certain axioms, then a
homomorphism into a certain numerical relational structure can be constructed
[…] Measurement can be regarded as the construction of homomorphisms (scales)
from empirical relational structures of interest into numerical relational
structures that are useful” [17, p. 9].

However, the procedure for numerical assignment may look somewhat arbitrary or
there may exist several alternatives which are equally good. For example, in
the case of rods, which rod size is chosen as unit is an arbitrary matter,
leading to equivalent scales. In other cases, it may be less immediate to see
which choices are arbitrary and which are not. For example, when we count how
many times the unit rod $u$ has to be concatenated for obtaining a given rod
$a$, why do we record $n$ instead of $n^{2}$ or $\mathrm{e}^{n}$?

The notion of _permissible transformation_ serves exactly the purpose of
answering this question: “A transformation $\phi\rightarrow\phi^{\prime}$ is
permissible if and only if $\phi$ and $\phi^{\prime}$ are both homomorphisms
of $\langle A,R_{1},\ldots,R_{n}\rangle$ into the _same_ numerical structure
$\langle\mathbb{R},S_{1},\ldots,S_{n}\rangle$” [17, p. 12]. An _uniqueness
theorem_ has the purpose of determining what this permissible transformation
is and this is often not obvious at all.

For example, in the case of rod and length, Hölder [16] developed the first
proof that if $\phi$ is order preserving and additive, i.e. a homomorphism of
$\langle A,\succ,\circ\rangle$ into $\langle\mathbb{R}^{+},>,+\rangle$, the
same is true for $\alpha\phi$ when $\alpha>0$; moreover, if $\phi^{\prime}$ is
_any_ homomorphism of $\langle A,\succ,\circ\rangle$ into
$\langle\mathbb{R}^{+},>,+\rangle$, then $\phi^{\prime}=\alpha\phi$ for some
$\alpha>0$.

The uniqueness theorem grasps the fact that even if we refer to different
scales, e.g. meters or feet for length, they are actually equivalent from the
standpoint of the permissible transformation and they are required to be so,
otherwise the homomorphism with the real world $\langle A,\succ,\circ\rangle$
would be lost.

In this context, Stevens [25] defined the different types of scales, i.e.
different types of $\phi$ which have to comply with specific axioms in order
to guarantee desired properties. They can be briefly summarized as follows:

  * •

Nominal scale: it is used when entities of the real world can be placed into
different classes or categories on the basis of their attribute under
examination, without any notion of ordering among them. Any distinct numeric
representation of the classes is an acceptable measure but there is no notion
of magnitude associated with numbers.

Therefore, any arithmetic operation on the numeric representation has no
meaning. As a consequence, the only allowable statistics is counting number of
items in each class, that is mode and frequency.

The class of permissible transformations is the set of all _one-to-one
mappings_ , i.e. bijective functions: $\phi^{\prime}=\mathrm{f}(\phi)$, since
they preserve the distinction among classes.

  * •

Ordinal scale: it can be considered as a nominal scale where, in addition,
there is a notion of ordering among the different classes or categories. Any
distinct numeric representation which preserves the ordering is acceptable.
Therefore, the magnitude of the numbers is used just to represent the ranking
among classes.

Addition, subtraction or other mathematical operations have no meaning. As a
consequence, besides the statistics already allowed for nominal scales,
median, quantiles, and percentiles are appropriate, since there is a notion of
ordering.

The class of permissible transformations is the set of all the _monotonic
increasing functions_ , since they preserve the ordering:
$\phi^{\prime}=\mathrm{f}(\phi)$.

  * •

Interval scale: besides relying on ordered classes, it also captures
information about the size of the intervals that separate the classes. An
interval scale preserves order, as an ordinal one, and differences among
classes have meaning – but not their ratio.

Addition and subtraction are acceptable operations but not multiplication and
division. As a consequence, besides the statistics allowed for ordinal scales,
mean and standard deviation are allowable since they depend just on sum and
subtraction111Note that when we talk about admissible operations, we mean
operations between items of the scale. So, for example, a mean involves
summing items of the scale, e.g. temperature, and this is possible on an
interval scale. The fact that a mean also requires a division by the number
$N$ of items added together is not in contrast with saying that only addition
and subtraction are allowed, since $N$ is not an item of the scale..

The class of permissible transformations is the set of all the _affine
transformations_ : $\phi^{\prime}=\alpha\phi+\beta,\,\alpha>0$.

Temperature is the typical example of an interval scale.

  * •

Ratio scale it allows us to compute ratios among the different classes since
classes, which are ordered.

All the arithmetic operations are allowed. As a consequence, besides the
statistics allowed for interval scales, geometric and harmonic mean, as well
as coefficient of variation, are allowable since they depend on multiplication
and division.

The class of permissible transformations is the set of all the _linear
transformations_ : $\phi^{\prime}=\alpha\phi,\,\alpha>0$.

Length and mass are typical examples of ratio scales.

Let us focus on interval scales, which are the matter of discussion in our
paper and in Moffat’s comment.

The important characteristics of interval scales is that they need to be based
on _equally spaced_ objects in the real world which, in turn, leads to equi-
spacing of the numerical mapping.

Stevens does not explicitly mention the term “equi-spacing” in Table 1 at page
678, where he summarizes the scale types. However, he explicitly says this in
the section where he explains what interval scales are: “most psychological
measurement aspires to create interval scales, and it sometimes succeeds. The
problem usually is to devise operations for _equalizing the units_ of the
scales” [25, p. 679], providing also concrete examples like “ _equal
intervals_ of temperature are scaled off by noting _equal volumes_ of
expansion” [25, p. 679]. Other sentences like “the scale form remains
invariant when a constant is added” [25, p. 679] or “if the purpose of the
scale is still served when its values are squared or cubed, it is not even an
interval scale” [25, p. 680] implicitly assume an equally spaced scale.

Let us now see how an interval scale is defined from a formal point of view.
Rossi [22, p. 56] explains “How can we assign numbers (measures) to them
[objects] in such a way that they properly express both the order and the
distances? For doing so, we have to establish an _equally spaced graduation_
”. In particular, the equally spaced graduation is formulated in terms of a
so-called _solvability condition_ , requiring that whenever we have two not
equivalent intervals, it is always possible to find elements which correspond
to each treat of the equally spaced graduation Rossi [22, p. 57].

All the properties required required to real world object to allow for the
creation of an interval scale are determined by the definition of a
_difference structure_ , i.e. specific type of empirical relational structure.
Axiom 12.4 of Definition 3.12 (Difference Structure) [22, p. 59] expresses the
_solvability condition_ :

if $\displaystyle\Delta_{ab}\succeq_{d}\Delta_{cd}\succeq_{d}\Delta_{aa}$
$\displaystyle\text{then there exist }d^{\prime}\in A\text{ and
}d^{\prime\prime}\in A$ $\displaystyle\text{so that
}\Delta_{ad^{\prime}}\sim_{d}\Delta_{cd}\sim_{d}\Delta_{d^{\prime\prime}b}$

where $\Delta_{ab}$ is the _difference_ in the real world, not among numbers,
and $\succeq_{d}$ is a weak order among differences, again in the real world.

The definition of difference structure is then used in the _Representation
Theorem_ 3.17 to demonstrate the existence of an interval scale [22, p. 62]:

$\Delta_{ab}\succeq_{d}\Delta_{cd}\iff\phi(a)-\phi(b)\geq\phi(c)-\phi(d)$

based on the equivalence${\iff}$between the notion of difference in the real
world, consisting of equi-space objects, and the notion of different in the
numerical system.

Finally, the _Uniqueness Theorem_ 3.18 demonstrates that the affine
transformation $\phi^{\prime}=\alpha\phi+\beta$, $\alpha>0$, is the
permissible transformation for an interval scale [22, p. 62].

A similar formalization is adopted even more extensively by Krantz et al. [17,
pp. 136ff.].

As a consequence of the above formal definition of interval scale, the ratio
of differences among classes, i.e. the ratio of intervals, is allowed and
invariant to an affine transformation [17, p. 10]:

$\frac{\phi^{\prime}(a)-\phi^{\prime}(b)}{\phi^{\prime}(c)-\phi^{\prime}(d)}=\frac{[\alpha\phi(a)+\beta]-[\alpha\phi(b)+\beta]}{[\alpha\phi(c)+\beta]-[\alpha\phi(d)+\beta]}=\frac{\phi(a)-\phi(b)}{\phi(c)-\phi(d)}$

###  3.2 Meaningfulness

_Meaningfulness_ is a technical term in the theory of measurement, which
relies on a precise mathematical formulation and serves the purpose of
developing a whole theory around it. It should not be confused with
“meaningful” in the everyday language sense, i.e. making sense or being
credible.

For a rigourous and formal definition of _meaningfulness_ , please, refer to
Narens [21]. For the purpose of the present discussion, the intuitive
definition by Adams et al. [1, pp. 99-100] should suffice: “the criterion of
appropriateness for a statement about a statistical operation is that the
statement be _empirically meaningful_ in the sense that its truth or falsity
must be invariant under permissible transformations of the underlying scale”.

Therefore, meaningfulness focuses on the _invariance_ of the statements we
make and not on how much sense the make to us or how much true or false they
are. A statement like “A Chihuahua dog is three times taller than a Great Dane
dog” is false (possibly it does not make much sense either) and it stays false
independently from whether we are using meters or feet, i.e. under a
permissible linear transformation of the scale.

_Meaningfulness_ is not different from the notion of _invariance_ we have in
geometry, when we ask that a shape remains the same independently from
translation or rotation. We may wonder if _meaningfulness_ is asking too much
or a too strong property to a scale. But, asking that the truth value of a
statement remains the same under permissible transformations, which we have
seen to be an intrinsic and indispensable property of a scale, is the same as
asking that we draw the same inferences and conclusions independently from
whether we are using meters or feet. All of this does not seem much stricter
than asking, when we are looking at a cube, that, if we rotate it by 30
degrees, we still see a cube and not a sphere instead.

To clarify how _meaningfulness_ works, for example in the case of an interval
scale, we report here an example taken from our previous paper [12].

######  Example 1 (Meaningfulness for an Interval Scale).

The statement ‘Today the difference in temperature between Rome and Oslo is
twice as high as it was one month ago” is meaningful. Indeed, if, on the
Celsius scale, the temperature today in Rome is $20$ ∘C and in Oslo is $10$ ∘C
while one month ago it was $12$ ∘C and $7$ ∘C, leading to $20-10=10$ which is
twice as $12-7=5$, on the Fahrenheit scale we would have $68-50=18$ which is
twice as $53.6-44.6=9$.

Suppose now that we have recorded two sets of temperatures from Paris and
Rome: $T_{P}^{C}=[2\;2\;4\;8\;36]$ and $T_{R}^{C}=[1\;2\;4\;15\;34]$ in
Celsius degrees and, the same, $T_{P}^{F}=[35.6\;35.6\;39.2\;46.4\;96.8]$ and
$T_{R}^{F}=[33.8\;35.6\;39.2\;59.0\;93.2]$ in Fahrenheit degrees.

The statement “The median temperature in Paris is the same as in Rome” is
meaningful, since $4=4$ in Celsius degrees and $39.2=39.2$ in Fahrenheit
degrees; this is due to the fact that interval scales are also ordinal scales
and quantiles are an allowable operation on ordinal scales.

The statement “The mean temperature in Paris is less than in Rome” is
meaningful as well, since $10.4<11.2$ in Celsius degrees and $50.72<52.16$ in
Fahrenheit degrees; this is due to the fact that addition and subtraction are
allowable operations on an interval scale and, as a consequence, mean is
allowable as well.

Finally, the statement “The geometric mean of temperature in Paris is greater
than in Rome” is not meaningful, since $5.40>5.27$ in Celsius degrees and
$46.74<48.17$ in Fahrenheit degrees; this is due to the fact that the
geometric mean involves the multiplication and division of values, which is
not a permitted operation on an interval scale.

Examples along this lines could be done for an ordinal scale showing that the
median (or any other percentile) remains _meaningful_ for any monotonic
increasing transformation but not the mean (or even the geometric mean).

##  4 Response to Main Arguments by Moffat

###  4.1 MA1: If you do know where the numbers came from$\ldots$

We all agree that numbers should be chosen in such a way to reflect the
attribute of a real world object and, in this respect, taking into account
also the user experience does not make an exception.

However, at the same time, from the discussion in Section 3.1, it should be
clear that operations among the numbers should keep corresponding to
operations among real world objects and that numbers should keep their link
with the attribute of the real world object.

More formally, the theory of measurement explicitly says that you have to
create an _homomorphism_ between the real world and the numerical system in
order to ensure that relations and operations are preserved. Even more, the
theory of measurement makes a step further and states that among real world
objects certain properties should hold in order to ensure both the existence
(_representation theorem_) of a mapping to numbers with desired properties and
its uniqueness (_uniqueness theorem_). This is, for example, the case of the
_difference structure_ [22, Section 3.4, pp. 55ff.] and [17, Chapter 4, pp.
136ff.] which impose axioms among the real world objects that allow for
constructing an interval scale.

Moffat reported the famous statement by Lord [18] who, via the opinion of a
statistician in his story, says: “since the numbers don’t remember where they
came from, they always behave just the same way, regardless”. This statement
is often used to support the use of whatever operation on numbers, regardless
of any scale consideration and justified by practical usefulness. It is well
known that Lord’s paper has been debated for decades and we reported the
different viewpoints on it in our original paper [12].

In particular, Scholten and Borsboom [24], referred also by Moffat, show that
Lord’s argument is broken and you cannot compute a mean on an ordinal scale
just because “numbers don’t remember where they come from”. On the contrary,
Scholten and Borsboom demonstrate, also formally in their appendix, that the
reason why the means computed by the statistician in Lord’s paper can work is
completely different and not related to Lord’s statement. Indeed, the question
these means are answering is not about “football players numbers”, as Lord
assumes, but about the bias in the machines assigning those numbers to players
and how they have been tampered with. In other terms, the means are about a
different attribute of a different real world object (the machines and not the
football players) and Scholten and Borsboom showed that on this new attribute
it is possible to define a _bisymmetrical structure_ 222Note that the
_bisymmetrical structure_ used by Scholten and Borsboom [24] to define an
interval scale relies on a _solvability condition_ (equi-spacing) like those
used in the _difference structures_ mentioned in Section 3.1. which, in turn,
leads to an interval scale. Therefore, Scholten and Borsboom demonstrate that
even the Lord’s argument, when properly conceptualized, leads to and supports
Stevens’s definition of scales and the admissible operations on them.

Moreover, Moffat’s improperly uses the term meaningfulness in its everyday
language sense instead of its scientific one and this leads to wrong
conclusions. Sentences like “that factual relationship makes the mapping’s
values meaningful, and hence interpretable in terms of the attribute from
which the measurement was derived” [20, p. 105569] or “the intervals between
the salary points are meaningful; they represent salary differentials that
must be paid in a competitive market, measured in dollars” [20, p. 105569] are
wrong and, certainly, do not support Moffat’s thesis about the scales being
created. Indeed, as explained, _meaningfulness_ is a form of invariance of the
statements you make; it is not some “quality” of the numbers you assign and,
certainly, it does not express how much sense those numbers may have for you.

Overall, we think that MA1 is not correct and does not hold since, for all the
reasons explained above: even “if you do know where the numbers came from”,
this is not enough to them manipulate them as if “numbers don’t remember where
they come from”. In other terms, you should still take into consideration the
properties of the scale those numbers belong to and admissible operations on
that scale.

###  4.2 MA2: All IR effectiveness metrics can be considered to be interval
scale measurements

This argument by Moffat revolves around two severe misunderstandings.

The first misconception is that an interval scale does not require equally
spaced steps and, thus, whatever IR measure, even not equally spaced, can
pretend to be an interval scale. In Section 3.1, we have explained how the
_solvability condition_ , which express equi-spacing, is one of the axioms
required to define an interval scale. Therefore, whatever numerical mapping
not complying with the solvability condition does not match the definition and
cannot be called an interval scale. On the other hand, a scale where order is
preserved but intervals are not equi-spaced exists and it is an _ordinal
scale_ , as also remarked by Stevens [25, p. 679]: “on an ordinal scale […]
the successive intervals on the scale are unequal in size”.

The second misconception is about what _meaningfulness_ is in the theory of
measurement. Moffat just uses meaningfulness in its everyday language use of
‘making sense’ or ‘being credible’ along examples like when, in Sections II-D
and II-E of his paper, the provost analyses the professor salaries or like
when, in Section III-D of his paper, a market study leads to associate a
Search Engine Result Page (SERP) with a numerical mapping corresponding to
Reciprocal Rank (RR). All of this has nothing to do with the notion of
_meaningfulness_ in the theory of measurement and, as it should be clear from
the discussion in the previous section, having some rationale in assigning
numbers to objects does not imply or guarantee any scale properties, since
much more precise conditions should be met in this case, such as the
solvability condition. Therefore, a sentence like “most current IR metrics are
well-founded, and, moreover, […] those metrics are more meaningful in their
current form” [20, p. 105564] is wrong because _meaningfulness_ neither is a
property of a measure nor it is a synonym of well-founded nor it something you
can have “more” or “less”, because either a statement is _meaningful_
(invariant) or it is not. Even more, it is not a transitive property you can
use to justify some sort of chain of reasoning like: the assignment of numbers
makes sense to me (this is not _meaningfulness_), thus the measure makes sense
to me (this is not _meaningfulness_), thus the measure is an interval scale
(this is neither _meaningfulness_ nor being an interval scale), thus the
operations with that numbers make sense (this is not _meaningfulness_), thus
the statements/inferences make sense (here, in case, _meaningfulness_ would be
about the invariance of the statement and not their sense or truth).

Overall, we think that MA2 is not correct and does not hold since, for all the
reasons explained above: neither all IR measures are interval scales nor can
you always compute means over them and obtain _meaningful_ statements in a
scientific sense nor interval scales with intervals not equi-spaced exist.

As a side note, for these reasons, the examples by Moffat on professor
salaries and SERP pages/RR are not interval scales, as a consequence means
cannot be computed and the resulting statement cannot be _meaningful_.

###  4.3 MA3: We believe that intervalization should be regarded with
scepticism

The intervalization procedure we proposed in our paper proceeds along this
lines: (i) generate all the possible SERP; (ii) compute the desired IR
evaluation measure; (iii) sort the SERP according to the computed measure;
(iv) use the rank assigned to a SERP in (iii), which is an interval scale by
construction, in the subsequent analyses and statistical test. Since, as
already discussed in Section 4.2, not all the IR evaluation measures can be
considered to be interval scales, the proposed intervalization could find some
useful application.

As we already discussed in Section 3.1 the _solvability condition_ , i.e.
equally spaced steps, is an axiom to be complied with for having an interval
scale. Moreover, despite what Moffat reports about Stevens’s paper, Stevens
actually says that equi-spacing is a requirement for an interval scale.
Therefore, not holding, this should not be taken as a motivation for regarding
the proposed intervalization with scepticism.

In our paper, we do not claim that the purpose of intervalization is to make
an IR evaluation measure a more “defensible measurement of SERP usefulness”.
We actually assume that every IR evaluation measure embeds its own user
viewpoint – being it defensible or not – and, in case that a measure does not
comply with the requirements for an interval scale, our intervalization
procedure tries to preserve that user viewpoint as much as possible, still
obtaining an interval scale, by keeping the same ordering of SERP produced by
that user viewpoint. Therefore, not holding, this should not be taken as a
motivation for regarding the proposed intervalization with scepticism.

The fact that the intervalization procedure changes the numerical mapping and
that this will affect the subsequent computations is quite a trivial
observation and it is exactly the purpose of this transformation. Indeed, our
paper reports an extensive experimentation and a throughout investigation of
the impacts and effects of this transformation on several kinds of statistical
analyses and across several standard test collections.

Overall, what our intervalization procedure gives you is the possibility of
formulating _meaningful_ statements, doing its best at preserving the user
viewpoint embedded by an IR evaluation measure; it does not aim at all at
making that user viewpoint more or less defensible. Therefore, researchers may
or may not be interested in this approach and may or may not adopt it in their
own experiments; researchers may hopefully also come up with other more
brilliant solutions to ensure the _meaningfulness_ of our statements. Perhaps,
researchers will not be sceptic about our intervalization procedure for the
very same reasons suggested by Moffat or, maybe, Moffat will provide some
experimental evidence to substantiate his scepticism and, in case, to help
identifying and quantifying specific issues and how to address them.

###  4.4 Other Considerations

#### Our line of work

There is some misunderstanding in Moffat’s comment about how different lines
of our work relate together, often mentioning them all together as if they
were all the same, reporting the same claims, or as if all of them could be
refuted by the same argument.

Fuhr [14] listed a series of practices he considers common mistakes in IR
evaluation, among which averaging RR since it is not an interval scale, to be
avoided. Sakai [23] already commented on the prescriptive nature of Fuhr’s
paper and on what he considers or not to be mistakes; among them, Sakai
considers averaging RR a legitimate operation.

Our work commented by Moffat actually originates from a different line of
research. In our first work [8], we started to seek for a way to apply the
theory of measurement to the IR evaluation by finding axioms (swap and
replacement among relevant documents in a SERP) that described the properties
of a SERP in the real word, a prerequisite for understanding the properties of
IR evaluation measures and their scales. Later on, in [9] and, more
completely, in [10] we used the notion of _difference structure_ explained in
Section 3.1 to formally describe the SERP in the real world and from there to
derive an interval scale measure; this, in turn, allowed for verifying which
IR evaluation measures were an interval scale (at least with respect to the
identified difference structure) by seeking for an affine transformation.
Then, in [11] we started to explore the impact that using or not an interval
scale can have in IR experimentation. Finally, in our last work [12] commented
by Moffat, we joined our interests and proposed _meaningfulness_ as a
fundamental concept to be accounted for in IR evaluation, we further
investigated the implications of IR measures being interval scales or not and
why, and we proposed intervalization as a viable approach to ensure
_meaningfulness_. All in all, the objective of all these works is to provide
better theoretical foundations to our evaluation methods and concrete means to
achieve them. In this respect, these works are in the wake that others have
also followed but using different approaches, such as van Rijsbergen [27],
Bollmann [3], Bollmann and Cherniavsky [4], or Amigó and Mizzaro [2].

Finally, to the best of our knowledge, Ferrante et al. [11, 12] represent the
first works to experimentally investigate in a systematic way the impact of
scales and departure from their assumptions on different types of statistical
analyses.

In this perspective, the opening statement in the abstract of Moffat’s paper
“A sequence of recent papers, including in this journal, has considered the
role of measurement scales in information retrieval (IR) experimentation, and
presented the argument that (only) uniform-step interval scales should be
used. Hence, it has been argued, well-known metrics such as reciprocal rank,
expected reciprocal rank, normalized discounted cumulative gain, and average
precision, should be either discarded as measurement tools, or adapted so that
their metric values lie at uniformly-spaced points on the number line” is, at
best, reductive of what our work actually is and shifts the focus of the
discussion from laying theoretical and experimental foundations for our
experimental methodology to “use/do not use interval scales” or ”use/do not
use that evaluation measure”.

#### Recall Base

When talking about the problems caused by the recall base (RB), i.e. the
number of relevant documents for a topic, in Section IV-B of his paper, Moffat
states that “our contention in this work is that the measurement scale is
always the positive real number line, and hence that no question of alignment
(or not) of measurement points across sets of topics arises” since, always
according to Moffat, “from the point of view of Fuhr and Ferrante et al.,
those difficulties arise because normalization by RB means that the set of
generable measurement points for any query in a set of topics might not
numerically align with the available measurement points for other topics that
have different values for RB”.

Actually, the view point expressed in our paper is that measures which
explicitly depend on the recall base in their formulation lead to different
scales on different topics and, as a consequence, they cannot be compared or
mixed up, like you would not mix up length and mass, even if they are both
ratio scales. So, the issue is more profound than a lack of numerical
alignment.

Finally, in Section III-G of his paper, Moffat suggests that, differently from
what reported in our previous works, also  Rank-Biased Precision (RBP) with
$p=0.5$ is not an interval scale when, for example, a SERP is truncated at a
length $k$ greater than the recall base for that topic. Actually, what our
previous work shows is that RBP with $p=0.5$ is an interval scale when you
construct it by assuming that as many relevant documents as needed are
available, independently from the length of the SERP or its truncation point.
This is quite a reasonable assumption because you are creating a scale which
should hold for all the topics and not a different RBP scale for topics with
one relevant document, topics with two relevant documents, and so on. It is
the same line of reasoning you adopt when creating a scale for length: neither
you create a scale for a geographical area with small trees and a separate one
for another area with tall trees, nor you attempt to remove from a scale the
ticks corresponding to some trees for discovering later on that then it is no
more an interval scale.

As a side note, from a more formal point of view, as discussed in Section 3.1,
the _solvability condition_ [22, pp. 56ff.] and [17, pp. 136ff.], which leads
to equally spaced steps, is one of the properties required for constructing an
interval scale and, if your real world systems do not match it, e.g. because
they are limited to the case of a single relevant document, it trivially
follows that you can construct an interval scale. However, as explained
before, this is not an issue of the numerical mapping but rather of the real
world objects that lack the needed properties to create an interval scale.

##  5 Concluding Remarks

In this paper we have replied to Moffat’s comment on our previous work [12].
In doing so, we have briefly summarised the main concepts of the
representational theory of measurement [17, 19, 26] and of _meaningfulness_
[21] and we have explained why the main arguments by Moffat do not hold,
mainly because of misconceptions on these foundational concepts of the
representational theory of measurment and of _meaningfulness_.

As said, we really welcome Moffat’s comment on our work because it offers the
opportunity for an open discussion on important topics for our field. On the
other hand, we remark that we would prefer avoiding to frame the discussion as
the contrast between “a bleak picture of past decades of IR evaluation” and “a
more optimistic view of IR evaluation”, suggested by Moffat. First, in our
work we have never criticized or even deprecated past decades of IR
evaluation. Saying that scale properties of evaluation measures matter or that
_meaningfulness_ matters is neither criticizing nor deprecating past research,
at least any more than talking about modern building techniques can be seen as
a criticism of the pyramids. Nor we can consider as a criticism asking
ourselves which statements in the IR literature are _meaningful_ , i.e.
invariant, because this, for example, would help in knowing what could
potentially generalize in an easier way. Second, framing the question as a
contrast risks to amplify a “defensive attitude” in the field, rightly
motivated by safeguarding the seminal and paramount results of our past
research, at the expense of an open-minded discussion of the topic and of a
collaboration among researchers on how to develop and adopt better foundations
for our evaluation methods.

A general feeling that emerges from Moffat’s comment is that we overlook the
user viewpoint or we do not account for the user experience. On the contrary,
we very much agree with Moffat and all the rest of the research community that
the user satisfaction is the ultimate goal of our measurement and that
evaluation measures should embed some user viewpoint. We just say that we
should strive for this goal in the most sound and safe way possible; the
proposed intervalization procedure is just a simple example of such an
attempt. We actually do hope that this discussion and, especially, further
research by others will deliver much better solutions in this respect.

Both here and in our work commented by Moffat, we have indicated what this
“sound and safe way” could be, i.e. a deeper investigation and adoption of the
concept of _meaningfulness_ , at least in its scientific sense of
_invariance_. Indeed, _meaningfulness_ could be a way the achieve that
_generalizability_ of results that we lack in our field. Moreover,
_meaningfulness_ frees us from the debate on “should we average or not?” or
“should we give or adhere to prescriptions or not?” and focus our attention on
the real goal, i.e. _drawing more robust and generalizable inferences and
conclusions through better foundations of our evaluation methods_.

Finally, independently from the stance researchers may have on these topics,
we think that more thorough experimentation should be carried out in the field
also by others, in order to transfer theoretical models and considerations to
practice, to gain a better understanding of the implications of the different
choices, and to have a more informed discussion on the pros and cons of the
various alternatives.

## References

  * Adams et al. [1965] E. W. Adams, R. F. Fagot, and R. E. Robinson.  A theory of appropriate statistics.  _Psychometrika_ , 30:99–127, June 1965.
  * Amigó and Mizzaro [2020] E. Amigó and S. Mizzaro.  On the nature of information access evaluation metrics: a unifying framework.  _Information Retrieval Journal_ , 23(3):318–386, June 2020.
  * Bollmann [1984] P. Bollmann.  Two Axioms for Evaluation Measures in Information Retrieval.  In C. J. van Rijsbergen, editor, _Proc. of the Third Joint BCS and ACM Symposium on Research and Development in Information Retrieval_ , pages 233–245. Cambridge University Press, UK, 1984.
  * Bollmann and Cherniavsky [1980] P. Bollmann and V. S. Cherniavsky.  Measurement-theoretical investigation of the MZ-metric.  In C. J. van Rijsbergen, editor, _Proc. 3rd Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR 1980)_ , pages 256–267. ACM Press, New York, USA, 1980.
  * Díez [1997a] J. A. Díez.  A Hundred Years of Numbers. An Historical Introduction to Measurement Theory 1887-1990. Part I: The Formation Period. Two Lines of Research: Axiomatics and Real Morphisms, Scales and Invariance.  _Studies in History and Philosophy of Science_ , 28(1):167–185, March 1997a.
  * Díez [1997b] J. A. Díez.  A Hundred Years of Numbers. An Historical Introduction to Measurement Theory 1887-1990. Part II: Suppes and the Mature Theory. Representation and Uniqueness.  _Studies in History and Philosophy of Science_ , 28(2):237–265, June 1997b.
  * Fenton and Bieman [2014] N. E. Fenton and J. Bieman.  _Software Metrics: A Rigorous & Practical Approach_.  Chapman and Hall/CRC, USA, 3rd edition, 2014.
  * Ferrante et al. [2015] M. Ferrante, N. Ferro, and M. Maistro.  Towards a Formal Framework for Utility-oriented Measurements of Retrieval Effectiveness.  In J. Allan, W. B. Croft, A. P. de Vries, C. Zhai, N. Fuhr, and Y. Zhang, editors, _Proc. 1st ACM SIGIR International Conference on the Theory of Information Retrieval (ICTIR 2015)_ , pages 21–30. ACM Press, New York, USA, 2015.
  * Ferrante et al. [2017] M. Ferrante, N. Ferro, and S. Pontarollo.  Are IR Evaluation Measures on an Interval Scale?  In J. Kamps, E. Kanoulas, M. de Rijke, H. Fang, and E. Yilmaz, editors, _Proc. 3rd ACM SIGIR International Conference on the Theory of Information Retrieval (ICTIR 2017)_ , pages 67–74. ACM Press, New York, USA, 2017.
  * Ferrante et al. [2019] M. Ferrante, N. Ferro, and S. Pontarollo.  A General Theory of IR Evaluation Measures.  _IEEE Transactions on Knowledge and Data Engineering (TKDE)_ , 31(3):409–422, March 2019.
  * Ferrante et al. [2020] M. Ferrante, N. Ferro, and E. Losiouk.  How do interval scales help us with better understanding IR evaluation measures?  _Information Retrieval Journal_ , 23(3):289–317, June 2020.
  * Ferrante et al. [2021] M. Ferrante, N. Ferro, and N. Fuhr.  Towards Meaningful Statements in IR Evaluation. Mapping Evaluation Measures to Interval Scales.  _IEEE Access_ , 9:136182–136216, 2021.
  * Ferro et al. [2018] N. Ferro, N. Fuhr, G. Grefenstette, J. A. Konstan, P. Castells, E. M. Daly, T. Declerck, M. D. Ekstrand, W. Geyer, J. Gonzalo, T. Kuflik, K. Lindén, B. Magnini, J.-Y. Nie, R. Perego, B. Shapira, I. Soboroff, N. Tintarev, K. Verspoor, M. C. Willemsen, and J. Zobel.  Manifesto from Dagstuhl Perspectives Workshop 17442 – From Evaluating to Forecasting Performance: How to Turn Information Retrieval, Natural Language Processing and Recommender Systems into Predictive Sciences.  _Dagstuhl Manifestos, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Germany_ , 7(1):96–139, 2018.
  * Fuhr [2017] N. Fuhr.  Some Common Mistakes In IR Evaluation, And How They Can Be Avoided.  _SIGIR Forum_ , 51(3):32–41, December 2017\.
  * Hand [2010] D. J. Hand.  _Measurement Theory and Practice: The World Through Quantification_.  John Wiley & Sons, USA, 2010.
  * Hölder [1901] O. Hölder.  Die Axiome der Quantität und die Lehre vom Mass.  _Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, Mathematisch-Physikaliche Classe_ , 53:1–64, 1901.
  * Krantz et al. [1971] D. H. Krantz, R. D. Luce, P. Suppes, and A. Tversky.  _Foundations of Measurement. Additive and Polynomial Representations_ , volume 1.  Academic Press, New York, USA, 1971.
  * Lord [1953] F. M. Lord.  On the Statistical Treatment of Football Numbers.  _American Psychologist_ , 8(12):750–751, 1953\.
  * Luce et al. [1990] R. D. Luce, D. H. Krantz, P. Suppes, and A. Tversky.  _Foundations of Measurement. Representation, Axiomatization, and Invariance_ , volume 3.  Academic Press, New York, USA, 1990.
  * Moffat [2022] A. Moffat.  Batch Evaluation Metrics in Information Retrieval: Measures, Scales, and Meaning.  _IEEE Access_ , 10:105564–105577, 2022.
  * Narens [2002] L. Narens.  _Theories of Meaningfullness_.  Lawrence Erlbaum Associates, Mahwah (NJ), USA, 2002.
  * Rossi [2014] G. B. Rossi.  _Measurement and Probability. A Probabilistic Theory of Measurement with Applications_.  Springer-Verlag, New York, USA, 2014.
  * Sakai [2020] T. Sakai.  On Fuhr’s Guideline for IR Evaluation.  _SIGIR Forum_ , 54(1):p14:1–p14:8, June 2020\.
  * Scholten and Borsboom [2009] A. Z. Scholten and D. Borsboom.  A reanalysis of Lord’s statistical treatment of football numbers.  _Journal of Mathematical Psychology_ , 53(2):69–75, April 2009.
  * Stevens [1946] S. S. Stevens.  On the Theory of Scales of Measurement.  _Science, New Series_ , 103(2684):677–680, June 1946.
  * Suppes et al. [1989] P. Suppes, D. H. Krantz, R. D. Luce, and A. Tversky.  _Foundations of Measurement. Geometrical, Threshold, and Probabilistic Representations_ , volume 2.  Academic Press, New York, USA, 1989.
  * van Rijsbergen [1974] C. J. van Rijsbergen.  Foundations of Evaluation.  _Journal of Documentation_ , 30(4):365–373, 1974.

  *[IR]: Information Retrieval
  *[SERP]: Search Engine Result Page
  *[RR]: Reciprocal Rank
  *[RBP]: Rank-Biased Precision


$\displaystyle\operatorname{rtg}(r_{1}*r_{2})$
$\displaystyle=\operatorname{rtg}(r_{1})^{(b(r_{1},r_{2}))}\operatorname{rtg}(r_{2})$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{1})(\operatorname{rtg}(r_{1})^{(b(r_{1},r_{2}))}\operatorname{rtg}(r_{2}))+_{b(r_{1},r_{2})}\operatorname{rtg}(r_{2})$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r_{1})+_{b}0)(\operatorname{rtg}(r_{1})^{(b(r_{1},r_{2}))}\operatorname{rtg}(r_{2}))+_{b(r_{1},r_{2})}(\operatorname{rtg}(r_{2})+_{b}0)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r_{1})(\operatorname{rtg}(r_{1})^{(b(r_{1},r_{2}))}\operatorname{rtg}(r_{2}))+_{b}0)+_{b(r_{1},r_{2})}(\operatorname{rtg}(r_{2})+_{b}0)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r_{1})(\operatorname{rtg}(r_{1})^{(b(r_{1},r_{2}))}\operatorname{rtg}(r_{2}))+_{b(r_{1},r_{2})}\operatorname{rtg}(r_{2}))+_{b}0$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{1}*r_{2})+_{b}0$

This concludes the proof of the intermediary property.

Let $c=b(r,s)$, the maximal test separating $r$ from $s$. The key insight here
is that $b\leq c$, so that $x+_{c}y\equiv_{\dagger}(x+_{b}z)+_{c}y$. With this
observation in hand, we can further calculate

$\displaystyle\operatorname{rtg}(r+s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{c}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r)+_{b}0)+_{c}(0+_{b}\operatorname{rtg}(s))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{b}(0+_{c}(0+_{b}\operatorname{rtg}(s)))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{b}((0+_{c}0)+_{b\vee
c}\operatorname{rtg}(s))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{b}(0+_{c}\operatorname{rtg}(s))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{b}\operatorname{rtg}(s)$

as well as

$\displaystyle\operatorname{rtg}(r*s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)^{(c)}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r)+_{b}0)^{(c)}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r)+_{b}0)(\operatorname{rtg}(r)^{(c)}\operatorname{rtg}(s))+_{c}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r)(\operatorname{rtg}(r)^{(c)}\operatorname{rtg}(s))+_{b}0)+_{c}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)(\operatorname{rtg}(r)^{(c)}\operatorname{rtg}(s))+_{b}(0+_{c}\operatorname{rtg}(s))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)(\operatorname{rtg}(r)^{(c)}\operatorname{rtg}(s))+_{b}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)(\operatorname{rtg}(r*s))+_{b}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)^{(b)}\operatorname{rtg}(s)$

This concludes the proof overall.

See 8

###### Proof

By induction on the proof of $r\equiv_{*}s$. In the base case, we verify the
one-free star behaviour axioms directly.

  * •

Every $r\in\mathsf{Det}$ such that $r+r\in\mathsf{Det}$ is $r\equiv_{*}0$, so
indeed
$\operatorname{rtg}(r+r)=\operatorname{rtg}(r)+_{1}\operatorname{rtg}(r)\equiv_{\dagger}\operatorname{rtg}(r)$.

  * •

If $r\perp_{b}s$, then

$\displaystyle\operatorname{rtg}(r+s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{b}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(s)+_{\bar{b}}\operatorname{rtg}(r)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(s+r)$
$\displaystyle\operatorname{rtg}((r+s)+t)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r)+_{b}\operatorname{rtg}(s))+_{c}\operatorname{rtg}(t)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{bc}(\operatorname{rtg}(s)+_{c}\operatorname{rtg}(t))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)+_{bc}\operatorname{rtg}(s+t)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r+(s+t))$
$\displaystyle\operatorname{rtg}((r+s)t)$
$\displaystyle=\operatorname{rtg}(r+s)\operatorname{rtg}(t)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(r)+_{b}\operatorname{rtg}(s))\operatorname{rtg}(t)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)\operatorname{rtg}(t)+_{b}\operatorname{rtg}(s)\operatorname{rtg}(t)$
$\displaystyle\operatorname{rtg}(e(fg))$
$\displaystyle=\operatorname{rtg}(e)\operatorname{rtg}(fg)$
$\displaystyle=\operatorname{rtg}(e)(\operatorname{rtg}(f)\operatorname{rtg}(g))$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(e)\operatorname{rtg}(f))\operatorname{rtg}(g)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}((ef)g)$
$\displaystyle\operatorname{rtg}(r*s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)^{(b)}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)(\operatorname{rtg}(r)^{(b)}\operatorname{rtg}(t))+_{b}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r)\operatorname{rtg}(r*t)+_{b}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r(r*t))+_{b}\operatorname{rtg}(s)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r(r*t)+s)$

For the inductive step, we need to consider the congruence properties and the
Horn rule.

  * ($+$)

Suppose the proof ends with

$\prftree{r_{1}=r_{2}\qquad s_{1}=s_{2}}{r_{1}+s_{1}=r_{2}+s_{2}}$

and assume that
$\operatorname{rtg}(r_{i})\equiv_{\dagger}\operatorname{rtg}(s_{i})$. We are
also assuming that $r_{i}+s_{i}$ is deterministic, so we must have
$b_{1},b_{2}\in\mathsf{BExp}$ such that $r_{i}\perp_{b_{i}}s_{i}$, $i=1,2$.
However, since $r_{1}\equiv_{*}r_{2}$ and $s_{1}\equiv_{*}s_{2}$,
$r_{1}\perp_{b}s_{1}$ if and only if $s_{1}\perp_{b}s_{2}$, so we may as well
take $b_{1}=b_{2}=b$. We have

$\displaystyle\operatorname{rtg}(r_{1}+s_{1})$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{1})+_{b}\operatorname{rtg}(s_{1})$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{2})+_{b}\operatorname{rtg}(s_{2})$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{2}+s_{2})$

  * ($*$)

Suppose the proof ends with

$\prftree{r_{1}=s_{1}\qquad r_{2}=s_{2}}{r_{1}*s_{1}=r_{2}*s_{2}}$

and assume that $\operatorname{rtg}(r_{i})=\operatorname{rtg}(s_{i})$,
$i=1,2$. Again, we obtain a common $b\in\mathsf{BExp}$ such that
$r_{i}\perp_{b}s_{i}$ for $i=1,2$. We have

$\displaystyle\operatorname{rtg}(r_{1}*s_{1})$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{1})^{(b)}\operatorname{rtg}(s_{1})$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{2})^{(b)}\operatorname{rtg}(s_{2})$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(r_{2}*s_{2})$

  * •

Suppose the proof ends with the Horn rule

$\prftree{t=rt+s}{t=r*s}$

and assume that
$\operatorname{rtg}(t)\equiv_{\dagger}\operatorname{rtg}(rt+s)$. Since we are
also assuming that $r*s\in\mathsf{Det}$, there is a $b\in\mathsf{BExp}$ such
that $r\perp_{b}s$. We also have $rt\perp_{b}s$, so

$\operatorname{rtg}(t)\equiv_{\dagger}\operatorname{rtg}(r)\operatorname{rtg}(t)+_{b}\operatorname{rtg}(s)$

It follows that

$\operatorname{rtg}(t)\equiv_{\dagger}\operatorname{rtg}(r)^{(b)}\operatorname{rtg}(s)\equiv_{\dagger}\operatorname{rtg}(r*s)$

We will need the following lemma in what follows.

###### Lemma 27

If $e\equiv_{\dagger}f$, then
$\operatorname{gtr}(e)\equiv_{*}\operatorname{gtr}(f)$.

###### Proof

By induction on the proof of $e\equiv_{*}f$. In the base case, we consider the
skip-free GKAT axioms directly.

  * •

For $e+_{b}e\equiv_{\dagger}e$, we derive

$\operatorname{gtr}(e+_{b}e)\equiv_{*}b\operatorname{gtr}(e)+\bar{b}\operatorname{gtr}(e)\equiv_{*}1\operatorname{gtr}(e)\equiv_{*}\operatorname{gtr}(e)$

  * •

For $e+_{1}f\equiv_{\dagger}e$, we derive

$\operatorname{gtr}(e+_{1}f)\equiv_{*}1\operatorname{gtr}(e)+0\operatorname{gtr}(f)\equiv_{*}\operatorname{gtr}(e)$

  * •

For $e+_{b}f\equiv_{\dagger}f+_{\bar{b}}e$, we derive

$\displaystyle\operatorname{gtr}(e+_{b}f)$
$\displaystyle\equiv_{*}b\operatorname{gtr}(e)+\bar{b}\operatorname{gtr}(f)$
$\displaystyle\equiv_{*}\bar{b}\operatorname{gtr}(f)+b\operatorname{gtr}(e)$
$\displaystyle\equiv_{*}\operatorname{gtr}(f+_{\bar{b}}e)$
$\displaystyle\operatorname{gtr}((e+_{b}f)g)$
$\displaystyle\equiv_{*}(b\operatorname{gtr}(e)+\bar{b}\operatorname{gtr}(f))\operatorname{gtr}(g)$
$\displaystyle\equiv_{*}b\operatorname{gtr}(e)\operatorname{gtr}(g)+\bar{b}\operatorname{gtr}(f)\operatorname{gtr}(g)$
$\displaystyle\equiv_{*}\operatorname{gtr}(eg+_{b}fg)$
$\displaystyle\operatorname{gtr}(e(fg))$
$\displaystyle\equiv_{*}\operatorname{gtr}(e)\operatorname{gtr}(fg)$
$\displaystyle\equiv_{*}\operatorname{gtr}(e)(\operatorname{gtr}(f)\operatorname{gtr}(g))$
$\displaystyle\equiv_{*}(\operatorname{gtr}(e)\operatorname{gtr}(f))\operatorname{gtr}(g)$
$\displaystyle\equiv_{*}\operatorname{gtr}((ef)g)$
$\displaystyle\operatorname{gtr}(e^{(b)}f)$
$\displaystyle\equiv_{*}(b\operatorname{gtr}(e))*(\bar{b}\operatorname{gtr}(f))$
$\displaystyle\equiv_{*}(b\operatorname{gtr}(e))((b\operatorname{gtr}(e))*(\bar{b}\operatorname{gtr}(f)))+\bar{b}\operatorname{gtr}(f)$
$\displaystyle\equiv_{*}b(\operatorname{gtr}(e)((b\operatorname{gtr}(e))*(\bar{b}\operatorname{gtr}(f))))+\bar{b}\operatorname{gtr}(f)$
$\displaystyle\equiv_{*}b\operatorname{gtr}(e(e^{(b)}f))+\bar{b}\operatorname{gtr}(f)$
$\displaystyle\equiv_{*}\operatorname{gtr}(e(e^{(b)}f)+_{b}f)$

For the inductive step, we need to consider the congruence properties and the
Horn rule.

  * ($+_{b}$)

Suppose the proof ends with

$\prftree{e_{1}=f_{2}\qquad e_{2}=f_{2}}{e_{1}+_{b}f_{1}=e_{2}+_{b}f_{2}}$

and assume that
$\operatorname{gtr}(e_{i})\equiv_{*}\operatorname{gtr}(f_{i})$. Then

$\displaystyle\operatorname{gtr}(e_{1}+_{b}f_{1})$
$\displaystyle\equiv_{*}b\operatorname{gtr}(e_{1})+\bar{b}\operatorname{gtr}(f_{1})$
$\displaystyle\equiv_{*}b\operatorname{gtr}(e_{2})+\bar{b}\operatorname{gtr}(f_{2})$
$\displaystyle\equiv_{*}\operatorname{gtr}(e_{2}+_{b}f_{2})$

  * ((b))

Suppose the proof ends with

$\prftree{e_{1}=f_{2}\qquad e_{2}=f_{2}}{e_{1}^{(b)}f_{1}=e_{2}^{(b)}f_{2}}$

and assume that
$\operatorname{gtr}(e_{i})\equiv_{*}\operatorname{gtr}(f_{i})$. Then

$\displaystyle\operatorname{gtr}(e_{1}^{(b)}f_{1})$
$\displaystyle\equiv_{*}b\operatorname{gtr}(e_{1})*\bar{b}\operatorname{gtr}(f_{1})$
$\displaystyle\equiv_{*}b\operatorname{gtr}(e_{2})*\bar{b}\operatorname{gtr}(f_{2})$
$\displaystyle\equiv_{*}\operatorname{gtr}(e_{2}^{(b)}f_{2})$

  * •

Suppose the proof ends with

$\prftree{g=eg+_{b}f}{g=e^{(b)}f}$

and assume that $\operatorname{gtr}(e)\equiv_{*}\operatorname{gtr}(eg+_{b}f)$.
Then

$\operatorname{gtr}(g)\equiv_{*}b\operatorname{gtr}(e)\operatorname{gtr}(g)+\bar{b}\operatorname{gtr}(f)$

By the Horn rule in skip-free RegEx,

$\operatorname{gtr}(g)\equiv_{*}(b\operatorname{gtr}(e))*(\bar{b}\operatorname{gtr}(f))\equiv_{*}\operatorname{gtr}(e^{(b)}f)$

We are now ready to prove the key lemma in our first completeness theorem.

See 9

###### Proof

We are going to show, by induction on $e\in\mathsf{GExp}^{-}$, that for any
$d\subseteq A$,
$e+_{d}0\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(e+_{d}0))$.
Along the way, we will use the observation that
$\operatorname{rtg}(\operatorname{gtr}(e+_{d}0))\equiv_{\dagger}\operatorname{rtg}(d\operatorname{gtr}(e))\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(e))+_{d}0$.
We will also use Lemma 8 and Lemma 27 extensively.

For the base case,

  * •

$\operatorname{rtg}(\operatorname{gtr}(0+_{d}0))=\operatorname{rtg}(0+0)\equiv_{\dagger}\operatorname{rtg}(0)=0\equiv_{\dagger}0+_{d}0$.

  * •

By induction on $|d|$, where $d=\alpha_{1}\vee\dots\vee\alpha_{n}$,

$\displaystyle\operatorname{rtg}(\operatorname{gtr}(p+_{d}0))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}\left(\sum_{\alpha\leq
d}\alpha p\right)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(\alpha_{n}p)+_{\alpha_{n}}\operatorname{rtg}\left(\sum_{\alpha_{i}\in
d\setminus\alpha_{n}}a_{i}p\right)$
$\displaystyle\equiv_{\dagger}(p+_{\alpha_{n}}0)+_{\alpha_{n}}(p+_{d\setminus\alpha_{n}}0)$
(IH)
$\displaystyle\equiv_{\dagger}p+_{\alpha_{n}}(p+_{d\setminus\alpha_{n}}0)$
$\displaystyle\equiv_{\dagger}p+_{d}0$

Now assume
$e+_{d}0\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(e+_{d}0))$ and
$f+_{d}0\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(f+_{d}0))$ for
all $d$.

  * •

In the guarded union case,

$\displaystyle\operatorname{rtg}(\operatorname{gtr}((e+_{b}f)+_{d}0))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(d\operatorname{gtr}(e+_{b}f))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(bd\operatorname{gtr}(e)+d\bar{b}\operatorname{gtr}(f))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(bd\operatorname{gtr}(e))+_{b}\operatorname{rtg}(d\bar{b}\operatorname{gtr}(f))$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(\operatorname{gtr}(e))+_{bd}0)+_{b}(\operatorname{rtg}(\operatorname{gtr}(f))+_{d\bar{b}}0)$
$\displaystyle\equiv_{\dagger}(\operatorname{rtg}(\operatorname{gtr}(e))+_{d}0)+_{b}(\operatorname{rtg}(\operatorname{gtr}(f))+_{d}0)$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(e+_{d}0))+_{b}\operatorname{rtg}(\operatorname{gtr}(f+_{d}0))$
$\displaystyle\equiv_{\dagger}(e+_{d}0)+_{b}(f+_{d}0)$
$\displaystyle\equiv_{\dagger}(e+_{b}f)+_{d}0$

  * •

For the sequential composition case,

$\displaystyle\operatorname{rtg}(\operatorname{gtr}(ef+_{d}0))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(d\operatorname{gtr}(ef))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(ef))+_{d}0$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(e))\operatorname{rtg}(\operatorname{gtr}(f))+_{d}0$
$\displaystyle\equiv_{\dagger}ef+_{d}0$

For the while loop case, it suffices to show that
$\operatorname{rtg}(\operatorname{gtr}(e^{(b)}f))\equiv_{\dagger}e^{(b)}f$. To
this end, compute

$\displaystyle\operatorname{rtg}(\operatorname{gtr}(e^{(b)}f))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(b\operatorname{gtr}(e)*\bar{b}\operatorname{gtr}(f))$
$\displaystyle\equiv_{\dagger}\operatorname{rtg}(b\operatorname{gtr}(e))^{(b)}\operatorname{rtg}(\bar{b}\operatorname{gtr}(f))$
(IH) $\displaystyle\equiv_{\dagger}(e+_{b}0)^{(b)}(0+_{b}f)$

Now let $g=(e+_{b}0)^{(b)}(0+_{b}f)$ and observe that

$\displaystyle g$ $\displaystyle\equiv_{\dagger}(e+_{b}0)g+_{b}(0+_{b}f)$
$\displaystyle\equiv_{\dagger}(eg+_{b}0)+_{b}(0+_{b}f)$
$\displaystyle\equiv_{\dagger}(eg+_{b}0)+_{b}f$
$\displaystyle\equiv_{\dagger}eg+_{b}(0+_{b}f)$
$\displaystyle\equiv_{\dagger}eg+_{b}f$
$\displaystyle\equiv_{\dagger}e^{(b)}f$

It follows from the above two derivations that
$\operatorname{rtg}(\operatorname{gtr}(e^{(b)}f))\equiv_{\dagger}e^{(b)}f$.
Thus,

$\operatorname{rtg}(\operatorname{gtr}(e^{(b)}f+_{d}0))\equiv_{\dagger}\operatorname{rtg}(\operatorname{gtr}(e^{(b)}f))+_{d}0\equiv_{\dagger}e^{(b)}f+_{d}0$

as desired.

##  Appendix 0.D Proofs for Section 6

Recall that for $e\in\mathsf{GExp}$ and $a\in\mathsf{BExp}$, we used $ae$ as a
shorthand for $e+_{a}0$. The following lemma is necessary in our proof of
Lemma 11.

###### Lemma 28

Let $e,f\in\mathsf{GExp}$ and $a,b\in\mathsf{BExp}$. The following hold: e +_a
¯a f ≡e +_a f ae +_a f ≡e +_a f (a ∧b)e ≡a(be) a(e +_b f) ≡ae +_b af a(e ⋅f)
≡(ae) ⋅f e ^(a) 0 ≡0 e ^(a) f ≡e ^(a) ¯af

###### Proof

We prove the equalities in order of appearance:

  * •

For $e+_{b}\overline{b}f\equiv e+_{b}f$, we derive:

$\displaystyle e+_{b}\overline{b}f$ $\displaystyle\equiv
e+_{b}(f+_{\overline{b}}0)$
$\displaystyle\equiv(e+_{b}f)+_{b\vee\overline{b}}0$
$\displaystyle\equiv(e+_{b}f)+_{1}0$ $\displaystyle\equiv e+_{b}f$
$\displaystyle ae+_{a}f$ $\displaystyle\equiv f+_{\overline{a}}ae$
$\displaystyle\equiv f+_{\overline{a}}e$ $\displaystyle\equiv e+_{a}f$ For
$(a\wedge b)e\equiv a(be)$, we derive: $\displaystyle(a\wedge b)e$
$\displaystyle\equiv(b\wedge a)e$ $\displaystyle\equiv e+_{b\wedge a}0$
$\displaystyle\equiv e+_{b\wedge a}(0+_{a}0)$
$\displaystyle\equiv(e+_{b}0)+_{a}0$ $\displaystyle\equiv a(be)$ For
$a(e+_{b}f)\equiv ae+_{b}af$, we derive: $\displaystyle a(e+_{b}f)$
$\displaystyle\equiv((a\vee\overline{b})\wedge(a\vee b))(e+_{b}f)$
$\displaystyle\equiv(a\vee\overline{b})((a\vee b)(e+_{b}f))$
$\displaystyle\equiv(a\vee\overline{b})((e+_{b}f)+_{a\vee b}0)$
$\displaystyle\equiv(a\vee\overline{b})(e+_{b}(f+_{a}0))$
$\displaystyle\equiv(a\vee\overline{b})(e+_{b}af)$
$\displaystyle\equiv(e+_{b}af)+_{a\vee\overline{b}}0$
$\displaystyle\equiv(af+_{\overline{b}}e)+_{a\vee\overline{b}}0$
$\displaystyle\equiv af+_{\overline{b}}(e+_{a}0)$ $\displaystyle\equiv
af+_{\overline{b}}ae$ $\displaystyle\equiv ae+_{b}af$

  * •

For $a(e\cdot f)\equiv(ae)\cdot f$, we derive

$a(e\cdot f)\equiv e\cdot f+_{a}0\equiv e\cdot f+_{a}0\cdot
f\equiv(e+_{a}0)\cdot f\equiv(ae)\cdot f$

  * •

For $e{\mathbin{{}^{(a)}}}0\equiv 0$, it suffices to prove the following, by
the fixpoint rule:

$0\equiv 0+_{b}0\equiv e\cdot 0+_{b}0$

  * •

For $e{\mathbin{{}^{(a)}}}f\equiv e{\mathbin{{}^{(a)}}}\overline{a}f$, it
suffices to prove the following, by the fixpoint rule:

$e{\mathbin{{}^{(a)}}}\overline{a}f\equiv e\cdot
e{\mathbin{{}^{(a)}}}\overline{a}f+_{b}\overline{a}f\equiv e\cdot
e{\mathbin{{}^{(a)}}}\overline{a}f+_{b}f$

See 10

###### Proof

It suffices to prove that if $a\in\mathsf{BExp}$ and
$a\mathcal{L}(e)=\emptyset$, then $ae\equiv 0$. After all, if this is true and
$e$ is dead then $1\mathcal{L}(e)=\mathcal{L}(e)=\emptyset$, and hence
$e=1e\equiv 0$.

We proceed by induction on $e$. In the base, there are two cases:

  * •

If $e=p\in\Sigma$, then for all $\alpha\leq a$ it holds that $\alpha{}p\in
a\mathcal{L}(e)$. We thus find that $a\equiv 0$, and therefore $0p\equiv
p+_{0}0\equiv 0+_{1}p\equiv 0$.

  * •

If $e=0$, then $b0\equiv 0+_{b}0\equiv 0$ immediately.

For the inductive step, there are three more cases.

  * •

If $e=e_{1}+_{b}e_{2}$ then $(a\wedge b)\mathcal{L}(e_{1})=\emptyset$ and
$(a\wedge\overline{b})\mathcal{L}(e_{2})=\emptyset$. By induction, we have
$(a\wedge b)e_{1}\equiv 0$ and $(a\wedge\overline{b})e_{2}\equiv 0$. We then
derive using Lemma 28:

$a(e_{1}+_{b}e_{2})\equiv ae_{1}+_{b}ae_{2}\equiv
bae_{1}+_{b}\overline{b}ae_{2}\equiv(a\wedge
b)e_{1}+_{b}(a\wedge\overline{b})e_{2}\equiv 0+_{b}0\equiv 0$

  * •

If $e=e_{1}\cdot e_{2}$, then $a\mathcal{L}(e_{1})=\emptyset$ or
$\mathcal{L}(e_{2})=\emptyset$. In the former case $ae_{1}\equiv 0$, so by
Lemma 28 we find $a(e_{1}\cdot e_{2})\equiv(ae_{1})\cdot e_{2}\equiv 0\cdot
e_{2}\equiv 0$. In the latter case $e_{2}\equiv 0$, and thus $a(e_{1}\cdot
e_{2})\equiv a(e_{1}\cdot 0)=a0=0$.

  * •

If $e=e_{1}{\mathbin{{}^{(b)}}}e_{2}$, then
$\overline{b}\mathcal{L}(e_{2})=\emptyset$, and so $\overline{b}e_{2}\equiv
0$. By Lemma 28:

$a(e_{1}{\mathbin{{}^{(b)}}}e_{2})\equiv
a(e_{1}{\mathbin{{}^{(b)}}}\overline{b}e_{2})\equiv
a(e_{1}{\mathbin{{}^{(b)}}}0)\equiv a0\equiv 0$

See 11

###### Proof

We proceed by induction on $e$. In the base, the claim holds immediately,
whether $e=0$ or $e=p\in\Sigma$. For the inductive step, there are three
cases.

  * •

If $e=e_{1}+_{b}e_{2}$, then $e_{1}+_{b}e_{2}\equiv\lfloor
e_{1}\rfloor+_{b}\lfloor e_{2}\rfloor\equiv\lfloor e_{1}+_{b}e_{2}\rfloor$.

  * •

Suppose $e=e_{1}\cdot e_{2}$. If $e_{2}$ is dead, then $e_{2}\equiv 0$ by
Lemma 10, and so $e_{1}\cdot e_{2}\equiv e_{1}\cdot 0\equiv 0\equiv\lfloor
e_{1}\cdot e_{2}\rfloor$. Otherwise $e_{1}\cdot e_{2}\equiv\lfloor
e_{1}\rfloor\cdot\lfloor e_{2}\rfloor\equiv\lfloor e_{1}\cdot e_{2}\rfloor$.

  * •

Suppose $e=e_{1}{\mathbin{{}^{(a)}}}e_{2}$. If $\overline{a}e_{2}$ is dead,
then $\overline{a}e_{2}\equiv 0$ by Lemma 10, and so
$e_{1}{\mathbin{{}^{(a)}}}e_{2}\equiv
e_{1}{\mathbin{{}^{(a)}}}\overline{a}e_{2}\equiv
e_{1}{\mathbin{{}^{(a)}}}0\equiv 0\equiv\lfloor
e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor$ by Lemma 28. Otherwise, we derive that
$e_{1}{\mathbin{{}^{(b)}}}e_{2}\equiv\lfloor
e_{1}\rfloor{\mathbin{{}^{(b)}}}\lfloor e_{2}\rfloor\equiv\lfloor
e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor$.

To prove Lemma 12, we need an auxiliary lemma.

###### Lemma 29

Let $(X,h)$ be a $G$-coalgebra and $x\in X$. Now
$\mathcal{L}(x,(X,h))=\emptyset$ if and only if $x\in D(X,h)$.

###### Proof

For the direction from right to left, it suffices to show that $D=\\{x\in
X:\mathcal{L}(x,(X,h))=\emptyset\\}$ satisfies the rules for dead states. To
see this, note that if $x\in D$ then certainly the case where
$h(x)(\alpha)=(p,\checkmark)$ is excluded, for then
$\alpha{}p\in\mathcal{L}(x,(X,h))$. Furthermore, if
$h(x)(\alpha)=(p,x^{\prime})$ for some $p\in\Sigma$, then
$\mathcal{L}(x^{\prime},(X,h))=\emptyset$, for otherwise $L(x,(X,h))$ cannot
be empty; hence $x^{\prime}\in D$.

For the converse, suppose $w\in\mathcal{L}(x,(X,h))$. Then we can find, by
induction on $w$, an $x^{\prime}\in D(X,h)$ with
$h(x^{\prime})(\alpha)=(p,\checkmark)$ for some $p\in\Sigma$ — a
contradiction.

See 12

###### Proof

It suffices to prove that
$R=\\{(x,y):\mathcal{L}(x,(X,h))=\mathcal{L}(y,(X,h))\\}$ is a bisimulation.
To see this, suppose that $\mathcal{L}(x,(X,h))=\mathcal{L}(y,(X,h))$.

  * •

If $\lfloor h\rfloor(x)(\alpha)=\bot$, then $h(x)(\alpha)=\bot$ or
$h(x)(\alpha)=(p,y^{\prime})$ with $x^{\prime}\in D(X,h)$. Therefore there is
no word in $\mathcal{L}(x,(X,h))=\mathcal{L}(x,(Y,h))$ of the form
$\alpha{}w$, by Lemma 29. Thus $h(y)(\alpha)=\bot$ or
$h(y)(\alpha)=(p,y^{\prime})$ where $\mathcal{L}(y^{\prime},(X,h))=\emptyset$,
whence $y^{\prime}\in D(X,h)$ by Lemma 29. In either case, $\lfloor
h\rfloor(y)(\alpha)=\bot$.

  * •

If $\lfloor h\rfloor(x)(\alpha)=(p,\checkmark)$ for some $p\in\Sigma$, then
$\alpha{}p\in\mathcal{L}(x,(X,h))$, and therefore
$\alpha{}p\in\mathcal{L}(y,(Y,h))$. But then $\lfloor
h\rfloor(y)(\alpha)=(p,\checkmark)$ as well.

  * •

If $\lfloor h\rfloor(x)(\alpha)=(p,x^{\prime})\in\Sigma\times X$, then
$x^{\prime}$ is not dead in $(X,h)$ by Lemma 29, and thus there exists some
$w$ s.t. $\alpha{}pw\in\mathcal{L}(x,(X,\lfloor
h\rfloor))=\mathcal{L}(y,(X,\lfloor h\rfloor))$. We then have $\lfloor
h\rfloor(y)(\alpha)=(p,y^{\prime})$ for some $y^{\prime}\in X$. A
straightforward argument then shows that $\mathcal{L}(x^{\prime},(X,\lfloor
h\rfloor))=\mathcal{L}(y^{\prime},(X,\lfloor h\rfloor))$, and so
$x^{\prime}\mathrel{R}y^{\prime}$.

The claim about the graph of
$\lfloor-\rfloor:\mathsf{GExp}^{-}\to\mathsf{GExp}^{-}$ being a bisimulation
of skip-free automata can also be shown by induction on $e$ and exhaustive
case analysis, as follows.

See 13

###### Proof

It suffices to show that
$\partial\circ\lfloor-\rfloor=G(\lfloor-\rfloor)\circ\lfloor\partial\rfloor$
We proceed by induction on $e$. In the base, $\lfloor e\rfloor=e$ and
$\lfloor\partial\rfloor(e)=\partial(e)$, and so the claim holds trivially. For
the inductive step, there are three cases.

  * •

Suppose $e=e_{1}+_{b}e_{2}$. Without loss of generality, we assume $\alpha\leq
b$.

    * –

If $\lfloor\partial\rfloor(e_{1}+_{b}e_{2})=\bot$, then either
$\partial(e_{1})(\alpha)=\bot$ or $\partial(e_{1})(\alpha)=(p,e_{1}^{\prime})$
with $e_{1}^{\prime}$ dead. In either case,
$\lfloor\partial\rfloor(e_{1})(\alpha)=\bot$, and so $\partial(\lfloor
e_{1}\rfloor)(\alpha)=\bot$ by induction. We then conclude that
$\partial(\lfloor e_{1}+_{b}e_{2}\rfloor)(\alpha)=\partial(\lfloor
e_{1}\rfloor)(\alpha)=\bot$.

    * –

If $\lfloor\partial\rfloor(e_{1}+_{b}e_{2})=(p,\checkmark)$ for some
$p\in\Sigma$, then $\partial(e_{1})(\alpha)=(p,\checkmark)$ as well. It
follows that $\lfloor\partial\rfloor(e_{1})(\alpha)=(p,\checkmark)$, and so
$\partial(\lfloor e_{1}\rfloor)(\alpha)=(p,\checkmark)$ by induction. We then
conclude that $\partial(\lfloor
e_{1}+_{b}e_{2}\rfloor)(\alpha)=\partial(\lfloor
e_{1}\rfloor)(\alpha)=(p,\checkmark)$.

    * –

If $\lfloor\partial\rfloor(e_{1}+_{b}e_{2})=(p,e_{1}^{\prime})$, then
$\partial(e_{1})(\alpha)=(p,e_{1}^{\prime})$ for some live
$e_{1}^{\prime}\in\mathsf{GExp}$. Hence
$\lfloor\partial\rfloor(e_{1})(\alpha)=(p,e_{1}^{\prime})$, and so
$\partial(\lfloor e_{1}\rfloor)(\alpha)=(p,\lfloor e_{1}^{\prime}\rfloor)$ by
induction. We then conclude that $\partial(\lfloor
e_{1}+_{b}e_{2}\rfloor)(\alpha)=\partial(\lfloor
e_{1}\rfloor)(\alpha)=(p,\lfloor e_{1}^{\prime}\rfloor)$.

  * •

Suppose $e=e_{1}\cdot e_{2}$. If $e_{2}$ is dead, then so is $e_{1}\cdot
e_{2}$; hence

$\lfloor\partial\rfloor(e_{1}\cdot
e_{2})(\alpha)=\bot=\partial(0)(\alpha)=\partial(\lfloor e_{1}\cdot
e_{2}\rfloor)(\alpha)$

Otherwise, if $e_{2}$ is live, then we have three cases to consider.

    * –

If $\lfloor\partial\rfloor(e_{1}\cdot e_{2})(\alpha)=\bot$, then we have two
more subcases to consider.

      * *

If $\partial(e_{1}\cdot e_{2})(\alpha)=\bot$, then
$\partial(e_{1})(\alpha)=\bot$, meaning
$\lfloor\partial\rfloor(e_{1})(\alpha)=\bot$. By induction, $\partial(\lfloor
e_{1}\rfloor)(\alpha)=\bot$, and so $\partial(\lfloor e_{1}\cdot
e_{2}\rfloor)(\alpha)=\bot$.

      * *

If $\partial(e_{1}\cdot e_{2})(\alpha)=(p,e^{\prime})$ with $e^{\prime}$ dead,
then we can exclude the case where $\partial(e_{1})(\alpha)=(p,\checkmark)$,
for then $e^{\prime}=e_{2}$, which contradicts that $e_{2}$ is live. We then
know that $e^{\prime}=e_{1}^{\prime}\cdot e_{2}$ such that
$\partial(e_{1})(\alpha)=(p,e_{1}^{\prime})$. Furthermore, since $e_{2}$ is
live and $e^{\prime}$ is dead, it must be the case that $e_{1}^{\prime}$ is
dead. We then find that $\lfloor\partial\rfloor(e_{1})(\alpha)=\bot$, and so
$\partial(\lfloor e_{1}\rfloor)(\alpha)=\bot$ by induction. We conclude that
$\partial(\lfloor e_{1}\cdot e_{2}\rfloor)(\alpha)=\partial(\lfloor
e_{1}\rfloor\cdot\lfloor e_{2}\rfloor)(\alpha)=\bot$.

    * –

If $\lfloor\partial\rfloor(e_{1}\cdot e_{2})=(p,\checkmark)$, then
$\partial(e_{1}\cdot e_{2})(\alpha)=(p,\checkmark)$, which is impossible. We
can therefore exclude this case.

    * –

If $\lfloor\partial\rfloor(e_{1}\cdot e_{2})=(p,e^{\prime})$, then
$\partial(e_{1}\cdot e_{2})(\alpha)=(p,e^{\prime})$ with $e^{\prime}$ live.
This gives us two more subcases.

      * *

If $\partial(e_{1})(\alpha)=(p,\checkmark)$ and $e^{\prime}=e_{2}$, then
$\lfloor\partial\rfloor(e_{1})(\alpha)=(p,\checkmark)$, and so by induction
$\partial(\lfloor e_{1}\rfloor)(\alpha)=(p,\checkmark)$. Thus
$\partial(\lfloor e_{1}\cdot e_{2}\rfloor)(\alpha)=(p,\lfloor
e^{\prime}\rfloor)$.

      * *

If $\partial(e_{1})(\alpha)=(p,e_{1}^{\prime})$ and
$e^{\prime}=e_{1}^{\prime}\cdot e_{2}$, then $e_{1}^{\prime}$ must be live. We
then have $\lfloor\partial\rfloor(e_{1})(\alpha)=(p,e_{1}^{\prime})$, and so
$\partial(\lfloor e_{1}\rfloor)(\alpha)=(p,\lfloor e_{1}^{\prime}\rfloor)$ by
induction. We conclude that $\partial(\lfloor e_{1}\cdot
e_{2}\rfloor)(\alpha)=(p,\lfloor e_{1}^{\prime}\rfloor\cdot\lfloor
e_{2}\rfloor)=(p,\lfloor e\rfloor)$.

  * •

Suppose $e=e_{1}{\mathbin{{}^{(b)}}}e_{2}$. If $\overline{b}e_{2}$ is dead,
then so is $e_{1}{\mathbin{{}^{(b)}}}e_{2}$; hence

$\lfloor\partial\rfloor(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=\bot=\partial(0)(\alpha)=\partial(\lfloor
e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor)(\alpha)$

Otherwise, if $\overline{b}e_{2}$ is live, then we first consider the case
where $\alpha\leq\overline{b}$.

    * –

If $\lfloor\partial\rfloor(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=\bot$, then
$\partial(e_{2})(\alpha)=\bot$ or $\partial(e_{2})(\alpha)=(p,e_{2}^{\prime})$
with $e_{2}^{\prime}$ dead. In either case,
$\lfloor\partial\rfloor(e_{2})(\alpha)=\bot$, and so $\partial(\lfloor
e_{2}\rfloor)(\alpha)=\bot$ by induction. We conclude that $\partial(\lfloor
e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor)(\alpha)=\partial(\lfloor
e_{2}\rfloor)(\alpha)=\bot$.

    * –

If
$\lfloor\partial\rfloor(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=(p,\checkmark)$,
then $\partial(e_{2})(\alpha)=(p,\checkmark)$. Thus
$\lfloor\partial\rfloor(e_{2})(\alpha)=(p,\checkmark)$ and so we have
$\partial(\lfloor e_{2}\rfloor)(\alpha)=(p,\checkmark)$ by induction. We then
conclude that $\partial(\lfloor
e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor)(\alpha)=\partial(\lfloor
e_{2}\rfloor)(\alpha)=(p,\checkmark)$.

    * –

If
$\lfloor\partial\rfloor(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=(p,e_{2}^{\prime})$,
then $\partial(e_{2})(\alpha)=(p,e_{2}^{\prime})$ with $e_{2}^{\prime}$ live.
It then follows that
$\lfloor\partial\rfloor(e_{2})(\alpha)=(p,e_{2}^{\prime})$, and so
$\partial(\lfloor e_{2}\rfloor)(\alpha)=(p,\lfloor e_{2}^{\prime}\rfloor)$ by
induction. We then conclude that $\partial(\lfloor
e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor)(\alpha)=\partial(\lfloor
e_{2}\rfloor)(\alpha)=(p,\lfloor e_{2}^{\prime}\rfloor)$.

It remains to consider the case where $\alpha\leq b$.

    * –

If $\lfloor\partial\rfloor(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=\bot$, then
we have two more subcases to consider.

      * *

If $\partial(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=\bot$, then
$\partial(e_{1})(\alpha)=\bot$ as well, since $\alpha\leq b$. This means that
$\lfloor\partial\rfloor(e_{1})(\alpha)=\bot$, and so $\partial(\lfloor
e_{1}\rfloor)(\alpha)=\bot$ by induction. We conclude that $\partial(\lfloor
e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor)(\alpha)=\bot$.

      * *

If $\partial(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=(p,e^{\prime})$ with
$e^{\prime}$ dead, then since $\alpha\leq b$ we must have that
$e^{\prime}=e_{1}^{\prime}\cdot e_{1}{\mathbin{{}^{(b)}}}e_{2}$, with
$\partial(e_{1})(\alpha)=(p,e_{1}^{\prime})$. Since $\overline{b}e_{2}$ is
live, so is $e_{1}{\mathbin{{}^{(b)}}}e_{2}$. It then follows that
$e_{1}^{\prime}$ is dead, and so $\lfloor\partial\rfloor(e_{1})(\alpha)=\bot$.
By induction, $\partial(\lfloor e_{1}\rfloor)(\alpha)=\bot$, and so
$\partial(\lfloor e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor)(\alpha)=\bot$.

    * –

If
$\lfloor\partial\rfloor(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=(p,\checkmark)$,
then $\partial(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=(p,\checkmark)$, which
is impossible when $\alpha\leq b$; we can therefore exclude this case.

    * –

If
$\lfloor\partial\rfloor(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=(p,e^{\prime})$,
then $\partial(e_{1}{\mathbin{{}^{(b)}}}e_{2})(\alpha)=(p,e^{\prime})$ with
$e^{\prime}$ live. Since $\alpha\leq b$, we have that
$\partial(e_{1})(\alpha)=(p,e_{1}^{\prime})$ and
$e^{\prime}=e_{1}^{\prime}\cdot e_{1}{\mathbin{{}^{(b)}}}e_{2}$. Since
$e^{\prime}$ and $e_{1}{\mathbin{{}^{(b)}}}e_{2}$ are live, so is
$e_{1}^{\prime}$. We then find that
$\lfloor\partial\rfloor(e_{1})(\alpha)=(p,e_{1}^{\prime})$, meaning
$\partial(\lfloor e_{1}\rfloor)(\alpha)=(p,\lfloor e_{1}^{\prime}\rfloor)$ by
induction. We conclude by deriving

$\partial(\lfloor e_{1}{\mathbin{{}^{(b)}}}e_{2}\rfloor)(\alpha)=(p,\lfloor
e_{1}^{\prime}\rfloor\cdot\lfloor e_{1}\rfloor{\mathbin{{}^{(b)}}}\lfloor
e_{2}\rfloor)=(p,\lfloor e^{\prime}\rfloor)$

##  Appendix 0.E Proofs for Section 7

We start by proving that our tweaked version of the syntactic GKAT automaton
does not make any difference with regard to bisimilarity of expressions. To
make this precise, we first recall the definition of the syntactic GKAT
automaton [41].

###### Definition 26

We define
$\delta^{\prime}:\mathsf{GExp}\to(\bot+\checkmark+\Sigma\times\mathsf{GExp})^{\mathsf{At}}$
in the same way as $\delta$, except for the following two cases:

  * •

When $e,f\in\mathsf{GExp}$ such that $\delta(e)(\alpha)=(p,e^{\prime})$, we
set $\delta(e\cdot f)(\alpha)=(p,e^{\prime}\cdot f)$.

  * •

When $e\in\mathsf{GExp}$ and $\alpha\leq b$, we set
$\delta(e^{(b)})(\alpha)=(p,e^{\prime}\cdot e^{(b)})$.

Essentially, $\delta$ and $\delta^{\prime}$ differ only by the use of $\cdot$
versus $\fatsemi$ in these two cases.

We can now show that an expression is bisimilar to its representation in the
syntactic automaton GKAT as defined in the literature; this then tells us that
two states are bisimilar in $(\mathsf{GExp},\delta)$ if and only if they are
bisimilar in $(\mathsf{GExp},\delta^{\prime})$.

######  Lemma 30 ()

Let $e\in\mathsf{GExp}$. Now
$(\mathsf{GExp},\delta^{\prime}),e\mathrel{\raisebox{1.00006pt}{$\underline{\leftrightarrow}$}}(\mathsf{GExp},\delta),e$.

###### Proof

Let $R$ be the smallest relation on $\mathsf{GExp}$ such that all of the
following hold: e R e e R e’
f ∈E e ⋅f R e’ ⨟f Let $e,f\in\mathsf{GExp}$ such that $e\mathrel{R}f$. We
proceed by induction on the construction of $R$. In the base, $e\mathrel{R}f$
because $e=f$; we proceed by induction on $e$. In the (inner) base, the
definitions of $\delta^{\prime}$ and $\delta$ coincide, and so those cases go
through immediately. For the (inner) inductive step, we have three more cases.

  * •

If $e=e_{1}+_{b}e_{2}$, then let $\alpha\in\mathsf{At}$ and assume without
loss of generality that $\alpha\leq b$. In that case,
$\delta^{\prime}(e_{1}+_{b}e_{2})(\alpha)=\delta^{\prime}(e_{1})(\alpha)$ and
$\delta(e_{1}+_{b}e_{2})(\alpha)=\delta(e_{1})(\alpha)$. The claim then
follows by induction.

  * •

If $e=e_{1}\cdot e_{2}$, then there are three more subcases to consider.

    * –

If $\delta^{\prime}(e_{1})(\alpha)=(p,e_{1}^{\prime})$, then by induction
$\delta(e_{1})(\alpha)=(p,e_{1}^{\prime\prime})$ such that
$e_{1}^{\prime}\mathrel{R}e_{1}^{\prime\prime}$. Now,
$\delta^{\prime}(e_{1}\cdot e_{2})(\alpha)=(p,e_{1}^{\prime}\cdot e_{2})$ and
$\delta(e_{1}\cdot e_{2})=(p,e_{1}^{\prime\prime}\fatsemi e_{2})$, while
$e_{1}^{\prime}\cdot e_{2}\mathrel{R}e_{1}^{\prime\prime}\fatsemi e_{2}$, as
desired.

    * –

If $\delta^{\prime}(e_{1})(\alpha)=\bot$, then $\delta(e_{1})(\alpha)=\bot$ by
induction, and so $\delta^{\prime}(e_{1}\cdot
e_{2})(\alpha)=\bot=\delta(e_{1}\cdot e_{2})(\alpha)$.

    * –

If $\delta^{\prime}(e_{1})(\alpha)=\checkmark$, then
$\delta(e_{1})(\alpha)=\checkmark$, so $\delta^{\prime}(e_{1}\cdot
e_{2})(\alpha)=\delta^{\prime}(e_{2})(\alpha)$ and $\delta(e_{1}\cdot
e_{2})(\alpha)=\delta(e_{1})(\alpha)$; the claim then follows by induction.

  * •

If $e=e_{1}^{(b)}$, then let $\alpha\in\mathsf{At}$. There are three more
subcases to consider.

    * –

If $\alpha\leq b$ and $\delta^{\prime}(e_{1})(\alpha)=(p,e_{1}^{\prime})$,
then by induction $\delta(e_{1})(\alpha)=(p,e_{1}^{\prime\prime})$ such that
$e_{1}^{\prime}\mathrel{R}e_{1}^{\prime\prime}$. We then find that
$\delta^{\prime}(e_{1}^{(b)})(\alpha)=(p,e_{1}^{\prime}\cdot e_{1}^{(b)})$ and
$\delta(e_{1}^{(b)})(\alpha)=(p,e_{1}^{\prime\prime}\fatsemi e_{1}^{(b)})$,
while $e_{1}^{\prime}\cdot e_{1}^{(b)}\mathrel{R}e_{1}^{\prime\prime}\fatsemi
e_{1}^{(b)}$.

For the (outer) inductive step, $e\mathrel{R}f$ because $e=e^{\prime}\fatsemi
g$ and $f=f^{\prime}\cdot g$ such that $e^{\prime}\mathrel{R}f^{\prime}$. We
distinguish two cases.

  * •

If $e^{\prime}=1$, then because $e^{\prime}\mathrel{R}f^{\prime}$ we have by
induction that $\delta^{\prime}(e^{\prime})(\alpha)=\checkmark$ for all
$\alpha\in\mathsf{At}$. But in that case we have that
$\delta^{\prime}(e)(\alpha)=\delta^{\prime}(g)(\alpha)$, and similarly
$\delta(f)(\alpha)=\delta(g)(\alpha)$. The claim follows by an argument
similar to the base.

  * •

Otherwise $e=e^{\prime}\cdot g$; there are now three cases.

    * –

If $\delta^{\prime}(e^{\prime})(\alpha)=\bot$, then
$\delta(f^{\prime})(\alpha)=\bot$ by induction, and so
$\delta^{\prime}(e)(\alpha)=\bot=\delta(f)(\alpha)$, as desired.

    * –

If $\delta^{\prime}(e^{\prime})(\alpha)=\checkmark$, then
$\delta(f^{\prime})(\alpha)=\checkmark$ by induction, and so
$\delta^{\prime}(e)(\alpha)=\delta^{\prime}(g)(\alpha)$ and
$\delta(f)(\alpha)=\delta(g)(\alpha)$; the claim then follows.

    * –

If $\delta^{\prime}(e^{\prime})(\alpha)=(p,e^{\prime\prime})$, then
$\delta^{\prime}(f^{\prime})(\alpha)=(p,f^{\prime\prime})$ with
$e^{\prime\prime}\mathrel{R}f^{\prime\prime}$ by induction. In that case,
$\delta^{\prime}(e)(\alpha)=(p,e^{\prime\prime}\cdot g)$ and
$\delta(f)(\alpha)=(p,f^{\prime\prime}\fatsemi g)$ while
$e^{\prime\prime}\cdot g\mathrel{R}f^{\prime\prime}\fatsemi g$, as desired.

See 14

###### Proof

For the forward direction, let $R$ be a $G$-bisimulation on $(X,d)$. We claim
that $R\cup\\{(\top,\top)\\}$ is an $F$-bisimulation on $(X,\tilde{d})$. To
see this, first note that the pair $(\top,\top)$ immediately satisfies the
conditions put on an $F$-bisimulation. Furthermore, if $x\mathrel{R}y$, then
we check the three conditions.

  * •

If $\tilde{d}(x)(\alpha)=\bot$, then $d(x)(\alpha)=\bot$ as well, which means
that $d(y)(\alpha)=\bot$ and hence $\tilde{d}(y)(\alpha)=\bot$; this condition
holds.

  * •

If $\tilde{d}(x)(\alpha)=\checkmark$, then $x=\top$, but this contradicts that
$x\mathrel{R}y$; we can therefore disregard this case.

  * •

If $\tilde{d}(x)(\alpha)=(p,x^{\prime})$, then there are two possibilities.

    * –

If $x^{\prime}=\top$ and $d(x)(\alpha)=(p,\checkmark)$, then
$d(y)(\alpha)=(p,\checkmark)$ as well. But then
$\tilde{d}(y)(\alpha)=(p,\top)$. Since $\top$ is related to $\top$ by
$R\cup\\{(\top,\top)\\}$, we are done.

    * –

If $d(x)(\alpha)=(p,x^{\prime})$, then $d(y)(\alpha)=(p,y^{\prime})$ such that
$x^{\prime}\mathrel{R}y^{\prime}$. But then
$\tilde{d}(y)(\alpha)=(p,y^{\prime})$ as well, and we are done.

For the converse claim, let $R$ be a bisimulation on $\mathsf{embed}(X,d)$.
First, we note that if $x\in X+\top$ and $x\mathrel{R}\top$ or
$\top\mathrel{R}x$, then necessarily $x=\top$ — after all, this tells us that
$\tilde{d}(x)(\alpha)=\checkmark$ for all $\alpha$, and $\top$ is the only
element of $X+\top$ that fits that description. We now claim that
$R^{\prime}=R\cap X\times X$ is a bisimulation on $(X,d)$. To this end, let
$x\mathrel{R^{\prime}}y$; we check the three conditions.

  * •

If $d(x)(\alpha)=\bot$, then $\tilde{d}(x)(\alpha)=\bot$ as well, which means
$\tilde{d}(x)(\alpha)=\bot$, and hence $d(x)(\alpha)=\bot$; this condition is
covered.

  * •

If $d(x)(\alpha)=(p,\checkmark)$, then $\tilde{d}(x)(\alpha)=(p,\top)$, which
means that $\tilde{d}(y)(\alpha)=(p,y^{\prime})$ such that
$\top\mathrel{R}y^{\prime}$. But by the considerations above, this means that
$y^{\prime}=\top$, and thus $d(y)(\alpha)=(p,\checkmark)$ as well.

  * •

If $d(x)(\alpha)=(p,x^{\prime})$, then $\tilde{d}(x)(\alpha)=(p,x^{\prime})$
as well. But then $\tilde{d}(y)(\alpha)=(p,y^{\prime})$ such that
$x^{\prime}\mathrel{R}y^{\prime}$. Now, since $x^{\prime}\neq\top$, also
$y^{\prime}\neq\top$ by the considerations above, and thus
$x^{\prime}\mathrel{R^{\prime}}y^{\prime}$.

See 15

###### Proof

For the special case of $\top$, we have that
$F(h)(\tilde{\partial}(\top))(\alpha)=\checkmark=\delta(1)(\alpha)=\delta(h(\top))(\alpha)$
for all $\alpha\in\mathsf{At}$. It remains to check that
$F(h)(\tilde{\partial}(e))(\alpha)=\delta(e)(\alpha)$ for all
$e\in\mathsf{GExp}$ and $\alpha\in\mathsf{At}$, which we do by induction on
$e$.

  * •

If $e=0$, then $F(h)(\tilde{\partial}(0))(\alpha)=\bot=\delta(0)(\alpha)$.

  * •

If $e=p$, then
$F(h)(\tilde{\partial}(p))(\alpha)=(p,h(\top))=(p,1)=\delta(p)(\alpha)$.

  * •

If $e=e_{0}+_{b}e_{1}$, then there are two cases to consider. First, if
$\alpha\leq b$, then

$F(h)(\tilde{\partial}(e_{0}+_{b}e_{1}))(\alpha)=F(h)(\tilde{\partial}(e_{0}))(\alpha)=\delta(e_{0})(\alpha)=\delta(e_{0}+_{b}e_{1})(\alpha)$

The case where $\alpha\not\leq b$ is similar.

  * •

If $e=e_{0}\cdot e_{1}$, then there are three cases to consider.

    * –

If $\partial(e_{0})(\alpha)=(p,e_{0}^{\prime})$, then
$\tilde{\partial}(e_{0})(\alpha)=(p,e_{0}^{\prime})$ as well. By induction,
$\delta(e_{0})(\alpha)=(p,e_{0}^{\prime})$, and so

$F(h)(\tilde{\partial}(e_{0}\cdot e_{1}))(\alpha)=(p,e_{0}^{\prime}\cdot
e_{1})=\delta(e_{0}\cdot e_{1})(\alpha)$

    * –

If $\partial(e_{0})(\alpha)=(p,\checkmark)$, then
$\tilde{\partial}(e_{0})(\alpha)=(p,\top)$. By induction,
$\delta(e_{0})(\alpha)=(p,1)$, and so

$F(h)(\tilde{\partial}(e_{0}\cdot e_{1}))(\alpha)=(p,e_{1})=(p,1\fatsemi
e_{1})=\delta(e_{0}\cdot e_{1})(\alpha)$

Here, we use that $e_{0}^{\prime}\in\mathsf{GExp}$, and thus
$e_{0}^{\prime}\neq 1$.

    * –

If $\partial(e_{0})(\alpha)=\bot$, then $\tilde{\partial}(e_{0})(\alpha)=\bot$
as well. By induction $\delta(e_{0})(\alpha)=\bot$, and so

$F(h)(\tilde{\partial}(e_{0}\cdot e_{1}))(\alpha)=\bot=\delta(e_{0}\cdot
e_{1})(\alpha)$

  * •

If $e=e_{0}{\mathbin{{}^{(b)}}}e_{1}$, then there are four cases to consider.

    * –

If $\alpha\leq b$ and $\partial(e_{0})(\alpha)=(p,e_{0}^{\prime})$, then
$\tilde{\partial}(e_{0})(\alpha)=(p,e_{0}^{\prime})$ as well. By induction
$\delta(e_{0})(\alpha)=(p,e_{0}^{\prime})$, so

$F(h)(\tilde{\partial}(e_{0}{\mathbin{{}^{(b)}}}e_{1}))(\alpha)=(p,e_{0}^{\prime}\cdot
e_{0}{\mathbin{{}^{(b)}}}e_{1})=\delta(e_{0}{\mathbin{{}^{(b)}}}e_{1})(\alpha)$

    * –

If $\alpha\leq b$ and $\partial(e_{0})(\alpha)=(p,\checkmark)$, then
$\tilde{\partial}(e_{0})(\alpha)=(p,\top)$. By induction,
$\delta(e_{0})(\alpha)=(p,1)$, and so

$F(h)(\tilde{\partial}(e_{0}{\mathbin{{}^{(b)}}}e_{1}))(\alpha)=(p,e_{0}{\mathbin{{}^{(b)}}}e_{1})=(p,1\fatsemi
e_{0}{\mathbin{{}^{(b)}}}e_{1})=\delta(e_{0}{\mathbin{{}^{(b)}}}e_{1})(\alpha)$

    * –

If $\alpha\leq b$ and $\partial(e_{0})(\alpha)=\bot$, then
$\tilde{\partial}(e_{0})(\alpha)=\bot$. By induction
$\delta(e_{0})(\alpha)=\bot$, and so

$F(h)(\tilde{\partial}(e_{0}{\mathbin{{}^{(b)}}}e_{1}))(\alpha)=\bot=\delta(e_{0}{\mathbin{{}^{(b)}}}e_{1})(\alpha)$

    * –

If $\alpha\not\leq b$, then we derive as follows:

$F(h)(\tilde{\partial}(e_{0}{\mathbin{{}^{(b)}}}e_{1}))(\alpha)=F(h)(\tilde{\partial}(e_{1}))(\alpha)=\delta(e_{1})(\alpha)=\delta(e_{0}{\mathbin{{}^{(b)}}}e_{1})(\alpha)$

See 17

###### Proof

We proceed by induction on $e$. In the base, there are two cases.

  * •

First, if $e=0$, then $\mathcal{L}(e)=\emptyset$ by definition, and
$\widehat{\mathcal{L}}(e)=\\{\alpha\in\mathsf{At}\mid\alpha\leq
0\\}=\emptyset$, and so we have that
$\widehat{\mathcal{L}}(e)=\emptyset=\emptyset\cdot\mathsf{At}=\mathcal{L}(e)\cdot\mathsf{At}$.

  * •

Second, if $e=p$, then $w\in\widehat{\mathcal{L}}(e)$ if and only if
$w=\alpha{}p\beta$ for some $\alpha,\beta\in\mathsf{At}$, which is true if and
only if $\alpha{}p\beta\in\mathcal{L}(e)\cdot\mathsf{At}$.

For the inductive step, we first note that for $b\in\mathsf{BExp}$ and
$e\in\mathsf{GExp}$, we have
$\widehat{\mathcal{L}}(b)\diamond(\mathcal{L}(e)\cdot\mathsf{At})=b\mathcal{L}(e)\cdot\mathsf{At}$.
We now distinguish three cases.

  * •

If $e=e_{1}+_{b}e_{2}$, then we derive

$\displaystyle\widehat{\mathcal{L}}(e_{1}+_{b}e_{2})$
$\displaystyle=\widehat{\mathcal{L}}(b)\diamond\widehat{\mathcal{L}}(e_{1})\cup\widehat{\mathcal{L}}(\overline{b})\diamond\widehat{\mathcal{L}}(e_{2})$
$\displaystyle=\widehat{\mathcal{L}}(b)\diamond(\mathcal{L}(e_{1})\cdot\mathsf{At})\cup\widehat{\mathcal{L}}(\overline{b})\diamond(\mathcal{L}(e_{2})\cdot\mathsf{At})$
$\displaystyle=b\mathcal{L}(e_{1})\cdot\mathsf{At}\cup\overline{b}\mathcal{L}(e_{2})\cdot\mathsf{At}$
$\displaystyle=(b\mathcal{L}(e_{1})\cup\overline{b}\mathcal{L}(e_{2}))\cdot\mathsf{At}$
$\displaystyle=\mathcal{L}(e_{1}+_{b}e_{2})\cdot\mathsf{At}$ (Lemma 2)
$\displaystyle\widehat{\mathcal{L}}(e_{1}\cdot e_{2})$
$\displaystyle=\widehat{\mathcal{L}}(e_{1})\diamond\widehat{\mathcal{L}}(e_{2})$
$\displaystyle=(\mathcal{L}(e_{1})\cdot\mathsf{At})\diamond(\mathcal{L}(e_{2})\cdot\mathsf{At})$
$\displaystyle=\mathcal{L}(e_{1})\cdot\mathcal{L}(e_{2})\cdot\mathsf{At}$
$\displaystyle=\mathcal{L}(e_{1}\cdot e_{2})\cdot\mathsf{At}$ (Lemma 2)
$\displaystyle\widehat{\mathcal{L}}(e_{1}{\mathbin{{}^{(b)}}}e_{2})$
$\displaystyle=(\widehat{\mathcal{L}}(b)\diamond\widehat{\mathcal{L}}(e_{1}))^{(*)}\diamond\widehat{\mathcal{L}}(\overline{b})\diamond\widehat{\mathcal{L}}(e_{2})$
$\displaystyle=(\widehat{\mathcal{L}}(b)\diamond(\mathcal{L}(e_{1})\cdot\mathsf{At}))^{(*)}\diamond\widehat{\mathcal{L}}(\overline{b})\diamond(\mathcal{L}(e_{2})\cdot\mathsf{At})$
$\displaystyle=(b\mathcal{L}(e_{1})\cdot\mathsf{At})^{(*)}\diamond(\overline{b}\mathcal{L}(e_{2})\cdot\mathsf{At})$
$\displaystyle=\Bigl{(}\bigcup_{n\in\mathbb{N}}b\mathcal{L}(e_{1})^{n}\cdot\mathsf{At}\Bigr{)}\diamond(\overline{b}\mathcal{L}(e_{2})\cdot\mathsf{At})$
$\displaystyle=\bigcup_{n\in\mathbb{N}}b\mathcal{L}(e_{1})^{n}\cdot\overline{b}\mathcal{L}(e_{2})\cdot\mathsf{At}$
$\displaystyle=\mathcal{L}(e_{1}{\mathbin{{}^{(b)}}}e_{2})\cdot\mathsf{At}$
(Lemma 2)

Open Access This chapter is licensed under the terms of the Creative
CommonsAttribution 4.0 International License
(http://creativecommons.org/licenses/by/4.0/), which permits use, sharing,
adaptation, distribution and reproduction in any medium or format, as long as
you give appropriate credit to the original author(s) and the source, provide
a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in
thechapter’s Creative Commons license, unless indicated otherwise in a credit
line to thematerial. If material is not included in the chapter’s Creative
Commons license andyour intended use is not permitted by statutory regulation
or exceeds the permitteduse, you will need to obtain permission directly from
the copyright holder.