‘æ‚QÍ@’ŠÛ‰ðŽßŠT—viŽå‚ÉCousot‰Šú˜_•¶‚©‚çj@@@@@@@

‚QD‚P@ƒvƒƒOƒ‰ƒ€‚̃Zƒ}ƒ“ƒeƒBƒNƒXiˆÓ–¡˜_j‚Æ’ŠÛ‰ðŽß‚ÌŠî–{—pŒê@@@@@@@@@@@@@@

@‚±‚±‚Å‚ÍAƒvƒƒOƒ‰ƒ€‚Ì’ŠÛ‰ðŽß‚ðƒtƒH[ƒ}ƒ‹‚É’è‹`‚·‚邽‚ß‚ÉŠÖŒW‚·‚éƒvƒƒOƒ‰ƒ€‚̃Zƒ}ƒ“ƒeƒBƒNƒX‚Æ’ŠÛ‰ðŽß‚Å—p‚¢‚ç‚ê‚éŠî–{“I—pŒê(*)‚ðŠÈ’P‚ÉЉ‚éBi‚±‚Ìß‚ÍCousot‰Šú˜_•¶‚Ì‚RßA‚Sß‚ÉŠY“–‚·‚éj@@
(*)ƒm[ƒh‚âŠÂ‹«Aó‘Ô‚È‚Ç‚Ì—pŒê‚ÍAScott and Strachey‚Ì"Mathematical semantics of Program"(1971)‚Å’è‹`‚³‚ê‚Ä‚¢‚éB

@‚Ü‚¸A€”õ‚Æ‚µ‚ăvƒƒOƒ‰ƒ€‚̃Zƒ}ƒ“ƒeƒBƒNƒX‚ɂ‚¢‚Äà–¾‚·‚éB

¡ƒvƒƒOƒ‰ƒ€‚̃Zƒ}ƒ“ƒeƒBƒNƒXiˆÓ–¡˜_j‚Æ‚ÍH

@ƒvƒƒOƒ‰ƒ€P‚̃Zƒ}ƒ“ƒeƒBƒNƒX‚Æ‚ÍA‚»‚̃vƒƒOƒ‰ƒ€‚ð•]‰¿‚µ‚½‚¢€–Ú‚É’…–Ú‚µ‚ÄA‚»‚ê‚̉”\‚ÈŽÀs‚ð

‹Lq‚·‚éuŒvŽZƒ‚ƒfƒ‹v‚Å‚ ‚éB‚µ‚½‚ª‚Á‚ÄA‚»‚±‚ł̓vƒƒOƒ‰ƒ€‚Ì•]‰¿‘ÎÛ‚ÉŠÖŒW‚Ì‚È‚¢€–Ú‚ÍŽÌ‘œ

‚³‚ê‚éBƒvƒƒOƒ‰ƒ€‚̃Zƒ}ƒ“ƒeƒBƒNƒX‚ð‹Lq‚·‚é•û–@‚Í‘½”‚ ‚邪A‚±‚±‚Å‚ÍŒvŽZƒXƒeƒbƒv’PˆÊ‚É‚»‚Ì

