# Optimization tools for Twin-in-the-Loop vehicle control design:
analysis and yaw-rate tracking case study

Federico Dettù<EMAIL_ADDRESS>Simone Formentin
<EMAIL_ADDRESS>Stefano Varisco<EMAIL_ADDRESS>Sergio
Matteo Savaresi<EMAIL_ADDRESS>Dipartimento di Elettronica,
Informazione e Bioingegneria, Politecnico di Milano.
Via G. Ponzio 34/5, 20133, Milano, Italy.  Vehicle Dynamics, Ferrari S.p.A.
Via Abetone Inferiore 4, 41053, Maranello, Italy.

###### Abstract

Given the urgent need of simplifying the end-of-line tuning of complex vehicle
dynamics controllers, the Twin-in-the-Loop Control (TiL-C) approach was
recently proposed in the automotive field. In TiL-C, a digital twin is run on-
board to compute a nominal control action in run-time and an additional block
$C_{\delta}$ is used to compensate for the mismatch between the simulator and
the real vehicle. As the digital twin is assumed to be the best replica
available of the real plant, the key issue in TiL-C becomes the tuning of the
compensator, which must be performed relying on data only. In this paper, we
investigate the use of different black-box optimization techniques for the
calibration of $C_{\delta}$. More specifically, we compare the originally
proposed Bayesian Optimization (BO) approach with the recently developed Set
Membership Global Optimization (SMGO) and Virtual Reference Feedback Tuning
(VRFT), a one-shot direct data-driven design method. The analysis will be
carried out within a professional multibody simulation environment on a novel
TiL-C application case study – the yaw-rate tracking problem – so as to
further prove the TiL-C effictiveness on a challenging problem. Simulations
will show that the VRFT approach is capable of providing a well tuned
controller after a single iteration, while $10$ to $15$ iterations are
necessary for refining it with global optimizers. Also, SMGO is shown to
significantly reduce the computational effort required by BO.

##  1 Introduction

Figure 1: Twin-in-the-Loop vehicle control scheme.

Although control theorists have been pushing forward for decades in developing
well performing and sophisticate control algorithms, a sort of detachment
arose when looking at what control practicioners do. A few years ago, the
survey (Samad, 2017) showed that Proportional Integral Derivative control is
perceived as the most impacting technology in industry, far above _e.g._
nonlinear or adaptive controls, and somewhat more relevant than extremely
popular Model Predictive Control. In the same survey, it emerges that the lack
of competences in industry is an important perceived issue when dealing with
modern controllers. In fact, calibrating and updating a developed controller
requires adjustment of several tuning knobs, whose effect is often poorly
understood without a deep knowledge of control theory.

Concentrating our efforts toward this direction, we recently proposed an
approach for simplifying the implementation of complex controllers and easing
the end-of-line tuning phase in the vehicle domain: the Twin-in-the-Loop
Control (TiL-C) framework111The dual problem of Twin-in-the-Loop Filtering
(TiL-F) is also under investigation (Riva et al., 2022b; Delcaro et al.,
2023). (Dettù et al., 2023b), schematically represented in Fig. 1222A
discussion on robust calibration for TiL controllers has been proposed in
Dettù et al. (2023a).. TiL-C runs a digital twin (DT) –a highly sophisticated
model– inside a vehicle control unit in real-time. This is made possible by
the most recent technological advances (see _e.g._ the Autohawk platform VI-
Grade (2022)). Further, in the automotive domain, DT often come for free, as
car manufacturer already have a portfolio of well calibrated models of their
production vehicles, used for off-line testing and virtual prototyping.
The TiL-C architecture is based upon a nominal controller $C$; such a
controller is calibrated on the DT and then used on-board at run-time. This
allows for the computation of a nominal control action to be applied as a
first - open-loop - contribution to the real vehicle. It was then shown that a
simple compensator $C_{\delta}$ (_e.g._ a PID) could be sufficient to
guarantee stability and maintain the same performance attained on the DT also
on the real vehicle. By using TiL-C, the end-of-line tuning shifts from the
implementation (and sometimes redesign) of a complex controller, to the tuning
of a few gains, which is more easily done and widely understood.

An important issue in TiL-C – deeply discussed in (Dettù et al., 2023b) – is
how to use data to calibrate such parameters of the compensator $C_{\delta}$:
since this controller manages the unknown dynamics between the DT and the
vehicle, no classical model-based design techniques (_e.g._ loop shaping) can
be used. Following a recently established literature trend (Dettù et al.,
2023; Busetto et al., 2023; Coutinho et al., 2023), we first proposed Bayesian
Optimization (BO) to solve this problem. Although effectiveness of BO in
calibrating TiL-C has been shown ($100$ iterations have been considered), no
discussions concerning the selection of a specific optimization algorithm have
been considered. Also, no analyses concerning the number of iterations
necessary to get to convergence has been carried out. Being vehicle testing
very costly, assessing (and possibly reducing) the number of the necessary
experiments is extremely important. We thus concentrate our efforts to
investigate and analyse different approaches for calibrating a TiL controller.

Related works. Within the context of black-box optimization (of which BO is a
particular case), many approaches have been developed throughout the years and
successfully applied to different fields. Two classic iterative methods are
_e.g._ Extremum Seeking (ES) (Hellström et al., 2013) or Iterative Feedback
Tuning (IFT) (Hjalmarsson et al., 1998). Although being simple to apply, these
approaches lost popularity, suffering from different issues, such as the high
number of iterations required to get a solution, or the impossibility of
including safety a-priori unknown constraints during the tuning process,
potentially yielding hazardous controller attempts. Furthermore, these methods
are not global, and they might become stuck in a local minimum, requiring re-
initialization and thus increased costs.

Among global optimizers, surrogate function based ones (such as BO) gained
much popularity with respect to _e.g._ genetic algorithms (Jaen-Cuellar et
al., 2013) or particle swarm (Kim et al., 2008) ones, due to the large –often
unfeasible in real applications– number of iterations required by the latter.
As already mentioned, BO (Shahriari et al., 2015) proved to be very effective
when solving black-box optimization problems: calibrating a controller for a
partially or totally unknown plant lies within this framework. BO fits a
Gaussian Process (GP) surrogate of the unknown cost function to be minimized,
and iteratively selects new candidate points to be evaluated based on the
acquired GP knowledge. A nice BO feature is the possibility of including
a-priori unknown constraints within the optimization problems: similarly as
done for the cost function, these constraint functions are iteratively
estimated from data. This opens up the possibility of _e.g._ maintaining the
system in a safe region throughout the calibration procedure.

The most significant issue with BO is the high computational burden yield by
the GP fitting and optimization: the more data points are added, the more
cumbersome this procedure becomes, undermining application of BO in low-cost
processing units. To solve this, Sabug Jr et al. (2022) recently presented Set
Membership Global Optimization-$\Delta$ (SMGO-$\Delta$); with respect to BO,
this approach provides a computationally efficient objective and constraints
model, based on hypercones, and focusing on quantifying the uncertainty
associated to the unknown function, rather than directly trying to fit it.
SMGO-$\Delta$ also allows accounting for black-box constraints, and the
authors proven its convergence under the assumption of Lipschitz continuity of
the objective and constraints. SMGO-$\Delta$ has recently been used in
practical control tuning problems (Galbiati et al., 2022; Busetto et al.,
2023; Sabug Jr et al., 2023).

A completely different philosophy when dealing with controller tuning is the
Virtual Reference Feedback Tuning (VRFT) one: VRFT is direct data-driven
approach, thus requiring a single experiment for learning the controller. It
is based upon frequency-domain considerations, and tries to match a reference
closed-loop behaviour. VRFT has been successfully used in different control
tuning problems, _e.g._ electric motors (Busetto et al., 2023), engines
(Passenbrunner et al., 2014) or brake-by-wire systems (Radrizzani et al.,
2020); however, some critical tuning knobs (like the reference model) exist
when applying VRFT, and the resulting controller might be underperforming or
even unstable if they are not properly selected.
Finally, although well promising, TiL-C has been so far exclusively applied to
braking control (Dettù et al., 2023a, b): in the strive of widening the
portfolio of applications and further proofing its efficacy, different case
studies should be considered.

Contributions. Taking into account considerations above, we consider here
SMGO-$\Delta$ for TiL calibration, comparing it with BO, and discussing the
convergence speed of both algorithms. We include a constraint during the
optimization process, in order to guarantee that unsafe regions are avoided.
Also, we apply VRFT to the same problem, eventually showing the significant
performance obtained with just one experiment. Combination of both methods
(VRFT and BO/SMGO) is also explored. On top of this, we apply TiL-C to the
vehicle yaw-rate tracking problem: such a problem is important both in
production vehicles driving assistance systems – it is at the basics of
Electronic Stability Control (ESC) Gimondi et al. (2021) – and in autonomous
driving, where it is combined with trajectory following (Corno et al., 2023;
Falcone et al., 2007). Being an established state-of-the-art (Lucchini et al.,
2020, 2021; Spielberg et al., 2022; Beal and Gerdes, 2012; Falcone et al.,
2007), we use Model Predictive Control as a baseline controller in yaw-rate
tracking. Yaw-rate control poses critical stability problems, in that the
vehicle sideslip might utterly increase if not properly addressed, leading to
unsafe situations and undesired drifting of the vehicle (_i.e._ too large
wheel slips): it is thus an interesting and challenging test bench for TiL-C.

The remainder of the paper is as follows. In Section 2, we describe the yaw-
rate control problem, the simplified model of the vehicle and derive the
baseline controller, to be used within TiL-C. Then, in Section 3, we show how
TiL-C can be applied to the presented problem, and discuss the different
optimization tools. Section 4 compares the optimizers in terms of cost
function minimization and constraints violation, and then gives an in-depth
time-domain analysis of the obtained results, on different maneuvers.

##  2 The yaw-rate tracking problem

The yaw-rate tracking problem is tackled in this research with Twin-in-the-
Loop control. This application problem is used to evaluate and analyse
different optimization tools for TiL-C. Hence, we start off by precisely
defining a control-oriented system model and a baseline controller. The goal
is that of following a reference yaw-rate $r_{ref}$ – generated by the driver
steering action $s_{ref}$ by means of a suitable reference generation
mechanism. The controller decides a steering action $s_{cmd}$ to be passed to
a steer-by-wire system, acting onto the front wheels. Measurements used for
feedback control are: the yaw-rate $r$, the vehicle sideslip angle $\beta$
(usually retrieved by means of an estimation algorithm (Carnier et al., 2023),
not in the scopes of this work), the steering actuator position $s_{act}$, the
longitudinal component of vehicle speed $v_{x}$ and the longitudinal
acceleration $a_{x}$.

###  2.1 System modelling

In the following, we describe the model used for developing lateral dynamic
controllers. The model takes into account simplified vehicle dynamics and the
steer-by-wire actuator.

##### Vehicle model

Figure 2: Single-track vehicle model. Figure 3: Steer-by-wire actuator model,
featuring transfer function, rate limiter and saturation.

The model considered in this research for the development of benchmark lateral
dynamics controllers is a non-linear single-track one (schematically
represented in Fig. 2). Assuming that the right-left tires at front and rear
axle can be lumped together, the model reads (Beal and Gerdes, 2012)

$\begin{split}\dot{\beta}=&\dfrac{F^{f}_{y}+F^{r}_{y}}{Mv_{x}}-r\\\
\dot{r}=&\dfrac{L_{f}F^{f}_{y}-L_{r}F^{r}_{y}}{J_{zz}}\end{split},$ (1)

$J_{zz}$ and $M$ are the vehicle yaw moment of inertia and mass; $L_{f}$ and
$L_{r}$ are the distance from the vehicle center-of-mass and the front/rear
wheels, respectively. The lumped lateral forces at front and rear wheels
$F^{f}_{y}$, $F^{r}_{y}$ can be modeled in different ways; a popular one is
the Pacejka magic formula, proposed here in a simplified version (Lucchini et
al., 2020)

$F_{y}^{j}=-\dfrac{F_{z}^{j}\mathcal{C}_{j}}{\mathcal{A}_{j}\mathcal{B}_{j}}\sin\left(\mathcal{B}_{j}\textrm{atan}\left(\mathcal{A}_{j}\tan\left(\alpha_{j}\right)\right)\right),$
(2)

whereas $j=f,r$, and $\mathcal{A}_{j},\ \mathcal{B}_{j},\ \mathcal{C}_{j}$ are
suitable parameters (to be identified from data). $F^{j}_{z}$ is the wheel
vertical load, $\alpha_{j}$ is the wheel lateral sideslip angle. Under the
assumption of small vehicle sideslip and steer ($s_{act}$) angles, the lateral
slip at front and rear tires can be written as

$\alpha_{f}=\beta+\dfrac{L_{f}}{v_{x}}r-s_{act},\
\alpha_{r}=\beta-\dfrac{L_{r}}{v_{x}}r.$ (3)

On the other hand, vertical forces can be computed by taking into account
static contributions (due to vehicle mass), aerodynamic contributions (speed-
dependent) and load transfer (acceleration-dependent) (Lucchini et al., 2021),
such that

$\begin{split}F_{z}^{f}=&\dfrac{L_{r}}{L_{f}+L_{r}}Mg+k^{f}_{a}v_{x}^{2}-k_{x}a_{x}\\\
F_{z}^{r}=&\dfrac{L_{f}}{L_{f}+L_{r}}Mg+k^{r}_{a}v_{x}^{2}+k_{x}a_{x}\end{split}$
(4)

where $g$ is the gravity acceleration, $k_{a}^{f},\ k_{a}^{r}$ are aerodynamic
coefficients, and $k_{x}$ is the load transfer coefficient.

##### Steer-by-wire actuator

With regards to the steer-by-wire actuator, we consider here a model
comprising a linear part (transfer function) and a non-linear one (rate
limiter and saturation), see Fig. 3. The transfer function model from
commanded to actuated steer takes into account the low-level control, and it
has been provided by partner company Ferrari S.p.A.

$G_{act}\left(s\right)=\dfrac{58.34s^{2}+1547s+9137}{1.002s^{3}+64.55s^{2}+1549s+9137}.$
(5)

The closed-loop low-level control system modelled by $G_{act}\left(s\right)$
has a bandwidth $\omega_{act}\approx 33.8\ rad/s$. Being
$G_{act}\left(s\right)$ complex for the control-oriented modelling purposes
herein, we consider a simplified first-order transfer function

$G_{act,s}\left(s\right)=\dfrac{\omega_{act}}{s+\omega_{act}}$ (6)

The rate-limiter block implements a saturation on the time derivative of the
actuated steer angle - it models a current limit in the low-level circuits,
specifically. Then, the saturation block implements a limit on the actuated
steer angle. Mathematically, this reads

