表現

コンピュータ サイエンスでは、「let」式は関数定義を制限されたスコープに関連付けます。

「let」式は数学でも定義され、ブール条件を制限された範囲に関連付けます。

「let」式は、値に適用されたラムダ抽象化と見なすことができます。数学では、let 式は、変数のスコープを制限する 存在量指定子内の式の結合と見なすこともできます。

let 式は、他の式の定義に使用する式のローカル定義を可能にするために、多くの関数型言語に存在します。let 式は、let または "let rec" の 2 つの形式で一部の関数型言語に存在します。let rec は、固定小数点コンビネータを使用して再帰を実装する単純な let 式の拡張です。

ダナ・スコットのLCF言語^[1]は、ラムダ計算が現代の関数型言語へと進化する過程の1つの段階でした。この言語はlet式を導入し、それ以降ほとんどの関数型言語に登場しています。

Scheme ^[2]、 ML、そして最近ではHaskell ^[3]などの言語は、LCFからlet式を継承しています。

ALGOLやPascalなどの状態のある命令型言語は、基本的にブロック構造で関数の制限されたスコープを実装するために let 式を実装します。^{[引用が必要]}

密接に関連する「where」節とその再帰的な変形である「where rec 」は、ピーター・ランディンの「式の機械的評価」にすでに登場しています。^[4]

「let」式は、別の式で使用する関数または値を定義します。多くの関数型プログラミング言語で使用される構造であるだけでなく、数学のテキストでよく使用される自然言語構造でもあります。これは、where 句の代替構文構造です。

どちらの場合も、全体の構造は値が 5 である式です。if -then-elseと同様に、式によって返される型は必ずしもブール型ではありません。

let式には主に4つの形式があります。

関数型言語では、let式は式内で呼び出すことができる関数を定義します。関数名のスコープは let 式構造に限定されます。

数学では、let 式は式に対する制約となる条件を定義します。構文は、let 式にローカルな存在量化された変数の宣言もサポートします。

用語、構文、セマンティクスは言語によって異なります。Scheme では、単純形式ではletが使用され、再帰形式ではlet rec が使用されます。ML では、 let は宣言ブロックの開始のみを示し、fun は関数定義の開始を示します。Haskell では、let は相互再帰になる可能性があり、コンパイラが何が必要かを判断します。

ラムダ抽象化は名前のない関数を表します。これがラムダ抽象化の定義における矛盾の原因です。しかし、ラムダ抽象化は名前のある関数を表すように構成することができます。この形式では矛盾は解消されます。ラムダ項、

${\displaystyle (\lambda fz)\ (\lambda xy)}$

は、 let式として記述できる式 で関数を定義することと同等です。 ${\displaystyle f}$${\displaystyle f\ x=y}$${\displaystyle z}$

${\displaystyle \operatorname {let} f\ x=y\operatorname {in} z}$

let 式は自然言語式として理解できます。let 式は、変数を値に置き換えることを表します。置換規則は、等号の意味を置換として記述します。

数学では、 let式は式の結合として記述されます。関数型言語では、let 式はスコープを制限するためにも使用されます。数学では、スコープは量指定子によって記述されます。let 式は、存在量指定子内の結合です。

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

ここで、EとF はブール型です。

let式を使用すると、置換を別の式に適用できます。この置換は、制限されたスコープ内でサブ式に適用できます。let 式の自然な使用法は、制限されたスコープに適用することです (ラムダ ドロップと呼ばれます)。これらのルールは、スコープを制限する方法を定義します。

${\displaystyle {\begin{cases}x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)\\x\in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=(\operatorname {let} x:G\operatorname {in} E)\ F\\x\not \in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ F\end{ケース}}}$

ここで、F はブール型ではありません。この定義から、関数型言語で使用される let 式の次の標準定義を導き出すことができます。

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x:x=y\operatorname {in} z)=z[x:=y]=(\lambda xz)\ y}$

簡潔にするために、存在変数を指定するマーカーは、文脈から明らかな場合は式から省略されます。 ${\displaystyle x:}$

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda xz)\ y}$

この結果を導くために、まず、

${\displaystyle x\not \in \operatorname {FV} (L)}$

それから

${\displaystyle {\begin{aligned}L\ (\operatorname {let} x:x=y\operatorname {in} z)&\iff (\operatorname {let} x:x=y\operatorname {in} L\ z)\\&\iff x=y\land L\ z\end{aligned}}}$

置換のルールを用いると、

${\displaystyle {\begin{aligned}&\iff x=y\land (L\ z)[x:=y]\\&\iff x=y\land (L[x:=y]\ z[x:=y])\\&\iff x=y\land L\ z[x:=y]\\&\implies L\ z[x:=y]\end{aligned}}}$

したがって、すべてのLについて、