ó‘Ԃ̕ω»‚ð‹Lq‚·‚éƒgƒŒ[ƒXƒx[ƒX‚Ì‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX(operatinal semantics)‚ðl‚¦‚éB

¡ƒgƒŒ[ƒXƒx[ƒX‚Ì‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX—á

@D. Schmidt, All the World is an abstract interpretation‚ÉÚ‚Á‚Ä‚¢‚éŠÈ’P‚È—á‚ð‰º‹L‚ÉŽ¦‚·G

@@@@@@@

@@@@@@@@ip0, p1, p2, p3‚̓vƒƒOƒ‰ƒ€is‚̈ʒu‚ðŽ¦‚·ƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgj

ã‹L‚̃vƒƒOƒ‰ƒ€‚Ì‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚ÍA‰º‹L‚Ì4‚‚̑JˆÚƒ‹[ƒ‹‚ðŽg—p‚µ‚ăvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚Æ•Ï”‚Ì’l‚Ì‘gpp, x‚ðXV‚·‚éG

@@@@@

‚±‚Ì‚Æ‚«Aã‹L‚̃vƒƒOƒ‰ƒ€‚Ì‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚͉º‹L‚̃gƒŒ[ƒX‚Æ‚µ‚Ä•\‚³‚ê‚éG

ƒvƒƒOƒ‰ƒ€‚Ì•Ï”x‚Ì’l‚ª12‚Æ‚µ‚Ä—^‚¦‚ç‚ꂽ‚Æ‚·‚é‚ÆA

@@@@@@@

ip0,12‚É‚æ‚èx=12A p1,12‚É‚æ‚èx=6A p0,6‚É‚æ‚èx=6Ap1,6‚É‚æ‚èx=3Ap0,3‚É‚æ‚èx=3Ap2,3‚É‚æ‚èx=12‚æ‚èp3,12)

‚±‚ê‚ðA‰¡Ž²‚ÉŽžŠÔ‚ÌŒo‰ß‚É‚æ‚éƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚̕ω»AcŽ²‚É•Ï”‚Ì’l‚ðŽæ‚èAƒOƒ‰ƒt‚Å•\‚·‚ÆA

‰º‚Ì}‚̂悤‚É•\Œ»‚Å‚«‚éG

@@@@@@@@@@

@@@@@@@@@@@}‚QD‚P@‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚̃gƒŒ[ƒX‚̃Oƒ‰ƒt

ã‹L‚̃vƒƒOƒ‰ƒ€‚Å•Ï”‚̉Šú’l‚Ì—^‚¦•û‚ð•Ï‚¦‚é‚ƈقȂéƒgƒŒ[ƒX‚ª“¾‚ç‚ê‚éB—Ⴆ‚ÎA

@@@x=3‚Ì‚Æ‚«Ap0,3¨p2,3¨p3,12

@@@x=4‚Ì‚Æ‚«Ap0,4¨p1,4¨p0,2¨p1,2¨p0,1¨p2,1¨p3,4

@@@@@

@@@@@@@}‚QD‚Q@‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚̉”\‚ȃgƒŒ[ƒXiˆê•”•ªj‚̃Oƒ‰ƒt

@‚±‚̂悤‚ÉAƒZƒ}ƒ“ƒeƒBƒNƒX‚Í‘S‚Ẳ”\‚ÈŽÀsŠÂ‹«‚ł̃vƒƒOƒ‰ƒ€‚ÌŽÀs‚ðˆÓ–¡‚·‚é‚Ì‚ÅAƒgƒŒ[ƒXƒx[ƒX‚Ì‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚ÍŽžŠÔt‚ÌŠÖ”‚Æ‚µ‚ăvƒƒOƒ‰ƒ€‚Ì•Ï”‚Ì’l‚Ȃǂ̃xƒNƒgƒ‹x(t)‚̕ω»‚ðŽ¦‚·ƒJ[ƒu‚Æ‚µ‚ĉº‹L‚̂悤‚É•\Œ»‚³‚ê‚éG

@@@@@@

@@@@@@@@@@}‚QD‚R@‰Â”\‚ȃgƒŒ[ƒX‚̃Oƒ‰ƒt•\Œ»—á

ˆÈ~A‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚ð’è‹`‚·‚邽‚߂ɉº‹L‚Ì—pŒê‚ɂ‚¢‚ÄŠÈ’P‚ÈŽ–—á‚É‚æ‚èà–¾‚·‚éG

@@@@EƒvƒƒOƒ‰ƒ€‚̃m[ƒh(Node)‚ÆŒÊ(Arc)‹y‚уvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg

@@@@Eƒm[ƒh‚̃^ƒCƒviŠJŽnA‘ã“üAÚ‡A•ªŠòAoŒûj

@@@@EŠÂ‹«(Encironment)

@@@@Eó‘Ô(State)

@@@@EƒRƒ“ƒeƒLƒXƒg(Context)

@@@@EƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹(Context-Vector)

@@@@En-ƒRƒ“ƒeƒLƒXƒg(n-context)

@@@@EF-contŠÖ”

i‚Pjƒm[ƒh‚Æ‚»‚̃^ƒCƒv

@@@ƒvƒƒOƒ‰ƒ€‚̃m[ƒh‚Í}‚QD‚S‚̂悤‚ÉAŠJŽnA‘ã“üAÚ‡A•ªŠòAoŒû‚ÌŠeƒm[ƒh‚ª‚ ‚éBŠeX‚Ì

@@ˆÓ–¡‚ÍA}‚̉E‚̃m[ƒh‚Ìà–¾‚ðŽQÆB

@@@@

@@@@@@}‚QD‚S@ƒvƒƒOƒ‰ƒ€‚̃m[ƒh

¡‘ã“üƒm[ƒh‚ɂ‚¢‚Ä‚Ì•â‘«à–¾F‘ã“üƒm[ƒhn‚ÍA‚»‚̃m[ƒhn‚Åu‰E‘¤‚ÌŽ®expr(n)‚Ì’l‚𶑤‚Ì

@Ž¯•ÊŽqid(n)‚É‘ã“ü‚·‚éB‚·‚È‚í‚¿Aid(n) = expr(n)@iã‚Ì—áx:=x+1‚Å‚ÍAid=x, expr=x+1j

@ ‚±‚±‚ÅAŽ¯•ÊŽq‚Æ‚ÍA•Ï”AŽè‘±‚«AŠÖ”‚Ì–¼‘O‚Å‚ ‚éBŽ¯•ÊŽq‚Ì‘S‘Ì‚ÍIdent‚Å•\‚·B

i‚QjŒÊ(arc)‚ƃvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg

@@ƒm[ƒhŠÔ‚Ì‘JˆÚ‚ƃvƒƒOƒ‰ƒ€‚ÌisˆÊ’u‚ðŽ¦‚·‚½‚߂ɌʂƃvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚ª‚ ‚éB}‚QD‚T‚ðŽQÆB

@@@

@@@@@@@@}‚QD‚T@ŒÊ‚ƃvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg

@ˆÈã‚̓vƒƒOƒ‰ƒ€‚Ì\‘¢‚ɂ‚¢‚Ä‚ÌŠî–{“I‚È—pŒê‚Å‚ ‚éBŽŸ‚ÉAƒvƒƒOƒ‰ƒ€ˆÓ–¡˜_‚ÅŽg‚í‚ê‚é—pŒê‚Å‚ ‚éuŠÂ‹«v‚Æuó‘Ôv‚ɂ‚¢‚Äà–¾‚·‚éB

i‚RjŠÂ‹«(Environment)

@@ŠÂ‹«‚ÍŽ¯•ÊŽqi•Ï”AŽè‘±‚«AŠÖ”‚Ì–¼‘Oj‚Æ‚»‚Ì’l‚ðŒ‹‚Ñ•t‚¯‚é‚à‚ÌB‚·‚È‚í‚¿AŠÂ‹«‚ÍŽ¯•ÊŽq

@‚©‚ç’l—̈æ‚Ö‚ÌŠÖ”‚Ì‘S‘Ì‚Å‚ ‚éF@@Env = Ident¨ Values@iValues‚Í’l‚ÌW‡j

@‚µ‚©‚µA‚±‚±‚Å‚ÍŽ¯•ÊŽq‚Æ‚µ‚Äu•Ï”v‚É‚Ì‚Ý’…–Ú‚µ‚Äl‚¦‚éB‚·‚È‚í‚¿AuAn environment(Env) is a

@valuation for each variable of the programv‚Å‚ ‚é‚Æ‚·‚éBŠÈ’P‚ÉŒ¾‚¦‚ÎAuŠÂ‹«‚Æ‚ÍA•Ï”‚Æ‚»‚Ì’l‚Ì

@‘ΉžB•Ï”‚Ì’†g‚ð’è‹`‚·‚é‚à‚Ìv‚Å‚ ‚éB‰º‚Ì}‚ðŽQÆB

@@@@@@

@@@@@@@@@@@@@}‚QD‚U@ŠÂ‹«‚Ìà–¾

@i—áje‚ð•Ï”x, y‚É5, 10‚ð‘Ήž‚³‚¹‚éŠÂ‹«‚Æ‚·‚éB ‚±‚ê‚ðeox¨5, y¨10p‚Æ‘‚­‚±‚Æ‚à‚ ‚éBˆÓ–¡

@@@‚Íe(x)=5, e(y)=10‚Æ“¯‚¶B¨ˆÈ~‚ÍAe(x)=a‚Ì•\‹L‚ðŽg—pBˆÓ–¡˜_‚Å‚Íe(x)=[[x]](e)‚Æ‚à‘‚­B

i‚Sjó‘Ô(State)

@@ó‘ÔState‚Í<Arc, Env>‚Ì‘g‚Å‚ ‚èAƒvƒƒOƒ‰ƒ€ŽÀsŽž‚Ì‚ ‚éƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚ł̃vƒƒOƒ‰ƒ€‚Ìó‘Ô‚ðŽ¦‚·iStates = Arcs~EnvjB¨}‚QD‚V‚ðŽQÆB

@@@

@@@@@@@}‚QD‚V@ó‘Ô‚Ìà–¾

¡ó‘Ô<Arc, Env>‚ÌŠÈ’P‚ȕω»—á‚ð}‚QD‚W‚ÉŽ¦‚·B

@

@@@@@@@}‚QD‚W@ó‘Ԃ̕ω»—á

ã‹L‚̃vƒƒOƒ‰ƒ€‚Ì‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚͉º‹L‚̃gƒŒ[ƒX‚Æ‚µ‚Ä•\‚³‚ê‚éG

@@@@ƒÐ0¨ƒÐ1¨ƒÐ2¨ EEEEE ¨ƒÐ303

ƒvƒƒOƒ‰ƒ€‚Ìó‘Ô‚ÍA‰Šúó‘Ô‚©‚ço”­‚µ‚ÄA—^‚¦‚ç‚ꂽó‘Ôs=<a, e>‚ÌuŽŸ‚Ìó‘Ô(next state)v‚ð

Ž¦‚·ŠÖ”n-state(State<a, e>)‚©‚çì‚邱‚Æ‚ª‚Å‚«‚éG

EI-States‚͉Šúó‘Ô‚ÌW‡‚Å‚ ‚éBƒvƒƒOƒ‰ƒ€‚Ì«Ž¿‚ÍŠeƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚ÉŠÖŒW‚µ‚½hó‘Ô‚Ì

@@W‡h‚ðŽg—p‚µ‚Ä’²‚ׂç‚ê‚éBI-States‚ÍŽŸ‚̂悤‚É’è‹`‚³‚ê‚éG

@@@@@@I-States = { <“üŒûƒm[ƒh‚̌㑱‚ÌŒÊ ,ƒ{ƒgƒ€‚ÌEnv >}

@@}‚QD‚W‚Ì—á‚Å‚ÍAI-States=<r0, e(x)=ƒÓ}>=ƒÐ0‚Å‚ ‚éB

@E—^‚¦‚ç‚ꂽó‘Ôs=<a, e>‚ÌuŽŸ‚Ìó‘Ô(next state)v‚ðŽ¦‚·ŠÖ”n-state(State<a, e>)‚͘_•¶’†‚Ì

@ƒAƒ‹ƒSƒŠƒYƒ€‚ðŽQÆBn-stateŠÖ”‚É‚æ‚è}‚QD‚W‚Ìó‘Ô‚ð•\Œ»‚·‚é‚ÆA

@@@ƒÐ0=I-States,ƒÐ1=n-state(ƒÐ0),ƒÐ2=n-state(ƒÐ1)=n-state(n-state(ƒÐ0))=n-state2(ƒÐ0),

@@@ƒÐ3=n-state(ƒÐ2)=n-state(n-state2(ƒÐ0))=n-state3(ƒÐ0),EEEEƒÐn= n-staten(ƒÐ0)

@@@¡An-state0‚ðP“™ŠÖ”‚Æ‚·‚é‚ÆAn=0,1,2,EEE‚ɑ΂µ‚ÄAƒÐn= n-staten(ƒÐ0)‚Æ‚È‚éB

@@@‚·‚È‚í‚¿A”CˆÓ‚Ìó‘Ԃ͉Šúó‘Ô‚Æn-stateŠÖ”‚©‚çì‚邱‚Æ‚ª‚Å‚«‚éB

@@@‚±‚±‚ÅAiƒvƒƒOƒ‰ƒ€‚ªŽû‘©‚µjÅIó‘Ô‚ª‚ ‚é‚Æ‚µ‚ÄA‚±‚ê‚ðn-state‚Æ‚·‚é‚ÆA

@@@n-state= n-state(n-state(EEE(ƒÐ0))EE)‚Å‚ ‚éB

@@@‚±‚ê‚ÍAó‘Ôs‚ÆŽŸ‚Ìó‘Ô‚ð‘Ήž‚³‚¹‚éŠÖ”F(s)=n-state(s)‚ÌŬ•s“®“_‚Å‚ ‚éB

@@@‚·‚È‚í‚¿An-state=F(n-state)@@iF‚͔Ċ֔j

@[ŋ߂̘_•¶‚©‚ç‚Ì’Žß]

@2000”N‚ÌP. Cousot‚̘_•¶u’ŠÛ‰ðŽßF‚»‚Ì’B¬‚Æ“W–]vi•¶Œ£‚ÌNO.‚P‚Oj‚Å‚ÍAƒvƒƒOƒ‰ƒ€‚Ì‘€ì“IƒZƒ}ƒ“ƒeƒBƒNƒX‚É‚æ‚èAƒgƒŒ[ƒXƒÐ0¨ƒÐ1¨ƒÐ2¨ EEEEE ¨ƒÐ303‚ð‹‚߂邱‚Æ‚ðA

u‚±‚̃gƒŒ[ƒX‚ɉˆ‚Á‚ÄŒ»‚ê‚éó‘Ô‚ÌW‡‚É‚æ‚éƒgƒŒ[ƒX‚Ì’ŠÛ‚Å‚ ‚éFƒ¿S(ƒÐ)={ƒÐkF k¸[0, |ƒÐ|]}v

‚Æl‚¦‚Ä‚¢‚éB‚µ‚½‚ª‚Á‚ÄA}‚QD‚W‚Ì—á‚ÍA|ƒÐ|=303‚È‚Ì‚Å

ƒ¿S(ƒÐ) = {ƒÐk F k¸[0, |ƒÐ|]}={ƒÐk F k¸[0, 303]} = {ƒÐ0,ƒÐ1,ƒÐ2,EEE,ƒÐ302,ƒÐ303 }‚Æ‚È‚éB

@ŽŸ‚ÉAƒvƒƒOƒ‰ƒ€‚Ì•Ï”‚Ì‘©˜_‚ð“WŠJ‚·‚邽‚ß‚É

@@@@EƒRƒ“ƒeƒLƒXƒg(Context)

@@@@EƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹(Context-Vector)

@@@@En-ƒRƒ“ƒeƒLƒXƒg(n-context)ŠÖ”

@@@@EF-contŠÖ”

@‚Æ‚¢‚¤ŠT”O‚ª“oê‚·‚éB

i‚TjƒRƒ“ƒeƒLƒXƒg(Context)

@@‚±‚ê‚Í‘S‚Ẳ”\‚Ȋ‹«‚ÌW‡‚Å‚ ‚èAƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgi‚·‚È‚í‚¿AŒÊ(Arc)j‚É•t‚¯‚ç‚ê‚Ä‚¢‚é;

@@@Context = 2Env@@@iƒRƒ“ƒeƒLƒXƒg‚͊‹«Env‚̃xƒLW‡j

@ƒtƒ[‚Ì—á‚Å‚ÍAEnv={e(x)=0, e(x)=1, e(x)=2,EEE(,e(x)=100)}‚È‚Ì‚ÅA

@@@@Context‚ÍAEnv={e(x)=0, e(x)=1, e(x)=2,EEE(,e(x)=100)}‚Ì‘S‚Ä‚Ì•”•ªW‡‚ÌW‡

¡ƒRƒ“ƒeƒLƒXƒgCq

@@ƒRƒ“ƒeƒLƒXƒgCq‚Ƃ̓vƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgq(¸Arcs)‚ł̃Rƒ“ƒeƒLƒXƒg‚Ì‚±‚Æ‚Å‚ ‚éB

@‚·‚È‚í‚¿AƒvƒƒOƒ‰ƒ€‚̉”\‚ÈŒvŽZƒV[ƒPƒ“ƒX‚É‚¨‚¢‚Äq‚ÉŠÖŒW‚·‚é‘S‚Ă̊‹«‚ÌW‡‚Å‚ ‚èA‰º‹L

@‚ÌŽ®‚Å•\‚³‚ê‚éG

@@@Cq={ e | <q, e>=n-statesn(i)‚Æ‚È‚én†0‚Æi¸I-States‚ª‘¶Ý‚·‚é}

@‚±‚ê‚Íq‚ðŒÅ’肵‚Äã‹L‚ÌŽ®‚ð–ž‚½‚·n‚ª‘¶Ý‚·‚ê‚΂悢‚Ì‚ÅA<q, e>=n-states(ƒÐ0), n-states2(ƒÐ0),

@n-states3(ƒÐ0),EEE, n-statesn(ƒÐ0)‚Ìó‘Ԃɑ΂·‚éŠÂ‹«e‚ÌW‡‚Æ‚È‚éB

@i—ájŽ–—á‚̃vƒƒOƒ‰ƒ€‚Å‚ÍA

@@@@Eq=r1‚Ì‚Æ‚«ACr1={e(x)=ƒ³}

@@@@Eq=r4‚Ì‚Æ‚«A

@@@@Cr4‚ÍA{ e(x)=1,@@@@@©in=4,‚·‚È‚í‚¿n-states4(ƒÐ0),ƒÐ0¸I-State‚Ìê‡j

@@@@@@@@@e(x)=2,@@@@@©in=7,‚·‚È‚í‚¿n-states7(ƒÐ0)‚Ìê‡j

@@@@@@@@@e(x)=3 ,@@@@@@©in=10,‚·‚È‚í‚¿n-states10(ƒÐ0)‚Ìê‡j

@@@@@@@@@EEE }–”‚Í‚±‚ê‚Ì•”•ªW‡

@@@@@Ë}‚QD‚W‚Ìó‘Ԃ̕ω»—á‚ƑΔ䂷‚é‚Æ•ª‚©‚èˆÕ‚¢B

@i‚UjƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹(Context-Vector) (Cv)

@@‚±‚ê‚ÍŠeƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgq¸Arcs‚ɃRƒ“ƒeƒLƒXƒg‚ðŠÖŒW‚³‚¹‚éƒxƒNƒgƒ‹‚Å‚ ‚èA‰º‹L‚ÌŽ®‚Å’è‹`

@‚³‚ê‚éG@ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv= (Cv(r0),Cv(r1),Cv(r2),EEE,Cv(q),EEEj

@@@@@@@@@@@@@@@@@@@@@= (Cr0, Cr1, Cr2,EEE,Cq,EEEj

@@@@@‚±‚±‚ÅACv(q)={ e | <q, e>=n-statesn(i)‚Æ‚È‚én†0‚Æi¸I-States‚ª‘¶Ý‚·‚é}(=Cq)

@@@@@@i@Cviqj‚ÍAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv‚Ì‘æq¬•ªj

@Cv(q)‚ÍŠeƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgq‚Å‹ÇŠ“I‚É’è‹`‚³‚ê‚éB

@}‚QD‚S‚Ì—á‚Å‚ÍA‰º‹L‚̂悤‚ȃxƒNƒgƒ‹‚Æ‚È‚éi}‚QD‚W‚Ìó‘Ԃ̕ω»—á‚ƑΔ䂷‚é‚Æ•ª‚©‚èˆÕ‚¢jG

@@@@@Cv= (Cv(r0),Cv(r1),Cv(r2),Cv(r3),Cv(r4),Cv(r5)j

@@@@@‚±‚±‚ÅA

@@@@@@Cv(r0)={e(x)=ƒÓ},Cv(r1)={e(x)=0}

@@@@@@@Cv(r2)={e(x)=0, e(x)=1, e(x)=2,EEE, e(x)=99, e(x)=100}–”‚Í‚±‚ê‚Ì•”•ªW‡,

@@@@@@@Cv(r3)={e(x)=0, e(x)=1, e(x)=2,EEE, e(x)=99}–”‚Í‚±‚ê‚Ì•”•ªW‡,

@@@@@@@Cv(r4)={e(x)=1, e(x)=2,EEE, e(x)=99}–”‚Í‚±‚ê‚Ì•”•ªW‡,

@@@@@@@Cv(r5)={e(x)=100}

@@@@@‚Æ‚È‚éB

@@¡ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì—v‘f‚̕ω»—á

@@@ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv‚Ì—v‘f‚̕ω»‚ð}‚QD‚X‚É}Ž¦‚µ‚Ä‚Ý‚éƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv‚Ì—v‘f‚Í

@@ƒ‹[ƒvˆ—‚Ì•”•ª‚ʼn½Žü‚·‚é‚©‚É‚æ‚è•Ï‰»‚·‚邱‚Æ‚É’ˆÓB

@@@@@@

@@@@@@@@@@@}‚QD‚X@ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì—v‘fir=ri‚ł̃Rƒ“ƒeƒLƒXƒgj‚̕ω»—á

@‚±‚±‚ÅAã‹L‚Ìà–¾’†‚Ìu–”‚Í‚±‚ê‚Ì•”•ªW‡v‚Æ‚¢‚¤ˆÓ–¡‚ÍAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ªƒ‹[ƒvˆ—‚Ì

•”•ª‚Å‚ÍAƒ‹[ƒv‚̉ñ”‚É‚æ‚èŒÊr‚ɑ΂µ‚ĈقȂéƒRƒ“ƒeƒLƒXƒgi•”•ªW‡j‚ƂȂ邱‚Æ‚ðŽw‚µ‚Ä‚¢‚éB

¨‚±‚Ì‚±‚Æ‚ÍAƒ‹[ƒv‚̉ñ”‚É‚æ‚èƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Í•¡”‘¶Ý‚µ•ïŠÜŠÖŒW‚É‚ ‚邱‚Æ‚ðŽ¦‚µ‚Ä‚¢‚éB

@—Ⴆ‚ÎACv1‚ðƒ‹[ƒv‚P‰ñ–ڂ̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹ACv2‚ðƒ‹[ƒv2‰ñ–ڂ̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Æ‚·‚é‚ÆA}‚QD‚X‚Å‚ÍA

@@Cv1=(Cv(r0),Cv(r1),ƒ‹[ƒv‚P‰ñ–Ú‚ÌCv(r2),ƒ‹[ƒv‚P‰ñ–Ú‚ÌCv(r3),ƒ‹[ƒv‚P‰ñ–Ú‚ÌCv(r4),Cv(r5)j

@@@@=({e(x)=ƒÓ}, {e(x)=0}, {e(x)=0}, {e(x)=0}, {e(x)=1}, {e(x)=ƒÓ})@©ƒxƒNƒgƒ‹‚Ì•À‚Ñ‚ÍŒÊri‚̔Ԇ‡(i=0,1,2,3,4,5)

@@Cv2=(Cv(r0),Cv(r1),ƒ‹[ƒv2‰ñ–Ú‚ÌCv(r2),ƒ‹[ƒv2‰ñ–Ú‚ÌCv(r3),ƒ‹[ƒv2‰ñ–Ú‚ÌCv(r4),Cv(r5)j

@@@@=({e(x)=ƒÓ}, {e(x)=0}, {e(x)=0, e(x)=1}, {e(x)=0, e(x)=1}, {e(x)=1, e(x)=2}, {e(x)=ƒÓ})

@‚Æ‚È‚èA”CˆÓ‚Ìr=r1,r2,r3,r4,r5‚ɑ΂µ‚ÄACv1(r)ºCv2(r)‚Æ‚È‚éB

@‚µ‚½‚ª‚Á‚ÄAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌW‡‚͉º‹L‚Ì”¼‡˜º`‚Ƙa¾`‚𓱓ü‚·‚邱‚Æ‚É‚æ‚è‘©‚É‚È‚éG

@@@Cvi, Cvj‚ð‚Q‚‚̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Æ‚·‚é‚Æ‚«A

@@@@E”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄA(Cviº`Cvj)(r)‚ðCvi(r)ºCvj(r)‚Æ‚·‚邱‚Æ‚É‚æ‚èƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì

@@@@ ”¼‡˜Cviº`Cvj‚ð’è‹`‚·‚éB

@@@@E”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄA(Cvi¾`Cvj)(r)=Cvi(r)¾Cvj(r)‚É‚æ‚èƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹ŠÔ‚Ì

@@@@ ˜a‚ð’è‹`‚·‚éB

@@@@[Ø–¾]‡@º`‚Í”¼‡˜‚Å‚ ‚éG

@@@@@@@@(i)”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄACvi(r)ºCvi(r)‚È‚Ì‚ÅCviº`Cvi‚Å‚ ‚éB

@@@@@@@@(ii)Cviº`Cvj‚©‚ÂCvjº`Cvk‚È‚ç‚ÎA”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄA

@@@@@@@@@Cvi(r)ºCvj(r),Cvj(r)ºCvk(r)‚È‚Ì‚ÅACvi(r)ºCvj(r)ºCvk(r)‚æ‚èCvi(r)ºCvk(r)

@@@@@@@@@@@@‚µ‚½‚ª‚Á‚ÄACviº`Cvk‚Æ‚È‚éB

@@@@@@@@(iii)Cviº`Cvj‚©‚ÂCvjº`Cvi‚È‚ç‚ÎA”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄA

@@@@@@@@@@@@Cvi(r)ºCvj(r),Cvj(r)ºCvi(r)‚È‚Ì‚ÅACvi(r)=Cvj(r)‚Æ‚È‚éB

@@@@@@@@@@‚µ‚½‚ª‚Á‚ÄACvi=Cvj‚Æ‚È‚éB

@@@@@@@‡AƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌW‡(Cv,º`)‚Í‘©‚Å‚ ‚éG

@@@@@@@@”CˆÓ‚Ìr¸Arcs‚ÆACvi,Cvj¸(Cv,º`)‚ɑ΂µ‚ÄA

@@@@@@@@ãŒÀ¾{Cvi,Cvj}=(Cvi¾`Cvj)(r)=Cvi(r)¾Cvj(r)‚ª‘¶Ý‚·‚邽‚ßB

@@@@@@@@‰ºŒÀ‚Í¿{Cvi,Cvj}=Cvi(r)¿Cvj(r)‚Ål‚¦‚ê‚΂悢i’jB@

@@@@@@@@i’jƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì’P’²‘‰Á‚¾‚¯‚ðl‚¦‚é‚È‚ç‚ΉºŒÀ‚Í•s—vB

@@@@@@@@@@@¾`‚݂̂̂悤‚Éjoin‚Æmeet‚Ì‚Ç‚¿‚ç‚©ˆê•û‚µ‚©•K—v‚Æ‚µ‚È‚¢‘©‚ð

@@@@@@@@@@@”¼‘©(semi-lattice)‚Æ‚¢‚¤B

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(Q.E.D)

@ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚̓‹[ƒvˆ—‚̉ñ”‚É‚æ‚è’P’²‘‰Á‚·‚邪AƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌW‡‚Ì

ƒgƒbƒvT`‚ƃ{ƒgƒ€Û`‚ÍŽŸ‚̂悤‚É’è‹`‚³‚ê‚éG

@@@@@@@@@”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄAT`(r)=Env

@@@@@@@@@@@”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄAÛ`(r)=ƒÓ

‚±‚Ì‚Æ‚«AƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌW‡‚É{ T``}‚ð•t‰Á‚µ‚½‚à‚Ì‚ð‰ü‚߂ăRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌW‡

‚Æ‚·‚é‚ÆA”CˆÓ‚̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv‚ɑ΂µ‚ÄA

@@@@@@@@@@@@@@@@@@@@Û` º`Cvº`T`

‚±‚Ì‚Æ‚«AƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì”CˆÓ‚ÌW‡‚ÍãŒÀA‰ºŒÀ‚ðŽ‚‚̂Ŋ®”õ‘©‚Æ‚È‚éB

i‚Vjn-contextŠÖ”

@i‚Tj‚ł̓vƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgq‚ł̃Rƒ“ƒeƒLƒXƒgCq‚ð’è‹`‚µ‚½BˆÈ~‚ł̓vƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚ƌʂ𓯈ꎋ‚µ‚ÄAŒÊr‚ł̃Rƒ“ƒeƒLƒXƒgCr‚Æ‚¢‚¤Œ¾‚¢•û‚ð‚·‚éB

@ƒvƒƒOƒ‰ƒ€‚̈Ӗ¡‚©‚çŒÊr‚ł̃Rƒ“ƒeƒLƒXƒgCr‚ÍAŒÊr‚É(r'‚ÌI’[ƒm[ƒh=r‚ÌŽn’[ƒm[ƒhj‚Æ‚¢‚¤ðŒ‚Å—×Ú‚·‚éŒÊr'‚̃Rƒ“ƒeƒLƒXƒgCr'‚ÆA‚»‚ê‚ç‚̌ʂ̊Ԃ̃Xƒe[ƒgƒƒ“ƒg‚É‚æ‚èC³‚³‚ꂽ‚à‚Ì‚ÅŒˆ‚Ü‚éi}‚QD‚P‚OŽQÆjB

@@@@@@@@

@@@@@@@@@@@}‚QD‚P‚O@ŒÊr‚Æ‚»‚Ì‘O‚É—×Ú‚·‚éŒÊ‚̃Rƒ“ƒeƒLƒXƒg‚Æ‚ÌŠÖŒW

@‚»‚±‚ÅAŒ»Ý‚ÌŒÊr‚ł̃Rƒ“ƒeƒLƒXƒgCr=Cv(r)‚ðAŒÊr‚ÌŠJŽnƒm[ƒh‚ªI’[ƒm[ƒh‚Æ‚È‚é—×Ú‚µ‚½ŒÊ‚̃Rƒ“ƒeƒLƒXƒg‚ÆA‚»‚ê‚ç‚̌ʂ̊Ԃ̃Xƒe[ƒgƒƒ“ƒg‚©‚ç‹‚ß‚éŠÖ”‚ðl‚¦A‚»‚ê‚ðn-context (n-‚Ínext‚̈Ӗ¡j‚Å’è‹`‚·‚éG@

@@@@@@@@@@Cr=Cv(r) = n-context(r, Cv)

‚·‚È‚í‚¿An-context‚ÍuCv(r)‚ðŽŸ‚ÌƒRƒ“ƒeƒLƒXƒg‚Æ‚·‚év‚悤‚ȃRƒ“ƒeƒLƒXƒg‚Å•\‚·ŠÖ”‚Å‚ ‚éB

@@@@@@i—áj}‚QD‚P‚O‚Ì—á‚Å‚ÍACr2=Cv(r2)=n-context(r2,Cv)=Cr1¾Cr4

@@@@@@@@@@@@@@@@@@@@@@@@@@@Cr4=Cv(r4)=n-context(r4,Cv)=Cr3¿{x=x+1}

‚Ü‚½An-contextŠÖ”‚̓vƒƒOƒ‰ƒ€‚̃Xƒe[ƒgƒƒ“ƒg‚ðƒRƒ“ƒeƒLƒXƒg‚É”½‰f‚·‚é‚Ì‚ÅAuƒvƒƒOƒ‰ƒ€‚ÌŠî–{–½—ßiƒXƒe[ƒgƒƒ“ƒgj‚̉ðŽßv‚Æl‚¦‚ç‚ê‚éB

ËCousot‰Šú˜_•¶‚Ì5.1ß‚Å‚ÍA‚±‚ê‚ÉŠÖ‚µ‚ĉº‹L‚Ì‹Lq‚ª‚ ‚éG

@@uThe local interpretation of elementary program constructs which is defined by n-context is used to

@@ associate a system of equations with the program.in-context‚É‚æ‚è’è‹`‚³‚ê‚éƒvƒƒOƒ‰ƒ€‚Ì‹ÇŠ“I

@@@‰ðŽß‚̓vƒƒOƒ‰ƒ€‚ÌŽ®‚̃VƒXƒeƒ€‚ÉŠÖ˜A‚³‚¹‚邽‚ß‚ÉŽg—p‚³‚ê‚éjv

@ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌW‡‚Í”¼‡˜º`‚ƾ`‚É‚æ‚è‘©‚ƂȂ邪A‚±‚±‚ÅAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv‚ª—^‚¦‚ç‚ꂽ‚Æ‚«AuCv‚ðŽŸ‚ÌƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Æ‚·‚év‚悤‚ȃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ð‹‚ß‚éŠÖ”‚ðl‚¦A‚±‚ê‚ðF-cont‚Æ‚·‚éB‚·‚È‚í‚¿A”CˆÓ‚Ìr¸Arcs‚ɑ΂µA

@@@@@@@F-cont(Cv)(r)=n-context(r,Cv)@‚ ‚é‚¢‚ÍAF-cont(Cv(r))= n-context(r,Cv)

‚Å‚ ‚éB‚±‚Ì‚Æ‚«AF-cont‚̓Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì”¼‡˜º`‚ÉŠÖ‚µ‚ć˜•Û‘¶‚Å‚ ‚éG

@@@@@@@Cv1º`Cv2@‚È‚ç‚ÎAF-cont(Cv1` F-cont(Cv2)

@@[Ø–¾]Cv1º`Cv2@‚È‚ç‚ÎA”CˆÓ‚Ìr¸Arcs‚ɑ΂µA

@@@@@@@@F-cont(Cv1)(r)= n-context(r,Cv1)= Cv1(r)ºCv2(r)=n-context(r,Cv2)= F-cont(Cv2)(r)@

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(Q.E.D)

@ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì’P’²‘‰Á—ñFÛ`º`Cv1º`Cv2º`Cv3º`EEEE‚É‚¨‚¢‚ÄA

@F-cont‚ðl‚¦‚é‚ÆAF-cont‚ͺ`‚ÉŠÖ‚µ‚ć˜•Û‘¶‚È‚Ì‚ÅF-cont‚ÍŠ®”õ‘©ã‚Ì’P’²‘‰ÁŠÖ”

‚Æ‚È‚éB‚µ‚½‚ª‚Á‚ÄAƒ^ƒ‹ƒXƒL‚Ì•s“®“_’è—‚æ‚èAF-cont‚Í•s“®“_Cv‚ðŽ‚ÂGF-cont(Cv) =Cv

@@‚±‚ÌCv‚̓vƒƒOƒ‰ƒ€‚Ì•Ï”x‚ÌŽæ‚蓾‚é’l‚ÌÅ‘å’l‚Æ‚È‚èAƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚Ɉˑ¶‚µ‚È‚¢

@ƒvƒƒOƒ‰ƒ€‚Ì‘åˆæ“I‚È«Ž¿‚Å‚ ‚éi’jB

@@i’jCousot‰Šú˜_•¶‚Ì—v–ñ‚Å‚ÍA‚±‚Ì‚±‚Æ‚ª‰º‹L‚̂悤‚É‘‚©‚ê‚Ä‚¢‚éG

@@@@uThe program global properties are defined as one of the extreme fixpoints of that, Tarski.

@@@@iƒvƒƒOƒ‰ƒ€‚̃Oƒ[ƒoƒ‹‚È«Ž¿‚̓^ƒ‹ƒXƒL‚Ì•s“®“_‚̈ê‚‚Ƃµ‚Ä’è‹`‚³‚ê‚éBjv

@[ŋ߂̘_•¶‚©‚ç‚Ì’Žß]

@ƒRƒ“ƒeƒLƒXƒg‚ƃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚͉Šú‚Ì’ŠÛ‰ðŽß‚̘_•¶‚É‚¨‚¯‚é”ñí‚Éd—v‚ÈŠT”O‚Å‚ ‚邪A

2000”N‚ÌP. Cousot‚̘_•¶u’ŠÛ‰ðŽßF‚»‚Ì’B¬‚Æ“W–]v‚Å‚ÍAŽŸ‚̂悤‚ÈŽ®‚Æ‚µ‚Ä•\Œ»‚³‚ê‚é‚悤‚É

‚È‚Á‚½i‚·‚È‚í‚¿A‚»‚±‚ł̓Rƒ“ƒeƒLƒXƒg‚âƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Æ‚¢‚¤Œ¾—t‚Í‚à‚Í‚â•\‚Éo‚È‚­‚È‚Á‚½jG

u’ŠÛ‰ðŽß‚̋ߎ—‚ªŽÀÛ‚ÉŽg—p‚µ‚Ä—LŒø‚Å‚ ‚é‚Æ‚¢‚¤‚±‚Ƃ𒼊´“I‚ÉŽ¦‚·‚½‚ß‚ÉAˆÀ‘S«‚̉ðÍ(safty analysis)‚ðl‚¦‚éBiƒ‰ƒ“ƒ^ƒCƒ€ƒGƒ‰[‚ª‘¶Ý‚µ‚È‚¢‚Æ‚¢‚¤‚悤‚ÈjˆÀ‘S«‚Æ‚¢‚¤«Ž¿‚ÍA‰½‚©ˆ«‚¢‚±‚Æ‚Í‹N‚«‚È‚¢A‚Ü‚½‚̓vƒƒOƒ‰ƒ€‚ÌŽÀs‚ÍŒ’‘S‚Èó‘Ô‚Ì‚Ü‚Ü‚Å‚ ‚éA‚Æ‚¢‚¤‚±‚Æ‚ð‹K’è‚·‚éB‚±‚ÌŠT”O‚͈ȉº‚Åà–¾‚·‚é‚悤‚É’ŠÛ‚Ì•¡‡(composition)‚É‚æ‚è’莮‰»‚Å‚«‚éBʼn‚Ì’ŠÛ‚ÍA‚±‚̃gƒŒ[ƒX‚ɉˆ‚Á‚ÄŒ»‚ê‚éó‘Ô‚ÌW‡‚É‚æ‚éƒgƒŒ[ƒX‚Ì’ŠÛ‚Å‚ ‚éFƒ¿S(ƒÐ)={ƒÐk F k¸[0, |ƒÐ|]}

ƒgƒŒ[ƒX‚ÌW‡X‚̋ߎ—‚ÍAW‡X‚Ì­‚È‚­‚Æ‚àˆê‚‚̃gƒŒ[ƒX‚ð•\‚·ó‘Ô‚ÌW‡‚Å‚ ‚éF

@@@@@@@@@@@ƒ¿S(X)=¾ƒÐ¸Xƒ¿S(ƒÐ)

ƒ¿S(X)‚ª•s•Ï(invariant)‚Å‚ ‚é‚Æ‚ÍAƒvƒƒOƒ‰ƒ€‚ðŽÀs‚µ‚ĉŠúó‘Ô‚©‚ç“ž’B‰Â”\‚È‘S‚Ä‚Ìó‘Ô‚ª‚»‚Ì«Ž¿‚ð–ž‚½‚³‚È‚¯‚ê‚΂Ȃç‚È‚¢‚Æ‚¢‚¤‚±‚Æ‚ðˆÓ–¡‚·‚éB

@ó‘Ôs‚ÍAƒvƒƒOƒ‰ƒ€C‚̃vƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgl (¸C)‚ÆA®”’l(x1, ... ,xn)¸Z‚ðŽæ‚éƒvƒƒOƒ‰ƒ€C‚Ì•Ï”X1, ... ,Xnix1¸X1, ... , xn¸Xn)‚ðŽw’è‚·‚駌äó‘Ô‚©‚ç\¬‚³‚ê‚Ä‚¢‚é‚Æ‚·‚éB‘å‹Ç“I‚È•s•ÏŽ®

ƒ¿S(X)‚ÍA‚»‚̃|ƒCƒ“ƒg‚ÅŠeƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚Æ•Ï”‚̉”\‚È’l‚Ì‘g‚ÌW‡‚ðŠÖŒW‚¯‚éA‹ÇŠ“I‚È•s•ÏŽ®‚̃xƒNƒgƒ‹‚É“¯Œ^(isomorphic)‚Å‚ ‚éF

@@@@@@@@@@@@ƒ¿l(Y)=ƒ®l¸C{(x1, ... ,xn)F(l, (x1, ... ,xn))¸Y}@EEEEiŽ®‚Pj

‚±‚̂悤‚ɃgƒŒ[ƒX‚̃vƒƒOƒ‰ƒ€W‡‚ÌŒvŽZ‚ÍnŽŸŒ³®”‹óŠÔZn‚Ì“_‚ÌW‡‚É‚æ‚è‹ßŽ—‚³‚ê‚éBv

‚±‚Ì’è‹`‚ðCousot‚̉Šú˜_•¶‚Å‚Ìuó‘Ôv‚Ì’è‹`‚ƑΔ䂷‚é‚ÆA

ó‘ÔState‚Í<Arc, Env>‚Ì‘g‚Å‚ ‚èAƒvƒƒOƒ‰ƒ€ŽÀsŽž‚Ì‚ ‚éƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚ł̃vƒƒOƒ‰ƒ€‚Ìó‘Ô‚ðŽ¦‚·iStates = Arcs~EnvjB¨}‚QD‚P‚PŽQÆB

@@@

@@@@@@@@@@@@}‚QD‚P‚P@ó‘Ô‚Ìà–¾

@@iŽ®‚Pj‚Íã‹L‚Ì—á‚Ìê‡AC={r0, r1, r2, r3, r4, r5, r6"A®”’lx¸Env=ZAY‚Íó‘Ô‚ÌW‡‚Å‚ ‚èA

@@@@ƒ¿l(Y)=ƒ®l¸C{(x1, ... ,xn)F(l, (x1, ... ,xn))¸Y}=ƒ®l¸C{ x¸ZF(l, x)¸Y}

@@@@@¨‚±‚ÌŽ®‚̈Ӗ¡‚ðCousot‚̉Šú˜_•¶‚ÌŒ¾—t‚Å•\Œ»‚·‚é‚ÆA

@@@@@@{ x¸ZF(l, x)¸Y}@Ì@ƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgl‚ł̃Rƒ“ƒeƒLƒXƒgCl‚Ì‚±‚ÆB

@@@@ŠeƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒgl¸C‚ɃRƒ“ƒeƒLƒXƒg‚ðŠÖŒW‚³‚¹‚éƒxƒNƒgƒ‹‚ªƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚È‚Ì‚ÅA

@@@@@@ƒ®l¸C{ x¸ZF(l, x)¸Y}@Ì@ƒvƒƒOƒ‰ƒ€C‚̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì‚±‚ÆB

@@@‚±‚̂悤‚ɉŠú˜_•¶‚̃Tƒ“ƒvƒ‹ƒvƒƒOƒ‰ƒ€‚̃gƒŒ[ƒX‚Í1ŽŸŒ³®”‹óŠÔZ‚Ì“_‚ÌW‡‚É‚æ‚è‹ßŽ—

@@@‚³‚ê‚éB

‚QD‚Q@ƒvƒƒOƒ‰ƒ€‚Ì’ŠÛ‰ðŽß@@@@@@@@@@@@@@@@@@@@@@

@‚QD‚Pß‚Å‚ÍAƒvƒƒOƒ‰ƒ€‚Ì•Ï”‚ÌŽæ‚é’l‚É’…–Ú‚µ‚ÄAƒRƒ“ƒeƒLƒXƒg‚ƃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Æ‚¢‚¤‚Q‚‚̊T”O‚𓱓ü‚µAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì•s“®“_‚ð‹‚߂邱‚Æ‚ð‹c˜_‚µ‚½B‚±‚±‚Å‚ÍA‚±‚ê‚ç‚ÌŠT”O‚ðŒ³‚É’ŠÛ‰ðŽß‚ðƒtƒH[ƒ}ƒ‹‚É’è‹`‚·‚éB‚Ü‚½A‚æ‚è’Pƒ‰»‚³‚ꂽ¢ŠE‚ŃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì•s“®“_‚ð‹‚߂邽‚ß‚ÉA“¯‚¶ƒvƒƒOƒ‰ƒ€P‚ɑ΂·‚é•¡”‚Ì’ŠÛ‰ðŽßŠÔ‚̃KƒƒAÚ‘±‚ª“oê‚·‚éBi‚±‚Ìß‚ÍCousot‰Šú˜_•¶‚Ì‚Tß`‚Wß‚ÉŠY“–j

‚QD‚QD‚P@ƒRƒ“ƒeƒLƒXƒg‚ƃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÉŠÖŒW‚·‚逖Ú

@‚QD‚Pß‚©‚çAƒRƒ“ƒeƒLƒXƒg‚ƃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì¢ŠE‚ð“Á’¥•t‚¯‚逖ڂ𮗂·‚é‚ÆA‰º‹L‚̂悤‚É‚È‚èAŠe€–Ú‚ª‘Ήž‚µ‚Ä‚¢‚éG

‡@ƒRƒ“ƒeƒLƒXƒg‚ÉŠÖŒW‚·‚逖ڂÍA

@EContexts

@iE˜a¾j@@@@@i’F‚QD‚Pß‚Å‚ÍA¾‚;`‚Ì’è‹`‚Ì‚½‚ß‚ÉŽg—p‚µ‚½j

@iE”¼‡˜ºj@@i’F‚QD‚Pß‚Å‚ÍAº‚ͺ`‚Ì’è‹`‚Ì‚½‚ß‚ÉŽg—p‚µ‚½j

@Eő匳=EnviŠÂ‹«j

@EŬŒ³=ƒÓi‹óW‡j

@EŽŸ‚̃Rƒ“ƒeƒLƒXƒg‚ð‹‚ß‚én-contextŠÖ”

‡AƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÉŠÖŒW‚·‚逖ڂÍA

@EContext vectors

@E˜a¾`

@E”¼‡˜º`

@Eő匳= T`(”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄAT`(r)=Env )

@EŬŒ³=Û`i”CˆÓ‚Ìr¸Arcs‚ɑ΂µ‚ÄAÛ`(r)=ƒÓj

@EŽŸ‚̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ð‹‚ß‚éF-contŠÖ”

‚»‚±‚ÅA‚QD‚Qß‚Å‚ÍAã‹L‚Ì€–Ú‚ðŒ³‚Éˆê”ʉ»‚µ‚ÄA’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`‚ðs‚¤B

’A‚µA’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`‚Ì‘O‚ÉA‚»‚Ì€”õ‚Æ‚µ‚Ä‚QD‚QD‚Q‚Å”¼‘©(semilattice)‚Ì’è‹`‚ðq‚ׂéB

‚QD‚QD‚Q@”¼‘©(semilattice)

@’è‹`F@L‚ª”¼‘©‚Å‚ ‚é‚Æ‚ÍA”CˆÓ‚Ìx, y, z¸L‚ɑ΂µ‚ĉº‹L‚ð–ž‚½‚·‰‰ŽZ›‚ª

@’è‹`‚³‚ꂽ‘ã”L=(L,›j‚Ì‚±‚Æ‚Å‚ ‚éG

@@@@(i)@x›x=x

@@@@(ii)@x›y=y›x

@@@@(iii)@x›(y›z)=(x›y)›z

@‚±‚Ì‚Æ‚«A‰º‹L‚Ì’è—‚ª¬—§‚·‚éG

@’è—F@”¼‘©L‚É‚¨‚¢‚ÄA‡˜xy‚ðx›y=y‚É‚æ‚è’è‹`‚·‚é‚ÆA(L,)‚Í”CˆÓ‚Ì—v‘f‚Ì‘g

@‚ªãŒÀ‚ðŽ‚”¼‡˜W‡‚É‚È‚éi’jB

@Ø–¾F@‚Ü‚¸A‚ª”¼‡˜‚Å‚ ‚邱‚Æ‚ðŽ¦‚·G

@@@@(i) x›x=x‚Í’è‹`‚æ‚èxx‚ðˆÓ–¡‚µ‚Ä‚¢‚éB

@@@@(ii) xy‚©‚Âyx‚È‚ç‚ÎAx›y=y‚©‚Ây›x=x‚µ‚½‚ª‚Á‚ÄAx= y›x= x›y=y‚Æ‚È‚èAx=y

@@@@(iii) xy‚©‚Âyz‚È‚ç‚ÎAx›z= x›(y›z)= (x›y)›z=y›z=z@]‚Á‚ÄAxz

@@@@ŽŸ‚ÉAx›(x›y)=(x›x)›y=x›y‚È‚Ì‚ÅAxx›y

@@@@“¯—l‚ÉAy›(x›y)=y›(y›x)= (y›y)›x= y›x= x›y‚È‚Ì‚ÅAyx›y

@@@@‚µ‚½‚ª‚Á‚ÄAx›y‚Í{x, y}‚ÌãŠE‚Å‚ ‚éB

@@@@¡Axz, yz‚Æ‚·‚é‚ÆA(x›y)›z=x›(y›z)=y›z=z‚È‚Ì‚ÅA(x›y)z

@@@@‚µ‚½‚ª‚Á‚ÄAx›y‚Í{x, y}‚ÌãŒÀ‚Å‚ ‚éB

@@@i’j“¯—l‚É‚µ‚ÄAyx‚ðx›y=x‚É‚æ‚è’è‹`‚·‚é‚ÆA(L,)‚Í”CˆÓ‚Ì—v‘f‚Ì‘g‚ª‰ºŒÀ‚ðŽ‚Â

@@@@@@”¼‡˜W‡‚É‚È‚é

ˆÈã‚Ì€”õ‚ðŒ³‚ÉŽŸ‚Ì‚QD‚QD‚R‚Å’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`‚ð—^‚¦‚éB

‚QD‚QD‚R@’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`

@‚QD‚QD‚Pß‚©‚çAƒRƒ“ƒeƒLƒXƒg‚Ì¢ŠE‚ð‹K’è‚·‚逖ڂð‘g(tuple)‚ÌŒ`Ž®‚Å•\‚·‚ÆA

@@@@@@@ƒContexts,i¾j,iºj,Env,ƒÓ, n-context„

‚Æ‚È‚éB‚±‚ê‚Í”¼‡˜º‚ÉŠÖ‚µŠ®”õ‘©‚Æ‚È‚Á‚Ä‚¢‚éiő匳‚ÍEnv,ŬŒ³‚̓ÓjB

@ƒvƒƒOƒ‰ƒ€P‚Ì’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`‚ÍA‚±‚ê‚ðˆê”ʉ»‚µ‚½‚à‚Ì‚Å‚ ‚éG

’è‹`F@ƒvƒƒOƒ‰ƒ€P‚Ì’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`‚Æ‚ÍA‰º‹L‚Ì‘g‚Ì‚±‚Æ‚Å‚ ‚éG

@@@@@@@@@I=ƒA-Cont,›,, T,Û, Int„

@@‚±‚±‚ÅA

@@EA-ContFƒvƒƒOƒ‰ƒ€P‚Ì’ŠÛƒRƒ“ƒeƒLƒXƒgi’j‚ÌW‡B

@@@@@@i’jƒvƒƒOƒ‰ƒ€‚̃Rƒ“ƒeƒLƒXƒg‚̓vƒƒOƒ‰ƒ€‚Ì‘S‚Ẳ”\‚Ȋ‹«‚ÌW‡‚Å‚ ‚邪A

@@@@@@@’ŠÛƒRƒ“ƒeƒLƒXƒg‚̓Rƒ“ƒeƒLƒXƒg‚»‚Ì‚à‚Ì‚Å‚à‚æ‚¢‚µA‚±‚ê‚ð’Pƒ‰»‚µ‚½‚à‚Ì‚Å‚à‚æ‚¢B

@@@@@@@—Ⴆ‚ÎA‚ ‚éƒvƒƒOƒ‰ƒ€ƒ|ƒCƒ“ƒg‚Å•Ï”‚˜‚ª{0, 1, 2, 3, 4, 5}‚Ì’l‚ðŽæ‚蓾‚éê‡A

@@@@@@@‚±‚ê‚ð’Pƒ‰»‚µ‚Ä—¼’[‚Ì[0, 5]‚ðl‚¦‚é‚È‚ÇB@

@@E›‚ÆF›‚Í@(i) x›x=xA(ii) x›y=y›xA(iii)x›(y›z)=(x›y)›z‚ð–ž‚½‚·‰‰ŽZB

@@@@@@@@‚ÍxyÌx›y=y‚É‚æ‚è’è‹`‚³‚ꂽ”¼‡˜‚Å‚ ‚èAƒA-Cont,

@@@@@@@@‚ÍŠ®”õ›|”¼‘©‚Å‚ ‚éB

@@@@@@@@¨A-Cont‚Ìő匳‚ÍTB‚Ü‚½AA-Cont‚ÍŬŒ³Û‚ðŽ‚‚à‚Ì‚Æ‚·‚éB

@@ETFA-cont‚̃gƒbƒvAÛFA-Cont‚̃{ƒgƒ€

@@EIntFƒvƒƒOƒ‰ƒ€‚o‚ÌŒÊ(arc) r‚Æ’ŠÛƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹A-Cont`i’j‚ð“ü—Í‚Æ‚µAƒvƒƒOƒ‰ƒ€P

@@@‚Ì’ŠÛƒRƒ“ƒeƒLƒXƒg‚ð•Ô‚·ŠÖ”B

@@@i’j’ŠÛƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÍAŠeŒÊr‚ɑ΂·‚é’ŠÛƒRƒ“ƒeƒLƒXƒg‚𬕪‚Æ‚·‚éƒxƒNƒgƒ‹‚ÅA

@@@@@@@@A-Cont`ir)=Int(r,A-Cont`)

@@‚Ü‚½A‚QD‚QD‚Pß‚©‚çAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì¢ŠE‚ð‹K’è‚·‚逖ڂð‘g(tuple)‚ÌŒ`Ž®‚Å•\‚·‚ÆA

@@@@@@@ƒContext vectors,¾``,T``, F-cont„

‚Æ‚È‚éB‚QD‚Pßi‚Uj‚Å‚Ì‹c˜_‚©‚炱‚Ì‘g‚ÍŠ®”õ‘©‚É‚È‚éB

ƒvƒƒOƒ‰ƒ€P‚Ì’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`‚Å‚ÍA‚±‚̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì¢ŠE‚àŽŸ‚̂悤‚É’è‹`‚·‚éB

’è‹`@ƒvƒƒOƒ‰ƒ€P‚Ì’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`I‚ɑΉž‚·‚é’ŠÛƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌŒ`Ž®’è‹`‚Æ‚ÍA

‰E‚Ì‘g‚Ì‚±‚Æ‚Å‚ ‚éF@< A-Cont`,›`,`, T``, Int`>

‚QD‚Pßi‚Vj‚Å‚Ì‹c˜_‚©‚炱‚Ì‘g‚ÍŠ®”õ‘©‚É‚È‚éB

@’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`‚Ì€–Ú‚Æ‚QD‚Pß‚Ì—á‚Ƃ̑Ήž‚ð“Z‚ß‚é‚ÆAŽŸ‚̂悤‚É‚È‚éB’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`

‚ÌŠe€–Ú‚Ì‹ï‘Ì“IƒCƒ[ƒW‚Æ‚µ‚Ä‚»‚̑ΉžŠÖŒW‚𓪂ɓü‚ê‚Ä‚¨‚­‚Æ‚æ‚¢B

‡@ƒRƒ“ƒeƒLƒXƒg‚ÉŠÖŒW‚·‚逖ڂÍA

@ƒ’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`„@@@@@@@@@@@@@@ƒ‚QD‚Pß‚Ì—á„

@@E’ŠÛƒRƒ“ƒeƒLƒXƒgA-Cont@@@@@@@@@@@@@Ì@@EContexts

@@E‰‰ŽZ›@@@@@@@@@@@@@@@@@@@@@@@@@@@@@Ì@@@iE˜a¾j@

@@E”¼‡˜@@@@@@@@@@@@@@@@@@@@@@@@@Ì@@iE”¼‡˜ºj

@@Eő匳T@@@@@@@@@@@@@@@@@@@@@@@Ì@@Eő匳=EnviŠÂ‹«j

@@EŬŒ³Û@@@@@@@@@@@@@@@@@@@@@@Ì@@EŬŒ³=ƒÓi‹óW‡j

@@EŽŸ‚Ì’ŠÛƒRƒ“ƒeƒLƒXƒg‚ð‹‚ß‚éIntŠÖ”@@Ì@@EŽŸ‚̃Rƒ“ƒeƒLƒXƒg‚ð‹‚ß‚én-contextŠÖ”

‡AƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÉŠÖŒW‚·‚逖ڂÍA

@ƒ’ŠÛ‰ðŽß‚ÌŒ`Ž®’è‹`„@@@@@@@@@@@@@@ƒ‚QD‚Pß‚Ì—á„

@@E’ŠÛƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹A-Cont`@@@@Ì@EContext vectors

@@E‰‰ŽZ›`@@@@@@@@@@@@@@@@@@@ Ì@E˜a¾`

@@E”¼‡˜`@@@@@@@@@@@@@@@@@Ì@E”¼‡˜º`

@@Eő匳= T`@@@@@@@@@@@@@@@@@Ì@Eő匳= T`(”CˆÓ‚Ìr¸Arcs‚ɑ΂µAT`(r)=Env )

@@EŬŒ³=Û`@@@@@@@@@@@@@@@@@Ì@EŬŒ³=Û`i”CˆÓ‚Ìr¸Arcs‚ɑ΂µAÛ`(r)=ƒÓj

@@EŽŸ‚Ì’ŠÛƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ð@@@@@Ì@EŽŸ‚̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ð‹‚ß‚éF-contŠÖ”

@@@‹‚ß‚éInt`ŠÖ”@@@

‚QD‚QD‚S@’ŠÛ‰ðŽß‚̈êŠÑ«

@ˆê”Ê‚ÉAƒvƒƒOƒ‰ƒ€‚Ì’ŠÛ‰ðŽß‚Í‚P‚‚Ƃ͌À‚ç‚È‚¢i’ŠÛƒRƒ“ƒeƒLƒXƒg‚Ì—^‚¦•û‚É‚æ‚éjB‚µ‚½‚ª‚Á‚ÄA

@@@E‚æ‚èƒvƒƒOƒ‰ƒ€‚É‹ß‚¢’ŠÛ‰ðŽßi‚bj¨‚±‚ê‚ðuh‹ï‘Ìh‰ðŽßv‚Æ‚àŒ¾‚¤B

@@@E‚æ‚è’Pƒ‰»‚³‚ꂽ’ŠÛ‰ðŽßi‚`j¨‚±‚ê‚ðuh’ŠÛh‰ðŽßv‚Æ‚àŒ¾‚¤B

‚ðì‚èA‚b‚Æ‚`‚É‘©‚Ì”¼‡˜ŠÖŒW‚ð•Û‘¶‚·‚é‚悤‚È“KØ‚ÈŽÊ‘œ‚ð\¬‚·‚邱‚Æ‚ª‚Å‚«‚ê‚ÎA’Pƒ‰»‚³‚ꂽA‚Å–â‘è‚ð‰ð‚¯‚Ηǂ¢‚±‚Æ‚ªŽ¦‚³‚ê‚éB‚Q‚‚̒ŠÛ‰ðŽß‚É‚±‚̂悤‚ȑΉžŠÖŒW‚ª‚ ‚邱‚Æ‚ðu’ŠÛ‰ðŽß‚̈êŠÑ«(Consistent Abstraction Interpretations)v‚Æ‚¢‚¤B

uƒKƒƒAÚ‘±v‚Í‚±‚̑ΉžŠÖŒW‚Æ‚µ‚Ä“oê‚·‚éi}‚QD‚P‚QŽQÆjB

@@@@@@@

@@@@@@@@@}‚QD‚P‚Q@•¡”‚Ì’ŠÛ‰ðŽß

@ã‹L‚Ì‚±‚Æ‚ðŒµ–§‚É’è‹`‚·‚é‚ÆŽŸ‚̂悤‚É‚È‚éB

’è‹`i’ŠÛ‰ðŽß‚̈êŠÑ«jF@@¡AƒvƒƒOƒ‰ƒ€‚Ì‚Q‚‚̒ŠÛ‰ðŽß‚ª‚ ‚Á‚½‚Æ‚µA

@@ˆê•û‚ÍAƒvƒƒOƒ‰ƒ€‚Ìh’ŠÛh‰ðŽßI|=< A-Cont|,›|,|, T||, Int|>A

@@‘¼•û‚Íh‹ï‘Ìh‰ðŽßI = < C-Cont,›,,ƒ±,Û, Int>‚Å‚ ‚é‚Æ‚·‚éB

@@‚±‚ê‚ɑΉž‚·‚éƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì‘©‚ÍA‰º‹L‚Å‚ ‚éG

@@@@@I|‚ɑΉž‚·‚é‚à‚ÌF@< (A-Cont|)`, (›|)`, (|)`, (T|)`, (Û|)`, (Int|)`>

@@@@@I‚ɑΉž‚·‚é‚à‚ÌF@< C-Cont`,›`,`, T``, Int`>

@@‚±‚Ì‚Æ‚«Ah’ŠÛh‰ðŽßI|=< A-Cont|,›|,|, T||, Int|>‚ªA

@@h‹ï‘Ìh‰ðŽßI = < C-Cont,›,,ƒ±,Û, Int>‚ƈêŠÑ«‚ª‚ ‚é‚Æ‚¢‚¤‚±‚Æ‚ÍA

@@I|‚©‚綂¶‚éƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv|‚ªA‚æ‚èÚׂȉðŽßI‚©‚綂¶‚éƒRƒ“ƒeƒLƒXƒg

@@ƒxƒNƒgƒ‹Cv‚̳‚µ‚¢‹ßŽ—‚É‚È‚Á‚Ä‚¢‚éꇂ̂±‚Æ‚ðŒ¾‚¤B

@‚±‚±‚ÅA³‚µ‚¢‹ßŽ—‚Æ‚ÍA‰º‹L‚Ì(1),(2)‚ª¬—§‚·‚邱‚Æ‚Å‚ ‚éG

(1)ƒRƒ“ƒeƒLƒXƒg‚Ì¢ŠE‚ÅAC-Cont‚ÆA-Cont|ŠÔ‚ɃKƒƒA‘}“ü‚̑ΉžŠÖŒW‚ª‘¶Ý‚·‚éG

@‚·‚È‚í‚¿AŽÊ‘œƒ¿FC-Cont¨A-Cont|,ƒÁFA-Cont|¨C-Cont‚ɑ΂µA‰º‹L‚ª¬—§‚·‚éG

@@@@@‡@ƒ¿AƒÁ‚Í’P’²ŠÖ”‚Å‚ ‚éB@@@@@@@@@@@@@@@@EEEE(G1)

@@@@@‡A”CˆÓ‚Ìx¸C-Cont‚ɑ΂µ‚ÄAxƒÁiƒ¿ixjj@EEEE(G2)

@@@@@‡B”CˆÓ‚Ìx|¸A-Cont|‚ɑ΂µ‚ÄAx|=ƒ¿iƒÁix|jjEEEE(G3)

(2)ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Ì¢ŠE‚ÅAC-Cont`‚Æ(A-Cont|)`ŠÔ‚ɃKƒƒAÚ‘±‚ÌŠÖŒW‚ª‘¶Ý‚·‚éG

@‚·‚È‚í‚¿A‹ï‘̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚Æ’ŠÛƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹ŠÔ‚̑Ήžiƒ¿`F’ŠÛ‰»j‚Æ‹t‚̑Ήž

@iƒÁ`F‹ï‘̉»j‚ʼnº‹L‚ð–ž‚½‚·ŽÊ‘œƒ¿`,ƒÁ`‚ª‘¶Ý‚·‚邱‚Æ‚Å‚ ‚éB

@@@@@@@@@@@@@@{Cv`ƒÁ`(Cv|)}‚©‚Â{ƒ¿`(Cv)`Cv|)}EEEE(G4)@i’j

@ã‹L‚Ì’è‹`‚Å“oê‚·‚逖ڂð}Ž¦‚·‚é‚ÆA}‚QD‚P‚R‚̂悤‚É‚È‚éB

@@@@@

@@@@@@@@@@@@@@}‚QD‚P‚R@’ŠÛ‰ðŽß‚̈êŠÑ«‚ÌŠÖŒW}

i’jðŒ(G4)‚Í”CˆÓ‚Ìr‚ɑ΂µ‚Ĭ—§‚·‚é‘å‹Ç“I‚ȉ¼’肾‚ªAŽÀÛ‚É‚Í‚±‚ê‚Ì‘ã‚í‚è‚ɃvƒƒOƒ‰ƒ€‚Ì

@@‹ï‘Ì‚Æ’ŠÛ‰ðŽß‚ɂ‚¢‚Ă̈ȉº‚Ì‹ÇŠ“I‰¼’肪Žg—p‚³‚ê‚éF

@@@{”CˆÓ‚Ì(r, x|)¸Arc~(A-Cont|)`‚ɑ΂µAInt(r,ƒÁ`(x|))ƒÁ(Int|(r, x|))

@@@‚©‚Â

@@@ {”CˆÓ‚Ì(r, x)¸Arc~C-Cont`‚ɑ΂µAƒ¿(Int(r, x))|Int|(r,ƒ¿`(x))@@EEEE(G5)

@@¨(G5)‚ÍA’ŠÛƒRƒ“ƒeƒLƒXƒg‚ð‹‚ß‚éŠÖ”Int|‚ªŒ’‘S(Sound)‚Å‚ ‚邱‚Æ‚ðŽ¦‚µ‚Ä‚¢‚éB

@@@@‚·‚È‚í‚¿Ah‹ï‘Ìh‰ðŽß‚Ì¢ŠE‚Å‹‚ß‚½ƒRƒ“ƒeƒLƒXƒgInt(r, x)‚ð’ŠÛ‰»ŽÊ‘œƒ¿‚ňڂµ‚½

@@@ƒ¿(Int(r, x))‚ÍAh’ŠÛh‰ðŽß‚Ì¢ŠE‚Å‹‚ß‚½’ŠÛƒRƒ“ƒeƒLƒXƒgInt|(r,ƒ¿`(x))‚ÉŠÜ‚Ü‚ê‚éB

¡’ŠÛ‰ðŽß‚̈êŠÑ«‚ÌŽ–—á‚PF‹æŠÔ‚Ì‘©

@@P‚ð’Pˆê‚Ì®”•Ï”x‚̃vƒƒOƒ‰ƒ€‚Æ‚·‚éB

‚±‚Ì‚Æ‚«AŠÂ‹«Env‚Í®”‘S‘ÌZi•Ï”‚Ì’lj‚Å‚ ‚éB‚µ‚½‚ª‚Á‚ÄAƒvƒƒOƒ‰ƒ€P‚Ì‚P‚‚̒ŠÛ‰ðŽß‚Æ‚µ‚Ä

@@@@@@@@I=ƒZ‚̃xƒLW‡,i¾j,iºj, T=Z¾{|‡,+‡},Û=ƒÓ, n-context„

‚ªl‚¦‚ç‚ê‚éB

@‚±‚±‚ÅAƒRƒ“ƒeƒLƒXƒgC‚Í®”‚Ì‚ ‚éW‡‚Å‚ ‚邪A‚±‚ê‚͕‹æŠÔƒ¿(C)=[min(C), max(C)]‚É‚æ‚è’ŠÛ‰»‚³‚ê‚éBC‚ª—LŒÀ‚Å‚È‚¢‚Æ‚«‹«ŠE‚Í|‡‚Ü‚½‚Í+‡‚É‚È‚éB‚Ü‚½A‹t‚̑ΉžƒÁ([a, b])={x| a…x…b}@‚Æ‚·‚éB‚±‚Ì‚Æ‚«A‚æ‚è’ŠÛ“I‚È’ŠÛ‰ðŽßIIiƒTƒtƒBƒbƒNƒX‚ÍInterval‚̈Ӗ¡j

@@@@@@@@II=ƒ‹æŠÔ‚̃xƒLW‡,i¾j,iºj,T=[|‡,+‡],Û=ƒÓ, n-context„

‚ª\¬‚Å‚«Aƒ¿(C)=[min(C), max(C)],ƒÁ([a, b])={x| a…x…b}‚̓KƒƒA‘}“ü‚É‚È‚Á‚Ä‚¢‚éB

i‚±‚ê‚Ìn-context‚ɂ‚¢‚Ä‚ÍŽŸ•Å‚Åà–¾‚·‚éj@‚±‚ê‚ð}Ž¦‚·‚é‚Æ}‚QD‚P‚S‚̂悤‚É‚È‚éB

@@

@@@@@@@@@@@@@@@@@}‚QD‚P‚S@®”‚Æ‹æŠÔ‚̃KƒƒAÚ‘±

@ã‹L‚Å‚ÍA‘Îۂ̃vƒƒOƒ‰ƒ€P‚ðu’Pˆê‚Ì®”•Ï”x‚̃vƒƒOƒ‰ƒ€‚Æ‚·‚éBv‚ƈê”Ê“I‚Éq‚ׂ½‚ªA

‹ï‘Ì“I‚ȉº‹L‚̃vƒƒOƒ‰ƒ€‚ɑ΂µ‚ăRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌŬ•s“®“_‚ð‹‚ß‚éB

@@@@@@@@@@@@@@@@@@@

@@@@@@@@@@@@@@@@@@@}‚QD‚P‚T@‘ÎÛƒvƒƒOƒ‰ƒ€

