端端舝

衄癹乒犯伙燴�⻌嬡ㄩ?
MSO午左奈玄穴玄件
RYOMA SIN＊YA
AUTOMATA & LOGIC WORKSHOP @ AKITA-U. 27 MAR 2019
q0
q1
q2
q3
q4
q5
A
K
I
T
A
U
9A9B9C
0
B
B
B
B
B
B
B
B
@
8x
2
4
(A(x) ^ ?B(X) ^ ?C(x))
_(A(x) ^ ?B(X) ^ ?C(x))
_(A(x) ^ ?B(X) ^ ?C(x))
3
5
^
8x, y E(x, y) ! ?
2
4
(A(x) ^ A(y))
_(B(x) ^ B(y))
_(C(x) ^ C(y))
3
5
1
C
C
C
C
C
C
C
C
A

衄癹乒犯伙燴�⻌嬡ㄩ?
MSO午左奈玄穴玄件
RYOMA SIN＊YA
AUTOMATA & LOGIC WORKSHOP @ AKITA-U. 27 MAR 2019
q0
q1
q2
q3
q4
q5
A
K
I
T
A
U
9A9B9C
0
B
B
B
B
B
B
B
B
@
8x
2
4
(A(x) ^ ?B(X) ^ ?C(x))
_(A(x) ^ ?B(X) ^ ?C(x))
_(A(x) ^ ?B(X) ^ ?C(x))
3
5
^
8x, y E(x, y) ! ?
2
4
(A(x) ^ A(y))
_(B(x) ^ B(y))
_(C(x) ^ C(y))
3
5
1
C
C
C
C
C
C
C
C
A
及☆凶分卅日厄憝�S★ㄐ

爀⻌
掛琌栳及衙猁
☆正奶皿反傺胍分ㄐ★

爀⻌
掛琌栳及衙猁
↗仇及�及砩庤反摽匹掊隴仄引允

爀⻌
淏�晟惤午反
? 淏�桶政(regular expression)匹𤩸仃月晟惤
? 左奈玄穴玄件匹忳燴匹五月晟逄

爀⻌
淏�晟惤午反
? 瞰ㄩa*(ba*b)*a*?
﹛﹛ˊ {汍, a, aa, bb, aaa, abb, bab, bba, ＃ }?
﹛﹛ˊ☆b及�杅互髒杅�及{a,b}奻及恅趼蹈★?
﹛﹛

爀⻌
淏�晟惤午反
? 瞰ㄩa*(ba*b)*a*?
﹛﹛ˊ {汍, a, aa, bb, aaa, abb, bab, bba, ＃ }?
﹛﹛ˊ☆b及�杅互髒杅�及{a,b}奻及恅趼蹈★?
﹛﹛
q0 q1
b
b
a a

爀⻌
淏�晟惤反嗣�卅杻釾勿仃毛厥勾
淏�晟惤
(恅趼蹈及摩磁)
{汍, a, aa, bb, aaa, abb, bab, bbb, ...}
0
a
1
b
b
a
衄癹左奈玄穴玄件
(�呾乒犯伙)
衄癹乒用奶玉
(測杅乒犯伙)
�g�媼蕆扴惤�燴
(�燴宒)
淏�恅楊
(汜傖恅楊)
淏�桶政
(桶政宒)
a*(ba*ba*)*
Pro?nite words
奻及嶱寯摩磁
(玄禾伕斥奈)
? 準赻隴分互肮�卅隅膽
? 宒ㄛ恅楊ㄛ�呾乒犯伙ㄛ
測杅ㄛ�燴宒ㄛ玄禾伕
斥奈, etc＃.
? ☆癶梢腔卅衙癩反嗣�卅?
﹛杻釾葆仃毛厥勾★

爀⻌
淏�晟惤
0
a
1
b
b
a
(�呾乒犯伙)
衄癹乒用奶玉
(測杅乒犯伙)
(�燴宒)
淏�恅楊
(汜傖恅楊)
淏�桶政
(桶政宒)
a*(ba*ba*)*
Pro?nite words
奻及嶱寯摩磁
(玄禾伕斥奈)
斥奈, etc＃.
? ☆癶梢腔卅衙癩反嗣�卅?
﹛杻釾葆仃毛厥勾★
? 掛揃蹋匹反左奈玄穴玄件午?
�g�媼蕆扴惤�燴及憝�S毛悝少ㄐ