$\begin{split}\dot{s}_{rl}&=\begin{cases}-\dot{s}_{max}&\text{$\dot{s}_{tf}<-\dot{s}_{max}$}\\\
\dot{s}_{tf}&\text{$-\dot{s}_{max}\leq\dot{s}_{tf}<\dot{s}_{max}$}\\\
\dot{s}_{max}&\text{$\dot{s}_{tf}\geq\dot{s}_{max}$}\end{cases},\\\
s_{act}&=\begin{cases}-s_{max}&\text{$s_{rl}<-s_{max}$}\\\
s_{act}&\text{-$s_{max}\leq{s}_{rl}<s_{max}$}\\\
s_{max}&\text{$s_{rl}>s_{max}$}\end{cases}.\\\ \end{split}$ (7)

##### Complete model and linearization

The model in Eqs. (1)-(6) contains a non-linearity in the lateral forces
$F_{y}^{f}$, $F_{y}^{r}$. We can linearize their expression for given front
and rear sideslip angles $\bar{\alpha}_{f},\ \bar{\alpha}_{r}$

$\displaystyle F_{y}^{j}\approx$
$\displaystyle\bar{F}_{y}^{j}-\bar{C}^{j}_{\alpha}\left(\alpha_{j}-\bar{\alpha}_{j}\right),$
(8a) $\displaystyle\bar{F}^{j}_{y}\left(\bar{\alpha}_{j},F_{z}^{j}\right)=$
$\displaystyle-\dfrac{F_{z}^{j}\mathcal{C}_{j}}{\mathcal{A}_{j}\mathcal{B}_{j}}\sin\left(\mathcal{B}_{j}\arctan\left(\mathcal{A}_{j}\bar{\alpha}_{j}\right)\right),$
(8b)
$\displaystyle\bar{C}^{j}_{\alpha}\left(\bar{\alpha}_{j},F_{z}^{j}\right)=$
$\displaystyle\dfrac{F_{z}^{j}\mathcal{C}_{j}}{1+\mathcal{A}^{2}_{j}\bar{\alpha}_{j}}\cos\left(\mathcal{B}_{j}\arctan\left(\mathcal{A}_{j}\bar{\alpha}_{j}\right)\right).$
(8c)

Rewriting Eqs. (1)-(6), and considering Eq. (8), we have the following
discrete-time model

$\begin{split}x_{k+1}=&Ax_{k}+Bu_{k}+Ed_{k},\\\ y_{k}=&Cx_{k}.\end{split}$ (9)

Whereas the discretization has been carried out via forward Euler approach,
with sampling time $T_{s}=0.01s$, and the subscript $k$ denotes the time step.
The model state $x_{k}$, output $y_{k}$, disturbance $d_{k}$ and input $u_{k}$
are

$\begin{split}x_{k}=&\begin{bmatrix}\beta_{k}\\\ r_{k}\\\
s_{act,k}\end{bmatrix},\ y_{k}=r_{k},\ u_{k}=s_{cmd,k},\\\
d_{k}=&\begin{bmatrix}\dfrac{\bar{F}_{y}^{f}+\bar{C}^{f}_{\alpha}\bar{\alpha}_{f}+\bar{F}_{y}^{r}+\bar{C}^{r}_{\alpha}\bar{\alpha}_{r}}{Mv_{x}}\\\
\dfrac{L_{f}\left(\bar{F}_{y}^{f}+\bar{C}^{f}_{\alpha}\bar{\alpha}_{f}\right)-L_{r}\left(\bar{F}_{y}^{r}+\bar{C}^{r}_{\alpha}\bar{\alpha}_{r}\right)}{J_{z}}\end{bmatrix}^{t}.\end{split}$

(10)

Whereas $\left(\cdot\right)^{t}$ denotes the matrix transpose operator. And
the model matrices are given in Eq. (11).

$\boxed{A=T_{s}\begin{bmatrix}T_{s}^{-1}-\dfrac{\bar{C}^{f}_{\alpha}+\bar{C}^{r}_{\alpha}}{Mv_{x}}&\dfrac{-L_{f}\bar{C}^{f}_{\alpha}+L_{r}\bar{C}^{r}_{\alpha}-Mv^{2}_{x}}{Mv^{2}_{x}}&\dfrac{\bar{C}^{f}_{\alpha}}{Mv_{x}}\\\
\dfrac{-L_{f}\bar{C}^{f}_{\alpha}+L_{r}\bar{C}^{r}_{\alpha}}{J_{zz}}&T_{s}^{-1}-\dfrac{L_{f}^{2}\bar{C}^{f}_{\alpha}+L_{r}^{2}\bar{C}^{r}_{\alpha}}{J_{zz}v_{x}}&\dfrac{\bar{C}^{f}_{\alpha}L_{f}}{J_{zz}}\\\
0&0&T_{s}^{-1}-\omega_{act}\end{bmatrix},\ B=\begin{bmatrix}0\\\ 0\\\
T_{s}\omega_{act}\end{bmatrix},\ E=\begin{bmatrix}T_{s}&0\\\ 0&T_{s}\\\
0&0\end{bmatrix},C=\begin{bmatrix}0\\\ 1\\\ 0\end{bmatrix}^{t}.}$ (11)

######  Remark.

_Note that the model in Eq. ( 9) is linear time varying, due to the presence
of vehicle speed $v_{x}$, normal wheel forces $F^{f}_{z},\ F_{z}^{r}$ and the
linearization of $F^{f}_{y},\ F^{r}_{y}$ around the current sideslip angles.
It is common practice to disregard the vehicle speed as a state when dealing
with control-oriented modelling for lateral dynamics (Beal and Gerdes, 2012),
as the same introduces unnecessary complexity; we consider it as a slow-
varying parameter. Similar considerations can be applied to the vertical
forces (Riva et al., 2022b). Concerning the lateral forces, two possibilities
emerge: a first and simpler one consists in linearizing their expression for
zero sideslip angles, i.e. $\bar{\alpha}_{f}=\bar{\alpha}_{r}=0$ (used e.g. in
(Corno et al., 2023)), the second one consists in linearizing their expression
at each time step around the current sideslip angle values (used e.g. in (Beal
and Gerdes, 2012; Lucchini et al., 2020; Spielberg et al., 2022))._

###  2.2 Reference generator

Figure 4: Static component of $r_{ref}$ against driver steer request
$s_{ref}$. For each showed speed value, the solid line represents the digital
twin behaviour, whereas the dashed one is the static model.

The reference generation approach considered herein transforms a driver steer
request into a desired yaw-rate to be imposed onto the vehicle. This can be
realized via a static adaptive gain and a transfer function. The static gain
defines the desired steady-state vehicle behavior. Considering the available
high-fidelity model as a starting point, the reference curves are fitted so as
to mimic the nominal vehicle behaviour, saturating the yaw-rate at the maximum
obtainable value, see Fig. 4. Although the static gain guarantees that the
driver request generates a feasible and meaningful yaw-rate reference, the
same does not guarantee dynamic feasibility of said reference. Hence, we
consider a filter with unitary gain and two poles

$F_{ref,dyn}(s)=\dfrac{\left(2\pi f_{ref}\right)^{2}}{\left(s+2\pi
f_{ref}\right)^{2}}.$ (12)

The two poles are set to $f_{ref}=6.3\ Hz$ so as to assign a desired
”bandwidth” to the controller, as done in (Gimondi et al., 2021) for a similar
problem.

###  2.3 Model Predictive Control

Figure 5: High-level control system architecture, depicting the software
elements, namely the reference generator and the controller, the employed
measurements and the control variable. Figure 6: Force-slip diagram with
indicated peak force point and two examples of linearized force values before
and after the peak.

MPC can be employed to optimally solve a constrained control problem. The main
ingredients of MPC are an internal model –to be used for predicting the future
system behavior at each time step– a set of constraints on state and input
variables, and a cost function to be minimized.

##### Internal model

Considering Remark Remark, we apply here the local linearization approach at
each time step, for the lateral forces model. Hence, we use as an internal
model within the MPC the one described in Eqs. (9) and (11), which is
iteratively initialized according to the following procedure

  1. 1.

At time step $k$, measure/estimate $v_{x,k},\ a_{x,k},\ s_{act,k},\
\beta_{k}$;

  2. 2.

Use Eq. (3) to estimate $\alpha_{f,k},\ \alpha_{r,k}$. Use Eq. (4) to estimate
$F_{z,k}^{f},\ F_{z,k}^{r}$;

  3. 3.

Linearize lateral forces via Eq. (8) to get $\bar{F}^{f}_{y,k},\
\bar{F}^{r}_{y,k},\ \bar{C}^{f}_{\alpha,k},\ \bar{C}^{r}_{\alpha,k}$;

  4. 4.

Substitute Eq. (11) to get matrix $A_{k}$.

The model obtained at each time step is thus Linear Time Invariant (LTI), and
the MPC requires forward integration of this model to get predictions on the
system behavior. For the system to stay LTI, it is necessary that external or
potentially time-varying inputs are constant. This means assuming that, for
all $k$

$\begin{split}F^{f}_{z,k+i}=&F^{f}_{z,k},\ i=1,\ldots,N_{p},\\\
F^{r}_{z,k+i}=&F^{r}_{z,k},\ i=1,\ldots,N_{p},\\\ v_{x,k+i}=&v_{x,k},\
i=1,\ldots,N_{p}.\end{split}$ (13)

The assumptions above are indeed common in the literature (Lucchini et al.,
2020; Beal and Gerdes, 2012). A special note is necessary here for what
concerns the lateral force model. Consider the force-slip relation for the
considered front tires, in Fig. 6: it is evident that the maximum attainable
force is achieved for $\alpha=\alpha_{max}$, much smaller than $s_{max}$.
Going above the force peak, the slope of the curve is inverted – _i.e._
$\bar{C}_{\alpha}$ changes sign – and the predictive controller would try to
increase $\alpha$ to reduce the lateral force, given its limited knowledge of
the force model; one can verify that this yields instability. While accounting
for the complete force model is non-viable for the introduced nonlinearities,
enforcing a constraint on $\alpha$ allows for smooth operation of the tire
within its physical limits. Although a human driver might want to stay beyond
the curve for fun-to-drive reasons – _e.g._ for increased slipping of the
vehicle – no advantages in terms of steering performance exist. Let us remark
that this consideration was not carried out in previous literature (Lucchini
et al., 2020, 2021), but is non-viable when dealing with driving at the limits
of handling. Since we are considering active front steering, only the front
sideslip angle $\alpha_{f}$ is constrained.

Indeed, constraining $\alpha$ requires good knowledge of the slip value for
which force generation is maximized: imperfect knowledge might yield to worse
control performance, and an ad-hoc learning approach to estimate this
parameter in real-time should be used (_e.g._ a neural-network, as in
(Spielberg et al., 2022)). For the present research, $\alpha_{max}$ is assumed
to be known with adequate accuracy.

##### Constraints

The system in Eq. (9) is characterized by physical limitations on the actuator
(Eq. (7)). Said limitations are to be included as hard constraints within the
optimization problem.

$\begin{split}&-s_{max}\leq s_{act,k}\leq s_{max},\ \forall
k=1,\ldots,N_{p}\\\ &-\dot{s}_{max}T_{s}\leq
s_{act,k}-s_{act,k-1}\leq\dot{s}_{max}T_{s},\ \forall
k=1,\ldots,N_{p}.\end{split}$

(14)

On the other hand, as discussed above, the front sideslip angle $\alpha_{f}$
should be limited to prevent the system from going above the tire limitations.
This not being a physical limit of the system (which is always able to enter
the above-peak force region), we implement it as a soft constraint, via slack
variable $\rho$

$\begin{split}&-\alpha_{f,max}-\rho\leq\alpha_{f,k}\leq\alpha_{f,max}+\rho,\
\forall k=1,\ldots,N_{p}\end{split}$ (15)

As discussed above, the constraint based on maximum $\alpha_{f,k}$ is much
more restrictive than the actuator capabilities (constraints in Eq. (14)).
Hence, first constraint in Eq. (15) can be discarded, as it is never
activated.

##### Cost function

$\boxed{\begin{split}\mathcal{U}*=&\mathop{\mathrm{argmin}}\limits_{\epsilon,{x}_{1},\ldots,{x}_{N_{p}},u_{0},\ldots,u_{N_{p}}}\sum_{k=0}^{N_{p}-1}{{x}^{t}_{k+1}}W_{x}{{x}_{k+1}}+w_{u}u_{k}^{2}+w_{\rho}\rho^{2},\\\
\textrm{subject to}&\\\
x_{0}=&\begin{bmatrix}\beta_{0}&r_{0}&s_{0}\end{bmatrix}^{t},\\\
{x}_{k+1}=&A{x}_{k}+Bu_{k}+Ed_{k},\ \forall k=0,\ldots,N_{p}-1\\\
-\dot{s}_{max}T_{s}\leq&\delta s_{k}\leq\dot{s}_{max}T_{s},\ \forall
k=1,\ldots,N_{p}\\\
-\alpha_{f,max}-\epsilon\leq&\alpha_{f,k}\leq\alpha_{f,max}+\epsilon,\ \forall
k=1,\ldots,N_{p}.\end{split}}$

(16)

The minimized cost is given in Eq. (16), together with the constraints. More
specifically, the state vector is weighted ($W_{x}$), while a penalty on the
control effort ($w_{u}$) avoids numerical instabilities, and the slack
variable is minimized ($w_{\rho}$) to ensure that $\rho=0$ when inside the
constraint limits. Given that the prediction model is locally Linear Time-
Invariant, the Single Shooting Approach can be applied to write the states,
the constraints and the cost metric as a function of the control inputs
(_e.g._ as in (Riva et al., 2022a)). The obtained optimization problem is a
Quadratic Programming one, fastly solved via benchmark tools – qpOASES is used
in this research (Ferreau et al., 2014).

##  3 Twin-in-the-Loop Control

Figure 7: TiL control scheme for yaw-rate tracking.

The TiL scheme of Figure 7 is considered in this Section. The architecture
features the MPC controller of Section 2.3, a DT and a compensator
$C_{\delta}$.

As stated in (Dettù et al., 2023b), under the hypothesis that the simulator is
a faithful replica of the real system, $C_{\delta}$ controls a small signal
dynamic, as the open-loop steering action from the DT $\tilde{s}_{cmd}$ does
most of the job. Hence, we consider a simple PID compensator. Leveraging
findings in (Gimondi et al., 2021), we employ here a mixed yaw-rate sideslip
control, whereas the regulator $C_{\delta}$ controls a mixed signal, rather
than the yaw-rate per-se

$\epsilon=(1-\zeta)r-\zeta\beta,\ \zeta\in\left[0,1\right]$ (17)

Introducing a correction onto the yaw-rate via $\beta$ yields better results
in case of very high cornering stiffness values, and allows to account for
$\beta$ within the Single Input Single Output controller. The control law, in
continuous time ($s$ denotes the Laplace domain variable), reads

$C_{\delta}\left(s,\theta\right)=k_{p}\left(1+\dfrac{1}{sT_{I}}+\dfrac{sT_{D}}{1+sT_{D}/N_{D}}\right).$
(18)

