ラムダ計算

数理論理学において、ラムダ計算（ λ計算とも表記される）は、変数束縛と置換を用いて関数の抽象化と適用に基づく計算を表現する形式体系である。本稿の主題である型なしラムダ計算は、汎用機械、すなわち任意のチューリングマシンをシミュレートできる（そしてその逆も可能な）計算モデルである。これは、数学者アロンゾ・チャーチが1930年代に数学の基礎に関する研究の一環として導入したものである。チャーチは1936年に論理的に一貫性のある定式化を発見し、1940年にそれを文書化した。

ラムダ計算は、形式構文によって定義されるラムダ項の言語と、それらの項を操作するための変換規則のセットから構成されます。BNFでは、構文は次のようになります。${\displaystyle e::=x\mid \lambda x{\text{.}}e\mid e\,e,}$変数${\displaystyle x,y,z}$無限個の名前の範囲。用語${\displaystyle M,N,t,s,e,f}$すべてのラムダ項にわたる範囲。これは次の帰納的定義に対応します。

• 変数​${\displaystyle x}$は有効なラムダ式です。
• 抽象化とはラムダ項のことである${\displaystyle (\lambda x{\text{.}}t)}$どこ${\displaystyle t}$はラムダ式であり、抽象化の本体と呼ばれ、${\displaystyle x}$は抽象化のパラメータ変数です。
• アプリケーションはラムダ項です${\displaystyle (t\,s)}$どこ${\displaystyle t}$そして${\displaystyle s}$ラムダ式です。

ラムダ項は、以下の3つの規則を繰り返し適用することで得られる場合に構文的に有効です。便宜上、ラムダ項を記述する際に括弧を省略できる場合が多くあります。詳細は「ラムダ計算の定義 § 表記法」を参照してください。

ラムダの用語では、何らかの囲み関数のパラメータではない変数の出現は、${\displaystyle \lambda }$は無料であると言われています。${\displaystyle x}$学期中${\displaystyle M}$に縛られている${\displaystyle \lambda x{\text{.}}M}$. 内の他の変数の任意の自由な出現${\displaystyle M}$自由のまま${\displaystyle \lambda x{\text{.}}M}$。

例えば、この用語では${\displaystyle x\,y}$、 両方${\displaystyle x}$そして${\displaystyle y}$無料で発生します。${\displaystyle (\lambda x{\text{.}}x\,y)}$、${\displaystyle y}$無料ですが、${\displaystyle x}$本体（つまりドットの後）は自由ではなく、（パラメータに）束縛されていると言われます。${\displaystyle y}$無料です${\displaystyle (\lambda x{\text{.}}x\,y)}$、それは${\displaystyle (\lambda y{\text{.}}\lambda x{\text{.}}x\,y)}$2 回出現します${\displaystyle x}$で${\displaystyle (\lambda y{\text{.}}(\lambda x{\text{.}}x\,y)\,x)}$―一方は束縛され、もう一方は自由である。

${\displaystyle \operatorname {FV} (M)}$は自由変数の集合です${\displaystyle M}$つまり、自由変数として出現する変数${\displaystyle M}$少なくとも一度は。帰納的に以下のように定義できる。

• ${\displaystyle \operatorname {FV} (x)=\{x\}}$
• ${\displaystyle \operatorname {FV} (M_{1}M_{2})=\operatorname {FV} (M_{1})\cup \operatorname {FV} (M_{2})}$
• ${\displaystyle \operatorname {FV} (\lambda x{\text{.}}M)=\operatorname {FV} (M)\backslash \{x\}}$

表記法${\displaystyle M[x:=N]}$キャプチャ回避置換を表す：置換${\displaystyle N}$自由発生ごとに${\displaystyle x}$で${\displaystyle M}$変数キャプチャを回避しながら。^{[ a ]}この操作は、以下のように帰納的に定義されます。