衄癹乒犯伙燴蹦⻌藷ㄩ紼釦倏午左奈玄穴玄件
醴棒
? 恅趼蹈(乒犯伙)午蹦燴宒
? 珨蕆扴惤�燴宒(FO) vs. �g�媼蕆扴惤�燴宒(MSO)
? 左奈玄穴玄件午B邦chi及隅燴(ゴ圉)
? 左奈玄穴玄件午B邦chi及隅燴(摽圉)

恅趼蹈(乒犯伙)午蹦燴宒

恅趼蹈毛�婖午仄化桶允
? 衄癹墿及恅趼蹈反衄癹及�婖午仄化棒及方丹卞桶政匹五月ㄝ
? Universe: 恅趼蹈及奶件犯永弁旦摩磁(赻�杅猁匼)
? 跪恅趼考﹋曳卞�仄化奶件犯永弁旦卞�𡛟允月恅趼互考匹
丐月媆及心淩午卅月1竘杅扴惤 P考ㄛ摯太
? 奶件犯永弁旦及湮苤掀廌毛俴丹媼�憝�S <

? 眕蔥ㄛ恅趼蹈﹛卞�𡛟允月�婖毛Ms午𤩸仁ㄝ
恅趼蹈

恅趼蹈
�婖

恅趼蹈
�婖
恅趼蹈及墿今互6卅及匹ㄛ
universe反1~6引匹及摩磁ㄝ

恅趼蹈
�婖
恅趼蹈及墿今互6卅及匹ㄛ
universe反1~6引匹及摩磁ㄝ
奶件犯永弁旦午恅趼毛憂葆
仃月扴惤ㄝ

�燴宒匹晟惤毛�扴允月
? 淏�桶政互恅趼蹈及摩磁毛�扴允月�卞ㄛ�燴宒反赻旯毛
喃逋允月�婖(恅趼蹈)ㄛ允卅歹切乒犯伙及摩磁毛�扴允月ㄝ
? 勾引曰ㄛ恅趼蹈毛�婖午�卅允珂幻升及桶政毛蕉尹木壬ㄛ﹛
�燴宒反☆晟惤及�扴★卞坻卅日卅中ㄝ
? �燴宒朴毛㦤凶允恅趼蹈及摩磁毛L(朴)午�扴允月ㄩ
L(朴) = {s 2 ??
| Ms |= 朴}

�燴宒匹晟惤毛�扴允月
? 淏�桶政互恅趼蹈及摩磁毛�扴允月�卞ㄛ�燴宒反赻旯毛
喃逋允月�婖(恅趼蹈)ㄛ允卅歹切乒犯伙及摩磁毛�扴允月ㄝ
? 勾引曰ㄛ恅趼蹈毛�婖午�卅允珂幻升及桶政毛蕉尹木壬ㄛ﹛
�燴宒反☆晟惤及�扴★卞坻卅日卅中ㄝ
? �燴宒朴毛㦤凶允恅趼蹈及摩磁毛L(朴)午�扴允月ㄩ
L(朴) = {s 2 ??
| Ms |= 朴}
仇及�瘍 |= 反TeX匹反 models 午𤩸仁ㄝ?
☆必正�瘍★卅升午手網壬木月ㄝ

�燴宒匹晟惤毛�扴允月ㄗ瞰ㄘ

﹛及摽欠卞﹛互懂卅中午中丹�燴宒ㄝ

午允月午﹛﹛﹛﹛卅及匹
( )

午允月午﹛﹛﹛﹛卅及匹
勾引曰反淏�桶政匹中丹垀及﹛ 卞坻卅日卅中ㄐ
( )

珨蕆扴惤�燴宒(FO) VS.?
�g�媼蕆扴惤�燴宒(MSO)
9x : element vs. 9X : set

珨蕆扴惤�燴宒(FO) VS. �g�媼蕆扴惤�燴宒(MSO)
淏�晟惤ˊ珨蕆扴惤�燴宒匹隅膽褫夔ˋ
? a*b*午中丹淏�桶政反珨蕆扴惤�燴宒匹隅膽允月仇午互匹
五凶ㄩ
? 匹反�化及淏�桶政反珨蕆�燴及��匹�扴匹五月及井ˋ引
凶公及欄反升丹卅及井ˋ

