Mechanized Mathematics and Its Applications, Works in Progress

Symmetrical Piecewise Linear Functions

Regular Paper

絶対値関数で表される左右対称な区分型線形関数の性質
Properties of Symmetrical Piecewise Linear Functions
Composed by Absolute Value Function
三石 貴志 1,*Takashi Mitsuishi1,*
1 長野大学企業情報学部
Faculty of Business and Informatics, Nagano University,
Shimonogo 658-1, Ueda, Japan* takashi-mitsuishi@nagano.ac.jp
Proof checked by Mizar Version: 8.1.12 and MML Version: 5.75.1447
Received: January 16, 2024. Accepted: March 15, 2024.

Abstract
In this paper, some mathematical properties about piecewise linear functions areformalized. The focused piecewise linear functions are symmetrical and composed byabsolute function. It is formalized that the membership functions of isosceles triangle type and isosceles trapezoid type can be constructed by absolute value functions.
Moreover it is proved and formalized that the centroids of the composite function of
two continuous functions are the weighted averages of the areas and centroids of thefunctions that compose them.

1

はじめに筆者は前稿 [1] において，区分的線形関数に関する形式化を行った．区分的線形関数とは，複数の線形関数が連結した合成関数であり，直観的な表現をすればグラフが折れ線である関数のことをいう．ファジィ推論に用いられる IF-THEN ルールを構成するファジィ集合のメンバシップ関数は通常，簡単な計算のために前件部および後件部ともに三角形か台形の形をしたものが用いられる．そしてさらにそれらは左右対称である．また，L-R
ファジィ数を表すメンバシップ関数も簡単のために二等辺三角形型等を用いる場合がある [2] [3] [4]．一部 z 型や s 型が用いられる場合もあるが，それはメンバシップ関数値が1 となる前件部変数が定義域のいわゆる端の部分に存在しているためである．左右対称性が必要とされているというよりむしろ非対称であることに意味がないためと考えられる．

MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

1/8

Mechanized Mathematics and Its Applications, Works in Progress

Symmetrical Piecewise Linear Functions

そこで本研究は，左右対称な二等辺三角形型メンバシップ関数および等脚台形型メンバシップ関数を絶対値関数と最小（大）値関数によって表す方法を形式化した．三角形型および台形型メンバシップ関数はこれまでに [5] で定義されている．これらとの互換性に関して，数学的諸性質を形式化した．
後半の節では，[6] によって定義した重心法（Centroid method）による 2 つの連続関数による合成関数の重心値に関する定理の形式化について述べている．2 つの連続関数がある一点で接続した関数について，その重心は 2 つの関数の重心と面積の加重平均となっていることを証明して形式化した．

絶対値関数による二等辺三角形型関数および等脚台形型

2関数
2.1

絶対値関数と対称性

以下の式 (1) および図 1 で表される絶対値関数および最大奇関数の合成関数 f1 は頂点の座標が (a, b) で，横軸上の 2 点 (a − c, 0) および (a + c, 0) を結ぶ線分が底辺である二等辺三角形型の関数である．ただし，区間 [a − c, a + c] 以外では 0 をとる．

b(x − a)f1 (x) = max 0, b −cb
(1)

bd00

図 1. Absolute value function f1 and isoaceles trapezoidal function f2
この関数を用いて本アーティクルでは，図 1 右の等脚台形型関数 f2 を以下のように定義した．

Listing 1. FUZZY 8:35
theorem :: FUZZY 8:35
for a,b,c,d be Real, f be Function of REAL,REAL stb > 0 & c > 0 & d > 0 & d < b & ( for x be Real holds f.x = min(d, max(0, b − |. b∗(x−a)/c .|)) )holds f | [.a−c,a+c.] = AﬃneMap (b/c,b−a∗b/c) | [. a−c, a+(d−b)/(b/c) .]+∗ AﬃneMap (0,d) | [. a+(d−b)/(b/c),a+(b−d)/(b/c) .]+∗ AﬃneMap (−b/c,b+a∗b/c) | [.a+(b−d)/(b/c), a+c.];

通常の数式では以下の式 (2) で記述される．

MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

2/8

Mechanized Mathematics and Its Applications, Works in Progressbabcx + b − cdf2 (x) =
− cb x + b + abc0Symmetrical Piecewise Linear Functionsx ∈ [a − c, a + c(d−b)]
bx ∈ [a + c(d−b), a + c(b−d)]bb(2)