• ${\displaystyle x[x:=N]=N}$;${\displaystyle y[x:=N]=y}$もし${\displaystyle y\neq x}$。
• ${\displaystyle (M_{1}M_{2})[x:=N]=(M_{1}[x:=N])(M_{2}[x:=N])}$。
• ${\displaystyle (\lambda y{\text{.}}M)[x:=N]}$3つのケースがあります。
  • もし${\displaystyle y=x}$、${\displaystyle \lambda x{\text{.}}M}$（${\displaystyle x}$拘束されている（変更なし）。
  • もし${\displaystyle y\notin \operatorname {FV} (N)}$、${\displaystyle \lambda y{\text{.}}(M[x:=N])}$。
  • もし${\displaystyle y\in \operatorname {FV} (N)}$、最初のαリネーム${\displaystyle \lambda y{\text{.}}M}$に${\displaystyle \lambda y'{\text{.}}M[y:=y']}$と${\displaystyle y'}$名前の衝突を避けるために新たに作成し、その後上記の手順を続けます。${\displaystyle \lambda y'{\text{.}}M[y:=y'][x:=N]}$と${\displaystyle y'\notin \operatorname {FV} (M)\cup \operatorname {FV} (N)}$。

ラムダ項を同等のラムダ項に還元することを可能にする「等価性」と「還元」の概念がいくつか存在する。^{[ 3 ]}

• α変換は、抽象化における束縛変数の特定の選択は（通常）重要ではないという直感を捉えています。${\displaystyle y\notin \operatorname {FV} (M)}$すると、その条件は${\displaystyle \lambda x{\text{.}}M}$そして${\displaystyle \lambda y{\text{.}}M[x:=y]}$アルファ等価とみなされ、${\displaystyle \lambda x{\text{.}}M\equiv _{\alpha }\lambda y{\text{.}}M[x:=y]}$同値関係は、この規則によって生成されるラムダ項に関する最小の合同関係です。例えば、${\displaystyle \lambda x{\text{.}}x}$そして${\displaystyle \lambda y{\text{.}}y}$これらはアルファと等価なラムダ項である。
• β還元規則は、β還元、形式の適用について述べている。${\displaystyle (\lambda x{\text{.}}t)s}$、次の項に簡略化されます。${\displaystyle t[x:=s]}$[ ^{b ]}例えば、すべて^の${\displaystyle s}$、${\displaystyle (\lambda x{\text{.}}x)s\to x[x:=s]=s}$これは、${\displaystyle \lambda x{\text{.}}x}$まさにアイデンティティです。同様に、${\displaystyle (\lambda x{\text{.}}y)s\to y[x:=s]=y}$これは、${\displaystyle \lambda x{\text{.}}y}$定数関数です。
• η変換は外延性を表現し、変換を行う${\displaystyle \lambda x{\text{.}}fx}$そして${\displaystyle f}$いつでも${\displaystyle x}$無料には表示されません${\displaystyle f}$ラムダ計算に関する多くの解説では、しばしば省略されている。

還元式(redex)とは、還元規則のいずれかによって還元できる部分項を指します。例えば、${\displaystyle (\lambda x{\text{.}}M)\,N}$は置換を表現するβ-レデックスである${\displaystyle N}$のために${\displaystyle x}$で${\displaystyle M}$. redex が還元される式をその還元式と呼び、${\displaystyle \lambda x{\text{.}}M\,N}$は${\displaystyle M[x:=N]}$。

ラムダ計算はチューリング完全であり、つまり、あらゆるチューリングマシンをシミュレートするために使用できる普遍的な計算モデルです。^{[ 4 ]}その名前の由来であるギリシャ文字のラムダ（λ）は、関数内の変数を束縛することを示すためにラムダ式とラムダ項で使用されます。

ラムダ計算は、型なしまたは型ありのいずれかです。型付きラムダ計算では、関数は、与えられた入力の「型」のデータを受け入れることができる場合にのみ適用できます。型付きラムダ計算は、型なしラムダ計算よりも厳密に弱いです。型なしラムダ計算は、型なしラムダ計算よりも表現できるものが少ないという意味で、この記事の主な主題です。一方、型付きラムダ計算では、より多くのことを証明できます。たとえば、単純型付きラムダ計算では、すべての評価戦略はすべての単純型付きラムダ項に対して終了するという定理があります^{[ 5 ]} 。一方、型なしラムダ項の評価は終了する必要はありません（下記参照）。型付きラムダ計算が数多く存在する理由の一つは、型なしラムダ計算でできることの多くを実現しつつ、ラムダ計算に関する強力な定理を証明できる能力を放棄したくないという願望があるからだ。

ラムダ計算は、数学、哲学^{[ 6 ]} 、言語学^{[ 7 ] [ 8 ]}、コンピュータ科学^{[ 9 ] [ 10 ]}など、さまざまな分野で応用されています。ラムダ計算は、プログラミング言語の理論の発展において重要な役割を果たしてきました。関数型プログラミング言語はラムダ計算を実装しています。ラムダ計算は、圏論における現在の研究テーマでもあります^{[ 11 ]}。

ラムダ計算は、数学の基礎に関する研究の一環として、1930年代に数学者アロンゾ・チャーチによって導入されました。^{[ 12 ] [ c ]}元のシステムは、1935年にスティーブン・クリーネとJB・ロッサーがクリーネ・ロッサーのパラドックスを提唱した際に、論理的に矛盾していることが示されました。^{[ 13 ] [ 14 ]}

その後、1936年にチャーチは計算に関連する部分だけを分離して発表し、現在では型なしラムダ計算と呼ばれているものを発表した。^{[ 15 ]} 1940年には、計算能力は劣るものの論理的に一貫性のあるシステムも導入し、これは単純型付きラムダ計算として知られている。^{[ 16 ]}

プログラミング言語との関係が明確になった1960年代までは、ラムダ計算は単なる形式体系に過ぎませんでした。リチャード・モンタギューをはじめとする言語学者たちが自然言語の意味論に応用したおかげで、ラムダ計算は言語学^{[ 17 ]とコンピュータ科学[ 18 ]}の両方で確固たる地位を築き始めました。

計算可能な関数は、コンピュータ科学と数学における基本的な概念です。ラムダ計算は、計算の性質を形式的に研究するのに役立つ、計算のためのシンプルな意味論を提供します。ラムダ計算は、その意味論をシンプルにする2つの簡略化を取り入れています。 最初の簡略化は、ラムダ計算では関数を「匿名」に扱い、明示的な名前を付けないということです。たとえば、関数

${\displaystyle \operatorname {square\_sum} (x,y)=x^{2}+y^{2}}$

匿名形式で書き直すと次のようになります。

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

（これは「タプル」と読みます）${\displaystyle x}$そして${\displaystyle y}$マッピング先​${\textstyle x^{2}+y^{2}}$「) ^{[ d ]}同様に、関数