${\displaystyle L\operatorname {let} x:x=y\operatorname {in} z\implies L\ z[x:=y]}$

ここでKは新しい変数です。すると、 ${\displaystyle L\ X=(X=K)}$

${\displaystyle (\operatorname {let} x:x=y\operatorname {in} z)=K\implies z[x:=y]=K}$

それで、

${\displaystyle \operatorname {let} x:x=y\operatorname {in} z=z[x:=y]}$

しかし、ベータ減少の数学的解釈から、

${\displaystyle (\lambda x.z)\ y=z[x:=y]}$

ここで、yが変数xの関数である場合、それはzのxと同じではありません。アルファリネームが適用される場合があります。したがって、

${\displaystyle x\not \in \operatorname {FV} (y)}$

それで、

${\displaystyle x\not \in \operatorname {FV} (y)\implies \operatorname {let} x:x=y\operatorname {in} z=(\lambda x.z)\ y}$

この結果は関数型言語では省略形で表現され、意味は明確です。

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y}$

ここで、変数x は、x を定義する方程式の一部であると同時に、存在量指定子の変数としても暗黙的に認識されます。

Eが で定義されている場合、矛盾が生じます。この場合、 ${\displaystyle E=\neg }$

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)}$

となり、

${\displaystyle \operatorname {let} x:G\operatorname {in} \neg F=\neg \ (\operatorname {let} x:G\operatorname {in} F)}$

そして、使用して、

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

${\displaystyle (\exists xG\land \neg F)=\neg \ (\exists xG\land F)}$

${\displaystyle =(\exists x\neg G\lor \neg F)}$

Gが偽ならこれは偽です。この矛盾を避けるために、Fはブール型であってはなりません。ブール型Fの場合、ドロップルールの正しい記述は等式ではなく含意を使用します。

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies (\operatorname {let} x:G\operatorname {in} E\ F\to E\ (\operatorname {let} x:G\operatorname {in} F))}$

ブール型に他の型とは異なるルールが適用されるのは奇妙に思えるかもしれません。その理由は、

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

Fがブール値の場合にのみ適用されます。2 つのルールを組み合わせると矛盾が生じ、1 つのルールが当てはまる場合、もう 1 つのルールは当てはまりません。

Let式は複数の変数で定義されることもある。

${\displaystyle (\exists v\cdots \exists w\exists xE\land F)\iff \operatorname {let} v,\ldots ,w,x:E\operatorname {in} F}$

すると、

${\displaystyle x\not \in FV(E)\implies (\exists v\cdots \exists w\exists xE\land F)\iff (\exists v\cdots \exists w(E\land \exists xF))}$

それで、

${\displaystyle x\not \in FV(E)\implies (\operatorname {let} v,\ldots ,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,\ldots ,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)}$

イータ削減は、ラムダ抽象化を記述するための規則を提供します。この規則は、上で導出された 2 つの法則とともに、ラムダ計算と let 式の関係を定義します。

数学的定義に伴う潜在的な問題を回避するために、Dana Scott はもともとラムダ計算からlet式を定義しました。これは、トップダウン、つまり公理的な数学的定義とは対照的に、ボトムアップ、つまり構成的なlet式の定義であると考えられます。

単純で非再帰的なlet式は、項に適用されるラムダ抽象化の 構文糖として定義されました。その定義では、

${\displaystyle (\operatorname {let} _{s}x=y\operatorname {in} z)\equiv (\lambda x.z)\ y}$

その後、単純なlet式の定義が拡張され、固定小数点コンビネータを使用した再帰が可能になりました。

固定小数点コンビネータは、次の式で表すことができます。

${\displaystyle \lambda f.\operatorname {let} x=f\ x\operatorname {in} x}$

この表現はラムダ項に変換できます。ラムダ抽象化では、適用された式内の変数名への参照はサポートされていないため、x はxへのパラメーターとして渡す必要があります。

${\displaystyle \lambda f.\operatorname {let} x\ x=f\ (x\ x)\operatorname {in} x\ x}$

イータ削減規則を用いると、

${\displaystyle f\ x=y\equiv f=\lambda x.y}$

与える、

${\displaystyle \lambda f.\operatorname {let} x=\lambda x.f\ (x\ x)\operatorname {in} x\ x}$

let式は、次のようにラムダ抽象化として表現できる。

${\displaystyle n\not \in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda n.L)\ E)}$

与える、

