Varieties ofMetric and QuantitativeAlgebras
蓮尾研 M2 日野 亘

1

修士論文の貢献
metric / quantitative algebra の variety theorem
metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitativeinferenceV

metricimplication

i xi ="i yi ! s =" tV[Mardare+ 2017]
Hω, S, P[Mardare+ 2017]
S, PSR[this thesis]
HR, S, P, PU[Weaver 1995]
S, PR[Khudyakov 2003]
S, P, LS2i si = " i t i ! s = " t背景: Variety Theorem
定理. [Birkhoff 1935] Σ-algebra のクラス K に対して
K は等式の族で定義可能 (= variety)K は 商代数 (H), 部分代数 (S), 直積 (P) で閉じる
• 例: Σ = {・, e, (—)-1} でK

群全体のクラスx · (y · z) = (x · y) · z
x·x 1 =eetc.

Σ-AlgA’A

Πi AiA”• 普遍代数における金字塔的定理「代数のどのような性質が等式で表現できるか」3

Metric Algebra[Weaver 1995] [Khudyakov 2003]

距離空間上の代数 (metric algebra) とmetric equation s s=ε=t" t を用いる
• 関数解析や作用素環への応用
後述

implicationで定義されたクラス

d(JsK, JtK)  "• 連続 な quasivarietyに対する variety theorem
定理. [Weaver 1995] metric algebra のクラス K に対して、
K が implication

Vsi ="i ti ! s =" t の連続な族で定義可能

K は 部分代数 (S) と 約積 (PR) で閉じる
4

Quantitative Algebra[Mardare, Panangaden & Plotkin, LICS 2016]

計算効果の代数的理論 [Plotkin & Power, 2001] の量的拡張•metric algebra + non-expansiveness•

公理として basic quantitative inference を使う
n^xi , yi : 変数x i = " i yi ! s = " ts, t : 項

i=1•

距離空間の構成 (Hausdorff距離, Kantorovich距離) が自由代数 になる•部分集合の間の距離完全な推論体系を与えた
5

確率測度の間の距離修士論文の貢献• metric / quantitative algebra の普遍代数的研究• variety theoremの証明(strict variety および continuous variety)• metric algebraに対する congruence の拡張
metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitative
inference
Vi xi ="i yi ! s =" t[Mardare+ 2017]
Hω, S, P[this thesis]
HR, S, P, PU

6V

metricimplication
i si = " i t i ! s = " t[Mardare+ 2017]
S, PSR[Weaver 1995] S, PR[Khudyakov 2003]
S, P, LS

Strict Variety Theorem
metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitative
inference
Vi xi ="i yi ! s =" t[Mardare+ 2017]
Hω, S, P[this thesis]
HR, S, P, PU

7

V

metricimplication
i si = " i t i ! s = " t[Mardare+ 2017]
S, PSR[Weaver 1995] S, PR[Khudyakov 2003]
S, P, LS

Strict Variety Theorem
定理. [H. 2016] metric algebra のクラス K に対して、
K が metric equation の族で定義可能
K は 商代数 (H), 部分代数 (S), 直積 (P) で閉じる•

古典的な variety theorem のナイーブな拡張•

証明には congruential pseudometric を用いる
8

Congruential Pseudometric•congruence の 距離バージョン
定義. [this thesis] metric algebra A = (A, d, ΣA) に対して、
A 上の pseudometric θ が congruential:θ ≦ d かつ、関係 θ(x, y) = 0 が congruence•

商代数 A/θ が定義できる•普遍代数の定理が再現できる•

第一同型定理•直積代数

permutable congruential pseudometrics9

証明の概略定理. [H. 2016] K が metric equation の族で定義可能
K は 商代数 (H), 部分代数 (S), 直積 (P) で閉じる
証明. (⇐) Kで成立するmetric equationの全体をE.
A⊨EA ∈ K を示せば良い：

T⌃ A/ / T⌃ A/✓K
自由代数

✏ zzA

✓K : T⌃ A/✓ 2 K なるcongruential pseudometric ✓ の上限

古典的な証明のcongruenceの代わりにcongruential pseudometric を使う
10

これで十分？ → NO！
距離等式は表現能力が弱すぎる•

strict variety theorem の応用:
metric equation で定義可能
商代数, 部分代数, 直積 で閉じる

普遍代数として：ノルム線形空間すら表せない
例: x =" y ! x =| |" y•