x ∈ [a + c(b−d), a + c]bx∈
/ [a − c, a + c]

左右対称なグラフを持つ関数の重心は明らかにその中心，例えば底辺の中点である．
したがって本アーティクルで形式化した絶対値関数によって左右対称なメンバシップ関数を記述する方法は，メンバシップ関数の重心（非ファジィ化値）を先に定め，それから関数を定義することを容易にしている．
以下の定理は絶対値関数を用いた関数の線対称性を示している．定理 FUZZY 8:19 は，
式 (2) の関数を一般化したものである．定数 b, d, e の取り方で二等辺三角形型もしくは等脚台形型のメンバシップ関数とすることができる．

Listing 2. FUZZY 8:18, FUZZY 8:19
theorem :: FUZZY 8:18
for f be Function of REAL,REAL, a,b,c be Real st (for x be Real holds f.x = b − |. b∗(x−a)/c .|)holds (for y be Real holds f.(a−y) = f.(a+y));theorem :: FUZZY 8:19
for f be Function of REAL,REAL, a,b,c,d,e be Real st (for x be Real holds f.x = min(d, max(e, b − |. b∗(x−a)/c .|)) )holds (for y be Real holds f.(a−y) = f.(a+y));2.2

等脚台形型関数の重心次の定理 FUZZY 8:20 は [5] で定義された台形型メンバシップ関数の形式で表せることを示している．上述の通り，等脚台形型メンバシップ関数の重心が上底（下底）の中点であることは自明である [1]．以下の定理はその形式化である．