${\displaystyle \lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

これはおそらく、ラムダ計算における固定小数点コンビネータの最も単純な実装です。ただし、1 つのベータ削減により、Curry の Y コンビネータのより対称的な形式が得られます。

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

「let rec」と呼ばれる再帰let式は、再帰 let 式の Y コンビネータを使用して定義されます。

${\displaystyle (\operatorname {let\ rec} x=y\operatorname {in} z)\equiv (\lambda x.z)\ (Y\ (\lambda x.y))}$

このアプローチは、相互再帰をサポートするために一般化されます。相互再帰的なlet式は、式を並べ替えてand条件を削除することで作成できます。これは、複数の関数定義を単一の関数定義に置き換えて、変数のリストを式のリストと等しくすることで実現されます。次に、YコンビネータのバージョンであるY*多変数固定小数点コンビネータ ^[5]を使用して、すべての関数の固定小数点を同時に計算します。結果は、let式の相互再帰実装です。

let式は集合の要素である値を表すために使われる。

${\displaystyle \operatorname {let} x\in X\operatorname {in} x}$

関数適用では、あるlet式を別のlet式に適用すると、

${\displaystyle {\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)\\&=\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y\\&=\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y\end{aligned}}}$

ただし、let 式をそれ自体に適用する場合は、異なるルールが適用されます。

${\displaystyle {\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)\\&=\operatorname {let} x\in X\operatorname {in} x\ x\end{aligned}}}$

値を組み合わせるための簡単なルールはないようです。必要なのは、値が値セットのメンバーである変数を表す一般的な形式の式です。式は、変数とセットに基づく必要があります。

この形式に関数を適用すると、同じ形式の別の式が生成されます。このように、複数の値を持つ関数の式は、1 つの値を持つものとして扱われます。

フォームが値のセットを表すだけでは不十分です。各値には、式が値を取るタイミングを決定する条件が必要です。結果として得られる構造は、条件と値のペアのセットであり、「値セット」と呼ばれます。代数的値セットの絞り込みを参照してください。

lambda 式とlet式間の変換を記述するメタ関数が提供されます。メタ関数は、プログラムをパラメータとして受け取る関数です。プログラムはメタプログラムのデータです。プログラムとメタプログラムは異なるメタレベルにあります。

プログラムとメタプログラムを区別するために、以下の規則が使用されます。

• 角括弧 [] は、メタプログラム内の関数の適用を表すために使用されます。
• メタプログラム内の変数には大文字が使用されます。プログラム内の変数は小文字で表されます。
• ${\displaystyle \equiv }$メタプログラム内のequalsに使用されます。

簡単にするために、一致する最初のルールが適用されます。また、このルールでは、ラムダ式が前処理され、各ラムダ抽象化に一意の名前が付けられていることが前提となっています。

置換演算子も使用されます。式は、L内のGのすべての出現をSに置き換え、式を返すことを意味します。使用される定義は、ラムダ計算ページにある定義から、式の置換をカバーするように拡張されています。式のマッチングでは、式をアルファの等価性 (変数の名前変更) について比較する必要があります。 ${\displaystyle L[G:=S]}$

次のルールは、構造を変更せずに ラムダ式からlet式に変換する方法について説明しています。

1. ${\displaystyle \operatorname {de-lambda} [V]\equiv V}$
2. ${\displaystyle \operatorname {de-lambda} [M\ N]\equiv \operatorname {de-lambda} [M]\ \operatorname {de-lambda} [N]}$
3. ${\displaystyle \operatorname {de-lambda} [F=\lambda P.E]\equiv \operatorname {de-lambda} [F\ P=E]}$
4. ${\displaystyle \operatorname {de-lambda} [E=F]\equiv \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$
5. ${\displaystyle \operatorname {de-lambda} [(\lambda F.E)L]\equiv \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]}$
6. ${\displaystyle V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]\equiv \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]}$
7. ${\displaystyle V\neq W\to \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]\equiv \operatorname {let} V,W:E\land F\operatorname {in} G}$
8. ${\displaystyle \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} F]\equiv \operatorname {let} V:E\operatorname {in} F}$

ルール 6 は、関数の名前として一意の変数 V を作成します。

例えば、Yコンビネータは、

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

に変換されます。

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p}$

これらのルールは、上記の変換を逆にします。構造を変更せずに、 let式から lambda 式に変換します。すべての let 式がこれらのルールを使用して変換できるわけではありません。ルールでは、式がde-lambdaによって生成されたかのように既に配置されていることを前提としています。

1. ${\displaystyle \operatorname {get-lambda} [F,G\ V=E]=\operatorname {get-lambda} [F,G=\lambda V.E]}$
2. ${\displaystyle \operatorname {get-lambda} [F,F=E]=\operatorname {de-let} [E]}$
3. ${\displaystyle \operatorname {de-let} [\lambda V.E]\equiv \lambda V.\operatorname {de-let} [E]}$
4. ${\displaystyle \operatorname {de-let} [M\ N]\equiv \operatorname {de-let} [M]\ \operatorname {de-let} [N]}$
5. ${\displaystyle \operatorname {de-let} [V]\equiv V}$
6. ${\displaystyle V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} V]\equiv \operatorname {get-lambda} [V,E]}$
7. ${\displaystyle V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv (\lambda V.\operatorname {de-let} [L])\ \operatorname {get-lambda} [V,E]}$
8. ${\displaystyle W\not \in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} G]\equiv \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} \operatorname {let} W:F\ \operatorname {in} G]}$
9. ${\displaystyle V\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ V=\operatorname {get-lambda} [V,E][V:=V\ V]\ \operatorname {in} L[V:=V\ V]]}$
10. ${\displaystyle W\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ W=\operatorname {get-lambda} [V,E][V:=V\ W]\ \operatorname {in} \operatorname {let} W:F[V:=V\ W]\ \operatorname {in} L[V:=V\ W]]}$