$\theta=\left\\{k_{p},T_{I},T_{D}\right\\}$ is the vector of tuning knobs, and
the high-frequency pole is set ten times faster ($N_{D}=10$) than $T_{D}$, as
in common practice. The controller is discretized via the Tustin approach,
with sampling time $T_{s}=0.01s$.

Following the peak force limit considerations in Section 2.3, we enforce a
saturation on the actuated steer angle

$s^{lb}_{max,d}-\tilde{s}_{cmd}\leq s_{\delta}\leq
s^{ub}_{max,d}-\tilde{s}_{cmd}.$ (19)

Whereas $s^{lb}_{max,d},s^{ub}_{max,d}$ are obtained by substituting in Eq.
(3) the maximum sideslip angle $\alpha_{f,max}$, used in the MPC constraints.

###  3.1 $C_{\delta}$ tuning

To calibrate $C_{\delta}$, we proposed an optimization problem, solved via
Bayesian Optimization (BO) in (Dettù et al., 2023b): this is necessary given
that the block controls the unknown residual dynamic between the vehicle and
its replica. However, performing experiments with black-box proposed
parameters might lead to instability or unsafe configurations; we introduce
here a constraint on $\beta$, to be satisfied during the optimization process.
This guarantees that while exploring the search space, the algorithm stays
away from high sideslip values — note that using the sideslip as an indicator
of vehicle maneuverability and safety is common in the literature (Gimondi et
al., 2021; Beal and Gerdes, 2012).

$\begin{split}\theta^{*}=&\operatorname*{arg\,min}_{\theta}f_{bo}\left(\theta\right)\\\
\textrm{s.t.}\ \ \ &\theta\subseteq\Theta\in\mathbb{R}^{N_{\theta}}\\\
&g_{c}\left(\theta\right)\geq 0\end{split}$ (20)

Where
$g_{c}\left(\theta\right)=-\left|\beta\left(\theta\right)\right|+\beta_{max}$
is the constraint. The cost function $f_{bo}$ reads

$f_{bo}(\theta)=\dfrac{1}{N_{exp}}\sum_{k=1}^{N_{exp}}\left(\tilde{\epsilon}_{k}-\epsilon_{k}\left(\theta\right)\right)^{2}+\gamma_{u}\left(\dot{{s}}_{cmd,k}\right)^{2}$
(21)

Where the first term on the right hand side weights the controller tracking
performance, and the second one weights the control action derivative,
similarly to what done in Eq. (16) for the MPC. $N_{exp}$ is the number of
samples in the considered experiment. As for the cost function, also the
constraint on $\beta$ is a black-box, and needs to be adequately treated.
Constrained BO (Khosravi et al., 2022) can been used to solve the problem. CBO
estimates the black-box constraint via a Gaussian Process, and the
availability of a set of data. Analogously to cost function regression, the
optimizer iteratively adjusts its knowledge of the constraint. In practice, at
each $n$-th iteration, the black-box optimizer evaluates
$\theta^{\left(n\right)}$, and the tuple
$\left(\theta^{\left(n\right)},f_{bo}^{\left(n\right)},g^{\left(n\right)}_{c}\right)$
is collected and used to increment the dataset
$\mathcal{X}^{n}=\mathcal{X}^{n-1}\cup\left(\theta^{\left(n\right)},f_{bo}^{\left(n\right)},g^{\left(n\right)}_{c}\right)$.
The dataset contains data about the unknown cost function and constraint,
allowing estimation of the same.
Although BO proved to be effective in solving the problem, it still requires
many iterations to converge to an optimal solution; given that performing an
experiment with the vehicle might be costly, we would like to assess whether a
faster convergence can be achieved by selecting different optimization tools.
Also, the high computational burden of BO is one important issue, and has been
recently tackled (Sabug Jr et al., 2022).

####  3.1.1 SMGO-$\Delta$

Set-Membership Global Optimization-$\Delta$ (SMGO-$\Delta$) is a novel data-
driven optimization, featuring unknown constraints (Sabug Jr et al., 2022).
Given a set of samples of the objective and constraints, SMGO-$\Delta$ uses
the existing information to build a surrogate Set Membership-based model of
the hidden functions, and iteratively selects the next point to evaluate. Such
a model is used to strategically decide between performing an exploitation
sampling in the vicinity of the current best sample, or exploration sampling
around the search space to discover the function shape. SMGO-$\Delta$ can be
used to solve a problem of the type in Eq. (20). We give here some details of
the algorithm functioning; the reader is referred to (Sabug Jr et al., 2022)
for detailed information.

By iteratively collecting data about the cost function and constraints as
detailed above, SMGO calculates Lipschitz constant
$\gamma_{f,g_{c}}^{\left(n\right)}$ and noise bound
$\varepsilon_{f,g_{c}}^{\left(n\right)}$ estimates for both $f_{bo}$ and
$g_{c}$ are computed and then used to estimate upper and lower confidence
bounds — note that BO attempts at fitting a surrogate of $f_{bo}$ and $g_{c}$,
while SMGO mostly considers the confidence bounds, thus being much lighter. As
an example, for $f_{bo}$, we have that

$\begin{split}\overline{f}_{bo}^{\left(n\right)}\left(\theta\right)=&\min_{k=1,\ldots,n}\left(f_{bo}^{\left(k\right)}+\gamma^{\left(n\right)}\left|\left|\theta-\theta^{\left(k\right)}\right|\right|\right),\\\
\underline{\smash{f}}_{bo}^{\left(n\right)}\left(\theta\right)=&\max_{k=1,\ldots,n}\left(f_{bo}^{\left(k\right)}-\gamma^{\left(n\right)}\left|\left|\theta-\theta^{\left(k\right)}\right|\right|\right).\end{split}$
(22)

The upper and lower bounds are then used to compute the mean value
$\tilde{f}_{bo}^{\left(n\right)}$ and the associated uncertainty
$\lambda^{(n)}\left(\theta\right)$

$\begin{split}\lambda^{(n)}\left(\theta\right)=&\overline{f}_{bo}^{(n)}\left(\theta\right)-\underline{\smash{f}}_{bo}^{(n)}\left(\theta\right),\\\
\tilde{f}_{bo}^{(n)}\left(\theta\right)=&\dfrac{1}{2}\left(\overline{f}_{bo}^{(n)}\left(\theta\right)+\underline{\smash{f}}_{bo}^{(n)}\left(\theta\right)\right)\end{split}$
(23)

The algorithm then selects the next point to evaluate $\tilde{\theta}^{(n)}$
based on the following problem

$\begin{split}\tilde{\theta}^{(n)}=&\operatorname*{arg\,min}_{\theta\in\mathcal{S}^{(n)}}\tilde{f}_{bo}^{(n)}\left(\theta\right)-\beta\lambda^{(n)}\left(\theta\right)\\\
\textrm{s.t.}\ \
&\Delta\tilde{g}^{(n)}\left(\theta\right)+\left(1-\delta\right)\underline{\smash{g}}^{(n)}\left(\theta\right)\geq
0\end{split}$ (24)

Whereas $\beta$ trades off between exploitation ($\beta=0$) and exploration
($\beta\geq 0$), and $\Delta$ trades off between cautiousness ($\delta=0$) and
riskiness ($\delta=1$) in constraint exploration. The candidate point
$\tilde{\theta}^{(n)}$ is then used to assess the inequality

$\underline{\smash{f}}_{bo}^{(n)}\left(\tilde{\theta}^{(n)}\right)\leq
f_{bo}^{*\left(n\right)}-\alpha_{smgo}\gamma^{(n)}_{f}$ (25)

If Eq. (25) above is satisfied, the algorithm effectively employs
$\tilde{\theta}^{(n)}$ as the next point to evaluate, otherwise, the
exploration routine is triggered, which aims at reducing the uncertainty (the
right hand side of Eq. (25)) while satisfying the constraints.

####  3.1.2 Virtual Reference Feedback Tuning

Figure 8: Reworked TiL control scheme, for VRFT implementation.

VRFT is a direct data-driven method for the design of Single-Input Single-
Output (SISO) parametric controllers, that does not require plant knowledge
(Campi et al., 2002). It selects a controller, parametrized by $\theta$, by
minimizing the following cost (whereas the controller is linear in this setup)

$\theta^{*}_{vrft}\left(\theta\right)=\operatorname*{arg\,min}_{\theta}\left|\left|\left(\dfrac{P\left(z\right)C_{\delta}\left(\theta\right)}{1+P\left(z\right)C_{\delta}\left(\theta\right)}-M_{r}\left(z\right)\right)M_{w}\left(z\right)\right|\right|_{2}^{2}.$

(26)

The cost in Eq. (26) means that VRFT tries to find a controller matching in
the frequency domain a discrete-time reference model $M_{r}(z)$, given a
weighting function $M_{w}(z)$. Indeed, theoretical guarantees on Eq. (26) only
apply to linear plants: in our specific case, no linearity assumption can be
drawn based on the plant in Fig. 8 (the plant encompasses both the digital
twin and its interaction with the controller). However, as showed in (Dettù et
al., 2023b), if the digital twin is a good replica of the real system, we can
reasonably assume that the dynamics to be controlled is a small signal one.
Nonetheless, VRFT has been succesfully used in many real systems, where the
”linearity” concept looses its meaning (Busetto et al., 2023; Radrizzani et
al., 2020; Passenbrunner et al., 2014).

Being the plant unknown, Eq. (26) is not usable; only sequences of input
$\left(s_{\delta,1},\ldots,s_{\delta,N_{exp}}\right)$ and output
$\left(y_{\epsilon,1},\ldots,y_{\epsilon,N_{exp}}\right)$ data are available
(an open-loop experiment suffices). Hence, the cost function in Eq. (26) is
suitably rewritten as a function of available data only (Care et al., 2019)

$f_{vrft}\left(\theta\right)=\dfrac{1}{N_{exp}}\sum_{k=1}^{N_{exp}}M_{w}(z)\left(C_{\delta}\left(\theta\right)\left(M_{r}(z)^{-1}-1\right)y_{\epsilon,k}-s_{\delta,k}\right).$

(27)

In the TiL setup, regulator $C_{\delta}$ controls the error
$y_{\epsilon}=\tilde{\epsilon}-\epsilon$, and regulates it to zero.

####  3.1.3 Comparing VRFT with global optimization

The obtained control parameters are then prone to be used as an initial guess
for a successive iterative algorithm (_e.g._ as in (Busetto et al., 2023)). As
one could note, the cost function of VRFT Eq. (27) is markedly different from
the one showed in Eq. (20). VRFT requires a reference model $M_{r}(z)$, and
cannot arbitrarily learn a controller minimizing the tracking error, as for
global optimizers. Apart from the reference model, to enhance performance is
often necessary to consider a $M_{w}(z)$, reasonably setting the frequencies
of interest. Nonetheless, we will show further on as the solution found by
VRFT is well performing if evaluated onto the cost of Eq. (21).

Also, global optimizers allow for an arbitrary cost function, _e.g._ taking
into account the control effort (see Eq. (20)): this is not possible in
classic VRFT. For a fair comparison of VRFT with BO, one could execute the
optimization routine described in Section 3.1 by using the VRFT cost in Eq.
(27), which in practice means pre-filtering the data according to $M_{r}(z)$
and $M_{w}(z)$, and removing the weight onto $\dot{s}_{act}$. VRFT is here
applied onto the tracking error $y_{\epsilon}$, and requires a virtual
reference to be passed through the desired model $M_{r}(z)$. However, the
reference for the error should be zero in a closed-loop setup like the one
considered in BO and SMGO, for this reason, the global optimizers cost
function is somewhat different in nature, in that it minimizes the $rms$ of
the error in a specific closed-loop experiment, with zero reference.

$f_{bo-
vrft}(\theta)=\dfrac{1}{N_{exp}}\sum_{k=1}^{N_{exp}}M_{w}(z)M_{r}(z)y_{\epsilon,k}^{2}$
(28)

##  4 Simulation results

In the following we conduct a series of simulation tests to assess the
performance of TiL lateral control onto the vehicle, while also analysing and
comparing the different optimization tools described above.

###  4.1 Simulation setup

####  4.1.1 The vehicle and the digital twin

$M\ [kg]$ $J_{zz}\ [kgm^{2}]$ $L_{f,r}\ [m]$ $\mathcal{A}_{f,r}$
$\mathcal{B}_{f,r}$ $1729.1$ $2482.7$ $1.48,\ 1.16$ $10.72,\ 19.75$ $1.51,\
0.75$ $\mathcal{C}_{f,r}$ $k_{a}^{f,r}\ [kg/m]$ $k_{x}\ [kg]$ $\dot{s}_{max}\
[deg/s]$ $\alpha^{f}_{max}\ [deg]$ $20.08,\ 28.69$ $0.065,\ 0.221$ $153.63$
$100$ $9.10$

Table 1: Set of vehicle parameters for the simplified model of Section 2.1.

For testing the TiL controller, since we do not have the possibility of
performing experiments on an actual vehicle, a different instance of the
Digital Twin is generated and regarded as the "Physical Vehicle". The
considered Digital Twin is modeled in VI-CarRealTime (an off-the-shelf
commercial simulation software (VI-Grade, 2022)). It models an high-
performance two seats car, and the most relevant parameters for the problem
under analysis are given in Table 1; they have been provided by partner
company Ferrari S.p.A. Note that the displayed parameters are those of the
simplified model derived in Section 2.1 and used within the MPC model. The
true underlying model features much more parameters; _e.g._ version 5 of the
Magic Formula is used for modelling the tire-road interaction, while we used a
3-parameters approximation of it within the MPC, encompassing lateral forces
only.

We assume that the real vehicle features some different elements and non-
idealities, which are absent in the Digital Twin:

  * 1.

The vehicle has real sensors, characterized by noise. Zero-mean Gaussian
distributed noise is added onto the yaw-rate measure $r$, characterized by
standard deviation $\sigma_{n,r}=0.006\ rad/s$. Similarly for the sideslip, we
mimic the presence of state-estimator, introducing a low-pass filtered noise
with standard deviation $\sigma_{n,\beta}=0.0044\ rad$. Overall, this yields
an $snr$ of $\approx 20$ in the considered signals, and the comparison between
real and noisy $\beta$ is similar to what obtained in recent works on the
topic (Carnier et al., 2023);

  * 2.

Additional masses are modelled in the real vehicle. Specifically, we add a
$100\ kg$ passenger and an unbalanced load on the front trunk ($70\ kg$ on the
left, $10\ kg$ on the right). The layout is the same considered in (Dettù et
al., 2023b);

  * 3.

We reduce the rear wheels cornering stiffness by the $15\ \%$, so as to mimic
a wrong tire model within the model based controller, or a modification of the
tire property due _e.g._ to low inflation pressure.

The modifications above reproduce a realistic case study, on which the
optimization is run and the controllers validated.