計算効果への応用として：Hausdorff距離やKantorovich距離を自由代数として表せない→ basic quantitative inference を使う
n^xi , yi : 変数x i = " i yi ! s = " ts, t : 項i=1

11

ω-Variety & Continuous Variety
metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitative
inference
Vi xi ="i yi ! s =" t[Mardare+ 2017]
Hω, S, P[this thesis]
HR, S, P, PU12Vmetricimplication
i si = " i t i ! s = " t[Mardare+ 2017]
S, PSR[Weaver 1995] S, PR[Khudyakov 2003]
S, P, LS

ω-Variety Theorem[Mardare, Panangaden & Plotkin, 2017]

定理. [Mardare+, 2017] metric algebra のクラス K がbasic quantitative inference の族で定義可能
K は 部分代数 (S), 直積 (P), ω-反射的商 (Hω) について閉じている• 一般に、仮定を有限個にするのにテクニックが要る• 今回は、商についてサイズに関する制約 (Hω)• [Weaver 1995], [Khudyakov 2003] と違って連続性がない

13

連続性条件[Weaver 1995] [Khudyakov 2003]

metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitativeinferenceVi xi ="i yi ! s =" t[Mardare+ 2017]
Hω, S, P[this thesis]
HR, S, P, PU

14

Vmetricimplication
i si = " i t i ! s = " t[Mardare+ 2017]
S, PSR[Weaver 1995] S, PR[Khudyakov 2003]
S, P, LS

連続性条件[Weaver 1995] [Khudyakov 2003]

定義. [Khudyakov 2003] implicationの族 Φ が連続的:

Vn

i=1 si ="i ti ! s =" t2なら、任意の ε’ > ε について δ > 0 が存在して、Vn

