Mercurial > hg > Papers > 2015 > atton-osc
changeset 0:7e1b309f3181
Add mindmap
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 20 May 2014 09:17:13 +0900 |
parents | |
children | c2e4b521d70c |
files | mindmap/osc2014.mm |
diffstat | 1 files changed, 85 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/mindmap/osc2014.mm Tue May 20 09:17:13 2014 +0900 @@ -0,0 +1,85 @@ +<map version="1.0.1"> +<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> +<node CREATED="1400543905917" ID="ID_572481524" MODIFIED="1400544155826" TEXT="OSC 2014"> +<node CREATED="1400543915755" ID="ID_1881286788" MODIFIED="1400543934606" POSITION="right" TEXT="Agda ネタ"> +<node CREATED="1400543939233" ID="ID_82647617" MODIFIED="1400543946927" TEXT="Peano Arithmetic"> +<node CREATED="1400544002554" ID="ID_1908147492" MODIFIED="1400544012244" TEXT="plus の交換法則"/> +<node CREATED="1400544019033" ID="ID_1616944195" MODIFIED="1400544186159" TEXT="dependencies"> +<node CREATED="1400544020530" ID="ID_12255115" MODIFIED="1400544029200" TEXT="equiv"> +<node CREATED="1400544029201" ID="ID_1489679280" MODIFIED="1400544032137" TEXT="normal form"> +<node CREATED="1400544032138" ID="ID_1421581484" MODIFIED="1400544231661" TEXT="lambda calculus"/> +<node CREATED="1400544045529" ID="ID_1071625493" MODIFIED="1400544050971" TEXT="beta-conversion"/> +</node> +<node CREATED="1400544094024" ID="ID_1739106366" MODIFIED="1400544201780" TEXT="equivalence"> +<node CREATED="1400544101561" ID="ID_477072376" MODIFIED="1400544102691" TEXT="refl"/> +<node CREATED="1400544103344" ID="ID_447392236" MODIFIED="1400544104058" TEXT="cong"/> +<node CREATED="1400544104312" ID="ID_1376962116" MODIFIED="1400544105690" TEXT="sym"/> +<node CREATED="1400544241667" ID="ID_1385721627" MODIFIED="1400544250127" TEXT="implicit arguments"/> +</node> +</node> +<node CREATED="1400544053257" ID="ID_675589478" MODIFIED="1400544066791" TEXT="Curry-Howard Isorophism"/> +<node CREATED="1400544079648" ID="ID_1462867262" MODIFIED="1400544081132" TEXT="Int"> +<node CREATED="1400544081839" ID="ID_532962324" MODIFIED="1400544087648" TEXT="data type"/> +</node> +<node CREATED="1400544377264" ID="ID_878106016" MODIFIED="1400544380714" TEXT="curry"/> +</node> +</node> +<node CREATED="1400543947180" ID="ID_1096006602" MODIFIED="1400543953110" TEXT="Refactor"> +<node CREATED="1400543973523" ID="ID_708710018" MODIFIED="1400543992971" TEXT="計算量が大きいものを定義して、小さいものと equiv であることを示す"> +<node CREATED="1400543992972" ID="ID_1112644761" MODIFIED="1400544000933" TEXT="何を書こうか。"/> +</node> +<node CREATED="1400544253412" ID="ID_1144242288" MODIFIED="1400544258074" TEXT="dependencies"> +<node CREATED="1400544267275" ID="ID_333289312" MODIFIED="1400544270415" TEXT="equiv"/> +</node> +</node> +<node CREATED="1400543953836" ID="ID_1008043602" MODIFIED="1400543969278" TEXT="何かの証明"> +<node CREATED="1400544014081" ID="ID_610236385" MODIFIED="1400544396086" TEXT="ネタ"> +<node CREATED="1400544397336" ID="ID_1639922482" MODIFIED="1400544401098" TEXT="三段論法"/> +<node CREATED="1400544401873" ID="ID_1559034607" MODIFIED="1400544408723" TEXT="逆裏対偶"/> +<node CREATED="1400544409137" ID="ID_1359908753" MODIFIED="1400544416211" TEXT="ドモルガン"/> +</node> +<node CREATED="1400544277178" ID="ID_267304939" MODIFIED="1400544279859" TEXT="dependencies"> +<node CREATED="1400544279860" ID="ID_651703274" MODIFIED="1400544319455" TEXT="Curry-Howard Isomorphism"/> +<node CREATED="1400544418632" ID="ID_318116560" MODIFIED="1400544420249" TEXT="Bool"/> +<node CREATED="1400544420528" ID="ID_1938809075" MODIFIED="1400544425702" TEXT="curry"/> +</node> +</node> +</node> +<node CREATED="1400544431341" ID="ID_94556426" MODIFIED="1400544435606" POSITION="left" TEXT="なんかツッコミ"> +<node CREATED="1400544435607" ID="ID_1082634470" MODIFIED="1400544440034" TEXT="どうしてAgda"> +<node CREATED="1400544694192" ID="ID_307683680" MODIFIED="1400544708948" TEXT="純粋な証明以外にも型システムとか扱いたいから"> +<node CREATED="1400544440582" ID="ID_1919074718" MODIFIED="1400544685608" TEXT="Coq はどんなんだろ"> +<node CREATED="1400544685609" ID="ID_1690844308" MODIFIED="1400544691034" TEXT="こんなん出てきた http://www.slideshare.net/qnighy/coq-13942184"/> +<node CREATED="1400544715808" ID="ID_1666336070" MODIFIED="1400544718066" TEXT="あるっぽいですね"/> +</node> +</node> +<node CREATED="1400544719408" ID="ID_892216000" MODIFIED="1400544727506" TEXT="Haskell で実装されてるから"> +<node CREATED="1400544727760" ID="ID_653063223" MODIFIED="1400544740299" TEXT="当研究室ではJungle-Haskell ってます"/> +<node CREATED="1400544741696" ID="ID_1949376399" MODIFIED="1400544755252" TEXT="syntax も Haskell 寄りだし?"/> +</node> +</node> +<node CREATED="1400544809531" ID="ID_369452116" MODIFIED="1400544824654" TEXT="Peano Arithmetic と church encoding の違い"> +<node CREATED="1400544824655" ID="ID_1123191209" MODIFIED="1400544829294" TEXT="Peano Arithmetic"> +<node CREATED="1400544829295" ID="ID_1573888283" MODIFIED="1400544838551" TEXT="自然数の表現の一種"> +<node CREATED="1400544839549" ID="ID_1503714497" MODIFIED="1400544847507" TEXT="0と後続数"/> +<node CREATED="1400544857915" ID="ID_1085255413" MODIFIED="1400544860373" TEXT="http://ja.wikipedia.org/wiki/%E3%83%9A%E3%82%A2%E3%83%8E%E3%81%AE%E5%85%AC%E7%90%86"/> +<node CREATED="1400544915539" ID="ID_1127823211" MODIFIED="1400544925384" TEXT="厳密な定義だと5つほど条件があるらしい"/> +</node> +</node> +<node CREATED="1400544863460" ID="ID_1790572502" MODIFIED="1400544867300" TEXT="church encoding"> +<node CREATED="1400544867301" ID="ID_1523964511" MODIFIED="1400544886375" TEXT="f : Int -> Int"/> +<node CREATED="1400544886805" ID="ID_1530260883" MODIFIED="1400544889062" TEXT="x : Int"/> +<node CREATED="1400544889364" ID="ID_1602645307" MODIFIED="1400544912255" TEXT="の型を持つ要素で構成される lambda-term"/> +</node> +<node CREATED="1400544974071" ID="ID_275800070" MODIFIED="1400544981096" TEXT="Agda の内部表現的には"> +<node CREATED="1400544981097" ID="ID_662247882" MODIFIED="1400544985953" TEXT="Peano Arithmetic"> +<node CREATED="1400544985954" ID="ID_273027252" MODIFIED="1400544987566" TEXT="data"/> +</node> +<node CREATED="1400544988513" ID="ID_772843893" MODIFIED="1400544991568" TEXT="church encoding"> +<node CREATED="1400544991569" ID="ID_627768019" MODIFIED="1400544997567" TEXT="lambda"/> +</node> +</node> +</node> +</node> +</node> +</map>