changeset 47:45d3ac176bf5

Mini fixes
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 30 Jan 2017 14:54:01 +0900
parents 3aeabd46d72b
children 623c90a21227
files paper/cbc.tex paper/type.tex
diffstat 2 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/paper/cbc.tex	Mon Jan 30 14:25:14 2017 +0900
+++ b/paper/cbc.tex	Mon Jan 30 14:54:01 2017 +0900
@@ -102,8 +102,9 @@
 % {{{ Continuation based C におけるメタ計算の例: GearsOS
 \section{Continuation based C におけるメタ計算の例: GearsOS}
 CbC におけるメタ計算は軽量継続を行なう際に Meta CodeSegment を挟むことで実現できる。
-CbC を用いてメタ計算を実現した例として、GearsOS\cite{weko_142108_1}が存在する。
+CbC を用いてメタ計算を実現した例として、GearsOS\cite{weko_142109_1}が存在する。
 GearsOS とはマルチコアCPUやGPU環境での動作を対象としたOSであり、現在OSの設計と並列処理部分の実装が行なわれている。
+GearsOS におけるメタ計算はMonadによって形式化されている\cite{Moggi:1991:NCM:116981.116984}。
 現在存在するメタ計算としてメモリの確保と割り当て、並列に書き込むことが可能な Synchronized Queue、データの保存に用いる非破壊赤黒木がある。
 
 GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。
--- a/paper/type.tex	Mon Jan 30 14:25:14 2017 +0900
+++ b/paper/type.tex	Mon Jan 30 14:54:01 2017 +0900
@@ -228,10 +228,9 @@
 \end{definition}
 
 例えば、
-
-\verb/if true then true else (if false then false else false)/
-
-は E-IFTRUE のインスタンスであり、 E-IFTRUEの $ t_2 $ が \verb/true/ かつ $ t_3 $ が \verb/if false then false else false/ の時である。
+$ if \; true \; then \; true \; else \; ( \;if \; false \; then \; false \; else \; false) $
+は E-IFTRUE のインスタンスであり、 E-IFTRUEの $ t_2 $ が \verb/true/ かつ、
+$ t_3 $ が $ if \; false \; then \; false \; else \; false \;$ の時に相当する。
 
 \begin{definition}
 1ステップ評価関係 $ \rightarrow $ とは、3つの評価の規則を満たす、項に関する最小の二項関係である。
@@ -584,7 +583,7 @@
 つまり、 $ s \, t \, u $ は $ (s \, t) \, u $ となる。
 
 また、抽象の本体はできる限り右側へと拡大する。
-例えば $ \lambda x . \;  \lambda y . \; x \, y \, x $ は $ \lambda x . (\lambda . y ((x \, y) \, x)) $ となる。
+例えば $ \lambda x . \;  \lambda y . \; x \, y \, x $ は$ \lambda x . (\lambda . y ((x \, y) \, x)) $ となる。
 
 ラムダ計算には変数のスコープが存在する。
 抽象 $ \lambda x . t $ の本体 $ t $ の中に変数 $ x $ がある時、 $ x $ の出現は束縛されていると言う。
@@ -954,7 +953,7 @@
     \BinaryInfC{$\vdash (\lambda x : Bool . x) \; true : Bool $}
 \end{prooftree}
 
-純粋型付きラムダ計算の型システムにおいて、閉じた項に対して進行定理と保存定理は成り立つ\ref{Pierce:2002:TPL:509043}\ref{pierce2013型システム入門プログラミング言語と型の理論}。  % FIXME: 進行定理と保存定理の証明。
+純粋型付きラムダ計算の型システムにおいて、閉じた項に対して進行定理と保存定理は成り立つ\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。  % FIXME: 進行定理と保存定理の証明。
 閉じた項、という制限が付いているのは $ f \; true $ といった自由変数が存在する項は正規形ではあるが値でないからである。
 しかし、開いた項に関しては評価が行なえないために型システムの検査対象に含まれない。