# Dynamic Reserve Price Design for Lazada Sponsored Search

Mang Li<EMAIL_ADDRESS>Lazada Monetization TechHang ZhouChina

(2022)

###### Abstract.

In e-commerce platform, users will be less likely to use organic search if
sponsored search shows them unexpected advertising items, which will be a
hidden cost for the platform. In order to incorporate the hidden cost into
auction mechanism which helps create positive growth for the platform, we turn
to a reserve price design to decide whether we sell the traffic, as well as
build healthy relationships between revenue and user experience. We propose a
dynamic reserve price design framework to sell traffic more efficiently with
minimal cost of user experience while keeping long-term incentives to the
advertisers to reveal their valuations truthfully. A distributed algorithm is
also proposed to compute the reserve price with billion-scale data in the
production environment. Experiments with offline evaluations and online A/B
testing demonstrate that it’s a simple and efficient method to be suitably
used in industrial production. It has already been fully deployed in the
production of Lazada sponsored search.

reserve price, incentive-compatibility, large-scale distributed algorithm,
sponsored search, advertising

††copyright: acmcopyright††journalyear: 2022††doi:
XXXXXXX.XXXXXXX††conference: 31st ACM International Conference on Information
and Knowledge Management; October 17-22, 2022; Atlanta, Georgia, USA††price:
15.00††isbn: 978-1-4503-XXXX-X/18/06††ccs: Information systems Computational
advertising

##  1\. Introduction

Advertising takes an important role in Internet companies like Google and
Meta, and it’s also the most efficient strategy of monetization in e-commerce
platforms such as Amazon, Taobao and Lazada. As we know, building the flywheel
to make an e-commerce platform continually grows is to build up a closed-loop
among monetization, user growth, and platform traffic & Gross Merchandise
Volume (GMV), which shows in figure 1. When money made by ads is invested into
user growth, the new or retained users’ contribution to GMV can make the
platform more valuable to sellers. However, people agree that search ads will
hurt user experience and GMV. The first reason for this is the different
targets monetization team and organic search team set, the former tries to
optimize cost per mille (CPM) while the latter focus on optimizing GMV per
mille (GPM). The second reason is that ad items are far less than what are in
organic search. But if we keep filling more, the marginal value of ads will
decrease, which will finally do harm to the platform. Therefore, building
relationship between user experience and revenue when we fill ads is necessary
and important. Furthermore, methods that fill ads dynamically are a better way
to boost revenue with little loss of user experience. Auction mechanisms, such
as reserve price design, can be used to achieve the purpose.

Figure 1. The flywheel to make e-commerce platform continually grow

Usually, conversion rate (CVR) or click-through rate (CTR) threshold is used
to decide whether we sell the traffic, but it will impose a negative impact on
advertisers especially when they are new or put new commodities on shelf
because of the uncertainty of estimation. Under the mechanism, no matter how
much advertisers raise their bid price, they will not get the traffic and
finally quit the campaign. Other methods like (Abrams and Schwarz, 2007) try
to design a mechanism that encourages advertisers to create an experience for
users that maximizes efficiency, but it doesn’t work well when ad supply is
not sufficient in some traffic because poor quality ads with low bids still
have the opportunity for impression. In this paper, we design a framework that
generates dynamic reserve price to build the relationship among revenue, user
experience, and monetization ratio111Monetization ratio defines how much
traffic we used to do advertising from the aspect of traffic while keeping the
incentive-compatible as well. To compute the reserved price on a large scale
of data, we propose distributed algorithm, which can also be used in different
problems with the same form.

From the perspective of reserve price design, to maximize the revenue earned
in a general second price auction (GSP), the platform can set reserve price
and not make any allocations when the bids are low (Krishna, 2009). Lots of
work have done to find the optimal reserve price to improve platform revenue
from the perspective of advertiser and keep the incentive ability to prevent
bid shading issues. A widely used method is based on advertiser’s history
behavior (Kanoria and Nazerzadeh, 2020). In order to estimate the value
distribution, the idea is to use advertiser’s history of the bids. However,
there are two drawbacks of this kind of method, one is that it uses
advertisers’ original bid to calculate the reserve price, which makes us more
careful about the incentive problems. Another one is, for an e-commerce
platform, what we sell to the advertisers is the user at different times,
which have very different values. It’s scarcely possible to estimate the
optimal reserve price in practice due to the data sparsity issue. In our
proposed method, we rethink the reserve price design from a traffic
perspective, and we can prove it’s the near-optimal choice to maximize
expected cost per mille (ECPM) under different kinds of platform constraints.
Moreover, it’s also very easy to prove the incentive compatibility property.

Our contributions can be summarized as follows: 1) We design dynamic reserve
price to build the relationship between user experience and revenue to make
the most of the traffic with incentive compatibility. 2) We proposed
distributed algorithm to handle the scalability issues, and it can also be
used in problems with the same form. 3) We conducted offline and online
experiments to evaluate the effectiveness of the method. In conclusion, it’s a
very useful method to decide whether we should reserve the traffic to deal
with the hidden cost of sponsored search.

##  2\. Preliminaries

A typical description for auction pipeline shows as figure 2, there’re $M$
advertisers in sponsored search scenario to compete for $N$ traffic. Due to
the intention expressed by the user through a search query, only $K\leq M$
suitable advertisers can participate in one traffic competition. And for each
traffic $i,\forall i\in[N]$, using a second price auction, we allocate the
traffic to the advertiser who has the highest $ecpm$. we can estimate the
$ecpm_{i}$ to define the potential revenue we can get, where $ecpm_{i}$ is
$bid_{i}ctr_{i}$ in cost per click (CPC) model and $bid_{i}$ is the winner
advertiser’s bid for traffic $i$, more specifically, the entire revenue can be
denoted as

(1) $\sum_{i=1}^{N}ecpm_{i}x_{i},x_{i}\in\\{1,0\\}$

where $x_{i}$ is the decision variable to decide whether we reserve the
traffic, $x_{i}=1$ denotes sell otherwise we reserve it. And if there’s no
other control strategy, the traffic will be filled by ads as much as possible.
However, more ads fill means greater potential for compromising the user
experience, because the marginal value of ads will decrease.

Figure 2. A simple description for e-commerce advertising, and reserve price
play a role in stage of filter and pricing in auction mechanism.

###  2.1. Problem Formulation

As we discuss above, we need to figure out the relation between revenue, user
experience, and monetization ratio, so global platform constraints have been
added as equation 3-5. We assume that all estimated value is accurate enough
to reflect the true probability, which means the CTR can represent the true
probability of click-through rate, and the others are similar. We only discuss
the reserve price mechanism design without considering the estimation
uncertainty. Consider the problem as an optimization problem with platform
metrics constraint, such that

(2) $\displaystyle max\sum_{i=1}^{N}ecpm_{i}x_{i}$ (3) $\displaystyle s.t.\
\sum_{i=1}^{N}(ctr_{i}-tctr)x_{i}\geq 0$ (4)
$\displaystyle\sum_{i=1}^{N}(gpm_{i}-tgpm)x_{i}\geq 0$ (5)
$\displaystyle\sum_{i=1}^{N}-x_{i}\geq-tpv$ (6) $\displaystyle
x_{i}\in\\{0,1\\},\forall i\in[N]$

where $tctr$, $tgpm$ means the lower bound of CTR and GPM respectively, which
denote user experience constraints, and $tpv$ is the upper bound of ads
impression that can also be used to control the user experience. The most
important part of the ads platform is the monetization ratio, which is $tpv/N$
and needs to be controlled very cautiously. It’s the basic 3 platform
constraints, at the same time, we can also add other constraints if it can be
written in a linear form.

###  2.2. Lagrangian Duality

The traffic is very large in sponsored search scenario generally. The scale of
the problems we aim to solve should give the solution with distributed cluster
rather than a single machine. In this part, we introduce the form of reserve
price design with derivation, at first. and then describe the distributed
solution.

We rewrite the problem above in a more general form

(7) $\displaystyle\mathop{max}\sum_{i=1}^{N}c_{i}x_{i}$ (8) $\displaystyle
s.t.\ \sum_{i=1}^{N}b_{ik}x_{i}\geq B_{k},\forall k\in[L]$ (9) $\displaystyle
x_{i}\in\\{0,1\\},\forall i\in[N]$

where $L$ denotes the constraint size, usually, the constraint is less than 10
in practice. Using the Lagrangian decomposition (Shapiro, 1979), We define