@}‚QD‚P‚T‚ÌC0, C1,EEE, C5‚̓Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌŠeŒÊ‚ɑ΂·‚鬕ª‚Æ‚·‚éB‚µ‚½‚ª‚Á‚ÄAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv‚ÍACv=(C0, C1, C2, C3, C4, C5)‚Æ•\‚³‚ê‚éBƒvƒƒOƒ‰ƒ€‚Ì•Ï”x‚Í®”Z‚Å‚ ‚éBŒÊr0‚̃Rƒ“ƒeƒLƒXƒgiŒÊr0‚Å‚Ì•Ï”x‚ÌŽæ‚é’l‚ÌW‡j‚Í•s’è‚È‚Ì‚ÅC0=Z¾{|‡, +‡}

n-contextŠÖ”‚ÍCv(r)=n-context(r,Cv)‚È‚Ì‚ÅA

C1=Cv(r1)=n-context(r1,Cv)=C0¿{x=0}@©n-contextŠÖ”‚Ì’è‹`‚©‚çAr1‚ł̃Rƒ“ƒeƒLƒXƒg‚Ír0‚Å‚Ì

@@@@@@@@@@@@@@@@@@@@@@@@@@@ƒRƒ“ƒeƒLƒXƒg‚Ær1‚Ì’¼‘O‚ÌŽ®‚Ì’l‚ÌW‡‚Æ‚ÌÏW‡

@@@@@@@@@@@@@@@@@@@@@@@@@@@ir0‚Ær1‚Í’¼—ñ‚Ì‚½‚ßÏW‡‚Æ‚È‚éj

C2=Cv(r2) =n-context(r2,Cv)=C1¾C4@@©n-contextŠÖ”‚Ì’è‹`‚©‚çAr2‚ł̃Rƒ“ƒeƒLƒXƒg‚Ír1‚Å‚Ì