淏�晟惤ˊ珨蕆扴惤�燴宒匹隅膽褫夔ˋ
? a*b*午中丹淏�桶政反珨蕆扴惤�燴宒匹隅膽允月仇午互匹
五凶ㄩ
? 匹反�化及淏�桶政反珨蕆�燴及��匹�扴匹五月及井ˋ引
凶公及欄反升丹卅及井ˋ
? 灍反ㄛ珨蕆�燴匹�扴匹五月晟惤及弁仿旦反淏�晟惤及扔皮
弁仿旦卞仄井卅日卅中ㄝ勾引曰淏�晟惤毛�扴允月及卞珨蕆
�燴匹反ʃ允亢月ㄐ

? 匹反�g�卞媼蕆卞奻互勻化心月午升丹井ˋ灍蕣ㄛ珨蕆匹�扴
匹五月��方曰反月井卞𣷣中��匹晟惤及�扴匹五月
淏�晟惤ˊ媼蕆扴惤�燴宒匹隅膽褫夔ˋ

? 仄井仄ㄛ灍反ㄛ媼蕆�燴反淏�晟惤方曰淩卞𣷣中晟惤弁仿
旦毛�扴匹五月夔薯毛厥勾ㄝ?
勾引曰ㄛ淏�晟惤毛�扴允月及卞媼蕆�燴匹反�允亢月ㄐ

瞰尹壬ㄛ眕狟及�燴宒反準淏�晟惤?
☆a午b及堤政隙杅互脹仄中恅趼蹈及摩磁★?
毛�扴仄化中月ㄝ

媼�憝�S毛講趙匹五月什日中�中午☆��g扞及
湔婓★引匹�扴匹五月ㄝ公及凶戶☆摩磁及啋及
�杅互脹仄中★及方丹卅乒用互𤩸仃化淏�晟惤
及��毛閉尹化仄引丹ㄝ

媼�憝�S毛講趙匹五月什日中�中午☆��g扞及
湔婓★引匹�扴匹五月ㄝ公及凶戶☆摩磁及啋及
�杅互脹仄中★及方丹卅乒用互𤩸仃化淏�晟惤
及��毛閉尹化仄引丹ㄝ

卅日�g�憝�Sㄛ勾引曰摩磁及講趙及心卞秶癹仄
凶媼蕆�燴卅日壬中仃月及匹反ㄗ眻覜ㄘˋ

淏�晟惤ˊ�g�媼蕆扴惤�燴宒匹隅膽褫夔ㄐ
( J.R. B邦chi, 1960)
晟惤互淏�晟惤匹丐月 ? 反�g�媼蕆�燴
(Monadic Second Order Logic, MSO)匹�扴
褫夔匹丐月ㄝ
? ☆淏�晟惤 ? MSO�扴褫夔★反��gㄝ?
左奈玄穴玄件毛扑立亙伊奈玄允月�燴宒毛匼眻卞MSO匹�扴允月仇午
互堤懂月(隅燴及ゴ圉)ㄝ
? 公及欄☆MSO�扴褫夔?淏�晟惤★互支支褣仄中(隅燴及摽圉)ㄝ

FO VS. MSO
? FO(珨蕆�燴)匹�扴匹五卅仁化MSO匹�扴匹五月晟惤ㄛ允
卅歹切FO匹�扴匹五卅中及反升丹中丹晟惤井ˋ
? 瞰尹壬(ab)*反FO匹�扴匹五月互ㄛ(aa)*反FO匹反�扴匹五
卅中ㄐ
? 仇及岈灍反珨蕆�燴午左奈玄穴玄件及測杅腔俶斮及�𡛟ㄛ
丐月中反Ehrenfeucht每Fra?ss谷 game卅升及衄癹乒犯伙燴�
及耋撿毛蚚中化尨六月互掛琌栳匹反畿賡仄卅中ㄝ

MSO反FO方曰淩卞�中
(aa)* = ☆髒杅�及§a§及靜曰殿仄★反眕狟及MSO宒匹桶六月ㄩ
?X
?
?
?x (?rst(x) ↙ X(x))
＿ ?x (last(x) ↙ ?X(x))
＿ ?x?y succ<(x, y) ↙ (X(x) ? ?X(y))
?
? ,
where ?rst(x) stands for ?y (y ≡ x), last(x) stands for ?y (y ≒ x), and
succ<(x, y) stands for (x < y) ＿ ??z (x < z ＿ z < y).

左奈玄穴玄件午B?CHI及隅燴
(ゴ圉)
q0
q1
q2
q3
q4
q5
A
K
I
T
A
U

