Formalization of fractional calculus and fractional order PI controller

Abstract

There are three kinds of commonly used fractional calculus definitions. And they are Grünwald-Letnikov (GL) calculus, Riemann-Liouville (RL) calculus, and Caputo calculus. Relationship among GL, RL and Caputo calculus is the basis for formalization of fractional order control systems. Higher order logic theorem proving method is applied to construe the relationship in this paper. The essential differences among these three definitions are introduced firstly. Relationship between GL calculus and Caputo calculus is verified by a higher order logic theorem prover. And then the relationship between RL definition and Caputo calculus is also formalized in this paper. The study provides a good research foundation for formal verification of fractional order PI controller. The fractional order PI controller in a humanoid robot system has been verified based on the formalization of fractional calculus. Results show that fractional order PI controller is very effective and reliable. And it also shows that the formalization of fractional calculus definitions is correct. It provides the research method for formalization of fractional order control systems.

Keywords

Fractional calculus theorem proving higher order logic formalization

1. Introduction

Fractional calculus is traceable in 1695 [1]. And it has a history of more than three hundred years. Fractional calculus extends the order of integer order calculus from integer to non-integer. Fractional order models based on fractional calculus can describe nature characteristics and property behavior of real-time systems more accurately. At present, fractional calculus has been widely used in various fields [2, 3, 4, 5, 6, 7]. It can be used to represent dynamic course of the system which cannot be described accurately by integer order system. Research has shown that fractional calculus can more accurately depict the attributive character of actual systems [8, 9, 10, 11, 12].

There are three kinds of commonly used definitions of fractional calculus. They are Grünwald-Letnikov (GL) calculus, Riemann-Liouville (RL) calculus, and Caputo calculus [13]. Relationship among GL, RL and Caputo calculus definitions is very important. And the relationship is the basis for fractional order control systems. Fractional order PI controller is one of fractional order PID controller. This relationship should have a complete proof. That will provide a firm foundation for correctness of fractional order systems. The complete formalization of fractional order PID controller is the guarantee of system operation.

The relationship can be verified by theoretical paper-and-pencil proof techniques. But traditional manpower analysis method is very easy to mistake due to the required complex calculations. The most commonly used analysis method for fractional calculus is simulation method which is on the basis of numerical computation. The simulation method cannot give accurate results. Therefore, the system is prone to error. Theorem proving has been successfully used in software and hardware [14]. Theorem proving provides a viable underpinning for an accurate analysis of the relationship among three fractional calculus definitions. Mathematical models of fractional calculus definitions can be converted into logical models in theorem proving. Logically it is verified to be correct. Siddique and Hasan [15] has formalized Gamma function and RL calculus. Shi et al. [16] has formalized GL calculus. In [17], we have established the formalization of Caputo calculus definition. And in this paper the relationship among three kinds of fractional calculus definitions will be verified using higher order logic theorem prover (HOL).

Higher Order Logic (HOL) system is used to the formal study on fractional order theory in this paper. HOL is an interactive theorem prover [18]. The formal logic is interfaced to a general purpose programming language in which terms and theorems of the logic can be denoted, proof strategies expressed and applied, and logical theories developed. The version of higher order logic used in HOL is predicate calculus with terms from the typed lambda calculus. This was originally developed as a foundation for mathematics. The primary application area of HOL was initially intended to be the specification and verification of hardware designs. However, the logic does not restrict applications to hardware. HOL has been applied to many other areas. The HOL syntax contains syntactic categories of types and terms whose elements are intended to denote respectively certain sets and elements of sets.

The rest of the paper is organized as follows: Section 2 presents formalizations of the relationship among three fractional calculus definitions in HOL. Section 3 proposes formalizations of fractional PI controller based on fractional calculus. Conclusions are drawn in Section 4.

2. Formalization of relationship

