}は正規形を持たない。x.x}にベータ簡約されることになる。x.x}は正規形であるので、やはり矛盾。X}のようなラムダ式は存在しない。一般にラムダ式の中にβ-変換できる部分式が複数ある場合、どこから評価を行うかによって評価の経過は複数存在する。それらの複数の経過からさらに評価することによって、同じラムダ式を得られる性質をチャーチ・ロッサー性、もしくは合流性と呼ぶ(チャーチ・ロッサーの定理)。あるラムダ式から一回のβ-簡約によって得られた二つのラムダ式が、同じラムダ式にβ-変換されるという性質は弱チャーチ・ロッサー性と呼ばれる。チャーチ・ロッサー性を持つ体系は弱チャーチ・ロッサー性も持つが、逆は必ずしもなりたたない。チャーチ・ロッサー性は本稿で取り扱っている型無しラムダ計算の体系では成立することが知られている。その他の体系、例えば型を付けて拡張されたラムダ計算の体系などに関しては、必ずしも成り立つとは限らない。β-変換は停止しない(無限ループに陥る)場合がある。次の式を適用する場合には停止しない。...ある種のラムダ計算の体系では、任意のラムダ式に対してβ-変換の停止性が保証されていることがある。どのような順序でβ-変換を行ったとしてもβ-変換が停止する性質を強正規化性といい、β-変換の順序を上手く選んだ場合にβ-変換が停止する性質を弱正規化性という。チャーチ・ロッサー性を満たし、かつ停止性を持つラムダ計算の体系では、ラムダ式をどのような順序で評価しても必ず同じ結果になることがわかる。強正規化的であり、かつ弱チャーチ・ロッサー性を持つラムダ計算の体系はチャーチ・ロッサー性を持つ(ニューマンの補題(英語版))。型無しラムダ計算の体系では、ある式の停止性を判断する事は決定不能であることが証明されている。おいて、ラムダ計算が手続的な抽象化と手続き(サブプログラム)の適用のしくみを提供しているがために、多くのプログラミング言語がラムダ計算にその基礎を置いているとみることができるとしている。ラムダ計算をコンピュータ上に実装するには、関数を第一級オブジェクトとして取り扱う必要があり、これはスタック・ベースのプログラミング言語においては問題となってくる。これはFunarg問題(英語版)として知られている。ラムダ計算と最も密接な関係をもつプログラミング言語は関数型言語と呼ばれる諸言語で、本質的にはいくつかの定数とデータ型を用いてラムダ計算を実装している。Lispでは関数の定義にラムダ記法の一変形を用いており、さらに、純Lispと呼ばれるLispのサブセットはラムダ計算と真に等価になっている。関数を第一級オブジェクトとして扱えるのは関数型言語だけというわけではない。Pascalなど、多くの命令型言語ではある関数を他の関数の引数として与える操作が許されている。CやC++では関数を指すポインタやクラス型関数オブジェクトを用いて同じことが実現できる。このような機能はサブ関数が明示的に書かれている場合にのみ用いることができ、したがってこの機能がそのまま高階関数をサポートしていることにはならない。いくつかの手続的なオブジェクト指向言語では関数を任意の階数に書くことができる。Smalltalkや、より最近の言語ではEiffel(エージェント)やC#(デリゲート)などで用意されている機能がそれである。(値呼び出し)に相当するオブジェクトを表している。このオブジェクトは他のあらゆるオブジェクトと同様に、変数に代入したり関数に渡したりすることができる。ここでの引数はタプルであるとみなされる。並行性編集ラムダ計算のチャーチ・ロッサー性は、評価(β-簡約)をどの順序で行っても、さらには同時に(並行に)行ってもよいことを意味している。(より詳しくいえば、ラムダ計算は参照透過である。)このため、ラムダ計算を用いて種々の非決定的評価戦略をモデル化することができる。Computingにある項目の資料が元になっている。3.0のもとで利用可能です。プライバシーデスクトップ。