Mercurial > hg > Papers > 2015 > atton-sigse

--- a/sigse.tex	Tue Dec 09 11:42:50 2014 +0900
+++ b/sigse.tex	Tue Dec 09 12:11:27 2014 +0900
@@ -94,9 +94,10 @@
 その際、前のバージョンの組み合せを保存しつつ新たな変更も取り入れるように組み合せる必要がある。
 バージョンの組み合せを表現するために Delta を Monad とする。

-Monad とはデータ構造とメタ計算を対応付ける手法である。(TODO: ref moggi?)
+Monad とはデータ構造とメタ計算を対応付ける手法である\cite{moggi}。
 ここでのメタ計算とはバージョン間の組み合せを一意に決めるルールである。
 関数の実行時にメタ計算も含めて実行することにより、異なるバージョンに存在するの独立した計算も全て実行することができる。
+なお、データ構造を Monad として定義する際に満たすべき Monad則が存在するが、Monad則を満たしていることは証明支援系言語Agda\cite{agda}によって証明した。
 TODO: ルールを得るサンプルを書くかな? or Delta の定義

 よって、プログラムをデータ構造 Delta とDelta を返す関数として記述することにより、全てのバージョンを同時に実行できるプログラムが得られる。
@@ -126,7 +127,7 @@
 可能なプログラムの全ての変更を Delta によって表現可能かどうか調べなくてはならない。
 この課題については Delta と他の Monad との組み合せが可能であれば可能であると考えている。
 今回 Delta を実装した Haskell においては入出力の処理が Monad として表現される。
-そのため、入出力を含めた変更は Monad に
+そのため、入出力を含めた変更は Monad との組み合せが必要になる。

 2 つめはDelta におけるそれぞれのバージョンのトレースを得ることである。
 異なるバージョンにおいて実行結果が変化する点を指摘するには実行結果が比較可能でなくてはいけない。
@@ -135,926 +136,24 @@
 トレースを得る Monad を定義し、そのMonadと Delta との組み合せで各バージョンのトレースを得る。

 3 つめは Delta を圏として表現することとその解析である。
-Monad は Kleisli圏の Kleisli Triple との対応が存在しており(TODO: ref higher order?)、Deltaもある圏を構築すると考えている。
+Monad は Kleisli圏の Kleisli Triple との対応が存在しており\cite{category}、Deltaもある圏を構築すると考えている。
 特に、 Parallel Debugger は圏における Product と対応すると考えている。