GL calculus, RL calculus and Caputo calculus are the most commonly used fractional calculus definitions. These definitions can be consistent in certain conditions. And they also have different characteristics, respectively [19, 20]. GL calculus extends calculus concept from integer to any real number based on integer higher order derivatives. It is suitable for numerical calculations. For numerical calculation of fractional differential equations, researchers have proposed many approaches based on GL calculus [21]. These methods have greatly improved the computational accuracy and complexity. GL calculus definition also has greatly contributed to the practical application of fractional order calculus. However, GL calculus is complex and this definition has a strong premise condition. GL calculus will have a certain limitation for practical problems. In 1872, Letnikov proposed another definition which can weaken the premise condition. That is RL calculus. RL calculus defines fractional calculus by Cauchy’s integral formula and general derivative. It is defined as the differential integral form which makes the mathematical analysis of fractional calculus become easier. RL calculus is good at the calculation for space fractional order derivative. Compared with GL calculus, RL calculus is more commonly used. But there is a little critical requirement that the function must be continuous and integrable in RL calculus. And the application of RL calculus is still restricted because the initial value lacks physical meaning [22]. In order to solve this problem, Caputo calculus was proposed [23]. Caputo calculus can facilitate the modeling of actual problems. Caputo calculus is more able to reflect the feature that fractional calculus is the expansion of integer order calculus. Therefore, Caputo calculus is more widely used in the modeling of actual problems.

When the initial value is zero, GL calculus and Caputo calculus are equivalent. And RL calculus and Caputo calculus are equivalent when the original function $f(t)$ is $(\lfloor v\rfloor+1)^{\text{th}}$ derivable and all of the derivatives are zero, where $v$ is the fractional order. Relationship between GL calculus and Caputo calculus is as follows:

${}_{a}^{C}D_{t}^{\alpha}f(t)={}_{\phantom{G}a}^{GL}D_{t}^{\alpha}f(t)-\frac{f(% a)t^{-\alpha}}{\Gamma(1-\alpha)}$ (1)

Where $f(a)$ is the value of function $f$ in $a$ . And $a$ is real number. And $\Gamma(1-\alpha)$ is a generalized factorial with the variable $(1-\alpha)$ . This relation can be formalized in HOL as shown below.

Definition 1 Formalization of relationship between GL calculus and Caputo calculus

val FRAC_C_GL =

$|-\forall$ f v a t b.(frac_c f v a t) b = frac_gl f v a b t - f a * t rpow (-v)/Gamma (1-v)

Where, F RAC C GL is a defined name that represents the relationship between two definitions. And f rac c represents Caputo calculus. f rac gl represents GL calculus. And f a is the value of the function f with lower limit a. And Gamma represents Gamma function. The variable is the real (1-v). When the initial value of function is zero, two fractional calculus definitions are equivalent. This can be verified in HOL.

Theorem 1 Consistency of GL calculus and Caputo calculus

FRAC_C_GL_EQ = $|-\forall$ f v a t b.(f a = 0) ==> ((frac_c f v a t) b = frac_cal f v a b t)

Here, $fa=0$ is the necessary condition of the consistency. In HOL, $f a$ shows the value of function $f$ in $a$ . When the value is zero, the consistency can be verified gradually in HOL.

Relationship between RL calculus and Caputo calculus is as following:

${}_{a}^{C}D_{t}^{\alpha}f(t)={}_{\phantom{R}a}^{RL}D_{t}^{\alpha}f(t)-\sum% \limits_{{k}=0}^{n-1}{\frac{(t-a)^{k-\alpha}}{\Gamma(k-\alpha+1)}}f^{k}(t)$ (2)

This relation is formalized in HOL as follows:

Definition 2 Formalization of relationship between RL calculus and Caputo calculus

val FRAC_C_RL = $|-\forall$ f v a t. frac_c f v a t = frac_rl f v a t - sum(0,flr v) ( $\lambda$ (k:num). 1/Gamma(&k - v + 1) * (t-a) rpow (&k - v) * n_order_deriv k f t)