${\displaystyle \operatorname {id} (x)=x}$

匿名形式で書き直すと次のようになります。

${\displaystyle x\mapsto x}$

入力は単純にそれ自身にマッピングされます。^{[ d ]}

2つ目の簡略化は、ラムダ計算では単一の入力の関数のみを使用するという点です。例えば、2つの入力を必要とする通常の関数は、${\textstyle \operatorname {square\_sum} }$関数は、単一の入力を受け取り、出力として別の関数を返す同等の関数に書き換えることができ、その関数もまた単一の入力を受け取ります。たとえば、

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

再加工して

${\displaystyle x\mapsto (y\mapsto (x^{2}+y^{2}))}$

この手法はカリー化と呼ばれ、複数の引数を取る関数を、それぞれが単一の引数を取る関数の連鎖に変換する。

機能の適用${\textstyle \operatorname {square\_sum} }$関数を引数 (5, 2) に渡すと、すぐに

${\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}$

${\textstyle =5^{2}+2^{2}}$

${\textstyle =29}$、

一方、カレー風味バージョンの評価にはもう1つのステップが必要となる。

${\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}$

${\textstyle =(y\mapsto 5^{2}+y^{2})(2)}$// 定義${\displaystyle x}$使用されてきた${\displaystyle 5}$内部表現において。これはβ還元に似ています。

