11institutetext: Boise State University 11email:
kennyballou<EMAIL_ADDRESS>
AI

    abstract interpretation
CFG

    control flow graph
DFA

    data-flow analysis
DFS

    depth-first search
DBM

    difference bounded matrix
JVM

    Java virtual machine
LIA

    linear integer arithmetic
NIA

    non-linear integer arithmetic
TVPI

    two variables per inequality
SMT

    satisfiability modulo theories
SMT-LIB

    satisfiability modulo theories library
StInG

    Stanford Invariant Generator
FS

    full state
FG

    Full Graph
CC

    Connect Components
NN

    Node Neighbors
MN

    Minimal Neighbors

# Minimally Comparing Relational Abstract Domains

Kenny Ballou  0000-0002-6032-474X Elena Sherman  0000-0003-4522-9725

###### Abstract

Value-based static analysis techniques express computed program invariants as
logical formula over program variables. Researchers and practitioners use
these invariants to aid in software engineering and verification tasks. When
selecting abstract domains, practitioners weigh the cost of a domain against
its expressiveness. However, an abstract domain’s expressiveness tends to be
stated in absolute terms; either mathematically via the sub-polyhedra the
domain is capable of describing, empirically using a set of known properties
to verify, or empirically via logical entailment using the entire invariant of
the domain at each program point. Due to _carry-over_ effects, however, the
last technique can be problematic because it tends to provide a simplistic and
imprecise comparisons.

We address limitations of comparing, in general, abstract domains via logical
entailment in this work. We provide a fixed-point algorithm for including the
minimally necessary variables from each domain into the compared formula.
Furthermore, we empirically evaluate our algorithm, comparing different
techniques of widening over the Zones domain and comparing Zones to an
incomparable Relational Predicates domain. Our empirical evaluation of our
technique shows an improved granularity of comparison. It lowered the number
of more precise invariants when comparing analysis techniques, thus, limiting
the prevalent _carry-over_ effects. Moreover, it removed undecidable
invariants and lowered the number of incomparable invariants when comparing
two incomparable relational abstract domains.

###### Keywords:

Static Analysis Abstract Domain Comparison Data-Flow Analysis Abstract
Interpretation

##  1 Introduction

Various value-based static analysis techniques express computed program
invariants as a logical formula over program variables. For example, abstract
interpretation [6] uses abstract domains such as Zones [15] and Octagons [17]
to describe an invariant as a set of linear integer inequalities in a
restricted format. Other techniques such as symbolic execution [11] and
predicate analysis combined with a symbolic component [20] do the same, only
using a general linear integer arithmetic format. These invariants are then
used for program verification [4, 24], program optimization [1, 10], and for
software development tasks.

Static analysis developers rarely use a computed invariant by itself, but
rather compare them to determine effects of new algorithms or abstract domain
choices on the invariant precision. For example, to evaluate tuning analyzer
parameters, static analysis researchers compare invariant values $\mathcal{I}$
and $\overset{\sim}{\mathcal{I}}$ from the original and tuned analyzer runs,
respectively. If an invariant becomes more precise, we conclude that the new
technique or a domain choice results in a more precise analysis. For
relational domains one can use queries to an SMT solver, such as Z3 [18], to
determine which invariant is more precise by checking their implication
relations.

However, to objectively measure such effects in a computed invariant after
statement $s$, $\mathcal{I}_{s}$, we need to compare only the part of
$\mathcal{I}_{s}$ affected by the transfer function of $s$, $\tau_{s}$. This
way, if $\overset{\sim}{\mathcal{I}}$ has already been more precise than
$\mathcal{I}$ before $s$ and $\tau_{s}$ has not changed the relevant facts,
then the comparison should disregard the _carry-over_ precision improvement in
$\overset{\sim}{\mathcal{I}}_{s}$.

The comparison of two relational invariants $\mathcal{I}$ and
$\overset{\sim}{\mathcal{I}}$ involves two steps: (1) identifying a changed
component of each invariant at a given statement and (2) performing minimal
comparison between the changed components of $\mathcal{I}$ and
$\overset{\sim}{\mathcal{I}}$. In our previous work [3] we addressed step (1)
for the Zones domain where using data-flow analysis (DFA) information, we
developed efficient algorithms that find a minimally changed set of
inequalities in a Zone invariant.

In this work we target step (2), assuming that an abstract domain has some
means to perform step (1) using either elementary or sophisticated algorithms.
Thus, the contributions of this paper include: (a) development and analysis of
a minimal comparison algorithm for relational abstract domains and (b)
investigating its effect on comparisons between different widening techniques
for Zones domain as well as comparison between Zones and incomparable
Predicate domains with a relational component.

The rest of the paper is organized as follows. In Section 2, we provide the
background, context, and motivation for our work. In Section 3, we describe
our fixed-point algorithm. In Section 4, we explain our experimental setup and
evaluation, and in Section 5, we examine the results of our experiments. We
connect this work with previous research in Section 6. Finally, we conclude
and discuss future work in Section 7.

##  2 Background and Motivation

We refer to an invariant and the corresponding abstract domain as relational
if it is expressed as a conjunction of formulas over program variables, e.g.,
a set of linear integer inequalities. We first explain the concept of the
minimal change for an invariant and then explain challenges of comparing two
relational domains, and sketch how our proposed approach works.

###  2.1 Minimal changes in relational abstract domains

Consider the relational invariants computed by a data-flow analysis framework
using the Zones abstract domain as shown in Figure 1(a). Let us assume the
analyzed code has four program variables: $w$, $x$, $y$, and $z$. Here, the
incoming flow to the conditional statement has the following invariant:
$\mathcal{I}_{in}=z\leq x\land w\to\top\land y\to\top$. That is, variables $w$
and $y$ are unbounded while $x$ and $z$ are bounded by a $\leq$ relation. The
transfer function of the true branch adds $y\leq x$ inequality, thus making
$y$ bounded. This results in $\mathcal{I}_{t}=z\leq x\land y\leq x\land
w\to\top$ invariant. Similarly, the invariant for the false branch becomes
$\mathcal{I}_{f}=z\leq x\land x\leq y-1\land w\to\top$.

Even though $\mathcal{I}_{f}$ and $\mathcal{I}_{t}$ are new invariants, they
inherit two unchanged inequalities $z\leq x$ and $w\to\top$ from
$\mathcal{I}_{in}$. This suggests that some part of a previously computed
invariants have not changed by the transfer function of the conditional
statement. Thus, if for some application $\mathcal{I}_{in}$ is more precise
because of $z\leq x$ and remains more precise in $\mathcal{I}_{t}$ because of
the same inequality, such _carry-over_ precision results should be
disregarded.

Previous work determining minimal changes in a relational abstract domain
approach [3] addresses this problem by identifying the part the invariant
affected by the statement’s transfer function. For example, the minimal change
algorithm for Zones [3] can compute the minimal sub-formula given the
potentially changed variables $x$ and $y$. Specifically, the algorithm
identifies only the $y\leq x$ part of $\mathcal{I}_{t}$ having changed from
$\mathcal{I}_{in}$. Likewise for $\mathcal{I}_{f}$, the algorithm identifies
two inequalities: $z\leq x$ and $x\leq y-1$ as the changed portion of the
invariant.

The minimal change algorithm can be sophisticated and accurately compute the
changed part of the invariants, or can be over-approximating, and in the worst
case return the entire invariant. In our previous work we developed an
efficient collection of such algorithms for the Zones abstract domain. In this
work, we assume that a relational domain has an invariant change method
$\Delta$ implemented, which takes as input an invariant and a set of updated
variables and returns a portion of $\mathcal{I}$, e.g., in our example
$\Delta(\mathcal{I}_{t},\\{x,y\\})=y\leq x$. The green shaded regions of an
invariant in the Figures 1(a) and 1(b) indicates the changed part of the
state.

if (y <= x) $\displaystyle z$ $\displaystyle\leq x\land$ $\displaystyle x$
$\displaystyle\leq y-1\land$ $\displaystyle w$ $\displaystyle\to\top$
$\displaystyle z$ $\displaystyle\leq x\land$ $\displaystyle y$
$\displaystyle\leq x\land$ $\displaystyle w$ $\displaystyle\to\top$ $z\leq
x\land w\to\top\land y\to\top$ft (a)

if (y <= x) $\displaystyle z$ $\displaystyle\leq x\land$ $\displaystyle x$
$\displaystyle\leq y-1\land$ $\displaystyle w$ $\displaystyle\leq y$
$\displaystyle z$ $\displaystyle\leq x\land$ $\displaystyle y$
$\displaystyle\leq x\land$ $\displaystyle w$ $\displaystyle\leq y$ $z\leq
x\land w\leq y$ft✓✗✓ (b)

Figure 1: Original Static Analysis (a) and Improved Static Analysis (b)

###  2.2 Comparing relational domains

Now consider invariants in Figure 1(b) computed for the same code fragment,
but using an improved algorithm. This algorithm is able to compute additional
information for $\overset{\sim}{\mathcal{I}}_{in}=z\leq x\land w\leq y$, which
is more precise than $\mathcal{I}_{in}$ since
$\overset{\sim}{\mathcal{I}}_{in}$ constrains the values of $w$ and $y$. The
checkmark symbol, ✓, by $\overset{\sim}{\mathcal{I}}$ in Figure 1(b) indicates
an increased precision comparing to the corresponding invariants $\mathcal{I}$
in Figure 1(a).

When we compare using the entirety of the invariants instead of simply the
changed portion of the invariants for the false branch, the result would be
that $\overset{\sim}{\mathcal{I}_{f}}$ is more precise than $\mathcal{I}_{t}$.
Thus, simply applying $\Delta$ for both invariants can filter out erroneous,
_carry-over_ improvements, which we annotate with the ✗ symbol.

In the case of the true branch, the set of variables in their changed portion
of the invariant are the same. However, this is not always the case, which we
can see on the false branches. There, $\Delta(\mathcal{I}_{f},\\{x,y\\})=y\leq
x$, but $\Delta(\overset{\sim}{\mathcal{I}}_{f},\\{x,y\\})=y\leq x\land w\leq
y$ has an extra variable $w$. In order to make a sound comparison, we need to
conjoin $w\to\top$ with the result of $\Delta(\mathcal{I}_{f},\\{x,y\\})$. The
challenge here is to identify the smallest necessary additions to the changed
portions of the invariants to perform a sound comparison.

