Mercurial > hg > Papers > 2018 > nozomi-master

--- a/paper/agda.tex	Mon Feb 06 15:42:45 2017 +0900
+++ b/paper/agda.tex	Mon Feb 06 16:13:14 2017 +0900
@@ -281,10 +281,10 @@
 % {{{ 依存型を持つ証明支援系言語 Agda

 \section{依存型を持つ証明支援系言語 Agda}
-型システムを用いて証明を行なうことができる言語に Agda が存在する。% ref Agda のref
+型システムを用いて証明を行なうことができる言語に Agda~\cite{agda} が存在する。
 Agda は依存型という強力な型システムを持っている。
 依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
-この節では Agda の文法的な紹介を行なう~\cite{agda-documetation}。 % ref pdf のアレ
+この節では Agda の文法的な紹介を行なう~\cite{Norell:2009:DTP:1481861.1481862}~\cite{agda-documentation}。

 まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
 トップレベルのモジュールはファイル名と同一となる。
Binary file paper/atton-master.pdf has changed
--- a/paper/cbc-type.tex	Mon Feb 06 15:42:45 2017 +0900
+++ b/paper/cbc-type.tex	Mon Feb 06 16:13:14 2017 +0900
@@ -222,7 +222,7 @@
 そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。
 CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。

-\lstinputlisting[label=agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda}
+\lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda}

 次にスタックへの操作に注目する。
 スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。
@@ -259,7 +259,7 @@

 \lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda}

-また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 % TODO
+また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。

 % }}}
--- a/paper/cbc.tex	Mon Feb 06 15:42:45 2017 +0900
+++ b/paper/cbc.tex	Mon Feb 06 16:13:14 2017 +0900
@@ -108,7 +108,7 @@
 現在存在するメタ計算としてメモリの確保と割り当て、並列に書き込むことが可能な Synchronized Queue、データの保存に用いる非破壊赤黒木がある。

 GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。
-マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL/CUDA における kernel も含まれる。 % TODO: ref OpenCL/CUDA
+マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL~\cite{opencl}/CUDA~\cite{cuda} における kernel も含まれる。
 kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行されるものである。
 通常 GPU でデータの処理を行なう場合はデータの転送、転送終了を同期で確認、 kernel 実行、kernel の終了を同期で確認する、という手順が必要である。
 CPU/GPU での処理をメタ計算で行なうことにより、ノーマルレベルでは CodeGear が実行されるデバイスや DataGear の位置を意識する必要が無いというメリットがある。
--- a/paper/reference.bib	Mon Feb 06 15:42:45 2017 +0900
+++ b/paper/reference.bib	Mon Feb 06 16:13:14 2017 +0900
@@ -129,6 +129,18 @@
     note = {Accessed: 2016/01/20(Fri)}
 }

