また 、 上 で は 2 + 3 の よう な 算術 を ラムダ 式 の 一部 として 用い た 。

2 + 3 など は 計算 可能 で ある から 、 もちろん ラムダ 計算 による 表現 が 可能 で ある 。

自然 数 を ラムダ 式 で 表現 する 方法 は いくつ か 異なる 手法 が 知ら れ て いる が 、 その 中 で もっとも 一般 的 な の は { 仮 リンク | チャーチ 数 | en | Church encoding # Church numerals }（ Church numerals ） と 呼ば れる もの で 、 以下 の よう に 定義 さ れ て いる 。

直感 的 に は 、 数 n は ラムダ 式 で は f という 関数 を もらっ て それ を n 回 適用 し た もの を 返す 関数 で ある 。

（ チャーチ の 提唱 し た 元々 の ラムダ 計算 は 、 ラムダ 式 の 引数 が 少なくとも 一 回 は 関数 の 本体 に 出現 し て い なく て は なら ない こと に なっ て い た 。

一般 に ラムダ 式 の 中 に β - 変換 できる 部分 式 が 複数 ある 場合 、 どこ から 評価 を 行う か によって 評価 の 経過 は 複数 存在 する 。

それら の 複数 の 経過 から さらに 評価 する こと によって 、 同じ ラムダ 式 を 得 られる 性質 を チャーチ・ロッサー 性 、 もしくは 合流 性 と 呼ぶ （ チャーチ・ロッサー の 定理 ） 。

また 、 ある ラムダ 式 から 一 回 の β - 簡約 によって 得 られ た 二つ の ラムダ 式 が 、 同じ ラムダ 式 に β - 変換 さ れる という 性質 は 弱 チャーチ・ロッサー 性 と 呼ば れる 。

チャーチ・ロッサー 性 は 本稿 で 取り扱っ て いる 型 無し ラムダ 計算 の 体系 で は 成立 する こと が 知ら れ て いる 。

しかし その他 の 体系 、 例えば 型 を 付け て 拡張 さ れ た ラムダ 計算 の 体系 など に関して は 、 必ずしも 成り立つ と は 限ら ない 。

ある 種 の ラムダ 計算 の 体系 で は 、 任意 の ラムダ 式 に対して β - 変換 の 停止 性 が 保証 さ れ て いる こと が ある 。

チャーチ・ロッサー 性 を 満たし 、 かつ 停止 性 を 持つ ラムダ 計算 の 体系 で は 、 ラムダ 式 を どの よう な 順序 で 評価 し て も 必ず 同じ 結果 に なる こと が わかる 。

強 正規 化 的 で あり 、 かつ 弱 チャーチ・ロッサー 性 を 持つ ラムダ 計算 の 体系 は チャーチ・ロッサー 性 を 持つ （{ 仮 リンク | ニューマン の 補題 | en | Newman ' s lemma }）。

型 無し ラムダ 計算 の 体系 で は 、 ある 式 の 停止 性 を 判断 する 事 は 決定 不能 で ある こと が 証明 さ れ て いる 。

ラムダ 計算 を コンピュータ 上 に 実装 する に は 、 関数 を 第 一 級 オブジェクト として 取り扱う 必要 が あり 、 これ は スタック ・ ベース の プログラミング 言語 において は 問題 と なっ て くる 。

ラムダ 計算 と 最も 密接 な 関係 を もつ プログラミング 言語 は 関数 型 言語 と 呼ば れる 諸 言語 で 、 本質 的 に は いくつ か の 定数 と データ 型 を 用い て ラムダ 計算 を 実装 し て いる 。

Lisp で は 関数 の 定義 に ラムダ 記法 の 一 変形 を 用い て おり 、 さらに 、 純 Lisp と 呼ば れる Lisp の サブ セット は ラムダ 計算 と 真に 等価 に なっ て いる 。

例えば 、 Eiffel の インライン ・ エージェント の 機能 を 用い た 以下 の コード は ラムダ 式 λ x . x * x （ 値呼び 出し ） に 相当 する オブジェクト を 表し て いる 。

ラムダ 計算 の チャーチ・ロッサー 性 は 、 評価 （ β - 簡約 ） を どの 順序 で 行っ て も 、 さらに は 同時に （ 並行 に ） 行っ て も よい こと を 意味 し て いる 。

（ より 詳しく いえ ば 、 ラムダ 計算 は 参照 透過 で ある 。