Listing 3. FUZZY 8:20, FUZZY 8:23
theorem :: FUZZY 8:20
for a,b,c,d be Real st b > 0 & c > 0 & d > 0 & d < b holds
for x be Real holds(d (#) TrapezoidalFS (a−c,a+(d−b)/(b/c),a+(b−d)/(b/c),a+c)).x = min(d, max(0, b − |. b∗(x−a)/c .|));
theorem :: FUZZY 8:23
for a,b,c,d be Real, f be Function of REAL,REAL stb > 0 & c > 0 & d > 0 & d < b & ( for x be Real holds f.x = min(d, max(0, b − |. b∗(x−a)/c .|)) )holds centroid (f,[’a−c,a+c’]) = a;下の定理は底辺がともに点 (a − c, 0) から (a + c, 0) の線分である二等辺三角形型関数と等脚台形型関数の重心が等しいことを表している．上の Listing 3 よりその重心は a である．

Listing 4. FUZZY 8:34
theorem :: FUZZY 8:34
for a,b,c,d be Real, f,F be Function of REAL,REAL stb > 0 & c > 0 & d > 0 & ( for x be Real holds f.x = max(0, b − |. b∗(x−a)/c .|) ) &( for x be Real holds F.x = min(d, max(0, b − |. b∗(x−a)/c .|)) ) holds
centroid (f,[’a−c,a+c’]) = centroid (F,[’a−c,a+c’]);MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

3/8

Mechanized Mathematics and Its Applications, Works in Progress

2.3

Symmetrical Piecewise Linear Functions

絶対値関数による区分的線形関数の性質

筆者らはファジィ制御に関する研究において，状態方程式の解の存在性に関する考察を行っている [7] [8]．その際に状態変数，ファジィ推論においては入力である前件部変数に対する Lipschitz 連続性が重要な役割を示す．以下の FUZZY 8:25 はファジィ推論計算の状
態変数上の Lipschitz 連続性の証明において，利用可能な定理となる．一方， FUZZY 8:26
はアーティクル [6] にて定義した非ファジィ化値（重心，centroid）に適用するため，絶対値関数によって表された区分的線形関数の積分可能性等に関する定理である．

Listing 5. FUZZY 8:25, FUZZY 8:26
theorem :: FUZZY 8:25
for a,b,c,d,e be Real, f be Function of REAL,REAL stc <> 0 & for x be Real holds f.x = min(d, max(e, b − |. b∗(x−a)/c .|))

holds f is Lipschitzian;theorem :: FUZZY 8:26
for a,b,c,d be Real, f be Function of REAL,REAL stc > 0 & ( for x be Real holds f.x = min(d, max(0, b − |. b∗(x−a)/c .|)) )holds f is integrable on A & f | A is bounded;

32 つの関数が連結した関数
ファジィ推論の推論結果は複数の後件部の関数の合成として出力される．つまり区分的線形関数のように複数の関数が連結したものとなっている．本研究では，ある 1 点で連結する 2 つの関数を +∗ 記号を用いて表している．積分可能性や積分値の分割（合成）に関する以下の定理を形式化した．

Listing 6. FUZZY 8:11, FUZZY 8:13
theorem :: FUZZY 8:11
for a being Real, f, g, h being Function of REAL,REAL stf | A is bounded & f is integrable on A & g | A is bounded & g is integrable on A &a in A & h = ( f | ].−infty,a.] ) +∗ ( g | [.a,+infty.[ ) & f.a = g.aholds h is integrable on A;
theorem :: FUZZY 8:13
for a,b,c being Real, f,g,h be Function of REAL,REAL sta <= b & b <= c & f is integrable on [’a,c’] & f | [’a,c’] is bounded &g is integrable on [’a,c’] & g | [’a,c’] is bounded & h = ( f | ].−infty,b.] ) +∗ ( g | [.b,+infty.[ ) & f.b = g.bholds integral(h,[’a,c’]) = integral(f,[’a,b’]) + integral(g,[’b,c’]);FUZZY 8:13 と関連する定理はアーティクル [9] に収録されている．
連結した関数 h を以下の式 (3) で定義する．ただし，関数 f, g は連続であり，f (b) = g(b)であるとする．

h(x) =f (x)x ∈ [a, b]

g(x)x ∈ [b, c](3)

このとき，h の区間 [a, c] における重心 centroid(h,[’a,c’]) は関数 f, g それぞれの面積と重心 centroid(f,[’a,b’]), centroid(g,[’b,c’]) の加重平均として次のように表せる．

MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

4/8

Mechanized Mathematics and Its Applications, Works in Progress

Symmetrical Piecewise Linear FunctionsRc
x · h(x)dxaRch(x)dxaRcRbx · f (x)dx R bx · g(x)dx R c
a· a f (x)dx + bR c· b g(x)dx
Rbg(x)dx
f (x)dxbaRc=h(x)dxaRc
Rbcentroid(f,[’a,b’]) · a f (x)dx + centroid(g,[’b,c’]) · b g(x)dx=RbRcf (x)dx + b g(x)dxacentroid(h,[’a,c’]) =以下の定理はこれを形式化した．証明には上述の FUZZY 8：13 を適用した．

Listing 7. FUZZY 8:14
theorem :: FUZZY 8:14
for f,g,h be Function of REAL,REAL, a,b,c be Real sta <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = f | [.a,b.] +∗ g | [.b,c.] &integral(f,[’a,b’]) <> 0 & integral(g,[’b,c’]) <> 0 & f.b = g.b holds
centroid(h, [’a,c’]) = 1 / integral(h,[’a,c’]) ∗ ( centroid(f, [’a,b’]) ∗ integral(f,[’a,b’]) + centroid(g, [’b,c’]) ∗ integral(g,[’b,c’]) );この定理によって，複雑な区分的線形関数の重心法による非ファジィ化計算が容易になると期待できる．

4

一般的な四角形型関数の重心
本章では，以下の図 2 のように横軸とで囲んだ図形が四角形になる区分的線形関数について考える．この関数を f とすると以下の式 (4) のように記述できる．

0(b,r)(c,s)

a bcdcentroid
図 2. Piecewise linear function f of (4)

acr



b−a x − b−a s−r x + s − c(s−r)
c−bf (x) = c−bd(−s)−sx−d−cd−c0x ∈ [a, b]x ∈ [b.c]x ∈ [c, d](4)x∈/ [a, d]

上式 (4) の f が各点を通ることを以下の定理で記述した．

Listing 8. FUZZY 8:36
theorem :: FUZZY 8:36
for a,b,c,d,r,s be Real st a < b & b < c & c < d holds

MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

5/8

Mechanized Mathematics and Its Applications, Works in Progress

Symmetrical Piecewise Linear Functions

AﬃneMap(r/(b − a),−a∗r/(b − a)).a = 0 & AﬃneMap(r/(b − a),−a∗r/(b − a)).b = r &AﬃneMap((s − r)/(c − b),s−c∗(s − r)/(c − b)).b = r & AﬃneMap((s − r)/(c − b),s−c∗(s − r)/(c − b)).c = s &AﬃneMap((−s)/(d − c),−d∗(−s)/(d − c)).c = s & AﬃneMap((−s)/(d − c),−d∗(−s)/(d − c)).d = 0;

次の定理は r = s ならば f が台形型の関数になることを，関数 TrapezoidalFS [5] の定数倍として書けることで示している．

Listing 9. FUZZY 8:41
theorem :: FUZZY 8:41
for a,b,c,d,r,s be Real sta < b & b < c & c < d & r >= 0 & s >= 0 & r = s holds
for x be Real holds( r (#) TrapezoidalFS (a,b,c,d) ).x = max+ ((AﬃneMap(r/(b − a),−a∗r/(b − a)) | ].−infty,b.]+∗ AﬃneMap((s − r)/(c − b),s−c∗(s − r)/(c − b)) | [.b,c.] +∗ AﬃneMap((−s)/(d − c),−d∗(−s)/(d − c)) | [.c,+infty.[).x);

ただし，最大値関数は以下で定義されている記号（max+）を用いて記述した．

Listing 10. RFUNCT 8:def 1, 2 [10]deﬁnition
let r be Real;func max+ r −> Real equals :: RFUNCT 3:def 1max (r,0);
correctness ;func max− r −> Real equals :: RFUNCT 3:def 2max ((− r),0);
correctness ;end;

式 (4) の f の区間 [a, d] における重心 centroid(f, [’a,d’]) は以下のように求められる．

Rdcentroid(f, [’a,d’]) = Rada(=(b − a)xf (x)dx
f (x)dx−ar b + ar(b2 + ba + a2 )/3 +·b−ab−a2
s−r 2c(s − r) c + b2+(c − b)(c + cb + b )/3 + s −·c−bc−b2 ),−s 2−s d + c2+(d − c)(d + dc + c )/3 + (−d)·d−cd−c2((b − a)rb+a−ar·+b−a2b−a+(d − c)+ (c − b)s−r c+bc(s − r)·+s−c−b2c−b−s d + c −d(−s)·+d−c2d−c)

この結果の形式化が以下の定理である．

Listing 11. FUZZY 8:43
theorem :: FUZZY 8:43
for a,b,c,d,r,s be Real, f be Function of REAL,REAL sta<b&b<c&c<d&f | [.a,d.] = AﬃneMap(r/(b − a),−a∗r/(b − a)) | [.a,b.]

MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

6/8

Mechanized Mathematics and Its Applications, Works in Progress

Symmetrical Piecewise Linear Functions+∗ AﬃneMap((s − r)/(c − b),s−c∗(s − r)/(c − b)) | [.b,c.]+∗ AﬃneMap((−s)/(d − c),−d∗(−s)/(d − c)) | [.c,d.] holds
centroid( f,[’a,d’] ) =( (b − a)∗( ( r/(b − a) )∗(b∗b +b∗a + a∗a)/3 + ( −a∗r/(b − a) )∗(b + a)/2 )+ (c − b)∗( ( (s − r)/(c − b) )∗(c∗c +c∗b + b∗b)/3 + ( s−c∗(s − r)/(c − b) )∗(c + b)/2 )+ (d − c)∗( ( (−s)/(d − c) )∗(d∗d +d∗c + c∗c)/3 + ( −d∗(−s)/(d − c) )∗(d + c)/2 ) ) /( (b − a)∗( ( r/(b − a) )∗(b + a)/2 + ( −a∗r/(b − a) ) )+ (c − b)∗( ( (s − r)/(c − b) )∗(c + b)/2 + ( s−c∗(s − r)/(c − b) ) )+ (d − c)∗( ( (−s)/(d − c) )∗(d + c)/2 + ( −d∗(−s)/(d − c) ) ) );5

まとめ
本研究では，前稿に引き続き区分的線形関数の主に重心法を用いた非ファジィ化計算に関する数学的諸性質に関する形式化を行った．本稿では特に，絶対値関数を用いて二等辺三角形型や等脚台形型の関数を記述し，重心の値や連続性，対称性に関する定理を証明した．本研究で提案した絶対値関数を用いた関数（メンバシップ関数）の表記は，メンバシップ関数の重心の値が既知であることと，三角形の底辺を示す定義域上の座標が直観的に分かりやすいという利点がある．
その他に，2 つの関数がある１点で連結した関数についていくつかの定理を証明した．

3 章で述べた定理 FUZZY 8:14 は，重心法による非ファジィ化値を個々の関数の重心の値と面積により求めることを可能としている．つまり，重心計算の分子の連結した関数の積分可能性の証明を省略できると考えられる．
これまでのアーティクルで Mamdani 法および代数積-和算-重心法で用いられる計算の形式化はほぼ終えたので，今後の展開として，限界積（Lukasiewicz t-norm）などの他の演算の形式化を課題としたい．

参考文献[1] Mitsuishi T. Isosceles Triangular and Isosceles Trapezoidal Membership Functions
Using Centroid Method. Formalized Mathematics. 2023;31:63–71.
[2] DUBOIS D, PRADE H. Operations on fuzzy numbers. International Journal ofSystems Science. 1978;9(6):613–626. Available from: https://doi.org/10.1080/00207727808941724.
[3] Mitsuishi T, Terashima T, Shimada N, Homma T, Shidama Y. Approximate reasoning using LR fuzzy number as input for sensorless fuzzy control. In: 2016 IEEESymposium on Sensorless Control for Electrical Drives (SLED); 2016. p. 1–5.
[4] Stefanini L, Sorini L. Fuzzy Arithmetic with Parametric LR Fuzzy Numbers. In:IFSA/EUSFLAT Conf.; 2009. p. 600–605.
[5] Grabowski A. The Formal Construction of Fuzzy Numbers. Formalized Mathematics. 2014;22(4):321–327.

MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

7/8

Mechanized Mathematics and Its Applications, Works in Progress[6] Mitsuishi T.

Symmetrical Piecewise Linear Functions

Definition of Centroid Method as Defuzzification.

Formalized

Mathematics. 2022;30(2):125–134. Available from: https://doi.org/10.2478/
forma-2022-0010.
[7] Mitsuishi T, Terashima T, Saigusa K, Shimada N, Homma T, Sawada K, et al.
Continuity of Discrete-Time Fuzzy Systems. In: Loo CK, Yap KS, Wong KW, TeohA, Huang K, editors. Neural Information Processing. Cham: Springer International
Publishing; 2014. p. 462–469.
[8] Mitsuishi T, Shimada N, Homma T, Ueda M, Kochizawa M, Shidama Y. Continuityof approximate reasoning using fuzzy number under Lukasiewicz t-norm. In: 2015
IEEE 7th International Conference on Cybernetics and Intelligent Systems (CIS)and IEEE Conference on Robotics, Automation and Mechatronics (RAM); 2015.
p. 71–74.
[9] Endou N. Improper Integral. Part II. Formalized Mathematics. 2021;29(4):279–294.
Available from: https://doi.org/10.2478/forma-2021-0024.
[10] Kotowicz J, Sakai Y. Properties of Partial Functions from a Domain to the Setof Real Numbers. Formalized Mathematics. 1992;3(2):279–288. Available from:http://fm.mizar.org/1992-3/pdf3-2/rfunct_3.pdf.

Mizar article information
Works in Progress
FUZZY 8 Symmetrical Piecewise Linear Functions Composed by Absolute Value
Functionby Takashi Mitsuishi
Summary: In this paper, some mathematical properties about piecewise linear functions are formalized. The focused piecewise linear functions are symmetrical and composed by absolute function. L-R fuzzy number is applied for various field. Since isosceles
triangle type and isosceles trapezoid type membership functions are simple, they areapplied for the membership functions of L-R fuzzy number in most cases. It is formalized that the membership functions of isosceles triangle type and isosceles trapezoid
type can be constructed by absolute value functions. It is proved and formalized thatthe centroids of the composite function of two continuous functions are the weighted
averages of the areas and centroids of the functions that compose them. Moreover,some calculation and operation between membership functions for fuzzy approximate
reasoning, e.g. Mamdani method and the product-sum-gravity method are formalized.

MMA-WiP (2024), vol.6, no.2 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.2 - ISSN 2434-5458 (Online)

8/8