Mercurial > hg > Papers > 2015 > atton-sigse

comparison sigse.tex @ 45:bfc3fc56ad90

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mini fixes from kngw-san, masa-san
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 25 Dec 2014 17:17:57 +0900
parents 9d0c57803ca0
children a6bc47128bd4
comparison
equal deleted inserted replaced
44:9d0c57803ca0 45:bfc3fc56ad90
36 % 英文著者名 36 % 英文著者名
37 \eauthor{Yasutaka Higa\affiref{ie-ryukyu} \and 37 \eauthor{Yasutaka Higa\affiref{ie-ryukyu} \and
38 Shinji Kono\affiref{ie-ryukyu}} 38 Shinji Kono\affiref{ie-ryukyu}}
39 39
40 \begin{abstract} 40 \begin{abstract}
41 大学の講義や卒業研究を通して形式手法を学んだ一年ほどの過程やつまづき，それらに基づいた形式手法を広めるための意見を述べます． 41 大学の講義や卒業研究を通して一年ほど形式手法を学んだ過程やつまづき，それらに基づいた形式手法を広めるための意見を述べます．
42 \end{abstract} 42 \end{abstract}
43 43
44 % 表題などの出力 44 % 表題などの出力
45 \maketitle 45 \maketitle
46 46
50 \section{現在行なっている研究} 50 \section{現在行なっている研究}
51 プログラムの信頼性の向上は自動で行なわれるべきだと思っています． 51 プログラムの信頼性の向上は自動で行なわれるべきだと思っています．
52 形式化された範囲で作成されたプログラムは，プログラムのみで高い信頼性を持つのが理想だと考えています． 52 形式化された範囲で作成されたプログラムは，プログラムのみで高い信頼性を持つのが理想だと考えています．
53 53
54 現在私はプログラムの変更を形式化する研究を行なっています． 54 現在私はプログラムの変更を形式化する研究を行なっています．
55 形式化された変更によりプログラムを変更する際，プログラムが完成に近づいているか判断することが目的です． 55 形式化された変更によりプログラムを変更する際，プログラムが完成に近づいているかどうか判断することが目的です．
56 現在は特定の二点間での信頼性に注目し，2つのバージョン間でのトレースの相違を指摘しようとしています． 56 現在は特定の二点間での信頼性に注目し，2つのバージョン間でのトレースの相違を指摘しようと考えています．
57 57
58 私の研究においてプログラムの変更は Monad として表現します． 58 私の研究においてプログラムの変更は Monad を用いて表現します．
59 Monad とは，圏においては Monad 則を満たす自然変換 $ \mu $ と $ \eta $ と Functor T です\cite{category}． 59 Monad とは，圏においては Monad 則を満たす自然変換 $ \mu $ と $ \eta $ と Functor T です\cite{category}．
60 Monad 則を満たすような $ \mu $ と $ \eta $ と Functor T として，プログラムの変更を表します． 60 つまり，ある法則を満たす3つの要素として，プログラムの変更を表します．
61 61
62 例題の記述にはプログラミング言語 Haskell を使用しています． 62 例題の記述にはプログラミング言語 Haskell を使用しています．
63 まず，プログラムの変更を表すようなデータ構造 Delta を定義します． 63 まず，プログラムの変更を表すようなデータ構造 Delta を定義します．
64 Delta は全ての変更時点のプログラムの値を保持します． 64 Delta は全ての変更時点のプログラムの値を保持します．
65 プログラムが変更されても変更前の値を持ち続けることにより，プログラムの変更を表す試みです． 65 プログラムが変更されても変更前の値を持ち続けることにより，プログラムの変更を表す試みです．
66 66
67 Delta を用いたプログラムでは，変数は必ず Delta で記述し，関数は必ず Delta を返すようにします． 67 Delta を用いたプログラムでは，変数は必ず Delta で記述し，関数は必ず Delta を返すようにします．
68 プログラムへの変更は，関数か変数のバージョンアップとして表現し，Delta への新しい値の追加として記述します． 68 プログラムへの変更は，関数か変数のバージョンアップとして表現し，Delta への新しい値の追加として記述します．
69 そうすることにより，任意の変数もしくは関数は必ず1つ以上のバージョンを持ちます． 69 その結果，任意の変数もしくは関数は必ず1つ以上のバージョンを持ちます．
70 70
71 次にバージョンを持った関数の適用を考えます． 71 次にバージョンを持った関数の適用を考えます．
72 関数の適用は変数と関数のバージョンの違いを考慮したルールに基づいて適用しなくてはなりません． 72 関数の適用は変数と関数のバージョンの違いを考慮したルールに基づいて適用しなくてはなりません．
73 例えば，バージョンが1つある変数に対してバージョンが3つある関数と2つある関数を適用する場合，結果の変数のバージョンがいくつになるか決めなくては適用することができません(図\ref{apply_function})． 73 例えば，バージョン数が1つの変数に対してバージョン数が3つの関数と2つの関数を適用する場合，結果の変数のバージョン数を決めなくては適用することができません(図\ref{apply_function})．
74 74
75 \begin{figure}[htbp] 75 \begin{figure}[htbp]
76 \begin{center} 76 \begin{center}
77 \includegraphics[scale=0.4]{./figure/apply_function.pdf} 77 \includegraphics[scale=0.4]{./figure/apply_function.pdf}
78 \caption{関数適用時のバージョンの組み合せ例} 78 \caption{関数適用時のバージョンの組み合せ例}
82 82
83 83
84 変数と関数のバージョンの組み合せのルールは Monad を用いて記述しました． 84 変数と関数のバージョンの組み合せのルールは Monad を用いて記述しました．
85 Haskell における Monad はデータ構造とメタな計算との対応付けです\cite{moggi}． 85 Haskell における Monad はデータ構造とメタな計算との対応付けです\cite{moggi}．
86 メタ計算としてバージョンの組み合せの解決を $ \mu $ と $ \eta $ により定義します． 86 メタ計算としてバージョンの組み合せの解決を $ \mu $ と $ \eta $ により定義します．
87 関数を適用する際に必ず $ \mu $ と $ \eta $ を用いて適用することにより，関数や値の変更時にバージョンの組み合せは気にする必要が無くなります． 87 関数を適用する際に必ず $ \mu $ と $ \eta $ を用いて適用することにより，関数や値の変更時にバージョンの組み合せを考える必要が無くなります．
88 メタ計算としてバージョンの組み合せを分離することで，任意の関数や変数に対し変更を行なっても変更後のプログラムが実行できます． 88 メタ計算としてバージョンの組み合せを分離することで，任意の関数や変数に対し変更を行なっても変更後のプログラムが実行できます．
89 89
90 また，バージョンの組み合せの解決はプログラム全体で一意でなくてはなりません． 90 また，バージョンの組み合せの解決はプログラム全体に対して一意でなくてはなりません．
91 一意で無い場合，特定の箇所のみを変更することでプログラム全体のバージョンの組み合せが変わってしまいます． 91 一意で無い場合，特定の箇所のみを変更することでプログラム全体のバージョンの組み合せが変わってしまいます．
92 プログラム全体における組み合せが一意になることの確認は Monad 則を満たすことにより行なえます． 92 プログラム全体における組み合せが一意であることは Monad 則を満たすことで確認できます．
93 定義した $ \mu $ と $ \eta $ が Monad 則を満たすことは証明支援系言語 Agda\cite{agda} によって証明しました． 93 定義した $ \mu $ と $ \eta $ が Monad 則を満たすことは証明支援系言語 Agda\cite{agda} によって証明しました．
94 94
95 現在行なったのはDelta に対する Monad 則の証明までです． 95 現在行なったのはDelta に対する Monad 則の証明までです．
96 これからプログラムのトレースの取得と，2つのプログラムのトレースの比較をしようと思っています． 96 これからプログラムのトレースの取得と，2つのプログラムのトレースの比較をしようと思っています．
97 97
113 Agda の特徴を取らえられたのは System T や Sytem F を Agda で記述していた時です． 113 Agda の特徴を取らえられたのは System T や Sytem F を Agda で記述していた時です．
114 114
115 Agda における証明の記述は Emacs の agda-mode で行なわれます． 115 Agda における証明の記述は Emacs の agda-mode で行なわれます．
116 証明を記述し，その証明が成り立っているか何度も対話的に繰り返します． 116 証明を記述し，その証明が成り立っているか何度も対話的に繰り返します．
117 また，等式を変形していく際に前後の文脈からどのような規則により変換されるのか提示することもできます． 117 また，等式を変形していく際に前後の文脈からどのような規則により変換されるのか提示することもできます．
118 System T における自然数の加法の結合法則が上手く記述できなかった私は，1つの等式を思い付く限り変形していました． 118 Agda の理解が深まったと思えたのは，System T における自然数の加法の結合法則を記述した時です．
119 結合法則を上手く記述できなかった私は，1つの等式を思い付く限り変形していました．
119 変形を繰り返していくうち，加法の交換法則によって変形が可能だと提示されました． 120 変形を繰り返していくうち，加法の交換法則によって変形が可能だと提示されました．
120 その時，Agda による証明が理解できたように思えました． 121 その時，Agda による証明が理解できたように思えました．
121 規則とそれから導出される証明も規則であり，それらによって等式を変形することで証明を記述しているのだと理解しました． 122 規則とそれから導出される証明も規則であり，それらによって等式を変形することで証明を記述しているのだと理解しました．
122 123
123 何度も等式の変形を試すことによって Agda を理解した私は，高速に何度も試行することが重要だと思っています． 124 何度も等式の変形を試すことによって Agda を理解した私は，高速に何度も試行することが重要だと思っています．
128 このように，問題の変換や詳細の把握，問題の分割などが行なえるため対話的実行は有用だと思っています． 129 このように，問題の変換や詳細の把握，問題の分割などが行なえるため対話的実行は有用だと思っています．
129 130
130 \section{形式手法を広めるには} 131 \section{形式手法を広めるには}
131 形式手法を広めるには，手軽に何度も試行可能にするのが重要だと思っています． 132 形式手法を広めるには，手軽に何度も試行可能にするのが重要だと思っています．
132 手軽に何度も試行することができれば，形式手法の学習にも役立ちます． 133 手軽に何度も試行することができれば，形式手法の学習にも役立ちます．
133 理解できない部分を問い，どうするべきか対話的に答えることで，学習者は解決に必要な情報を得られます． 134 学習者は理解できない部分を問い，対話的な答えから解決に必要な情報を得ます．
134 必要になった部分のみ学習することで，学習コストを最小限に抑えることができると思われます． 135 必要になった部分のみ学習することで，学習コストを最小限に抑えることができると思われます．
135 また，必要な分だけを実行するのは学習コストの面以外にもメリットがあると思います． 136 また，必要な分だけを実行するのは学習コストの面以外にもメリットがあると思います．
136 例えば，検証の実行コストがあります． 137 例えば，検証の実行コストがあります．
137 検証する範囲の指定とコストを対話的に何度も提示できるのなら，払うコストに対して最大の効果が得られる範囲を探れます． 138 検証する範囲の指定とコストを対話的に何度も提示可能なら，払うコストに対して最大の効果が得られる範囲を探ることができます．
138 企業のようにコストや利益の見積りを考えた上で製品を開発しなくてはならない場合，どのようなコストに対してどのような効果が得られるか判断可能であれば，形式手法の導入の検討もしやすいのではないかと思えます． 139 企業のようにコストや利益の見積りを考えた上で製品を開発しなくてはならない場合，コスト対効果が明確であることは検討の際の指針になると思えます．
139 さらに，必要以上に検証することを見積りの段階で防げるのなら，コストを最小化することも可能に思えます． 140 さらに，検証範囲を対話的に指定できれば，必要以上の検証や不必要な部分の洗い出しも可能かもしれません．
140 よって形式手法を広めるには，手軽に何度も試行可能であり，必要なコストや必要な情報を提示可能であることが重要だと思います． 141 よって形式手法を広めるには，手軽に何度も試行可能であり，必要なコストや必要な情報を提示可能であることが重要だと思います．
141 142
142 %} 143 %}
143 144
144 \begin{thebibliography}{10} 145 \begin{thebibliography}{10}