@@@@@@@@@@@@@@@@@@@@@@@@@@@@ƒRƒ“ƒeƒLƒXƒgC1‚Ær4‚ł̃Rƒ“ƒeƒLƒXƒgC2‚Ƃ̘aW‡B

@@@@@@@@@@@@@@@@@@@@@@@@@@@ir2‚Ír1‚Ær4‚̇—¬‚Ì‚½‚ߘaW‡‚Æ‚È‚éj

“¯—l‚É‚µ‚ÄA

C3= Cv(r3) =n-context(r3,Cv)=C2¿{x…99}

C4= Cv(r4) =n-context(r4,Cv)=C3¿{x=x+1}

C5= Cv(r4) =n-context(r4,Cv)=C2¿{100…x}

‚µ‚½‚ª‚Á‚ÄA}‚QD‚P‚Q‚̃vƒƒOƒ‰ƒ€‚ɑ΂·‚éƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹Cv‚ªŽ®‚ÌW‡‚Æ‚µ‚Ä‹‚Ü‚Á‚½G

Cv=(C0, C1, C2, C3, C4, C5)

@@@C0= Z¾{|‡, +‡}

@@@C1=C0¿{x=0}

@@@C2=C1¾C4

@@@C3=C2¿{x…99}

@@@C4=C3¿{x=x+1}