In the next section we present our proposed approach that addressees this
problem by developing a fixed-point algorithm that, in each iteration,
discovers a minimal set of inequalities (modulo $\Delta$) in one invariant
that is adequate for comparison with the changed part of the other invariant.

##  3 Approach

In this section, we explain the theoretical basis for our approach to
minimally compare relational invariants via logical entailment. We start by
defining the problem, and then we present our algorithm that solves it. At the
end, we perform the analysis of the proposed algorithm.

###  3.1 Problem definition

We define the problem in a context of a DFA framework, where the framework
provides a set of updated variables $dv$ that resulted in a new invariant
$\mathcal{I}$. An abstract domain for $\mathcal{I}$ has a function $\Delta$
implemented, which returns a portion of $\mathcal{I}$ that is changed by $dv$.
In the worst case $\Delta(\mathcal{I},dv)=\mathcal{I}$, i.e., the entire
invariant has been affected. In the best case
$\Delta(\mathcal{I},dv)=\emptyset$, i.e., nothing has changed. We also
introduce a function $V$ that returns the set of variables used in
$\mathcal{I}$. For example, we use it to define the following property:
$V(\Delta(\mathcal{I},dv))\subseteq V(\mathcal{I})$.

Let $\mathcal{I}_{1}$ and $\mathcal{I}_{2}$ be two relational invariants, and
let $dv_{1}$ and $dv_{2}$ be their corresponding sets of updated variables.
Then the problem of finding a minimal changed part of two invariants reduces
to finding a common minimal updated set of variables $S$ such that

$S=V(\Delta(\mathcal{I}_{1},S))=V(\Delta(\mathcal{I}_{2},S))$ (1)

A minimal solution for such recursive definitions is commonly obtained by a
fixed point iteration algorithm with initial values $S_{0}$ set to the
smallest set, which in our case is $S_{0}=dv_{1}\cup dv_{2}$.

###  3.2 Finding a common changed variable set

1:$V(\mathcal{I}_{1})=V(\mathcal{I}_{2})\land
V(\Delta(\mathcal{I}_{1},dv_{1}))\subseteq V(\mathcal{I}_{1})\land
V(\Delta(\mathcal{I}_{2},dv_{2}))\subseteq V(\mathcal{I}_{2})$

2:$S_{1}=S_{2}\subseteq V(\mathcal{I}_{1})$

3:function CommonVarSet($dv_{1}$, $dv_{2}$, $\mathcal{I}_{1}$,
$\mathcal{I}_{2}$)

4: $S_{1}\leftarrow$ V($\Delta$($\mathcal{I}_{1}$, $dv_{1}$))

5: $S_{2}\leftarrow$ V($\Delta$($\mathcal{I}_{2}$, $dv_{2}$))

6: while $S_{1}\neq S_{2}$ do

7: if $S_{1}\supset S_{2}$ then

8: $dv_{2}\leftarrow S_{1}\setminus S_{2}$

9: $S_{2}\leftarrow S_{2}\cup$ $V(\Delta$($\mathcal{I}_{2}$, $dv_{2}$))

10: else if $S_{2}\supset S_{1}$ then

11: $dv_{1}\leftarrow S_{2}\setminus S_{1}$

12: $S_{1}\leftarrow S_{1}\cup$ V($\Delta$($\mathcal{I}_{1}$, $dv_{1}$))

13: else

14: $dv_{1}\leftarrow S_{2}\setminus S_{1}$

15: $dv_{2}\leftarrow S_{1}\setminus S_{2}$

16: $S_{1}\leftarrow S_{1}\cup$ V($\Delta$($\mathcal{I}_{1}$, $dv_{1}$))

17: $S_{2}\leftarrow S_{2}\cup$ V($\Delta$($\mathcal{I}_{2}$, $dv_{2}$))

18: end if

19: end while

20: return $S_{1}$

21:end function

Algorithm 1 Common minimal changed variable set

Algorithm 1 shows the pseudocode of the optimized fixed point computation
algorithm to solve Equation 1. The algorithm takes as arguments, the updated
variables for each domain, $dv_{1}$ and $dv_{2}$, two invariants to compare,
$\mathcal{I}_{1}$ and $\mathcal{I}_{2}$. It requires basic conditions for its
correctness: both invariants are described over the same set of variables and
$\Delta$ does not introduce any new variables. The output is the solution for
Equation 1.

The algorithm first computes the initial changed variable sets, $S_{1}$ and
$S_{2}$ for each invariant, lines 4 and 5, affected by the updated variables
$dv_{1}$ and $dv_{2}$, respectively

At line 6, the algorithm compares the two sets and if they are not equal,
i.e., the fixed point has not been reached, the algorithm enters the main
iteration loop. Inside the body of the loop, the algorithm first tests whether
one set of variables is a proper superset of the other, lines 7 and 10.

If one of the sets is a proper superset, it only augments the smaller set as
done on lines 8–9 and lines 11–12. For example, if $S_{1}\supset S_{2}$,
$S_{2}$ is augmented by the variables which are not already in $S_{2}$.

Afterwards, a new updated variable set is computed from the set difference of
$S_{1}$ and $S_{2}$, line 8. Then, the changed variable set is computed as the
union between the existing set $S_{2}$ and the newly computed minimum
variables, line 9. Similar computations are done for the case when
$S_{2}\supset S_{1}$, lines 11–12.

Finally, when the changed variable sets are incomparable— line 13— then both
changed variable sets are recomputed in a similar fashion as described in
lines 14–17. Upon the loop’s termination, i.e., when $S_{1}=S_{2}$, the
algorithm returns one of the dependent sets, line 20.

To demonstrate how Algorithm 1 compares two invariants, consider the
invariants on the true branch from our example in Figure 1(b). There,
$\mathcal{I}_{1}=z\leq x\land y\leq x\land w\to\top$ and
$\mathcal{I}_{2}=z\leq x\land y\leq x\land w\leq y$. The updated variables are
$dv_{1}=\\{x,y\\}$ and $dv_{2}=\\{x,y\\}$.

The algorithm computes $\\{x,y\\}$ for $S_{1}$ and $\\{w,x,y\\}$ for $S_{2}$.
Since $S_{2}$ is a proper superset of $S_{1}$, we recompute $S_{1}$, lines 11
and 12. Specifically, $dv_{1}$ becomes $\\{w\\}$. $S_{1}$ is then recomputed:
$S_{1}=S_{1}\cup V(\Delta(\mathcal{I}_{1},dv_{1}))$, which results in
$S_{1}=\\{x,y\\}\cup\\{w\\}=\\{w,x,y\\}$. At this point, $S_{1}=S_{2}$,
terminating the loop, and the algorithm returns the set $S_{1}=\\{w,x,y\\}$.
Then, an SMT solver can be used to compare logical relations of
$\Delta(\mathcal{I}_{1},S_{1})$ and $\Delta(\mathcal{I}_{1},S_{1})$, for
example, using implication relations. Or, in case of Zones, one can use its
custom equivalence engine [15].

As mentioned, under worst-case conditions, Algorithm 1 returns the entire set
of variables. In other words, it devolves into a full invariant comparison.
This can happen if the variables within the invariant are tightly coupled with
all other variables. Another situation which can cause a worst-case comparison
is when an abstract domain has an ineffective $\Delta$ function, which
performs a basic dependency analysis such as slicing [3, 23].

Below we present termination and complexity analysis for Algorithm 1. We start
with a proof sketch of termination.

###### Proof

First, we begin with the following assumptions: the variable projections for
both domains are equivalent, i.e., $V(\mathcal{I}_{1})=V(\mathcal{I}_{2})$;
and we assume the invariant minimization functions for each domain yield a
subset of the variable projections, that is,
$\Delta(\mathcal{I}_{1},dv_{1})\subseteq V(\mathcal{I}_{1})$, and similarly
for $\mathcal{I}_{2}$.

At each iteration, the union of variables over the minimization function is
always increasing by at least one variable in either $S_{1}$ or $S_{2}$.
Therefore, within a finite number of iterations $S_{1}$ and $S_{2}$ reach
fixed point, which is bounded by $V(\mathcal{I}_{1})=V(\mathcal{I}_{2})$
condition. Thus, Algorithm 1 terminates. ∎

The complexity of Algorithm 1 is $O(N)\cdot(C_{\Delta_{1}}+C_{\Delta_{2}})$,
where $N$ is the number of variables in the program under analysis and
$C_{\Delta_{i}}$ is the complexity of the invariant minimization function for
the corresponding domain. In the worst-case, at each iteration the sets
$S_{1}$ and $S_{2}$ augmented by a single variable from $\Delta$ computations.
Overall, the time-complexity of Algorithm 1 depends on the number of variables
and the complexity of the $\Delta$ functions of the abstract domains.

##  4 Methodology

To determine the effectiveness of the proposed algorithm, we use it to compare
invariants produced by different techniques and by different abstract domains
on the same program. For each subject program, each analysis outputs
invariants after each statement. Over the corpus of programs, we compute
$6564$ total invariants. We store the invariants as logical formulas in SMT-
LIB format. We run analyses on two relational domains, Zones and Relational
Predicates [20], and compare the results of a standard Zones analysis to
advanced Zones analyses, and Zones analysis to Relational Predicates analysis.

The goal of the empirical evaluation is to answer the following research
questions:

RQ1

Does our technique affect the invariant comparison between different analysis
techniques for the same abstract domain?

RQ2

Does our technique affect the invariant comparison between two different
relational domains?

RQ3

How effective and efficient is Algorithm 1 on real-world invariant
comparisons?

We consider different analysis techniques over the Zones domain to measure the
precision gained by various advanced techniques. We consider the iteration
parameter before widening. We also consider the widening method employed,
which ensures termination for Zones analysis.

We then compare the most precise Zones technique to Relational Predicates
[20], two incomparable domains. Our previous work [3] has shown the benefit of
minimally comparing incomparable domains to demonstrate realized precision.
However, in this case, we extend the invariants of the Predicates domain with
a symbolic relational component.

For Relational Predicates, the minimization function is a selection based
solely on notions of variable reachability, e.g., variable dependence, but it
might not be minimal because of the generality of inequalities used in the
relational part. We also computed minimization over Relational Predicates
using a purely connected component concept, similar to the technique by Visser
et al. [23], however, reachable performed marginally better.

We use the Minimal Neighbors (MN) minimization function from our previous work
[3] for Zones which provides the smallest invariant partition given a set of
changed variables. This minimization algorithm considers the semantics of the
formulas under the changed variables. Using these semantics, it selects the
minimal dependent substate from the logical formula representing the
invariant.

