λ計算で並列論理和が定義できないことの初等的証明
自分自身の研究テーマの一つであるプログラム等価性の証明法について、とある研究者とメールのやり取りをしていたら、λ計算で並列論理和が定義できないことの証明らしきものを再発明してしまった（詳細は確認していません）。Mitchellの教科書(Foundations for Programming Languages)に同様の証明があることに後から気づいた…
簡単のため、名前呼びλ計算＋論理値プリミティブで考える。一般に、任意のλ項Cについて、次のいずれかが成立する。証明はCの構文と（簡約が停止する場合は）簡約列の長さに関する帰納法による。
- あるλ項Dと変数xiが存在して、xiはDの簡約位置にあり、任意のλ項M1,...,Mnについて、[M1/x1,...,Mn/xn]C →* [M1/x1,...,Mi/xi,...,Mn/xn]D （直観としては「M1,...,Mnのいずれかを使用」する場合に相当）
- ある値Vが存在して、任意のM1,...,Mnについて、[M1/x1,...,Mn/xn]C →* [M1/x1,...,Mn/xn]V （M1,...,Mnのいずれも使用せず簡約が停止する場合に相当）
- あるC'が存在して、任意のM1,...,Mnについて、[M1/x1,...,Mn/xn]C →* [M1/x1,...,Mn/xn]C'
かつC'は値でない （M1,...,Mnを使用せず簡約がstuck）
- 任意のM1,...,Mnについて、[M1/x1,...,Mn/xn]C →∞ （M1,...,Mnを使用せず発散）
仮にC = por(x1,x2)が存在したとする。上の1.の場合、por(,true)かpor(true,
)のいずれかの簡約が停止せず、porの定義に矛盾。2.の場合、por(true,true) →* trueかつpor(false,false) →* falseというporの定義に矛盾。3., 4.の場合もporの定義に矛盾。
