Mercurial > hg > Papers > 2015 > atton-thesis

changeset 1:d8386a964947

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add mind map
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 17:23:44 +0900
parents 03fbdce3fb87
children 1e28ac702c1e
files .hgignore mindmap/mindmap.mm
diffstat 2 files changed, 195 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Tue Feb 03 16:47:18 2015 +0900
+++ b/.hgignore	Tue Feb 03 17:23:44 2015 +0900
@@ -4,6 +4,8 @@
 
 *.swp
 
+*.lof
+*.lot
 *.log
 *.aux
 *.dvi
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/mindmap/mindmap.mm	Tue Feb 03 17:23:44 2015 +0900
@@ -0,0 +1,193 @@
+<map version="1.0.1">
+<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
+<node CREATED="1422949791529" ID="ID_1248140398" MODIFIED="1422949804941" TEXT="Categorical Formalization for Program Modification">
+<node CREATED="1422949835922" ID="ID_1426063364" MODIFIED="1422949839172" POSITION="right" TEXT="Category">
+<node CREATED="1422949860903" ID="ID_1292695301" MODIFIED="1422949916428" TEXT="Category">
+<node CREATED="1422949866542" ID="ID_1518583103" MODIFIED="1422949868440" TEXT="object"/>
+<node CREATED="1422949868693" ID="ID_415242676" MODIFIED="1422949871944" TEXT="morphism"/>
+<node CREATED="1422949872157" ID="ID_357562664" MODIFIED="1422949875175" TEXT="arrow composition"/>
+</node>
+<node CREATED="1422949904913" ID="ID_1689417330" MODIFIED="1422949919057" TEXT="Functor">
+<node CREATED="1422949919058" ID="ID_1189883928" MODIFIED="1422949921851" TEXT="functor-laws"/>
+</node>
+<node CREATED="1422949923200" ID="ID_1358081223" MODIFIED="1422949927570" TEXT="natural transformation"/>
+<node CREATED="1422949930607" ID="ID_1546681698" MODIFIED="1422949932624" TEXT="Monad">
+<node CREATED="1422949932625" ID="ID_686090142" MODIFIED="1422949933778" TEXT="mu"/>
+<node CREATED="1422949934015" ID="ID_1478454300" MODIFIED="1422949934682" TEXT="eta"/>
+<node CREATED="1422949934919" ID="ID_496949840" MODIFIED="1422949936314" TEXT="monad-laws"/>
+<node CREATED="1422949938327" ID="ID_324416662" MODIFIED="1422949942353" TEXT="Kleisli Triple"/>
+</node>
+<node CREATED="1422950034982" ID="ID_903584038" MODIFIED="1422950165676" TEXT="Details">
+<node CREATED="1422949839408" ID="ID_1137787025" MODIFIED="1422949842274" TEXT="Product"/>
+<node CREATED="1422949843352" ID="ID_1693669846" MODIFIED="1422949845923" TEXT="CoProduct"/>
+<node CREATED="1422949846807" ID="ID_1543846313" MODIFIED="1422949849354" TEXT="Limit"/>
+<node CREATED="1422949850023" ID="ID_1212007111" MODIFIED="1422949852097" TEXT="CoLimit"/>
+<node CREATED="1422950168729" ID="ID_552214019" MODIFIED="1422950172819" TEXT="Equalizer"/>
+<node CREATED="1422950173065" ID="ID_486753790" MODIFIED="1422950175819" TEXT="CoEqualizer"/>
+<node CREATED="1422950176360" ID="ID_15015375" MODIFIED="1422950201097" TEXT="Proof through Indexed Category">
+<node CREATED="1422950538510" ID="ID_146756811" MODIFIED="1422950548362" TEXT="Introduction to higher order categorical logic"/>
+</node>
+</node>
+<node CREATED="1422950167033" ID="ID_1012510608" MODIFIED="1422950189114" TEXT="Adjoint">
+<node CREATED="1422950431432" ID="ID_1364735058" MODIFIED="1422950432226" TEXT="?"/>
+</node>
+<node CREATED="1422950210301" ID="ID_1162629391" MODIFIED="1422950275793" TEXT="Monad in Functional Programming">
+<node CREATED="1422950218132" ID="ID_275907320" MODIFIED="1422950233440" TEXT="Notions of Computations and Monads">
+<node CREATED="1422950234587" ID="ID_700434335" MODIFIED="1422950235525" TEXT="moggi"/>
+</node>
+<node CREATED="1422950236802" ID="ID_1229215612" MODIFIED="1422950244626" TEXT="examples of monads">
+<node CREATED="1422950244627" ID="ID_916207265" MODIFIED="1422950246716" TEXT="fail"/>
+<node CREATED="1422950247297" ID="ID_1502867290" MODIFIED="1422950250804" TEXT="non-determinism"/>
+<node CREATED="1422950251273" ID="ID_649095094" MODIFIED="1422950254907" TEXT="interactive input"/>
+<node CREATED="1422950293172" ID="ID_466802075" MODIFIED="1422950305571" TEXT="Categorical Definition of Delta?"/>
+</node>
+</node>
+<node CREATED="1422950445399" ID="ID_1843980612" MODIFIED="1422950448079" TEXT="morphisms">
+<node CREATED="1422950448080" ID="ID_1951830123" MODIFIED="1422950452073" TEXT="isomorphism"/>
+<node CREATED="1422950452334" ID="ID_1834101596" MODIFIED="1422950457080" TEXT="automorphism"/>
+</node>
+</node>
+<node CREATED="1422950314563" ID="ID_37453596" MODIFIED="1422950317077" POSITION="left" TEXT="Proofs">
+<node CREATED="1422950317403" ID="ID_1897119854" MODIFIED="1422950322693" TEXT="First Order Logic">
+<node CREATED="1422950323025" ID="ID_1209193790" MODIFIED="1422950323025" TEXT=""/>
+</node>
+<node CREATED="1422950326153" ID="ID_1972293244" MODIFIED="1422950331796" TEXT="Natural Deduction">
+<node CREATED="1422950333112" ID="ID_1751485732" MODIFIED="1422950360961" TEXT="imply"/>
+<node CREATED="1422950350591" ID="ID_1918801475" MODIFIED="1422950357378" TEXT="or"/>
+<node CREATED="1422950352360" ID="ID_868465468" MODIFIED="1422950354026" TEXT="and"/>
+<node CREATED="1422950406786" ID="ID_1244618529" MODIFIED="1422950411617" TEXT="Quantifiers">
+<node CREATED="1422950411618" ID="ID_1696313791" MODIFIED="1422950414228" TEXT="universal"/>
+<node CREATED="1422950414458" ID="ID_614614777" MODIFIED="1422950417188" TEXT="exsistentional"/>
+</node>
+</node>
+<node CREATED="1422950385771" ID="ID_1341835209" MODIFIED="1422950399809" TEXT="Sequent Calculs ?"/>
+<node CREATED="1422950418761" ID="ID_502598820" MODIFIED="1422950425157" TEXT="Curry-Howard Isomorphism">
+<node CREATED="1422950468660" ID="ID_1065234683" MODIFIED="1422950474039" TEXT="Proofs and Types">
+<node CREATED="1422950477468" ID="ID_224493054" MODIFIED="1422950484342" TEXT="girard"/>
+</node>
+<node CREATED="1422950865446" ID="ID_1790265469" MODIFIED="1422950873384" TEXT="proof methods in types">
+<node CREATED="1422950873934" ID="ID_871077428" MODIFIED="1422950875352" TEXT="refl"/>
+<node CREATED="1422950875806" ID="ID_1411556617" MODIFIED="1422950876416" TEXT="sym"/>
+<node CREATED="1422950876661" ID="ID_1072901715" MODIFIED="1422950880047" TEXT="cong"/>
+<node CREATED="1422950880261" ID="ID_1489517351" MODIFIED="1422950881015" TEXT="trans"/>
+</node>
+</node>
+<node CREATED="1422950561211" ID="ID_807654330" MODIFIED="1422950566478" TEXT="Dependent types">
+<node CREATED="1422950566691" ID="ID_1735441355" MODIFIED="1422950568799" TEXT="agda">
+<node CREATED="1422950885317" ID="ID_100810535" MODIFIED="1422950887591" TEXT="reasoning"/>
+<node CREATED="1422950891332" ID="ID_464079116" MODIFIED="1422950896806" TEXT="Set"/>
+<node CREATED="1422950897108" ID="ID_879720519" MODIFIED="1422950900150" TEXT="record">
+<node CREATED="1422950909298" ID="ID_730652438" MODIFIED="1422950916244" TEXT="Set of laws"/>
+</node>
+<node CREATED="1422950900939" ID="ID_989740172" MODIFIED="1422950903019" TEXT="examples">
+<node CREATED="1422950903020" ID="ID_1860288870" MODIFIED="1422950904917" TEXT="nat?"/>
+<node CREATED="1422950905299" ID="ID_603719171" MODIFIED="1422950906221" TEXT="list?"/>
+</node>
+<node CREATED="1422950920921" ID="ID_1186471863" MODIFIED="1422950921788" TEXT="data"/>
+<node CREATED="1422951522712" ID="ID_565512040" MODIFIED="1422951524707" TEXT="level"/>
+<node CREATED="1422951526632" ID="ID_415549755" MODIFIED="1422951528314" TEXT="equality"/>
+</node>
+</node>
+</node>
+<node CREATED="1422950570299" ID="ID_1923422030" MODIFIED="1422950707988" POSITION="right" TEXT="Delta Definitions">
+<node CREATED="1422950710220" ID="ID_1466431811" MODIFIED="1422950712444" TEXT="languages ">
+<node CREATED="1422950578931" ID="ID_1236151800" MODIFIED="1422950581988" TEXT="Haskell">
+<node CREATED="1422950717493" ID="ID_115506279" MODIFIED="1422950719479" TEXT="for sample"/>
+<node CREATED="1422950941367" ID="ID_1584306276" MODIFIED="1422950946257" TEXT="not have constraints"/>
+</node>
+<node CREATED="1422950582218" ID="ID_1801350600" MODIFIED="1422950583204" TEXT="Agda">
+<node CREATED="1422950720876" ID="ID_264850344" MODIFIED="1422950729046" TEXT="for proofs"/>
+<node CREATED="1422950948597" ID="ID_1984925220" MODIFIED="1422950951014" TEXT="have constraints">
+<node CREATED="1422950951015" ID="ID_75060203" MODIFIED="1422950952241" TEXT="mu"/>
+<node CREATED="1422950952454" ID="ID_623824422" MODIFIED="1422950953273" TEXT="eta"/>
+<node CREATED="1422950954894" ID="ID_838801152" MODIFIED="1422950956265" TEXT="and more"/>
+</node>
+</node>
+</node>
+<node CREATED="1422950583474" ID="ID_305480205" MODIFIED="1422950585378" TEXT="target">
+<node CREATED="1422950585379" ID="ID_177246050" MODIFIED="1422950614171" TEXT="automatically detection enbug">
+<node CREATED="1422950617726" ID="ID_114356602" MODIFIED="1422950644014" TEXT="not used property"/>
+</node>
+<node CREATED="1422950650682" ID="ID_567585682" MODIFIED="1422950657991" TEXT="formalizetion of  program modification">
+<node CREATED="1422950658986" ID="ID_45139927" MODIFIED="1422950661821" TEXT="repository"/>
+<node CREATED="1422950662113" ID="ID_1658619159" MODIFIED="1422950665604" TEXT="development methods"/>
+<node CREATED="1422950666346" ID="ID_1739084420" MODIFIED="1422950667356" TEXT="tests"/>
+</node>
+<node CREATED="1422951232715" ID="ID_1132611118" MODIFIED="1422951236174" TEXT="Improve Reliance">
+<node CREATED="1422951239307" ID="ID_549944525" MODIFIED="1422951241189" TEXT="Program"/>
+<node CREATED="1422951242331" ID="ID_1316714432" MODIFIED="1422951247165" TEXT="debug methods">
+<node CREATED="1422951259569" ID="ID_1234713209" MODIFIED="1422951262588" TEXT="parallel debuger"/>
+</node>
+</node>
+</node>
+<node CREATED="1422950689487" ID="ID_488480945" MODIFIED="1422950696545" TEXT="definitions">
+<node CREATED="1422950750178" ID="ID_1039114059" MODIFIED="1422950762395" TEXT="list with constraints">
+<node CREATED="1422950762855" ID="ID_699012514" MODIFIED="1422950774063" TEXT="non-nil list"/>
+<node CREATED="1422950769103" ID="ID_1886159495" MODIFIED="1422950807640" TEXT="all delta have same versions"/>
+</node>
+<node CREATED="1422950811956" ID="ID_958052648" MODIFIED="1422950840557" TEXT="functor">
+<node CREATED="1422950817412" ID="ID_1888805595" MODIFIED="1422950819629" TEXT="in haskell">
+<node CREATED="1422950832362" ID="ID_1817224697" MODIFIED="1422950833100" TEXT="fmap"/>
+</node>
+<node CREATED="1422950845169" ID="ID_1349607548" MODIFIED="1422950847042" TEXT="in agda">
+<node CREATED="1422950847042" ID="ID_1086817747" MODIFIED="1422950848163" TEXT="fmap"/>
+<node CREATED="1422950848640" ID="ID_1034792943" MODIFIED="1422950854024" TEXT="proofs">
+<node CREATED="1422950854025" ID="ID_1413122621" MODIFIED="1422950855642" TEXT="preserve-id"/>
+<node CREATED="1422950855855" ID="ID_1876757441" MODIFIED="1422950859042" TEXT="covariant"/>
+<node CREATED="1422950859335" ID="ID_1882223604" MODIFIED="1422950861433" TEXT="fmap-equiv"/>
+</node>
+</node>
+</node>
+<node CREATED="1422950820827" ID="ID_1537822947" MODIFIED="1422950822715" TEXT="monad">
+<node CREATED="1422950822716" ID="ID_1566056735" MODIFIED="1422950827589" TEXT="in haskell">
+<node CREATED="1422950827818" ID="ID_755996969" MODIFIED="1422950829516" TEXT="bind"/>
+<node CREATED="1422950830314" ID="ID_146123704" MODIFIED="1422950831236" TEXT="return"/>
+</node>
+<node CREATED="1422950966101" ID="ID_1913271013" MODIFIED="1422950967909" TEXT="in agda">
+<node CREATED="1422950967910" ID="ID_1404401270" MODIFIED="1422950969007" TEXT="eta"/>
+<node CREATED="1422950969221" ID="ID_388891102" MODIFIED="1422950969871" TEXT="mu"/>
+<node CREATED="1422950970261" ID="ID_439903450" MODIFIED="1422950978275" TEXT="proofs">
+<node CREATED="1422950983890" ID="ID_1297976526" MODIFIED="1422950989755" TEXT="unity-law">
+<node CREATED="1422950989756" ID="ID_1510051038" MODIFIED="1422950990677" TEXT="right"/>
+<node CREATED="1422950990882" ID="ID_226447138" MODIFIED="1422950992349" TEXT="left"/>
+</node>
+<node CREATED="1422950993306" ID="ID_502547745" MODIFIED="1422950995437" TEXT="association-law"/>
+</node>
+</node>
+</node>
+</node>
+<node CREATED="1422950999250" ID="ID_1737277691" MODIFIED="1422951001922" TEXT="with Monad">
+<node CREATED="1422951001923" ID="ID_1385758476" MODIFIED="1422951007107" TEXT="Inner Monad constraints">
+<node CREATED="1422951008785" ID="ID_460845815" MODIFIED="1422951046176" TEXT="functor">
+<node CREATED="1422951050237" ID="ID_1621733487" MODIFIED="1422951057039" TEXT="preserve-id"/>
+<node CREATED="1422951057291" ID="ID_987100412" MODIFIED="1422951059423" TEXT="covariant"/>
+<node CREATED="1422951059659" ID="ID_1739448000" MODIFIED="1422951061399" TEXT="fmap-equiv"/>
+</node>
+<node CREATED="1422951046390" ID="ID_1429702029" MODIFIED="1422951047456" TEXT="monad">
+<node CREATED="1422951063044" ID="ID_968778460" MODIFIED="1422951070803" TEXT="unity-law">
+<node CREATED="1422951070804" ID="ID_1073476437" MODIFIED="1422951072181" TEXT="right"/>
+<node CREATED="1422951072659" ID="ID_1444573713" MODIFIED="1422951074005" TEXT="left"/>
+</node>
+<node CREATED="1422951074851" ID="ID_1258522947" MODIFIED="1422951077701" TEXT="association-law"/>
+</node>
+</node>
+<node CREATED="1422951009640" ID="ID_1149767856" MODIFIED="1422951011105" TEXT="target">
+<node CREATED="1422951011106" ID="ID_1298654118" MODIFIED="1422951015280" TEXT="compose monads">
+<node CREATED="1422951015281" ID="ID_280484761" MODIFIED="1422951136207" TEXT="general program use monads in haskell">
+<node CREATED="1422951156651" ID="ID_1406086205" MODIFIED="1422951160565" TEXT="real examples"/>
+</node>
+</node>
+<node CREATED="1422951166914" ID="ID_82359367" MODIFIED="1422951184688" TEXT="prove delta modulallity">
+<node CREATED="1422951184689" ID="ID_878683239" MODIFIED="1422951207209" TEXT="Delta be able to notate all program modification"/>
+</node>
+</node>
+</node>
+<node CREATED="1422951467878" ID="ID_1815249376" MODIFIED="1422951469174" TEXT="kinds">
+<node CREATED="1422951469174" ID="ID_19945496" MODIFIED="1422951471615" TEXT="pair delta"/>
+<node CREATED="1422951471853" ID="ID_1802255885" MODIFIED="1422951477743" TEXT="infinite delta"/>
+<node CREATED="1422951477997" ID="ID_827291344" MODIFIED="1422951484720" TEXT="length fixed infinite delta"/>
+<node CREATED="1422951485011" ID="ID_1840511542" MODIFIED="1422951493414" TEXT="length fixed infinite delta with monad"/>
+</node>
+</node>
+</node>
+</map>