@@@C5=C2¿{100…x}

‚±‚±‚ÅAƒKƒƒA‘}“ü‚É‚æ‚éƒRƒ“ƒeƒLƒXƒg‚Ì’ŠÛ‰»ƒ¿(C)=[min(C), max(C)],ƒÁ([a, b])={x| a…x…b}‚ðƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚É“K—p‚·‚é‚ÆA’ŠÛƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹A-Cv‚ÍŽŸ‚̂悤‚É‚È‚éG

A-Cv=(A-C0, A-C1, A-C2, A-C3, A-C4, A-C5)

@@@A-C0=[|‡, +‡]

@@@A-C1=(A-C0)¿[0, 0]

@@@A-C2=(A-C1)¾(A-C4)

@@@A-C3=(A-C2)¿[|‡,99]

@@@A-C4=(A-C3)+[1, 1]

@@@A-C5=(A-C2)¿[100,+‡]

ã‹L‚Í‹æŠÔ‚ÉŠÖ‚·‚鉉ŽZ‚ÌŽ®‚Å‚ ‚éB‚±‚±‚ÅA‹æŠÔ‚̉‰ŽZ‚͉º‹L‚É‚æ‚è’è‹`‚³‚ê‚é‚à‚Ì‚Æ‚·‚éG

@@E [a, b]¾[c, d]=[min(a, c), max(b, d)]

@@E [a, b]¿[c, d]=[max(a, c), min(b, d)]

@@E [a, b]+[c, d]=[a+c, b+d]

@ƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹ŠÔ‚̃KƒƒAÚ‘±iƒ¿`,ƒÁ`j‚͉º‹L‚Æ‚È‚éG

@ƒ¿`(Cv)=(ƒ¿(C0),ƒ¿(C1),...,ƒ¿(C5))=([min(C0), max(C0)], [min(C1), max(C1)],...,[min(C5), max(C5)])

@ƒÁ`([a0, b0],[a1, b1],...,[a5, b5])=({x| a0…x…b0 },{x| a1…x…b1",...,{x| a5…x…b5 })

ˆÈã‚Ì‘S‘Ì‘œ‚ð}Ž¦‚·‚é‚ÆA}‚QD‚P‚U‚̂悤‚É‚È‚éB

@@@

@@@@@@@}‚QD‚P‚U@ƒvƒƒOƒ‰ƒ€‚Ì’ŠÛ‰ðŽß‘S‘Ì‘œ‚Ì—á

@}‚QD‚P‚U‚ðŒ©‚é‚ÆAƒvƒƒOƒ‰ƒ€‚Ì‚Q‚‚̒ŠÛ‰ðŽß‚ªs‚í‚ê‚Ä‚¢‚éB‚P‚‚͕ϔ‚ÌW‡‚ð®”‚Ì‘©‚Æ‚µ‚½h‹ï‘Ìh‰ðŽß‚Å‚ ‚èA‚à‚¤ˆê‚‚͕ϔ‚ÌW‡‚ð‹æŠÔ‚Ì‘©‚Æ‚µ‚½h’ŠÛh‰ðŽß‚Å‚ ‚éB‚±‚ê‚̓KƒƒA‘}“ü(ƒ¿AƒÁj‚É‚æ‚è‘Ήž•t‚¯‚ç‚ê‚Ä‚¢‚éB‚Ü‚½A‚±‚ê‚ç‚̃Rƒ“ƒeƒLƒXƒg‚ɑΉž‚µ‚ăRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ªŽ®‚ÌW‡‚Æ‚µ‚ÄŠeX•\Œ»‚³‚ê‚Ä‚¢‚ÄA‚»‚ê‚ç‚ɂ̓KƒƒAÚ‘±iƒ¿`,ƒÁ`j‚ª‘Ήž‚µ‚Ä‚¢‚éB

@ÅI“I‚És‚¢‚½‚¢‚±‚Æ‚ÍAh’ŠÛh‰ðŽß‚Ì¢ŠE‚ŃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌŬ•s“®“_‚ð‹‚߂邱‚ÆA‚·‚È‚í‚¿AƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌŽ®‚̃VƒXƒeƒ€A-Cv=(A-C0, A-C1, A-C2, A-C3, A-C4, A-C5)

@@@@@@A-C0=[|‡, +‡]

@@@@@@A-C1=(A-C0)¿[0, 0]

@@@@@@A-C2=(A-C1)¾(A-C4)

@@@@@@A-C3=(A-C2)¿[|‡,99]

@@@@@@A-C4=(A-C3)+[1, 1]

@@@@@@A-C5=(A-C2)¿{100…x}

‚É‚¨‚¢‚ÄA‚»‚Ì•s“®“_A-Cv=F-Cont(A-Cv)‚ð‹‚߂邱‚Æ‚Å‚ ‚éB

@Ž®‚̃VƒXƒeƒ€‚Ì•s“®“_‚ð‹‚ß‚é•û–@‚É‚ÍAƒNƒŠ[ƒl‚̃V[ƒPƒ“ƒXi’j‚ðŒvŽZ‚·‚éh”½•œhƒAƒ‹ƒSƒŠƒYƒ€‚ª‚ ‚éF‚·‚È‚í‚¿AÛ`‚©‚ço”­‚µ‚ÄAInt``)Int`(Int``))...‚ðŒJ‚è•Ô‚µA‚±‚ê‚ÌŬ•s“®“_¾{Int`n`) | n¸N}‚ðCv‚Æ‚·‚éB

i’jƒNƒŠ[ƒlƒ`ƒFƒCƒ“(Kleene chain)‚Æ‚àŒ¾‚¤BL‚ðŠ®”õ”¼‡˜W‡‚Æ‚µAf:L¨L‚ðScott˜A‘±ŠÖ”‚Æ‚·‚éB‚±‚Ì‚Æ‚«AL‚ÌŬŒ³Û‚©‚çf‚𔽕œ‚·‚邱‚Æ‚É‚æ‚蓾‚ç‚ê‚鉺‹L‚̃`ƒFƒCƒ“‚ð㸃NƒŠ[ƒlƒ`ƒFƒCƒ“(ascending Kleene chain)‚Æ‚¢‚¤F
@@Ûf(Û) f(f(Û))... fn(Û) ...@

@ŽŸ‚Ì‚QD‚QD‚Tß‚Å‚ÍAƒRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ÌŽ®‚̃VƒXƒeƒ€A-Cv=(A-C0, A-C1, A-C2, A-C3, A-C4, A-C5)‚Ì•s“®“_A-Cv=F-Cont(A-Cv)‚𔽕œƒAƒ‹ƒSƒŠƒYƒ€‚ÅŽÀÛ‚É‰ð‚¢‚Ä‚Ý‚éB

[ŋ߂̘_•¶‚©‚ç‚Ì’Žß]