${\textstyle =5^{2}+2^{2}}$// 定義${\displaystyle y}$使用されてきた${\displaystyle 2}$これもまた、β還元と同様である。

${\textstyle =29}$

同じ結果にたどり着く。

ラムダ計算では、関数は「第一級の値」とみなされるため、関数は入力として使用することも、他の関数からの出力として返すこともできます。例えば、ラムダ項${\displaystyle \lambda x.x}$恒等関数を表す。${\displaystyle x\mapsto x}$。 さらに遠く、${\displaystyle \lambda x.y}$定数関数を表す${\displaystyle x\mapsto y}$常に返す関数${\displaystyle y}$入力に関係なく。関数に対して作用する関数の例として、関数合成は次のように定義できます。${\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))}$。

β還元はα変換まで合流的であることが示せる（つまり、2つの正規形が、一方を他方にα変換できる場合に等しいとみなされる）。チャーチ・ロッサーの定理によれば、与えられたラムダ項から始まり、最終的に終了する還元ステップの任意の特定のシーケンスは、同じβ正規形を生成する。しかし、書き換え規則としてのβ還元による型なしラムダ計算は、強く正規化も弱く正規化もせず、 Ωのような正規形を持たない項が存在する。

個々の項について考えると、強正規化項と弱正規化項はいずれも一意の正規形を持つ。強正規化項については、どのような縮約戦略を用いても必ず正規形が得られるが、弱正規化項については、一部の縮約戦略では正規形を見つけられない場合がある。

基本的なラムダ計算は、次のサブセクションi、ii、iii、および§ ivで示されているように、算術、ブール値、データ構造、および再帰をモデル化するために使用できます。

ラムダ計算には、数多くのプログラミング慣用表現が存在します。これらの多くは、もともとラムダ計算をプログラミング言語のセマンティクスの基盤として用いるという文脈で開発されたものであり、実質的にラムダ計算を低レベルプログラミング言語として利用しています。いくつかのプログラミング言語にはラムダ計算（あるいはそれに非常によく似たもの）が断片として含まれているため、これらの手法は実際のプログラミングでも利用されていますが、その場合、難解あるいは馴染みのないものとして認識される可能性があります。

型付きラムダ計算は、ラムダ記号 (${\displaystyle \lambda }$) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see Kinds of typed lambda calculi). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type.^[29]

Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages such as ML and Haskell and, more indirectly, typed imperative programming languages. Typed lambda calculi play an important role in the design of type systems for programming languages; here typability usually captures desirable properties of the program, e.g., the program will not cause a memory access violation.

Typed lambda calculi are closely related to mathematical logic and proof theory via the Curry–Howard isomorphism and they can be considered as the internal language of classes of categories, e.g., the simply typed lambda calculus is the language of a Cartesian closed category (CCC).^[30]

Whether a term is normalising or not, and how much work needs to be done in normalising it if it is, depends to a large extent on the reduction strategy used. Common lambda calculus reduction strategies include:^[31][32][33]

Normal order

The leftmost outermost redex is reduced first. That is, whenever possible, arguments are substituted into the body of an abstraction before the arguments are reduced. If a term has a beta-normal form, normal order reduction will always reach that normal form.

Applicative order

The leftmost innermost redex is reduced first. As a consequence, a function's arguments are always reduced before they are substituted into the function. Unlike normal order reduction, applicative order reduction may fail to find the beta-normal form of an expression, even if such a normal form exists. For example, the term ${\displaystyle (\;\lambda x.y\;\;(\lambda z.(zz)\;\lambda z.(zz))\;)}$ is reduced to itself by applicative order, while normal order reduces it to its beta-normal form ${\displaystyle y}$.

Full β-reductions

Any redex can be reduced at any time. This means essentially the lack of any particular reduction strategy—with regard to reducibility, "all bets are off".

Weak reduction strategies do not reduce under lambda abstractions:

Call by value

適用順序に似ていますが、抽象化内部では還元は行われません。これは、C言語のような厳密な言語の評価順序に似ています。関数の引数は関数呼び出し前に評価され、引数が代入されるまで関数本体は部分的にも評価されません。