Here, FRAC_C_RL is the name that represents the relationship between Caputo calculus and RL calculus. And frac_rl represents RL calculus. And $\textit{sum}(0,\textit{flr v})g$ shows summation function. It represents the sum of function $g$ from $0$ to flr v. And $(t-a)\textit{rpow}({\&}k-v)$ shows $(t-a)^{k-\alpha}$ in HOL. And $n{\_}\textit{order}{\_}\textit{deriv k f a}$ is the value of the $k$ th order derivative of function $f$ in $a$ . Where $k$ is an integer, and it represents an integer order calculus.

We should also be able to deduce that two definitions are consistent when function $f(t)$ has $(m+1)$ order derivative and $m$ is larger than $\lfloor\alpha\rfloor=n-1$ and $f^{k}(a)=0(k=0,1,2,\ldots,n-1)$ . This property can be verified in HOL is shown as follows:

Theorem 2 Consistency of RL calculus and Caputo calculus

FRAC_C_RL_QE =

$|-\forall$ f v a t. (( $\forall$ k. k <= flr v + 1 ==> ( $\lambda$ x.n_order_derivk f x) differentiable x)/ $\backslash$

( $\forall$ k. n_order_deriv k f a = 0)) ==> (frac_c f v a t = frac_rl f v a t)

Formal difficulty is how to construct the model in HOL. In prerequisite, function $f(t)$ has $(m+1)$ order derivative. That is to say, when any integer $k$ is less than or equal to $(m+1)$ , function $f(t)$ must have $k$ order derivative. This condition can be verified in HOL as ( $\forall$ k. k <= flr v+1==> ( $\lambda$ x.n_order_derivk f x) differentiable x). Where $v$ is the order and it can be any real number. The relation between $m$ and $v$ is $m=\lfloor v\rfloor$ . In HOL, f differentiable x indicates that $f$ is differentiable to $x$ . In this Theorem, ( $\forall$ k. k <= flr v + 1) indicates the first prerequisite. The second prerequisite is ( $\forall$ k. n_order_deriv k f a = 0). And it shows that the initial value for the $k$ th derivative of function $f$ is zero. With these two conditions, RL calculus and Caputo calculus are equivalent.

Because high order logic formalized validation is completeness validation method. The results of theorem proving are also precise and perfect. Then fractional PI controller has been formalized based on fractional calculus and some of the properties [24].

3. Formalization of fractional PI controller

Fractional order PI controller is one of fractional order PID controller [25]. During the robot’s autonomous positioning and navigation, fractional PI controller can reduce the error between actual position and estimate position [26]. This method is very effective and reliable in the NAO humanoid robot navigation. In [26], the coefficient of fractional PI controller, K_p $=$ 0.7, K_i $=$ 0.2, alpha $=-$ 0.1, respectively. Higher-order logic theorem proving formal analysis of fractional order PI controller is done in this section. Main process is shown in the figure below.

Mathematical expressions of fractional order PI controller in the time domain and frequency domain have:

$\displaystyle u(t)=K_{p}e(t)+K_{i}[D^{-\alpha}e(t)],(\alpha>0)$ (3) $\displaystyle C(s)=\frac{U(s)}{E(s)}=K_{p}+\frac{K_{i}}{s^{\alpha}}$ (4)

The higher-order logic formalization of Eq. (3) is as follows:

Definition 3 Formalization of fractional PI controller in the time domain

val FOPI_controller_time_domain =

$|-\forall$ u_t_pi K_p e_t K_i lambda t. u_t_pi K_p e_t K_i lambda t

= K_p * e_t t + K_i * frac_c e_t (-lambda) 0 t

Here, u_t_pi is output of fractional PI controller; e_t is input; K_p is the proportionality coefficient; K_i is integration coefficient; and lambda is order of integration. The higher-order logic formalization of Eq. (4) is as follows:

Definition 4 Formalization of fractional PI controller in the frequency domain

Figure 1.

Formal analysis of fractional order PI controller.

val FOPI_controller_frequency_domain =

$|-\forall$ C_s_pi s K_p K_i alpha.C_s_pi s (K_p:real) (K_i:real) alpha

= K_p + K_i * s complex_rpow (-alpha)

Where, C_s_pi is the transfer function. (s complex_rpow v) denotes power operation when bottom number is complex number. And the higher-order logic formalization is:

Definition 5 Formalization of power operation based on complex bottom number

val complex_rpow =

$|$ - (z:complex) complex_rpow (x:real) = exp (complex_scalar_lmul x (complex_ln z))

Here complex_ln represents natural logarithm function based on complex number. And its mathematical expressions is $z=re^{i\theta}$ . According to the nature of natural logarithm, there is $\ln z=\ln(re^{i\theta})=\ln r+\ln e^{i\theta}=\ln r+i\theta$ . And the formalization of natural logarithm is:

Definition 6 Formalization of natural logarithm based on complex number

val complex_ln =

$|$ - complex_ln (z:complex) =

(ln (modu z),0) + (complex_scalar_rmul (0:real,1:real) (arg z))

Based on these formalization definitions and fractional calculus, fractional PI controller in [26] can be verified in HOL. Firstly, linearity of fractional PI controller is verified.

Theorem 3 Linearity of fractional PI controller

$|-\forall$ (e_t_1:real->real) (e_t_2:real->real) (t:real) (k:real) (l:real) (v:real) (a:real) (t:real) (n:num) (p:real) (q:real).

(( $\forall$ e_t_1 e_t_2 v a t n p q l. (frac_c_exists e_t_1 v a t n l)

/ $\backslash$ (frac_c_exists e_t_2 v a t n l)

/ $\backslash$ (frac_c_exists( $\lambda$ t.(k:real) * (e_t_1 t):real) v a t n l)

/ $\backslash$ (frac_c_exists ( $\lambda$ t. (l:real) * (e_t_2 t):real) v a t n l))

/ $\backslash$ (u_t_pi_1 0.7 e_t_1 0.2 0.1 t = 0.7 * e_t_1 t + 0.2 * frac_c e_t_1 (-0.1) 0 t)

/ $\backslash$ (u_t_pi_2 0.7 e_t_2 0.2 0.1 t = 0.7 * e_t_2 t + 0.2 * frac_c e_t_2 (-0.1) 0 t))

==> (u_t_pi 0.7 (( $\lambda$ t.(k * e_t_1 t + l * e_t_2 t)):real->real) 0.2 0.1 t

= k * (u_t_pi_1 0.7 e_t_1 0.2 0.1 t) + l * (u_t_pi_2 0.7 e_t_2 0.2 0.1 t))

Fractional order PI controller can reduce error and improve the precision. Then the fractional order PI controller can be validated in HOL.

Theorem 4 Stability of fractional PI controller

$|$ - 0 < t / $\backslash$ ( $\forall$ a t n l v. frac_c_exists (unit_imp t) v a t n l)

==> (lim( $\lambda$ (n:num). (u_t_pi (0.7) ((unit_imp (t:real)):real->real) (0.2) (0.1) (&n)))

= (0:real))

Firstly, object function is simplified by above formalization definitions in HOL. Then original target is divided into two subgoals. For the first subgoal, strategy METIS_TAC can be used during the verification. Another subgoal can be simplified by fractional calculus formalization definition. Goal is verified by Theorems and Strategy SELECT_ELIM_TAC and CONJ_TAC.

4. Conclusions

High order logic formalized validation is a formal verification method. The formalization process is intuitive and mathematic. Based on theorem prover HOL, the relationship among three fractional calculus definitions is verified. The relationship among three fractional calculus definitions is the theoretical bases for extensive application of fractional order systems. Therefore, formalizations of the relationship are the critical work in this paper. Then fractional PI controller is formalized based on formalized. The achievements will provide a theoretical basis for the higher order logic formalized analysis of fractional order systems.

Footnotes

Acknowledgments

This work was supported by the National Natural Science Foundation of China (61862062, 6110 4035).

References

Zhao

C.N.

Y.S.

and Lu

, Fractional system analysis and design, National Defence Industry Press, 2011.

Shikaa

and Vinod

, Time-fractional diffusion model on dynamical effect of dendritic cells on HIV pathogenesis, Journal of Computational Methods in Sciences and Engineering 18(1) (2018), 193–212.