2000”N‚ÌP. Cousot‚̘_•¶u’ŠÛ‰ðŽßF‚»‚Ì’B¬‚Æ“W–]v‚Å‚ÍAƒvƒƒOƒ‰ƒ€‚̧Œä‚̃|ƒCƒ“ƒg‚É•t‚¯‚ç‚ꂽ®”•Ï”‚Ì’l‚Ì‹æŠÔ‚É‚æ‚èAƒgƒŒ[ƒX‚ÌW‡‚ð’ŠÛ‰»‚·‚邱‚Æ‚Í’ŠÛ‚̇¬

@@@@@@@@@@@@@@@ƒ¿(T)=ƒ¿i(ƒ¿r(ƒ¿l(ƒ¿S(T))))

‚É‚æ‚è—^‚¦‚ç‚ê‚éB

‚±‚±‚ÅAƒ¿S‚̓gƒŒ[ƒX‚ɉˆ‚Á‚ÄŒ»‚ê‚éó‘Ô‚ÌW‡‚É‚æ‚éƒgƒŒ[ƒX‚Ì’ŠÛ‚Å‚ ‚éG

@@@@@@@@@@@@@@ƒ¿S(ƒÐ)={ƒÐkF k¸[0, |ƒÐ|]}

ƒ¿l‚Íó‘Ô‚ÌW‡Y‚ɃRƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹‚ð‘Ήž‚³‚¹‚éG

@@@@@@@@@@@@@@ƒ¿l(Y)=ƒ®l¸C{(x1, ... ,xn)F(l, (x1, ... ,xn))¸Y}

ƒ¿r‚̓vƒƒOƒ‰ƒ€•Ï”‚ÌŠÔ‚ÌŠÖŒW‚𖳎‹‚µ‚½•Ï”—̈æ‚̋ߎ—‚Å‚ ‚éF

@@@@@@@@@@ƒ¿r(X)= ƒ®i=1,..,n{xiFÎx1, ... ,xi-1, xi+1, ... ,xnF(x1, .,xi ,.. ,xn)¸X}

‚±‚ê‚ÍŠe•Ï”‚ÌŠÖŒW‚𖳎‹‚µ‚½’¼Ï—̈æ‚ðŽ¦‚µ‚Ä‚¢‚éBCousot‚̉Šú˜_•¶‚̃Tƒ“ƒvƒ‹ƒvƒƒOƒ‰ƒ€‚ÍA

‚PŽŸŒ³‚̃Rƒ“ƒeƒLƒXƒg‚Ì¢ŠE‚Ȃ̂Ń¿r(X)‚ÍP“™ŽÊ‘œ‚Æ‚È‚éB‚Ü‚½ACousot‚̉Šú˜_•¶‚̃Tƒ“ƒvƒ‹ƒvƒƒOƒ‰ƒ€‚Å‚ÍA‚±‚Ì•”•ªiƒ¿i(Z)=[min Z, max Z]j‚ªƒKƒƒAÚ‘±‚Æ‚µ‚Äà–¾‚³‚ê‚Ä‚¢‚½B

‚µ‚½‚ª‚Á‚ÄAƒ¿(T)=ƒ¿i(ƒ¿r(ƒ¿l(ƒ¿S(T))))‚ðCousot‚̉Šú˜_•¶‚̃Tƒ“ƒvƒ‹ƒvƒƒOƒ‰ƒ€‚őΔ䂷‚é‚ÆA

}‚QD‚P‚U‚É‚¨‚¢‚ÄA

@@TÌ ‘Îۂ̃vƒƒOƒ‰ƒ€‚̃gƒŒ[ƒX‚ÌW‡¨‚±‚̃gƒŒ[ƒX‚ɉˆ‚Á‚ÄŒ»‚ê‚éó‘Ô‚ÌW‡ƒÐ‚ðl‚¦‚éB

@ ƒ¿S(T)̃¿S(ƒÐ) = {ƒÐk F k¸[0, |ƒÐ|]}={ƒÐkFk¸[0, 303]}={ƒÐ0,ƒÐ1,ƒÐ2,EEE,ƒÐ302,ƒÐ303 } (=ƒ¿S(X) )=Y

@ƒ¿l(ƒ¿S(T))̃¿l(ƒ¿S(ƒÐ))=ƒ¿l(Y)=ƒ®l¸C{(x1, ... ,xn)F(l, (x1, ... ,xn))¸Y}=ƒ®l¸C{ x¸ZF(l, x)¸Y}

@@@@@@@@@@@@@@@@@=ƒvƒƒOƒ‰ƒ€C‚̃Rƒ“ƒeƒLƒXƒgƒxƒNƒgƒ‹i¨‰º‚Ì}‚ÌCv‚ð\¬‚·‚銂܂Åj

@ƒ¿r(ƒ¿l(ƒ¿S(T))̃¿r(ƒ¿l(ƒ¿S(T))=ƒ¿l(ƒ¿S(ƒÐ))©‚PŽŸŒ³‚Ì¢ŠE‚Ål‚¦‚Ä‚¢‚é‚̂Ń¿r‚ÍP“™ŽÊ‘œB

@@ƒ¿i(ƒ¿r(ƒ¿l(ƒ¿S(T))))̃¿i(Z)=[min Z, max Z]@i}‚QD‚P‚U‚Ì’ŠÛ‰»ŽÊ‘œƒ¿‚ÉŠY“–j

i•â‘«à–¾FƒgƒŒ[ƒXƒZƒ}ƒ“ƒeƒBƒNƒX‚ð‹æŠÔ‚Å’ŠÛ‰»‚·‚邱‚Æ‚ð}Ž¦‚·‚é‚ÆA

@@@@@@@

@@@@@@}‚QD‚P‚V@ƒgƒŒ[ƒXƒZƒ}ƒ“ƒeƒBƒNƒX‚Ì‹æŠÔ‚É‚æ‚é’ŠÛ

¡’ŠÛ‰ðŽß‚̈êŠÑ«‚ÌŽ–—á‚QF•„†‚Ì‹K‘¥@i‚±‚Ì•”•ª‚ÍA•¶Œ£‚Ì‚T‚æ‚èj

@’ŠÛ‰ðŽß‚ÌÅ‚à’¼Š´“I‚È—á‚Í•„†‚Ì‹K‘¥‚Å‚ ‚éB•„†‚Ì‹K‘¥‚Æ‚ÍAX‚ð”‚Æ‚·‚é‚Æ‚«

@@@@@@EX‚ª•‰‚Ì”‚È‚ç‚Î-1

@@@@@@EX‚ª0‚È‚ç‚Î0

@@@@@@EX‚ª³‚È‚ç‚Î+1

‚ð‘Ήž‚³‚¹‚é‹K‘¥‚Å‚ ‚éB

—Ⴆ‚Î-1515*17‚ÍAŽZp‰‰ŽZ‚̈Ӗ¡˜_‚ª•„†‚̃‹[ƒ‹‚Å’è‹`‚³‚ꂽ’ŠÛ¢ŠE{(+), (-), (})}‚Å‚ÌŒvŽZ‚ðŽ¦‚·‚à‚Ì‚Æ‚µ‚Ä—‰ð‚³‚ê‚éB-1515*17‚Ì’ŠÛ¢ŠE‚Å‚ÌŽÀs‚Í-(+)*(+)¨ (-)*(+)¨(-)‚Æ‚È‚èA-1515*17‚Í•‰‚Ì”‚Æ‚È‚éB’ŠÛ‰ðŽß‚Í’Êí‚ÌŒvŽZ¢ŠE‚Ì“Á•Ê‚È\‘¢i‚±‚Ì—á‚Å‚Í•„†j‚ÉŠÖŒW‚·‚éB‚»‚ê‚ÍŽÀÛ‚ÌŽÀs‚Ì‚ ‚鑤–Ê‚Ì—v–ñ‚ð—^‚¦‚Ä‚¢‚éB

@¡AZ‚ð®”‚ÌW‡‚Æ‚µA{-1, 0, 1}‚𕄆‚ÌW‡‚Æ‚·‚éB

Z‚̃xƒLW‡2Z‚Æ{-1, 0, 1}‚̃xƒLW‡2{-1, 0, 1}‚Ƃ̊Ԃ̑Ήž

@@@@ƒ¿F2Z@¨@2{-1, 0, 1}"ƒÁF2{-1, 0, 1}¨@2Z@

‚ðAŽŸ‚̂悤‚É’è‹`‚·‚éG

@@@@ƒ¿({z1,z2,...,zn})={z1‚Ì•„†, z2‚Ì•„†,...,zn‚Ì•„†}

@@@@ƒÁ({-1})=•‰‚Ì®”‘S‘Ì,ƒÁ({0})={0},ƒÁ({-1,0})={0}¾•‰‚Ì®”‘S‘Ì

@@@@ƒÁ({1})=³‚Ì®”‘S‘Ì,ƒÁ({0,1})={0}¾³‚Ì®”‘S‘Ì,ƒÁ({-1,1})=0‚𜂭®”‘S‘Ì,

@@@@ƒÁ({-1,0,1})=Z

@@@@@i—ájƒ¿({-1,-2,-7})={-1},ƒ¿({0,-2,-5})={-1,0},ƒ¿({0,2,4,14,5,10,35})={0,1}

@@œ‚±‚Ì‚Æ‚«iƒ¿AƒÁj‚̓KƒƒA‘}“ü‚Æ‚È‚éB

@@@–¾‚ç‚©‚ɃÁ(ƒ¿({z1,z2,...,zn}))=ƒÁ({z1‚Ì•„†, z2‚Ì•„†,...,zn‚Ì•„†})»{z1,z2,...,zn}

@@@@‚È‚Ì‚ÅAX¸2Z@‚Æ‚·‚é‚Æ‚«AXºƒÁ(ƒ¿(X))‚Æ‚È‚éBEEE‡@

@@@@‚Ü‚½Aƒ¿(ƒÁ({-1}))=ƒ¿(•‰‚Ì®”‘S‘Ì)=-1,ƒ¿(ƒÁ({0}))={0},

@@@@@ƒ¿(ƒÁ({-1,0}))=ƒ¿({0}¾•‰‚Ì®”‘S‘Ì)={-1,0}

@@@@@ƒ¿(ƒÁ({1}))=ƒ¿(³‚Ì®”‘S‘Ì)={1},ƒ¿(ƒÁ({0,1}))=ƒ¿({0}¾³‚Ì®”‘S‘Ì)={0,1},

@@@@@ƒ¿(ƒÁ({-1,1}))=ƒ¿(0‚𜂭®”‘S‘Ì)={-1,1},ƒ¿(ƒÁ({-1,0,1}))=ƒ¿(Z)= {-1,0,1}

@@@@‚È‚Ì‚ÅAY¸2{-1, 0, 1}‚Æ‚·‚é‚Æ‚«AY=ƒ¿(ƒÁ(Y))‚Æ‚È‚éBEEE‡A

@@@@‡@A‡A‚æ‚èiƒ¿AƒÁj‚̓KƒƒA‘}“ü‚Å‚ ‚éB

@@@@•„†‚Ì‹K‘¥‚É‚æ‚é’ŠÛ‰ðŽß‚Ì‘©‚͉º‹L‚̂悤‚É‚È‚éB

@@@@@@@@@@@@@@@@

@@@@@@@@@@@@@@}‚QD‚P‚W@@•„†‚Ì‹K‘¥‚Ì‘©

@@@ŽŸ‚ÉA®”‚ÌW‡ŠÔ‚̘a‚âÏ‚Í’ŠÛ‰»ŽÊ‘œƒ¿‚Å‚Ç‚¤‚È‚é‚©‚ðl‚¦‚Ä‚Ý‚éB

œ—Ⴆ‚ÎA®”‚ÌW‡ŠÔ‚ÌÏ

@@@@@@@@@{-1,-2,-7}*{0,-2,-5}={0,2,4,14,5,10,35}@EEE‡B

‚ðl‚¦‚éB‡B‚̶•Ó‚ÌŠeX‚ðƒ¿‚ÅˆÚ‚·‚ÆAƒ¿({-1,-2,-7})*|ƒ¿({0,-2,-5})={-1}*|{-1,0}={1,0}

ˆê•ûA‡B‚̉E•Ó‚ðƒ¿‚ÅˆÚ‚·‚ÆAƒ¿({0,2,4,14,,5,10,35})={1,0}@]‚Á‚ÄA‰º‹L‚ª¬—§G

@@@@@@@ƒ¿({-1,-2,-7}*{0,-2,-5})=ƒ¿({-1,-2,-7}) *|ƒ¿({0,-2,-5})

‚·‚È‚í‚¿A’ŠÛ¢ŠE‚Å‚Ì•ÏŠ·iÏj‚Í‹ï‘Ì¢ŠE‚Å‚Ì•ÏŠ·iÏj‚ðƒ¿‚ÅˆÚ‚µ‚½‚à‚Ì‚É“™‚µ‚­‚È‚éB

®”‚ÌW‡ŠÔ‚ÌÏ‚Å‚Í‚±‚ꂪ¬—§‚·‚邪A‚±‚ê‚ðA’ŠÛ•ÏŠ·‚ÌŠ®‘S«(completeness)‚Æ‚¢‚¤B

@@@

@@@@@@}‚QD‚P‚X@®”‚ÌW‡ŠÔ‚ÌÏ‚Ì’ŠÛ‰»

œŽŸ‚ɗႦ‚ÎA®”‚ÌW‡ŠÔ‚̘a

@@@@{-3,-4,-7}+{1,2,3}={-2,-3,-6,-1,-2,-5,0,-1,-4}EEE‡C

‚ðl‚¦‚éB‡C‚̶•Ó‚ÌŠeX‚ðƒ¿‚ÅˆÚ‚·‚ÆAƒ¿({-3,-4,-7})+|ƒ¿({1,2,3})={-1}+|{1}={-1,0,1}

ˆê•ûA‡C‚̉E•Ó‚ðƒ¿‚ÅˆÚ‚·‚ÆAƒ¿({-2,-3,-6,-1,-2,-5,0,-1,-4})={-1,0}@]‚Á‚ÄA‰º‹L‚ª¬—§G

@@@@@ƒ¿({-3,-4,-7}+{1,2,3})ºƒ¿({-3,-4,-7}) +|ƒ¿({1,2,3})

‚·‚È‚í‚¿A’ŠÛ¢ŠE‚Å‚Ì•ÏŠ·i˜aj‚Í‹ï‘Ì¢ŠE‚Å‚Ì•ÏŠ·i˜aj‚ðƒ¿‚ÅˆÚ‚µ‚½‚à‚Ì‚ðŠÜ‚ÞB

®”‚ÌW‡ŠÔ‚̘a‚Å‚Í‚±‚ꂪ¬—§‚·‚邪A‚±‚ê‚ðA’ŠÛ•ÏŠ·‚ÌŒ’‘S«(soundness)‚Æ‚¢‚¤B

@@@@

@@@@@@@@@}‚QD‚Q‚O@®”‚ÌW‡ŠÔ‚̘a‚Ì’ŠÛ‰»

@ˆê”Ê‚ÉAP, AFW‡@P=2P,A=2A‚Æ‚µA

@@@@ƒ¿:P¨A‚ð’ŠÛ‰»ŽÊ‘œiã‚Ì—á‚Å‚Í•„†‚Ì‹K‘¥‚ɑΉž‚³‚¹‚郿j

@@@@FFP¨P‚ðPã‚Ì•ÏŠ·‚Æ‚·‚éiã‚Ì—á‚ł͘a(+)‚âÏ(*)j

@@@@F‚ðƒ¿(P)=Aã‚Ì’ŠÛ•ÏŠ·‚Æ‚·‚éBFFA¨Aiã‚Ì—á‚Å‚Í’ŠÛ‰»‚ł̘a(+|)‚âÏ(*|)j

@‚±‚Ì‚Æ‚«A’ŠÛ•ÏŠ·F`‚ªŒ’‘S‚Å‚ ‚é‚Æ‚ÍA”CˆÓ‚Ìp¸P‚ɑ΂µ‚ÄAƒ¿(F(p))ºF`(ƒ¿(p))

@‚Ü‚½A’ŠÛ•ÏŠ·F`‚ªŠ®‘S‚Å‚ ‚é‚Æ‚ÍA”CˆÓ‚Ìp¸P‚ɑ΂µ‚ÄAƒ¿(F(p)) = F`(ƒ¿(p))

@@@@@

@@@@@

@@@@@@@@@@@@}‚QD‚Q‚P@’ŠÛ•ÏŠ·

 

‚QD‚QD‚T@’ŠÛ‰ðŽß‚Å“¾‚ç‚ꂽ“™Ž®ŒQ‚̉ð–@i”½•œƒAƒ‹ƒSƒŠƒYƒ€j

@’ŠÛ‰ðŽß‚Å“¾‚ç‚ꂽ‰º‹L‚Ì“™Ž®ŒQ‚ð‰ð‚­‚±‚Æ‚ðl‚¦‚éBi‚±‚±‚Å‚ÍAƒRƒ“ƒeƒLƒXƒg‚Ì•Ï”–¼‚ð

@A-C0¨X0, A-C1¨X1, A-C2¨X2, A-C3¨X3, A-C4¨X4, A-C5¨X5‚Æ’uŠ·‚¦‚Äl‚¦‚éj

@@@@@@

@‚±‚ê‚ÍX2‚ª‹‚Ü‚ê‚ÎX3ˆÈ~‚Í‚·‚®‚É•ª‚©‚é‚Ì‚ÅAŽŸ‚Ì–â‘è‚Æ‚µ‚ÄÝ’è‚Å‚«‚éG

y–â‘èz‰º‹L‚̃vƒƒOƒ‰ƒ€‚ðŽÀs‚µ‚½‚Æ‚«‚ÌAƒvƒƒOƒ‰ƒ€‚ÌX2‚Å‚Ì•Ï”x‚ÌŽæ‚蓾‚é’l‚͈̔͂ðƒvƒƒOƒ‰ƒ€‰ðÍ‚Å‹‚ß‚æB

@@@@@@

‡@A‡A‚©‚çX2‚Ì’l‚ð•Ï”x‚Å•\‚·‚ÆAiˆÈ~@@‚ð¾A¿‚Å•\‚·j

@X2=X1¾X4=X1¾(X3[x:=x+1])=X1¾((X2¿[-‡, 99])[x:=x+1])=[0, 0]¾((X2¿[-‡, 99])[x:=x+1])

]‚Á‚ÄA@X2=[0, 0]¾((X2¿[-‡, 99])[x:=x+1])

‚±‚ê‚ÍX2‚ÉŠÖ‚·‚éÄ‹AŽ®‚Å‚ ‚éB

œã‚Å‹‚ß‚½‰º‹L‚ÌŽ®‚©‚çX2‚ð‹‚ß‚é‚É‚ÍH

@@@@@@@@X2=[0, 0]¾((X2¿[-‡, 99])[x:=x+1])@ EEE‡D

y]—ˆ‚̃f[ƒ^ƒtƒ[‰ðÍ‚Ì•û–@z

@E‚˜‚Ì’l‚ðŬŒ³‚©‚çŽn‚ß‚ÄAŽ®‡D‚ðiËi+1‚Ì’P’²‘‘å‚·‚é‘Q‰»Ž®‡E‚É‚æ‚èA‚±‚êˆÈãx‚ÌŽæ‚蓾‚é

@ ”͈͂ª‘‚¦‚È‚¢i•s“®“_j‚É’B‚·‚é‚Ü‚ÅŒJ‚è•Ô‚µŒvŽZ‚·‚éG

@@@@X2(i+1)=[0, 0]¾((X2(i)¿[-‡, 99])[x:=x+1])@EEE‡E

@@‚±‚ÌŽ®‚𔼇˜‚ÌŬŒ³Ûi‚±‚±‚Å‚Í‹óW‡ƒÓ‚Æl‚¦‚Ä—Ç‚¢j‚©‚ço”­‚µ‚Ä‹‚ß‚Ä‚¢‚­‚ÆA

@@@@@@@@@@@

@@ã‹L‚ª¬—§‚·‚邱‚Ƃ͇EŽ®‚©‚ç‚·‚®‚É•ª‚©‚éG

@@@X2(1)=[0, 0]¾((X2(0)¿[-‡, 99])[x:=x+1]) = [0, 0]¾(Û¿[-‡, 99])[x:=x+1])

@@@@@=[0, 0]¾(Û)[x:=x+1])=[0, 0]¾(Û)=[0, 0]

@@ X2(2)=[0, 0]¾((X2(1)¿[-‡, 99])[x:=x+1]) = [0, 0]¾([0, 0]¿[-‡, 99])[x:=x+1])

@@@@@@=[0, 0]¾([0, 0])[x:=x+1])=[0, 0]¾([1, 1])=[0, 1]

œ‚±‚ê‚ðŒJ•Ô‚·‚Æi100‰ñˆÊjA

@@@@@@@@@EEEE

@@@X2(99)=[0, 98]

@@@X2(100)=[0, 0]¾((X2(99)¿[-‡, 99])[x:=x+1])=[0, 0]¾(([0, 98]¿[-‡, 99])[x:=x+1])