+@misc{opencl,
+    title = {OpenCL | NVIDIA Developer},
+    howpublished = {\url{https://developer.nvidia.com/opencl}},
+    note = {Accessed: 2016/02/06(Mon)}
+}
+
+@misc{cuda,
+    title = {CUDA Zone | NVIDIA Developer},
+    howpublished = {\url{https://developer.nvidia.com/cuda-zone}},
+    note = {Accessed: 2016/02/06(Mon)}
+}
+


 @techreport{weko_142109_1,
@@ -164,3 +176,88 @@
   year={2013},
   publisher={オーム社}
 }
+
+@inproceedings{Norell:2009:DTP:1481861.1481862,
+ author = {Norell, Ulf},
+ title = {Dependently Typed Programming in Agda},
+ booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
+ series = {TLDI '09},
+ year = {2009},
+ isbn = {978-1-60558-420-1},
+ location = {Savannah, GA, USA},
+ pages = {1--2},
+ numpages = {2},
+ url = {http://doi.acm.org/10.1145/1481861.1481862},
+ doi = {10.1145/1481861.1481862},
+ acmid = {1481862},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {dependent types, programming},
+}
+
+@article{Backus:1978:HFI:960118.808380,
+ author = {Backus, John},
+ title = {The History of FORTRAN I, II, and III},
+ journal = {SIGPLAN Not.},
+ issue_date = {August 1978},
+ volume = {13},
+ number = {8},
+ month = aug,
+ year = {1978},
+ issn = {0362-1340},
+ pages = {165--180},
+ numpages = {16},
+ url = {http://doi.acm.org/10.1145/960118.808380},
+ doi = {10.1145/960118.808380},
+ acmid = {808380},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@ARTICLE{Landin64,
+  AUTHOR = {Peter J. Landin},
+  TITLE = {The Mechanical Evaluation of Expressions},
+  JOURNAL = {Computer Journal},
+  VOLUME = 6,
+  NUMBER = 4,
+  MONTH = JAN,
+  YEAR = 1964,
+  PAGES = {308--320},
+  CHECKED = {5 June 1992, by JCR}
+}
+@book{GlossarWiki:Church:1941,
+   author = {Church, Alonzo},
+   title = {The Calculi of Lambda-Conversion},
+   publisher = {Princeton University Press},
+   year = {1941},
+   address = {Princeton, New Jork},
+   url = {http://books.google.de/books/about/The_Calculi_of_Lambda_conversion.html?id=KCOuGztKVgcC},
+   quality = {5},
+   note = {}
+ }
+
+@article{haskell-sigplan
+    ,author="Hudak, P. and Peyton Jones, S. and Wadler (editors), P."
+    ,title="Report on the {P}rogramming {L}anguage {H}askell,
+           {A} {N}on-strict {P}urely {F}unctional {L}anguage ({V}ersion 1.2)"
+    ,journal="ACM SIGPLAN Notices"
+    ,volume=27
+    ,number=5
+    ,month=May
+    ,year=1992
+    }
+
+@article{DEBRUIJN1972381,
+title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
+journal = "Indagationes Mathematicae (Proceedings)",
+volume = "75",
+number = "5",
+pages = "381 - 392",
+year = "1972",
+note = "",
+issn = "1385-7258",
+doi = "http://dx.doi.org/10.1016/1385-7258(72)90034-0",
+url = "http://www.sciencedirect.com/science/article/pii/1385725872900340",
+author = "N.G de Bruijn",
+
+}
--- a/paper/type.tex	Mon Feb 06 15:42:45 2017 +0900
+++ b/paper/type.tex	Mon Feb 06 16:13:14 2017 +0900
@@ -49,7 +49,7 @@

     \item 効率性

-        そもそも、科学計算機における最初の型システムは Fortran などにおける式の区別であった。% TODO ref fortran
+        そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける式の区別であった。
         整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
         型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
         昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。
@@ -119,7 +119,7 @@

 また、項の帰納的表現の略記法として、二次元の推論規則形式を用いる方法もある。
 これは論理体系を自然演繹スタイルで表現するためによく使われる。
-自然演繹による証明は\ref{agda}章内で触れるが、今回は項表現として導入する。
+自然演繹による証明は\ref{chapter:agda}章内で触れるが、今回は項表現として導入する。

 \begin{definition}
     項の集合は次の規則によって定義される。
@@ -552,9 +552,9 @@
 計算とは何か、エラーとは何か、を算術式を定義することによって示してきた。
 また、型を導入することにより行き詰まり状態を回避することも示した。
 ここで、プログラミング言語における計算を形式的に定義していく。
-プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61
+プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した~\cite{Landin64}。
 この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算であった。
-ラムダ計算は Alonzo Church が発明した形式的体系の一つである。 % TODO: ref
+ラムダ計算は Alonzo Church が発明した形式的体系の一つである~\cite{GlossarWiki:Church:1941}。
 ラムダ計算では全ての計算が関数定義と関数適用の基本的な演算に帰着される。
 ラムダ計算はプログラミング言語の機能の仕様記述や、言語設計と実装、型システムの研究に多く使われている。
 この計算体系の重要な点は、ラムダ計算内部で計算が記述できるプログラミング言語であると同時に、それ自身について厳格な証明が可能な数学的対象としてみなせる点にある。
@@ -563,7 +563,7 @@
 数や組やレコードなどはラムダ計算そのもので模倣することができるが、記述が冗長になってしまう。
 それらの機能のための具体的な特殊構文を加えることは言語の利用者の視点で便利である。
 他にも書き換え可能な参照セルや非局所的な例外といった複雑な機能を表現することもできるが、膨大な変換を用いなければモデル化できない。
-それらを言語として備えた拡張に ML や Haskell といったものがある。 % TODO: ref
+それの機能を言語として備えた拡張に ML や Haskell~\cite{haskell-sigplan} といったものがある。

 ラムダ計算(または $ \lambda $ 計算) とは、関数定義と関数適用を純粋な形で表現する。
 ラムダ計算においてはすべてが関数である。
@@ -743,7 +743,7 @@

 この定義は少なくとも代入が行なわれる際には正しく代入が行なえる。
 さらに、抽象が束縛している変数を名前では無く数字として扱う名無し表現も存在する。
-これは De Brujin 表現と呼ばれ、コンパイラ内部などでの項表現として用いられる。 % TODO: ref and spell check
+これは De Brujin 表現~\cite{DEBRUIJN1972381}と呼ばれ、コンパイラ内部などでの項表現として用いられる。

 最終的な型無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。