VI-CarRealTime is provided with a virtual driver feature, which is here used
to maintain a given speed profile (working as a longitudinal dynamics
controller): indeed, depending on the vehicle lateral dynamics, slightly
different speed profile tracking might be achieved

####  4.1.2 Parameters selection

We here briefly describe the parameters selection for the various controllers
and optimization algorithms used. Concerning the MPC, the following weights
are chosen; they have been found through fine tuning onto the Digital Twin

$w_{u}=1,\ w_{\rho}=100,\ w_{\beta}=0.2,\ w_{r}=0.8,\ w_{s}=0.$ (29)

The same are used within the TiL control scheme of Fig. 7. In $C_{\delta}$,
the parameter $\zeta$ (see Eq. (17)) trades off yaw-rate tracking for sideslip
minimization. It is set to $0.2$ so as to focus on the first objective, while
avoiding unsafe sideslip increments.

With regards to SMGO, $\Delta=0.5$ is used, to guarantee a balanced trade-off
between cautiousness and riskiness in constraint exploring. Other tuning
parameters for SMGO are let at their default values (Sabug Jr et al., 2022).

With regards to CBO, default values, the exploration ratio is set to $0.5$,
and the acquisition function is set as the Expected Improvement one.
$\beta_{max}$ is set at $4.5\ deg$, which is $\approx 2.5\ deg$ more than what
achieved by using the nominal MPC in the optimization maneuver: we want not to
significantly exceed this limit while training the controllers onto the same
maneuver. Indeed, this is not an issue for different maneuvers, where the
sideslip might naturally exceed this limit also in nominal conditions, and
$\beta_{max}$ has to be chosen for the specific maneuver of interest.

VRFT requires tuning of reference model $M_{r}(z)$ and frequency weighting
function $M_{w}(z)$. The first one is taken from the literature (Gimondi et
al., 2021), where a controller for yaw-rate dynamics is closed at the
bandwidth of $3.5\ Hz$: we thus set it as a first-order low-pass filter, with
one pole at this frequency. The frequency range is instead taken from the
reference generation filter (see Section 4); since the reference is cut after
$f_{ref}=6.3\ Hz$, we assign the same dynamics to $M_{w}(z)$. Of course, both
reference model and weight function are suitably discretized via the Tustin
approach.

###  4.2 Optimization results comparison

Figure 9: Input and output signals for VRFT use. Figure 10: Comparison of
black-box optimization algorithms for TiL calibration. Figure 11: Comparison
of black-box optimization algorithms for TiL calibration. Highlight on the
cost function.

Controller |  $rms(\tilde{r}-r)$ $\left[deg/s\right]$ |  $rms(\tilde{\beta}-\beta)$ $\left[deg\right]$ |  $rms(\dot{s}_{act})$ $\left[deg/s\right]$
---|---|---|---
MPC | $1.85$ | $1.81$ | $918.79$
TiL-SMGO-$\Delta$ | $0.74$ | $0.86$ | $514.41$
TiL-VRFT | $1.06$ | $0.95$ | $475.47$
TiL-SMGO-$\Delta$ (VRFT cost) | $1.04$ | $0.89$ | $935.42$

Table 2: Performance indices of the controllers evaluated in the optimization
test (double-lane-change with step-steer at $120\ km/h$).

For the optimization of $C_{\delta}$, we consider a double-lane change
maneuver, followed by a step steer, executed at $120\ km/h$.
To use VRFT, we execute the maneuver onto the digital twin (_i.e._ on the
upper branch in Fig. 7), while feeding the physical vehicle with a Pseudo
Random Binary Input signal (as in Radrizzani et al. (2020)), to excite the
dynamics to be controlled. These information is displayed in Fig. 9; the upper
plot depicts the command from DT $\tilde{s}_{cmd}$ and the one fed in open-
loop $s_{\delta}$. The lower plot depicts the system outputs $r$ and $\beta$,
as well as their combination $\epsilon$.

The learned controller is then used as a prior for global optimization; each
optimization iterates for $60$ steps. To minimize the effect of randomization
present in both CBO and SMGO-$\Delta$, we perform each optimization $10$
times. The results are displayed in Fig. 10: in the upper plot, the optimal
cost found at each iteration (averaged per the $10$ optimization runs) is
displayed.

The lower plot instead displays the number of infeasible experiments for each
controller, at each iteration, _i.e._ breaking the constraint on $\beta$. From
the upper plot, we note as VRFT is capable of delivering an almost optimal
solution, with just one experiment; BO and SMGO are able to approach VRFT cost
after $>10$ iterations on average. Figure 11 shows an highlight of the upper
plot: SMGO provides the better results in terms of cost function minimization,
while CBO is somewhat less performing. In general, both optimizers fail at
converging at the best point when VRFT prior is not provided. It is
interesting to note that these results confirm the findings in (Busetto et
al., 2023), for a different application.
If one looks at the bottom plot is clear as the increased performance achieved
with SMGO is traded with somewhat less cautious exploration, in that the
number of unfeasible attempts grows. This is consistent to what found in
(Busetto et al., 2023); when provided with VRFT prior, SMGO fastly switches
from exploitation mode to exploration mode (as the global minimum is in
practice already achieved by using VRFT), and this eventually translates into
breaking the constraints more easily.

Concerning the computation time, at each iteration CBO takes on average
333These results have been obtained with MATLAB 2022a, on a $16GB$ RAM Asus
Laptop, with an Intel Core i7-8750H $2.20GHz$ processor. $0.4442\ s$ –with
$0.0961\ s$ of standard deviation– to compute the next point to be evaluated;
SMGO-$\Delta$ is on the other hand significantly faster, taking $0.0238\ s$ on
average, with $0.0017\ s$ of standard deviation. In practice, SMGO-$\Delta$ is
almost two orders of magnitude faster than CBO for this optimization problem –
consistently to what found in (Sabug Jr et al., 2022), and this potentially
allows for the whole tuning procedure to be run on low cost computing units
and at real-time.

###  4.3 Time-domain results comparison

In the following, we compare the controllers optimized as above in the time-
domain. Being CBO and SMGO-$\Delta$ calibrations very similar, we show here
the second one. Also, given that the two global optimizers are able to
converge only by using VRFT control parameters as a prior, we consider the
corresponding SMGO-$\Delta$ calibration initialized with VRFT. We then show
the results obtained via VRFT calibration, and for the optimization maneuver,
we also show what would happen if explicitly using the VRFT cost function
within SMGO-$\Delta$.

####  4.3.1 Double lane change with step steer - $120\ km/h$

Figure 12: Controller validation onto the optimization experiment: yaw-rate
and sideslip tracking. Figure 13: Controller validation onto the optimization
experiment: speed and steer profiles.

Controller |  $rms(\tilde{r}-r)$ $\left[deg/s\right]$ |  $rms(\tilde{\beta}-\beta)$ $\left[deg\right]$ |  $rms(\dot{s}_{act})$ $\left[deg/s\right]$
---|---|---|---
MPC | $1.65$ | $1.46$ | $921.92$
TiL-SMGO-$\Delta$ | $0.75$ | $1.07$ | $462.35$
TiL-VRFT | $1.17$ | $1.25$ | $424.56$

Table 3: Performance of the controllers in the first validation test (double-
lane-change with step-steer at $140\ km/h$).

We show here the time-domain results when considering the optimization test,
_i.e._ the double lane change followed by a step steer, at $120\ km/h$. Figure
12 depicts the vehicle yaw-rate (upper plot) and sideslip angle (bottom plot).
The black dashed line $\tilde{r}$ is the reference behaviour obtained in
nominal conditions by using MPC onto the digital twin (see the scheme of Fig.
7). The nominal MPC exhibits some issues in the final part of the experiment,
and fails at maintaining the sideslip angle at an acceptable level, while also
badly tracking the yaw-rate. On the other hand, the TiL enhanced controller is
capable of smoothly recovering the system behaviour and guaranteeing good yaw-
rate tracking and minimization of the sideslip. Note that perfectly ”tracking”
the sideslip is not possible (nor it is required), since the cornering
stiffness is different and the physical vehicle has a different steady-state
response.

Looking at the performance obtained with VRFT in the time-domain confirms that
the method is adequate for learning a TiL controller, and significantly eases
the tuning phase, at the cost of a minimum performance reduction (note that
VRFT is achieving in a single iteration what BO or SMGO are able to do only
after 10 or 15 experiments). When considering SMGO with VRFT cost (_i.e._
filtering the output errors within the cost function), we note an oscillating
response. This is explainable, as the pre-filtering applied onto the measured
signals during the training process ”hides” some high- frequencies, and SMGO
is in fact over-fitting the controller onto a filtered version of the system,
poorly performing outside of that frequency range.

For the same experiment, Fig. 13 depicts speed (constant) and steer profiles
when using the same controllers. What observed from the oscillating yaw-rate
response in the SMGO with VRFT cost is further noted by the steer profile,
which is particularly aggressive. $s_{ref}$ is the driver steer request: one
can note as the controllers cut the request and apply a slightly different
steering angle, so as to guarantee the vehicle stability and avoid spinning
(_i.e._ too high sideslip angles). Finally, Table 2 quantifies the cost
indexes for the given experiment and the controllers.

####  4.3.2 Double lane change with step steer - $140\ km/h$

Figure 14: Controller validation onto the first testing experiment: yaw-rate
and sideslip tracking. Figure 15: Controller validation onto the first testing
experiment: speed and steer profiles.

We show here the time-domain results when considering a double lane change
followed by a step steer, at $140\ km/h$. Figure 16 depicts the vehicle yaw-
rate (upper plot) and sideslip angle (bottom plot). As in the previous case,
TiL is able to make the real vehicle track the digital twin: both SMGO and
VRFT calibrations suffices for our purposes, and yield very similar results.
Figure 17 shows the speed and steer profiles in the same test, while Table 4
provides some quantitative metrics.

####  4.3.3 Chikane test

Figure 16: Controller validation onto the second testing experiment: yaw-rate
and sideslip tracking. Figure 17: Controller validation onto the second
testing experiment: speed and steer profiles.

Controller |  $rms(\tilde{r}-r)$ $\left[deg/s\right]$ |  $rms(\tilde{\beta}-\beta)$ $\left[deg\right]$ |  $rms(\dot{s}_{act})$ $\left[deg/s\right]$
---|---|---|---
MPC | $5.40$ | $3.73$ | $3.09\times 10^{3}$
TiL-SMGO-$\Delta$ | $2.30$ | $1.25$ | $1.39\times 10^{3}$
TiL-VRFT | $3.59$ | $1.92$ | $1.19\times 10^{3}$

Table 4: Performance of the controllers in the second validation test
(chikane)

We show here the time-domain results when considering the second validation
test, _i.e._ a chikane maneuver inspired from the Savelli curve (nr. 7 in
Mugello track). In this case, a realistic speed profile is considered
(displayed in the bottom plot of Fig. 15), with the driver pushing the gas
pedal at the middle of the curve, thus combining lateral with longitudinal
acceleration; this kind of profile if particularly challenging for the
considered MPC controller, which assumes the longitudinal speed is constant in
the prediction horizon. In fact, from Fig. 14, one can note the worsened yaw-
rate tracking performance, with respect to constant speed tests. Also in this
case, the nominal MPC exhibits a much worse behaviour than TiL-enhanced ones.
This is further noted from the steering command, in the upper plot of Fig. 15,
which shows significant oscillations. Table 3 gives the quantitative metrics
for the chikane test: it is interesting to note that although slightly less
performing, VRFT calibration is somewhat less aggressive in terms of
$rms(\dot{s}_{act})$.

##  5 Conclusions

In this paper, we took a challenging case study for the recently proposed
TiL-C architecture, namely, the yaw-rate tracking problem, for which a
baseline Model Predictive Controller is designed, and then enhanced with a
simple PID compensator. A thorough discussion on different tools for
optimizing the compensator gains is carried out: specifically, we compared the
widely popular Bayesian Optimization with the newly proposed Set Membership
Global Optimization. We also consider a philosophically different approach,
the Virtual Reference Feedback Tuning, which is a direct control design
method, requiring just one batch of open-loop data for obtaining the
compensator gains.

The comparisons show as VRFT is capable of getting very close to the global
minimum, with just one experiment, while BO and SMGO need at least $10-15$
tests to overcome it, and fail at converging at the best point if not provided
with the previously computed VRFT controller gains.

The time-domain results validate the calibrated controllers in different
scenarios, considering both constant and varying speed profiles, thus
confirming the effectiveness of TiL-C with respect to the baseline controller,
and showing the amount of improvement achieved by performing some iterations
of BO/SMGO, as compared to VRFT.

## Acknowledgments

We would like to thank companies VI-Grade GmbH and Ferrari S.p.A. for the
technical support provided during the work.