####  4.0.1 Subject programs

Our subject programs consist of $192$ Java methods from previous research on
the Predicates domain [20]. These methods were extracted from a wide range of
real-world, open-source projects and have a high number of integer operations.
The subject programs range from $1$ to $1993$ Jimple instructions, a three
address intermediate representation. The average branch count for the methods
is $6$ ($\sigma=11$), with one method containing a maximal $56$ branches. A
plurality of our subject methods, $81$, contain at least one loop, with one
method containing $12$ loops.

####  4.0.2 Experimental platform

We execute each of the analyses on a cluster of CentOS 7 GNU/Linux compute
nodes, running Linux version 3.10.0-1160.76.1, each equipped with an Intel
Xeon Gold 6252 and $192\text{\,}\mathrm{GB}$ of system memory. We use an
existing DFA static analysis tool [2, 20] implemented in the Java programming
language. The analysis framework uses Soot [19, 22] version 4.2.1. Similarly,
we use Z3 [18], version 4.8.17 with Java bindings to compare SMT expressions
for the abstract domain states. Finally, we use Java version 11 to execute the
analyses, providing the following JVM options: -Xms4g, -XX:+UseG1GC,
-XX:+UseStringDeduplication, and -XX:+UseNUMA.

####  4.0.3 Implementation

We modified an existing DFA framework such that the Zones analysis outputs its
entire invariant for each program point. Each invariant is further reduced
using a redundant inequality reduction technique proposed by Larsen et al.
[12]. For all domains, unbounded variables are set to top, $\top$, and
excluded from the output expression. This further simplifies the formulas.
After entailment, we use Z3, using the linear integer arithmetic (LIA) theory
for Zones to Zones comparisons and the non-linear integer arithmetic (NIA)
theory for Zones to Relational Predicates comparisons, to decide model
behavior of each domain.

####  4.0.4 Evaluations

In total, we perform _three_ different invariant comparisons, summarized in
the following list:

$Z\preceq Z_{k=5}$—

Zones using standard widening after two iterations and Zones widening after
five iterations.

$Z\preceq Z_{ths}$—

Zones with standard widening and Zones with threshold widening.

$Z_{ths}\prec\succ P$—

Zones with threshold widening and Relational Predicates.

In all instances of Zones sans $Z_{k=5}$, widening happens after _two_
iterations over widening nodes. We use a generic set of thresholds for Zones
based on powers of 10: $\\{0,1,10,100,1000\\}$. Using a tuned set of
thresholds for each program would yield better results.

We use a generic disjoint domain for the basis of the Relational Predicates,
based on Collberg et al.’s [5] study of numerical constants in Java Programs.
Specifically, the predicate domain used in this study consists of the
following set of disjoint elements: $\\{(-\infty,-5]$, $(-5,-2]$, $-1$, $0$,
$1$, $[2,5)$, $[5,+\infty)\\}$.

##  5 Evaluation Results and Discussions

In this section, we present the results of our experiments and discuss their
implications to the research questions posed in the previous section.

###  5.1 Technique Comparisons

Comparison | $Z\equiv Z_{k=5}$ | $Z\prec Z_{k=5}$
---|---|---
Full | 6555 | 9
Minimal | 6562 | 2
Table 1: Zones $k=2$ widening compared to Zones $k=5$ widening

Comparison | $Z\equiv Z_{ths}$ | $Z\prec Z_{ths}$
---|---|---
Full | 6519 | 45
Minimal | 6545 | 19
Table 2: Zones compared to Zones with Threshold Widening

To answer RQ1, we consider the comparisons of different techniques using the
Zones abstract domain. Since different techniques using the same domain create
a partial ordering of their respective precision, we need only consider
equivalent and less precise outcomes. To ensure correctness of our
implementation, we ensured that there were no other precision outcomes.

Table 2 shows the breakdown of invariants computed by standard widening after
_two_ iterations and standard widening after _five_ iterations. Comparing
invariants using the entire invariant, deferred widening produces _nine_ more
precise invariants. However, when using our minimized comparison technique,
the slim advantage reduces to _two_ invariants.

Table 2 shows the breakdown of invariants between standard widening after two
iterations and threshold widening after two iterations. Here, we see the
largest gain in precision. Using the entire invariant to compare, threshold
widening computes $45$ more precise invariants. Again, however, the precision
gain is cut by more than $50\%$ when using minimal comparisons. The choice of
thresholds could improve the precision, but for best results, the set of
thresholds needs to be tailored specifically to each program.

As we can see between $Z\preceq Z_{k=5}$ and $Z\preceq Z_{ths}$, our
comparison technique lowers the number of more precise invariants, thus
eliminating the _carry-over_ precision instances. That is, our technique
lowers the number of more precise invariants advanced techniques compute.
However, in doing so, our technique presents a more granular image of the
realized precision gain advanced techniques offer.

###  5.2 Zones versus Relational Predicates

Comparison | $Z_{ths}\equiv P$ | $Z_{ths}\prec P$ | $Z_{ths}\succ P$ | $Z_{ths}\prec\succ P$ | $Z_{ths}\,?\,P$
---|---|---|---|---|---
Full | 1227 | 3173 | 196 | 1947 | 21
Minimal | 3675 | 2353 | 248 | 288 | 0
Table 3: Zones with Threshold Widening compared to Relational Predicates

Table 3 shows the precision breakdown of Zones with threshold widening
compared to Relational Predicates. Given that Zones and Predicates are
inherently incomparable domains, we must consider all precision comparison
categories. With the full invariant compairsions, Relational Predicates are
more precise than Zones in about $50\%$ of the invariants. The next largest
category of invariants is incomparable, $\prec\succ$, which accounts for
$30\%$ of invariants. Here, Zones and Predicates are complementary, neither
more nor less precise than the other. Zones and Predicates are equivalent in
$19\%$ of all invariants, and Zones are more precise in about $3\%$ of all
invariants. Finally, using the full invariant, $21$ of the program points
between the relation between two invariants could not be established by Z3
since it returned UNKNOWN.

Our technique eliminates the undecidable results. Moreover, it dramatically
reduces the number of incomparable invariants– only $4\%$ of invariants remain
incomparable. Similar to _carry-over_ precision, incomparable invariants arise
when one domain computes a more precise invariant for one variable, and the
other domain computes a more precise invariant for another, unrelated variable
at a later program point. Considering the entire invariant results in
incomparable precision. However, by comparing only the relevant, changed
variables, our technique largely disentangles the imprecision in the
comparison.

The equivalent invariant category is the next largest affected category, where
more than half, $56\%$, of computed invariants between Zones and Relational
Predicates become equivalent. Relational Predicates lose $13\%$ of more
precise invariants, and Zones gains about $1\%$ of invariants which it
computes more precisely than Relational Predicates.

By comparing only the necessary variables at each program point, our technique
allows general, relational abstract domains to be compared without undecidable
results. The reduction in incomparable invariants between two otherwise
difficult to compare domains provides a clearer precision performance picture
between the two domains.

###  5.3 Iterations and variable reductions

$0$$1000$$2000$$3000$$4000$$5000$$6000$$7000$$0$$0.2$$0.4$$0.6$$0.8$$1$(a)$0$$200$$400$$600$$800$$1000$$1200$$1400$$1600$$1800$$2000$$0$$0.2$$0.4$$0.6$$0.8$$1$(b)

Frequency

Proportion of variables

\makebox(0.0,0.0)[]{{}}

Proportion of variables

Figure 2: Frequency plot of proportion of variables selected by Algorithm 1
which are necessary for comparing two invariants. (a) represents the
frequencies of proportions when comparing techniques using Zones. (b)
represents the frequencies of proportions when comparing Zones to Relational
Predicates.

To determine if Algorithm 1 is efficient, RQ3, we use the iteration depth
count to determine how many times the algorithm iterates before it reaches a
stable set of variables for comparison. Over all instances of Zones
comparisons, the iteration count was either _zero_ or _one_ , with no
outliers. That is, either Zones computed the same set of changed variables and
the dependent set between two techniques was immediately equivalent. Or, the
set of dependent variables is captured with only a single extension, mostly to
the Zones using standard widening, $Z$.

Comparing Zones to Relational Predicates, we see similar results. The average
number of iterations is between _zero_ and _one_ iteration. However, we have
several outliers at two iterations. Instrumentation found $12$ instances of
extreme outliers, $11$ for _three_ iterations, and one instance of _four_
iterations. Furthermore, more variety exists in the branches for Zones versus
Relational Predicates. Unlike comparing techniques between Zones invariants,
comparing Zones to a more general, relational formula required more
augmentation by each domain.

To evaluate effectiveness of Algorithm 1, RQ3, we consider the proportion of
variables necessary for comparison. We instrumented our algorithm to compute
the proportion of variables it returns after reaching a stable set, compared
to the variable projection of the incoming invariants. We plot the frequency
of proportions of variables returned by Algorithm 1 in Figure 2. In Figure 2a,
we plot variable reductions across all comparisons of Zones: standard widening
after two iterations versus standard widening after five iterations and
standard widening versus threshold widening. Figure 2b shows the variable
reductions for Zones with threshold widening versus Relational Predicates.
Considering a single bin in Figure 2, for example, $0.1$, represents the
frequency where Algorithm 1 needed only $10\%$ of the variables occurring in
the original invariants to adequately compare the two.

Shown in Figure 2, the large frequencies in the $0$ bin shows our technique
was able to remove all variables from the invariants from comparison,
eliminating the need to compare the two invariants. Comparing advanced
techniques utilizing Zones shows more than $6500$ instances, and about $1850$
in Zones versus Relational Predicates.

Our technique reduces the number of variables necessary for comparison by
$50\%$ or more in $90\%$ of comparisons between techniques of Zones, and at
least by $25\%$ in $93\%$ of comparisons. For Zones and Relational Predicates,
our technique reduces the necessary, relevant variables by $50\%$ or more in
$80\%$ of comparisons and by $12\%$ in $93\%$ of comparisons. That is, in the
majority of comparisons, our technique reduces the number of variables
necessary for comparing two relational domains or techniques. The quality of a
domain’s $\Delta$ function affects the performance and effectiveness of
Algorithm 1. We see only a few iterations in the algorithm when comparing
analysis techniques utilizing Zones since we used a minimal $\Delta$ function
for Zones. However, we see an increase in iterations when comparing with a
non-optimal $\Delta$, as in Zones and Relational Predicates. That is, the
quality of $\Delta$ can have an outsized impact on the practicality of our
technique. However, given the preponderance of variable reductions and low
iteration counts over the corpus of methods and comparisons, we conclude that
the proposed algorithm is practical and effective.