-圏における他の性質から、プログラムの変更の性質の解析や他の手法を提案しようと考えている。
-
-
-%}{
-
-\section{投稿から出版まで}\label{sec:Enum}\label{sec:item}
-
-投稿する論文の作成から，論文が掲載された論文誌が出版されるまでの流れは，以下
-の通りである\footnote[2]{%
-%
-ジャーナルの手順に沿った説明となっており，トランザクションでは個々に固有の異
-なる手順が定められていることがある．詳細については各トランザクション編集委員
-会に照会されたい．}
-．
-%
-\begin{Enumerate}%{
-\item {\bf スタイルファイルの取得}\\
-情報処理学会のWEB site \|http://www.ipsj.or.jp/|から，スタイルファイルなど
-からなる論文作成キットをダウンロードすることができる．このキットには以下のファ
-イルが含まれている\footnote[3]{%
-%
-下記のほかに非日本語環境でのBib{\TeX}スタイルとして，\texttt{ipsjsort-e.bst}
-と\texttt{ipsjunsrt-e.bst}も含まれている．}．
-%
-\begin{itemize}%{
-\item\|ipsjpapers.sty| : 製版用スタイル
-\item\|ipsjpapers.cls| : {\LATEXe} 用製版用スタイル
-\item\|ipsjdrafts.sty| : 投稿用スタイル
-\item\|ipsjcommon.sty| : 製版／投稿用補助スタイル
-\item\|ipsjsort.bst  | : jBib{\TeX}スタイル（著者名順）
-\item\|ipsjunsrt.bst | : jBib{\TeX}スタイル（出現順）
-\item\|sample.tex    | : このガイドのソース（製版用）
-\item\|dsample.tex   | : このガイドのソース（投稿用）
-\item\|esample.tex   | : 英文ガイドのソース（製版用）
-\item\|desample.tex  | : 英文ガイドのソース（投稿用）
-\item\|bibsample.bib | : 文献リストのサンプル
-\item\|ebibsample.bib| : 英文文献リストのサンプル
-\end{itemize}%}
-%
-キットは Unix 用，Windows (DOS) 用，Macintosh 用などが用意されており，著者の
-作業環境に応じたものを選択できるようになっている．
-
-\item {\bf 投稿用原稿の作成と投稿}\\
-このガイドにしたがって，後述の \|draft| オプションを指定した {\LaTeX} ソース
-を作成し，その \|.dvi| ファイルをPDFファイルに変換する．
-なお著者の氏名・所属，著者紹介，謝辞は投稿用原稿に含まれていてはならないが，
-後述するコマンド等を用いて指定していれば自動的に出力が抑止される．
-PDFファイルを投稿するにはまず，
-\begin{itemize}\item[]\tt
-http://www.ipsj.or.jp/08editt/\\\phantom{http://}journal/submit/
-\end{itemize}
-にアクセスして投稿情報を登録し，その結果送られてくるemailに記載のURLをアクセ
-スする．
-
-\item {\bf 製版用原稿の作成}\\
-採録が決定したら，査読者からのコメントなどにしたがって原稿を修正し，著者紹介
-など投稿時になかった項目があれば追加する．また図表などのレイアウトも最終的な
-ものとする．なお後の校正の手間を最小にするために，{\bf この段階で記述の誤り
-などを完全に除去するように綿密なチェックをお願いしたい}．
-
-\item {\bf 製版用原稿とファイルの送付}\\
-学会へは {\bf {\LaTeX} ファイル（をまとめたもの）とハードコピーの双方を}送付
-する．送付するファイル群の標準的な構成は \|.tex| と \|.bbl| であり，この他に
-PostScript ファイルや特別なスタイルファイルがあれば付加する．なお \|.tex| は
-印刷業者が修正することがあるので，{\bf 必ず一つのファイルにしていただきたい}．
-また必要なファイルが全てそろっていること，特に特別なスタイルファイルに洩れが
-ないことを，注意深く確認して頂きたい．
-
-ファイルの送付方法などについては，採録通知とともに学会事務局から送られる指示
-にしたがっていただきたい．
-
-\item {\bf 著者校正}\\
-学会では用語や用字を一定の基準にしたがって修正することがあり，また {\LaTeX}
-の実行環境の差異などによって著者が作成したハードコピーと実際の製版結果が微妙
-に異なることがある．これらの修正や差異が問題ないかを最終的に確認するために，
-著者にゲラ刷りが送られるので，もし問題があれば朱書によって指摘して返送する．
-なお{\bf この段階での記述誤りの修正は原則として認められない}ので，原稿送付時
-に細心の注意を払っていただきたい．
-
-\item {\bf 製版・出版}\\
-著者の校正に基づき最終的な製版を行ない，オンライン出版する．
-\end{Enumerate}%}
-
-%}{
-
-\section{{\protect\LATex}の実行環境}\label{sec:ITEM}
-
-スタイルファイルはNTTの斉藤康己氏による j{\TeX}（いわゆるNTT版）と，アスキー
-社による日本語 {\TeX}（いわゆるアスキー版）のどちらにも対応しているので，著者
-の {\LaTeX} 環境に関わらず同じスタイルファイルを使用できる\footnote{%
-%
-英文論文であればオリジナルの（すなわち非日本語の）{\LaTeX}を使用することもで
-きる．}．
-
-NTT版およびアスキー版の{\LATEXe}について，以下のバージョンでの動作確認を行なっ
-ている．
-%
-\begin{ITEMIZE}%{
-\item
-NTT版${}={}${j\TeX} 1.6${}+{}$%
-    {\LATEXe} 1994/12/01 patch level 3
-\item
-アスキー版${}={}${p\TeX} 3.141592 p3.1.4${}+{}$%
-    {p\LATEXe} 2004/08/10
-\end{ITEMIZE}%}
-%
-いずれについても，ネイティブ・モードと{\LaTeX} 2.09 互換モードのどちらでも使
-用することができる．また{\LaTeX} 2.09については，以下のバージョンでの動作確
-認を行っている．
-%
-\begin{ITEMIZE}%{
-\item
-NTT版${}={}${j\TeX} 1.52${}+{}${\LaTeX} 2.09
-\item
-アスキー版${}={}${\TeX} 2.99-j1.7${}+{}${\LaTeX} 2.09
-\end{ITEMIZE}%}
-%
-なお上記以前の版についても動作すると期待できるが，できれば新しい版を使って頂
-きたい．
-
-%}{
-
-\section{スタイルファイルの使い方}
-\subsection{一般的な注意事項}
-
-会議の予稿集などとは違い，論文誌の体裁には伝統的かつ「堅い」約束事が数多くあ
-る．そのためスタイルファイルも「堅い」ものとなっており，{\LaTeX} の特徴の一
-つであるカスタマイズ機能は大幅に制限される．例えば \|\textheight| などのいわ
-ゆる style parameter を変更するのは当然やめていただきたい．どのようなカスタ
-マイズが許されるのかを示すのは難しいが，一つの基準として「スタイルファイルを
-読んでみて大丈夫だと確信が持てる」こと以外はしないことを強く勧める．
-
-なお，これらの変更やこのガイドで述べている「やめて欲しいこと」を行なっても，
-{\bf エラーになったりせず単に結果が変になる}ことに注意していただきたい．
-
-%}{
-
-\subsection{論文の構成}\label{sec:config}
-
-ファイルは次の形式で作る．なお下線部は投稿時にはなくてもよい．またトランザク
-ション特有のコマンドなどについては，付録\ref{sec:app-sig}を参照されたい．
-%
-\begin{Quote}\small*
-\|\documentclass{ipsjpapers}|\footnote{%
-    {\LATExe} を2.09互換モードで使う場合，および{\LaTeX} 2.09を使う場合
-    には \CS{documentstyle} を使用し，必要に応じてオプション引数に補助ス
-    タイル名を加える．} または\\
-\|\documentclass[draft]{ipsjpapers}|\footnotemark[1]\\
-必要ならばオプションのスタイルを指定する．\\
-必要ならば補助スタイルを \|\usepackage| で指定する．\\
-\Underline{\|\setcounter{|{\bf 巻数}\|}{|\<巻数\>\|}|}\\
-\Underline{\|\setcounter{|{\bf 号数}\|}{|\<号数\>\|}|}\\
-\Underline{\|\setcounter{volpageoffset}{|\<先頭ページ\>\|}|}\\
-\Underline{\|\|{\bf 受付}\|{|\<年\>\|}{|\<月\>\|}{|\<日\>\|}|}\\
-\Underline{\|\|{\bf 採録}\|{|\<年\>\|}{|\<月\>\|}{|\<日\>\|}|}\\
-必要ならばユーザのマクロ定義などをここに書く．\\
-\|\begin{document}|\\
-\|\title{|\<表題（和文）\>\|}|\\
-\|\etitle{|\<表題（英文）\>\|}|\\
-\Underline{\|\affilabel{|\<所属ラベル\>\|}%|}\\
-\Underline{\mbox{}\qquad\qquad\|{|\<和文所属\>\|\\|\<英文所属\>\|}|}\\
-\Underline{\mbox{}\qquad\qquad\ldots\ldots\ldots}\\
-必要ならば \|\paffilabel| により現在の所属を宣言する．\\
-\Underline{\|\author{|\<第一著者（和文）\>\|\and|}\\
-\Underline{\leavevmode\phantom{\tt @author@}\<第二著者（和文）\>\|\and|}\\
-\Underline{\leavevmode\phantom{\tt @author@} \ldots{} \|}|}\\
-\Underline{\|\eauthor{|\<第一著者（英文）\>\|\and|}\\
-\Underline{\leavevmode\phantom{\tt @eauthor@}\<第二著者（英文）\>\|\and|}\\
-\Underline{\leavevmode\phantom{\tt @eauthor@} \ldots{} \|}|}\\
-\|\begin{abstract}|\\
-\mbox{}\quad\<概要（和文）\>\\
-\|\end{abstract}|\\
-\|\begin{eabstract}|\\
-\mbox{}\quad\<概要（英文）\>\\
-\|\end{eabstract}|\\
-\|\maketitle|\\
-\|\section{|\<第1節の表題\>\|}|\\
-\mbox{}\quad $\ldots\ldots\ldots$\\
-\mbox{}\quad\<本文\>\\
-\mbox{}\quad $\ldots\ldots\ldots$\\
-謝辞があれば \|acknowledgment| 環境を使ってここに記す．\\
-\|\bibliographystyle{ipsjunsrt}| または\\
-\|\bibliographystyle{ipsjsort}|\\
-\|\bibliography{|\<文献データベース\>\|}|\\
-付録があれば \|\appendix| に続いてここに記す．\\
-\Underline{\|\begin{biography}|}\\
-\Underline{\mbox{}\quad\<著者紹介\>}\\
-\Underline{\mbox\qquad$\ldots\ldots\ldots$}\\
-\Underline{\|\end{biography}|}\\
-\|\end{document}|
-\end{Quote}
-
-%}{
-
-\subsection{オプション・スタイル}\label{sec:ENUM}
-
-\|\documentclass| （または \|\documentstyle|）の標準オプションとして，以下の6
-つのものが用意されている．
-%
-\begin{ENUMERATE}%{
-\item\|landscape     | オンライン出版用\footnote{%
-%
-A4横長のオンライン出版用の製版を行なうオプションは、現在は
-陽に指定しなければならないが、次回のリリースからはデフォルトとなる予定である。}
-\item\|portrait      | 紙出版用
-\item\|draft         | 投稿用
-\item\|technote      | テクニカルノート用
-\item\|preface       | 序文用
-\item\|english       | 英文用
-\item\|sigrecommended| 研究会推薦論文
-\item\|invited       | 招待論文
-\end{ENUMERATE}%}
-%
-これらのオプションは（意味があれば）任意の組合せで指定することができる．
-また論文誌への投稿／掲載以外の目的で使うことができるように，研究
-報告用の \|techrep| と，（著者自身のweb site等に掲載するための）「著者版」を
-作成する \|private| も用意されている．さらに後者では
-%
-\begin{itemize}\item[]%{
-\|\copyrightnotice{|\<著作権情報\>\|}|
-\end{itemize}%}
-%
-により，最初のページの左肩に学会著作権規定で定められた著作権に関する注意書を
-出力することもできる．
-
-\|\usepackage| で\footnote{{\LaTeX} 2.09の場合は \CS{documentstyle} のオプショ
-ン引数で．}%
-補助的なスタイルファイルを指定した場合には，製版用のファイル群に必ずスタイル
-ファイルを含める．ただし，{\LATEXe} の標準配布に含まれているもの（たとえば
-\|graphicx|）については同封の必要はない．なおスタイルファイルによっては論文
-誌スタイルと矛盾するようなものもあるので，スタイルファイルの性格を良く理解し
-て使用していただきたい．
-
-\subsection{巻数，号数などの記述}
-学会より指示された巻数，号数，先頭ページ番号\hbox{（\|\volpageoffset|）}，受
-付／採録年月日（年は平成年）を記述する．なお学会からの指示がない項目に関して
-は，記述しなくてよい．
-
-%}{
-
-\subsection{表題などの記述}\label{sec:Desc}
-
-表題，著者名とその所属，および概要を前述のコマンドや環境により{\dg 和文と英
-文の双方について}定義した後，\|\maketitle| によって出力する．
-なお投稿時には，表題と概要がそれぞれ別のページに出力され，著者名と所属は出力
-されない．
-%
-\begin{Description}
-\item[表題]
-\|\title| および \|\etitle| で定義した表題はセンタリングされる．文字数の多い
-ものについては{\dg 自動的な改行が行なわれない}ので，適宜 \|\\| を挿入して改行
-する．その際には各行は左詰めで組版され，その後最も長い行を基準にしてセンタリ
-ングされる．なお和文表題は奇数ページのヘッダにも表示されるので，ヘッダに納ま
-らないような長い表題の場合には
-%
-\begin{quote}
-\|\title[|\<ヘッダ用表題\>\|]{|\<表題\>\|}|
-\end{quote}
-%
-のように，ヘッダ用に短くしたものをオプション引数として指定する．
-
-\item[著者名と所属]
-各著者の所属を第一著者から順に \|\affilabel| を用いてラベル（第1引数）を付け
-ながら定義すると，脚注に ${\dagger}1$ や ${\dagger}2$ を付けて和文の所属
-（第2引数の\|\\|より前）と英文の所属（\|\\|より後）が出力される．なお，複数
-の著者が同じ所属である場合には，一度定義するだけで良い．また論文執筆時と発行
-時とでは所属が異なる場合には，\|\paffilabel| を用いて新しい所属を定義する．
-新しい所属は脚注に${\ast}1$や${\ast}2$などを付けて出力される．
-
-著者名は \|\author| と \|\eauthor| で定義し，複数の著者は \|\and| で区切る．
-また各著者名の直後に \|\affiref|\allowbreak\hbox{\|{|\<所属ラベル\>\|}|}
-をおいて（複数可）所属ラベル （\|\affilabel| や \|\paffilabel| で定義したも
-の）を参照し，対応する脚注参照記号を付加する．
-
-なお，和文著者名は必ず{\dg 姓と名を半角（ASCII）の空白で区切る}．
-
-\item[概要]
-和文の概要は \|abstract| 環境の中に，英文の概要は \|eabstract| 環境の中に，
-それぞれ記述する．
-\end{Description}
-
-%}{
-
-\subsection{見出し}
-
-節や小節の見出しには \|\section|, \|\subsection| といったコマンドを使用する．
-\|\section|の見出しは2行を占め，他は1行に出力される．
-
-「定義」，「定理」などについては，\|\newtheorem|で適宜環境を宣言し，
-その環境を用いて記述する．なお見出しは{\bf 定理1}などのように日本語の題と番
-号の組合せを想定しているので，題と番号の間には微小な空白しか入らない．もし
-{\bf Thorem 1}のような英語と番号の組合せを用いる場合には，\|\newtheorem*|に
-よって環境を宣言すれば，空白が挿入される．
-
-%}{
-
-\subsection{文章の記述}\label{sec:desc*}\label{sec:enum}
-
-\begin{description*}
-\item[行送り]
-学会誌は2段組を採用しており，左右の段で行の基準線の位置が一致することを原則
-としている．また，節見出しなど，行の間隔を他よりたくさんとった方が読みやすい
-場所では，この原則を守るようにスタイルファイルが自動的にスペースを挿入する．
-したがって本文中では \|\vspace| や \|\vskip| を用いたスペースの調整を行なわ
-ないでいただきたい．なお \|\begin{document}| の前にコマンド \|\checkline| を
-挿入しておくと，本文の各行が持つべき基準線が印刷されるので，行送りが正しいか
-どうかをチェックすることができる．ただしこのコマンドは原稿送付時には使用しな
-いでいただきたい．
-\item[フォントサイズ]
-このガイドの印刷結果からもわかるように，論文誌スタイルでは様々な大きさのフォ
-ントが使われるが，これらは全てスタイルファイルが自動的かつ注意深く選択したも
-のである．したがって，著者が自分でフォントサイズを変更する必要はなく，かえっ
-て行送りの原則を守る妨げにもなる．もし特定の箇所で1行に多くの文字を入れたい
-などの理由から小さいフォントを使用する場合には，\|\small*| あるいは
-\|\footnotesize*| という\|*|が付いたコマンドを使用していただきたい（この二つ
-以外は禁止）．これらは基準線間隔を変えずにフォントの大きさだけを変更するもの
-である．なお \|\small*| の例が\ref{sec:config}節と次のページに示されている．
-
-\item[句読点]
-句点には全角の「．」，読点には全角の「，」を用いる．ただし英文中や数式
-中で「.」や「,」を使う場合には，半角文字を使う．「。」や「、」は一切使
-わない．
-
-\item[全角文字と半角文字]
-全角文字と半角文字の両方にある文字は次のように使い分ける．
-%
-\begin{enumerate}
-\item 括弧は全角の「（」と「）」を用いる．但し，英文の概要，図表見出し，書誌
-データでは半角の「(」と「)」を用いる．
-
-\item
-英数字，空白，記号類は半角文字を用いる．ただし，句読点に関しては，前項で述べ
-たような例外がある．
-
-\item
-カタカナは全角文字を用いる．
-
-\item
-引用符では開きと閉じを区別する. 開きには \|``|（``） を用い，閉じには \|''|
-（''） を用いる．
-\end{enumerate}
-
-\item[OverfullとUnderfull]
-製版時にはoverfullを起こさないことを原則としている．従って，まず提出するソー
-スが著者の環境でoverfullを起こさないように，文章を工夫するなどの最善の努力を
-払っていただきたい．但し，\|flushleft| 環境，\|\\|，\|\linebreak| などによる
-両端揃えをしない形でのoverfullを回避は，できるだけ避けていただきたい．また著
-者の
-環境では発生しないoverfullが，印刷時の環境では発生することもある．このような
-事態をできるだけ回避するために，文中の長い数式や \|\verb| を避ける，パラグラフ
-の先頭付近では長い英単語を使用しない，などの注意を払っていただきたい．
+圏における他の性質から、プログラムの変更の性質の解析や他の手法を提案する。

-また，\verb|\\| をパラグラフの終りで使用すると
-%
-\begin{Quote}\small*
-\|Underfull \hbox (badness 10000) detected|
-\end{Quote}
-%
-のwarningが発生し，空行が挿入される．このような空行は見苦しく，また重要なエ
-ラー・メッセージを見逃す原因にもなるので，ソースを提出する時点では全て除去さ
-れているようにしていただきたい．特に，箇条書用環境の直前， \|\item| の直前，
-箇条書用環境の末尾などで \verb|\\| を使うと，前述のwarning が出力されること
-に注意していただきたい．
-\end{description*}
-
-%}{
-
-\subsection{数式}\label{sec:Item}
-
-\begin{Itemize}
-\item 本文中の数式\\
-本文中の数式は \|$| と \|$|, \|\(| と \|\)|, あるいは \|math| 環境のいずれで
-囲んでもよい．なお \smash{$\frac{a}{b}$} (\|\frac{a}{b}|) のように背が高い要
-素は見苦しくかつ行送りを乱すことにもなるので，使用しないようにしていただきた
-い．
-
-\item 別組の数式\\
-別組数式(displayed math)については {\bf \|$$| と \|$$| は使用してはならない}．
-すなわち \|\[| と \|\]| で囲むか, \|displaymath|, \|equation|, \|eqnarray|
-のいずれかの環境を用いなければならない．これらは
-%
-\begin{equation}
-\Delta_l = \sum_{i=l+1}^L\delta_{pi}
-\end{equation}
-%
-のように，センタリングではなく固定字下げで数式を出力し，かつ背が高い数式によ
-る行送りの乱れを吸収する機能がある．
-
-\item \|eqnarray|環境\\
-互いに関連する別組の数式が2行以上連続して現れる場合には，単に \|\[| と \|\]|，
-あるいは \|\begin{equation}| と \|\end{equation}| で囲った数式を書き並べるの
-ではなく，\|\begin|\allowbreak\|{eqnarray}| と \|\end{eqnarray}| を使って，
-等号（あるいは不等号）の位置で縦揃えを行なった方が読みやすい．なお
-\|eqnarray| の中では改ページが行なわれないので，行数が多く途中で改ページが起
-こって欲しい場合には，\|\begin{eqnarray}[s]| のようにオプション \|[s]| を指
-定すればよい．
-
-\item 数式のフォント\\
-{\LaTeX}が標準的にサポートしているもの以外の特殊な数式用フォントは，できるだ
-け使わないようにしていただきたい．どうしても使用しなければならない場合には，
-その旨申し出ていただくとともに，印刷工程に深く関与していただくこともあること
-に留意されたい．
-\end{Itemize}
-
-%}{
-
-\subsection{図}
-
-1段の幅におさまる図は，\figref{fig:single} の形式で指定する. 位置の指定に \|h|
-は使わない．また，図の下に{\dg 和文と英文の双方の}見出しを，\|\caption| と %
-\|\ecaption| で指定する．文字数が多い見出しはは自動的に改行して最大幅の行を
-基準にセンタリングするが，見出しが2行になる場合には適宜 \|\\| を挿入して改行
-したほうが良い結果となることがしばしばある（\figref{fig:single} の英文見出し
-を参照）．
-
-\begin{figure}
-\setbox0\vbox{
-\hbox{\|\begin{figure}[tb]|}
-\hbox{\quad \<図本体の指定\>}
-\hbox{\|\caption{|\<和文見出し\>\|}|}
-\hbox{\|\ecaption{|\<英文見出し\>\|}|}
-\hbox{\|\label{| $\ldots$ \|}|}
-\hbox{\|\end{figure}\|}}
-\centerline{\fbox{\box0}}
-\caption{1段幅の図}
-\ecaption{Single column figure with caption\\
-    explicitly broken by $\backslash\backslash$.}
-\label{fig:single}
-\end{figure}
-
-2段の幅にまたがる図は，\figref{fig:double} の形式で指定する. 位置の指定は
-\|t| しか使えない．
-
-\begin{figure*}
-\setbox0\vbox{\large
-\hbox{\|\begin{figure*}[t]|}
-\hbox{\quad\<図本体の指定\>}
-\hbox{\|\caption{|\<和文見出し\>\|}|}
-\hbox{\|\ecaption{|\<英文見出し\>\|}|}
-\hbox{\|\label{| $\ldots$ \|}|}
-\hbox{\|\end{figure*}|}}
-\centerline{\fbox{\hbox to.9\textwidth{\hss\box0\hss}}}
-\caption{2段幅の図}
-\ecaption{Double column figure.}
-\label{fig:double}
-\end{figure*}
-
-図の中身では本文と違い，どのような大きさのフォントを使用しても構わない
-（\figref{fig:double} 参照）．また図の中身として，encapsulate された
-PostScript ファイル（いわゆるEPSファイル）を読み込むこともできる．読み込みの
-ためには，プリアンブルで
-%
-\begin{Quote}
-\|\usepackage{graphicx}|
-\end{Quote}
-%
-を行った上で，\|\includegraphics| コマンドを図を埋め込む箇所に置き，その引数
-にファイル名（など）を指定する．また{\LaTeX} 2.09の場合は，\|epsf| を
-\|\documentstyle| のオプションで指定し，\|\epsfile| コマンドで図を埋め込む．
-
-この節を注意深く見ると，\figref{fig:single} や\figref{fig:double} の最初の参照
-はゴチック体であるのに対し，2回目以降では明朝体であるのに気づくだろう．この
-切替えは論文誌の伝統的体裁に基づくもので，図の参照を（「図\hbox{\|\ref{|\<ラ
-ベル\>\|}|}」ではなく）\|\figref{|\<ラベル\>\|}|を用いて行なえば自動的に成され
-る．
-
-%}{
-
-\subsection{表}
-
-表の罫線はなるべく少なくするのが，仕上がりをすっきりさせるコツである．罫線を
-つける場合には，一番上の罫線には二重線を使い，左右の端には縦の罫線をつけない
-（\tabref{tab:example}）．表中のフォントサイズのデフォルトは\|\small|である．
-
-また，表の上に{\dg 和文と英文の双方の}見出しを， \|\caption|と \|\ecaption|
-で指定する．表の参照は \|\tabref{|\<ラベル \>\|}| を用いて行なう．
-
-\begin{table}[b] \caption{箇条書環境の使用箇所（表の例）} \ecaption{Sections
-and sub-sections in which list-like environments are used (example of
-table).} \label{tab:example}
-% 左右の罫線はつけず，一番上の罫線は二重線
-\hbox to\hsize{\hfil
-\begin{tabular}{l|lll}\hline\hline
-&enumerate&itemize&description\\\hline
-type-1& \ref{sec:enum}& \ref{sec:item}& ---\\
-type-2& ---&        \ref{sec:item*}&\ref{sec:desc*}\\
-type-3& \ref{sec:Enum}& \ref{sec:Item}& \ref{sec:Desc}\\
-type-4& \ref{sec:ENUM}& \ref{sec:ITEM}& \ref{sec:DESC}\\\hline
-\multicolumn{4}{l}{type-1\,: enumerate等\quad type-2\,: enumerate*等}\\
-\multicolumn{4}{l}{type-3\,: Enumerate等\quad type-4\,: ENUMERATE等}\\
-\end{tabular}\hfil}
-\end{table}
-
-%}{
-
-\subsection{箇条書}\label{sec:item*}
-
-論文誌では箇条書に関する形式を特に定めておらず，場合に応じて様々な様式が用い
-られている．スタイルファイルでは，{\LaTeX} の箇条書用の環境である
-\|enumerate|, \|itemize|, \|description| に4種類のファミリーを設け，状況に応
-じた使い分けができるようにしている．
-%
-\begin{itemize*}
-\item \|enumerate|, \|itemize|, \|description|\\
-{\LaTeX} の標準的なものと同じ．但しインデンテーションは \|enumerate| では全角3
-文字分，その他は全角2文字分である．また \|enumerate| のラベルは，標準の
-%
-\begin{quote}
-1.\quad (a)\quad i.\quad A.
-\end{quote}
-%
-ではなく，
-%
-\begin{quote}
-(\,1\,)\quad (\,a\,)\quad (\,i\,)\quad (\,A\,)
-\end{quote}
-%
-のように全て括弧付きであり，数字などの前後に小さな空白が挿入される．
-
-\item \|enumerate*|, \|itemize*|, \|description*|\\
-\|enumerate|などとほぼ同じだが，インデンテーションは全角1文字分である．
-
-\item \|Enumerate|, \|Itemize|, \|Description|\\
-文章のインデンテーションを行なわない．
-
-\item \|ENUMERATE|, \|ITEMIZE|, \|DESCRIPTION|\\
-文章のインデンテーションを行なわず，先頭行（ラベルがある行）を全角1文字分だ
-けインデントする．
-\end{itemize*}
-%
-\tabref{tab:example} に示すように
-このパンフレットの各章／節に各々の環境の使用例があるので，適宜参照されたい．
-
-%}{
-
-\subsection{左右の段の行揃え}
-
-文章の記述のところでも述べたように，論文誌では左右の段で行の位置をそろえる必
-要がある．ユーザが特別な高さのボックスを使ったために行の位置が乱れてしまうよ
-うな場合には，その部分を \|\begin|\allowbreak\|{adjustvboxheight}| と %
-\|\end|\allowbreak\|{adjustvboxheight}| で囲っていただきたい．この環境は中途
-半端な行送りを吸収するためのものである．例えば次の；
-%
-\begin{adjustvboxheight}
-\begin{quote}
-\fbox{$\displaystyle\sum_{i=0}^n i$}
-\end{quote}
-\end{adjustvboxheight}
-%
-は，以下のようにして出力したものである．
-%
-\begin{Quote}
-\|\begin{adjustvboxheight}|\\
-\|\begin{quote}|\\
-\|\fbox{$\displaystyle\sum_{i=0}^n i$}|\\
-\|\end{quote}|\\
-\|\end{adjustvboxheight}|
-\end{Quote}
-%
-ただしこのようなものを本文中に挿入することを推奨しているわけではない．
-
-%}{
-
-\subsection{脚注}
-脚注は \|\footnote| コマンドを使って書くと，ページ単位に\footnote{脚注の例．}
-や\footnote{二つめの脚注．}のような参照記号とともに脚注が生成される．なお，
-ページ内に複数の脚注がある場合，参照記号は {\LaTeX} を2回実行しないと正しく
-ならないことに注意されたい．
-（{\LaTeX} ブック \cite{latex} の156ページ参照．）
-
-また場合によっては，脚注をつけた位置と脚注本体とを別の段に置く方がよいことも
-ある．この場合には，\|\footnotemark| コマンドや \|\footnotetext| コマンドを
-使って対処していただきたい．
-
-%}{
-
-\subsection{参考文献の参照}
-
-本文中で参考文献を参照する場合には，参考文献番号が文中の単語
-として使われる場合と，そうでない参照とでは，使用する文字の大きさが異
-なる．前者は\|\Cite|により参照し，後者は\|\cite|により参照する．たとえば；
-%
-\begin{Quote}
-文献 \|\Cite{total}| は \|\LaTeX\cite{latex}| の総合的な解説書である．
-\end{Quote}
-%
-と書くと；
-%
-\begin{Quote}
-文献\Cite{total}は\LaTeX\cite{latex}の総合的な解説書である．
-\end{Quote}
-%
-が得られる．
-
-また，一つの \|\Cite| あるいは \|\cite| コマンドで三つ以上の文献を参照し，か
-つそれらの参照番号が連続している場合，\Cite{article1,article2,article3}や
-「文献\cite{latex,article4,article5,article6}」のように，自動的に先
-頭と末尾の文献番号が `--' (en-dash) で結合される．なお，非常に多数の文献を参
-照し，それら全てを \|\Cite| や \|\cite|で指定するのが面倒な場合は
-%
-\begin{Quote}\raggedright
-\|\multiCite{|\<先頭文献のラベル\>\|}|\nobreak\hskip-2em\allowbreak
-    \hspace*{2em}\hbox{\|{|\<末尾文献のラベル\>\|}|}\\
-\|\multicite{|\<先頭文献のラベル\>\|}|\nobreak\hskip-2em\allowbreak
-    \hspace*{2em}\hbox{\|{|\<末尾文献のラベル\>\|}|}
-\end{Quote}
-%
-を用いて，\multiCite{article1}{book3}や「文献
-\multicite{booklet1}{unpublished}」のような結果を得ることもできる．
-
-%}{
-
-\subsection{参考文献リスト}
-
-参考文献リストには，原則として本文中で引用した文献のみを列挙する．順序は参照
-順あるいは第一著者の苗字のアルファベット順とする．文献リストは BiB{\TeX}
-と \|ipsjunsrt.bst|（参照順）または \|ipsjsort.bst|（アルファベット順）を用
-いて作り，\|\bibliograhpystyle| と \|\bibliography| コマンドにより読み込むこ
-とを原則とする\footnotemark ．これらを用いれば，規定の体裁にあったものができ
-%
-% 23 行下の \footnotetext 参照．
-%
-るので，できるだけ利用していただきたい．
-なおこのガイドの参考文献は，\|bibsample.bib| を文献スタイル \|ipsjunsort| で
-処理した結果であるので，両者を適宜参照されたい．また製版用のファイル群には
-\|.bib| ファイルではなく \|.bbl| ファイルを必ず含めることに注意されたい．
-
-一方，何らかの理由で \|thebibliography| 環境で文献リストを「手作り」しなけれ
-ばならない場合は，このガイドの参考文献リストを注意深く見て，そのスタイルにし
-たがっていただきたい．
-
-%}{
-
-\subsection{謝辞，付録}
-
-謝辞がある場合には，参考文献リストの直前に置き，\|acknowledgment|環境の中に
-入れる．この環境の中身は投稿時には出力されない．
-
-付録がある場合には，参考文献リストの直後にコマンド \|\appendix| に引き続いて
-書く．なお付録では，\|\section| コマンドが{\bf A.1}，{\bf A.2}などの見出しを
-生成する．また付録全体に見出しをつける場合には，\|\appendix[|\<見出し\>\|]| %
-のように見出しをオプション引数として与える．
-
-\footnotetext{このガイドはファイルを一つにするために
-{\TT thebibliography} 環境を用いているが，その中身はBiB{\TeX}で作成したもの
-である．
-また，このfootnoteは左カラムにマークがあるのにfootnote自体は
-右カラムに現われている．これは簡単なトリックで実現できる．ソースファイ
-ル参照．}
-% 31 行上の \footnotemark 参照．
-
-%}{
-
-\subsection{著者紹介}\label{sec:DESC}
-
-本文の最後（\|\end{document}| の直前）に，以下のように著者紹介を記述する．
-%
-\begin{quote}
-\|\begin{biography}|\\
-\|\member{|\<第一著者名\>\|}|\\
-\mbox{}\quad\<第一著者の紹介\>\\
-\|\member{|\<第二著者名\>\|}|\\
-\mbox{}\quad\<第二著者の紹介\>\\
-\mbox{}\quad $\ldots\ldots\ldots$ \\
-\|\end{biography}|
-\end{quote}
-%
-なお著者が学生会員あるいは非会員の場合は，正会員用の \|\member| の代わりに
-下記を用いる．
-%
-\begin{DESCRIPTION}
-\item[学生会員]：\|\stmember{|\<著者名\>\|}|
-\item[非会員\phantom{あ}]：\|\nomember{|\<著者名\>\|}|
-\end{DESCRIPTION}
-%
-なお著者紹介は投稿時には出力されない．
-
-%}{
-
-\subsection{ページ数の見積り}
-
-投稿用スタイルでは1ページが\(35\hbox{字}\times32\hbox{行}=1120\hbox{字}\)，
-また製版用では\(24\hbox{字}\times46\hbox{行}\times2\hbox{段}=2208\hbox{字}\)
-である．したがって粗い見積りとして，製版時には投稿時の半分のページ数になると
-考えることができる．たとえば，このガイドは投稿用では19ページ，製版用では9ペー
-ジであるので，ほぼ見積った通りである．
-
-また投稿用のファイルを製版用にするのは簡単であるので，投稿時にあらかじめどの
-ように製版されるかを試せば，もっと良い見積りが得られる．
-
-%}{
-
-\section{おわりに}
-
-論文誌の {\LaTeX} 化は10年以上の運用実績があるが，解決されていない問題点も
-皆無とはいえない．
-これらを著者の方々の御協力を仰ぎつつ，少しでも使いやすく
-するための改良を加えていくつもりである．そこで，スタイル・ファイルに関する要
-望や意見を，是非
-%
-\begin{Quote}
-\|texnicians@ipsj.or.jp|
-\end{Quote}
-%
-までお寄せいただきたい．また技術的な質問も同じアドレスで受け付けるが，その他
-の一般的な質問については
-%
-\begin{Quote}
-\|editt@ipsj.or.jp|
-\end{Quote}
-%
-にお寄せいただきたい．
-
-\begin{acknowledgment}
-論文誌の {\LaTeX}化に御協力いただいた三美印刷（株），（株）ウルス，ならびに
-試行のためのボランティアをお願いした著者の皆様に，謹んで感謝の意を表する．
-\end{acknowledgment}

 %}{

 \begin{thebibliography}{10}

-\bibitem{latex}
-Lamport, L.: {\em A Document Preparation System {\LaTeX} User's Guide \&
-  Reference Manual}, Addison Wesley, Reading, Massachusetts (1986).
-\newblock （Cooke, E., et al.訳：文書処理システム {\LaTeX}，アスキー出版局
-  (1990)）.
-
-\bibitem{total}
-伊藤和人：{\LaTeX} トータルガイド，秀和システムトレーディング (1991).
-
-\bibitem{article1}
-桜井貴文：直観主義論理と型理論，情報処理， Vol.~30, No.~6, pp.\ 626--634
-  (1989).
-
-\bibitem{article2}
-野口健一郎，大谷　真：OSIの実現とその課題，情報処理， Vol.~31, No.~9, pp.\
-  1235--1244 (1990).
-
-\bibitem{article3}
-Itoh, S. and Goto, N.: An Adaptive Noiseless Coding for Sources with Big
-  Alphabet Size, {\em Trans. IEICE},  Vol.~E74, No.~9, pp.\ 2495--2503 (1991).
-
-\bibitem{article4}
-田中{正次}，村松　茂，山下　茂：9段数7次陽的Runge-Kutta法の最適化について，情%
-報処理学会論文誌， Vol.~33, No.~12, pp.\ 1512--1526 (1992).
-
-\bibitem{article5}
-Abrahamson, K., Dadoun, N., Kirkpatrick, D.~G. and Przytycka, T.: A Simple
-  Parallel Tree Contraction Algorithm, {\em J. Algorithms},  Vol.~10, No.~2,
-  pp.\ 287--302 (1989).
-
-\bibitem{article6}
-田中{正次}ほか：9段数7次陽的Runge-Kutta法の次数条件式の解について，情報処理学%
-会論文誌， Vol.~33, No.~12, pp.\ 1506--1511 (1992).
-
-\bibitem{book3}
-Chang, C.~L. and Lee, R. C.~T.: {\em Symbolic Logic and Mechanical Theorem
-  Proving}, Academic Press, New York (1973).
-\newblock （長尾真，辻井潤一訳: 計算機による定理の自動証明, 日本コンピュータ%
-  協会 (1983)）.
-
-\bibitem{booklet1}
-新世代コンピュータ技術開発機構：第五世代コンピュータプロジェクトの概要，{FGCS'%
-92}にて配布 (1992).
-
-\bibitem{unpublished}
-情報処理学会論文誌編集委員会：{\LaTeX}による論文作成のガイド（第1版） (1995).
-\newblock （論文著者に配布）.
+\bibitem{moggi} Eugenio Moggi: Notion of Computation and Monads(1991)
+\bibitem{category} Michael Barr and Charles Wells: Category Theory for Computing Science(1989)
+\bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)
+\bibitem{agda} The Agda Wiki - Agda \\ \verb|http://wiki.portal.chalmers.se/agda/pmwiki.php|

 \end{thebibliography}

 %}{

-\appendix
-\section{研究会論文誌用コマンド}\label{sec:app-sig}
-
-各研究会論文誌（トランザクション）には各々に固有のサブタイトル，略称，通番が
-ある．製版用原稿では，以下のコマンドを\|\begin{document}|の前に置くことによ
-り，これらの情報を与える．
-%
-\begin{itemize}\item[]
-\|\transaction{|\<略称\>\|}{|\<巻数\>\|}{|\<号数\>\|}|
-\end{itemize}
-%
-なお\<略称\>は以下のいずれかであり，\<巻数\>と\<号数\>は学会あるいは研究会論
-文誌編集委員会の指示に基づいて与える．
-%
-\begin{itemize}%{
-\item
-\|PRO|（プログラミング）
-\item
-\|TOM|（数理モデル化と応用）
-\item
-\|TOD|（データベース）
-\item
-\|ACS|（コンピューティングシステム）
-\item
-\|CVIM|（コンピュータビジョンとイメージメディア）
-\item
-\|TBIO|（Bioinformatics）\footnote{%
-TBIO, SLDM, CVAは英文論文誌であるので和名はない．}
-\item
-\|SLDM|（System LSI Design Methodology）\footnotemark[1]
-\item
-\|CVA|（Computer Vision and Applicaitons）\footnotemark[1]
-%
-\end{itemize}%}
-%
-また上記の\<号数\>は発行月とは連動していないので，学会あるいは編集委員会の指
-示に基づき発行月を；
-%
-\begin{itemize}\item[]
-\|\setcounter{|{\bf 月数}\|}{|\<発行月\>\|}|
-\end{itemize}
-%
-によって指定する．
-
-この他，以下の各節で示すように，いくつかの論文誌に固有の機能を実現するための
-コマンドなどが用意されている．
-
-%}{
-
-\subsection{「プログラミング」固有機能}
-
-「論文誌：プログラミング」には論文以外に，プログラミング研究会での研究発表の
-内容梗概が含まれている．この内容梗概は，\|\documentclass|または
-\|\documentstyle|のオプションとして\|abstract|を指定した上で，
-\ref{sec:config}節の\|\maketitle|までの内容からなるファイル（すなわち本文が
-ないファイル）から生成する．なお\|\|{\bf 受付}や\|\|{\bf 採録}は不要であるが，
-代わりに発表年月日を；
-%
-\begin{itemize}\item[]
-\|\|{\bf 発表}\|{|\<年\>\|}{|\<月\>\|}{|\<日\>\|}|
-\end{itemize}
-%
-により指定する．
-
-%}{
-
-\subsection{「数理モデル化と応用」固有機能}
-
-「論文誌：数理モデル化と応用」の論文では，受付や採録の日付以外に再受付日付を
-記載するように指示されることがある．その場合には；
-%
-\begin{itemize}\item[]
-\|\|{\bf 再受付}\|{|\<年\>\|}{|\<月\>\|}{|\<日\>\|}|
-\end{itemize}
-%
-により指定する．なお複数回の再受付が行われた場合，上記のコマンドを繰り返し使
-用する．
-
-%}{
-
-\subsection{「データベース」固有機能}
-
-「論文誌：データベース」の論文の担当編集委員の氏名は；
-%
-\begin{itemize}\item[]
-\|\edInCharge{|\<氏名\>\|}|
-\end{itemize}
-%
-により指定する．
-
-%}{
-
-\subsection{「Bioinformatics」固有機能}
-
-Trans.\ Bioinformatics (TBIO)に固有の機能を利用するためには，\|\documentclass|
-（または\|\documentstyle|）のオプションで\|TBIO|を指定する．なおTBIOは英文論
-文誌であるので，\|TBIO|オプションの指定によって自動的に\|english|オプション
-が指定されたものとみなされる．したがって；
-%
-\begin{itemize}\item[]
-\|\documentclass[TBIO]{ipsjpaper}|
-\end{itemize}
-%
-のように\|english|オプションを省略することができる．またこのオプションの指定
-により，以下のコマンドが使用可能となる．
-%
-\begin{itemize}%{
-\item
-論文の種別は；
-%
-\begin{itemize}\item[]
-\|\TBIOpapercategory{|\<種別\>\|}|
-\end{itemize}
-%
-を用いて，\|original|, \|survey|, \|database| のいずれかを指定する．この結果，
-``{\it Original Paper}'', ``{\it Survey Paper}'' または ``{\it
-Database\slash Software Paper}'' のいずれかが先頭ページのタイトルの左上に表
-示される．なおこのコマンドが与えられなければ \|original| とみなされる．
-
-\item
-担当編集委員の氏名は；
-%
-\begin{itemize}\item[]
-\|\edInCharge{|\<氏名\>\|}|
-\end{itemize}
-%
-により指定する．
-
-\item
-査読過程で条件付採録となった論文の再受付日は；
-%
-\begin{itemize}\item[]
-\|\rereceived{|\<年\>\|}{|\<月\>\|}{|\<日\>\|}|
-\end{itemize}
-%
-により指定する．
-
-\end{itemize}%}
-%
-なお後の2つのコマンドの使用はオプショナルであり，学会あるいは編集委員会から
-の情報提供や指示がなければ省略しても構わない．
-
-%}{
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % ウィンターワークショップでは不要（ここから）
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%