Mercurial > hg > Papers > 2015 > atton-sigse
view mindmap.mm @ 25:5c27de156e78
Update mind map
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 10 Dec 2014 16:57:49 +0900 |
parents | c86aa006497b |
children | fa9bde939db6 |
line wrap: on
line source
<map version="1.0.1"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> <node CREATED="1418180915266" ID="ID_91344823" MODIFIED="1418180918413" TEXT="形式手法 -産学連携で普及拡大を目指す-"> <node CREATED="1418180919812" ID="ID_1639973897" MODIFIED="1418180981990" POSITION="right" TEXT="証明するアプローチ"> <node CREATED="1418180981992" ID="ID_1157185658" MODIFIED="1418180994566" TEXT="割と1データ型に対してコストが高い"> <node CREATED="1418180994567" ID="ID_905788309" MODIFIED="1418180997440" TEXT="証明を書くのに"> <node CREATED="1418181345166" ID="ID_907688181" MODIFIED="1418181354566" TEXT="Delta は一回あたり1ヶ月ほど"> <node CREATED="1418181354567" ID="ID_1771472289" MODIFIED="1418181363138" TEXT="定義を変えたら1ヶ月越えた気もする"/> </node> <node CREATED="1418181366653" ID="ID_1913589464" MODIFIED="1418181381121" TEXT="たぶん データ型1つと付随する関数5つくらい"> <node CREATED="1418181383134" ID="ID_1911930342" MODIFIED="1418181392209" TEXT="そんなんで実用に耐えうるのかなのか"/> </node> </node> <node CREATED="1418180997668" ID="ID_900558037" MODIFIED="1418181006647" TEXT="自動は無理っぽい"> <node CREATED="1418181007460" ID="ID_1468593122" MODIFIED="1418181019991" TEXT="coq とかならともかく"/> <node CREATED="1418181020204" ID="ID_31071323" MODIFIED="1418181028070" TEXT="Agda は手で書かないといけない"/> </node> <node CREATED="1418181031243" ID="ID_1908587433" MODIFIED="1418181045908" TEXT="証明済み基礎データ型みたいなのの組合せで書く"> <node CREATED="1418181045909" ID="ID_828327547" MODIFIED="1418181053690" TEXT="そうするとある程度保証される"> <node CREATED="1418181053692" ID="ID_411317141" MODIFIED="1418181064222" TEXT="証明された規則での変形"/> <node CREATED="1418181064498" ID="ID_1194413342" MODIFIED="1418181082811" TEXT="データ型そのものが持つ性質"/> <node CREATED="1418181077635" ID="ID_496017643" MODIFIED="1418181077635" TEXT=""/> </node> <node CREATED="1418181089970" ID="ID_1111677954" MODIFIED="1418181093940" TEXT="それで書けないのをどうするか"> <node CREATED="1418181110672" ID="ID_1555848580" MODIFIED="1418181126403" TEXT="だが許すと証明された規則が消えてしまう"/> <node CREATED="1418181126648" ID="ID_266121578" MODIFIED="1418181130602" TEXT="なので強制することになるはず"/> </node> <node CREATED="1418181094202" ID="ID_159439470" MODIFIED="1418181100076" TEXT="それで全て表現可能なのか"> <node CREATED="1418181102609" ID="ID_501203024" MODIFIED="1418181110307" TEXT="追加や拡張はコストが高い"/> <node CREATED="1418181136367" ID="ID_1164500334" MODIFIED="1418181186529" TEXT="System F でコードが書けるのか、という話に似ているはず"> <node CREATED="1418181158535" ID="ID_1260862407" MODIFIED="1418181161897" TEXT="書けはするけれど"/> <node CREATED="1418181162111" ID="ID_212009215" MODIFIED="1418181167129" TEXT="おそらく実用的な範囲外"/> </node> </node> <node CREATED="1418181100665" ID="ID_1611809731" MODIFIED="1418181222151" TEXT="Agda Standard Library みたいなもんかな"/> </node> <node CREATED="1418181225109" ID="ID_1053237860" MODIFIED="1418181229327" TEXT="じゃあいれない"> <node CREATED="1418181229914" ID="ID_1803168817" MODIFIED="1418181234579" TEXT="どうやって保証するか"> <node CREATED="1418181234580" ID="ID_1636639123" MODIFIED="1418181239892" TEXT="model checking"> <node CREATED="1418181239893" ID="ID_735643632" MODIFIED="1418181244631" TEXT="そんなに万能なのか"/> <node CREATED="1418181394509" ID="ID_1300439708" MODIFIED="1418181407159" TEXT="そのあたりは自分の知識的に用検証"/> </node> </node> <node CREATED="1418181245658" ID="ID_1970618421" MODIFIED="1418181258931" TEXT="自動で型にあてはめる、くらいで良いのかな"> <node CREATED="1418181258932" ID="ID_414181546" MODIFIED="1418181261629" TEXT="ATS みたいな"> <node CREATED="1418181262130" ID="ID_801641798" MODIFIED="1418181277612" TEXT="高い信頼性を持つ型付き部分"/> <node CREATED="1418181278809" ID="ID_1479777082" MODIFIED="1418181285618" TEXT="とりあえず動くベタコード部分"/> </node> <node CREATED="1418181290050" ID="ID_324009537" MODIFIED="1418181294265" TEXT="そこは自動でいけるのか"> <node CREATED="1418181294266" ID="ID_587580129" MODIFIED="1418181298347" TEXT="推論だけでいけるのか"/> <node CREATED="1418181298802" ID="ID_1558354110" MODIFIED="1418181309356" TEXT="ほんとに自動で対応しているのがきちんと対応しているのか"/> <node CREATED="1418181309576" ID="ID_1115441920" MODIFIED="1418181315652" TEXT="明示的に書く?"/> </node> </node> </node> <node CREATED="1418181321680" ID="ID_1702292110" MODIFIED="1418181328111" TEXT="書いてしまえばご自由にどうぞ"> <node CREATED="1418181328112" ID="ID_1459622184" MODIFIED="1418181332895" TEXT="その範囲であれば問題無し"/> <node CREATED="1418182219889" ID="ID_201679429" MODIFIED="1418182233822" TEXT="ただしそこをプログラマが正しくマッピングできるかどうかという問題が"/> </node> </node> <node CREATED="1418182698609" ID="ID_735630562" MODIFIED="1418182709372" TEXT="きちんと対応が取れるか問題"/> <node CREATED="1418182709624" ID="ID_252376527" MODIFIED="1418182714787" TEXT="over verification"/> </node> <node CREATED="1418181411845" ID="ID_269659410" MODIFIED="1418181423087" POSITION="left" TEXT="Category"> <node CREATED="1418181423515" ID="ID_97428056" MODIFIED="1418181429614" TEXT="なぜ Formalization にいったか"> <node CREATED="1418181429915" ID="ID_150938332" MODIFIED="1418181438934" TEXT="Parallel debugger はどうしてそのまま書かなったか"> <node CREATED="1418181440027" ID="ID_1895994685" MODIFIED="1418181456558" TEXT="割と mercurial repository checkout でいける"/> <node CREATED="1418181456779" ID="ID_1429431108" MODIFIED="1418181473453" TEXT="副作用的なものを含めているのをどうするのか非自明"> <node CREATED="1418181474994" ID="ID_1072354018" MODIFIED="1418181480349" TEXT="haskell ならどうにか?"/> <node CREATED="1418181480611" ID="ID_1482677118" MODIFIED="1418181512835" TEXT="副作用を含む場合の prallel debbugging がきちんと対応するのかまず考えたかった"> <node CREATED="1418181516936" ID="ID_1426285126" MODIFIED="1418181523331" TEXT="書いてから悩めよ節もあるけれど"/> <node CREATED="1418181523593" ID="ID_1361560439" MODIFIED="1418181538651" TEXT="個人的には凶悪な外部IFとか書かないと無理なのではと思ってた"/> </node> </node> </node> </node> <node CREATED="1418181545918" ID="ID_1417713796" MODIFIED="1418181557255" TEXT="Category は役に立つのか"> <node CREATED="1418181557256" ID="ID_940725954" MODIFIED="1418181570538" TEXT="形式化手法としてはどうなんだろう"/> <node CREATED="1418181571383" ID="ID_53776958" MODIFIED="1418181591038" TEXT="Categorical Formalized なスコープに落とすと良いよね、みたいな使い方なイメージ"> <node CREATED="1418181591039" ID="ID_716874884" MODIFIED="1418181595489" TEXT="Free Monoid とか"/> <node CREATED="1418181596094" ID="ID_100297480" MODIFIED="1418181604248" TEXT="そのスコープ内でしかできないといえばできない"/> <node CREATED="1418181616509" ID="ID_1023470454" MODIFIED="1418181626871" TEXT="対応関係はプログラマが考える"/> </node> <node CREATED="1418181630691" ID="ID_387443474" MODIFIED="1418181636579" TEXT="実際の表現能力"> <node CREATED="1418181636580" ID="ID_1548187078" MODIFIED="1418181645287" TEXT="正直パッとは書けない"> <node CREATED="1418181645619" ID="ID_327454102" MODIFIED="1418181651790" TEXT="必須知識が多すぎる"/> </node> <node CREATED="1418181655339" ID="ID_1909823549" MODIFIED="1418181664570" TEXT="こわい Haskeller とかなら自明なのかもしれないけれど"/> <node CREATED="1418181672890" ID="ID_1680851110" MODIFIED="1418181688101" TEXT="それが有用なのか、って次元を語るにはまだ経験が足りてない"> <node CREATED="1418181695297" ID="ID_78590582" MODIFIED="1418181704180" TEXT="とはいえ1年分はやってる計算なのか"/> </node> </node> </node> </node> <node CREATED="1418181719512" ID="ID_1778092327" MODIFIED="1418181771222" POSITION="right" TEXT="私の考え"> <node CREATED="1418181723657" ID="ID_1975836647" MODIFIED="1418181767752" TEXT="理想"> <node CREATED="1418181724721" ID="ID_24312002" MODIFIED="1418181726951" TEXT="自動化したい"> <node CREATED="1418181726952" ID="ID_768596212" MODIFIED="1418181733896" TEXT="バグの検出"> <node CREATED="1418181733897" ID="ID_566566124" MODIFIED="1418181737899" TEXT="想定外の仕様とか"/> <node CREATED="1418181738872" ID="ID_486640500" MODIFIED="1418181781025" TEXT="満たしてない条件とか"/> <node CREATED="1418181781247" ID="ID_1294427996" MODIFIED="1418181784249" TEXT="例外とか"/> <node CREATED="1418181784846" ID="ID_1490731973" MODIFIED="1418181791081" TEXT="実際バグの種類って何があるのだろう"/> <node CREATED="1418181960406" ID="ID_601452297" MODIFIED="1418181971910" TEXT="特殊なの"> <node CREATED="1418181971911" ID="ID_298778954" MODIFIED="1418181973393" TEXT="副作用"/> <node CREATED="1418181973614" ID="ID_284089863" MODIFIED="1418181984265" TEXT="並列時にのみ起きる"/> <node CREATED="1418181984485" ID="ID_783522097" MODIFIED="1418182014303" TEXT="たぶんこれらは順番の問題かな"/> </node> </node> <node CREATED="1418181743991" ID="ID_1564140730" MODIFIED="1418181760964" TEXT="通常のソースを意識せずに書いてどうこうしたい"> <node CREATED="1418182245347" ID="ID_304940298" MODIFIED="1418182247219" TEXT="通常とは"> <node CREATED="1418182247220" ID="ID_621892916" MODIFIED="1418182250411" TEXT="おそらく"> <node CREATED="1418182250412" ID="ID_1727870100" MODIFIED="1418182254614" TEXT="構造化プログラミング"/> <node CREATED="1418182254834" ID="ID_1377709393" MODIFIED="1418182257573" TEXT="オブジェクト指向"/> <node CREATED="1418182257820" ID="ID_1208383542" MODIFIED="1418182260864" TEXT="関数型"/> </node> </node> </node> <node CREATED="1418182273546" ID="ID_1167120953" MODIFIED="1418182278698" TEXT="つまり言語レベルでサポートしたい"> <node CREATED="1418182278699" ID="ID_1498408070" MODIFIED="1418182285404" TEXT="そのために必要なのは何かを考えないといけない"/> </node> </node> </node> <node CREATED="1418181793613" ID="ID_865440637" MODIFIED="1418181795982" TEXT="どうするのか"> <node CREATED="1418181795983" ID="ID_1355385238" MODIFIED="1418181805031" TEXT="どれだけの情報があればバグを検出できる?"> <node CREATED="1418181828645" ID="ID_1429160748" MODIFIED="1418181838951" TEXT="それを知らないといけない"/> <node CREATED="1418181848050" ID="ID_282731223" MODIFIED="1418181950485" TEXT="たとえば"> <node CREATED="1418181805032" ID="ID_73966373" MODIFIED="1418181811384" TEXT="おきえる例外一覧"/> <node CREATED="1418181811989" ID="ID_1539486184" MODIFIED="1418181825687" TEXT="型による値の取りえる範囲"/> <node CREATED="1418181854618" ID="ID_1158859050" MODIFIED="1418181861549" TEXT="用意された構文"/> <node CREATED="1418181861811" ID="ID_605487006" MODIFIED="1418181868605" TEXT="外部パッケージとの連携"/> <node CREATED="1418181951238" ID="ID_1351920238" MODIFIED="1418181957613" TEXT="デッドロック"/> </node> </node> <node CREATED="1418181878201" ID="ID_1385164960" MODIFIED="1418181888298" TEXT="その情報をどうやってバグを見つけて警告するか"> <node CREATED="1418181888299" ID="ID_1389711641" MODIFIED="1418181896949" TEXT="条件網羅的"/> <node CREATED="1418181897178" ID="ID_746549506" MODIFIED="1418181903444" TEXT="値への動作が undefined"/> <node CREATED="1418181905560" ID="ID_1204757281" MODIFIED="1418181913440" TEXT="undefined じゃなくてミスるのが厄介"> <node CREATED="1418181913441" ID="ID_768690529" MODIFIED="1418181919764" TEXT="レンジを出す"/> <node CREATED="1418181920808" ID="ID_1152696018" MODIFIED="1418181924706" TEXT="その程度で見つかんのか"/> </node> </node> <node CREATED="1418182323894" ID="ID_555056207" MODIFIED="1418182339207" TEXT="それらを満たす言語を使って書くべき"> <node CREATED="1418182365815" ID="ID_297560677" MODIFIED="1418182386664" TEXT="つまり"> <node CREATED="1418182354271" ID="ID_1499062376" MODIFIED="1418182364882" TEXT="情報からバグへの流れも明示的"/> <node CREATED="1418182339208" ID="ID_30956356" MODIFIED="1418182353825" TEXT="必要な情報が明示的に分かる"/> </node> <node CREATED="1418182372478" ID="ID_895703509" MODIFIED="1418182377329" TEXT="というか人間がチェックするもんじゃない"/> <node CREATED="1418182391333" ID="ID_1660768254" MODIFIED="1418182401408" TEXT="べつに現状の言語解析でも良いっちゃ良い"> <node CREATED="1418182403949" ID="ID_1855838686" MODIFIED="1418182412247" TEXT="ただ、対応を取るのが可能とは思えない"/> <node CREATED="1418182412556" ID="ID_80188673" MODIFIED="1418182424135" TEXT="とりあえず対応がいけてるっぽい言語を考えるのが安直だと思う"/> </node> </node> </node> <node CREATED="1418185640611" ID="ID_648398253" MODIFIED="1418185644652" TEXT="まとめ"> <node CREATED="1418185644653" ID="ID_394508811" MODIFIED="1418185668716" TEXT="形式手法からの情報は対話的に手に入るべき"> <node CREATED="1418185668716" ID="ID_312721489" MODIFIED="1418185679637" TEXT="いらないならいらない"> <node CREATED="1418187792947" ID="ID_869688654" MODIFIED="1418187799289" TEXT="それでも generic なのはあるはず"> <node CREATED="1418187799806" ID="ID_445879821" MODIFIED="1418187806064" TEXT="devide by 0"/> <node CREATED="1418187806533" ID="ID_983998348" MODIFIED="1418187812960" TEXT="ivalid index"/> </node> </node> <node CREATED="1418185679850" ID="ID_1108864490" MODIFIED="1418185699325" TEXT="必要ならどれだけでも欲しい"> <node CREATED="1418187815388" ID="ID_719300461" MODIFIED="1418187825368" TEXT="それを記述する能力も欲しい"/> </node> </node> <node CREATED="1418185701065" ID="ID_1261000963" MODIFIED="1418185707122" TEXT="その情報はどれだけ必要なのか"> <node CREATED="1418185707123" ID="ID_369768931" MODIFIED="1418185712564" TEXT="それを探したい"/> <node CREATED="1418185716713" ID="ID_327038586" MODIFIED="1418185724378" TEXT="注目してるのは型"> <node CREATED="1418185724379" ID="ID_247247026" MODIFIED="1418185727947" TEXT="実際どうなのかはともかく"/> <node CREATED="1418185732064" ID="ID_1593924626" MODIFIED="1418185737396" TEXT="今のところはそこそこ良さそう"/> </node> </node> </node> </node> <node CREATED="1418182444156" ID="ID_803786977" MODIFIED="1418182448263" POSITION="left" TEXT="Agda とかどうだったのか"> <node CREATED="1418182448643" ID="ID_1005517265" MODIFIED="1418182451404" TEXT="学習コスト"> <node CREATED="1418182451404" ID="ID_1000430200" MODIFIED="1418182464741" TEXT="正直エラー読んで分かるもんじゃなかった"/> <node CREATED="1418182465339" ID="ID_434679711" MODIFIED="1418182475293" TEXT="どちらかと言えば満たすべき sub-proof を吐くもの"/> <node CREATED="1418182478306" ID="ID_716180383" MODIFIED="1418182497592" TEXT="とりあえず性質先行である必要がある"> <node CREATED="1418182497593" ID="ID_1456688053" MODIFIED="1418182501365" TEXT="それから定義を考える"/> <node CREATED="1418182502066" ID="ID_5465711" MODIFIED="1418182508932" TEXT="それを満たすまでひたすらに書く、って感じ"/> </node> </node> <node CREATED="1418182512745" ID="ID_484097984" MODIFIED="1418182544055" TEXT="duck typiing とは真逆をいってるはず"> <node CREATED="1418182544056" ID="ID_1664375557" MODIFIED="1418182553106" TEXT="とりあえず、って訳にはいかない"/> <node CREATED="1418182553344" ID="ID_1803463788" MODIFIED="1418182561961" TEXT="満たすまで終わらないぜ的な"/> </node> <node CREATED="1418182565614" ID="ID_228954736" MODIFIED="1418182568238" TEXT="どっちかと言えば"> <node CREATED="1418182568239" ID="ID_943070641" MODIFIED="1418182576222" TEXT="Algorithm の方が良いのかな"> <node CREATED="1418182576223" ID="ID_1021999389" MODIFIED="1418182593844" TEXT="SSL のアレとか"/> <node CREATED="1418182595365" ID="ID_1131465800" MODIFIED="1418182603231" TEXT="ゲームルールとか"/> </node> <node CREATED="1418182604204" ID="ID_1236591481" MODIFIED="1418182610838" TEXT="別にデータ構造のやつでも良いんだけれど"> <node CREATED="1418182616532" ID="ID_1450828974" MODIFIED="1418182626462" TEXT="既にある証明の rewrite"/> <node CREATED="1418182627301" ID="ID_899694880" MODIFIED="1418182634270" TEXT="あれと同じ、みたいなことになる"/> <node CREATED="1418182634645" ID="ID_146613907" MODIFIED="1418182646559" TEXT="とりあえず適当に作ってこれどうなの、とするにはコストが高すぎる"/> <node CREATED="1418182646788" ID="ID_470200250" MODIFIED="1418182663405" TEXT="water fall の仕様定義レベルでこれを書いちゃえばたぶん万全な仕様になりかねない"> <node CREATED="1418182663986" ID="ID_1522360088" MODIFIED="1418182668261" TEXT="でもたぶんこっちのが時間かかる"/> </node> </node> </node> </node> </node> </map>