###  5.4 Discussion

The evaluation results show our technique enables more precise comparison
between relational abstract domain invariants. When comparing two techniques
using the same domain, our minimal comparison strategy precisely captures the
techniques’ relative precision, disentangling accumulated, _carry-over_
effects from realized precision gains.

While we do not have a proven state minimization function for Relational
Predicates, our technique still shows improvement when comparing incomparable
relational abstract domains. Specifically, our comparison removes unknowns and
dramatically reduced incomparable invariants, which makes it easier to make
software engineering decisions.

The average iteration depth for Algorithm 1 shows the algorithm’s efficiency
and practicality. Even when using an imprecise minimization function for
Relational Predicates, our technique only needed a maximum of _four_
iterations to arrive at a stable set of common variables for comparison.
Moreover, in the majority of comparisons, Algorithm 1 returned a significantly
smaller proportion of variables than the entirety of the variables in each
invariant, demonstrating the efficacy of the technique.

##  6 Related Work

Our previous work [3] found a set of algorithms for efficiently computing
$\Delta$ for the Zones domain. Using the algorithms, it compared Zones to
other non-relational domains, which in the context of data-flow analysis (DFA)
and this work, have trivial $\Delta$ functions. We extend the previous work by
considering comparisons between relational abstract domains, abstracting the
$\Delta$ function for each domain.

Comparing the precision gain of new analysis techniques or comparing the
precision of newly proposed abstract domains is a common problem in the
literature. Previous work in this area generally compare precision in one of
two ways. One, the comparison is based on known a priori program properties on
benchmark programs [7, 8, 9, 13, 14]. Two, the comparison is based on logical
entailment of computed invariants [9, 16, 20].

To the best of our knowledge, this work represents one of the first studies
improving the granularity of precision characteristics for the latter
categorization of relational abstract precision comparisons. We believe this
work would benefit existing work which compares relational abstract domains or
new analysis techniques using relational abstract domains.

##  7 Conclusion and Future Work

In this study, we defined the problem of minimally comparing relational
invariants, proposed an algorithm which solves the problem, and experimentally
evaluated whether the algorithm indeed solves the problem using real-world
programs. Using our algorithm, we can remove the precision _carry-over_
effects advanced analysis techniques introduce, providing clear precision
benefits for advanced techniques. For example, the benefits of deferred
widening and threshold widening are smaller than anticipated. Moreover, our
technique enables the comparison of relational abstract domains which are
otherwise difficult to compare directly. Specifically, we see our technique
removed the UNKNOWN invariants and dramatically reduced the incomparable
invariants when comparing Zones to Relational Predicates. Finally, Algorithm
1’s average iteration depth and variable reduction demonstrate the algorithm’s
overall practicality and usefulness when comparing analysis techniques and
relational abstract domains.

####  7.0.1 Future Work

Developing a minimization function, $\Delta$ for Relational Predicates would
enable a comprehensive, empirical study of the relative precision of weakly-
relational numerical abstract domains to Predicates. Furthermore, we believe
the proposed technique of comparison can benefit adaptive analysis techniques
which selectively choose the appropriate abstract domain during analysis.
Octagons [17] are not included in this study because a minimization strategy
for Octagons has not been developed. However, this is an interesting avenue to
pursue and we intend to use the technique of this work to compare Zones to
Octagons, which will empirically quantify the precision gain of Octagons over
Zones.

## References

  * [1] Abate, C., Blanco, R., Ciobâcă, c., Durier, A., Garg, D., Hritţcu, C., Patrignani, M., Tanter, E., Thibault, J.: An extended account of trace-relating compiler correctness and secure compilation. ACM Transactions on Programming Languages and Systems 43(4), 1–48 (Dec 2021). https://doi.org/10.1145/3460860
  * [2] Ballou, K., Sherman, E.: Incremental transitive closure for zonal abstract domain. NASA Formal Methods p. 800–808 (2022). https://doi.org/10.1007/978-3-031-06773-0_43
  * [3] Ballou, K., Sherman, E.: Identifying minimal changes in the zone abstract domain (2023), to appear in upcoming Theoretical Aspects of Software Engineering 2023, accessible at https://arxiv.org/abs/2304.14550
  * [4] Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation - PLDI ’03 (2003). https://doi.org/10.1145/781131.781153
  * [5] Collberg, C., Myles, G., Stepp, M.: An empirical study of java bytecode programs. Software: Practice and Experience 37(6), 581–641 (2007). https://doi.org/10.1002/spe.776
  * [6] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. p. 238–252. POPL ’77, Association for Computing Machinery, New York, NY, USA (1 1977). https://doi.org/10.1145/512950.512973
  * [7] Gange, G., Ma, Z., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: A fresh look at zones and octagons. ACM Transactions on Programming Languages and Systems 43(3), 1–51 (Sep 2021). https://doi.org/10.1145/3457885
  * [8] Gurfinkel, A., Chaki, S.: Boxes: A symbolic abstract domain of boxes. Lecture Notes in Computer Science p. 287–303 (2010). https://doi.org/10.1007/978-3-642-15769-1_18
  * [9] Howe, J.M., King, A.: Logahedra: A new weakly relational domain. Lecture Notes in Computer Science p. 306–320 (2009). https://doi.org/10.1007/978-3-642-04761-9_23
  * [10] Katz, S.: Program optimization using invariants. IEEE Transactions on Software Engineering SE-4(5), 378–389 (Sep 1978). https://doi.org/10.1109/tse.1978.233858
  * [11] King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (Jul 1976). https://doi.org/10.1145/360248.360252, http://dx.doi.org/10.1145/360248.360252
  * [12] Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proceedings Real-Time Systems Symposium. pp. 14–24. IEEE Comput. Soc (1997). https://doi.org/10.1109/real.1997.641265
  * [13] Laviron, V., Logozzo, F.: Subpolyhedra: A (more) scalable approach to infer linear inequalities. Verification, Model Checking, and Abstract Interpretation p. 229–244 (2008). https://doi.org/10.1007/978-3-540-93900-9_20
  * [14] Logozzo, F., Fähndrich, M.: Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. Science of Computer Programming 75(9), 796–807 (9 2010). https://doi.org/10.1016/j.scico.2009.04.004
  * [15] Miné, A.: A new numerical abstract domain based on difference-bound matrices. Lecture Notes in Computer Science p. 155–172 (2001). https://doi.org/10.1007/3-540-44978-7_10
  * [16] Miné, A.: Weakly Relational Numerical Abstract Domains (12 2004), https://pastel.archives-ouvertes.fr/tel-00136630
  * [17] Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (3 2006). https://doi.org/10.1007/s10990-006-8609-1, http://dx.doi.org/10.1007/s10990-006-8609-1
  * [18] de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. Lecture Notes in Computer Science p. 337–340 (2008). https://doi.org/10.1007/978-3-540-78800-3_24
  * [19] OSS, S.: Soot (2020), https://soot-oss.github.io/soot/
  * [20] Sherman, E., Dwyer, M.B.: Exploiting domain and program structure to synthesize efficient and precise data flow analyses (t). 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE) (11 2015). https://doi.org/10.1109/ase.2015.41
  * [21] Tange, O.: Gnu parallel 20220722 (’roe vs wade’) (Jul 2022). https://doi.org/10.5281/zenodo.6891516, GNU Parallel is a general parallelizer to run multiple serial command line programs in parallel without changing them.
  * [22] Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a java bytecode optimization framework. In: Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research. p. 13. CASCON ’99, IBM Press (1999)
  * [23] Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: Reducing, reusing and recycling constraints in program analysis. Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (Nov 2012). https://doi.org/10.1145/2393596.2393665, http://dx.doi.org/10.1145/2393596.2393665
  * [24] Zhu, H., Magill, S., Jagannathan, S.: A data-driven chc solver. Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Jun 2018). https://doi.org/10.1145/3192366.3192416

  *[SMT]: satisfiability modulo theories
  *[DFA]: data-flow analysis
  *[SMT-LIB]: satisfiability modulo theories library
  *[MN]: Minimal Neighbors
  *[JVM]: Java virtual machine
  *[LIA]: linear integer arithmetic
  *[NIA]: non-linear integer arithmetic


11institutetext:  Pyrofex Corp.
11email<EMAIL_ADDRESS>
22institutetext: Synereo, Ltd
22email<EMAIL_ADDRESS>
# Logic as a distributive law

Michael Stay
11 L.G. Meredith
22

###### Abstract

We present an algorithm for deriving a spatial-behavioral type system from a
formal presentation of a computational calculus. Given a 2-monad
$\mathrm{Calc}\colon\mathrm{Cat}\to\mathrm{Cat}$ for the free calculus on a
category of terms and rewrites and a 2-monad BoolAlg for the free Boolean
algebra on a category, we get a 2-monad Form = BoolAlg + Calc for the free
category of formulae and proofs. We also get the 2-monad
$\mathrm{BoolAlg}\circ\mathrm{Calc}$ for subsets of terms.

The interpretation of formulae is a natural transformation
$\llbracket-\rrbracket\colon\mathrm{Form}\Rightarrow\mathrm{BoolAlg}\circ\mathrm{Calc}$
defined by the units and multiplications of the monads and a distributive law
transformation
$\delta\colon\mathrm{Calc}\circ\mathrm{BoolAlg}\Rightarrow\mathrm{BoolAlg}\circ\mathrm{Calc}.$
This interpretation is consistent both with the Curry-Howard isomorphism and
with realizability.

We give an implementation of the “possibly” modal operator parametrized by a
two-hole term context and show that, surprisingly, the arrow type constructor
in the $\lambda$-calculus is a specific case. We also exhibit nontrivial
formulae encoding confinement and liveness properties for a reflective higher-
order variant of the $\pi$-calculus.

##  1 Introduction

Sylvester coined the term “universal algebra” to describe the idea of
expressing a mathematical structure as set equipped with functions satisfying
equations; the idea itself was first developed by Hamilton and de Morgan [7].
Most modern programming languages have a notion of a “module” or an
“interface” with this same information; for example, consider this Agda
definition of a monoid.

        data Monoid (M : Set)(Eq : Equivalence M) : Set where
          monoid :
            (e   : M)
            (_*_ : M -> M -> M)
            (leftId : LeftIdentity Eq z _+_)
            (rightId : RightIdentity Eq z _+_)
            (assoc : Associative Eq _+_) ->
               Monoid M Eq