## References

  * Beal and Gerdes (2012) Beal, C.E., Gerdes, J.C., 2012\.  Model predictive control for vehicle stabilization at the limits of handling.  IEEE Transactions on Control Systems Technology 21, 1258–1269.
  * Busetto et al. (2023) Busetto, R., Lucchini, A., Formentin, S., Savaresi, S.M., 2023\.  Data-driven optimal tuning of bldc motors with safety constraints: A set membership approach.  IEEE/ASME Transactions on Mechatronics .
  * Campi et al. (2002) Campi, M.C., Lecchini, A., Savaresi, S.M., 2002.  Virtual reference feedback tuning: a direct method for the design of feedback controllers.  Automatica 38, 1337–1346.
  * Care et al. (2019) Care, A., Torricelli, F., Campi, M.C., Savaresi, S.M., 2019\.  A toolbox for virtual reference feedback tuning (vrft), in: 2019 18th European control conference (ECC), IEEE. pp. 4252–4257.
  * Carnier et al. (2023) Carnier, S., Corno, M., Savaresi, S.M., 2023.  Hybrid kinematic-dynamic sideslip and friction estimation.  Journal of Dynamic Systems, Measurement, and Control 145, 051004.
  * Corno et al. (2023) Corno, M., Gimondi, A., Panzani, G., Roselli, F., Alessandretti, A., Savaresi, S.M., 2023\.  A non-optimization-based dynamic path planning for autonomous obstacle avoidance.  IEEE Transactions on Control Systems Technology 31, 722–734.
  * Coutinho et al. (2023) Coutinho, J.P., Santos, L.O., Reis, M.S., 2023.  Bayesian optimization for automatic tuning of digital multi-loop pid controllers.  Computers & Chemical Engineering 173, 108211.
  * Delcaro et al. (2023) Delcaro, G., Dettù, F., Formentin, S., Savaresi, S.M., 2023\.  Dealing with the curse of dimensionality in twin-in-the-loop observer design, in: 22nd IFAC World Congress.
  * Dettù et al. (2023a) Dettù, F., Formentin, S., Savaresi, S.M., 2023a.  Dealing with the curse of dimensionality in twin-in-the-loop observer design, in: 22nd IFAC World Congress.
  * Dettù et al. (2023b) Dettù, F., Formentin, S., Savaresi, S.M., 2023b.  The twin-in-the-loop approach for vehicle dynamics control.  IEEE/ASME Transaction on Mechatronics .
  * Dettù et al. (2023) Dettù, F., Corno, M., D’Ambrosio, D., Acquistapace, A., Taroni, F., Savaresi, S.M., 2023\.  Modeling, control design and experimental automatic calibration of a leveling system for combine harvesters.  Control Engineering Practice 132, 105411.
  * Falcone et al. (2007) Falcone, P., Borrelli, F., Asgari, J., Tseng, H.E., Hrovat, D., 2007.  Predictive active steering control for autonomous vehicle systems.  IEEE Transactions on control systems technology 15, 566–580.
  * Ferreau et al. (2014) Ferreau, H., Kirches, C., Potschka, A., Bock, H., Diehl, M., 2014.  qpOASES: A parametric active-set algorithm for quadratic programming.  Mathematical Programming Computation 6, 327–363.
  * Galbiati et al. (2022) Galbiati, R., Sabug, L., Ruiz, F., Fagiano, L., 2022\.  Direct control design using a set membership-based black-box optimization approach, in: 2022 IEEE Conference on Control Technology and Applications (CCTA), IEEE. pp. 1259–1264.
  * Gimondi et al. (2021) Gimondi, A., Corno, M., Savaresi, S.M., 2021.  A mixed sideslip yaw rate stability controller for over-actuated vehicles, in: International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, American Society of Mechanical Engineers. p. V001T01A001.
  * Hellström et al. (2013) Hellström, E., Lee, D., Jiang, L., Stefanopoulou, A.G., Yilmaz, H., 2013.  On-board calibration of spark timing by extremum seeking for flex-fuel engines.  IEEE Transactions on control systems technology 21, 2273–2279.
  * Hjalmarsson et al. (1998) Hjalmarsson, H., Gevers, M., Gunnarsson, S., Lequin, O., 1998\.  Iterative feedback tuning: theory and applications.  IEEE control systems magazine 18, 26–41.
  * Jaen-Cuellar et al. (2013) Jaen-Cuellar, A.Y., de J. Romero-Troncoso, R., Morales-Velazquez, L., Osornio-Rios, R.A., 2013.  Pid-controller tuning optimization with genetic algorithms in servo systems.  International Journal of Advanced Robotic Systems 10, 324.
  * Khosravi et al. (2022) Khosravi, M., König, C., Maier, M., Smith, R.S., Lygeros, J., Rupenyan, A., 2022\.  Safety-aware cascade controller tuning using constrained bayesian optimization.  IEEE Transactions on Industrial Electronics 70, 2128–2138.
  * Kim et al. (2008) Kim, T.H., Maruta, I., Sugie, T., 2008.  Robust pid controller tuning based on the constrained particle swarm optimization.  Automatica 44, 1104–1110.
  * Lucchini et al. (2021) Lucchini, A., Azza, F.P., Corno, M., Formentin, S., Savaresi, S.M., 2021.  Design and implementation of a mpc-based rear-wheel steering controller for sports cars, in: 2021 IEEE Conference on Control Technology and Applications (CCTA), IEEE. pp. 802–807.
  * Lucchini et al. (2020) Lucchini, A., Formentin, S., Corno, M., Piga, D., Savaresi, S.M., 2020.  Torque vectoring for high-performance electric vehicles: an efficient mpc calibration.  IEEE Control Systems Letters 4, 725–730.
  * Passenbrunner et al. (2014) Passenbrunner, T.E., Formentin, S., Savaresi, S.M., del Re, L., 2014\.  Direct multivariable controller tuning for internal combustion engine test benches.  Control Engineering Practice 29, 115–122.
  * Radrizzani et al. (2020) Radrizzani, S., Todeschini, D., Riva, G., Formentin, S., Panzani, G., Savaresi, S.M., 2020\.  A data-driven approach for fast controller calibration of brake-by-wire actuators, in: 2020 IEEE Conference on Control Technology and Applications (CCTA), IEEE. pp. 561–566.
  * Riva et al. (2022a) Riva, G., Formentin, S., Corno, M., Savaresi, S.M., 2022a.  Model predictive control of high-performance braking systems: A force-based approach.  IEEE Control Systems Letters 6, 2383–2388.
  * Riva et al. (2022b) Riva, G., Formentin, S., Corno, M., Savaresi, S.M., 2022b.  Twin-in-the-loop state estimation for vehicle dynamics control: theory and experiments.  arXiv:2209.02263 .
  * Sabug Jr et al. (2023) Sabug Jr, L., Incremona, G.P., Tanelli, M., Ruiz, F., Fagiano, L., 2023.  Simultaneous design of passive and active spacecraft attitude control using black-box optimization.  Control Engineering Practice 135, 105516.
  * Sabug Jr et al. (2022) Sabug Jr, L., Ruiz, F., Fagiano, L., 2022.  Smgo-$\delta$: Balancing caution and reward in global optimization with black-box constraints.  Information Sciences 605, 15–42.
  * Samad (2017) Samad, T., 2017.  A survey on industry impact and challenges thereof [technical activities].  IEEE Control Systems Magazine 37, 17–18.
  * Shahriari et al. (2015) Shahriari, B., Swersky, K., Wang, Z., Adams, R.P., De Freitas, N., 2015.  Taking the human out of the loop: A review of bayesian optimization.  Proceedings of the IEEE 104, 148–175.
  * Spielberg et al. (2022) Spielberg, N.A., Brown, M., Gerdes, J.C., 2022.  Neural network model predictive motion control applied to automated driving with unknown friction.  IEEE Transactions on Control Systems Technology 30, 1934–1945.
  * VI-Grade (2022) VI-Grade, 2022.  Autohawk.  https://www.vi-grade.com/en/products/autohawk/.  [Online; accessed 17-October-2022].
  * VI-Grade (2022) VI-Grade, 2022.  Vi-carrealtime.  https://www.vi-grade.com/en/products/vi-carrealtime/.  [Online; accessed 23-March-2022].


Formalizing Relations in Type Theory]Formalizing Relations in Type Theory

F. Kachapova]Farida Kachapova
Department of Mathematical Sciences

Auckland University of Technology

New Zealand

Type theory plays an important role in foundations of mathematics as a framework for formalizing mathematics and a base for proof assistants providing semi-automatic proof checking and construction. Derivation of each theorem in type theory results in a formal term encapsulating the whole proof process. In this paper we use a variant of type theory, namely the Calculus of Constructions with Definitions, to formalize the standard theory of binary relations. This includes basic operations on relations, criteria for special properties of relations, invariance of these properties under the basic operations, equivalence relation, well-ordering, and transfinite induction. Definitions and proofs are presented as flag-style derivations.

[2020]Primary 03B30; Secondary 03B38

§ INTRODUCTION

First type theories were proposed by B. Russell [10] as a foundation of mathematics. Other important type theories are typed $\lambda$-calculus introduced by A. Church [2] and intuitionistic type theory introduced by P. Martin-Löf [7]. A higher-order typed $\lambda$-calculus known as Calculus of Constructions (CoC) was created by T. Coquand [3]. Variants of CoC make formal bases of proof assistants, which are computer tools for formalizing and developing mathematics. In particular, the well-known proof assistant Coq is based on the strong variant of CoC called the Calculus of Inductive Constructions (CIC).

Here we use the variant $\lambda D$ of CoC developed in [8]; $\lambda D$ is called the Calculus of Constructions with Definitions. We choose $\lambda D$ because of its following useful properties.

– In $\lambda D$, as in other variants of CoC, proofs are expressed as formal terms and thus are incorporated in the system.

– In $\lambda D$ type checking is decidable and therefore proof checking is decidable. So the correctness of a proof can be checked by an algorithm.

– $\lambda D$ is strongly normalizing, which implies the logical consistency of this theory, even with classical logic (when no extra axioms are added) - see [1].

The theory $\lambda D$ is weaker than CIC because $\lambda D$ does not have inductive types. This does not limit its capability for formalizing mathematics because in $\lambda D$ we can use axiomatic approach and higher-order logic to express the objects that CIC defines with inductive types.

In Section 2 we briefly describe the theory $\lambda D$, derived rules of intuitionistic logic in $\lambda D$, and the classical axiom of excluded third that can be added to $\lambda D$ if necessary; we also briefly explain the flag format derivation.
In Section 3 we describe the equality in $\lambda D$ and its derived properties.

In Section 4 we study binary relations in $\lambda D$, operations on relations, and their properties. In Section 5 we formally prove criteria of relexivity, symmetry, antisymmetry and transitivity, and study the invariance of these properties under some basic operations. In Section 6 we formally define partitions in $\lambda D$ and provide a proof of their correspondence with equivalence relations. In Section 6 we also provide an example of partial order with  a formal proof, definition of well-ordering in $\lambda D$ and a formal proof of the principle of transfinite induction.

In our formalizations we aim to keep the language and theorems as close as possible to the ones of standard mathematics.
In definitions and proofs we use the flag-style derivation described in [8]. Long formal derivations are moved from the main text to Appendices for better readability.

§ TYPE THEORY $\LAMBDA D$

In [8] Nederpelt and Geuvers developed a formal theory  $\lambda D$ and formalized some parts of logic and mathematics in it. Here we briefly describe main features of $\lambda D$.

§.§ Type Theory $\lambda D$

The language of $\lambda D$ described in [8] has an infinite set of variables, $V$, and an infinite set of constants, $C$; these two sets are disjoint. There are also special symbols $\square$ and $*$.

Expressions of the language are defined recursively as follows.

* Each variable is an expression.

* Each constant is an expression.

* Constant * is an expression.

* Constant $\square$ is an expression.

* (Application) If $A$ and $B$ are expressions, then $AB$ is an expression.

* (Abstraction) If $A$,  $B$ are expressions and $x$ is a variable, then $\lambda x:A.B$ is an expression.

* (Dependent Product) If $A$,  $B$ are expressions and $x$ is a variable, then $\Pi x:A.B$ is an expression.

* If $A_1,A_2,\ldots,A_n$ are expressions and $c$ is a constant, then $c\left(A_1,A_2,\ldots,A_n\right)$ is an expression.

An expression $A\rightarrow B$ is introduced as a particular type of Dependent Product from (7) when $x$ is not a free variable in $B$.

* A statement is of the form $M:N$, where $M$ and $N$ are expressions.

* A declaration is of the form $x:N$, where $x$ is a variable and $N$ is an expression.

* A descriptive definition is of the form:

\[\bar{x}:\bar{A}\rhd c(\bar{x}):=M:N,\]

where $\bar{x}$ is a list $x_1,x_2,\ldots,x_n$ of variables, $\bar{A}$ is a list $A_1,A_2,\ldots,A_n$ of expressions, $c$ is a constant, and $M$ and $N$ are expressions.

* A primitive definition is of the form:

\[\bar{x}:\bar{A}\rhd c(\bar{x}):=\Bot:N,\]

where $\bar{x}$, $\bar{A}$, and $c$ are described the same way as in (3), and $N$ is an expression. The symbol $\Bot$  denotes the non-existing definiens. Primitive definitions are used for introducing axioms where no proof terms are needed.

* A definition is a descriptive definition or a primitive definition.

* A judgement is of the form:

\[\Delta;\Gamma \vdash M:N,\]

where $M$ and $N$ are expressions of the language, $\Delta$ is an environment (a properly constructed sequence of definitions) and $\Gamma$ is a context (a properly constructed sequence of declarations).

For brevity we often use implicit variables in definitions, that is we omit the previously declared variables $\bar{x}$ in $c(\bar{x})$ in (3) and (4).

The following informally explains the meaning of expressions.

* If an expression $M$ appears in a derived statement of the form $M$ $:*$, then $M$ is interpreted as a type, which represents a set or a proposition.

Note: There is only one type $*$ in $\lambda D$. But informally we often use $*_p$ for propositions and $*_s$ for sets to make proofs more readable.

* If an expression $M$ appears in a derived statement of the form $M:N$, where $N$ is a type, then $M$ is interpreted as an object at the lowest level.

When $N$ is interpreted as a set, then $M$ is regarded as an element of this set.

When $N$ is interpreted as a proposition, then $M$ is regarded as a proof (or a proof term) of this proposition.

* The symbol $\square$ represents the highest level.

* Sort is $*$ or $\square$. Letters $s, s_1,s_2,\ldots$ are used as variables for sorts.

* If an expression $M$ appears in a statement of the form $M:\square$, then $M$ is called a kind.
$\lambda D$ contains the derivation rule:

\[\varnothing;\varnothing \vdash *:\square,\]

which is its (only) axiom because it has an empty environment and an empty context.

Further details of the language and derivation rules of the theory $\lambda D$ can be found in [8]. Judgments are formally derived in $\lambda D$ using the derivation rules.

§.§ Flag Format of Derivations

The flag-style deduction was introduced by Jaśkowski  [5] and Fitch [4]. A derivation in the flag format is a linear deduction. Each "flag" (a rectangular box) contains a declaration that introduces a variable or an assumption; a collection of already introduced variables and assumptions makes the current context. The scope of the variable or assumption is established by the "flag pole". In the scope we construct definitions and proof terms for proving statements/ theorems in $\lambda D$. Each new flag extends the context and at the end of each flag pole the context is reduced by the corresponding declaration.
For brevity we can combine several declarations in one flag.

More details on the flag-style deduction can be found in [9] and [8].

§.§ Logic in $\lambda D$

The rules of intuitionistic logic are derived in the theory $\lambda D$ as shown in [8]. We briefly describe it here by showing the introduction and elimination rules for logical connectives and quantifiers.

§.§.§ Implication

The logical implication $A\Rightarrow B$ is identified with the arrow type $A\rightarrow B$. The rules for implication follow from the following general rules for the arrow type (we write them in the flag format):

*A:s_1 | B:s_2
*u:A→B | v:A
*λx:A.M : A→B

Here $x$ is not a free variable in $B$.

In $\lambda D$ arrows are right associative, that is $A\rightarrow B\rightarrow C$ is a shorthand for $A\rightarrow (B\rightarrow C)$.

§.§.§ Falsity and Negation

Falsity $\bot$ is introduced in $\lambda D$ by:

\[\bot:=\Pi A:*_p.A\;:\;*_p.\]

From this definition we get a rule for falsity:

The rule states that falsity implies any proposition.

As usual, negation is defined by: $\neg A:= A\rightarrow \bot$.

Other logical connectives and quantifiers are also defined using second order encoding. Here we only list their derived rules and names of the corresponding terms, without details of their construction.
The exact values of the terms can be found in [8].

Some of our flag derivations contain the proof terms that will be re-used in other proofs; such proof terms are written in bold font, e.g. $\boldsymbol{\wedge}\textbf{-in}$ in the first derived rule for conjunction as follows.

