# HG changeset patch # User Yasutaka Higa # Date 1418300137 -32400 # Node ID b19932e572b77e17f2e4906e7c534081fabed5b4 # Parent 6145fed6a470c7bcc150f06eb6e5d4c2909b12b1 Rewriting position paper ... diff -r 6145fed6a470 -r b19932e572b7 mindmap.mm --- a/mindmap.mm Thu Dec 11 18:41:17 2014 +0900 +++ b/mindmap.mm Thu Dec 11 21:15:37 2014 +0900 @@ -1,7 +1,7 @@ - + @@ -61,7 +61,7 @@ - + @@ -92,7 +92,7 @@ - + @@ -172,7 +172,7 @@ - + @@ -200,7 +200,7 @@ - + @@ -300,5 +300,85 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 6145fed6a470 -r b19932e572b7 sigse.pdf Binary file sigse.pdf has changed diff -r 6145fed6a470 -r b19932e572b7 sigse.tex --- a/sigse.tex Thu Dec 11 18:41:17 2014 +0900 +++ b/sigse.tex Thu Dec 11 21:15:37 2014 +0900 @@ -27,27 +27,12 @@ %\checklines % 行送りを確認する時に使用 \begin{document}%{ % 和文表題 -\title{卒業研究を通して形式手法を学んで} -% 英文表題 -\etitle{} +\title{形式手法を学び始めて思うことと，形式手法を広めるには} % 所属ラベルの定義 \affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.} % 和文著者名 \author{比嘉健太\affiref{ie-ryukyu} \and 河野真治\affiref{ie-ryukyu}} -% 英文著者名 -\eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and - Shinji Kono\affiref{ie-ryukyu}} - -% 和文概要 -\begin{abstract} -卒業研究において形式手法を用いて問題を形式化した． -この一年間でどのようなことを行なったか，どう感じたか述べる． -\end{abstract} -% 英文概要 -\begin{eabstract} - -\end{eabstract} % 表題などの出力 \maketitle @@ -55,71 +40,68 @@ %}{ % 本文はここから始まる -\section{自己紹介} -私は琉球大学工学部情報工学科に所属する四年次の学生だ． -自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマに取り組んでいる． -卒業研究において形式手法を用いて形式化することとなったのでその経緯と感想を述べたい． +\section{現在行なっている研究} +プログラムの信頼性の向上は自動で行なわれるべきだと思っています． +形式化された範囲で作成されたプログラムは，人による性質の記述無しに高い信頼性を持つのが理想だと考えています． -\section{卒業研究と型とAgda} -私の初期の研究テーマはプログラムから自動でバグを指摘する機構を作ることであった． +現在私はプログラムの変更を形式化する研究を行なっています． +研究目的はプログラムの変更を形式化することによりプログラムの変更時に完成に近づいているかを判断することです． +現在は特定の二点間での信頼性に注目し，2つのバージョン間でのトレースの相違を指摘しようとしています． + +私の研究においてプログラムの変更は Monad として表現します． +Monad とは，圏においては Monad 則を満たす自然変換 $ \mu $ と $ \eta $ と Functor T です． +Monad 則を満たすような $ \mu $ と $ \eta $ と Functor T として，プログラムの変更を表します． -研究を進めるにつれ，プログラムのバグを見付けるには仕様やテストを記述する必要があることを知った． -テストを記述するコストはおそらくプログラムを書くコストと同じかそれ以上かかる． -あくまで私はプログラムのみでバグを見付けたかった． -そのために，プログラムの変更に着目することによりバグを見付ける手法を提案することとなった． +例題の記述にはプログラミング言語 Haskell を使用しています． +まず，プログラムの変更を表すようなデータ構造 Delta を定義します． +Delta は過去のバージョンの値を持ち，バージョンが上がるたびに値を増やすようにします． +プログラムが変更されても過去の値を持ち続けることにより，プログラムの変更を表す試みです． +Delta は複数のバージョンの値を持っているため，計算の時にどのバージョンの値と処理の対応を判断しなくてはなりません． +バージョンの判断に Monad を使いました． +Haskell における Monad はデータ構造とメタな計算との対応付けです． +Delta と Delta に対する関数は，互いにどのようなバージョンを持っていても一意になるよう， $ \mu $ と $ \eta $ を定義しました． +一意になることの確認には Monad 則を満たすことにより確認できます． +Monad 則を満たす証明のためには証明支援系言語 Agda を用いました． -そこで問題となったのがプログラムの変更の表現だった． -この問題に対し，指導教員からプログラムに対する変更を Monad によって形式化するアイデアを頂いた． - -Monad はプログラミング言語 Haskell では型クラスとして用意されており，型とは何かを知る必要があった． -そこで，Proofs and Types を指導教員と読むこととなった． -Proofs and Types では型と論理の対応について知ることができた． -特に自然演繹は直感的に理解でき，対応する型は私の関心の対象となった． -直感的に理解できたのは型を持つプログラミング言語を記述したことがあるのも大きい． +現在進んでいるのはここまでで，これから二点のトレースの比較をしようと思っています． -Proofs and Types の例題は証明支援系言語 Agda によって記述した． -Agda では項の定義とその書き換えによる等式変形を意識することとなった． -Agda における証明は依存型で記述される． -依存型を記述する言語の経験は無く，慣れるまでに時間が必要だった． -あくまで等式の変形であることに気付くまでは依存型の趣旨が全く理解できなかった． +\section{Agdaを学んだ流れとつまづき} +形式化や Agda は三年次向けの講義で知りました． +もともと形式手法を知らず，バグを自動で検出したかった私には関心の高い講義でした． +その講義では Curry-Howard 対応や Agda における証明を行ないました． -型の理論背景を知った後，次に Monad とは一体何か知る必要があった． -Monad は圏論を元に計算機科学へ提案された表現であり，圏論を学ぶこととなった． -Monad の理解に必要な圏や関手，自然変換などを学んだが，その解釈にも私は型を用いた． -特に， Monad には満たすべき Monad 則が存在するが，依存型で表現してしまえば私にとって型に見えた． +型や自然演繹は直感的に理解できました． +型の変換は値の変換に応じて型が変わるため，関数によって値を変えることだと思えたからです． +自然演繹もルールが数個しかなく，理解するのにそれほど時間はかかりませんでした． +しかし，Agda による証明記述はすぐには理解できませんでした． +依存型を持つAgda では，証明は型で記述されます． +証明を満たす型を持つ値，というのが直感的に理解できませんでした． -型の理論背景と Monad を学んだ私は当初のアイデアであるプログラムに対する変更を Monad で表現することにした． -Monad という指針が存在したため，プログラムの変更を Monad として定義することができた． -特に，具体的にどのような則を満たすような型を定義すると良いか，という指針を得られたのは大きい． - -\section{卒業研究を通して形式手法に思うこと} -形式手法に関して，私の卒業研究を通して得た知見は2つある． +Agda の特徴を取らえられたのは System T や Sytem F を Agda で記述していた時です． +四年次になり研究室に配属された私は，プログラムのバグを自動で検出したいと希望しました． +そこで，Proofs and Types\cite{proofs-and-types} を読むことになりました． +Proofs and Types ではもう一度 Curry-Howard 対応や自然演繹，それに加えて System T や System F などを学びました． +System T における自然数の加法の結合法則を証明を記述している時，等式変形に加法の交換法則を用いました． +この時に，規則とそれから導出される証明も規則であり，それらによる等式を変形で証明を記述しているのだと理解しました． +理解するまでには Agda で証明を書き続ける必要がありました． -まず1つめは形式手法を直接用いるためには専門家が必須なことである． -形式手法の提案とどのように形式化するかを指摘するには必須な知識が多く存在する． -例えば，今回の指導教員が行なった指摘には論理や圏論やプログラングなどに造形が深い必要がある． -正直に言ってしまえば，指導教員の指摘が無ければ形式手法を用いる発想は出なかったであろう． - -2つめは，システムとして確立されているのなら利用しやすかったことである． -型の理論的背景を理解せずとも，これまでにプログラムを書いた経験から型システムは問題無く利用できた． -これはプログラムを書いた経験に基づくように思われる． - +また，Agda の agda-mode で実行するたびに必要な証明が指摘されているのを見た時，対話的に実行することのメリットを感じました． +この証明を変形するにはどの証明が必要か，などと何度も試せるからです． +試していくうちに必要な他の証明が見えてきます． +他の証明が必須だと思った時に新な証明を記述していくようにしました． +こうすることにより，証明すべき大きな式は見失わずに必要な小さな式に分割することができます． +対話的に実行することで問題の変換や詳細化や分割などが行なえるため対話的実行は有用だと思っています． \section{形式手法を広めるには} -形式手法を用いるには多くの知識が必須である． -よって，前提知識を減らしたシステムとしてより手軽に利用する方が良いと考える． - -例えば，Agdaでは証明はほぼ自ら記述するが，プログラムから証明が自動で導出できれば手軽に利用できる． -型のように推論が可能であれば既存のプログラムにも適用しやすい． -まずは制約が弱くとも導入しやすいシステムとして提供し，必要に応じて制約を強くするような手法はどうだろうか． +形式手法を広めるには対話的な手法を導入するのが良いと思っています． +私は Agda を書き続けることで依存型に対する理解を得られましたが，書き続けるには時間が必要にです． +理解できている部分だけ実行しつつ，理解できない部分はどうするべきか対話的に聞くことで必要な情報を速く得ます． +必要になった部分だけ学習することで，実行したい部分に対して必要十分な理解が得られると思います． +このことにより，形式手法を学習する時間は必要な部分だけに納まり，より試しやすいものになると思います． -\section{まとめ} -私は卒業研究において形式手法を用いて問題を形式化した． -その際に必須な知識は多く，形式化よりもその知識の修得に時間がかかってしまった． -しかし，形式化する中で満たすべき条件が明確化されているのは処理を考える指針となった． - -また，型に対する理論的背景が無くとも型システムは直感的に理解できた． -導入が手軽なシステムとして普及させ，その後から強力な手法を適用するために制約を加えていくことで普及拡大を目指すのはどうだろうか． +また，必要な分だけを実行するのは形式手法の学習コスト以外にもメリットがあると思います． +必要な分だけを検証することにより，過剰な検証コストを防ぐことができます． +検証の範囲と必要な条件が対話的に得られるのであれば，適切なコストで検証を行なうこともできると思います． %}