再帰的に使用される自由変数を持つlet式に対して、ラムダ計算には構造的に正確な同等のものはありません。この場合、パラメータの追加が必要です。ルール 8 と 10 はこれらのパラメータを追加します。

ルール 8 と 10 は、 let式内の相互再帰方程式が 2 つある場合には十分です。ただし、相互再帰方程式が 3 つ以上ある場合には機能しません。一般的なケースでは、ループの追加レベルが必要となり、メタ関数が少し難しくなります。一般的なケースを実装する際には、以下のルールがルール 8 と 10 に代わるものです。ルール 8 と 10 は、より単純なケースを最初に検討できるように残されています。

1. lambda-form - 式を、それぞれが変数=式という形式の式の連結に変換します。
   1. ${\displaystyle \operatorname {lambda-form} [G\ V=E]=\operatorname {lambda-form} [G=\lambda V.E]}$
   2. ${\displaystyle \operatorname {lambda-form} [E\land F]=\operatorname {lambda-form} [E]\land \operatorname {lambda-form} [F]}$
   3. ${\displaystyle \operatorname {lambda-form} [V=E]=V=E}$......ここで、Vは変数です。
2. lift-vars - 式には自由変数として X があるため、パラメーターとしてX を必要とする変数のセットを取得します。
   1. ${\displaystyle X\in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{V\}}$
   2. ${\displaystyle X\not \in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{\}}$
   3. ${\displaystyle \operatorname {lift-vars} [X,E\land F]=\operatorname {lift-vars} [X,E]\cup \operatorname {lift-vars} [X.F]}$
3. サブ変数- セット内の各変数を、式内の X に適用された変数に置き換えます。これにより、X は式の右側の自由変数ではなく、パラメータとして渡される変数になります。
   1. ${\displaystyle \operatorname {sub-vars} [E,\{V\}\cup S,X]=\operatorname {sub-vars} [E[V:=V\ X],S,X]}$
   2. ${\displaystyle \operatorname {sub-vars} [E,\{\},X]=E}$
4. de-let - Eの各条件を解除して、 X が式の右側の自由変数にならない ようにします。
   1. ${\displaystyle {\begin{aligned}L&=\operatorname {lambda-form} [E]\land S=\operatorname {lift-vars} [X,L]\to \operatorname {de-let} [\operatorname {let} V\ldots W,X:E\land F\ \operatorname {in} G]\\&\equiv \operatorname {de-let} [\operatorname {let} V\ldots W:\operatorname {sub-vars} [L,S,X]\ \operatorname {in} \operatorname {let} \operatorname {sub-vars} [\operatorname {lambda-form} [F],S,X]\ \operatorname {in} \operatorname {sub-vars} [G,S,X]]\end{aligned}}}$

例えば、Yコンビネータから得られるlet式は、

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)\ \operatorname {in} p}$

に変換されます。

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))}$

2番目の例として、 Yコンビネータのリフトバージョンを取り上げます。

${\displaystyle \operatorname {let} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p}$

に変換されます。

${\displaystyle (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)}$

3番目の例として、

${\displaystyle \operatorname {let} x:x\ f=f\ (x\ f)\ \operatorname {in} x}$

は、

${\displaystyle (\lambda x.x\ x)\ (\lambda x.\lambda f.f\ (x\ x\ f))}$

4番目の例として、

${\displaystyle \operatorname {let} x:x=f\ x\ \operatorname {in} x}$

は、

${\displaystyle (\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

これは有名なy コンビネータです。

• ダナ・スコット

• 範囲（コンピュータサイエンス）
• ラムダリフティング
• 固定小数点コンビネータ
• ラムダ計算
• カリーのパラドックス
• 演繹的ラムダ計算
• 制約論理プログラミング
• 代数的値集合の狭まり

• ミッチェル、ジョン C. (1996)。プログラミング言語の基礎。MIT 出版。ISBN 978-0-262-13321-0。
• Plotkin, GD (1977年12月). 「プログラミング言語として考えるLCF」.理論計算機科学. 5 (3): 223–255. doi : 10.1016/0304-3975(77)90044-5 .