λ計算で並列論理和が定義できないことの初等的証明 - sumiiのブログ自分自身の研究テーマの一つであるプログラム等価性の証明法について、とある研究者とメールのやり取りをしていたら、λ計算で並列論理和が定義できないことの証明らしきものを再発明してしまった（詳細は確認していません）。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のいずれかを使用」する場合に