The code defines a sort $M$, a nullary term constructor $e$, and a binary term
constructor $*,$ subject to three equations. In universal algebra, such a
structure is called an “equational theory”.

In 1963, Lawvere [13] showed that an equational theory was a presentation of a
category with finite products where all the objects are powers of a single
generating object; such a category is now called a Lawvere theory. The Agda
code above is a presentation of a category Th(Mon) whose objects are
$1,M,M^{2},M^{3},\ldots,$ and whose morphisms are generated by projections,
$e,$ and $*,$ modulo the equations. This category is purely syntactic.

To interpret the equational theory as denoting sets and functions, we use a
product-preserving functor from the Lawvere theory to Set: such a functor maps
$M$ to a set and $e$ and $*$ to functions satisfying the equations. The
category Set encodes what we mean by semantics; if instead of Set we used the
category Vect of vector spaces and linear maps and mapped the product in
Th(Mon) to the tensor product in Vect, a model of the theory would be an
associative algebra instead. If we used a category of endofunctors and natural
transformations and mapped the product in Th(Mon) to composition, a model of
the theory would be a monad.

The category of product-preserving functors from Th(Mon) to Set and natural
transformations between them is equivalent to the category Mon of monoids and
monoid homomorphisms. There is a forgetful functor
$U\colon\mathrm{Mon}\to\mathrm{Set}$ that forgets all the structure with a
left adjoint $L\colon\mathrm{Set}\to\mathrm{Mon}$ that picks out the free
monoid on a set. Abusing notation somewhat, we use Mon also to mean the monad
$UL$ that picks out the underlying set of the free monoid on a set. This
pattern is a general one: every Lawvere theory corresponds to a finitary monad
on Set and vice-versa [8].

Often modules or interfaces are used to model data structures. In computing,
however, we consider not only the structure of data but the behavior of
processes that change the data. The $\lambda$-calculus is the paradigmatic
model of functional programming. It has a single data type, called lambda
term, described by a one-line grammar. In this model, computation consists of
repeatedly applying a single rewrite rule called $\beta$-reduction; the
rewrite rule matches the current term to a pattern, then rearranges the parts
of the term. When the term no longer matches the pattern, the rewriting stops
and the resulting term is taken as the “answer”. Similarly, the
$\pi$-calculus, arguably the paradigmatic model of concurrent programming, has
a structured data type called a process that is also described by a simple
grammar. Computations in the $\pi$-calculus are carried out by repeatedly
applying rewrite rules, primarily the $\mathsf{comm}$-rule.

This pattern has been recognized and formalized many times. In his seminal
paper, “Functions as Processes” [19], Milner developed what is now the
standard presentation of a computational calculus. The presentation consists
of a grammar describing the primary data type over which computations are
carried out, a structural equivalence, used to erase syntactic differences
that are irrelevant to computation, and a set of rewrite rules describing how
to realize computation through operations on the data structures. On one hand,
this generalizes universal algebra’s generators and relations presentation,
with the grammar replacing the generators as the free construction, the
structural equivalence replacing the relations, and the rewrites providing the
computational semantics. On the other hand, this presentation maps quite well
onto Plotkin’s SOS format for operational semantics [20], but the scope is
much larger. Even the presentation of the Java VM can be seen as essentially a
rewrite system with the state of the virtual machine as instances of a data
type over which computation is carried out, and the transitions of the virtual
machine as the rewrite rules [9]. Capturing this higher-order computational
phenomena, expressed as generalized rewrites, is what motivates our movement
to higher categorical semantics.

Lawvere theories can be generalized from 1-categories to 2-categories. As one
might expect, the corresponding notion of equational theory involves one more
level of structure; we have sorts, term constructors, rewrites instead of
equations between term constructors, and equations between rewrites. We
typically interpret such a theory in Cat, the 2-category of categories,
functors and natural transformations.

We can use Lawvere 2-theories to describe terms in a computational calculus
and the permissible rewrites. We have a sort for terms; our examples are
necessarily simple calculi due to space constraints, but our approach should
work with any formalization of a computational model such as the K framework
[21], the “kiama” Scala package [24], even packages largely focused on
documentation and specification, such as Ott [23]. We also have term
constructors for building up specific terms, rewrites between term
constructors for running programs, and equations between rewrites to preserve
invariants. The Lawvere 2-theory captures the syntax of a computational
calculus; a 2-functor from the theory into Cat assigns operational semantics.
Note that this is fully consistent with Curry-Howard style interpretations.

A spatial-behavioral type system is a language in which one can describe both
the structure and future behavior of terms. In keeping with realizability
style semantics [10], the interpretation of a formula should be a set of terms
satisfying the formula. The interpretation of a proof should be a function
that maps a set of assumptions to a set of consequents.

The obvious language for describing the structure of a term is the 2-theory
Th(Calc) of the calculus itself, equipped with extra term constructors for
true, false, disjunction, conjunction, and negation. This suggests adding the
2-monad Calc to the 2-monad BoolAlg for Boolean algebras to get Form, the
2-monad for formulae.

The obvious language for interpreting formulae is the 2-category of subsets of
terms with pointwise rewrites between them. This suggests composing the monad
BoolAlg with the monad Calc.

The obvious way to interpret formulae is then a natural transformation
$\llbracket-\rrbracket\colon\mathrm{Form}\Rightarrow\mathrm{BoolAlg}\circ\mathrm{Calc}$
defined by the units and multiplications of the monads and a distributive law
transformation
$\delta\colon\mathrm{Calc}\circ\mathrm{BoolAlg}\Rightarrow\mathrm{BoolAlg}\circ\mathrm{Calc}.$

We can extend this naive type system with fixed points and with modal
operators that denote sets of terms that all exhibit a particular behavior;
for an example of the latter, the arrow type $A\Rightarrow B$ in the
$\lambda$-calculus is the type of terms that when applied to a term of type
$A$ eventually rewrite to a term of type $B$. Other formulae can capture
eventual properties like

  * •

Authority: it is the case that if my banking service eventually evolves to a
state in which Alice has the ability to withdraw money from my account, then
the banking service both sent an email to my address requesting confirmation
and received the confirmation email in response.

  * •

Confinement: this process will only ever send a messages on channels in this
set.

  * •

Liveness: this process will always eventually handle another message.

  * •

Termination: this computation will always halt.

  * •

Structure: at the end of sorting, the data will be ordered.

The slogan “logic via distributive law” is more apt than might first be
supposed, however. At heart, the algorithm says that logical formula can be
thought of as describing collections of terms in terms of terms built over
collections. Since a very broad class of collections are captured via the
notion of monad, the distributive law, together with the monad laws are
iteratively applied to instances of the latter to arrive at instances of the
former. In this sense $\mathrm{BoolAlg}$ is just one notion of “collection”,
namely that of $\mathrm{Set}$. There are other notions of collection, such as
list, bag, tree, all of which are captured as monads and for which we could
use a distributive law to provide a semantics for a notion of formula that has
utility and considerable expressive power. Thus, for example, if the notion of
collection were _sets of sequences_ , then the semantics generated by our
algorithm would interpret formulae as sets of sequences of terms, instead of
sets of terms, and the term language extracted for the collection monad would
be the familiar operators of classical linear logic and this would correspond
to the well-known fact that quantales provide full and faithfull models of the
_formulae_ of linear logic. The higher categorical machinery provides the
right setting in which to express this idea in it’s full generality. In this
paper, however, we focus the exegesis of these results on $\mathrm{BoolAlg}$
to conserve space, and highlight the core ideas.

##  2 Related work

There is a very large body of work on Lawvere theories and their
generalizations, and we cannot give a proper review here; instead we list a
few key papers with many references. Hyland and Power [8] reviewed the history
of both Lawvere theories and monads as an approach to universal algebra, how
monads came to the fore, Plotkin’s work, and the renewed interest in Lawvere
theories in a computer science setting. Trimble [26] constructed multisorted
Lawvere theories. Lack and Rosický [11] unified the work of several earlier
authors by considering models in categories other than Set, extending the
notion of Lawvere theory to enriched categories, and using all limits rather
than just products all at once.

Our results can be seen as a natural consequence of Abramsky’s programme, laid
out in “Domain theory in Logical Form” [1], and expanded in “Proofs as
Processes” [2]. Moreover, they can be seen as bringing the seminal work of
Caires [4] under the rubric of that programme.

##  3 A 1-categorical example

Here we return in slightly greater detail to the example of the logic for the
language of monoids. Because we are working with categories instead of
2-categories, the “virtual machine” is particularly bland; it only has terms
(the elements of the monoid), not rewrites.

Let FinSet be a skeleton of the category of finite sets. The Lawvere theory of
a computational calculus is a category Th(Calc) with finite products equipped
with an identity-on-objects functor
$\theta\colon\mathrm{FinSet}^{\mathrm{op}}\to\mathrm{Th(Calc)}.$ Because the
objects of FinSet are coproducts of the one-element set, the objects of
category Th(Calc) are therefore products of a generating object we will write
as $S,$ for “sort”. The morphisms of Th(Calc) are generated from a set of
morphisms from finite powers of $S$ to $S$ by products and composition, so
Th(Calc) may be presented by

  * •

a sort $S$,

  * •

a set of term constructors $f_{i}\colon S^{n_{i}}\to S,$ where $i$ ranges over
some index set $I$ and $n_{i}\in\mathbb{N},$

  * •

and a set of equations between term constructors.

We say the arity of $f_{i}$ is $n_{i}.$

A product-preserving functor from Th(Calc) to Set picks out a set and equips
it with structure maps satisfying the equations. The category Prod(Th(Calc),
Set) of product-preserving functors and natural transformations between them
is equivalent to the category Calc of calculi and calculus homomorphisms.
There is a forgetful functor ${U\colon\mathrm{Calc}\to\mathrm{Set}}$ that
forgets the extra structure. The functor $U$ has a left adjoint
${L\colon\mathrm{Set}\to\mathrm{Calc}}$ that picks out the free calculus on a
set of base terms. The monad
$\mathrm{Calc}=UL\colon\mathrm{Set}\to\mathrm{Set}$ picks out the underlying
set $ULX$ of the free calculus $LX$ on a set $X$. Lawvere theories are in
bijection with finitary monads; the qualifier “finitary” means that each term
constructor has a finite arity.