名前で呼ぶ

通常の順序と同様ですが、抽象化内部では還元は実行されません。たとえば、λ x .(λ y . y ) xは、redex (λ y . y ) xを含みますが、この戦略によれば正規形です。

共有を用いた戦略は、並列処理において「同じ」計算を削減する。

最適な削減

通常の順序で行われますが、同じラベルを持つ計算は同時に削減されます。

必要に応じて呼び出し

名前による呼び出し（つまり弱い呼び出し）ですが、関数アプリケーションで用語が重複する場合は、代わりに引数に名前を付けます。引数は「必要に応じて」評価され、その時点で名前のバインディングが縮小された値で更新されます。これは、通常の順序での評価と比較して時間を節約できます。

任意の 2 つのラムダ式を入力として受け取り、一方の式が他方の式に還元されるかどうかに応じてTRUEまたはFALSEを出力するアルゴリズムは存在しません。 ^{[ 15 ]}より正確には、計算可能な関数ではこの問題を決定できません。これは、歴史的に決定不能性が証明された最初の問題でした。このような証明の場合、通常どおり、計算可能とは、チューリング完全な計算モデルによって計算可能であることを意味します。実際、計算可能性自体はラムダ計算によって定義できます。自然数の関数F : N → Nは、任意のペアx、y ∈ Nに対して、f ( x ) = yとなるようなラムダ式fが存在する場合に限り、計算可能な関数です。ここで、xとy_はそれぞれxとyに対応するチャーチ数であり、 = _βは β 還元との等価性を意味します。計算可能性とその等価性を定義する他のアプローチについては、チャーチ・チューリングのテーゼを参照してください。  

チャーチの計算不能性の証明は、まず与えられたラムダ式が正規形を持つかどうかを判定することに問題を帰着させる。次に、この述語は計算可能であり、したがってラムダ計算で表現できると仮定する。クリーネの以前の研究に基づき、ラムダ式のゲーデル数を構築することで、ゲーデルの第一不完全性定理の証明に非常に近いラムダ式eを構築する。eを自身のゲーデル数に適用すると、矛盾が生じる。

ラムダ計算の計算複雑性の概念は、β 縮約のコストが実装方法によって異なる可能性があるため、少し厄介です。^{[ 34 ]} 正確には、式E内の束縛変数Vのすべての出現位置を何らかの方法で見つける必要があり、これは時間コストを意味します。または、自由変数の位置を何らかの方法で追跡する必要があり、これは空間コストを意味します。E内のVの位置を単純に検索すると、 Eの長さnに対してO ( n )になります。ディレクター ストリングは、この時間コストを 2 乗の空間使用と交換する初期のアプローチでした。^{[ 35 ]}より一般的には、これは明示的な置換を使用するシステムの研究につながりました。

2014年に、通常の順序の縮約によって項を縮約するために要するβ縮約ステップの数が妥当な時間コストモデルであることが示されました。つまり、縮約はステップ数に比例する多項式時間でチューリングマシン上でシミュレートできます。^{[ 36 ]}これは、各β縮約でサイズが指数関数的に増加するラムダ項の存在によるサイズ爆発のため、長年の未解決問題でした。この結果は、コンパクトな共有表現を使用することでこれを回避します。この結果は、縮約中にラムダ項を評価するために必要なスペースの量が項のサイズに比例しないことを明らかにしています。スペース複雑性の適切な尺度が何であるかは現在わかっていません。^{[ 37 ]}