(10) $\displaystyle L(x_{i};\lambda_{k})$
$\displaystyle=\sum_{i=1}^{N}c_{i}x_{i}+\sum_{k=1}^{L}\lambda_{k}(\sum_{i=1}^{N}b_{ik}x_{i}-B_{k})$
(11)
$\displaystyle=\sum_{i=1}^{N}(c_{i}+\sum_{k=1}^{L}\lambda_{k}b_{ik})x_{i}-\sum_{k=1}^{L}\lambda_{k}B_{k}$

so we have the Lagrangian relax form and the Lagrange multipliers
$\lambda_{k}$. corresponding to the inequality constraints
$\sum_{i=1}^{N}b_{ik}x_{i}\geq B_{k},\forall k\in[L]$, $\lambda_{k}$ are
restricted to be non-negative,

(12) $\displaystyle\mathop{\max}\limits_{x_{i}}L(x_{i};\lambda_{k})$ (13)
$\displaystyle\ s.t.\ \lambda_{k}>0,\forall k\in[L]$ (14) $\displaystyle
x_{i}\in\\{0,1\\},\forall i\in[N]$

based on the KKT condition (Boyd et al., 2004), the optimal solution for the
above problem satisfy

(15) $\displaystyle\lambda_{k}(\sum_{i=1}^{N}b_{ik}x_{i}-B_{k})=0,\forall
k\in[L]$ (16) $\displaystyle\sum_{i=1}^{N}b_{ik}x_{i}-B_{k}\geq 0,\forall
k\in[L]$ (17) $\displaystyle\lambda_{k}>0,\forall k\in[L]$

So, to maximize $L(x_{i};\lambda_{k})$ with a fixed $\lambda_{k}$, we only
need to select the positive adjust-cost by the decision variable $x_{i}$,
which can be interpreted as

(18) $x_{i}=\left\\{\begin{array}[]{ll}1,\mbox{ }if\
c_{i}+\sum_{k=1}^{L}\lambda_{k}b_{ik}>0\\\ 0,\mbox{ }if\
c_{i}+\sum_{k=1}^{L}\lambda_{k}b_{ik}\leq 0\end{array}\right.$

therefore, bringing the problem defined in section 2.1 into equation 18, the
dynamic reserve price can be interpreted as follow

(19) $\begin{split}r_{i}=&[\lambda_{1}(tctr-ctr_{i})+\lambda_{2}(tgpm-
gpm_{i})+\lambda_{3}]/ctr_{i},\\\ &\forall i\in[N]\end{split}$

where $\lambda_{1}$,$\lambda_{2}$ and $\lambda_{3}$ is the Lagrangian
multiplier 222$\lambda$ can be interpreted as the shadow price or marginal
utility of the metrics we want to control. for constraint 3-5 respectively

###  2.3. Distributed Algorithm for Dynamic Reserve Price

####  2.3.1. Dual Descent Dynamic Reserve Price (D3RP)

First, we consider the dual descent algorithm (Macklin et al., 2020).
According to the decomposability of the Lagrangian dual problem, we can get
the solution of the traffic level decision variable parallelly. By using the
dual descent algorithm, which is an iterative procedure based on the
decomposability of the dual, we can get more optimal Lagrangian multipliers.
After we calculate $x_{i}$ using equation 18, the Lagrangian multipliers can
be updated as follow:

(20)
$\lambda_{k}^{(t)}=max(\lambda_{k}^{(t-1)}-\alpha(\sum_{i=1}^{N}b_{ik}x_{i}-B_{k}),0)$

where $\alpha$ is the learning rate for each iteration, and $t\in[0,T]$
denotes the iteration step, where $T$ is the maximum iterations. In algorithm
1, we introduce a distributed version of dual descent to calculate the dynamic
reserve price. Particularly, in each iteration. 1) first we use map op in
Spark to calculate $x_{i}$ independently for each traffic, and then we can get
the traffic gradient coefficient $b_{ik}x_{i}$ for each Lagrangian multiplier.
2) we use reduce op to sum all gradient coefficients and collect to the driver
to update $\lambda_{k}$ using dual descent as equation 20.

Algorithm 1 Dual Descent Dynamic Reserve Price (D3RP)

1: initialization: $\lambda_{k}^{0}=0,k\in[L]$

2: repeat

3: solve $x_{i}^{(t)},i\in[N]$ with multiplier $\lambda_{k}^{(t-1)}$ by eq 18
in parallel

4: for each $k\in[L]$ in parallel do

5: calculate $cons_{k}^{(t)}=\sum_{i=1}^{N}b_{ik}x_{i}^{(t-1)}$

6: update $\lambda_{k}^{(t)}$ with equation 20

7: end for

8: until ($\lambda_{k}^{(t)}$ is converged)

####  2.3.2. Coordinate Descent Dynamic Reserve Price (CD2RP)

we can see that the algorithm above is simple and efficient enough, however,
it requires setting the learning rate $\alpha$ manually, which would be many
and diverse. especially, if we try several settings of hyper-parameter in
computationally intensive scenarios with a large scale of data, it will waste
lots of calculation resources. So we propose a method using coordinate descent
algorithm (Wright, 2015) to calculate the reserve price, which updated one
multiplier $\lambda_{k}$ and keeps the other fixed. To avoid the setting of
the learning rate, our method prepares an ordered collection of $\lambda_{k}$
firstly and then selects the minimal $\lambda_{k}$, which can make the primal
problem feasible. We reorganized the subproblem, and write it in the form of a
coordinated update as follows

(21)
$\displaystyle\mathop{max}\sum_{i=1}^{N}(c_{i}+\lambda_{k^{\prime}}b_{ik^{\prime}}+\sum_{k=1,k\neq
k^{\prime}}^{L}{\lambda_{k}b_{ik}})x_{i},$ (22) $\displaystyle
x_{i}\in\\{0,1\\},\forall i\in[N],\forall k\in[L]$

let $f_{i}(\lambda_{k^{\prime}})=c_{i}+\sum_{k=1,k\neq
k^{\prime}}^{L}\lambda_{k}b_{ik}+\lambda_{k^{\prime}}b_{ik^{\prime}},\forall
i\in[N]$, according to equation 18, the decision variable is only related to
the sign of the coefficient function $f_{i}(\lambda_{k^{\prime}})$, the
interaction with the horizontal axis can make the decision variable change, so
the ordered set of $\lambda_{k}$ can be defined as

(23)
$\lambda_{k}\in\\{\lambda_{k^{\prime}}|f_{i}(\lambda_{k^{\prime}})=0,\forall
i\in[N]\\}.$

and we can see that $N$ is a number of billion-scale, the candidate set of
$\lambda_{k}$ is the same order of magnitude as $N$. So $\lambda_{k}$ search
algorithm with time complexity $O(n)$ is unacceptable. We can design dual
binary search (DBS) to find the temporary optimal $\lambda_{k}$ if the primal
problem is feasible.

More specifically, the procedure of the algorithm 2 shows below: 1) we
calculate sorted candidates of $\Lambda$ by equation 23 in parallel, 2) use
binary search to find the minimum threshold to guarantee the constraint not
less than $B_{k}$ and then update $\lambda_{k}$.

Algorithm 2 Coordinate Descent Dynamic Reserve Price (CD2RP)

1: initialization: $\lambda_{k}^{0}=0,k\in[L]$

2: repeat

3: for each $k\in[L]$ do

4: compute sorted candidate set $\Lambda_{k}^{(t)}$ by eq 23 in parallel

5: search optimal $\lambda_{k}^{(t)}$ and $x_{i}^{(t)},i\in[N]$ with candidate
set $\Lambda_{k}^{(t)}$ and algorithm 3

6: end for

7: until ($\lambda_{k}^{(t)}$ is converged)

Algorithm 3 Dual Binary Search (DBS)

1: input:
$\Lambda_{k}^{(t)}=\\{\lambda_{k_{0}}^{(t)},\lambda_{k_{1}}^{(t)},...,\lambda_{k_{K-1}}^{(t)}\\},B_{k}$,
where $K=|\Lambda_{k}^{(t)}|$ and $k\in[L]$

2: initialization: $l=0,u=K-1$

3: while $l<u$ do

4: $p=\lfloor(\ell+u)/2\rfloor$

5: solve $x_{i_{p}}^{(t)},i\in[N]$ with multiplier $\lambda_{k_{p}}^{(t)}$ by
eq 18 in parallel

6: calculate $cons_{k}^{(t)}=\sum_{i=1}^{N}b_{ik}x_{i_{p}}^{(t)}$ in parallel

