eval の設計

設計目標

eval は文献や下流パッケージで言及される簡約戦略に名前を与え、rewrite の単一ステップ機構を通じて任意の規則上でそれらを実行する。戦略の選択は、別の関数を呼ぶことではなく、保存・比較・表示できる値であるべきである。

数学的背景

戦略は任意の規則 $r$ に対して定義される。古典的な結果はラムダ計算の β 規則 $(\lambda x.\,b)\,a \to_\beta b[x := a]$ について述べられており、そこでは Apply をカリー化されたスパイン、Bind を $\lambda$ と読む。

簡約文脈

戦略は、簡約基を縮約してよい文脈と、それらの間の順序によって記述される。穴を $\Box$ と書く：

$$\begin{aligned} \text{full:}\qquad C &::= \Box \;\mid\; \lambda x.\,C \;\mid\; C(\bar u) \;\mid\; t(u_0, \dots, C, \dots, u_n), \\ \text{weak head:}\qquad H &::= \Box \;\mid\; H(\bar u). \end{aligned}$$

• 正規順序 は、すべての完全な文脈 $C$ の中で最左最外の簡約基を縮約する。
• 適用順序 は、すべての完全な文脈 $C$ の中で最左最内の簡約基を縮約する。
• 弱頭部 簡約は、根に簡約基があればそれを縮約し、なければヘッド位置 $H$ のみを探す。束縛子や引数の中には決して入らない。

弱頭部簡約が β 簡約基を見つけない項は弱頭部正規形である：抽象 $\lambda x.\,t$、またはヘッド $h$ が変数か値であるスパイン $h\,u_1 \cdots u_n$ である。

β に関する古典的な結果

標準化と正規化。 項が β 正規形をもつならば、正規順序簡約はそこに到達する。¹1 Curry と Feys、Combinatory Logic I、1958。Barendregt、The Lambda Calculus、定理 13.2.2 も参照。 したがって正規順序は正規化戦略であり、これがラムダ計算パッケージの既定である理由である。

適用順序は正規化的ではない。 $\Omega = (\lambda w.\,w\,w)(\lambda w.\,w\,w)$ とする。これは自分自身にしか簡約されない。$t = (\lambda x.\,y)\,\Omega$ について：

$$\begin{aligned} \text{normal order:}\quad & (\lambda x.\,y)\,\Omega \;\to_\beta\; y && \text{root redex is outermost,}\\ \text{applicative order:}\quad & (\lambda x.\,y)\,\Omega \;\to_\beta\; (\lambda x.\,y)\,\Omega \;\to_\beta\; \cdots && \Omega \text{ is innermost.} \end{aligned}$$

一致性。 β 簡約は合流的（Church–Rosser）であるので、二つの戦略がともに β 正規形に到達するならば、それらの正規形は α同値である。²2 Church と Rosser、“Some properties of conversion”、Transactions of the AMS 39、1936。 戦略は停止しないことはあり得るが、異なる正規形を生み出すことはない。

弱頭部簡約 は、弱頭部正規形が存在すればそれを計算する。これは名前呼び言語および utlc/nbe の遅延評価器の評価順序である。

設計上の決定

列挙型としての戦略

問題。 呼び出し側は戦略を選択・記録・比較する必要がある。たとえば二つの戦略を互いに照合するテストなどである。

選択肢。 ステップ関数を渡す。トレイトオブジェクトを渡す。列挙型から選ぶ。

選択。 Strategy は Eq と Debug をもつ単純な列挙型であり、reduce_once によって解釈される。独自の戦略も引き続き可能である：任意のステップ関数を @rewrite.normalize や @rewrite.trace に直接渡せる。列挙型は名前付きの戦略のみを扱う。

各戦略は rewrite の一つの走査である

$$\begin{aligned} \texttt{NormalOrder},\ \texttt{FullNormal} &\;\mapsto\; \texttt{top\_down\_once} && \text{(pre-order: leftmost-outermost)},\\ \texttt{ApplicativeOrder} &\;\mapsto\; \texttt{bottom\_up\_once} && \text{(post-order: leftmost-innermost)},\\ \texttt{WeakHead} &\;\mapsto\; \text{root, then head of } \texttt{Apply}, \text{ recursively}. \end{aligned}$$

前順探索は、他のどの簡約基にも含まれない最初の簡約基を返す。ヘッドを引数より先に、引数は左から右へ走査する。これは最左最外の簡約基であり、rewrite の設計 の正規形補題により NoStep は「正規形である」ことを意味する。後順探索は他の簡約基を含まない簡約基、すなわち最左最内のものを返す。弱頭部探索はスパインのみをたどるので、その NoStep は「弱頭部正規形である」ことのみを意味し、それ以上の意味はない。

evaluate と trace は独自の簡約ロジックを追加しない：戦略のステップ関数を @rewrite.normalize と @rewrite.trace に渡すだけである。その結果、すべての戦略がトレースをもち、ステップ数の契約はすべての戦略で同じになる。

独立した名前としての FullNormal

現在 FullNormal は NormalOrder と同じ走査に対応している。違いは意図にある：NormalOrder はステップの順序（最左最外）を約束し、FullNormal は完全な正規形のみを約束する。二つの名前を保つことで、NormalOrder の意味を変えずに、将来 FullNormal をより高速な完全正規化器に置き換えられる。

正しさ / 不変条件

• reduce_once はすべての戦略について rewrite の単一簡約基契約を満たす。WeakHead のステップで報告される経路は ApplyHead フレームのみからなる。
• NormalOrder、FullNormal、ApplicativeOrder では、NoStep は規則がどこにも適用できないことを意味する。WeakHead では、ヘッドスパイン上のどこにも適用できないことを意味する。
• β 規則のもとで、β 正規形をもつすべての $t$ に対し、$k$ が正規順序簡約の長さ以上であれば、evaluate(t, _, beta, NormalOrder, k) は NormalForm を返す（正規化定理）。
• 合流的な規則に対して二つの戦略がともに NormalForm を返すならば、それらの項は α同値である（Church–Rosser）。

ライブラリのテストは、名前付きと De Bruijn の β ステップを互いに照合し（src/utlc/lambda/lambda_test.mbt）、正規順序を NbE 正規化器と照合する（src/utlc/nbe/nbe_test.mbt）。

却下した代替案

• 値への値呼び評価。 通常の値呼び戦略は束縛子の下で簡約せず、抽象を値として扱う。これは独自のステップ関数として表現できるが、パッケージが必要とする完全戦略やヘッド戦略の一つではないため、列挙型には含まれない。
• 束縛子の下での頭部簡約。 頭部簡約（外側の束縛子の下で $\lambda \bar x.\,(\lambda y.\,b)\,a\,\bar u$ を簡約すること）は独自のステップ関数として書ける。列挙型は実際に使われる戦略に限っている。
• 戦略固有の結果型。 すべての戦略は NormalizationResult を共有するので、呼び出し側はコードを変えずに戦略を切り替えられる。

境界

• 戦略は位置を選ぶだけであり、名前替え・共有・メモ化は一切行わない。繰り返し現れる部分項は別々に簡約される。
• 値呼び、必要呼び、頭部戦略は名前付きのケースとしては提供されない。
• 停止性は max_steps によって制限されるのであって、判定されるわけではない。
• eval は Term[T] のみを扱う。下流の AST はトップダウンの @rewrite.generic_normalize を使う。

Footnotes

1. Curry と Feys、Combinatory Logic I、1958。Barendregt、The Lambda Calculus、定理 13.2.2 も参照。 ↩

2. Church と Rosser、“Some properties of conversion”、Transactions of the AMS 39、1936。 ↩