不合理なモデルが必ずしも非効率を意味するわけではありません。最適削減では、同じラベルを持つすべての計算を 1 つのステップで削減し、重複作業を回避しますが、与えられた項を正規形に削減するための並列 β 削減ステップの数は、項のサイズに対してほぼ線形です。これは、任意のチューリング マシンをチューリング マシンのサイズに線形に比例するサイズでラムダ計算にエンコードできるため、妥当なコスト尺度としては小さすぎます。ラムダ項を削減する真のコストは、β 削減自体によるものではなく、β 削減中の redex の重複の処理によるものです。^{[ 38 ]}最適削減の実装が、正規形への最左端ステップ数などの妥当なコスト モデルに関して測定した場合に妥当かどうかはわかりませんが、ラムダ計算の断片については、最適削減アルゴリズムが効率的であり、最左端と比較して最大で 2 乗のオーバーヘッドがあることが示されています。^{[ 37 ]}さらに、BOHM プロトタイプによる最適縮約の実装は、純粋なラムダ項においてCaml Light と Haskell の両方を上回った。^{[ 38 ]}

ピーター・ランディンの1965年の論文「ALGOL 60とチャーチのラムダ記法との対応関係」 ^{[ 39 ]}で指摘されているように、逐次手続き型プログラミング言語はラムダ計算の観点から理解することができ、これは手続き的抽象化と手続き（サブルーチン）適用の基本的なメカニズムを提供する。

(ラムダx : x ** 2 )

ラムダ計算の項が他のラムダ計算の項、さらには自分自身に対しても関数として作用するという事実は、ラムダ計算の意味論に関する疑問を生じさせた。ラムダ計算の項に意味のある意味を割り当てることはできるだろうか？自然な意味論としては、関数空間D → Dと同型な、それ自身に対する関数の集合Dを見つけることである。しかし、 DからDへのすべての関数の集合はDよりも大きな濃度を持つため、濃度制約により、そのような非自明なDは存在しない。ただし、Dが単一集合である場合は例外である。

1970年代に、ダナ・スコットは、連続関数のみを考慮すれば、必要な性質を持つ集合または領域Dが見つかることを示し、ラムダ計算のモデルを提供した。 ^{[ 40 ]}

この研究は、プログラミング言語の表示的意味論の基礎も形成した。

これらの拡張機能はラムダキューブに含まれています。

• 型付きラムダ計算– 型付き変数（および関数）を用いたラムダ計算
• システムF – 型変数を持つ型付きラムダ計算
• 構成の計算– 型を第一級の値とする型付きラムダ計算

これらの形式体系は、ラムダ計算の拡張であり、ラムダキューブには含まれていない。

• バイナリラムダ計算– バイナリ入出力（I/O）、項のバイナリ符号化、および指定されたユニバーサルマシンを備えたラムダ計算のバージョン。
• ラムダμ計算–古典論理を扱うためのラムダ計算の拡張

これらの形式体系はラムダ計算の変形である。

• カッパ計算― ラムダ計算の1階版

これらの形式体系はラムダ計算に関連している。

• 組み合わせ論理― 変数を用いない数理論理の表記法
• SKIコンビネータ計算– S、K、Iコンビネータに基づく計算システムであり、ラムダ計算と同等であるが、変数置換なしで簡約可能である。

この記事の一部は、FOLDOCの資料に基づいており、許可を得て使用しています。

