計算理論・ラムダ計算の問題
型なしラムダ計算を考える。適用は左結合()、抽象は右に最大限のびるものとし、 同値な項は同一視する。簡約は 簡約のみを考える( 簡約は考えない)。 は変数とする。
項
の 正規形として正しいものを、次のア〜オから 1 つ選べ。
ア
イ
ウ
エ
オ は 正規形をもたない
この問題で使うもの
- β 簡約と β 正規形(説明と入口の問題)
ヒント
行き詰まったら、上から順に 1 つずつ開いてください。
ヒント 1
技能「β 簡約と β 正規形」を使います。まず外側の を 簡約しますが、代入する項 の自由変数に注意しましょう。
ヒント 2
の中の は自由変数です。代入先 の束縛変数 に捕獲されないよう、先に と名前を替えてから代入します。
ヒント 3
1 回目の簡約で が得られます。残っている redex を簡約しましょう。
答えと解説
答えを見る
イ
どこでつまずきましたか?(選ぶと、戻る場所を案内します)
解説を読む
手順 1: 自由変数・束縛変数を確認する。
の形で、、 である。 の中で は束縛変数、 は自由変数である。一方 の中では は に束縛されている。
手順 2: 捕獲を避けて代入する。
簡約 を行う。そのまま を に置き換えると となり、 の自由変数 が に捕獲されてしまう(意味が変わる)。そこで先に の束縛変数 を新しい変数 に 変換しておく:
これに代入して
手順 3: 残っている redex を簡約する。
は redex で、 である( は の中の束縛変数と衝突しないので名前替えは不要)。よって
手順 4: 正規形か確かめる。
には の形の部分項(redex)がないので 正規形である。
なお、ア は手順 2 で名前替えをせずに を捕獲してしまったときに得られる誤りであり、ウは引数の順序を取り違えたもの、エは を誤って消したものである。 は 2 回の簡約で正規形に達するのでオも誤り。
したがって答えは イ である。
別解
において、引数 の は自由変数である。 の本体に代入すると束縛変数 に捕獲されるので、まず 変換して とする。
。
これ以上 簡約できる部分( の形)はないので 正規形である。
選択肢の検討:
ア : 自由な が捕獲された誤った結果で、誤り。
イ : 上の結果と 同値ではないが一致しており、正しい。
ウ : に代入される順序が逆で、誤り。
エ : 抽象が消えており、 簡約も考えないので誤り。
オ: 正規形をもつので誤り。
検算: を 簡約の逆向きにたどると、 に戻り、 の簡約と一致する。