i=1 si ="i + ti ! s ="0 t 2
Vnx ) =0
かつ、 i=1 xi =0 yi ! (~である。

(~y ) 2

implication の連続な族で定義されたクラスは、•

metric algebra の完備化と超積について閉じる•Qi Ai /UU : 超フィルター

後者は「位相的に閉」[Kapovich+ 1995] → ロバストネス
15

Continuous Variety Theorem
metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitative
inference
Vi xi ="i yi ! s =" t[Mardare+ 2017]
Hω, S, P[this thesis]
HR, S, P, PU

16

V

metricimplication
i si = " i t i ! s = " t[Mardare+ 2017]
S, PSR[Weaver 1995] S, PR[Khudyakov 2003]
S, P, LS

Continuous Variety Theorem
定理. [this thesis] metric algebra のクラス K が、basic quantitative inference の連続な族で定義可能
K は 部分代数 (S), 直積 (P), 反射的商 (HR) および 超積 (PU) について閉じている•

超積は 有限性 + 連続性 のため••商に関するサイズの条件は無い

証明には 距離空間上の自由代数 を用いる
17

既存研究との比較• basic quantitative inference は [Mardare+ 2016] による• 距離空間上のK-自由代数は、Kで成り立つBQIで決まる

K• サイズに関する条件について、┫• [Mardare+ 2017] 商に対して条件 (Hω)

Met

• [this thesis] 超積による (アイデアは[Weaver 1995])
metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitativeinferenceVi xi ="i yi ! s =" t[Mardare+ 2017]
Hω, S, P[this thesis]
HR, S, P, PU

18

Vmetricimplication
i si = " i t i ! s = " t[Mardare+ 2017]
S, PSR[Weaver 1995] S, PR[Khudyakov 2003]
S, P, LS

今後の展望••圏論的な普遍代数論との関連、例えば：•

monad & Eilenberg-Moore algebra (cf. [MacLane 1971])•factorization system [Adámek, Herrlich & Strecker 1990]•enriched Lawvere theory [Power 1999]

距離空間としての性質
例：いつ自由代数が完備／コンパクトになるか？

19まとめ• metric / quantitative algebra の variety theorem(strict variety / continuous variety) を証明した• metric algebra に対する congruence としてcongruential pseudometric を導入し調べた• 同型定理• 直積代数permutable congruential pseudometric20参考文献 (一部)
•N. Weaver. Quasi-varieties of metric algebras. Algebra
universalis, 33(1):1–9, 1995.

•V. A. Khudyakov. Quasivarieties of metric algebras.
Algebra and Logic, 42(6):419–427, 2003.

•

R. Mardare, P. Panangaden, and G. D. Plotkin.
Quantitative algebraic reasoning. LICS 2016.

•P. Mardare, P. Panangaden, and G. D. Plotkin. On theaxiomatizability of quantitative algebras. unpublished,2017. http://people.cs.aau.dk/~mardare/papers/Quasi.pdf
21

対外発表リスト
査読付き論文• Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs.
Healthiness from Duality. LICS 2016.
投稿予定• Wataru Hino. Varieties of Metric and Quantitative Algebras.
口頭発表• Varieties of metric algebras. 数学基礎論若手の会 2016.
• Varieties, Quasivarieties and Prevarieties: Completing the Picture.
CALCO 2015 Early Ideas.
• Quotient monads and their algebras. CSCAT 2015.

22

動機づけ23

計算効果
JfK :int
Z→! int
Z と見なせないかもf:f int→!
int int は [[f]]:: int
•

非停止性

•

非決定性

•

副作用 (状態, 入出力)•

大域的脱出 (継続)•

確率的分岐計算効果24

モナドによる定式化[Moggi, LICS 1989]

f : int ! int を、JfK : Z ! T Z として解釈する
計算効果を表すモナド

例: 非決定性 P , ステート (⇥ S)S, 入力 ( )I利点
• 様々な計算効果を同一の枠組みで扱える欠点• 計算効果の合成を統一的に扱えない• 演算 (∨, read, write, etc.) を別途与える必要25

普遍代数的定式化[Plotkin & Power, FoSSaCS 2001]

operation + equation → free algebra•

例: nondet. choice (∨) + semilattice の公理
x_x=x

利点

x_y =y_xetc.

•

計算効果の syntax に対応して自然な意味論•

等式論理を用いて reasoning ができる•

普遍代数で計算効果の合成を統一的に扱える[Hyland, Plotkin & Power, TCS 2006]
26

Quantitative algebraの理論へ•

計算効果の代数的理論は、プログラムの同一性を推論する体系を与える•

確率的プログラムに対しては、同一性だけでなく、どのくらい近いかを調べたい
0 0.8 1•

quantitative な等式概念へ

0027

0.2 1

Metric / Quantitative Algebra••

metric algebra = Σ-algebra (A, ΣA) と A上の距離 d の対•演算と距離の間に関係性を仮定しない•

定理によっては適宜、連続性などを仮定する

quantitative algebra = metric algebra + non-expansiveness•

各演算 σA : An → A が non-expansived( (~x), (~y ))  maxi d(xi , yi ) for ~x, ~y 2 An•

圏論的には自然：距離空間の圏での Σ-algebra•

ノルム線形空間などを扱えない (例: “2倍”)
28

超積とGromov-Hausdorff Metric29超積 と Gromov-Hausdorff距離• コンパクト距離空間全体のクラスに距離が定まる(Gromov-Hausdorff距離) [Gromov 1999]• 距離空間の収束や連続変形を扱える
例:
n→∞
1/n

30

超積 と Gromov-Hausdorff距離定理. [Kapovich+ 1995] U : N 上の非単項超フィルター

コンパクト距離空間の列 (Xn )n が、Gromov-Hausdorff
Q
距離について X に収束するとき、X ' Xn /U
距離代数の収束 : 距離代数の超積

位相的に閉なクラス : 超積で閉じたクラス

31

閉包条件
•

H: 商代数, Hω: ω-反射的商, HR: 反射的商•

S: 部分代数, P: 直積•

PU: 超積, PR: 約積, PSR: 部分超積
metricequations =" t—continuous[H. 2016]
H, S, P—basic quantitative
inferenceVi xi ="i yi ! s =" t[Mardare+ 2017]
Hω, S, P[this thesis]
HR, S, P, PU

32

V

metricimplication
i si = " i t i ! s = " t[Mardare+ 2017]
S, PSR[Weaver 1995] S, PR[Khudyakov 2003]
S, P, LSω-反射的商
定義. metric algebraの射 f : A → B が ω-反射的:

任意の有限部分集合 B’ ⊂ B に対して、有限部分集合 A’ ⊂ A が存在して、fA’ : A’ → B’ が等長同型∃A’∩fA’∀
B’
∩

AfB

AB
33

反射的商
定義. metric algebraの射 f : A → B が 反射的:部分集合 A’ ⊂ A が存在して fA’ : A’ → B が等長同型

A

∃A’
∩

fA’

AfA’
B
B34