@@@@@@@@=[0, 0]¾(([0, 98])[x:=x+1])=[0, 0]¾(([1, 99])=[0, 99]

@@@X2(101)=[0, 0]¾((X2(100)¿[-‡, 99])[x:=x+1])=[0, 0]¾(([0, 99]¿[-‡, 99])[x:=x+1])

@@@@@@@@=[0, 0]¾(([0, 99])[x:=x+1])=[0, 0]¾(([1, 100])=[0, 100]

@@@X2(102)=[0, 0]¾((X2(101)¿[-‡, 100])[x:=x+1])=[0,0]¾(([0,100]¿[-‡,99])[x:=x+1])

@@@@@@@@=[0, 0]¾(([0, 99])[x:=x+1])=[0, 0]¾(([1, 100])=[0, 100]

@@‚Æ‚È‚èAn†101‚Å‚ÍX2(n)=[0, 100]‚ÆA•s“®“_‚É’B‚·‚éi‚±‚ꂪ‹‚ß‚é‰ðjB

@ã‹L‚̉ð–@‚ð–{Ž‘—¿‚Ì‘æ‚PÍ‚PD‚Qß‚ÌuÄ‹A‚Æ•s“®“_v‚ÌŽ‹“_‚©‚ç®—‚·‚é‚ÆAŽŸ‚̂悤‚É‚È‚éG

i‚PjƒvƒƒOƒ‰ƒ€‚ÌX2‚ð‹‚ß‚é“™Ž®‚ÍA‰º‹L‚̂悤‚ÉX2‚ÉŠÖ‚·‚éÄ‹AŽ®(zŠÂ’è‹`j‚Æ‚È‚Á‚Ä‚¢‚éB

@@@@X2=[0, 0]¾((X2¿[-‡, 99])[x:=x+1])@EEE‡@

i‚Qj‚±‚ê‚ð‰ð‚­‚½‚ß‚ÉA‰º‹L‚Ì‘Q‰»Ž®‚ðl‚¦‚½G

@@@@@X2(i+1)=[0, 0]¾((X2(i)¿[-‡, 99])[x:=x+1])@EEE‡A

i‚RjX2(0)=ÛiŬŒ³j‚©‚ço”­‚µ‚Äi‚Qj‚Ì‘Q‰»Ž®‚Ì’l‚ð‹‚ß‚é‚ÆA

@@ X2(1)=[0, 0]¾((X2(0)¿[-‡, 99])[x:=x+1])=[0, 0]¾(Û¿[-‡, 99])[x:=x+1])

@@@@@=[0, 0]¾(Û)[x:=x+1])=[0, 0]¾(Û)=[0, 0]

@@@X2(2)=[0, 0]¾((X2(1)¿[-‡, 99])[x:=x+1])=[0, 0]¾([0, 0]¿[-‡, 99])[x:=x+1])

@@@@@@=[0, 0]¾([0, 0])[x:=x+1])=[0, 0]¾([1, 1])=[0, 1]

@@@‚Æ‚È‚èAX2(0)º X2(1)ºX2(2)ºEEEEºX2@@EEE‡B

‚·‚È‚í‚¿A‹‚ß‚½‚¢X2‚ÍA’P’²‘‰Á‚ÌW‡—ñ‚Ìæi‹ÉŒÀj‚É‚ ‚éB

‚±‚±‚ÅAX2(i)‚ðX2(i+1)‚ɑΉž‚³‚¹‚éŠÖ”‚ðF‚Æ‚·‚é‚ÆA

@@@@@X2(i+1) =F(X2(i))@EEE‡C

@@@@@@@@i=[0, 0]¾((X2(i)¿[-‡, 99])[x:=x+1])j

@‚±‚ÌŠÖ”F‚ÍAÄ‹AƒvƒƒOƒ‰ƒ€‚ð•\‚·Ž®X2‚Ì‘Q‰»Ž®ã‚ÌŠÖ”‚Å‚ ‚èAF‚Ì’è‹`‚É‚Í‚à‚Í‚âÄ‹A‚ªŒ»‚ê‚È‚¢‚±‚Æ‚É’ˆÓBF‚Í‚Ü‚½A•Ï”x‚à•\Œ»‚ÉŠÜ‚ß‚é‚ÆA

@@@@@FiX2(i))(x)=[0, 0]¾((X2(i)¿[-‡, 99])[x:=x+1]

@‚Å•\Œ»‚³‚ê‚éB‚±‚ê‚ÍAX2(i) (x)‚ðŠÖ”‚ÆŒ©‚½‚Æ‚«F‚ÍŠÖ”‚ð•Ï”‚Æ‚·‚éŠÖ”iŠÖ”‚ÌŠÖ”j‚Æl‚¦‚ç‚ê‚é‚Ì‚Åi”ÄjŠÖ”‚Æ‚¢‚¤B

‚Ü‚½AX2‚ªX2(i)‚Ì‹ÉŒÀiX2(0)º X2(1)ºX2(2)ºEEEEºX2j‚Æ‚¢‚¤‚±‚Æ‚ÍAX2(i)¨X2A@X2(i+1)¨X2

@@@@‚µ‚½‚ª‚Á‚ÄA‡CŽ®‚©‚牺‹L‚ª¬—§‚·‚éG

@@@@@@@@X2 =F(X2)

@‚±‚ê‚ÍA‘Q‰»Ž®‡C‚̉ðX2‚ªF‚Ì•s“®“_‚Å‚ ‚邱‚Æ‚ðŽ¦‚µ‚Ä‚¢‚éB

ˆÈã‚ÍA’ŠÛ‰ðŽß‚Å“¾‚ç‚ꂽ“™Ž®ŒQ‚̉ð–@i”½•œƒAƒ‹ƒSƒŠƒYƒ€j‚Å‚ ‚邪A‚±‚̉ð–@‚ɂ͉º‹L‚Ì–â‘è“_‚ª‚ ‚éB

y–â‘è“_zX2‚Ì’l‚ð‹‚߂邽‚ß‚É101‰ñ‚ÌŒJ‚è•Ô‚µŒvŽZ‚ª•K—v‚¾‚ªA‚±‚ê‚ðŠÈ’P‚Éo—ˆ‚È‚¢‚©H‚Ü‚½AŒJ‚è•Ô‚µ‰ñ”‚ª—LŒÀ‚Å‚È‚¢‚Æ‚«‚Í‚Ç‚¤‚·‚é‚©H‚±‚ê‚ɑ΂·‚é‰ðŒˆ–@‚ªŽŸ‚Ìß‚Ì’ŠÛ‰ðŽß‚ÌWidening‚Å‚ ‚éB

‚QD‚R@•s“®“_‹ßŽ—–@EEEWidening

@Widening‚Í’ŠÛ‰ðŽß‚É‚¨‚¢‚ÄAƒvƒƒOƒ‰ƒ€‚©‚çì‚ç‚ꂽ“™Ž®ŒQ‚ð‰ð‚­ê‡A•K—v‚ÈŒvŽZƒXƒeƒbƒv‚Ì”‚ð‘å•‚ÉŒ¸‚炵‚ÄŬ•s“®“_‚̋ߎ—‚𓾂邽‚ß‚ÉŽg—p‚·‚éB‚Ü‚½A–³ŒÀ‰ñ‚Ì‘€ì‚ð—LŒÀ‚Å‘Å‚¿Ø‚邱‚Æ‚ª‚Å‚«‚邽‚ßAƒvƒƒOƒ‰ƒ€‰ðÍ‚ÌŠ®—¹‚ð•ÛØ‚·‚éB‚±‚Ìß‚Í•ÊŽ‘—¿i•¶Œ£‚Uj‚ÌWidening‚Ì“à—e‚ð’†S‚Éà–¾‚·‚éiCousot˜_•¶‚Ìu‚Xß@•s“®“_‹ßŽ—–@v‚Ìwidening‚Æ“¯—l‚Ì—á‚È‚Ì‚ÅjB

‚QD‚RD‚P@Widening‰‰ŽZŽq

@(L,ºj‚ðŠ®”õ‘©iŠÖŒWº‚ÉŠÖ‚µãŒÀA‰ºŒÀ‚ª‘¶Ý‚·‚éj‚Æ‚·‚éB

‰º‹L‚ð–ž‚½‚·‚Æ‚«AÞFL~L¨L‚ªwidening‰‰ŽZŽq‚Å‚ ‚é‚Æ‚¢‚¤G

@‡@Þ‚ÍãŠE‰‰ŽZŽq‚Å‚ ‚éB

@@@‚·‚È‚í‚¿A”CˆÓ‚Ìx, y¸L‚ɑ΂µ‚ÄAx¾yºxÞy

@‡A—LŒÀ½(Chain)‚ÌðŒ

@@ L‚Ì’P’²‘‘å‚·‚é½ x0ºx1ºEEEºxnEEE‚ɑ΂µ‚ÄA

@@ Þ‰‰ŽZŽq‚É‚æ‚é½@

@@@@@@y0=x0, y1=y0Þx1, y2=y1Þx2,EEE, yn+1=ynÞxn+1,EEE

@@@‚ÍA—LŒÀ‚ňÀ’è‚·‚éi‘‘傪—LŒÀ‰ñ‚ÅŽ~‚Ü‚éj’P’²‘‘彂ł ‚éB‚·‚È‚í‚¿A

@@@ˆ½‚ém‚ª‘¶Ý‚µ‚ÄA‚™0ºy1ºEEEºym=ym+1=ym+2=EEE

‚·‚È‚í‚¿A–³ŒÀ‚̽(xn)‚ɑ΂µ‚ÄAwidening‰‰ŽZŽqÞ‚É‚æ‚è—LŒÀ‚ňÀ’è‚·‚é½(yn)‚ª’è‹`‚³‚ê‚éB

@@@@

¡windening‰‰ŽZŽq‚Ì—á

@ ‹æŠÔ‚ÌW‡‚ɑ΂µ‚Äwidening‰‰ŽZŽq‚ðˆÈ‰º‚̂悤‚É’è‹`‚·‚é

@@

‚±‚Ì‚Æ‚«AÞ‚Íwidening‰‰ŽZŽq‚ÌðŒ‚ð–ž‚½‚·G

@(xn)FÛº[0, 0]º[0, 1]º[0, 2]ºEEEE

@‚ɑ΂µ‚ÄAy0=Û, y1=y0Þx1=ÛÞ[0, 0]=[0, 0], y2=y1Þx2=[0, 0]Þ[0, 1]=[0,‡],

@@@@@@@@@y3=y2Þx3=[0,‡]Þ[0, 2]=[0,‡]

@‚Æ‚È‚èA(yn)FÛº[0, 0]º[0,‡]=[0,‡]EEE

@‚·‚È‚í‚¿A—LŒÀ‰ñi3‰ñj‚Å[0,‡]‚ÉŽû‘©‚·‚éB

‚QD‚RD‚Q@’ŠÛ‰ðŽß‚Å“¾‚ç‚ꂽ“™Ž®ŒQ‚ÌWidening‚É‚æ‚é‰ð–@iŽ–—á‚Pj

@‘O€‚Å’è‹`‚µ‚½‹æŠÔ‚Ìwidenig‰‰ŽZŽq‚ð‚QD‚QD‚S‚Ì“™Ž®ŒQ‚É“K—p‚·‚é‚ÆA‰º‚̂悤‚É3‰ñ‚ÅŽû‘©‚·‚éB

@@

¡ã‹L‚Ìwidening‚ÌŽ®‚Ìà–¾

@@‡@widening‘O‚Ì’P’²‘‘å‚·‚é½iƒ`ƒFƒCƒ“j‚͉º‹LG

@@

@@‡Aã‹L½‚ɑΉž‚·‚éwidening‚̽‚ð‹‚ß‚éG

@@@@widening‚ÌX2(0)=Œ³‚̽‚ÌX2(0)

@@@@widening‚ÌX2(1)= widening‚ÌX2(0)ÞŒ³‚̽‚ÌX2(1)=ÛÞ([0,0]¾Û)=ÛÞ[0,0]

@@@@widening‚ÌX2(2)= widening‚ÌX2(1)ÞŒ³‚̽‚ÌX2(2)= [0,0]Þ([0,0]¾[1,1]))

@@@@@@@@@@@@@@@@@@= [0,0]Þ[0,1]=[0,‡]

@@@“¯—l‚ÉAwidening‚ÌX2(3)=[0,‡]‚Æ‚È‚èAŽû‘©‚·‚éB

@@@]‚Á‚ÄAwidening‚ÌX2(i)‚ðX2(i)‚Æ‚·‚é‚Ɖº‚ÌŒ‹‰Ê‚ª‹‚Ü‚éB

@@@

@@‡Bwidening‚É‚æ‚èX2(2)=[0,‡]‚ÉŽû‘©‚µ‚½B

@@@@‚±‚Ì’l‚ðŽ®@X2(i+1) = [0, 0]¾((X2(i)¿[-‡, 99])[x:=x+1])

@@@@‚É‘ã“ü‚·‚邱‚Æ‚É‚æ‚èA—LŒÀ‚Ì•s“®“_‚É“ž’B‚·‚éB‚±‚̃vƒƒZƒX‚ðDescending sequence‚Æ‚¢‚¤B

@@@

@‚±‚ê‚Í]—ˆ‚ÌŽè–@‚Ì101‰ñ‚ÌŒJ‚è•Ô‚µŒvŽZ‚Æ“¯‚¶Œ‹‰Ê‚Æ‚È‚Á‚Ä‚¢‚éB


‚QD‚RD‚R@Widening‚É‚æ‚é‰ð–@iŽ–—á‚Pj‚Ì‚Ü‚Æ‚ß

@@widening‰‰ŽZŽq‚Ædescending sequence‚É‚æ‚èAu]—ˆ‚̉ðÍŽè–@‚Å‚Í101‰ñ—v‚µ‚Ä‚¢‚½ŒvŽZ‚ª

@‚킸‚©4‰ñ‚Å‹‚߂邱‚Æ‚ª‚Å‚«‚½i’jBv@‚±‚ê‚ÍWidening‚̈ЗÍi–w‚ÇŒvŽZ‚¹‚¸‚ÉŒ‹‰Ê‚ðŽ¦‚·jB

@i’j‚±‚ÌŽ–—á‚Í’Pƒ‚È‚Ì‚Å“¯‚¶‰ð[0, 100]‚ª“¾‚ç‚ꂽ‚ªˆê”ʂɂͳŠm‚ȉð‚æ‚è‚ÍL‚¢‹ßŽ—‰ð‚Æ‚È‚éB

@@@

@@@@@@@@@@@}‚QD‚Q‚Q@Widening‰‰ŽZ‚Ìà–¾

@@‚Ü‚½AWidening‚É‚æ‚éŽû‘©ŒvŽZ‚̃Oƒ‰ƒt•\Œ»‚Ædescending‚̈Ӗ¡‚ɂ‚¢‚Äl‚¦‚Ä‚Ý‚éB

@@@@@@@@@@X2(i+1)=F(X2(i))=[0, 0]¾((X2(i)¿[-‡, 99])[x:=x+1])

@‚Æ‚·‚é‚Æ‚«A‚±‚ê‚ÌWidening‚É‚æ‚éŽû‘©ŒvŽZ‚Í}‚QD‚P‚U‚̂悤‚É•\Œ»‚³‚ê‚éiŽQlŽ‘—¿‚T‚̃Xƒ‰ƒCƒh‚ðŒ³‚Éì¬jG

@@@

@@@@@@@@@}‚QD‚Q‚R@Widening‚É‚æ‚éŽû‘©ŒvŽZ‚̃Oƒ‰ƒt•\Œ»

‚QD‚RD‚S@’ŠÛ‰ðŽß‚Å“¾‚ç‚ꂽ“™Ž®ŒQ‚ÌWidening‚É‚æ‚é‰ð–@iŽ–—á‚QFZero divide‚̉”\«‚Ì—áj

@‰º‹L‚̂悤‚È’Pƒ‚ȃvƒƒOƒ‰ƒ€‚ð—á‚É‚µ‚Ĉȉº‚Ì–â‘è‚ðݒ肵A‰ðÍ‚ðs‚È‚¤BËPolyspace Technologies‚̃Xƒ‰ƒCƒh‚ÅЉ‚ꂽ—áB

y–â‘èz‰º‹L‚̃vƒƒOƒ‰ƒ€‚ÅZero divide‚ª”­¶‚·‚é‚©H

@@@

@‚±‚ê‚ð’Êí‚̃fƒoƒbƒO‚ÅŠm”F‚·‚é‚ÆAK‚ÌŽæ‚蓾‚é’l‚ªL‚¢‚Ì‚Å‚©‚È‚èŽèŠÔ‚ª‚©‚©‚éB

@@PolySpace‚ÌŽ‘—¿‚Å‚ÍAŽ®‚ÆŬ•s“®“_‚É‚æ‚é‰ð‚ª‚ ‚éB˂ǂ̂悤‚É‚µ‚Ä“±‚©‚ê‚é‚©‚Æ‚¢‚¤ŒvŽZ‰ß’ö‚Í‘‚©‚ê‚Ä‚È‚¢B

@@

@ˆÈ~A‚±‚ÌŽ®‚Ì“±o‰ß’ö‚ðà–¾‚·‚éB

•Ï”i,j,k‚ÌŽæ‚蓾‚é”͈͂ɒ…–Ú‚·‚é‚ÆAƒvƒƒOƒ‰ƒ€‚ÌŠeƒXƒeƒbƒv‚̈Ӗ¡‚͉º‹L‚̂悤‚É‚È‚éB

@@

‚·‚È‚í‚¿AƒvƒƒOƒ‰ƒ€‚Ì“™Ž®•\Œ»‚͉º‹L‚̉E‚̂悤‚É‚È‚éB

@@

@ŽŸ‚É‚±‚ê‚ðuƒJƒIƒX“IŒJ‚è•Ô‚µ–@v‚Æuwidening‰‰ŽZ–@v‚Ì‚Q‚Â‚Å‰ð‚¢‚Ä‚Ý‚éB