Here is a presentation of the “Lawvere theory of a monoid” Th(Mon):

Sorts:  • $S$
Term constructors:  • $\cdot\colon S^{2}\to S$ • $e\colon 1\to S$ |  Equations:  • $\cdot\circ(S\times\cdot)=\cdot\circ(\cdot\times S)$ (associativity) • $\cdot\circ(e\times S)\circ\mathrm{left}^{-1}=S$ (left unit) • $\cdot\circ(S\times e)\circ\mathrm{right}^{-1}=S$ (right unit)
---|---

where ${\mathrm{left}\colon 1\times S\stackrel{{\scriptstyle\sim}}{{\to}}S}$
and ${\mathrm{right}\colon S\times 1\stackrel{{\scriptstyle\sim}}{{\to}}S}$
are the canonical isomorphisms.

An implementation of this specification is a product-preserving functor from
Th(Mon) to Set; such a functor will assign a set of values to the sort and
functions to the term constructors such that the equations are satisfied, i.e.
it will pick out a monoid. The category of product-preserving functors from
Th(Mon) to Set and natural transformations between them is equivalent to the
category of monoids and monoid homomorphisms. There is a forgetful functor
$U\colon\mathrm{Mon}\to\mathrm{Set}$ that forgets the multiplication and unit,
and outputs the underlying set of elements. The functor $U$ has a left adjoint
$L\colon\mathrm{Set}\to\mathrm{Mon}$ that outputs the free monoid on a set.
The composite functor $\mathrm{Mon}=UL\colon\mathrm{Set}\to\mathrm{Set}$ is
the corresponding monad.

All our formulae about monoids will denote subsets of the elements of the
monoid; we use Th(BoolAlg) to describe them.

Sorts:  • $S$ Term constructors:  • $\land,\lor\colon S^{2}\to S$ • $\top,\bot\colon 1\to S$ • $\neg\colon S\to S$ |  Equations:  • associativity, commutativity and unit laws for $\land$ and $\lor$ • distributivity of $\land$ over $\lor$ • involution for $\neg$ • de Morgan’s laws
---|---

From this theory, we can derive the monad BoolAlg for the free Boolean algebra
on a set.

The sum of the two theories above is a new theory Th(Form) = Th(Mon) +
Th(BoolAlg) whose terms are our formulae. Th(Form) is presented by identifying
the sorts and taking the union of the term constructors and the union of the
equations.

The process of deriving a monad from a theory preserves sums. Since the sum of
two monads is the free product of the two, a general formula will be a term in
an alternating composition of the two monads. For example, suppose that
$a,b,c,d\in X;$ then one formula is

$(({a}\lor{(b\cdot d)})\cdot({c}\lor{d})),$

which is a term in Mon(BoolAlg(Mon($X$))). The interpretation of this formula
should be the set of monoid elements

$\\{ac,ad,bdc,bdd\\},$

or in other words, the term

$(a\cdot c)\lor(a\cdot d)\lor((b\cdot d)\cdot c)\lor((b\cdot d)\cdot d)$

in BoolAlg(Mon(X)).

In order to move all the uses of Mon to the right of the uses of BoolAlg in
the alternating composition, we need a distributive law natural transformation

$\delta\colon\mathrm{Mon}\circ\mathrm{BoolAlg}\Rightarrow\mathrm{BoolAlg}\circ\mathrm{Mon}.$

Given $\delta$ and the monad units and multiplications, we can define an
interpretation natural transformation

$\llbracket-\rrbracket\colon\mathrm{Form}\Rightarrow\mathrm{BoolAlg}\circ\mathrm{Mon}$

in the obvious way. Below, we write subsets of Mon($X$) using set notation:

$\llbracket\top\rrbracket_{X}$ | = $\mathrm{Mon}(X)$ | $\llbracket\bot\rrbracket_{X}$ | = $\emptyset$
---|---|---|---
$\llbracket{A}\lor{B}\rrbracket_{X}$ | = $\llbracket A\rrbracket_{X}\cup\llbracket B\rrbracket_{X}$ | $\llbracket{A}\land{B}\rrbracket_{X}$ | = $\llbracket A\rrbracket_{X}\cap\llbracket B\rrbracket_{X}$
$\llbracket\neg A\rrbracket_{X}$ | = $\mathrm{Mon}(X)-\llbracket A\rrbracket_{X}$ | $\llbracket{A}\cdot{B}\rrbracket_{X}$ | = $\mathrm{Mon}(\cdot)(\llbracket A\rrbracket_{X}\times\llbracket B\rrbracket_{X})$
$\llbracket e\rrbracket_{X}$ | = $\\{e\\}$ | $\llbracket x\in X\rrbracket_{X}$ | = $\\{x\\}$

Even in this simple example, we have nontrivial formulae; for example,

$prime=\neg e\land\neg(\neg e\cdot\neg e)$

is a 1-line formula for primality. For the monoid of natural numbers under
multiplication, this formula says a number is prime if it is neither 1 nor has
a nontrivial factorization. It is easy to verify that $\llbracket
prime\rrbracket_{X}=X.$

##  4 Moving to 2-categories

In a computational context, when a data structure has some symmetry we do not
care about, we often test two instances of the structure for equality by
computing a normal form for each instance and then comparing the normal forms.
Monoids are associative, but we can imagine storing words of a monoid as
binary trees internally and then comparing them by computing a normal form.
For the case of a normal form for the trees, we can eliminate 1 in a product
by rewriting $(1\cdot x)$ and $(x\cdot 1)$ to $x$, and we can shift all the
parentheses to the right by rewriting $((x\cdot y)\cdot z)$ to $(x\cdot(y\cdot
z)).$

The Lawvere 2-theory Th(Mon) is much the same as the 1-theory, except for the
weakening of some equations to rewrites and the addition of new equations
between the rewrites.

Sorts:  • $S$ Term constructors:  • $\cdot\colon S^{2}\to S$ • $e\colon 1\to S$ |  Rewrites:  • $a\colon\cdot\circ(S\times\cdot)\Rightarrow\cdot\circ(\cdot\times S)$ • $l\colon\cdot\circ(e\times S)\circ\mathrm{left}^{-1}\Rightarrow S$ • $r\colon\cdot\circ(S\times e)\circ\mathrm{right}^{-1}\Rightarrow S$ Equations:  • $a\circ a=(S\times a)\circ a\circ(a\times S)$ (pentagon equation) • $r\times S=(S\times l)\circ a$ (triangle equation)
---|---

From Th(Mon) we can derive a 2-monad Mon that essentially produces the free
monoid on a set, but keeps track of the internal representation of the
monoid—a binary tree—and accounts for the work needed to convert the internal
representation to its normal form. From this perspective, we can think of the
trees as programs for a simple computational calculus and the process of
normalization as the execution of the program. Later in the paper, we will
examine the case of the SKI combinator calculus, a Turing-complete programming
language that was a predecessor to the $\lambda$-calculus; it, too, uses
binary trees as programs, and execution of the program is a normalization
process.

When we add the 2-monad BoolAlg to Mon, we get formulae like $(1\cdot\top)$
denoting the set of trees whose leftmost child is the identity; because Mon is
a 2-monad, we also get proofs like

$((r\circ l)\lor y)\colon((e\cdot(x\cdot e))\lor y)\to(x\lor y)$

whose interpretations are homomorphisms of Boolean algebras.

The formulae in these examples have been propositions about the structure of
terms. Later in the paper, we will also show how to add modal operators that
are propositions about the behavior of terms; the arrow type constructor from
the $\lambda$-calculus is a prominent example.

##  5 Multisorted Lawvere theories

In the motivation section, each theory had only one sort; practical theories
for virtual machines are usually multisorted. Given a finite set of sorts
$\Sigma,$ the category $\mathrm{FinSet}/\Sigma$ is the category whose objects
are pairs $(S,s\colon S\to\Sigma),$ where $S$ is a finite set, and whose
morphisms are functions $f\colon S\to S^{\prime}$ such that the relevant
triangle commutes.

A multisorted Lawvere theory is a category Th(Calc) with finite products
equipped with an identity-on-objects functor
${\theta\colon(\mathrm{FinSet}/\Sigma)^{\mathrm{op}}\to\mathrm{Th(Calc)}.}$
The category Prod(Th(Calc), $\mathrm{Set}^{\Sigma}$) is equivalent to the
category Calc of calculi and calculus homomorphisms. There is a forgetful
functor ${U\colon\mathrm{Calc}\to\mathrm{Set}^{\Sigma}}$ with a left adjoint
${L\colon\mathrm{Set}^{\Sigma}\to\mathrm{Calc}}$ that picks out the free
calculus on a $|\Sigma|$-tuple of sets. The monad
${UL\colon\mathrm{Set}^{\Sigma}\to\mathrm{Set}^{\Sigma}}$ picks out the
underlying $|\Sigma|$-tuple of sets $ULX$ of the free calculus $LX$ on a
$|\Sigma|$-tuple of sets $X$.

An example of a multisorted Lawvere theory is that of a group action on a set,
which involves a choice of both a group $G$ and a set $V$ to act on. The
presentation of Th(GrpAct) has a pair of sorts $(G,V)$, all the term
constructors and equations as the theory of a group (where we replace $S$ by
$G$), together with a new term constructor

  * •

$a\colon G\times V\to V$

and equations

  * •

$a\circ(e\times V)\circ\mathrm{left}^{-1}_{V}=V$ (identity action)

  * •

$a\circ(m\times V)=a\circ(G\times a)$ (compatibility).

Another example is the theory of a directed graph, with one sort for vertices
and another for edges, with source and target maps for term constructors.

##  6 Lawvere 2-theories

In this paper, the multisorted Lawvere 2-theory of a calculus is a 2-category
Th(Calc) with strict finite products (that is, its underlying category has
products) equipped with an identity-on-objects functor
$\theta\colon(\mathrm{FinSet}/\Sigma)^{\mathrm{op}}\to\mathrm{Th(Calc)},$
where we promote $(\mathrm{FinSet}/\Sigma)$ to a 2-category by adding identity
2-morphisms to every 1-morphism. As noted in the related work section, other
authors have considered much more powerful notions of 2-theory, but we will,
for the most part, not need the extra features; however, see the notion of
“lambda theory” below. Our notion of a multisorted Lawvere 2-theory may be
presented by a finite set of sorts, a set of term constructors with finite
arity, a set of rewrites, and a set of equations between rewrites.