7: if $cons_{k}^{(t)}<B_{k}$ then

8: $l=p+1$

9: else

10: $u=p$

11: end if

12: end while

13: return $\lambda_{k_{u}}^{(t)}$, $x_{k_{u}}^{(t)}$

###  2.4. Incentive Compatibility Discussion

Incentive compatibility is the most important feature for reserve price
design, as the bid of an advertiser may determine the price he pays in future
auctions, if we don’t design the reserve price with incentive compatibility,
it may lead the advertisers to shade their bids and finally result in a loss
in revenue for the platform. In this part, we prove the incentive
compatibility of our design of reserve price. Consider one advertiser $j$ in
an auction of traffic $i,\forall i\in[N]$ and assume that the other advertiser
will be truthful. We can see that for each advertiser $j$, the dynamic reserve
price and her prices to win the traffic do not depend on $j$’s own bids at
all. Hence, the bid of the advertiser $j$ does not affect his utility in
future rounds and myopically maximizing utility in each round is optimal for
maximizing the long-term utility. Since truthful bidding is myopically a
dominant strategy in each round, being truthful is the best choice, and all
advertiser following the always truthful strategy constitutes an equilibrium
status. Without loss of generality, let’s consider the simple case for single
ad slot. Advertiser $j$ uses $bid_{ij}$ to compete traffic $i,\forall i\in[N]$
with his valuation $v_{ij}$, and the dynamic reserve price for the advertiser
$j$ is $drp_{ij}$, which do not depend on $bid_{ij}$, and the pay per click
(PPC) is $ppc_{ij}=max_{k\neq j}bid_{ik}$ if there’s no reserve price.
Otherwise, we charge advertiser $max(max_{k\neq j}bid_{ik},drp_{ij})$, so the
traffic $i$’s utility for advertiser $j$ is $u_{ij}=bid_{ij}-max(max_{k\neq
j}bid_{ik},drp_{ij})$. Let’s consider the following situations in table 1, we
can see that telling the truth i.e. $bid_{ij}=v_{ij}$ is a weakly dominant
strategy, which can lead to a truthfully bidding, so this kind of dynamic
reserve price design is incentive compatibility.

Table 1. Advertiser incentive discussion with different kinds of competition context bidding strategy |  competition context |  utility |  optimal utility
---|---|---|---
$bid_{ij}>v_{ij}$ |  $bid_{ij}>drp_{ij}>v_{ij}>ppc_{ij}$ |  $<0$ |  $=0$
|  $bid_{ij}>drp_{ij}>ppc_{ij}>v_{ij}$ |  $<0$ |  $=0$
|  $bid_{ij}>v_{ij}>drp_{ij}>ppc_{ij}$ |  $>0$ |  $>0$
|  $bid_{ij}>v_{ij}>ppc_{ij}>drp_{ij}$ |  $>0$ |  $>0$
|  $bid_{ij}>ppc_{ij}>v_{ij}>drp_{ij}$ |  $<0$ |  $=0$
|  $bid_{ij}>ppc_{ij}>drp_{ij}>v_{ij}$ |  $<0$ |  $=0$
$bid_{ij}<v_{ij}$ |  $v_{ij}>drp_{ij}>bid_{ij}>ppc_{ij}$ |  $=0$ |  $>0$
|  $v_{ij}>drp_{ij}>ppc_{ij}>bid_{ij}$ |  $=0$ |  $>0$
|  $v_{ij}>bid_{ij}>drp_{ij}>ppc_{ij}$ |  $>0$ |  $>0$
|  $v_{ij}>bid_{ij}>ppc_{ij}>drp_{ij}$ |  $>0$ |  $>0$
|  $v_{ij}>ppc_{ij}>bid_{ij}>drp_{ij}$ |  $=0$ |  $>0$
|  $v_{ij}>ppc_{ij}>drp_{ij}>bid_{ij}$ |  $=0$ |  $>0$

###  2.5. Convergence and Optimality Discussion

In general, when the algorithm converges to a result, that jointly satisfies
the optimality condition of equation 15-17, and is the optimal solution to the
primal problem. However, the Lagrangean techniques can not guarantee to get an
optimal solution to the primal integer programming (IP) problem, because a
duality gap occurs due to the LP relaxation (Dantzig, 1957). However, the
solution computed from 12-14 is optimal for any IP problems derived from
15-17, when $B_{k}$ is replaced by $B_{k}-\delta_{k}$ (Shapiro, 1979), where
$\delta_{k}$ is non-negative variables, which satisfy for any $\lambda_{k}>0$
such that $\delta_{k}$ is $0$. But we can still analyze the gap between
optimal and our algorithm empirically, the result in table 2 shows that it can
achieve a nearly optimal solution. In particular, the optimality gap decreases
as the number of traffic increases. Generally, the data scale is quite large
in the e-commerce scenario, which means we can get the near-optimal solution
in general.

##  3\. Experimental Evaluations

we do the test on both artificial data and Lazada sponsored search scenario
data. For artificial setting, we generate $c_{i}$ and the coefficient of
global constraint $b_{ik}$ using two uniformly distribution in $[0,1]$
respectively, at the same time, without losing generality, we set the
constraint $B_{k}$ between $0$ and $N$, and make it has a feasible solution.
For a real scenario on a large dataset, $c_{i}$ is replaced by
$ecpm_{i}=ctr_{i}bid_{i}$, and we test three constraints as described in
section 2.1. The optimality is evaluated by duality gap (Champion, 2004),
which can quantify the discrepancy between the objective value computed by a
current feasible but suboptimal solution of the primal problem and the value
calculated by the dual problem.

###  3.1. Optimality Testing

First, we evaluate the optimality ratio, which is defined as the ratio of
objective value solving by SCIP 333SCIP is currently one of the fastest non-
commercial solvers for mixed integer programming (MIP) and mixed integer
nonlinear programming (MINLP) (Achterberg, 2009) to that using our distributed
algorithm. Because it’s difficult to find any solver that can solve billion-
scale IP problems, therefore, we only test the optimality under medium-scale
problems using artificial data generated as described above. The experiment
results show in figure 3, which demonstrate that the optimality ratio is above
0.995 with $N=2000$, and above 0.998 with $N=10000$ under all scenarios of
local constraints for all experiment cases. More details, we compare the two
algorithms described above across the different number of constraints, where
$1\leq K\leq 20$ and all coefficients generated by the uniform distribution.
We draw the average optimality ratio curve with 20 times test as we vary $K$,
the result shows in Figure 1. The optimality gap increases while $K$
increases, at the same time, decreases while $N$ increases. In practice in
industry, we usually have small $K$ but large $N$, so it proves empirically we
can get a near-optimal solution.

Figure 3. Optimality ratio between solutions computed by SCIP and algorithm by
LP relaxation

###  3.2. Duality Gap on Production Data

we test the algorithm with real search scenario data to measure the optimality
of the solution. As it’s difficult to find the solution to billion-scale
problems, therefore, one of the choices is to calculate the duality gap $D$
combined with primal objective value $O$, and if the relative duality gap
defined as $D/O$ is small enough, it means that we find the near-optimal
solution. So, we use it to describe the level of optimization. As described
above we test the two algorithms by real data with three constraints, table 2
shows the result of the relative duality gap after 15 iterations, which
indicates we have already achieved a near-optimal solution. We can see the
relative duality gap curve from figure 4, which shows that D3RP is sensitive
to the learning rate while having a slower converge speed than CD2RP.

Table 2. Comparison of relative duality gap after 15 iterations Iteration |  D3RP ($\alpha=1.5e^{-9}$) |  D3RP ($\alpha=2e^{-9}$) |  CD2RP
---|---|---|---
15 |  $6.3869e^{-4}$ |  $5.4895e^{-5}$ |  $1.5866e^{-9}$
Figure 4. Duality gap curve over iterations for D3RP and CD2RP

###  3.3. Solving Speed

The distributed implementation of our algorithm is using Spark, and in order
to study the scalability, we try different scales of traffic sampled in real
data with $N$ range from million-scale to billion-scale with fix $K=3$ (CTR,
GPM and PVR), and we set 512 number of executors, where each one with 1 core
and 2G memory. Experiment has been tested 3 times in the same setting to get
more reliable results. Figure 5 shows the solving time with different scales
of traffic. The optimization for 20 million-scale decision variables within
$K\in\\{1,3,5,7\\}$ global constraints can be able to converge to a near-
optimal solution within an hour, which shows in figure 6.