§.§.§ Conjunction

These are derived rules for conjunction $\wedge$:

*u:A | v:B
*∧-in(A,B,u,v)   : A∧B
*∧-el_1(A,B,w)   : A
*∧-el_2(A,B,w)   : B

§.§.§ Disjunction

These are derived rules for disjunction $\vee$:

*∨-in_1(A,B,u)   : A∨B
*∨-in_2(A,B,u)   : A∨B
*u:A∨B | v:A⇒C | w:B⇒C
*∨-el(A,B,C,u,v,w)   : C

§.§.§ Bi-implication

Bi-implication $\Leftrightarrow$ has the standard definition:

\[(A\Leftrightarrow B):=(A\Rightarrow B)\wedge (B\Rightarrow A).\]

We will often use this lemma to prove bi-implication $A\Leftrightarrow B$.

*u:A⇒B | v:B⇒A
*bi-impl(A,B,u,v):=∧-in(A⇒B,B⇒A,u,v) : A⇔B

§.§.§ Universal Quantifier

The universal quantifier $\forall$ is defined through the dependent product:

*S:*_s | P:S→*_p
*Definition  ∀(S,P) :=Πx:S.Px : *_p
* Notation: (∀𝐱:𝐒.𝐏𝐱)  for ∀(S,P)

§.§.§ Existential Quantifier

These are derived rules for the existential quantifier $\exists$.

*S:*_s | P:S→*_p
*y:S | u:Py
*∃-in(S,P,y,u)   : (∃x:S.Px)
*u:(∃x:S.Px) | v:(∀x:S.(Px⇒C))
*∃-el(S,P,u,C,v)   : C

Here $x$ is not a free variable in $C$.

§.§.§ Classical Logic

We use mostly intuitionistic logic. But sometimes classical logic is needed; in these cases we add the following Axiom of Excluded Third:

*exc-thrd(A):= : A∨A

This axiom implies the Double Negation theorem:

§.§ Sets in $\lambda D$

Here we briefly repeat some definitions from [8]
relating to sets, in particular, subsets of type $S$.

*ps(S):=S→*_pPower set of S
{x:S | xεV} for λx:S.Vx

*x: S
*Notation: xε_S V  or xεV for element(S,x,V)

Thus, a subset $V$ of $S$ is regarded as a predicate on $S$ and $x\varepsilon V$ means $x$ satisfies the predicate $V$.

§ INTENSIONAL EQUALITY IN $\LAMBDA D$

Here we introduce intensional equality for elements of any type; we will call it just equality. In the next section we will introduce extensional equality and the axiom of extensionality relating the two types of equality.

*x,y: S
*eq(S,x,y):=ΠP:S→*_p. (Px⇒Py):*_p
* Notation: x=_Sy  for  eq(S,x,y)Intensional equality

§.§ Properties of Equality

§.§.§ Reflexivity

The following diagram proves the reflexivity property of equality in $\lambda D$.

*S:* | x: S
*P: S→*_p

Proof terms are constructed similarly for the following properties of Substitutivity, Congruence, Symmetry, and Transitivity (see [8]).

§.§.§ Substitutivity

Substitutivity means that equality is consistent with predicates of corresponding types.

*P: S→*_p
*x,y: S | u:x=_Sy | v:Px

§.§.§ Congruence

Congruence means that equality is consistent with functions of corresponding types.

*f: Q→S
*x,y: Q | u:x=_Qy

§.§.§ Symmetry

The following diagram expresses the symmetry property of equality in $\lambda D$.

*x,y: S | u:x=_Sy

§.§.§ Transitivity

The following diagram expresses the transitivity property of equality in $\lambda D$.

*x,y,z: S | u:x=_Sy | v:y=_Sz

§ RELATIONS IN TYPE THEORY

§.§ Sets in $\lambda D$

Here we briefly repeat some definitions from [8]
relating to sets, in particular, subsets of type $S$.

*ps(S):=S→*_pPower set of S
{x:S | xεV} for λx:S.Vx

*x: S
*Notation: xε_S V  or xεV for element(S,x,V)

Thus, a subset $V$ of $S$ is regarded as a predicate on $S$ and $x\varepsilon V$ means $x$ satisfies the predicate $V$.

§.§ Defining Binary Relations in $\lambda D$

Binary relations are introduced in [8], together with the properties of reflexivity, symmetry, antisymmetry, and transitivity, and definitions of equivalence relation and partial order. We use them as a starting point for formalizing the theory of binary relations in $\lambda D$.

A relation on $S$ is a binary predicate on $S$, which is regarded in $\lambda D$ as a composition of unary predicates. For brevity we introduce the type $br(S)$ of all binary relations on $S$:

*S: *_s

*Definition  br(S):= S→S→*_p  : □

In the rest of the article we call binary relations just relations.
The equality of relations and operations on relations are defined similarly to the set equality and set operations.

Next we define the extensional equality of relations vs the intentional equality introduced in the previous section.

*S: *_s
*Definition  ⊆(S,R,Q) :=(∀x,y:S.(Rxy⇒Qxy)) : *_p
* Notation: R⊆Q  for  ⊆(S,R,Q)
*Definition  Exeq(S,R,Q) :=R⊆Q∧Q⊆R : *_p
* Notation: R=Q  for  Exeq(S,R,Q) Extensional equality

We add to the theory $\lambda D$ the following axiom of extensionality for relations.

*S: *_s
*extaxiom(S,R,Q,u) := :  R=_br(S)QExtensionality Axiom

The axiom is introduced in the last line by a primitive definition with the symbol $\Bot$ replacing a non-existing proof term.
The Extensionality Axiom states that the two types of equality are the same for binary relations. So we will use the symbol = for both and we will not elaborate on details of applying the axiom of extensionality when converting one type of equality to the other.

§.§ Operations on Binary Relations

Using the flag format, we introduce the identity relation $id_S$ on type $S$ and converse  $R^{-1}$ of a relation $R$.

*S: *_s
*Definition  id_S :=λx,y:S.(x=_Sy) : br(S)Identity relation

*Definition  conv(S,R) :=λx,y:S.(Ryx) : br(S)
* Notation: R^-1  for  conv(S,R)Converse relation

Next we introduce the  operations of union $\cup$,  intersection $\cap$, and composition $\circ$ of relations.

*S: *_s

*Definition  ∪(S,R,Q) :=λx,y:S.(Rxy∨Qxy) : br(S)
* Notation: R∪Q  for  ∪(S,R,Q)Union

*Definition  ∩(S,R,Q) :=λx,y:S.(Rxy∧Qxy) : br(S)
* Notation: R∩Q  for  ∩(S,R,Q)Intersection

*Definition  ∘(S,R,Q) :=λx,y:S.(∃z:S. (Rxz∧Qzy)) : br(S)
* Notation: R∘Q  for  ∘(S,R,Q)Composition

§.§ Properties of Operations

The following two technical lemmas will be used in some future proofs.

This lemma gives a shortcut for constructing an element of a composite relation.

*S: *_s | R,Q:br(S) | x,y,z:S
*u:Rxy | v:Qyz
*a:=∧-in (Rxy,Qyz,u,v) : Rxy∧Qyz
*prod-term (S,R,Q,x,y,z,u,v):=∃-in (S,λt.Rxt∧Qtz,y,a) : (R∘Q)xz

This lemma gives a shortcut for proving equality of two relations.

*S: *_s | R,Q:br(S)
*u:R⊆Q | v:Q⊆R
*relequal (S,R,Q,u,v):=∧-in (R⊆Q,Q⊆R,u,v) : R= Q

For relations $R,P$ and $Q$ on $S$ the following hold.

1) $(R^{-1})^{-1}=R.$

2) $(R\circ Q)^{-1}=Q^{-1}\circ R^{-1}.$

3) $(R\cap Q)^{-1}=R^{-1}\cap Q^{-1}.$

4) $(R\cup Q)^{-1}=R^{-1}\cup Q^{-1}.$

5) $R\circ(P\cup Q)=R\circ P\cup R\circ Q.$

6) $(P\cup Q)\circ R=P\circ R\cup Q\circ R.$

7) $R\circ(P\cap Q)\subseteq R\circ P\cap R\circ Q.$

8) $(P\cap Q)\circ R\subseteq P\circ R\cap Q\circ R.$

9) $(R\circ P)\circ Q=R\circ(P\circ Q).$

The formal proof is in part A of Appendix. The proof of part 2) has the form:

*S: *_s | R,Q:br(S)
*convprod(S,R,Q):=… : (R∘Q)^-1=Q^-1∘R^-1

Its proof term $conv\mhyphen prod(S,R,Q)$ will be re-used later in the paper.

§ PROPERTIES OF BINARY RELATIONS

The properties of reflexivity, symmetry, antisymmetry, transitivity, and the relations of equivalence and partial order are defined in [8] as follows.

*S:*_s | R:br(S)

*Definition  refl(S,R) :=∀x:S.(Rxx) : *_p

*Definition  sym(S,R) :=∀x,y:S.(Rxy⇒Ryx) : *_p

*Definition  antisym(S,R) :=∀x,y:S.(Rxy⇒Ryx⇒x=_Sy) : *_p

*Definition  trans(S,R) :=∀x,y,z:S.(Rxy⇒Ryz⇒Rxz) : *_p

*Definition  equiv$-$relation(S,R) :=refl(S,R)∧sym(S,R)
∧ trans(S,R) : *_p

*Definition  part$-$ord(S,R) :=refl(S,R)∧antisym(S,R)
∧ trans(S,R) : *_p

Suppose $R$ is a relation on type $S$. Then the following hold.

1) Criterion of reflexivity.
$R$ is reflexive $\Leftrightarrow id_S\subseteq R$.

2) First criterion of symmetry.
$R$ is symmetric $\Leftrightarrow R^{-1}\subseteq R$.

3) Second criterion of symmetry.
$R$ is symmetric $\Leftrightarrow R^{-1}= R$.

4) Criterion of antisymmetry.
$R$ is antisymmetric $\Leftrightarrow R^{-1}\cap R\subseteq id_S$.

5) Criterion of transitivity. $R$ is transitive $\Leftrightarrow R\circ R\subseteq R$.

The formal proof is in part B of Appendix. The proof of part 3) has the form:

*S: *_s | R:br(S)
*symcriterion(S,R):=… : sym(S,R)⇔R^-1=R

Its proof term $sym\mhyphen criterion(S,R)$ will be re-used later in the paper.

Relation $R$ on $S$ is reflexive, symmetric and antisymmetric $\Rightarrow R=id_S.$

The formal proof is in the following flag diagram.

*S:*_s | R:br(S)
*u_1:refl(S,R) | u_2:sym(S,R) | u_3:antisym(S,R)
*x,y:S | v:Rxy
*a_3:=λx,y:S.λv:Rxy.a_2 : (R⊆id_S)
*x,y:S | v:(id_S)xy
*Notation P:=λz:S.Rxz : S→*_p
*a_6:=λx,y:S.λv:(id_S)xy.a_5 : (id_S⊆R)

Invariance under converse operation. Suppose $R$ is a relation on type $S$. Then the following hold.

1) $R$ is reflexive $\Rightarrow R^{-1}$ is reflexive.

2) $R$ is symmetric $\Rightarrow R^{-1}$ is symmetric.

3) $R$ is antisymmetric $\Rightarrow R^{-1}$ is antisymmetric.

4) $R$ is transitive $\Rightarrow R^{-1}$ is transitive.

*S:*_s | R:br(S)
*a:=λx:S.ux : refl(S,R^-1)

*S:*_s | R:br(S)
*x,y:S | v:R^-1xy
*a_1:=uyxv : Rxy
*a_2:=λx,y:S.λv:R^-1xy.a_1 : sym(S,R^-1)

*S:*_s | R:br(S)
*x,y:S | v:R^-1xy | w:R^-1yx
*a_1:=uxywv : x=y
*a_2:=λx,y:S.λv:R^-1xy.λw:R^-1yx.a_1 : antisym(S,R^-1)

*S:*_s | R:br(S)
*x,y,z:S | v:R^-1xy | w:R^-1yz
*a_1:=uzyxwv : Rzx
*a_2:=λx,y,z:S.λv:R^-1xy.λw:R^-1yz.a_1 : trans(S,R^-1)

Invariance under intersection. Suppose $R$ and $Q$ are relations on type $S$. Then the following hold.

1) $R$ and $Q$ are reflexive $\Rightarrow R\cap Q$ is reflexive.

2)  $R$ and $Q$ are symmetric $\Rightarrow R\cap Q$ is symmetric.

3)  $R$ or $Q$ is antisymmetric $\Rightarrow R\cap Q$ is antisymmetric.

4)  $R$ and $Q$ are transitive $\Rightarrow R\cap Q$ is transitive.

*S:*_s | R,Q:br(S)
*u:refl(S,R) | v:refl(S,Q)
*a_1:=ux : Rxx
*a_2:=vx : Qxx
*a_3:=∧-in (Rxx,Qxx,a_1,a_2) : (R∩Q)xx
*a_4:=λx:S.a_3 : refl(S,R∩Q)

*S:*_s | R,Q:br(S)
*u:sym(S,R) | v:sym(S,Q)
*x,y:S | w:(R∩Q)xy
*a_1:=∧-el_1(Rxy,Qxy,w) : Rxy
*a_2:=∧-el_2(Rxy,Qxy,w) : Qxy
*a_3:=uxya_1 : Ryx
*a_4:=vxya_2 : Qyx
*a_5:=∧-in (Ryx,Qyx,a_3,a_4) : (R∩Q)yx
*a_6:=λx,y:S.λw:(R∩Q)xy. a_5 : sym(S,R∩Q)

*S:*_s | R,Q:br(S)
*Notation A:=antisym(S,R):*_p
*Notation B:=antisym(S,Q):*_p
*Notation C:=antisym(S,R∩Q):*_p
*x,y:S | w_1:(R∩Q)xy | w_2:(R∩Q)yx
*a_1:=∧-el_1(Rxy,Qxy,w_1) : Rxy
*a_2:=∧-el_1(Ryx,Qyx,w_2) : Ryx
*a_3:=vxya_1a_2 : x=y
*[2]a_4:=λv:A.λx,y:S.λw_1:(R∩Q)xy.λw_2:(R∩Q)yx.a_3 : (A⇒C)

*x,y:S | w_1:(R∩Q)xy | w_2:(R∩Q)yx
*a_5:=∧-el_2(Rxy,Qxy,w_1) : Qxy
*a_6:=∧-el_2(Ryx,Qyx,w_2) : Qyx
*a_7:=vxya_5a_6 : x=y
*[2]a_8:=λv:B.λx,y:S.λw_1:(R∩Q)xy.λw_2:(R∩Q)yx.a_7 : (B⇒C)

