Mercurial > hg > Papers > 2018 > nozomi-master
diff paper/type.tex @ 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 |
line wrap: on
line diff
--- 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 $ といった自由変数が存在する項は正規形ではあるが値でないからである。 しかし、開いた項に関しては評価が行なえないために型システムの検査対象に含まれない。