Figure 5. Time cost over different scales of traffic on 3 constraints and 512
executors using CD3RP Figure 6. Time cost over different number of constraint
on ten million scale decision variable using CD3RP

###  3.4. Production Deployment

We present the online performance of the proposed dynamic reserve price design
in Lazada sponsored search scenario, in which we consider not only efficiency,
such as CTR and GPM, but also the relevance score444Relevance score is a human
evaluation metric defining whether the ads are relevant to the query.. We
consider four metrics, i.e., Revenue, CTR, GPM, top query555Top query is the
query with top 50% search request. relevance and mid query666Mid query is the
query with mid 10% search request. relevance, and conduct online A/B testing
with these metrics. We define the relevance score to be better than 85% in top
query and 75% in mid query, at the same time, CTR and GPM gap of ad slot
compared with pure organic bucket should be less than 20% and 30%
respectively. Table 3 shows the relative improvements with 10% of production
traffic during a week, and the benchmark is the traffic not using any traffic
control strategy. From the experiments, dynamic reserve price can make it
possible to get high performance of CTR, GPM and relevance with a low cost of
revenue. At the same time, as the online platform contains millions of user
requests every day, the results can prove stable. The distributed algorithm we
developed in this paper has already been fully deployed in production.

Table 3. Online experiment for Lazada sponsored search in Thailand CTR |  GPM |  Top Query Relevance |  Mid Query Relevance |  Revenue
---|---|---|---|---
+24.71% |  +30.6% |  +59.71% |  +30.14% |  -1.77%

##  4\. Related Work

In this section, we briefly discuss the work related to reserve price design
for the application of online advertising. Most of the methods design the
reserve price from the advertiser perspective using their history purchase,
which differs from our work designing reserve price from the traffic
perspective.

the recent study on reserve price strategy is based on Myerson optimal auction
(Myerson, 1981) and tries to estimate the advertisers’ unknown valuations to
maximize platform revenue. In practice, Ostrovsky and Schwarz conducted an
experiment on reserve prices for online auctions (Ostrovsky and Schwarz,
2011), which showed that it can significantly increase the revenue of
sponsored search. And a common insight, which is widely used in practice, is
to estimate advertisers’ valuation distributions using history bids. However,
These methods can not bring long-term incentives to the advertisers. Because
it may lead them to shade their bids and ultimately hurt platform revenue
(Taylor, 2004; Villas-Boas, 2004; Fudenberg and Villas-Boas, 2006).

The rapid development of e-commerce technology in recent years (Turban et al.,
2015), it renewed interest in reserve price design based on advertiser
behavior, which is setting a personal reserve price for each advertiser based
on their previous bid price to boost revenue (Amin et al., 2013; Acquisti and
Varian, 2005; Mohri and Munoz, 2014; Chen and Wang, 2016; Kanoria and
Nazerzadeh, 2020). Unfortunately, some designs of personalized reserve price
still have incentive-compatibility issues, which have been discussed in
(Kanoria and Nazerzadeh, 2020).

Yash Kanoria al. (Kanoria and Nazerzadeh, 2020) show how behavior base reserve
price can be used to optimize reserve prices in an incentive-compatible way by
appropriately learning from the previous bids. they propose an incentive-
compatible mechanism that sets a personal reserve price for each advertiser
based on the previous bids of other advertisers. However, all of these methods
above potentially assume that all traffic value is similar to the advertiser,
which may not be suitable for an e-commerce scenario.

##  5\. Conclusion

We introduce the dynamic reserve price design framework for Lazada sponsored
search, it can be used to define the relationship between revenue and user
experience with incentive compatibility. We proposed distributed algorithms to
solve the billion-scale problem with limited constraints, which can also be
used to solve other similar problems in computational advertising. The
proposed algorithm can be implemented not only using Spark but also using
other distributed frameworks (Dean and Ghemawat, 2004) such as MPI and Flink.
The implementation in the production environment is simple to guarantee the
stability of the whole advertising system.

## References

  * Myerson (1981) Myerson, R.B.  Optimal auction design.  Mathematics of operations research 1981, 6, 58–73.
  * Ostrovsky and Schwarz (2011) Ostrovsky, M.; Schwarz, M.  Reserve prices in internet advertising auctions: A field experiment.  In Proceedings of the Proceedings of the 12th ACM conference on Electronic commerce, 2011, pp. 59–60.
  * Stokey (1979) Stokey, N.L.  Intertemporal price discrimination.  The Quarterly Journal of Economics 1979, pp. 355–371.
  * Salant (1989) Salant, S.W.  When is inducing self-selection suboptimal for a monopolist?  The Quarterly Journal of Economics 1989, 104, 391–397.
  * Hart and Tirole (1988) Hart, O.D.; Tirole, J.  Contract renegotiation and Coasian dynamics.  The Review of Economic Studies 1988, 55, 509–540.
  * Villas-Boas (2004) Villas-Boas, J.M.  Price cycles in markets with customer recognition.  RAND Journal of Economics 2004, pp. 486–501.
  * Taylor (2004) Taylor, C.R.  Consumer privacy and the market for customer information.  RAND Journal of Economics 2004, pp. 631–650.
  * Fudenberg and Villas-Boas (2006) Fudenberg, D.; Villas-Boas, J.M.  Behavior-based price discrimination and customer recognition.  Handbook on economics and information systems 2006, 1, 377–436.
  * Bikhchandani and McCardle (2012) Bikhchandani, S.; McCardle, K.  Behavior-based price discrimination by a patient seller.  The BE Journal of Theoretical Economics 2012, 12.
  * Amin et al. (2013) Amin, K.; Rostamizadeh, A.; Syed, U.  Learning prices for repeated auctions with strategic buyers.  Advances in Neural Information Processing Systems 2013, 26.
  * Acquisti and Varian (2005) Acquisti, A.; Varian, H.R.  Conditioning prices on purchase history.  Marketing Science 2005, 24, 367–381.
  * Mohri and Munoz (2014) Mohri, M.; Munoz, A.  Optimal regret minimization in posted-price auctions with strategic buyers.  Advances in Neural Information Processing Systems 2014, 27.
  * Chen and Wang (2016) Chen, X.; Wang, Z.  Bayesian Dynamic Learning and Pricing with Strategic Customers.  2016\.
  * Kanoria and Nazerzadeh (2020) Kanoria, Y.; Nazerzadeh, H.  Dynamic reserve prices for repeated auctions: Learning from bids.  arXiv preprint arXiv:2002.07331 2020.
  * Achterberg (2009) Achterberg, T.  SCIP: solving constraint integer programs.  Mathematical Programming Computation 2009, 1, 1–41.
  * Shapiro (1979) Shapiro, J.F.  A survey of Lagrangean techniques for discrete optimization. In Annals of Discrete Mathematics; Elsevier, 1979; Vol. 5, pp. 113–138.
  * Dean and Ghemawat (2004) Dean, J.; Ghemawat, S.  MapReduce: Simplified data processing on large clusters 2004.
  * Boyd et al. (2004) Boyd, S.; Boyd, S.P.; Vandenberghe, L.  Convex optimization; Cambridge university press, 2004.
  * Agarwal et al. (2012) Agarwal, D.; Chen, B.C.; Elango, P.; Wang, X.  Personalized click shaping through lagrangian duality for online recommendation.  In Proceedings of the Proceedings of the 35th international ACM SIGIR conference on Research and development in information retrieval, 2012, pp. 485–494.
  * Wright (2015) Wright, S.J.  Coordinate descent algorithms.  Mathematical Programming 2015, 151, 3–34.
  * Macklin et al. (2020) Macklin, M.; Erleben, K.; Müller, M.; Chentanez, N.; Jeschke, S.; Kim, T.Y.  Primal/dual descent methods for dynamics.  In Proceedings of the Computer Graphics Forum. Wiley Online Library, 2020, Vol. 39, pp. 89–100.
  * Krishna (2009) Krishna, V.  Auction theory; Academic press, 2009.
  * Lahaie and Pennock (2007) Lahaie, S.; Pennock, D.M.  Revenue analysis of a family of ranking rules for keyword auctions.  In Proceedings of the Proceedings of the 8th ACM Conference on Electronic Commerce, 2007, pp. 50–56.
  * Evans (2009) Evans, D.S.  The online advertising industry: Economics, evolution, and privacy.  Journal of economic perspectives 2009, 23, 37–60.
  * Goldfarb and Tucker (2011) Goldfarb, A.; Tucker, C.  Online display advertising: Targeting and obtrusiveness.  Marketing Science 2011, 30, 389–404.
  * Turban et al. (2015) Turban, E.; King, D.; Lee, J.K.; Liang, T.P.; Turban, D.C.  Marketing and advertising in e-commerce. In Electronic commerce; Springer, 2015; pp. 403–456.
  * Dantzig (1957) Dantzig, G.B.  Discrete-variable extremum problems.  Operations research 1957, 5, 266–288.
  * Abrams and Schwarz (2007) Abrams, Z.; Schwarz, M.  Ad auction design and user experience.  In Proceedings of the International Workshop on Web and Internet Economics. Springer, 2007, pp. 529–534.
  * Champion (2004) Champion, T.  Duality gap in convex programming.  Mathematical programming 2004, 99, 487–498.
  * Aggarwal et al. (2009) Aggarwal, G.; Muthukrishnan, S.; Pál, D.; Pál, M.  General auction mechanism for search advertising.  In Proceedings of the Proceedings of the 18th international conference on World wide web, 2009, pp. 241–250.