*S:*_s | R,Q:br(S)
*u_1:trans(S,R) | u_2:trans(S,Q)
*x,y,z:S | v:(R∩Q)xy | w:(R∩Q)yz
*a_1:=∧-el_1(Rxy,Qxy,v) : Rxy
*a_2:=∧-el_2(Rxy,Qxy,v) : Qxy
*a_3:=∧-el_1(Ryz,Qyz,w) : Ryz
*a_4:=∧-el_2(Ryz,Qyz,w) : Qyz
*a_5:=u_1xyza_1a_3 : Rxz
*a_6:=u_2xyza_2a_4 : Qxz
*a_7:=∧-in (Rxz,Qxz,a_5,a_6) : (R∩Q)xz
*a_8:=λx,y,z:S.λv:(R∩Q)xy.λw:(R∩Q)yz.a_7 : trans(S,R∩Q)

Invariance under union. Suppose $R$ and $Q$ are relations on type $S$. Then the following hold.

1) $R$ or $Q$ is reflexive $\Rightarrow R\cup Q$ is reflexive.

2)  $R$ and $Q$ are symmetric $\Rightarrow R\cup Q$ is symmetric.

*S:*_s | R,Q:br(S)
*u:refl(S,R) | x:S
*ux : Rxx
*a_1:=∨-in_1(Rxx,Qxx,ux) : (R∪Q)xx
*a_2:=∨-in_2(Rxx,Qxx,ux) : (Q∪R)xx
*a_3:=λu:refl(S,R).λx:S.a_1 : (refl(S,R)⇒refl(S,R∪Q))
*a_4(R,Q):=λu:refl(S,R).λx:S.a_2 : (refl(S,R)⇒refl(S,Q∪R))
*a_5:=a_4(Q,R) : (refl(S,Q)⇒refl(S,R∪Q))
*a_7:=∨el(refl(S,R),refl(S,Q),refl(S,R∪Q),u,a_3,a_5) : refl(S,R∪Q)

*S:*_s | R,Q:br(S)
*u_1:sym(S,R) | u_2:sym(S,Q)
*x,y:S | v:(R∪Q)xy
*a_1:=u_1xyw : Ryx
*a_2:=∨-in_1(Ryx,Qyx,a_1) : (R∪Q)yx
*a_3:=λw:Rxy. a_2 : (Rxy⇒(R∪Q)yx)

*a_4:=u_2xyw : Qyx
*a_5:=∨-in_2(Ryx,Qyx,a_4) : (R∪Q)yx
*a_6:=λw:Qxy. a_5 : (Qxy⇒(R∪Q)yx)
*a_7:=∨-el(Rxy,Qxy,(R∪Q)yx,v,a_3,a_6) : (R∪Q)yx
*a_8:=λx,y:S.λv:(R∪Q)xy. a_7 : sym(S,R∪Q)

Invariance under composition. Suppose $R$ and $Q$ are relations on type $S$. Then the following hold.

1) $R\circ R^{-1}$ is always symmetric.

2) $R$ and $Q$ are reflexive $\Rightarrow R\circ Q$ is reflexive.

3) Suppose $R$ and $Q$ are symmetric. Then

\[R\circ Q\text{ is symmetric }\Leftrightarrow R\circ Q=Q\circ R.\]

*S:*_s | R:br(S)
*x,y:S | u:(R∘R^-1)xy

* Notation P:=λz:S.Rxz∧R^-1zy : S→*_p
*z:S | v:Pz
*a_3:=prod-term (S,R,R^-1,y,z,x,a_2,a_1) : (R∘R^-1)yx
*a_4:=λz:S.λv:Pz. a_3 : (∀z:S.(Pz⇒(R∘R^-1)yx))
*a_5:=∃-el (S,P,u,(R∘R^-1)yx,a_4): (R∘R^-1)yx
*a_6:=λx,y:S.λu:(R∘R^-1)xy. a_5 : sym(S,R∘R^-1)

*S:*_s | R,Q:br(S)
*u:refl(S,R) | v:refl(S,Q)
*ux : Rxx
*vx : Qxx
*a_1:=prod-term (S,R,Q,x,x,x,ux,vx) : (R∘Q)xx
*a_2:=λx:S.a_1 : refl(S,R∘Q)

3) Here we use the proof term $sym\mhyphen criterion(S,R)$ from Theorem <ref>.3) for the second criterion of symmetry and the proof term $conv\mhyphen prod$ from
Theorem <ref>.2).

*a_1:=symcriterion(S,R) : sym(S,R)⇔(R^-1=R)
: (R^-1=R)⇒sym(S,R)
*R,Q:br(S) | u:sym(S,R) | v:sym(S,Q)
*a_6:=convprod(S,R,Q) : (R∘Q)^-1=Q^-1∘R^-1
* Notation P_1:=λK:br(S).((R∘Q)^-1=K∘R^-1) : br(S)→*_p
* Notation P_2:=λK:br(S).((R∘Q)^-1=Q∘K) : br(S)→*_p
*a_7:=eqsubs(br(S),P_1, Q^-1,Q,a_5,a_6) :
*a_8:=eqsubs(br(S),P_2, R^-1,R,a_4,a_7) :
* Notation A:=sym(S,R∘Q) : *_p
* Notation B:=(R∘Q=Q∘R) : *_p

*a_9:=a_2(R∘Q)w : (R∘Q)^-1=R∘Q
*a_10:=eqsym(br(S),(R∘Q)^-1,R∘Q,a_9) : R∘Q=(R∘Q)^-1
*a_11:=eqtrans(br(S),R∘Q,(R∘Q)^-1,Q∘R,a_10,a_8) : R∘Q=Q∘R
*a_12:=λw:A.a_11 : A⇒B

*a_13:=eqsym(br(S),R∘Q,Q∘R,w) : Q∘R=R∘Q
*a_14:=eqtrans(br(S),(R∘Q)^-1,Q∘R,R∘Q,a_8,a_13) : (R∘Q)^-1=R∘Q
*a_15:=a_3(R∘Q)a_14 : sym(S,R∘Q)
*a_16:=λw:B.a_15 : B⇒A

§ SPECIAL BINARY RELATIONS

§.§ Equivalence Relation and Partition

Invariance of equivalence relation under converse operation and intersection. Suppose $R$ and $Q$ are equivalence relations on type $S$. Then the following hold.

1) $R^{-1}$ is an equivalence relation on $S$.

2) $R\cap Q$ is  an equivalence relation on $S$.

1) can easily be derived from Theorem
<ref>.1), 2), 4) using intuitionistic logic.

2) can easily be derived from Theorem <ref>.1), 2), 4) using intuitionistic logic.

We skip the formal proofs.

Next we formalize the fact that there is a correspondence between equivalence relations on $S$ and partitions of $S$.
Equivalence classes are introduced in [8] as follows.

*S:*_s | R:br(S) | u:equivrel(S,R)
*class(S,R,u,x):={y:S | Rxy}:ps(S)
*Notation [x]_R for class(S,R,u,x)

Next we define a partition of type $S$:

*S:*_s | R:S→ps(S)

As usual, we can regard a partition $R$ as a collection $Rx\,( x\in S)$ of subsets of $S$. From this point of view, the above diagram expresses the standard two facts for a partition:

* any element of $S$ belongs to one of subsets from the collection (namely $Rx$);

* if the intersection of two subsets $Rx$ and $Ry$ is non-empty, then they coincide.

(1) implies that each subset from the collection is non-empty and that the union of all subsets from the collection is $S$.

Any equivalence relation $R$ on type $S$ is a partition of $S$ and vice versa.

The type of partitions of $S$ is $S\rightarrow ps(S)$, which is $S\rightarrow S\rightarrow *_p$, and it is the same as the type $br(S)$ of relations on $S$. The proof consists of two steps.

Step 1. Any equivalence relation is a partition.

*S:*_s | R:S→S→*_p
*a_3:=λx:S.a_2 : (∀x:S.xεX)

This proves the first part of the definition of $partition(S,R)$ and the second part was proven in [8], pg. 291.

Step 2. Any partition is an equivalence relation.

*S:*_s | R:S→S→*_p
*Notation A:=∀x:S.(xεRx)
*Notation B:=∀x,y,z:S.(zεRx⇒zεRy⇒Rx=Ry)
*a_4:=λx:S.a_3 : refl(S,R)
*x,y:S | v:Rxy
*a_5:=a_1y : (yεRy)
*a_6:=a_2xyyva_5 : Rx=Ry
*a_7:=a_1x : (xεRx)
*a_8:=eqsubs(ps(S),λZ:ps(S).xεZ,Rx,Ry,a_6,a_7) : (xεRy)
*a_9:=λx,y:S.λv:Rxy.a_8 : sym(S,R)
*x,y,z:S | v:Rxy | w:Ryz
*a_10:=a_9yzw : Rzy

*a_11:=a_2zxya_10v : Rz=Rx
*a_12:=a_1z : (zεRz)
*a_13:=eqsubs(ps(S),λZ:ps(S).zεZ,Rz,Rx,a_11,a_12) : zεRx
*a_14:=λx,y,z:S.λv:Rxy.λw:Ryz.a_13 : trans(S,R)
: equivrel(S,R)

§.§ Partial Order

Invariance of partial order under converse operation and intersection. Suppose $R$ and $Q$ are partial orders on type $S$. Then the following hold.

1) $R^{-1}$ is a partial order on $S$.

2) $R\cap Q$ is a partial order on $S$.

1) can easily be derived from Theorem
<ref>.1), 3), 4) using intuitionistic logic.

2) can easily be derived from Theorem <ref>.1), 3), 4) using intuitionistic logic.
We skip the formal proofs.

$\subseteq$ is a partial order on the power set $ps(S)$ of type $S$.

This is the formal proof.

*Notation R:=λX,Y:ps(S).X⊆Y : br(ps(S))
*Notation A:=refl(ps(S),R)
*Notation B:=antisym(ps(S),R)
*Notation C:=trans(ps(S),R)
*a_1:=λx:S.λu:(xεX).u : X⊆X
*a_2:=λX:ps(S).a_1 : A

*X,Y:ps(S) | u:X⊆Y | v:Y⊆X
*a_3:=∧in(X⊆Y,Y⊆X,u,v) : X=Y
*a_4:=λX,Y:ps(S).λu:X⊆Y.λv:Y⊆X.a_3 : B

*X,Y,Z:ps(S) | u:X⊆Y | v:Y⊆Z
*x:S | w:xεX
*a_5:=uxw : (xεY)
*a_6:=vxa_5 : (xεZ)
*a_7:=λx:S.λw:(xεX).a_6 : X⊆Z
*a_8:=λX,Y,Z:ps(S).λu:X⊆Y.λv:Y⊆Z.a_7 : C
*a_9:=∧in(A∧B, C,∧in(A,B,a_2,a_4),a_8) : A∧B∧C

§.§ Well-Ordering and Transfinite Induction

We will use the notation $\leqslant$ for partial order. In the following diagram we define the strict order $<$, the least element of a partially ordered set, and well-ordering of type $S$.

*S:*_s | ⩽:br(S) | u:partord(S,⩽)
*Definition < :=λx,y:S.(x⩽y∧(x=y))
*X:ps(S) | x:S
*Definition least(S,⩽,X,x):=xεX∧∀y:S.(yεX⇒x⩽y)
*Definition wellord(S,⩽):=partord(S,⩽)

Transfinite Induction. Suppose $\leqslant$ is a well-ordering of type $S$. Then for any predicate $P$ on $S$:

\[\forall x:S.[(\forall y:S.(y<x\Rightarrow Py)\Rightarrow Px]\Rightarrow \forall x:S.Px.\]

Here is the formal proof.

*S:*_s | ⩽:br(S) | u_1:wellord(S,⩽) | P:S→*_p
*u_2 : ∀x:S.[∀y:S.(y<x⇒Py)⇒Px]
*Notation A:=partord(S,⩽)
*Notation B:=[∀X:ps(S).(∃x:S.xεX⇒∃x:S.least(S,⩽,X,x))]
*a_1:=∧el_1(A,B,u_1) :A
*a_2:=∧el_2(A,B,u_1) :B
: refl(S,⩽)∧antisym(S,⩽)
: antisym(S,⩽)
*Notation X:=λx:S.Px : ps(S)
*a_5:=a_2Xv_1 : [∃x:S.least(S,⩽,X,x)]
*x:S | v_2:least(S,⩽,X,x)
*a_6:=∧el_1(xεX,∀y:S.(yεX⇒x⩽y),v_2) : xεX
*a_7:=∧el_2(xεX,∀y:S.(yεX⇒x⩽y),v_2) : [∀y:S.(yεX⇒x⩽y)]
*y:S | w_1:y<x
*a_8:=∧el_1(y⩽x,(x=y),w_1) : y⩽x
*a_9:=∧el_2(y⩽x,(x=y),w_1) : (x=y)
*a_12:=a_9a_11 :
*a_13:=λw_2:Py.a_12 : Py
*a_14:=doubneg(Py)a_13 : Py
*a_15:=λy:S.λw_1:y<x.a_14 : [∀y:S.(y<x⇒Py)]
*a_16:=u_2xa_15 : Px
*a_17:=a_6a_16 :
*a_18:=λx:S.λv_2:least(S,⩽, X,x).a_17 : [∀x:S.(least(S,⩽, X,x)⇒)]
*a_19:=∃el(S,λx:S.least(S,⩽, X,x),a_5,,a_18) :
*a_20:=λv_1:(∃x:S.xεX).a_19 : (∃x:S.xεX)
*a_21:=∃in(S,λz:S.zεX,x,w) : (∃z:S.zεX)
*a_22:=a_20a_21 :
*a_23:=λw:Px.a_22 : Px
*a_24:=doubneg(Px)a_23 : Px
*a_25:=λx:S.a_24 : (∀x:S.Px)

Here we used (twice) the Double Negation theorem with the proof term $doub\mhyphen neg$. This is the only place in this paper where we use the classical (not intuitionistic) logic.

§ CONCLUSION

Starting with the definitions from [8] of binary relations and properties of reflexivity, symmetry, antisymmetry, and transitivity, we formalize in the theory $\lambda D$ (the Calculus of Constructions with Definitions) criteria for these properties and prove their invariance under operations of union, intersection, composition, and taking converse. We provide a formal definition of partition and formally prove correspondence  between equivalence relations and partitions. We derive a formal proof that $\subseteq$ is a partial order on power set. Finally we formally prove the principle of transfinite inductions for a type with well-ordering.

The results can be transferred to the proof assistants that are based on
the Calculus of Constructions. Since binary relations are the abstract concepts used in many areas of mathematics, the results can be useful for further formalizations of mathematics in $\lambda D$. Our next direction of research is formalization of parts of probability theory in $\lambda D$ that we outlined in [6].

§ APPENDIX

§ PROOF OF THEOREM <REF>

*S: *_s | R:br(S)
*a_1:=λu:(R^-1)^-1xy.u : (R^-1)^-1xy⇒Rxy

*a_2:=λu:Rxy.u : Rxy⇒(R^-1)^-1xy

*a_3:=λx,y:S.a_1 : (R^-1)^-1⊆R
*a_4:=λx,y:S.a_2 : R⊆(R^-1)^-1
*a_5:=relequal (R^-1)^-1, R,a_3,a_4) : (R^-1)^-1=R