• アベルソン、ハロルド＆ジェラルド・ジェイ・サスマン。『コンピュータプログラムの構造と解釈』MIT出版。ISBN 0-262-51087-1。
• Barendregt、Hendrik Pieterラムダ微積分の入門。
• Barendregt, Hendrik Pieter、「論理学とコンピュータ科学におけるラムダ計算の影響」。『記号論理学紀要』第3巻、第2号、1997年6月。
• Barendregt, Hendrik Pieter、「型自由ラムダ計算」、『数理論理学ハンドブック』 1091–1132ページ、North-Holland (1977) ISBN 0-7204-2285-X
• Cardone, Felice および Hindley, J. Roger、2006 年。「ラムダ計算と組み合わせ論理の歴史」 。Wayback Machineに 2021 年 5 月6 日にアーカイブされました。Gabbay および Woods (編)、Handbook of the History of Logic、第 5 巻。Elsevier。
• チャーチ、アロンゾ、「初等整数論の解決不可能な問題」、アメリカ数学ジャーナル、58（1936）、pp.  345–363。この論文には、ラムダ式の同値性が一般に決定不可能であることの証明が含まれています。
• チャーチ、アロンゾ（1941）。ラムダ変換の計算。プリンストン：プリンストン大学出版局。2020年4月14日取得。( ISBN) 978-0-691-08394-0）
• Frink Jr., Orrin (1944). 「レビュー: Alonzo Church によるラムダ変換の計算」 (PDF) . Bulletin of the American Mathematical Society . 50 (3): 169– 172. doi : 10.1090/s0002-9904-1944-08090-7 .
• Kleene, Stephen, A theory of positive integers in formal logic, American Journal of Mathematics, 57 (1935), pp. 153–173 and 219–244. Contains the lambda calculus definitions of several familiar functions.
• Landin, Peter, A Correspondence Between ALGOL 60 and Church's Lambda-Notation, Communications of the ACM, vol. 8, no. 2 (1965), pages 89–101. Available from the ACM site. A classic paper highlighting the importance of lambda calculus as a basis for programming languages.
• Larson, Jim, An Introduction to Lambda Calculus and Scheme. A gentle introduction for programmers.
• Michaelson, Greg (10 April 2013). An Introduction to Functional Programming Through Lambda Calculus. Courier Corporation. ISBN 978-0-486-28029-5.^[1]
• Schalk, A. and Simmons, H. (2005) An introduction to λ-calculi and arithmetic with a decent selection of exercises. Notes for a course in the Mathematical Logic MSc at Manchester University.
• de Queiroz, Ruy J.G.B. (2008). "On Reduction Rules, Meaning-as-Use and Proof-Theoretic Semantics". Studia Logica. 90 (2): 211–247. doi:10.1007/s11225-008-9150-5. S2CID 11321602. A paper giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is different from proof-theoretic semantics as in the Dummett–Prawitz tradition since it takes reduction as the rules giving meaning.
• Hankin, Chris, An Introduction to Lambda Calculi for Computer Scientists,ISBN 0954300653

Monographs/textbooks for graduate students

• Sørensen, Morten Heine and Urzyczyn, Paweł (2006), Lectures on the Curry–Howard isomorphism, Elsevier, ISBN 0-444-52077-5 is a recent monograph that covers the main topics of lambda calculus from the type-free variety, to most typed lambda calculi, including more recent developments like pure type systems and the lambda cube. It does not cover subtyping extensions.
• Pierce, Benjamin (2002), Types and Programming Languages, MIT Press, ISBN 0-262-16209-1 covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.

Documents

• A Short Introduction to the Lambda Calculus-(PDF) by Achim Jung
• A timeline of lambda calculus-(PDF) by Dana Scott
• A Tutorial Introduction to the Lambda Calculus-(PDF) by Raúl Rojas
• Lecture Notes on the Lambda Calculus-(PDF) by Peter Selinger
• Graphic lambda calculus by Marius Buliga
• Lambda Calculus as a Workflow Model by Peter Kelly, Paul Coddington, and Andrew Wendelborn; mentions graph reduction as a common means of evaluating lambda expressions and discusses the applicability of lambda calculus for distributed computing (due to the Church–Rosser property, which enables parallel graph reduction for lambda expressions).

• Graham Hutton, Lambda Calculus, a short (12 minutes) Computerphile video on the Lambda Calculus
• Helmut Brandl, Step by Step Introduction to Lambda Calculus
• "Lambda-calculus", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• David C. Keenan, To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
• L. Allison, Some executable λ-calculus examples
• Georg P. Loczewski, The Lambda Calculus and A++
• Bret Victor, Alligator Eggs: A Puzzle Game Based on Lambda Calculus
• LCI Lambda Interpreter a simple yet powerful pure calculus interpreter
• Lambda Calculus links on Lambda-the-Ultimate
• Mike Thyer, Lambda Animator, a graphical Java applet demonstrating alternative reduction strategies.
• Implementing the Lambda calculus using C++ Templates
• Shane Steinert-Threlkeld, "Lambda Calculi", Internet Encyclopedia of Philosophy
• Anton Salikhmetov, Macro Lambda Calculus