Equational Reasoning for Non-determinism Monad]
Equational Reasoning for Non-determinism Monad:

The Case of Spark Aggregation

Shin-Cheng Mu

Institute of Information Science
Academia Sinica

As part of the author's studies on equational reasoning for monadic programs, this report focus on non-determinism monad.
We discuss what properties this monad should satisfy, what additional operators and notations can be introduced to facilitate equational reasoning about non-determinism, and put them to the test by proving a number of properties in our example problem inspired by the author's previous work on proving properties of Spark aggregation.

§ INTRODUCTION

In functional programming, pure programs are those that can be understood as static mappings from inputs to outputs.
The main advantage of staying in the pure realm is that properties of pure entities can be proved by equational reasoning.
Side effects, in contrast, used to be considered the “awkward squad” that are difficult to be reasoned about.
<cit.>, however, showed that effectful, monadic programs may also be reasoned about in a mathematical manner, using monad laws and properties of effect operators.

This report is part of a series of the author's studies on equational reasoning for monadic programs.
In this report we focus on non-determinism monad — in our definition that is a monad having two effect operators, one allowing a program to fail, another allowing a non-deterministic choice between two results.
We discuss what properties these operators should satisfy, what additional operators and notations can be introduced to facilitate equational reasoning of this monad, and put them to the test by proving a number of properties in our example problem: Spark aggregation.

Much of this report is inspired by the author's joint work with <cit.>, in which we formalised Spark, a platform for distributed computation, and derived properties under which a distributed Spark aggregation represents a deterministic computation.
Therefore, many examples in this report are about finding out when processing a non-deterministic permutation (simulating arbitrary distribution of data) produces a deterministic result.

§ MONAD AND NON-DETERMINISM

A monad consists of a type constructor  and two operators  and “bind”  that satisfy the following monad laws:

\begin{align}
\ensuremath{\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{return}\;\Varid{x}} &= \ensuremath{\Varid{f}\;\Varid{x}}\mbox{~~,} \label{eq:monad-bind-ret}\\
\ensuremath{\Varid{return}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m}} &= \ensuremath{\Varid{m}} \mbox{~~,} \label{eq:monad-ret-bind}\\
\ensuremath{\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}(\Varid{g}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m})} &= \ensuremath{(\lambda \Varid{x}\to \Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{g}\;\Varid{x})\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m}} \mbox{~~.}
\label{eq:monad-assoc}
\end{align}

Rather than the usual , in the laws above we use the reversed bind , which is consistent with the direction of function composition and more readable when we program in a style that uses composition.
When we use bind with $\lambda$-abstractions, it is more natural to write .
In this report we use the former more than the latter, thus the choice of notation.

We also define . Note that  has type .

[8]::(b→M c)→(a→M b)→a→M c[E]

[B](f0.7<=<g) x=f0.7=<<g x[E]

[B](0.50.5⟨ 0.8$ 0.50.5⟩)[8]
[8]::(a→b)→M a→M b[E]

[B]f0.50.5⟨ 0.8$ 0.50.5⟩m=(return·f)0.7=<<m[E]

[8]::(b→c)→(a→M b)→(a→M c)[E]

[B]  [E]

Some monadic operators we find handy for this paper.

More operators we find useful are given in Figure <ref>. Right-to-left Kleisli composition, denoted by , composes two monadic operations  and  into an operation . Operators  and  are monadic counterparts of function application and composition:  applies a pure function to a monad, while  composes a pure function after a monadic function.

We now introduce a collections of properties that allows us to rotate an expression that involves two operators and three operands.
These properties will be handy when we need to move parenthesis around in expressions.
To begin with, the following properties show that  and  share properties similar to pure function application and composition:

\begin{align}
\ensuremath{(\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}\Varid{g})\;\Varid{x}} &= \ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\Varid{g}\;\Varid{x}} \mbox{~~,}
\label{eq:comp-ap}\\
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}(\Varid{g}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\Varid{m})} &= \ensuremath{(\Varid{f}\mathbin{\cdot}\Varid{g})\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\Varid{m}} \mbox{~~,}
\label{eq:comp-ap-ap}\\
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}(\Varid{g}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}\Varid{h})} &= \ensuremath{(\Varid{f}\mathbin{\cdot}\Varid{g})\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}\Varid{h}} \mbox{~~.}
\label{eq:comp-mcomp-mcomp}
\end{align}

We also have the following law that allows us to rotate an expression that uses  and :

\begin{align}
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}(\Varid{g}\mathbin{\cdot}\Varid{h})}   &= \ensuremath{(\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}\Varid{g})\mathbin{\cdot}\Varid{h}} \mbox{~~.}
\label{eq:mcomp-comp-mcomp}
\end{align}

Note that  in (<ref>) must be a function returning a monad. Furthermore, (<ref>) and (<ref>) relate  and , both operators applying functions to monads,
while (<ref>) and (<ref>) relate  and , both operators composing functions on monads:

\begin{align}
\ensuremath{\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}(\Varid{g}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\Varid{m})} &= \ensuremath{(\Varid{f}\mathbin{\cdot}\Varid{g})\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m}} \mbox{~~,}
\label{eq:comp-bind-ap}\\
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}(\Varid{g}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m})} &= \ensuremath{(\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}\Varid{g})\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m}} \mbox{~~,}
\label{eq:mcomp-bind-ap}\\
\ensuremath{\Varid{f}\mathrel{\hstretch{0.7}{<\!\!\!=\!\!<}}(\Varid{g}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}\Varid{h})} &= \ensuremath{(\Varid{f}\mathbin{\cdot}\Varid{g})\mathrel{\hstretch{0.7}{<\!\!\!=\!\!<}}\Varid{h}} \mbox{~~,}
\label{eq:kc-mcomp}\\
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}(\Varid{g}\mathrel{\hstretch{0.7}{<\!\!\!=\!\!<}}\Varid{h})} &= \ensuremath{(\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle \bullet \rangle}}}\Varid{g})\mathrel{\hstretch{0.7}{<\!\!\!=\!\!<}}\Varid{h}} \mbox{~~.}
\label{eq:mcomp-kc}
\end{align}

Having these properties is one of the advantages of writing  and  backwards.
All the properties above can be proved by expanding definitions, and it is a good warming-up exercise proving some of them.
Some of them are proved in Appendix <ref>.

None of these operators and properties are strictly necessary: they can all be reduced to , , and $\lambda$-abstractions. As is often the case when designing notations, having more operators allows ideas to be expressed concisely in a higher level of abstraction, at the expense of having more properties to memorise. It is personal preference where the balance should be. Properties (<ref>) through (<ref>) may look like a lot of properties to remember. In practice, we find it usually sufficient to let us be guided by types. For example, when we have  and want to bring  and  together, by their types we can figure out the resulting expression should be .

Non-determinism Monad

Non-determinism is the only effect we use in this report.
We assume two operators  and : the former denotes failure, while  denotes that the computation may yield either  or .
As pointed out by <cit.>, for proofs and derivations, what matters is not how a monad is implemented but what properties its operators satisfy.
What laws  and  should satisfy, however, can be a tricky issue.
As discussed by <cit.>, it eventually comes down to what we use the monad for.
It is usually expected that  be a monoid. That is,  is associative, with  as its zero:

\begin{align*}
\ensuremath{(\Varid{m}\mathbin{\talloblong}\Varid{n})\mathbin{\talloblong}\Varid{k}}~ &=~ \ensuremath{\Varid{m}\mathbin{\talloblong}(\Varid{n}\mathbin{\talloblong}\Varid{k})} \mbox{~~,}\\
\ensuremath{\emptyset\mathbin{\talloblong}\Varid{m}} ~=~ & \ensuremath{\Varid{m}} ~=~ \ensuremath{\Varid{m}\mathbin{\talloblong}\emptyset} \mbox{~~.}
\end{align*}

It is also assumed that monadic bind distributes into  from the end,
while  is a right zero for :

\begin{align}
\ensuremath{\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}(\Varid{m}_{1}\mathbin{\talloblong}\Varid{m}_{2})} ~&=~ \ensuremath{(\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m}_{1})\mathbin{\talloblong}(\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\Varid{m}_{2})} \mbox{~~,}
\label{eq:bind-mplus-dist}\\
\ensuremath{\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}}\emptyset} ~&=~ \ensuremath{\emptyset} \label{eq:bind-mzero-zero} \mbox{~~.}
\end{align}

For our purpose in this section, we also assume that  is commutative () and idempotent (). Implementation of such non-determinism monads have been studied by <cit.>.

Here are some induced laws about how  interacts with  and non-determinism operators:

\begin{align}
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\Varid{return}\;\Varid{x}} &= \ensuremath{\Varid{return}\;(\Varid{f}\;\Varid{x})} \mbox{~~,}\label{eq:ap-return}\\
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\emptyset} &= \ensuremath{\emptyset} \mbox{~~,} \label{eq:ap-mzero}\\
\ensuremath{\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}(\Varid{m}_{1}\mathbin{\talloblong}\Varid{m}_{2})} &= \ensuremath{(\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\Varid{m}_{1})\mathbin{\talloblong}(\Varid{f}\mathrel{\raisebox{0.5\depth}{\scaleobj{0.5}{\langle}} \scaleobj{0.8}{\$} \raisebox{0.5\depth}{\scaleobj{0.5}{\rangle}}}\Varid{m}_{2})}\mbox{~~.}
\label{eq:ap-mplus}
\end{align}

§ PERMUTATION AND INSERTION

As a warm-up example, the function  non-deterministically computes a permutation of its input, using an auxiliary function  that inserts an element to an arbitrary position in a list:
[22][1.5mu a1.5mu]→M [1.5mu a1.5mu][E]

[B]perm [1.5mu 1.5mu][18]
[22]return [1.5mu 1.5mu][E]

[B]perm (x:xs)[18]
[22]insert x0.7=<<perm xs  ,[E]

[22]a→[1.5mu a1.5mu]→M [1.5mu a1.5mu][E]

[B]insert x [1.5mu 1.5mu][18]
[22]return [1.5mu x1.5mu][E]

[B]insert x (y:xs)[18]
[22]return (x:y:xs)((y:)0.50.5⟨ 0.8$ 0.50.5⟩insert x xs)  .[E]
For example, possible results of  include
, , , , , and

The following lemma presents properties under which permuting the input list does not change the result of a :

Given . If  for all  and , we haveB@>l<@
[3]foldr (⊙) z0.50.5⟨∙⟩perm=return·foldr (⊙) z  .[E]

Since  is defined in terms of , proof of Lemma <ref> naturally depends on a lemma about a related property of :

Given , we haveB@>l<@
[3]foldr (⊙) z0.50.5⟨∙⟩insert x=return·foldr (⊙) z·(x:)  ,[E]
provided that
for all  and .

Prove . Induction on .

Case :
[4]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩insert x [1.5mu 1.5mu][E]

[4]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩return [1.5mu x1.5mu][E]

[4]return (foldr (⊙) z [1.5mu x1.5mu])[31]
[31]  .[E]

Case :
[4]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩insert x (y:xs)[E]

[4]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩(return (x:y:xs)((y:)0.50.5⟨ 0.8$ 0.50.5⟩insert x xs))[E]

[4]return (foldr (⊙) z (x:y:xs))((foldr (⊙) z·(y:))0.50.5⟨ 0.8$ 0.50.5⟩insert x xs)  .[E]
Focus on the second branch of :
[4](foldr (⊙) z·(y:))0.50.5⟨ 0.8$ 0.50.5⟩insert x xs[E]

[4]((y⊙)·foldr (⊙) z)0.50.5⟨ 0.8$ 0.50.5⟩insert x xs[E]

[4](y⊙)0.50.5⟨ 0.8$ 0.50.5⟩(foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩insert x xs)[E]

[4](y⊙)0.50.5⟨ 0.8$ 0.50.5⟩return (foldr (⊙) z (x:xs))[E]

[4]return (y⊙foldr (⊙) z (x:xs))[E]

[4]return (y⊙(x⊙foldr (⊙) z xs))[E]

[4]return (foldr (⊙) z (x:y:xs))  .[E]
Thus we have
[4](foldr (⊙) z0.50.5⟨∙⟩insert x) (y:xs)[E]

[4]return (foldr (⊙) z (x:y:xs))return (foldr (⊙) z (x:y:xs))[E]

[4]return (foldr (⊙) z (x:y:xs))  .[E]

Proof of Lemma <ref> then follows:

Prove that .
Induction on .

Case :
[3]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩perm [1.5mu 1.5mu][E]

[3]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩return [1.5mu 1.5mu][E]

[3]return (foldr (⊙) z [1.5mu 1.5mu])  .[E]

Case :
[4]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩perm (x:xs)[E]

[4]foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩(insert x0.7=<<perm xs)[E]

[4](foldr (⊙) z0.50.5⟨∙⟩insert x)0.7=<<perm xs[E]

[4](return·foldr (⊙) z·(x:))0.7=<<perm xs[E]

[4]((x⊙)·foldr (⊙) z)0.50.5⟨ 0.8$ 0.50.5⟩perm xs[E]

[4](x⊙)0.50.5⟨ 0.8$ 0.50.5⟩(foldr (⊙) z0.50.5⟨ 0.8$ 0.50.5⟩perm xs)[E]

[4](x⊙)0.50.5⟨ 0.8$ 0.50.5⟩(return (foldr (⊙) z xs))[E]

[4]return (x⊙foldr (⊙) z xs)[E]

[4]return (foldr (⊙) z (x:xs))  .[E]

Map, Filter, and Permutation
It is not hard for one to formulate the following relationship between
and , which is also based on a related property relating  and :
[Lemma <ref> and <ref> are in fact free theorems

of  and  <cit.>. They serve as good exercises, nevertheless.]

The lemma is true because  is a pure computation — in reasoning about monadic programs it is helpful, and sometimes essential, to identify its pure segments, because these are the parts more properties are applicable. Note that the composition  on the lefthand side is turned into  once we move  leftwards.

We prove only Lemma <ref>.

Prove by induction on  that  for all . We present only the inductive case
[4]map f0.50.5⟨ 0.8$ 0.50.5⟩insert x (y:xs)[E]

[4]map f0.50.5⟨ 0.8$ 0.50.5⟩(return (x:y:xs)((y:)0.50.5⟨ 0.8$ 0.50.5⟩insert x xs))[E]

[4]return (map f (x:y:xs))(map f0.50.5⟨ 0.8$ 0.50.5⟩((y:)0.50.5⟨ 0.8$ 0.50.5⟩insert x xs))  .[E]
For the second branch we reason:
[4]map f0.50.5⟨ 0.8$ 0.50.5⟩((y:)0.50.5⟨ 0.8$ 0.50.5⟩insert x xs)[E]

[4](map f·(y:))0.50.5⟨ 0.8$ 0.50.5⟩insert x xs[E]

[4]((f y:)·map f)0.50.5⟨ 0.8$ 0.50.5⟩insert x xs[E]

[4](f y:)0.50.5⟨ 0.8$ 0.50.5⟩(map f0.50.5⟨ 0.8$ 0.50.5⟩insert x xs)[E]

[4](f y:)0.50.5⟨ 0.8$ 0.50.5⟩insert (f x) (map f xs)  .[E]
Thus we have
[4]map f0.50.5⟨ 0.8$ 0.50.5⟩insert x (y:xs)[E]

[4]return (f x:f y:map f xs)((f y:)0.50.5⟨ 0.8$ 0.50.5⟩(insert (f x) (map f xs)))[E]

[4]insert (f x) (map f (y:xs))  .[E]

One may have noticed that the style of proof is familiar: replace  by  and  by , the proof is more-or-less what one would do for a list version of . This is exactly the point: the style of proofs we use to do for pure programs still works for monadic programs, as long as the monad satisfies the demanded laws, be it a list, a more advanced implementation of non-determinism, or a monad having other effects.