(ゴ圉)
q0
q1
q2
q3
q4
q5
A
K
I
T
A
U
9X09X1 ﹞ ﹞ ﹞ 9Xm?1 'part ^ 'start ^ 'trans ^ 'accept

左奈玄穴玄件午B?CHI及隅燴(ゴ圉)
( J.R. B邦chi, 1960)
褫夔匹丐月ㄝ

☆淏�晟惤 ? MSO�扴褫夔★毛尨允
A = (Q, q0, F, 汛)﹛﹛﹛﹛﹛﹛﹛ 毛袨颷摩磁Qㄛ場ヽ袨颷 q0ㄛ忳燴袨颷摩磁Fㄛ?
腛痄憝杅汛: Q ℅ 曳 ↙ Q 午允月𢜪隅俶左奈玄穴玄件ㄛ匹m�及?
袨颷互丐月午允月ㄩㄝQ = {q0, . . . , qm?1}

袨颷互丐月午允月ㄩㄝ
L(A)互眕狟及MSO�燴宒匹桶六日木月仇午毛尨允ㄝ
Q = {q0, . . . , qm?1}
朴A = 9X09X1 ﹞ ﹞ ﹞ 9Xm?1 'part ^ 'start ^ 'trans ^ 'accept.

袨颷互丐月午允月ㄩㄝ
L(A)互眕狟及MSO�燴宒匹桶六日木月仇午毛尨允ㄝ
Q = {q0, . . . , qm?1}
介勻仁曰眻覜毛晟丹午仇及�燴宒反左奈玄穴玄件A卞方月�
呾毛扑立亙伊奈玄仄化云曰ㄛ跪Xi卞�仄化x ﹋ Xi 反?
☆x楓醴及恅趼毛網氏匹袨颷qi卞腛痄允月★毛桶仄化中月ㄝ

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳part反跪 X0, X1, ＃, Xm-1互奶件犯永弁旦摩磁及煦賃卞卅勻化中月
仇午毛桶仄化中月ㄩ

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳part反跪 X0, X1, ＃, Xm-1互奶件犯永弁旦摩磁及煦賃卞卅勻化中月
仇午毛桶仄化中月ㄩ
?x
m?1
i=0
Xi(x) ＿
j?=i
?Xj(x)'part =

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳start反煦賃及珂螹互場ヽ袨颷井日及袨颷腛痄午脹仄中仇午毛桶
仄化中月ㄩ

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳start反煦賃及珂螹互場ヽ袨颷井日及袨颷腛痄午脹仄中仇午毛桶
仄化中月ㄩ
?x
a﹋曳
Pa(x) ＿ ?y (y ≡ x) ↙ X汛(q0,a)(x)'start =

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳trans反跪 X0, X1, ＃, Xm-1互左奈玄穴玄件及袨颷腛痄汛卞𣶹勻化中
月仇午毛桶仄化中月ㄩ

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳trans反跪 X0, X1, ＃, Xm-1互左奈玄穴玄件及袨颷腛痄汛卞𣶹勻化中
月仇午毛桶仄化中月ㄩ
?x?y
m?1
i=0 a﹋曳
(x ? y) ＿ Xi(x) ＿ Pa(y) ↙ X汛(qi,a)(y)
'trans =

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳accept反郔摽及袨颷互忳燴袨颷匹丐月仇午毛桶仄化中月ㄩ

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳accept反郔摽及袨颷互忳燴袨颷匹丐月仇午毛桶仄化中月ㄩ
?x ?y (y ≒ x) ↙
qi﹋F
Xi(x)'accept =

A = (Q, q0, F, 汛) where Q = {q0, . . . , qm?1}
耳partㄛ耳startㄛ耳transㄛ耳accept 及公木冗木及隅膽方曰
匹丐月仇午反隴日井ㄝ
L(A) = L(朴A) = {s 2 ??
| Ms |= 朴A}

左奈玄穴玄件毛扑立亙伊奈玄允月�燴宒毛匼眻卞MSO匹�扴允月
仇午互堤懂月(隅燴及ゴ圉)ㄝ
( J.R. B邦chi, 1960)
褫夔匹丐月ㄝ
? 灍蕣ㄛ仇仇匹及偩隴井日☆淏�晟惤??MSO�扴褫夔★
午卅月仇午互歹井月ㄝ

(摽圉)

左奈玄穴玄件午B?CHI及隅燴(摽圉)
( J.R. B邦chi, 1960)
褫夔匹丐月ㄝ