*S: *_s | R,Q:br(S)
* Notation A:=(R∘Q)^-1 :br(S)
* Notation B:=Q^-1∘R^-1 :br(S)
* Notation P_1:=λz:S.Ryz∧Qzx : S→*_p
* Notation P_2:=λz:S.Q^-1xz∧R^-1zy : S→*_p
*z:S | v:P_1z
*a_3:=prod-term (S,Q^-1,R^-1,x,z,y,a_2,a_1) : (Q^-1∘R^-1)xy
*a_4:=λz:S.λv:P_1z.a_3 : (∀z:S.(P_1z ⇒Bxy))
*a_5:=∃-el (S,P_1,u,Bxy,a_4):Bxy
λu:Axy.a_5 : A⊆B

*x,y:S | u:Bxy
*z:S | v:P_2z
*a_9:=prod-term (S,R,Q,y,z,x,a_8,a_7) : (R∘Q)yx
*a_10:=λz:S.λv:P_2z.a_9 : (∀z:S.(P_2z ⇒Axy))
*a_11:=∃-el (S,P_2,u,Axy,a_10):Axy
λu:Bxy.a_11 : B⊆A
*convprod(S,R,Q):=relequal (A,B,a_6,a_12) : (R∘Q)^-1=Q^-1∘R^-1

*S: *_s | R,Q:br(S)
* Notation A:=(R∩Q)^-1 :br(S)
* Notation B:=R^-1∩Q^-1 :br(S)
*x,y:S | u:Axy
* u:Ryx∧Qyx
*a_4:=λx,y:S.λu:Axy.a_3 : A⊆B

*x,y:S | u:Bxy
* u:R^-1xy∧Q^-1xy
*a_8:=λx,y:S.λu:Bxy.a_7 : B⊆A
*a_9:=relequal (A,B,a_4,a_8):(R∩Q)^-1= R^-1∩Q^-1

*S: *_s | R,Q:br(S)
* Notation A:=(R∪Q)^-1 :br(S)
* Notation B:=R^-1∪Q^-1 :br(S)
*x,y:S | u:Axy
* u:(R∪Q)yx
* u:Ryx∨Qyx
*a_2:=λv:Ryx.a_1 : Ryx⇒Bxy

*a_4:=λv:Qyx.a_3 : Qyx⇒Bxy

*a_5:=∨-el (Ryx,Qyx,Bxy,u,a_2,a_4) : Bxy
*a_6:=λx,y:S.λu:Axy.a_5 : A⊆B

*x,y:S | u:Bxy
* u:R^-1xy∨Q^-1xy
*a_8:=λv:R^-1xy.a_7 : R^-1xy⇒Axy

*a_10:=λv:Q^-1xy.a_9 : Q^-1xy⇒Axy

*a_11:=∨-el (R^-1xy,Q^-1xy,Axy,u,a_8,a_10) : Axy
*a_12:=λx,y:S.λu:Bxy.a_11 : B⊆A
*a_13:=relequal (A,B,a_6,a_12) : (R∪Q)^-1= R^-1∪Q^-1

*S: *_s | R,P,Q:br(S)
* Notation A:=R∘(P∪Q) :br(S)
* Notation B:=R∘P∪R∘Q :br(S)
* Notation P_0:=λz:S.Rxz∧(P∪Q)zy : S→*_p
*z:S | v:P_0z
*a_3:=prod-term (S,R,P,x,z,y,a_1,w) : (R∘P)xy
*a_5:=λw:Pzy.a_4 : Pzy⇒Bxy
*a_6:=prod-term (S,R,Q,x,z,y,a_1,w) : (R∘Q)xy
*a_7:=∨-in _2((R∘P)xy,(R∘Q)xy,a_6):Bxy
*a_8:=λw:Qzy.a_7 : Qzy⇒Bxy
*a_9:=∨-el (Pzy,Qzy,Bxy,a_2,a_5,a_8):Bxy
*a_10:=λz:S.λv:P_0z.a_9 : (∀z:S.(P_0z ⇒Bxy))
*a_11:=∃-el (S,P_0,u,Bxy,a_10):Bxy
λu:Axy.a_11 : A⊆B

* Notation P_1:=λz:S.Rxz∧Pzy : S→*_p
* Notation P_2:=λz:S.Rxz∧Qzy : S→*_p
*z:S | w:P_1z
*a_13:=∧el_1(Rxz,Pzy,w) : Rxz
*a_14:=∧el_2(Rxz,Pzy,w) : Pzy
*a_16:=prod-term (S,R,(P∪Q),x,z,y,a_13,a_15) : Axy
*a_17:=λz:S.λw:P_1z.a_16 : (∀z:S.(P_1z⇒Axy))
*a_18:=∃-el (S,P_1,v,Axy,a_17):Axy
*a_19:=λv:(R∘P)xy.a_18 : ((R∘P)xy⇒Axy)

*z:S | w:P_2z
*a_20:=∧-el_1(Rxz,Qzy,w) : Rxz
*a_21:=∧-el_2(Rxz,Qzy,w) : Qzy
*a_23:=prod-term (S,R,(P∪Q),x,z,y,a_20,a_22) : Axy
*a_24:=λz:S.λw:P_2z.a_23 : (∀z:S.(P_2z⇒Axy))
*a_25:=∃-el (S,P_2,v,Axy,a_24):Axy
*a_26:=λv:(R∘Q)xy.a_25 : ((R∘Q)xy⇒Axy)
*a_27:=∨-el((R∘P)xy,(R∘Q)xy, Axy,u,a_19, a_26) : Axy
*[2]a_28:=λx,y:S.λu:Bxy.a_27 : B⊆A
*a_29:=relequal (A,B,a_12,a_28) : R∘(P∪Q)=R∘P∪R∘Q

6) is proven similarly to 5).

*S: *_s | R,P,Q:br(S)
* Notation A:=R∘(P∩Q) :br(S)
* Notation B:=R∘P∩R∘Q :br(S)
* Notation P:=λz:S.Rxz∧(P∩Q)zy : *_p
* u:(∃z:S.Pz)
*z:S | v:Pz
*a_5:=prod-term (S,R,P,x,z,y,a_1,a_3) : (R∘P)xy
*a_6:=prod-term (S,R,Q,x,z,y,a_1,a_4) : (R∘Q)xy
*a_7:=∧-in ((R∘P)xy,(R∘Q)xy,a_5,a_6) : Bxy
*a_8:=λz:S.λv:Pz.a_7 : (∀z:S.(Pz⇒Bxy))
*a_9:=∃-el (S,P,u,Bxy,a_8):Bxy
*[2]a_10:=λx,y:S.λu:Axy.a_9 : R∘(P∩Q)⊆R∘P∩R∘Q

8) is proven similarly to 7).

*S: *_s | R,P,Q:br(S)
* Notation A:=(R∘P)∘Q :br(S)
* Notation B:=R∘(P∘Q) :br(S)
* Notation P_1(x,y):=λz:S.(R∘P)xz∧Qzy : S→*_p
* Notation P_2(x,y):=λz:S.Rxz∧(P∘Q)zy : S→*_p
* Notation P_3(x,y):=λz:S.Rxz∧Pzy : S→*_p
* Notation P_4(x,y):=λz:S.Pxz∧Qzy : S→*_p
*x,y:S | u:Axy
* u:(∃z:S.P_1(x,y)z)
*z:S | v:P_1(x,y)z

*z_1:S | w:P_3(x,z)z_1
*a_5:=prod-term (S,P,Q,z_1,z,y,a_4,a_2) : (P∘Q)z_1y
*a_6:=prod-term (S,R,(P∘Q),x,z_1,y,a_3,a_5) : Bxy
*a_7:=λz_1:S.λw:P_3(x,z)z_1.a_6 : (∀z_1:S.(P_3(x,z)z_1⇒Bxy))
*a_8:=∃-el (S,P_3(x,z),a_1,Bxy,a_7):Bxy
*a_9:=λz:S.λv:P_1(x,y)z.a_8 : (∀z:S.(P_1(x,y)z⇒Bxy))
*a_10:=∃-el (S,P_1(x,y),u,Bxy,a_9):Bxy
*a_11:=λx,y:S.λu:Axy.a_10 : A⊆B

*x,y:S | u:Bxy
* u:(∃z:S.P_2(x,y)z)
*z:S | v:P_2(x,y)z

*z_1:S | w:P_4(z,y)z_1
*a_16:=prod-term (S,R,P,x,z,z_1,a_12,a_14) : (R∘P)xz_1
*a_17:=prod-term (S,R∘P,Q,x,z_1,y,a_16,a_15) : Axy
*a_18:=λz_1:S.λw:P_4(z,y)z_1.a_17 : (∀z_1:S.(P_4(z,y)z_1⇒Axy))
*a_19:=∃-el (S,P_4(z,y),a_13,Axy,a_18):Axy
*a_20:=λz:S.λv:P_2(x,y)z.a_19 : (∀z:S.(P_2(x,y)z⇒Axy))
*a_21:=∃-el (S,P_2(x,y),u,Axy,a_20):Axy
*a_22:=λx,y:S.λu:Bxy.a_21 : B⊆A
*a_23:=relequal(A,B,a_11,a_22) : (R∘P)∘Q=R∘(P∘Q)

§ PROOF OF THEOREM <REF>

Each statement here is a bi-implication, so we use the proof term bi-impl from Lemma <ref>.

*S:*_s | R:br(S)
* Notation A:=refl(S,R):*_p
* Notation B:=id_s⊆R:*_p
*x,y:S | v:(id_S)xy
* Notation  P:=λz:S.Rxz : S→*_p
*a_1:=eq$-$subs(S,P,x,y,v,ux) : Py
*a_2:=λx,y:S.λv:(id_S)xy.a_1 : (id_S⊆R)
*a_3:=λu:A.a_2 : (A⇒B)

*a_4:=eq$-$refl(S,x) : x=_Sx
*a_5:=uxxa_4 : Rxx
*a_6:=λx:S.a_5 : (∀x:S.Rxx)
*a_7:=λu:B.a_6 : (B⇒A)
*a_8:=biimpl (A,B,a_3,a_7) : refl(S,R)⇔id_s⊆R

2) and 3) are proven together as follows.

*S:*_s | R:br(S)
* Notation A:=sym(S,R):*_p
* Notation B:=R^-1⊆R:*_p
* Notation C:=R^-1= R:*_p
*x,y:S | v:R^-1xy
* uyx:(Ryx⇒Rxy)
*a_1:=uyxv : Rxy
*a_2:=λx,y:S.λu:R^-1xy.a_1 : (R^-1⊆R)

*x,y:S | v:Rxy
* uxy:(Rxy⇒Ryx)
*a_3:=uxyv : Ryx
*a_4:=λx,y:S.λu:Rxy.a_3 : (R⊆R^-1)
*a_5:=relequal(S,R^-1,R,a_2,a_4) : R^-1=R
*a_6:=λu:A.a_2 : A⇒B
*a_7:=λu:A.a_5 : A⇒C

*x,y:S | v:Rxy
*a_8:=uyxv : Ryx
*a_9:=λx,y:S.λv:Rxy.a_8 : sym(S,R)
*a_10:=λu:B.a_8 : (B⇒A)

*a_12:=a_10a_11 : A
*a_13:=λu:C.a_12 : (C⇒A)
*a_14:=biimpl (A,B,a_6,a_10) : sym(S,R)⇔R^-1⊆R
*symcriterion(S,R):=biimpl (A,C,a_7,a_13) : sym(S,R)⇔R^-1=R

*S:*_s | R:br(S)
* Notation A:=antisym(S,R):*_p
* Notation B:=R∩R^-1⊆id_S:*_p

*x,y:S | v:(R∩R^-1)xy
*a_3:=uxya_2a_1 : (x=y)
*a_4:=λx,y:S.λv:(R∩R^-1)xy.a_3 : (R∩R^-1⊆id_S)
*a_5:=λu:A.a_4 : (A⇒B)

*x,y:S | v:Rxy | w:Ryx
*a_7:=uxya_6 :  (id_S)xy
*a_8:=λx,y:S.λv:Rxy.λw:Ryx. a_7 : antisym(S,R)
*a_9:=λu:B.a_8 : (B⇒A)

*S:*_s | R:br(S)
* Notation A:=trans(S,R):*_p
* Notation B:=R∘R⊆R:*_p
* Notation P:=λz:S.Rxz∧Rzy : S→*_p
*z:S | w:Pz
*a_3:=uxzya_1a_2 : Rxy
*a_4:=λz:S.λw:Pz.a_3 : (∀z:S.(Pz ⇒Rxy))
*a_5:=∃-el (S,P,v,Rxy,a_4) : Rxy
*[2]a_6:=λx,y:S.λv:(R∘R)xy.a_5 : (R∘R⊆R)
*a_7:=λu:A.a_6 : (A⇒B)

*x,y,z:S | v:Rxy | w:Ryz
*a_8:=prodterm(S,R,R,x,y,z,v,w) : (R∘R)xz
*a_9:=uxz : ((R∘R)xz⇒Rxz)
*a_10:=a_9a_8 : Rxz
*a_11:=λx,y,z:S.λv:Rxy.λw:Ryz.a_10 : trans(S,R)
*a_12:=λu:B.a_11 : (B⇒A)

[1]
H. Barendregt.
Lambda calculi with types.
In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–309. Oxford
University Press, 1992.

[2]
A. Church.
A formulation of the simple theory of types.
Journal of Symbolic Logic, 5(2):56–68, 1940.

[3]
T. Coquand and G. Huet.
The calculus of constructions.
Information and Computation, 76(2-3):95–120, 1988.

[4]
F. B. Fitch.
Symbolic Logic.
Ronald Press Company, 1952.
ISBN: 978-0826030955.

[5]
S. Jaśkowski.
On the rules of suppositions in formal logic.
Oxford University Press, 1967.
ISBN: 978-0198243045.

[6]
F. Kachapova.
Formalizing probability concepts in a type theory.
Journal of Mathematics and Statistics, 14(1):209–218, 2018.

[7]
P. Martin-Löf.
Intuitionistic type theory: Notes by Giovanni Sambin.
Prometeus Books, 1985.
ISBN: 978-8870881059.

[8]
R. Nederpelt and H. Geuvers.
Type Theory and Formal Proof.
Cambridge University Press, 2014.
ISBN: 978-1-107-03650-5.

[9]
R. Nederpelt and F. Kamareddine.
Logical Reasoning: A First Course.
College Publications, 2 edition, 2011.
ISBN: 978-0954300678.

[10]
B. Russell.
The Principles of Mathematics.
W. W. Norton & Company, 1996.
ISBN: 978-0393314045.