A similar property relating  and  can be formulated.

Its proof is routine and omitted. Finally, in a number of occasions it helps to know that  is a result of . The proof is also routine and omitted.

For all  we have that  for some .

§ SPARK AGGREGATION

Spark <cit.> is a popular platform for scalable distributed data-parallel computation based on a flexible programming environment with high-level APIs, considered by many as the successor of MapReduce.
In a typical Spark program, data is partitioned and stored distributively on read-only Resilient Distributed Datasets (RDDs) —
we can think of it as a list of lists, where each sub-list is potentially stored on a remote node.
On an RDD one can apply operations, called combinators, such as , , and .
The  combinator, for example, takes user-defined functions  and :  accumulates a sub-result for each data partition while  merges sub-results across different partitions.

Programming in Spark, however, can be tricky.
Since sub-results are computed across partitions concurrently, the order of their applications varies on different executions.
Aggregation in Spark is therefore inherently non-deterministic.
An example from <cit.> showed that computing the integral of $x^{73}$ from $x=-2$ to $x=2$, which should be $0$, using a function in the Spark machine learning library, yields results ranging from $-8192.0$ to $12288.0$ in different runs.
It is thus desirable to find out conditions, which Spark's documentation does not specify formally, under which a Spark computation yields deterministic outcomes.

§.§ List Homomorphism

Since a Spark aggregation is typically used to computes a list homomorphism <cit.>,
we digress a little in this section to give a brief review and present some results that we will use.
A function  is called a list homomorphism if there exists , , and  such that:
[B]h [1.5mu 1.5mu][15]

[B]h [1.5mu x1.5mu][15]
[15]=k x[E]

[B]h (xs++ys)[15]
[15]=h xs⊕h ys  .[E]
That  is such a list homomorphism is denoted by .
Note that the properties above implicitly demand that  be associative with  as its identity element.

Lemma <ref> and <ref> below are about when a computation defined in terms of  is actually a list homomorphism. In Lemma <ref>,  denotes the image of a function .

if and only if , where .

Let  be associative on  with  as its identity, where .
We have  if and only if
for all
and .

Notice, in Lemma <ref>, that .
Proofs of both lemmas are interesting exercises, albeit being a bit off-topic.
They are recorded in Appendix <ref>.

§.§ Formalisation and Results

Distributed collections of data are represented by Resilient Distributed Datasets (RDDs) in Spark. Informally, an RDD is a collection of data entries; these data entries are further divided into partitions stored on different machines. Abstractly, an  can be seen as a list of lists:
[B]𝐭𝐲𝐩𝐞 Partition a[19]
[19]=[1.5mu a1.5mu]  ,[E]

[B]𝐭𝐲𝐩𝐞 RDD a[19]
[19]=[1.5mu Partition a1.5mu]  ,[E]
where each  may be stored in a different machine.

While Spark provides a collection of combinators (functions on s that are designed to be composed to form larger programs), in this report we focus on a particular one, . It can be seen as a parallel implementation . The combinator processes an  in two levels: each partition is first processed locally on one machine by . The sub-results are then communicated and combined —
this second step can be think of as another  with .
[In fact, the actual Spark aggregation (and that modelled in <cit.>) are like .
For convenience in our proofs we see all list operations the other way round and use . This is not a fundamental difference.]

Spark programmers like to assume that their programs are deterministic. To exploit concurrency, however, the sub-results from each machine might be processed in arbitrary order and the result could be non-deterministic.
The following is our characterisation of , where we use  to model the fact that sub-results from each machine are processed in unknown order:
[B]aggregate::b→(a→b→b)→(b→b→b)→RDD a→M b[E]

[B]aggregate z (⊗) (⊕)=foldr (⊕) z0.50.5⟨∙⟩(perm·map (foldr (⊗) z))  .[E]
It is clear from the types that  and  are pure computations, and non-determinism is introduced solely by .

Deterministic Aggregation
We are interested in finding out conditions under which  produces deterministic outcomes.

Given  and , where  is associative and commutative, we have:B@>l<@
[3]aggregate z (⊗) (⊕)=return·foldr (⊕) z·map (foldr (⊗) z)  .[E]

We reason:
[4]aggregate z (⊗) (⊕)[E]

[4]foldr (⊕) z0.50.5⟨∙⟩(perm·map (foldr (⊗) z))[E]

[4](foldr (⊕) z0.50.5⟨∙⟩perm)·map (foldr (⊗) z)[E]

[4]return·foldr (⊕) z·map (foldr (⊗) z)  .[E]

The following corollary summaries the results and present conditions under which  computes a homomorphism.

, provided that
is associative, commutative, and has  as identity, and that  for all
and .

We reason:
[4]aggregate z (⊗) (⊕)[E]

[4]return·foldr (⊕) z·map (foldr (⊗) z)[E]

[4]return·hom (⊕) (⊗z) z·concat  .[E]

Determinism Implies Homomorphism
The final part of the report deals with an opposite question:
what can we infer if we know that  is deterministic?
To answer that, however, we need to assume two more properties:

\begin{align}
\ensuremath{\Varid{m}_{1}\mathbin{\talloblong}\Varid{m}_{2}\mathrel{=}\Varid{return}\;\Varid{x}} ~~&\Rightarrow~~ \ensuremath{\Varid{m}_{1}\mathrel{=}\Varid{m}_{2}\mathrel{=}\Varid{return}\;\Varid{x}} \mbox{.}
\label{eq:mplus-return}\\
\ensuremath{\Varid{return}\;\Varid{x}_{1}\mathrel{=}\Varid{return}\;\Varid{x}_{2}} ~~&\Rightarrow~~ \ensuremath{\Varid{x}_{1}\mathrel{=}\Varid{x}_{2}} \mbox{.}
\label{eq:return-injective}
\end{align}

Property (<ref>) can be seen as the other direction of idempotency of ,
while (<ref>) states that  is injective.

The following lemma can be understood this way: when , which could be non-deterministic, can be performed by a deterministic function, the operator  should be insensitive to ordering:

If ,
and  for some , we have
[3]foldr (⊗) z (concat xss)=[E]

[5]foldr (⊕) z (map (foldr (⊗) z) xss)=[E]

[7]foldr (⊕) z (map (foldr (⊗) z) yss)  .[E]

We reason:
[4]return·foldr (⊗) z·concat$xss[E]

[4]aggregate z (⊗) (⊕)$xss[E]

[4](foldr (⊕) z·map (foldr (⊗) z))0.50.5⟨ 0.8$ 0.50.5⟩perm xss[E]

[4](return·foldr (⊕) z·map (foldr (⊗) z)$yss)[E]

[7]((foldr (⊕) z·map (foldr (⊗) z))0.50.5⟨ 0.8$ 0.50.5⟩m)  .[E]
Thus by (<ref>) and (<ref>),
The former also equals
by Lemma <ref>,
for some .

Based on Lemma <ref>, the following theorem explicitly states that  should be associative, commutative, and has  as its identity in restricted domain.

If ,
we have that , when restricted to values in , is associative, commutative, and has  as its identity.

In the discussion below, let ,, and  be in . That is, there exists , , and  such that ,
, and .

Identity. We reason:

[7]foldr (⊗) z (concat [1.5mu xs1.5mu])[E]

[7]foldr (⊕) z (map (foldr (⊗) z) [1.5mu xs1.5mu])[E]

[7]y⊕z  .[E]
Thus  is a right identity of . Similarly,

[7]foldr (⊗) z (concat [1.5mu [1.5mu 1.5mu],xs1.5mu])[E]

[4]foldr (⊕) z (map (foldr (⊗) z) [1.5mu [1.5mu 1.5mu],xs1.5mu])[E]

[7]z⊕y  .[E]
Thus  is also a left identity of .

Commutativity. We reason:

[7]foldr (⊕) z (map (foldr (⊗) z) [1.5mu xs,ys1.5mu])[E]

[7]foldr (⊕) z (map (foldr (⊗) z) [1.5mu ys,xs1.5mu])[E]

[7]y⊕x  .[E]

Associativity. We reason:

[7]foldr (⊕) z (map (foldr (⊗) z) [1.5mu xs,ys,ws1.5mu])[E]

[7]foldr (⊕) z (map (foldr (⊗) z) [1.5mu ws,xs,ys1.5mu])[E]

[7](x⊕y)⊕w  .[E]

If ,
we have .

Apparently  and
We are left with proving the case for concatenation.
[7]foldr (⊗) z (xs++ys)[E]