☆MSO�扴褫夔?淏�晟惤★毛尨允
? 公及凶戶卞反講趙仿件弁(quanti?er rank, qr) 午正奶皿(type)
午網壬木月衙癩毛爀⻌允月斛猁互丐月ㄝ
? 正奶皿及衙癩反乒犯伙燴�卞云中化手笭猁匹丐月互ㄛ?
衄癹乒犯伙燴�卞云中化手笭猁午卅月ㄝ
? 凶分仄ㄛ杻卞B邦chi及隅燴及偩隴卞云中化反妏歹木源互癶
籵及乒犯伙燴�卞云仃月妏歹木源午�卅月(嗣煦ㄝ乒犯伙
燴��仄仁卅中仃升)ㄝ

講趙仿件弁
? 講趙仿件弁反MSO�燴宒耳卞�仄化䔝慮腔卞隅膽今木月
棒及�qr(耳)匹丐月ㄝ
qr(9x') = qr(8x') = qr(') + 1
qr(9X') = qr(8X') = qr(') + 1
qr(x = y) = qr(x < y) = qr(Pa(x)) = qr(x 2 X) = 0
qr(?') = qr(')
qr('1 _ '2) = qr('1 ^ '2) = max(qr('1), qr('2))

講趙仿件弁
? 講趙仿件弁反MSO�燴宒耳卞�仄化䔝慮腔卞隅膽今木月
棒及�qr(耳)匹丐月ㄝ
qr(9x') = qr(8x') = qr(') + 1
qr(9X') = qr(8X') = qr(') + 1
qr(x = y) = qr(x < y) = qr(Pa(x)) = qr(x 2 X) = 0
qr(?') = qr(')
qr('1 _ '2) = qr('1 ^ '2) = max(qr('1), qr('2))
? 勾引曰qr(耳)反☆耳及講趙赽及生旦玄及郔湮�★毛桶允ㄝ

講趙仿件弁
? 講趙仿件弁互凶井分井k匹丐月方丹卅赻蚕劐杅及剠中
MSO�燴宒(勾引曰MSO本件氾件旦)及摩磁毛MSO[k]匹
桶允ㄝ

講趙仿件弁
? 講趙仿件弁互凶井分井k匹丐月方丹卅赻蚕劐杅及剠中
MSO�燴宒(勾引曰MSO本件氾件旦)及摩磁毛MSO[k]匹
桶允ㄝ
? 笭猁卅萸反ㄛMSO[k]反(�燴腔肮�匹賃月午)凶井分井?
衄癹�及�燴宒仄井漪引卅中午中丹仇午匹丐月ㄝ
? 仇木反�燴宒及講趙仿件弁午赻蚕劐杅及�杅卞�允月䔝
慮楊匹��g卞尨允仇午互匹五月ㄝ

正奶皿
? MSO[k]及窒煦摩磁T互consistent卅�磁ㄛ允卅歹切丐月
恅趼蹈 s ﹋曳* 匹?
?
午卅月(乒犯伙毛厥勾)�磁卞T毛k-正奶皿午網少ㄝ丐月中
反T毛恅趼蹈s及k-正奶皿午網少ㄝ
T = {朴 2 MSO[k] | Ms |= 朴}

正奶皿
?
T = {朴 2 MSO[k] | Ms |= 朴}
瞰
T = {朴 2 MSO[1] | M" |= 朴}

正奶皿
?
T = {朴 2 MSO[k] | Ms |= 朴}
瞰
T = {朴 2 MSO[1] | M" |= 朴}
反諾恅趼蹈汍﹋ {a,b}*及1-正奶皿
= {8x (x = x), 8x ?(x = x),
8x Pa(x), 8x Pb(x), 8x Pa(x) _ 8x Pb(x)}

正奶皿
? MSO[k]反恅趼蹈及摩磁毛衄癹�及正奶皿卞煦賃允月ㄩ
{a, b}?

正奶皿
8x (Pa(x))
{a, b}?

正奶皿
8x (Pa(x))
true
false
{a, b}?

正奶皿
8x (Pa(x))
aaa true
false
{a, b}?

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
9x(Pb(x))
true
false

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
9x(Pb(x))
true
false

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
"
abbab
bbab

cf. Wassily Kandinsky ※circles in a circle§ (1923)

(蜊戶化)☆MSO�扴褫夔?淏�晟惤★毛尨允
朴 2 MSO[k]
L(朴) = {s 2 ??
| Ms |= 朴} = L(A)﹛﹛﹛﹛﹛﹛﹛﹛﹛﹛﹛﹛﹛﹛﹛﹛午卅月左奈玄穴玄件A毛
�傖允月ㄝ仇及午五ㄛA反正奶皿毛蚚中化棒及方丹卞�傖匹五
月ㄩ﹛﹛﹛﹛﹛﹛﹛﹛仇仇匹A = (Q, T0, F, 汛)

朴 2 MSO[k]
L(朴) = {s 2 ??
月ㄩ﹛﹛﹛﹛﹛﹛﹛﹛仇仇匹A = (Q, T0, F, 汛)
T0 = T" = {耳 2 MSO[k] | M" |= 耳}反諾恅趼蹈及k-正奶皿

朴 2 MSO[k]
L(朴) = {s 2 ??
月ㄩ﹛﹛﹛﹛﹛﹛﹛﹛仇仇匹A = (Q, T0, F, 汛)
Q = {T0, . . . , Tm}反�化及k-正奶皿及摩磁

朴 2 MSO[k]
L(朴) = {s 2 ??
月ㄩ﹛﹛﹛﹛﹛﹛﹛﹛仇仇匹A = (Q, T0, F, 汛)
F ? Q反朴午consistent卅k-正奶皿及摩磁

朴 2 MSO[k]
L(朴) = {s 2 ??
月ㄩ﹛﹛﹛﹛﹛﹛﹛﹛仇仇匹A = (Q, T0, F, 汛)
F ? Q反朴午consistent卅k-正奶皿及摩磁
汛(Ts, a) = Tsa i? Ts反丐月恅趼蹈s及k-正奶皿?
﹛﹛井勾Tsa反sa及k-正奶皿

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1q2

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1q2
q3

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1q2
q3
q4

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1q2
q3
q4 q5

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1q2
q3
q4 q5
q6

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1q2
q3
q4 q5
q6 q7

正奶皿
8x (Pa(x))
aaa
aba
true
false
{a, b}?
朴aA? = 9x(8y(x ? y) ) Pa(x))
朴aA?
true
false
9x(Pb(x))
true
false
abbab
bbab
q0 q1q2
q3
q4 q5
q6 q7
仇及�卞跪正奶皿毛袨颷心卅仄ㄛ?
☆羥ピ卞★場ヽ袨颷ㄛ袨颷腛痄ㄛ?
忳燴袨颷摩磁毛隅戶化支木壬啋及?
�燴宒朴﹋ MSO[k] 卞�仄 L(朴) = A午卅月?
(𢜪隅俶)左奈玄穴玄件A互�傖匹五月ㄐ

? 公及欄☆MSO�扴褫夔?淏�晟惤★互支支褣仄中(隅燴及摽
圉)ㄝ
? 講趙仿件弁毛秶癹仄正奶皿毛衄癹卞允月仇午匹ㄛ啋及�
燴宒井日左奈玄穴玄件互�傖匹五凶ㄐ
( J.R. B邦chi, 1960)
褫夔匹丐月ㄝ

云引仃
淏�晟惤
0
a
1
b
b
a
(�呾乒犯伙)
衄癹乒用奶玉
(測杅乒犯伙)
(�燴宒)
淏�恅楊
(汜傖恅楊)
淏�桶政
(桶政宒)
a*(ba*ba*)*
Pro?nite words
奻及嶱寯摩磁
(玄禾伕斥奈)
斥奈, etc＃.
? 掛揃蹋匹反賤掊仄卅井勻凶
互ㄛ嗣�极(variety)及衙癩
毛籵元化晟惤午�燴午測杅
反藝仄中�𡛟毛�六月ㄝ

云引仃
哫�ㄩ淏�晟惤午晟惤午測杅午�燴及�𡛟
/sinya8282/an-introduction-to-eilenbergs-variety-theorem

衄癹乒犯伙燴�及
(湮劐掂心支允中)?
⻌嬡𤩸
Written by Leonid Libkin

測杅腔左奈玄穴玄件
燴�及匼ル日仄中
⻌嬡𤩸ㄝ
晟惤及嗣�极及�
支EILENBERG＊S VARIETY
THEOREM及偩隴手徭勻
化月ㄝ
Written by Mark Lawson

端端舝

衄癹乒犯伙燴蹦⻌藷ㄩ紼釦倏午左奈玄穴玄件

More Related Content

衄癹乒犯伙燴蹦⻌藷ㄩ紼釦倏午左奈玄穴玄件