Our models of multisorted Lawvere 2-theories are functors into
$\mathrm{Cat}^{\Sigma}$ that preserve products up to isomorphism, not merely
up to equivalence; that is, the 2-functor has an underlying functor that
preserves products. As with 1-theories, the 2-category of product-preserving
functors from Th(Calc) to $\mathrm{Cat}^{\Sigma}$, natural transformations,
and modifications is equivalent to the 2-category of calculi, calculus
homomorphisms, and calculus transformations.

As mentioned above, the SKI combinator calculus is a Turing-complete language;
it was invented by Schönfinkel [22] and Curry [5] in the 1920s as a way to
clarify the role of quantified variables in logic, essentially by eliminating
them. The single-sorted Lawvere 2-theory Th(SKI) has a presentation

Sorts:  • $T$ Term constructors:  • $S,K,I\colon 1\to T$ • $(-\;-)\colon T^{2}\to T,$ |  Rewrites:  • $\forall x,y,z\in T,\quad\sigma\colon(((S\;x)\;y)\;z)\Rightarrow((x\;z)\;(y\;z))$ • $\forall y,z\in T,\quad\kappa\colon((K\;y)\;z)\Rightarrow y$ • $\forall z\in T,\quad\iota\colon(I\;z)\Rightarrow z$ No equations.
---|---

In this context, the Church-Rosser theorem for the SKI calculus says that any
two terminating rewrites out of an SKI term have the same codomain. We do not
usually want to impose equality on the rewrites, since they can differ greatly
in computational complexity. For example, suppose that we have the term
$((K\;I)\;x),$ where $x$ is some term that takes a long time to reduce to its
normal form; a rewrite that reduces $x$ first and then uses $\kappa$ takes
much longer than just doing $\kappa$ first, though both rewrites begin and end
at the same term.

The free model of Th(SKI) on a category takes its objects as terms and its
morphisms as rewrites, then freely adjoins $S,K,$ and $I$ and all applications
of one object to another, as well as new morphisms generated by
$\sigma,\kappa,$ and $\iota.$ The free model on the empty category will
contain only terms and rewrites from the SKI calculus.

Just as Lawvere theories capture the notion of a set equipped with functions
satisfying equations, 2-Lawvere theories capture the notion of a category
equipped with functors and natural transformations satisfying equations. The
former describes what might be called data structures, while the latter
captures both the state of a system and the processes that update that state.
In the next section, we introduce a language for talking about sets of states
and updates that satisfy some criterion, terms and rewrites that share some
property.

##  7 Categories of formulae and proofs

Any 1-theory can be promoted to a 2-theory by turning each equation into a
rewrite, then adding an equation asserting that the rewrite is equal to the
identity rewrite. Therefore as before, given a single-sorted Lawvere 2-theory
Th(Calc), we get a 2-theory of formulae Th(Form) by adding the 2-theory of
Boolean algebras Th(BoolAlg). The models of Th(Form) are categories of
formulae and proofs.

For multisorted Lawvere 1- and 2-theories, there is no canonical choice of
sorts to identify between the theory of the calculus and the theory of Boolean
algebras; one may choose to add one or more different copies of Th(BoolAlg)
and identify each single sort with different sorts in the theory of the
calculus. For example, given the theory of a group action, one could add a
copy of Th(BoolAlg) for both $G$ and $V$ and write formulae involving subsets
of the group and of the set it acts on. Later in the paper, we will see how we
can use formulae involving names to create namespaces that enforce confinement
on processes in the $\pi$-calculus.

##  8 Interpretation

When describing the semantics of a logic, questions of soundness and
completeness are natural. The whole point of our approach is that it is
correct by construction. Soundness and completeness for the modal-free
fragment follow directly from the definitions; soundness, in particular, is a
direct consequence of the way realizability is incorporated into the approach.
For the formulae, the intuitions underlying the completeness argument amount
to the fact that the term language for the logical operators associated with
the collections are extractions of a term language for the collection monad.
Thus, they are in perfect correspondence with the model. In the case of
$\mathrm{Set}$, this is equivalent to the well-known fact that boolean
algebras are effectively realized by the powerset lattice.

Likewise, in the case of $\mathrm{Set}$, the semantics that maps formulae to
the composition of the collection monad with the monad for the term language
supporting computation is nothing more than a pointwise lifting of the
powerset semantics. The categorical presentation provides an appropriately
abstracted form of this simple observation. In particular, interpretation is a
natural transformation between 2-monads on Cat; it assigns to each category
$X$ a functor

$\llbracket-\rrbracket_{X}\colon(\mathrm{BoolAlg}+\mathrm{Calc})(X)\to(\mathrm{BoolAlg}\circ\mathrm{Calc})(X).$

Functoriality means that the interpretation is sound; if the functor is full,
the interpretation is complete. Since we define interpretation in terms of the
monad laws and BoolAlg + Calc is the free product on the two monads,
$\llbracket-\rrbracket_{X}$ is the identity when restricted to
$(\mathrm{BoolAlg}\circ\mathrm{Calc})(X)$ and thus full.

Notice we have said nothing about the faithfulness of this functor. In
particular, if we consider rewrites as equalities then proofs (and therefore
homsets) collapse, recovering the usual situation of posets as models of
classical logic. On the other hand, when they are not treated as equalities,
we are able to distinguish proofs, even in the classical setting. There is
much, much more to say about this and other phenomena associated with Joyal’s
lemma [3], but we defer the discussion to another paper.

##  9 Modal operators

So far, all the examples of formulae have dealt with the structure of the
term. Far more interesting are sets of terms that all share some behavior. For
example, in the SKI calculus, we want to add the idea of an arrow type to our
formulae, and have the interpretation of $A\Rightarrow B$ be the subset of
terms $t$ such that given a term $u\in\llbracket A\rrbracket$, the term
$(t\;u)$ eventually evolves to a term $v\in\llbracket B\rrbracket.$

This notion of eventuality is an example of a modal operator. Possibility is
another, where possibility is to eventuality as “there exists” is to “for
all”. In the SKI calculus, they coincide due to the fact that the calculus is
confluent, but they differ in the general case. Many interesting properties
can be stated in terms of eventual and possible states as noted earlier.

To add a modal operator to a formula language, we first add it formally as a
term constructor to the term theory, then add the collection theory as before.

To interpret the modal operator, we first interpret the formulae as above,
then interpret modal terms as collections of terms, then use the join from the
collection monad.

###  9.1 Example: Arrow types in the SKI calculus

The Lawvere 2-theory of the arrow type Th(Arrow) has one term constructor, no
rewrites, and no equations. The lack of rewrites and equations are because the
arrow is a purely formal type, and it is only in our choice of semantics that
it acquires its customary interpretation.

In order to avoid notational confusion between the arrow type constructor and
2-morphisms, we will use a triple-arrow in the theory.

Sorts:  • $T$ Term constructors:  • $\Rrightarrow\colon T^{2}\to T$ |  No rewrites; no equations.
---|---

We get the theory of SKI with arrow Th(SKIArr) by adding Th(SKI) to Th(Arrow),
and we get the theory of formulae Th(Form) by adding Th(SKIArr) to
Th(BoolAlg).

To interpret terms from Th(Form), we compose the interpretation natural
transformation above with another natural transformation
$\alpha\colon\mathrm{SKIArr}\Rightarrow\mathrm{BoolAlg}\circ\mathrm{SKI},$
followed by the join from the collection monad. In particular,

$\alpha(u\Rrightarrow v)=\\{t\;|\;\exists\rho\colon(t\;u)\Rightarrow v\\}.$

In Lambek’s 1980 paper [12] on the denotational semantics of the
$\lambda$-calculus, he defined a category whose objects were types and whose
morphisms were equivalence classes of lambda terms with one free variable. In
a future paper, we will show how Mellies and Zeilberger’s approach to type
refinement lets us recapitulate Lambek’s construction and extend the arrow to
a profunctor.

###  9.2 Modal operators parametric in a term constructor

A term context is a term with a “hole” that can be filled by some other term.
Given a Lawvere theory with a sort $S$ for terms, one can derive a new theory
of term contexts by replacing each term constructor $f\colon S^{n}\to S$ with
$n$ term constructors $f_{i}\colon S^{n-1}\to S$ where $1\leq i\leq n$. We
think of $f_{i}$ as being $f$ with the $i$th input being a hole. Equivalently,
if we have a theory with coproducts, we can replace each occurrence of $S$ on
the left-hand side of a term constructor with $S+1,$ where the new point
represents the hole.

The arrow type is a special case of a more general modal operator parametrized
by a two-hole term context $C.$ We denote the operator itself with angle
brackets as a reminder of the diamond “possibly” modality: $u\langle C\rangle
v.$ The interpretation is similar to that of the arrow:

$\llbracket u\langle C\rangle v\rrbracket=\\{t\;|\;\exists\rho\colon
C[t,u]\Rightarrow v\\};$

that is, $u\langle C\rangle v$ denotes those terms $t$ that when put in the
context $u$ may possibly evolve to $v.$

This definition is inspired by the work of Sewell, Leifer, and Milner, in
which they formalize the notion of a context-labelled transition [14]. Given
the now standard Hennessy-Milner interpretation of modal logics which
interpret possibility in terms of actions labelling transitions, when Sewell
et al. gave a notion of context-labelled transitions, it was only natural to
consider modal operators based on contexts.

##  10 Recursion

Suppose that we have a single-sorted Lawvere 2-theory of a calculus with sort
$S$. We add recursion to our formulae by introducing a new sort $V$ for type
variables and new term constructors

  * •

$-\colon V\to S$ to let us use type variables in formulae and

  * •

$\mu\colon V\times S\to S$ to express fixed points.

We interpret terms of the form $\mu X.P[X]$ as the greatest fixed point of
$P[X].$

###  10.1 The reflective higher-order $\pi$-calculus

Lawvere theories are limited in that they only talk about products of sorts. A
lambda theory is a generalization of a Lawvere theory that has the ability to
talk about function sorts like $A\Rightarrow B$ and sums like $A+B$ or
$1+A+A^{2}+\cdots,$ more commonly denoted with the Kleene star $A^{*}.$ One
can think of lambda theories as having access to a “library” that takes care
of the details of bound variables and substitution for us so we do not have to
implement all that machinery. Much of the work on nominal logics has been
about exactly this factorization [6]. A lambda theory Th(Calc) is a
bicartesian closed 2-category equipped with an identity-on-objects functor
from $(\mathrm{FinSet}/\Sigma)^{\mathrm{op}}$ to Th(Calc). Models of Th(Calc)
are functors to Cat that preserve all the structure.

