背景

ラムダ項の最長リダクション戦略については、図2.1に示すようにかなりのことが分かっている。図において斜線部 分は最長リダクション戦略が知られていることを表している。弱正規性(WN)を持たないラムダ項では、どのように リダクションを行っても正規形とはならないことから、全てのリダクション戦略が最長となる。弱正規性は持つが強 正規性を持たないラムダ項では、perpetualなリダクション戦略が無限のリダクションとなる、すなわち最長となるこ とが知られている([1]参照)。perpetualなリダクション戦略としては、F_∞やcall–by–value等がある。そして型付ラ ムダ項やラムダ項の展開でも、F_∞リダクション戦略が最長である([35],[36]参照)。つまり、今まで分かっているとこ ろでは、F_∞リダクション戦略が全ての場合において最長である。そのため、図2.1の空白部分でも、F_∞リダクショ ン戦略が最長となるのではないかと予想される。

F_∞ F_∞

λ-Term

Typedλ Development WN

SN

All

Perpetual(F_∞, Call-by-Value, etc.)

図2.1: 最長リダクション戦略

ここで、F_∞リダクション戦略を示しておこう。それは次のようなものである。

定義2.1.1 (F_∞リダクション戦略) Mを正規形ではないラムダ項とする。1ステップのF_∞リダクション戦略の結果 をF_∞(M)で表すとする。

1. M ≡(λx.M₁)M₂のとき。

(a) x∈FV(M₁)のとき。

F_∞(M)≡[M₂/x]M₁ (b) x∈FV(M₁)のとき。

i. M₂が正規形でないとき。

F_∞(M)≡(λx.M₁)F_∞(M₂) ii. M₂が正規形のき。

F_∞(M)≡[M₂/x]M₁ 2. M ≡λx.M₁のとき。

F_∞(M)≡λx.F_∞(M₁)

3. M ≡M₁M₂で、M₁M₂自身はレデックスでないとき。

(a) M₁が正規形でないとき。

F_∞(M)≡F_∞(M₁)(M₂) (b) M₁が正規形のき。

F_∞(M)≡(M₁)F_∞(M₂)

つまり、リダクションをしてラムダ項が消える場合には、代入項が正規形になってからそのレデックスをリダクショ ンするが、消えない場合には、そこからリダクションするという戦略である。

このとき最長リダクションに関する次の3つの定理が成り立つ。証明については、それぞれ[1],[35],[36] を参照の こと。

定理2.1.2 (perpetualな戦略) M を強正規性を持たないラムダ項とする。このとき、F_∞リダクション戦略は無限 列となる。

定理2.1.3 (ラムダ項の展開における最長リダクション戦略) M をλ項とする。このとき、βリダクションにおいて F_∞リダクション戦略は最長となる。

定理2.1.4 (型付きラムダ項における最長リダクション戦略) Mを型付きラムダ項とする。このとき、F_∞リダクショ

ン戦略は最長となる。

では、最短リダクション戦略はどうであろうか。[15]によれば次の定理がなりたつ。

定理2.1.5 最左完全並行リダクションは最短リダクションである。

最左完全並行リダクションは並行リダクションの一つであり、最左レデックスをリダクションするが、そのときにコ ピーされたレデックスも同時にリダクションするものである。この並行リダクションはリダクションを越えたもので あるが、最左完全並行リダクションでコピーが生じない場合はリダクションに一致する。すなわち次の系が直ちに成 り立つ。

系 2.1.6 BCK’–ラムダ項では最左リダクションが最短リダクションである。

ここでBCK’–ラムダ項は次のようなラムダ項である。

定義2.1.7 (BCK’–ラムダ項) 1. xが変数⇒ xはBCK–ラムダ項

2. M₁, M₂がBCK–ラムダ⇒(M₁M₂)はBCK–ラムダ項

3. M がBCK–ラムダ項でありxが変数で、xがM に高々1つしか自由出現しない ⇒(λx.M)はBCK–ラムダ項 すなわち、リダクションを行ってもラムダ項がコピーされないようなラムダ項である。

以上を図示すると図2.2になる。弱正規性を持たないラムダ項では、どのようにリダクションをしても正規形に辿り 着かないため、つまり全てのリダクション戦略が最短である。

λ-Term

Typedλ Development

leftmost

WN SN

All

BCK’

図2.2: 最短リダクション戦略

ラムダ項が弱正規性を持てば、幅優先探索により最短リダクション戦略を求めることは可能である。しかしながら、

その場合は実際にリダクションを行うかそれ以上の手間がかかり実効的¹とはいえない。我々が欲しいのは実効的なリ ダクション戦略である。

1ここでいう実効的とは実際にリダクションを行うよりは簡単に見い出せるということである。[1]には「比較的簡単に」というあいまいな表現 で定義されている。

本章では、ラムダ項の展開において実効的な最短リダクション戦略を与える。同じ証明手法をBCK–ラムダ項に適 用し、BCK–ラムダ項に対する最短リダクション戦略の別証明を与える。