Mercurial > hg > Papers > 2015 > atton-osc

view mindmap/osc2014.mm @ 4:1d22fbc3680d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update mindmap
author atton
date Wed, 21 May 2014 19:55:16 +0900
parents 7e1b309f3181
children
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="1400543905917" ID="ID_572481524" MODIFIED="1400668661914" TEXT="OSC 2014">
<node CREATED="1400543915755" ID="ID_1881286788" MODIFIED="1400543934606" POSITION="right" TEXT="Agda &#x30cd;&#x30bf;">
<node CREATED="1400543939233" ID="ID_82647617" MODIFIED="1400543946927" TEXT="Peano Arithmetic">
<node CREATED="1400544002554" ID="ID_1908147492" MODIFIED="1400544012244" TEXT="plus &#x306e;&#x4ea4;&#x63db;&#x6cd5;&#x5247;"/>
<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="&#x8a08;&#x7b97;&#x91cf;&#x304c;&#x5927;&#x304d;&#x3044;&#x3082;&#x306e;&#x3092;&#x5b9a;&#x7fa9;&#x3057;&#x3066;&#x3001;&#x5c0f;&#x3055;&#x3044;&#x3082;&#x306e;&#x3068; equiv &#x3067;&#x3042;&#x308b;&#x3053;&#x3068;&#x3092;&#x793a;&#x3059;">
<node CREATED="1400543992972" ID="ID_1112644761" MODIFIED="1400544000933" TEXT="&#x4f55;&#x3092;&#x66f8;&#x3053;&#x3046;&#x304b;&#x3002;"/>
</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="&#x4f55;&#x304b;&#x306e;&#x8a3c;&#x660e;">
<node CREATED="1400544014081" ID="ID_610236385" MODIFIED="1400544396086" TEXT="&#x30cd;&#x30bf;">
<node CREATED="1400544397336" ID="ID_1639922482" MODIFIED="1400544401098" TEXT="&#x4e09;&#x6bb5;&#x8ad6;&#x6cd5;"/>
<node CREATED="1400544401873" ID="ID_1559034607" MODIFIED="1400544408723" TEXT="&#x9006;&#x88cf;&#x5bfe;&#x5076;"/>
<node CREATED="1400544409137" ID="ID_1359908753" MODIFIED="1400544416211" TEXT="&#x30c9;&#x30e2;&#x30eb;&#x30ac;&#x30f3;"/>
</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="&#x306a;&#x3093;&#x304b;&#x30c4;&#x30c3;&#x30b3;&#x30df;">
<node CREATED="1400544435607" ID="ID_1082634470" MODIFIED="1400544440034" TEXT="&#x3069;&#x3046;&#x3057;&#x3066;Agda">
<node CREATED="1400544694192" ID="ID_307683680" MODIFIED="1400544708948" TEXT="&#x7d14;&#x7c8b;&#x306a;&#x8a3c;&#x660e;&#x4ee5;&#x5916;&#x306b;&#x3082;&#x578b;&#x30b7;&#x30b9;&#x30c6;&#x30e0;&#x3068;&#x304b;&#x6271;&#x3044;&#x305f;&#x3044;&#x304b;&#x3089;">
<node CREATED="1400544440582" ID="ID_1919074718" MODIFIED="1400544685608" TEXT="Coq &#x306f;&#x3069;&#x3093;&#x306a;&#x3093;&#x3060;&#x308d;">
<node CREATED="1400544685609" ID="ID_1690844308" MODIFIED="1400544691034" TEXT="&#x3053;&#x3093;&#x306a;&#x3093;&#x51fa;&#x3066;&#x304d;&#x305f; http://www.slideshare.net/qnighy/coq-13942184"/>
<node CREATED="1400544715808" ID="ID_1666336070" MODIFIED="1400544718066" TEXT="&#x3042;&#x308b;&#x3063;&#x307d;&#x3044;&#x3067;&#x3059;&#x306d;"/>
</node>
</node>
<node CREATED="1400544719408" ID="ID_892216000" MODIFIED="1400544727506" TEXT="Haskell &#x3067;&#x5b9f;&#x88c5;&#x3055;&#x308c;&#x3066;&#x308b;&#x304b;&#x3089;">
<node CREATED="1400544727760" ID="ID_653063223" MODIFIED="1400544740299" TEXT="&#x5f53;&#x7814;&#x7a76;&#x5ba4;&#x3067;&#x306f;Jungle-Haskell &#x3063;&#x3066;&#x307e;&#x3059;"/>
<node CREATED="1400544741696" ID="ID_1949376399" MODIFIED="1400544755252" TEXT="syntax &#x3082; Haskell &#x5bc4;&#x308a;&#x3060;&#x3057;?"/>
</node>
</node>
<node CREATED="1400544809531" ID="ID_369452116" MODIFIED="1400544824654" TEXT="Peano Arithmetic &#x3068; church encoding &#x306e;&#x9055;&#x3044;">
<node CREATED="1400544824655" ID="ID_1123191209" MODIFIED="1400544829294" TEXT="Peano Arithmetic">
<node CREATED="1400544829295" ID="ID_1573888283" MODIFIED="1400544838551" TEXT="&#x81ea;&#x7136;&#x6570;&#x306e;&#x8868;&#x73fe;&#x306e;&#x4e00;&#x7a2e;">
<node CREATED="1400544839549" ID="ID_1503714497" MODIFIED="1400544847507" TEXT="0&#x3068;&#x5f8c;&#x7d9a;&#x6570;"/>
<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="&#x53b3;&#x5bc6;&#x306a;&#x5b9a;&#x7fa9;&#x3060;&#x3068;5&#x3064;&#x307b;&#x3069;&#x6761;&#x4ef6;&#x304c;&#x3042;&#x308b;&#x3089;&#x3057;&#x3044;"/>
</node>
</node>
<node CREATED="1400544863460" ID="ID_1790572502" MODIFIED="1400544867300" TEXT="church encoding">
<node CREATED="1400544867301" ID="ID_1523964511" MODIFIED="1400544886375" TEXT="f : Int -&gt; Int"/>
<node CREATED="1400544886805" ID="ID_1530260883" MODIFIED="1400544889062" TEXT="x : Int"/>
<node CREATED="1400544889364" ID="ID_1602645307" MODIFIED="1400544912255" TEXT="&#x306e;&#x578b;&#x3092;&#x6301;&#x3064;&#x8981;&#x7d20;&#x3067;&#x69cb;&#x6210;&#x3055;&#x308c;&#x308b; lambda-term"/>
</node>
<node CREATED="1400544974071" ID="ID_275800070" MODIFIED="1400544981096" TEXT="Agda &#x306e;&#x5185;&#x90e8;&#x8868;&#x73fe;&#x7684;&#x306b;&#x306f;">
<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 CREATED="1400668663626" ID="ID_515690773" MODIFIED="1400668674190" POSITION="right" TEXT="&#x4f55;&#x3092;&#x308f;&#x304b;&#x3063;&#x3066;&#x3082;&#x3089;&#x3046;&#x304b;">
<node CREATED="1400669027632" ID="ID_1085165502" MODIFIED="1400669031320" TEXT="bacic of agda">
<node CREATED="1400669031321" ID="ID_1335142822" MODIFIED="1400669037091" TEXT="type and value"/>
<node CREATED="1400669040016" ID="ID_1784465189" MODIFIED="1400669045363" TEXT="lambda term"/>
</node>
<node CREATED="1400668769696" ID="ID_1216787910" MODIFIED="1400668773939" TEXT="peano arithmetic">
<node CREATED="1400668874217" ID="ID_657325662" MODIFIED="1400668875283" TEXT="add"/>
<node CREATED="1400668875848" ID="ID_1416777243" MODIFIED="1400668876555" TEXT="mul"/>
</node>
<node CREATED="1400669110897" ID="ID_410845070" MODIFIED="1400669115193" TEXT="operation of agda">
<node CREATED="1400669054288" ID="ID_101951478" MODIFIED="1400669056059" TEXT="?">
<node CREATED="1400669058504" ID="ID_577677812" MODIFIED="1400669059691" TEXT="goal"/>
</node>
<node CREATED="1400669068408" ID="ID_397237814" MODIFIED="1400669083107" TEXT="normarization">
<node CREATED="1400669128112" ID="ID_1701331628" MODIFIED="1400669137593" TEXT="1 + 1 = 2"/>
</node>
</node>
<node CREATED="1400669153273" ID="ID_388850162" MODIFIED="1400669164929" TEXT="description of target lemma"/>
<node CREATED="1400669007079" ID="ID_1284884272" MODIFIED="1400669015667" TEXT="equivalence definition"/>
<node CREATED="1400668794345" ID="ID_1629665659" MODIFIED="1400668826873" TEXT="equivalence">
<node CREATED="1400668831080" ID="ID_1585589019" MODIFIED="1400668833099" TEXT="refl"/>
<node CREATED="1400668833624" ID="ID_1759609548" MODIFIED="1400668838227" TEXT="sym"/>
<node CREATED="1400668838825" ID="ID_745967048" MODIFIED="1400668840787" TEXT="trans"/>
</node>
<node CREATED="1400668706802" ID="ID_1359244831" MODIFIED="1400668744059" TEXT="Reasoning on Agda">
<node CREATED="1400669556825" ID="ID_1133406151" MODIFIED="1400669561496" TEXT="motivation">
<node CREATED="1400669561497" ID="ID_1910699629" MODIFIED="1400669573003" TEXT="1 + 2 + 3 = 3 + 3 = 6"/>
<node CREATED="1400669573952" ID="ID_1325133153" MODIFIED="1400669588298" TEXT="part of equality : 1 + 2 = 3"/>
</node>
<node CREATED="1400668748320" ID="ID_1294472557" MODIFIED="1400668752265" TEXT="example">
<node CREATED="1400669244641" ID="ID_762502821" MODIFIED="1400669252051" TEXT="refl reasoning"/>
<node CREATED="1400669324920" ID="ID_1483054930" MODIFIED="1400669368609" TEXT="reasoning template"/>
<node CREATED="1400669305881" ID="ID_970615230" MODIFIED="1400669373873" TEXT="normarization">
<node CREATED="1400669373873" ID="ID_603853377" MODIFIED="1400669433235" TEXT="start element"/>
<node CREATED="1400669433616" ID="ID_1227888812" MODIFIED="1400669437355" TEXT="end element"/>
</node>
</node>
<node CREATED="1400668902216" ID="ID_1361569494" MODIFIED="1400668916857" TEXT="lenmma">
<node CREATED="1400668889305" ID="ID_285305355" MODIFIED="1400668892217" TEXT="add-sym"/>
<node CREATED="1400668926480" ID="ID_1918706488" MODIFIED="1400668931227" TEXT="add-assoc"/>
<node CREATED="1400668934776" ID="ID_986075106" MODIFIED="1400668942035" TEXT="add-distribution">
<node CREATED="1400668949720" ID="ID_1695784338" MODIFIED="1400668953843" TEXT="add-distribution-one"/>
</node>
<node CREATED="1400668961584" ID="ID_1753300084" MODIFIED="1400668965986" TEXT="mul-sym">
<node CREATED="1400669498496" ID="ID_1279020545" MODIFIED="1400669501617" TEXT="target"/>
</node>
<node CREATED="1400668982217" ID="ID_346491763" MODIFIED="1400668987081" TEXT="mul-assoc"/>
</node>
</node>
</node>
</node>
</map>