The $\pi$-calculus was invented in the early 1990s by Robin Milner as a model
of networks of processes with a dynamically changing topology; two processes
initially unaware of each other can be introduced by a third process. The
reflective higher order $\pi$-calculus uses quoted processes as names; the
term constructors for quote and eval replace the more traditional nu and
replicate constructors. We also add a “comm” term to restrict the contexts in
which reduction can occur [25].

Here is a presentation of the multisorted lambda theory Th(RHOpi) for the
reflective higher-order $\pi$-calculus:

Sorts:  • $N$ for names • $P$ for processes
Term constructors:  • $\mathrm{send}\colon N\times P^{*}\to P$ • $\mathrm{recv}\colon N\times(N^{*}\Rightarrow P)\to P$ • $|\colon P^{2}\to P$ • $0\colon 1\to P$ • $\mathrm{comm}\colon 1\to P$ • $``-"\colon P\to N$ • $\mathrm{eval}(-)\colon N\to P$ |  Rewrites:  • $\alpha\colon(p_{1}|p_{2})|p_{3}\Rightarrow p_{1}|(p_{2}|p_{3})$ • $\beta\colon p_{1}|p_{2}\Rightarrow p_{2}|p_{1}$ • $\iota\colon 0|p\Rightarrow p$ • $\chi\colon\mathrm{send}(x,p_{1},\ldots,p_{n})\;|\;\mathrm{recv}(x,q)\;|\;\mathrm{comm}\Rightarrow q(``p_{1}",\ldots,``p_{n}")\;|\;\mathrm{comm}$ • $\epsilon\colon\mathrm{eval}(``p")\Rightarrow p$ Equations:  •
---|---

The simplest RHOpi processes are 0, the “do nothing” process; and comm, a
“catalyst” process that enables communication on a channel. The only rewrite
that is not an identity is $\chi,$ the communication event. The $\chi$ rewrite
is neither confluent nor deterministic. For example, we can model contention
for resources with the term

$\mathrm{recv}(x,P)\;|\;\mathrm{recv}(x,Q)\;|\;\mathrm{send}(x,R)\;|\;\mathrm{comm}$

which has two rewrites out of it, one where the continuation $P$ is invoked on
the name $``R"$ and the other where the continuation $Q$ is invoked on it. We
can model message arrival order nondeterminism with the term

$\mathrm{send}(x,P)\;|\;\mathrm{send}(x,Q)\;|\;\mathrm{recv}(x,R)\;|\;\mathrm{comm}$

which has two similar rewrites out of it, one where the continuation $P$ is
invoked on the name $``R"$ and one where $P$ is invoked on the name $``Q"$.

In the theory above, comm is preserved by the rewrites; one can think of each
comm instance as representing a processor. An alternative would be to consume
comm in the $\chi$ rewrite; then comm would track clock ticks; an application
of a consumable comm is the formal verification of billing code for tracking
compute resources.

Replication of processes, and therefore general recursion, can be encoded [16]
via

$D(x)=\mathrm{recv}(x,y\mapsto\mathrm{send}(x,\mathrm{eval}(y))|\mathrm{eval}(y))$

$!P=\mathrm{send}(x,D(x)|P)|D(x).$

Caires’ [4] operator $\triangleright$ for rely-guarantee properties, the
adjunct to $|,$ is an instance of our generic modal operator, where
$u\triangleright v=u\langle-|-\rangle v:$

$\llbracket u\triangleright
v\rrbracket=\\{t\;|\;\exists\rho\colon(t\;|\;u)\Rightarrow v\\}$

The logic is generated as above, adding modal operators and recursion to the
term language, then adding the Boolean algebra; it is equivalent to the logic
we generated by hand in [15]. As an example of a formula in this logic, here
is a one-line formula for a process that will always be able to handle another
message:

$\mu X.\mathrm{recv}(\top,x\mapsto X)\;|\;\top.$

It says that the process must factor into a piece that is waiting for a
message on some channel, and when it receives that message, the continuation
will have the same form.

####  10.1.1 Namespaces

When we add a copy of BoolAlg to RHOpi for both $N$ and $P,$ we can write down
formulae that talk about sets of names. The formula $\top$ denotes the set of
all names; the formula $``\top"$ denotes the set of names that are quoted
processes. These two sets differ when we have a nonempty set of generating
names.

An application of namespace logic is a formula for a “firewall”: any process
satisfying this formula receives no messages except on a name in $``\phi".$

$\mu X.\mathrm{recv}(``\phi",x\mapsto(X\lor
0)\;|\;\neg\mathrm{recv}(``\neg\phi",\top))\;|\;\neg\mathrm{recv}(``\neg\phi",\top)$

It is, perhaps, surprising that this can be accomplished with a compile-time
check, since we usually think of firewalls as a dynamic check. An application
of namespaces to statically proving security properties of code in an object
capabilities language can be found in [18].

##  11 Conclusion and future work

We have presented an algorithm for generating a logic from three data: a
2-Lawvere theory describing a notion of computation, a monad for describing a
notion of collection, and a distributive law. As mentioned in the
introduction, the picture emerging from this view of logic is that logically
useful collections of individuals look like nothing so much as the individuals
that represent the formulae that collect them. The range of applications of
this algorithm is quite broad. Any of the languages given semantics in the K
Framework, including C/C++, Java, Javascript, and many others can
automatically be equipped with logics that serve as a basis for of program
specification and automatically checked verification, and simultaneously as a
basis equipping these languages with new and powerful type systems. This
considerably lowers the barrier to embuing popular untyped languages with type
systems. Likewise, the algorithmic nature of the approach also serves as an
aid in future language design. For example, Synereo is designing a language
for the smart contracts on the blockchain based on the $\mathsf{RHO}$-calculus
[17]. Equipping this language with a type system amounts to nothing more than
deciding on the type of collection one wants to collect type inhabitants in.

## References

  * [1] Samson Abramsky, _Domain theory in logical form_ , Ann. Pure Appl. Logic 51 (1991), no. 1-2, 1–77.
  * [2] Samson Abramsky, _Proofs as processes_ , Theor. Comput. Sci. 135 (1992), no. 1, 5–9.
  * [3] Samson Abramsky, _No-cloning in categorical quantum mechanics_ , 2009.
  * [4] Luis Caires, _Logical semantics of types for concurrency_ , Algebra and Coalgebra in Computer Science, Lecture Notes in Computer Science (2007), 2007, pp. 16–35.
  * [5] H Curry, _Grundlagen der kombinatorischen logik_ , American Journal of Mathematics 52 (3) (1930), 509–536.
  * [6] M. J. Gabbay, _The $\pi$-calculus in FM_, Thirty-five years of Automath (Fairouz Kamareddine, ed.), Kluwer, 2003.
  * [7] G. Grätzer, _universal algebra_ , Van Nostrand, 1968.
  * [8] Martin Hyland and John Power, _The category theoretic understanding of universal algebra: Lawvere theories and monads_ , Electr. Notes Theor. Comput. Sci. 172 (2007), 437–458.
  * [9] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler, _Featherwieght java: A minimal core calculus for java and GJ_ , Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA ’99), Denver, Colorado, USA, November 1-5, 1999. (Brent Hailpern, Linda M. Northrop, and A. Michael Berman, eds.), ACM, 1999, pp. 132–146.
  * [10] Jean-Louis Krivine, _The curry-howard correspondence in set theory_ , Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, LICS 2000 (Martin Abadi, ed.), IEEE Computer Society Press, June 2000.
  * [11] Stephen Lack and Jirí Rosický, _Notions of lawvere theory_ , Applied Categorical Structures 19 (2011), no. 1, 363–391.
  * [12] J. Lambek, _From lambda calculus to cartesian closed categories_ , (1980), 376–402.
  * [13] William F. Lawvere, _Functorial Semantics of Algebraic Theories_ , Ph.D. thesis, 2004, pp. 1–121.
  * [14] James J. Leifer and Robin Milner, _Deriving bisimulation congruences for reactive systems_ , CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings (Catuscia Palamidessi, ed.), Lecture Notes in Computer Science, vol. 1877, Springer, 2000, pp. 243–258.
  * [15] L. Gregory Meredith and Matthias Radestock, _Namespace logic: A logic for a reflective higher-order calculus._ , in _TGC_ [16], pp. 353–369.
  * [16] , _A reflective higher-order calculus._ , Electr. Notes Theor. Comput. Sci. 141 (2005), no. 5, 49–67.
  * [17] L.G. Meredith, J. Pettersen, and G. Stepenson, _Contracts, composition, and scaling: rholang spec 0.1_ , 2016.
  * [18] Lucius Gregory Meredith, Mike Stay, and Sophia Drossopoulou, _Policy as types_ , CoRR abs/1307.7766 (2013).
  * [19] Robin Milner, _Functions as processes_ , Mathematical Structures in Computer Science 2 (1992), no. 2, 119–141.
  * [20] Gordon D. Plotkin, _The origins of structural operational semantics_ , Journal of Logic and Algebraic Programming, 2004, pp. 60–61.
  * [21] Grigore Rosu and Traian-Florin Serbanuta, _An overview of the K semantic framework_ , J. Log. Algebr. Program. 79 (2010), no. 6, 397–434.
  * [22] Moses Schönfinkel, _On the Building Blocks of Mathematical Logic_ , From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (Jean van Heijenoort, ed.), iuniverse.com, 1924, pp. 355–366.
  * [23] Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa, _Ott: Effective tool support for the working semanticist_ , J. Funct. Program. 20 (2010), no. 1, 71–122.
  * [24] Anthony M. Sloane, _Lightweight language processing in kiama_ , Generative and Transformational Techniques in Software Engineering III - International Summer School, GTTSE 2009, Braga, Portugal, July 6-11, 2009. Revised Papers (João M. Fernandes, Ralf Lämmel, Joost Visser, and João Saraiva, eds.), Lecture Notes in Computer Science, vol. 6491, Springer, 2009, pp. 408–425.
  * [25] Mike Stay and Lucius Gregory Meredith, _Higher category models of the pi-calculus_ , CoRR abs/1504.04311 (2015).
  * [26] T Trimble, _Multisorted lawvere theories_.