Mercurial > hg > Papers > 2015 > atton-thesis

annotate main.tex @ 9:324111203070

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add example used delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 07 Feb 2015 19:30:09 +0900
parents c4da3e667aad
children c2dda6eeab57
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \documentclass[a4j,12pt]{jreport}
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
2 \usepackage[dvipdfmx]{graphicx}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 \usepackage{mythesis}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 \usepackage{multirow}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 \usepackage{here}
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
6 \usepackage{listings, jlisting}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 \setlength{\itemsep}{-1zh}
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
8 \title{圏によるプログラムの変更の形式化}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 \icon{
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
10 \includegraphics[width=80mm,bb=0 0 595 842]{fig/ryukyu.pdf}
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
11 }
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
12 \year{平成26年度 卒業論文}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 \belongto{琉球大学工学部情報工学科}
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
14 \author{115763K 比嘉健太 \\ 指導教員 {河野真治} }
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
15
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
16
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 %%
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 %% プリアンブルに記述
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 %% Figure 環境中で Table 環境の見出しを表示・カウンタの操作に必要
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 %%
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 \makeatletter
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 \newcommand{\figcaption}[1]{\def\@captype{figure}\caption{#1}}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 \newcommand{\tblcaption}[1]{\def\@captype{table}\caption{#1}}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 \makeatother
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 \setlength\abovecaptionskip{0pt}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
27 %% listings settings
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
28
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
29 \lstset{%
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
30 frame=single,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
31 stringstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
32 commentstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
33 identifierstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
34 keywordstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
35 basicstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
36 breaklines=true,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
37 xleftmargin=0zw,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
38 xrightmargin=0zw,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
39 framerule=.2pt,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
40 columns=[l]{fullflexible},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
41 numbers=left,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
42 stepnumber=1,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
43 numberstyle={\scriptsize},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
44 numbersep=1em,
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
45 language={},
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
46 tabsize=4,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
47 lineskip=-0.5zw,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
48 morecomment={[s][]{/**}{*/}},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
49 }
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
50
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 \begin{document}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 % タイトル
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 \maketitle
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 \baselineskip 17pt plus 1pt minus 1pt
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 \pagenumbering{roman}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 \setcounter{page}{0}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
60 \tableofcontents % 目次
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
61 \listoffigures % 図目次
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
62 \listoftables % 表目次
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
64 \input{introduction}
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
65 \input{delta}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
3
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
67 \chapter{Categorical Definitions of Monad}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
68 \section{Category}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
69 \section{Functor}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
70 \section{Natural Transformation}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
71 \section{Monad}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
72 \section{Monads in Functional Programming}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
73
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
74 \chapter{Agda による証明手法}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
75 \section{Natural Deduction}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
76 \section{Curry-Howard Isomorphism}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
77 \section{Agda による証明}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
78 \section{Reasoning}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
79
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
80 \chapter{Delta が Monad である証明}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
81 \section{Agda における Functor 則}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
82 \section{Agda における Monad 則}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
83 \section{Delta が Functor 則を満たす証明}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
84 \section{Delta が Monad 則を満たす証明}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
85
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
86 \chapter{任意の Monad と Delta の組み合せ}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
87 \section{Monad と組み合せた Delta である DeltaM の定義}
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
88 \section{DeltaM が Monad 則を満たす証明}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
3
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
90 \chapter{結論}
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
91
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
92 % 今後の課題
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
93 \input{future.tex}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 % 参考文献
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 \input{bibliography.tex}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 % 謝辞
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 \input{thanks.tex}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 % 付録
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 %\input{appendix.tex}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 \end{document}