Mercurial > hg > Papers > 2015 > atton-thesis

annotate main.tex @ 48:422e96fda05a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wrote description monad-laws on delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 15 Feb 2015 12:35:58 +0900
parents d65a84d36eba
children ca389989b660
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}
36
2ff5acb0d2e9 Add escape script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
6 \usepackage{listings}
23
61e5659e04a9 Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
7 \usepackage{bussproofs}
28
c684abcc781b Add agda-resoning
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
8 \usepackage{amssymb}
36
2ff5acb0d2e9 Add escape script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
9 \usepackage[utf8]{inputenc}
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
10
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 \setlength{\itemsep}{-1zh}
40
470d99799398 Add description functor record
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
12 \title{プログラムの変更の圏による形式化}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 \icon{
20
beebe0ffbcad Fix figures
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
14 \includegraphics[width=80mm,bb=0 0 595 642]{fig/ryukyu.pdf}
4
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 \year{平成26年度 卒業論文}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 \belongto{琉球大学工学部情報工学科}
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
18 \author{115763K 比嘉健太 \\ 指導教員 {河野真治} }
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
19
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
20
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 %%
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 %% プリアンブルに記述
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 %% Figure 環境中で Table 環境の見出しを表示・カウンタの操作に必要
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 %%
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 \makeatletter
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 \newcommand{\figcaption}[1]{\def\@captype{figure}\caption{#1}}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 \newcommand{\tblcaption}[1]{\def\@captype{table}\caption{#1}}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 \makeatother
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 \setlength\abovecaptionskip{0pt}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
31 %% listings settings
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
32
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
33 \lstset{
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
34 frame=single,
26
de3397af1f8d Temporary save
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
35 keepspaces=true,
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
36 stringstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
37 commentstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
38 identifierstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
39 keywordstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
40 basicstyle={\ttfamily},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
41 breaklines=true,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
42 xleftmargin=0zw,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
43 xrightmargin=0zw,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
44 framerule=.2pt,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
45 columns=[l]{fullflexible},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
46 numbers=left,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
47 stepnumber=1,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
48 numberstyle={\scriptsize},
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
49 numbersep=1em,
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
50 language={},
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
51 tabsize=4,
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
52 lineskip=-0.5zw,
36
2ff5acb0d2e9 Add escape script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
53 escapechar={@},
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
54 }
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
55 \def\lstlistingname{リスト}
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
56 \def\lstlistlistingname{リスト目次}
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
57
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
58
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 \begin{document}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 % タイトル
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 \maketitle
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 \baselineskip 17pt plus 1pt minus 1pt
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 \pagenumbering{roman}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 \setcounter{page}{0}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
68 \tableofcontents % 目次
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
69 \listoffigures % 図目次
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
70 \listoftables % 表目次
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
71 \lstlistoflistings % ソースコード目次
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
72
46
1b688e70f2a8 Move proofs to appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
73 % 本文
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
74 \input{introduction}
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
75 \pagenumbering{arabic}
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
76 \input{delta}
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
77 \input{category}
33
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
78 \input{functional_programming}
23
61e5659e04a9 Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
79 \input{agda}
47
d65a84d36eba Fix appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
80 \input{proof_delta}
46
1b688e70f2a8 Move proofs to appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
81 \input{delta_with_monad.tex}
3
4cac648eb36e Add table of contents v1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
82
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83
4
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
84 % 今後の課題
cc74def322a8 Add introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
85 \input{future.tex}
2
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 % 参考文献
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 \input{bibliography.tex}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 % 謝辞
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 \input{thanks.tex}
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
1e28ac702c1e Add template
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 % 付録
47
d65a84d36eba Fix appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
94 \appendix
d65a84d36eba Fix appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
95 % \input{proof_deltaM}
d65a84d36eba Fix appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
96 % TODO: 実験環境
d65a84d36eba Fix appendix
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
97 % TODO: Delta と DeltaM の本体
2
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 \end{document}