Muhammad

Hamood

U.R.

and Muzammal

, Computational examples of a class of fractional order nonlinear evolution equations using modified extended direct algebraic method, Journal of Computational Methods in Sciences and Engineering 15(3) (2015), 359–365.

Yang

H.Y.

Zhu

X.L.

and Cao

K.C.

, Distributed coordination of fractional order multi-agent systems with communication delays, Fractional Calculus and Applied Analysis 17(1) (2014), 23–37.

Liu

D.Y.

et al., Non-asymptotic fractional order differentiator for a class of fractional order linear systems, Automatica 78 (2017), 61–71.

Hajipour

and Baleanu

, On the adaptive sliding mode controller for a hyperchaotic fractional-order financial system, Physica A: Statistical Mechanics and its Applications 497 (2018), 139–153.

Khan

and Tyagi

, Fractional order disturbance observer based adaptive sliding mode synchronization of commensurate fractional order Genesio-Tesi system, AEU – International Journal of Electronics and Communications 82 (2017), 346–357.

Lehaibi

and Eman

A.N.

, Two-temperature generalized thermoelasticity with fractional order strain of an infinite body with a spherical cavity, Journal of Computational Methods in Sciences and Engineering 18(4) (2018), 1055–1066.

Liao

G.K.

et al., Investigation on the viscoelastic behavior of an fe-base bulk amorphous alloys based on the fractional order rheological model, Acta Physica Sinica 64(13) (2015), 1361–1368.

10.

Yan

L.M.

et al., Transmission lines modeling method based on fractional order calculus theory, Transactions of China Electrotechnical Socirty 29(9) (2014), 260–268.

11.

H.F.

Z.T.

and Mao

C.L.

, Fractional differential and variational method for image fusion and super-resolution, Neurocomputing 171 (2016), 138–148.

12.

Heremans

Suykens

J.A.K.

and Orshoven

J.V.

, The effect of imposing ‘fractional abundance constraints’ onto the multilayer perceptron for sub-pixel land cover classification, International Journal of Applied Earth Observation and Geoinformation 44 (2016), 226–238.

13.

Podlubny

, Fractional differential equations, Academic press, 1999.

14.

Harrison

, Handbook of practical logic and automated reasoning, Cambridge University Press, Cambridge, 2009.

15.

Siddique

and Hasan

, Formal analysis of fractional order systems in HOL, Formal Methods in Computer-Aided Design (2011), 163–170.

16.

Shi

L.K.

et al., Formalization of real binomial coefficient in HOL4, Computer Science 41(2) (2014), 15–18.

17.

S.S.

et al., Research on the higher-order logic formalization of fractance element, IEEE/CAA Journal of Automatica Sinica 13(9) (2016), 248–256.

18.

Harrison

, Theorem proving with the real numbers, Springer-Verlag, 1998.

19.

Caputo

and Fabrizio

, A new definition of fractional derivative without singular kernel, Progress on Fractional Differentiation and Applications 1 (2015), 73–85.

20.

Losada

and Nieto

J.J.

, Properties of a new fractional derivative without singular kernel, Progress on Fractional Differentiation and Applications 1 (2015), 87–92.

21.

MacDonald

C.L.

et al., Efficient computation of the Grünwald-Letnikov fractional diffusion derivative using adaptive time step memory, Journal of Computational Physics 297 (2015), 221–236.

22.

Wang

J.F.

, The analysis of control performance for fractional-order systems, Electronic Industry Press, 2010.

23.

Chen

Sun

H.G.

and Li

X.C.

, Fractional derivative model of mechanical and engineering problems, Science Press, 2010.

24.

Zhao

C.N.

et al., Formal modeling and verification of fractional order linear systems, ISA Transactions 62 (2016), 87–93.

25.

Wang

Liang

and Wang

, GA PID control research in inverter motor speed governing system, Journal of Computational Methods in Sciences and Engineering (2018), 1–8.

26.

Wen

et al., The study of fractional order controller with SLAM in the humanoid robot, Advances in Mathematical Physics 4 (2014), 57–66.