計算理論・ラムダ計算の問題
型なしラムダ計算を考える。適用は左結合（）、抽象は右に最大限のびるものとし、 同値な項は同一視する。簡約は 簡約のみを考える（ 簡約は考えない）。 以上の整数 に対してチャーチ数を
で定める。
正規順序戦略とは、各ステップで、項に含まれる 基（ の形の部分項）のうち最も左外側にあるもの（項を文字列として書いたときに、その 基の先頭が最も左にあるもの）を 1 回だけ縮約する戦略である。
項 から出発して正規順序戦略で 簡約を繰り返すと、有限回で 正規形に到達する。正規形に到達するまでに行われる 簡約の回数（ステップ数）を求めよ。
この問題で使うもの
- β 簡約と β 正規形（説明と入口の問題）
- チャーチ数と対による計算（説明と入口の問題）
ヒント
行き詰まったら、上から順に 1 つずつ開いてください。
ヒント 1
正規順序では、項の先頭（頭部）にある 基を常に優先します。適用 で が抽象でなければ 自体は 基ではないので、まず の中を簡約します。先頭が変数になったら、その引数を左から順に簡約します。
ヒント 2
を使います。、 とおくと、1 ステップ目で 、2 ステップ目で になります。
ヒント 3
を縮約して先頭の 基を処理すると、4 ステップ目で になります。 を 1 つ処理するのに 2 ステップかかることに注意して、残りの と の分を数えましょう。
答えと解説
答えを見る
どこでつまずきましたか？（選ぶと、戻る場所を案内します）
解説を読む
記号を簡単にするため 、 とおく。 である（ は新しい変数）。各ステップで最も左外側の 基を縮約する。
(1) 全体が 基なので
(2) 本体 は 基なので 。
(3) 本体 は、 が抽象ではなく適用なので 基ではない。最も左の 基は先頭の で、。
(4) 先頭が 基になったので 。
(5) 先頭の を縮約して 。
(6) 。
(7) 先頭は変数 なので、引数の中で最も左の 基である を縮約して 。
(8) 。
(9) の中の を縮約して （ は の略記）。
(10) 。
(11) を縮約して 。
(12) 。
(13) を縮約して 。
(14) 。
最後の項 は 基を含まないので 正規形であり、 同値のもとで に等しい。これは の正規形が であることと合っている。
よって、正規形に到達するまでのステップ数は である。
別解
とおく。正規順序で、各ステップの最も左外側の β 基を縮約する。
1.
2. 本体の最も外側の基 を縮約する。ここで とおく。結果は
3. 先頭にある基 を縮約する。結果は
4. 外側の基を縮約する。結果は
5.
6.
7. 内側の
8. 。これで全体は
9.
10.
11.
12.
13.
14.
最終項は で、 と一致する。正規形に到達するまでのステップ数は 14 である。