[7]foldr (⊗) z (concat [1.5mu xs,ys1.5mu])[E]

[7]foldr (⊕) z (map (foldr (⊗) z) [1.5mu xs,ys1.5mu])[E]

[7]foldr (⊗) z xs⊕(foldr (⊗) z ys⊕z)[E]

[7]foldr (⊗) z xs⊕foldr (⊗) z ys  .[E]

Given  and .
if and only
if  forms a commutative monoid, and
that .

A conclusion following from Theorem <ref>,
Theorem <ref>, and Theorem <ref>.

§.§.§ Acknowledgements

In around late 2016,
Yu-Fang Chen, Chih-Duo Hong, Ondřej Lengál,
Nishant Sinha and Bow-Yaw Wang invited me into their project
formalising Spark. It was what inspired my interests in reasoning about monads, which led to a number of subsequent work.
The initial proofs of properties of  and other combinators were done by Ondřej Lengál, without using monads.
<cit.> modelled a hierarchy of monadic effects in Coq. The formalisation was applied to verify a number of equational proofs of monadic programs, including some of the proofs in an earlier version of this report. I am solely responsible for any remaining errors, however.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Affeldt, Nowak, and SaikawaAffeldt
et al2019]
authorpersonReynald Affeldt, personDavid
Nowak, and personTakafumi Saikawa.
A hierarchy of monadic effects for program
verification using equational reasoning. In
booktitleMathematics of Program Construction,
editorpersonGraham Hutton (Ed.).

authorpersonRichard S. Bird.
An introduction to the theory of lists.
In booktitleLogic of Programming and Calculi of
Discrete Design, editorpersonManfred Broy (Ed.).
Number 36 in seriesNATO ASI Series F.
publisherSpringer-Verlag, pages3–42.

[Chen, Hong, Lengál, Mu, Sinha, and
WangChen et al2017]
authorpersonYu-Fang Chen, personChih-Duo
Hong, personOndřej Lengál,
personShin-Cheng Mu, personNishant Sinha, and
personBow-Yaw Wang. year2017.
An executable sequential specification for Spark
aggregation. In booktitleInternational Conference on
Networked Systems. publisherSpringer-Verlag.

[Fischer, Kiselyov, and ShanFischer
et al2011]
authorpersonSebastian Fischer, personOleg
Kiselyov, and personChung-chieh Shan.
Purely functional lazy nondeterministic
journalJournal of Functional Programming
volume21, number4-5 (dateSeptember
year2011), pages413–465.

[Gibbons and HinzeGibbons and Hinze2011]
authorpersonJeremy Gibbons and personRalf
Hinze. year2011.
Just do it: simple monadic equational reasoning.
In booktitleInternational Conference on Functional
Programming, editorpersonOlivier Danvy (Ed.).
publisherACM Press, pages2–14.

authorpersonOleg Kiselyov.
titleLaws of MonadPlus.

authorpersonJanis Voigtländer.
Free theorems involving type constructor classes.
In booktitleInternational Conference on Functional
Programming, editorpersonAndrew Tolmach (Ed.).
publisherACM Press, pages173–184.

[Zaharia, Chowdhury, Das, Dave, Ma, McCauley,
Franklin, Shenker, and StoicaZaharia et al2012]
authorpersonMatei Zaharia, personMosharaf
Chowdhury, personTathagata Das, personAnkur Dave,
personJustin Ma, personMurphy McCauley,
personMichael J. Franklin, personScott Shenker, and
personIon Stoica. year2012.
Resilient distributed datasets: a fault-tolerant
abstraction for in-memory cluster computing. In
booktitleNetworked Systems Design and Implementation,
editorpersonSteven Gribble and
personDina Katabi (Eds.). publisherUSENIX.

§ MISCELLANEOUS PROOFS

Proving (<ref>) .
We reason:
[7]f0.7=<<(g0.50.5⟨ 0.8$ 0.50.5⟩m)[E]

[7](λx→f0.7=<<return (g x))0.7=<<m[E]

[7](λx→f (g x))0.7=<<m[E]

[7](f·g)0.7=<<m  .[E]

Proving (<ref>) .
We reason:
[4]f0.50.5⟨ 0.8$ 0.50.5⟩(g0.50.5⟨ 0.8$ 0.50.5⟩m)[E]

[4](return·f)0.7=<<(g0.50.5⟨ 0.8$ 0.50.5⟩m)[E]

[4](f·g)0.50.5⟨ 0.8$ 0.50.5⟩m  .[E]

For the next results we prove a lemma:

\begin{align}
\ensuremath{(\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}})\mathbin{\cdot}(\Varid{g}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}})} &= \ensuremath{(((\Varid{f}\mathbin{\hstretch{0.7}{=\!\!<\!\!<}})\mathbin{\cdot}\Varid{g})\mathbin{\hstretch{0.7}{=\!\!<\!\!<}})} \mbox{~~.} \label{eq:bind-comp-bind}
\end{align}

[4](λm→(λy→f0.7=<<g y)0.7=<<m)[E]

[4](((f0.7=<<)·g)0.7=<<)  .[E]

Proving (<ref>) .
We reason:

[6](f·g)0.50.5⟨∙⟩m  .[E]

Proving (<ref>) .
We reason:

[4](f·g)0.7<=<h  .[E]

Proving (<ref>) .
We reason:

[4](f0.50.5⟨∙⟩g)0.7<=<h  .[E]

Proof of Lemma <ref>

A Ping-pong proof.

Direction $(\Rightarrow)$. Let , prove  by induction on .

Case :
[7]foldr (⊕) z (map h [1.5mu 1.5mu])[E]

[7]foldr (⊕) z [1.5mu 1.5mu][E]

[7]h (concat [1.5mu 1.5mu])  .[E]

Case :
[7]foldr (⊕) z (map h (xs:xss))[E]

[7]h xs⊕foldr (⊕) z (map h xss)[E]

[7]h xs⊕h (concat xss)[E]

[7]h (concat (xs:xss))  .[E]

Direction $(\Leftarrow)$. Assuming , prove that .

Case empty list:
[7]h [1.5mu 1.5mu][E]

[7]h (concat [1.5mu 1.5mu])[E]

[7]foldr (⊕) z (map h [1.5mu 1.5mu])[E]

[7]z  .[E]

Case singleton list: certainly .

Case concatentation:
[7]h (xs++ys)[E]

[7]h (concat [1.5mu xs,ys1.5mu])[E]

[7]foldr (⊕) z (map h [1.5mu xs,ys1.5mu])[E]

[7]h xs⊕(h ys⊕z)[E]

[7]h xs⊕h ys  .[E]

Proof of Lemma <ref>

A Ping-pong proof.

Direction $(\Leftarrow)$. We show that , provided that .

It is immediate that  around
For , note that

\begin{align*}
\ensuremath{\Varid{foldr}\;(\otimes)\;\Varid{z}\;(\Varid{xs}\mathbin{+\!\!\!\!\!+}\Varid{ys})} &= \ensuremath{\Varid{foldr}\;(\otimes)\;(\Varid{foldr}\;(\otimes)\;\Varid{z}\;\Varid{ys})\;\Varid{xs}} \mbox{~~.}
\label{eq:fold-cat}
\end{align*}

The aim is thus to prove that
[3]foldr (⊗) (foldr (⊗) z ys) xs=(foldr (⊗) z xs)⊕(foldr (⊗) z ys)  .[E]
We perform an induction on . The case when  trivially
holds. For , we reason:
[7]foldr (⊗) (foldr (⊗) z ys) (x:xs)[E]

[7]x⊗foldr (⊗) (foldr (⊗) z ys) xs[E]

[7]x⊗((foldr (⊗) z xs)⊕(foldr (⊗) z ys))[E]

[7](x⊗(foldr (⊗) z xs))⊕(foldr (⊗) z ys)[E]

[7](foldr (⊗) z (x:xs))⊕(foldr (⊗) z ys)  .[E]

Direction $(\Rightarrow)$. Given
prove that  for  and  in the range of .

Let  and  for some
and . We reason:

[7]x⊗(foldr (⊗) z xs⊕foldr (⊗) z ys)[E]

[7]x⊗(foldr (⊗) z (xs++ys))[E]

[7]foldr (⊗) z (x:xs++ys)[E]

[7]foldr (⊗) z (x:xs)⊕foldr (⊗) z ys[E]

[7](x⊗foldr (⊗) z xs)⊕foldr (⊗) z ys[E]

[7](x⊗y)⊕w  .[E]