Papers/2017/atton-master: paper/type.tex comparison

comparison paper/type.tex @ 37:881bd1d12a45

Writing expression ...

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Sat, 28 Jan 2017 11:28:38 +0900
parents	34812c1b33c2
children	5d4097922243

comparison

equal deleted inserted replaced

-:34812c1b33c2
+:881bd1d12a45
 これらの振舞いが同じプログラムを実行した時に何かしらの意味であれば、結果としてその言語の実装の正しさを証明することに繋がる。
 まずはブール式のみの操作的意味論を定義する。
 \begin{definition}
+ブール値(B)
 構文
 \begin{align*}
 t ::=                             && \text{項}     \\
 true                              && \text{定数真} \\
 false                             && \text{定数偽} \\
 if \; t \; then \; t \; else \; t && \text{条件式}
 \end{align*}
-\end{definition}
-\begin{definition}
 値
 \begin{align*}
 v ::=                             && \text{値} \\
 true                              && \text{真} \\
 false                             && \text{偽}
 \end{align*}
-\end{definition}
-\begin{definition}
 評価
 \begin{align*}
 if \; true  \; then \; t_2 \; else t_3 \rightarrow t_2 && \text{(E-IFTRUE)}  \\
 if \; false \; then \; t_2 \; else t_3 \rightarrow t_3 && \text{(E-IFFALSE)} \\
 \AxiomC{$ t_1 \rightarrow t_1'$}
 \UnaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \rightarrow if \; t_1' \; then t_2 \; else \;t_3 $}
 \DisplayProof
 && \text{(E-IF)}
 \end{align*}
-\end{definition}
+\end{definition}
+評価の最終結果になりえる項である値は定数 $ true $ と $ false $ のみである。
+評価の定義は評価関係の定義である。
+評価関係 $ t \rightarrow t' $ は「$ t $ が1ステップで $ t' $ に評価される」と読む。
+直感的には抽象機械の状態が $ t $ ならば $ t' $ が手に入るという意味である。
+評価関係は3つあるが、2つは前提を持たないため、2つの公理と1つの規則から成る。
+1つめの規則 E-IFTRUE の意味は、評価の対象となる項の条件式が定数 $ true $ である時に、then 節にある $ t_2 $ を残して他の全ての項を捨てるという意味である。
+E-EIFFALSE も同様に条件式が $ false $ の時に $ t_3 $ のみを残す。
+3つ目の規則 E-IF は条件式の評価である。
+条件式 $ t $ が $ t'$ に評価されうるのならば then 節と else 節を変えずに条件部のみを評価する。
+評価の定義から分かることの中に、if の中の then節 と else 節は条件部より先に評価されないことがある。
+よって、この言語は条件式の評価に対し条件部から評価が優先されるという評価戦略を持つことが分かる。
+\begin{definition}
+推論規則のインスタンスとは、規則の結論や前提に対し、一貫して同じ項による書き換えを行なったものである。
+\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/ の時である。
+\begin{definition}
+1ステップ評価関係 $ \rightarrow $ とは、3つの評価の規則を満たす、項に関する最小の二項関係である。
+$ (t, \; t') $ がこの関係の元である時、「評価関係式 $ t \rightarrow t'$ は導出可能である」と言う。
+\end{definition}
+ここで「最小」という言葉が表れるため、評価関係式 $ t \rightarrow t'$ が導出可能である時かつその時に限り、その関係式は規則によって正当化される。
+すなわち評価関係式は公理 E-IFTRUE か E-IFFALSE 、前提が成り立つ時の E-IF のインスタンスとなる。
+与えられた評価関係式が導出可能であることを証明するには、葉が E-IFTRUE か E-IFFALSE であり、内部ノードのラベルが E-IF のインスタンスである導出木が示せれば良い。
+例えば以下の略記の元 $ if \; t \; then \; false \; then \; false  \rightarrow if \; u \; then \; false \; else \; false  $ の導出可能性は以下のような導出木によって示せる。
+\begin{itemize}
+\item $ s = if \; true \;  then \; false \; else \; false $
+\item $ t = if \; s \;     then \; true \;  else \; true $
+\item $ u = if \; false \; then \; true \;  else \; true $
+\end{itemize}
+\begin{prooftree}
+\AxiomC{}
+\RightLabel{E-IFTRUE}
+\UnaryInfC{ $ s  \rightarrow true $ }
+\RightLabel{E-IF}
+\UnaryInfC{ $ t  \rightarrow  u $}
+\RightLabel{E-IF}
+\UnaryInfC{ $ if \; t \; then \; false \; then \; false/ \rightarrow if \; u \; then \; false \; else \; false $}
+\end{prooftree}
+1ステップ評価関係は与えられた項に対して抽象機械の状態遷移を定義する。
+この時、機械がそれ以上ステップを進められない時にそれが最終結果となる。
+\begin{definition}
+正規形
+項 $ t $ が正規形であるとは、$ t \rightarrow t'$となる評価規則が存在しないことである。
+\end{definition}
+この言語において $ true $ や $ false $ は正規形である。
+逆に言えば、構文的に正しい if が用いられている場合は評価することが可能なため正規形ではない。
+極端に言えばこの言語における全ての値は正規形なのである。
+しかし、他の言語における値は一般的に正規形ではない。
+実のところ、値でない正規形は実行時エラーとなって表れる。
+実際にこの言語に整数を導入して値では無い正規形を確認していく。
 % {{{ 型なしラムダ計算
 \section{型なしラムダ計算}

Mercurial > hg > Papers > 2017 > atton-master

comparison paper/type.tex @ 37:881bd1d12a45