# HG changeset patch # User atton # Date 1485755641 -32400 # Node ID 45d3ac176bf5961d359eff157599058656bb8492 # Parent 3aeabd46d72b2a88e1621ff43faf0446bf8ceffd Mini fixes diff -r 3aeabd46d72b -r 45d3ac176bf5 paper/cbc.tex --- 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 と呼ばれている。 diff -r 3aeabd46d72b -r 45d3ac176bf5 paper/type.tex --- 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 $ といった自由変数が存在する項は正規形ではあるが値でないからである。 しかし、開いた項に関しては評価が行なえないために型システムの検査対象に含まれない。