i‚PjƒJƒIƒX“IŒJ‚è•Ô‚µ–@‚É‚æ‚é‰ð–@

@@ã‚Å‹‚ß‚½“™Ž®‚ðX1‚©‚燂ɑã“ü‚µ‚ÄÅŒã‚ÌX8‚ð‹‚ß‚éG

@‡@ X0={ (0, 0, k) | k¸[-231, 231-1] }‚ðX1‚É‘ã“ü‚·‚é‚ÆA

@@@X1={ (2, j, k) | (i, j, k)¸X0 }={ (2, 0, k) | k¸[-231, 231-1] }

@‡A ã‚Å‹‚ß‚½X1={ (2, 0, k) | k¸[-231, 231-1] }‚ðX2‚É‘ã“ü‚·‚é‚ÆA

@@ @@X2={ (2, k+5, k) | k¸[-231, 231-1] }

@ã‹L‚Ì‚Q‚‚͊ȒP‚É‹‚ß‚ç‚ꂽ‚ªAŽŸ‚ÌX3‚ÍŽû‘©ŒvŽZ‚ª•K—v‚Æ‚È‚éG

@‡B ã‚Å‹‚ß‚½X2={ (2, k+5, k) | k¸[-231, 231-1] }‚ðX3‚É‘ã“ü‚·‚é‚ÆA

@@@X3=X2¾X6={ (2, k+5, k) | k¸[-231, 231-1] }¾{ (i, j+3, k) | (i, j, k)¸X4 }

@@@@@@@= {(2, k+5, k) | k¸[-231, 231-1] }¾{ (i, j+3, k) | (i-1, j, k)¸X3 , iƒ10 }

@@‚·‚È‚í‚¿AX3‚Ì‚Ý‚ð•Ï”‚Æ‚·‚éÄ‹AŽ®‚ª‹‚ß‚ç‚ꂽG

@@ X3= {(2, k+5, k) | k¸[-231, 231-1] }¾{ (i, j+3, k) | (i-1, j, k)¸X3 , iƒ10 }

@ ‚±‚ê‚ðX3‚ÌŬŒ³‚©‚çŽn‚ß‚Ä’P’²‘‘å‚·‚鉺‹L‚Ì‘Q‰»Ž®‚É‚æ‚èAX3‚Ì’l‚͈̔͂ª‘‚¦‚È‚­‚È‚é‚Ü‚Å

@@ŒJ‚è•Ô‚µŒvŽZ‚·‚é(Ŭ•s“®“_ŒvŽZjG

@@@X3(n+1)= {(2, k+5, k) | k¸[-231, 231-1] }¾{ (i, j+3, k) | (i-1, j, k)¸X3(n) , iƒ10}

@@‚±‚Ì‘Q‰»Ž®‚É‚æ‚éŬ•s“®“_ŒvŽZ‚ð‰º‹L‚ÉŽ¦‚·B

@@@X3(n+1)= {(2, k+5, k) | k¸[-231, 231-1] }¾{ (i, j+3, k) | (i-1, j, k)¸X3(n) , iƒ10}@EEE(1)

@@‚±‚Ì(1)Ž®‚ðn‚ɂ‚¢‚Ä‚Ì‘Q‰»Ž®‚ðŬŒ³i‹óW‡j‚©‚ço”­‚µ‚Ä‰ð‚¢‚Ä‚¢‚­G

@@n=0‚Ì‚Æ‚«AX3(0)=ƒÓi‹óW‡j

@@‚±‚ê‚ð(1)Ž®‚É‘ã“ü‚·‚é‚ÆA

@@X3(1)={(2, k+5, k) | k¸[-231, 231-1] }¾ƒÓ={(2, k+5, k) | k¸[-231, 231-1] }

@@‚±‚ê‚ðÄ‚Ñ(1)Ž®‚É‘ã“ü‚·‚é‚ÆA

@@X3(2)={(2, k+5, k) | k¸[-231, 231-1] }¾{(i, j+3, k) | (i-1, j, k)¸X3(1) , iƒ10}

@@@@@={(2, k+5, k) | k¸[-231, 231-1] }¾{(3, k+5+3, k) | k¸[-231, 231-1] , iƒ10}

@@@@@={(i, j, k) | k¸[-231, 231-1], i¸[2, 3],@j=k+5–”‚Íj=k+5+3}EEE(2)

@@‚±‚±‚ÅAj=k+5–”‚Íj=k+5+3‚ÍŽŸ‚̂悤‚Él‚¦‚éG

@@j=k+5=k+3*2-1, j=k+5+3=k+3*3-1‚·‚È‚í‚¿Ai=2, 3‚Ì‚Æ‚«Aj=k+3*i-1‚Æ“Z‚ß‚ç‚ê‚éB

@@‚µ‚½‚ª‚Á‚ÄA(2)‚ÍŽŸ‚̂悤‚É‚È‚éG

@@X3(2)={(i, j, k) | k¸[-231, 231-1], i¸[2, 3],@j=k+3*i-1}

@@ˆÈ‰ºA“¯—l‚ÉŒJ‚è•Ô‚µŒvŽZ‚µ‚Ä‚¢‚­‚ÆA

@X3(9)={(i, j, k) | k¸[-231, 231-1], i¸[2, 3, 4,EEE, 10],@j=k+3*i-1}@EEE(3)

@X3(10)=X3(9)‚Æ‚È‚èA(3)‚ªX3‚ÌŬ•s“®“_‚Å‚ ‚邱‚Æ‚ª•ª‚©‚éB

@@‚·‚È‚í‚¿A

@@X3={(i, j, k) | k¸[-231, 231-1], i¸[2, 3, 4,EEE, 10],@j=k+3*i-1}

@@ @={(i, j, k) | k¸[-231, 231-1], i¸[2, 10], j=k+3*i-1}@@@i[2, 10]‚Í‹æŠÔ‚ðŽ¦‚·j

@‡CŽŸ‚ÉX3={(i, j, k) | k¸[-231, 231-1], i¸[2, 10], j=k+3*i-1}‚ðX4‚̉E•Ó‚É‘ã“ü‚·‚邱‚Æ‚ÅX4‚Ì’l‚ð

@@‹‚ß‚éG@X4={ (i+1, j, k) | (i, j, k)¸X3 ,iƒ10}@EEE(4)

@@‚±‚±‚ÅAX3‚Ìi‚ÍX4‚Å‚Íi+1‚É’u‚«Š·‚¦‚ç‚ê‚Ä‚¢‚é‚Ì‚ÅAX4‚Ìi+1‚ði‚Å•\Œ»‚·‚é‚ÆA

@@X3‚Ìi‚Íi-1‚Æ‚È‚éG i-1¸[2, 10]¨i¸[2+1, 10],@j=k+3*(i-1)-1

@@‚µ‚½‚ª‚Á‚ÄA(4)‚ÍŽŸ‚̂悤‚É‚È‚éG

@@X4={(i, j, k) |@k¸[-231, 231-1], i¸[2+1, 10],@j=k+3*(i-1)-1}

@@@@={(i, j, k) |@k¸[-231, 231-1], i¸[3, 10],@j=k+3*i-4}

@‡D“¯—l‚ÉAX4 ={(i, j, k) |@k¸[-231, 231-1], i¸[3, 10],@j=k+3*i-4}‚ðX5‚̉E•Ó‚É

@ @‘ã“ü‚·‚邱‚Æ‚ÅX5‚Ì’l‚ð‹‚ß‚éG

@@@@X5={ (i, j+3, k) | (i, j, k)¸X4}@EEE(5)

@@‚±‚±‚ÅAX4‚Ìj‚ÍX5‚Å‚Íj+3‚É’u‚«Š·‚¦‚ç‚ê‚Ä‚¢‚é‚Ì‚ÅAX5‚Ìj+3‚ðj‚Å•\Œ»‚·‚é‚ÆA

@@X4‚Ìj‚Íj-3‚Æ‚È‚éG@j-3=k+3*i-4¨j=k+3*i-1

@@‚µ‚½‚ª‚Á‚ÄA(5)‚ÍŽŸ‚̂悤‚É‚È‚éG

@@X5 ={(i, j, k) |@k¸[-231, 231-1], i¸[3, 10],@j=k+3*i-1}

@‡EX6=X5

@‡F“¯—l‚ÉA X3 ={(i, j, k) | k¸[-231, 231-1], i¸[2, 10],@j=k+3*i-1}‚ðX7‚̉E•Ó‚É‘ã“ü‚·‚邱‚Æ‚Å

@@X7‚Ì’l‚ð‹‚ß‚éBi=10‚È‚Ì‚Å‚±‚ê‚ð‘ã“ü‚·‚é‚ÆA

@@X7={ (i, j, k) | (i, j, k)¸X3,i†10 }

@@@@={(10, j, k) |@k¸[-231, 231-1], j=k+3*10-1=k+29}

@‡G“¯—l‚ÉA X7 ={(10, j, k) |@k¸[-231, 231-1], j=k+29}‚ðX8‚̉E•Ó‚É‘ã“ü‚·‚邱‚Æ‚ÅX8‚Ì’l‚ð

@@‹‚ß‚éBX8‚É’B‚·‚邽‚ß‚É‚Íi‚j‚È‚Ì‚ÅA

@@X8={ (i, j, k) | (i, j, k)¸X7 ,i‚j }

@@@@={(10, j, k) |@k¸[-231, 231-1], j=k+29, i‚j }@EEE(6)

@ˆÈã‚É‚æ‚èAPolySpace‚ÌŽ‘—¿‚ÌŬ•s“®“_‚É‚æ‚é‰ð‚ª‹‚ß‚ç‚ꂽB

ŽŸ‚ÉAÅŒã‚ÌŽ®(6)‚̈Ӗ¡‚ðl‚¦‚éG

@@@X8={(10, j, k) |@k¸[-231, 231-1], j=k+29, i‚j }@

‚±‚ÌŽ®‚©‚çAj=10‚Ì‚Æ‚«i=j=10‚Æ‚È‚èAƒvƒƒOƒ‰ƒ€‚̓‰ƒxƒ‹‚V‚É‚¨‚¢‚ÄZero divide

‚ª”­¶‚·‚邱‚Æ‚ª•ª‚©‚éB‚Ü‚½A‚±‚Ì‚Æ‚«‚Ìk=-19‚Å‚ ‚éB

i‚QjWidening‚É‚æ‚é‰ð–@

¡‰º‹L‚Ì(1)Ž®‚ðwidening‚ʼnð‚­B

@X3(n+1)= {(2, k+5, k) | k¸[-231, 231-1] }¾{ (i, j+3, k) | (i-1, j, k)¸X3(n) , iƒ10}@EEE(1)

ã‹L(1)Ž®‚Í(i, j, k)‚Æ‚¢‚¤‚R•Ï”‚ÌŽ®‚¾‚ªAk¸[-231, 231-1]‚Í‚±‚êˆÈã‚»‚Ì’l‚͈̔͂ªŠg‘傹‚¸A j=k+3*i-1‚©‚çj‚Íi, k‚É‚æ‚èˆêˆÓ“I‚ÉŒˆ‚Ü‚é‚Ì‚ÅAwidening‚Æ‚µ‚ÄŠg‘å‚·‚齂Íi‚ɂ‚¢‚Ä‚Ì‚Ýl‚¦‚éB‚·‚È‚í‚¿A‚P•Ï”‹æŠÔ‚É‚æ‚éwidening‚őΉž‚Å‚«‚éi’jB

@@@@@@@@@@@@@@@@@

ˆÈ‰ºA‚»‚ÌŽè‡‚ðŽ¦‚·G

‡@widening‘O‚Ì’P’²‘‘å‚·‚齂Ìʼn‚Ì”€‚ðl‚¦‚éi‚±‚ê‚ÍA4.2(4)‚ÅŒvŽZÏj

@@@X3(0)=ƒÓi‹óW‡j

@@@X3(1)={(2, k+5, k) | k¸[-231, 231-1] }

@@@X3(2)={(i, j, k) | k¸[-231, 231-1], i¸[2, 3],@j=k+3*i-1}

@‚±‚±‚ÅAi‚݂̂ɂ‚¢‚Ă̽‚ðl‚¦‚éBi‚ɂ‚¢‚Ă̽‚Í

@@@[X3(0)]i =ƒÓA[X3(1)]i =[2, 2]A[X3(2)]i =[2, 3]@@

‡Aã‹L‚Ìi‚ɂ‚¢‚Ă̽‚ɑΉž‚µ‚Äwidening‚̽‚ð‹‚ß‚éG

@@@widening‚̽‚Ì[X3(0)]i =Œ³‚̽‚Ì[X3(0)]i =ƒÓA

@@@widening‚̽‚Ì[X3(1)]i =(widening‚̽‚Ì[X3(0)]i)Þ(Œ³‚̽‚Ì[X3(1)]i) =ƒÓÞ [2, 2]=[2, 2]

@@@widening‚̽‚Ì[X3(2)]i =(widening‚̽‚Ì[X3(1)]i)Þ(Œ³‚̽‚Ì[X3(2)]i) =[2, 2]Þ[2, 3]=[2,‡]

@@@@@EEE‚±‚êˆÈãi‚ÍŠg‘債‚È‚¢‚Ì‚Åwidening‚ÍŽû‘©I

‚µ‚½‚ª‚Á‚ÄAwidening‚Å‹‚ß‚½X3(n)‚ÌŽû‘©’l‚Í

@@X3(2)={(i, j, k) | i¸[2, +‡], k¸[-231,231-1], j=k+3*i-1}EEE(2)

‚Æ‚È‚èA‚±‚ê‚ð(1)Ž®‚É‘ã“ü‚·‚é‚ÆA

X3(3)= {(2, k+5, k) | k¸[-231, 231-1]@}¾{(i, j+3, k) | (i-1, j, k)¸X3(2) , iƒ10}EEE(3)

‚±‚±‚ÅA (3)Ž®‚Ì{(i, j+3, k) | (i-1, j, k)¸X3(2) , iƒ10}‚Ì

•Ï”i‚ªŽæ‚蓾‚é’l‚ÍA(2)Ž®‚æ‚èi-1¸[2, +‡] & (iƒ10)‚æ‚èAi-1=2, 3, 4, 5, 6, 7, 8, 9

@@@Ëi=3, 4, 5, 6, 7, 8, 9, 10@‚·‚È‚í‚¿Ai¸[3, 10]

•Ï”j‚Ì’l‚ÍA (i-1, j, k)¸X3(2)‚æ‚èAj=k+3*(i-1)-1@Ëj+3=k+3*(i-1)-1+3=k+3i-1

‚±‚ê‚É‚æ‚èA{(i, j+3, k) | (i-1, j, k)¸X3(2) , iƒ10}

@@={(i, J, k) | k¸[-231,231-1], i¸[3, 10], J=k+3*i-1}

‚µ‚½‚ª‚Á‚ÄA(3)Ž®‚ÍA

X3(3)= {(2, k+5, k) | k¸[-231, 231-1] }¾{(i, J, k) | k¸[-231,231-1], i¸[3, 10],@

@@@@@@@J=k+3*i-1} ={(i, J, k) | k¸[-231, 231-1], i¸[2, 10],@J=k+3*i-1}

‚Æ‚È‚èA‚QD‚RD‚Si‚Pj‚ÌŒJ‚è•Ô‚µŒvŽZ‚Æ“¯‚¶Œ‹‰Ê‚ª“¾‚ç‚ꂽBi’Êí‚̃vƒƒOƒ‰ƒ€‰ðÍ‚Å‚Í10‰ñ‚ÌŒJ‚è•Ô‚µ

ˆ—‚ª•K—v‚¾‚ªAwidening‚Å‚Í2‰ñ‚ÅŽû‘©Ij

ËWidening‚̓vƒƒOƒ‰ƒ€‚̃‹[ƒvˆ—‚ðˆê‹C‚É‰ðŒˆ‚·‚éŽè–@B

@@@@@@@@@@@@@@


‚QD‚RD‚T@Widening‚Ì‚Ü‚Æ‚ß

i‚PjŽOŽÒ”äŠr

@@@@@@

i‚QjWidening‰‰ŽZŽq‚̃Rƒ“ƒZƒvƒgG

@E‚±‚̉‰ŽZŽq‚̓‹[ƒv/ƒTƒCƒNƒ‹‚Ì‚P‚‚̃CƒeƒŒ[ƒVƒ‡ƒ“Œã‚Ìó‘Ԃ̕ω»‚𒲂×A“¯‚¶•ÏŠ·‚ª–³ŒÀ‰ñ

@ ‹N‚«‚é‚©‚à‚µ‚ê‚È‚¢‚Ɖ¼’肵‚ÄA‚±‚Ìî•ñ‚©‚烋[ƒv‚ÌU•‘‚¢‚ðŠO‘}‚µ‚悤‚Æ‚·‚éB

@E‚±‚̉‰ŽZŽq‚̓‹[ƒv‚ÌŒJ‚è•Ô‚µ‚ªi‚Ì’l‚ð‘‘傳‚¹‚Ä‚¢‚邱‚Æ‚ðŒŸ’m‚µA‚»‚ꂪ–³ŒÀ‰ñ‹N‚«‚邱‚Æ‚ð

@ŠO‘}‚·‚éB‚±‚ÌŠO‘}‚ÍT‚¦–ډ߂¬‚é‚©‚à‚µ‚ê‚È‚¢‚ª•ªÍ‚ÌŠ®—¹‚ð•ÛØ‚·‚éB

@@@@@@@@@@@

@