グローバリゼーションのメタプロセス
ラムダ リフティングは、関数がグローバル スコープ 内で互いに独立して定義されるように コンピュータ プログラムを 再構築する メタプロセス です 。個々の「リフト」は、ローカル 関数を グローバル関数に変換します。これは、次の 2 つのステップで構成されるプロセスです。
パラメータを追加して関数内の 自由変数を 削除します。 関数を制限されたスコープからより広いスコープまたはグローバル スコープに移動します。 「ラムダ リフティング」という用語は、1982 年頃に Thomas Johnsson によって初めて導入され、歴史的には 関数型プログラミング言語を実装するためのメカニズムと考えられていました。一部の最新の コンパイラ では、他の手法と組み合わせて使用されています 。
ラムダ リフトはクロージャ変換と同じではありません。すべての 呼び出しサイトを 調整する必要があり (呼び出しに余分な引数を追加)、リフトされたラムダ式のクロージャは導入されません 。 対照的に、クロージャ変換では呼び出しサイトを調整する必要はなく、自由変数を値にマッピングするラムダ式のクロージャが導入されます。
この手法は、コード リファクタリング で個々の関数に使用して 、関数をそれが記述されたスコープ外でも使用できるようにする場合があります。 ラムダ リフトは、プログラムを変換するために繰り返すこともできます。 リフトを繰り返し使用すると、 ラムダ計算で記述されたプログラムを、ラムダを使用しない 再帰関数 のセットに変換できます 。 これは、ラムダ計算で記述されたプログラムと関数として記述されたプログラムの同等性を示しています。 [1] ただし、ラムダ リフトで使用される イータ削減は、変数の条件を満たす値が 1 つだけであることを最初に確認せずに変数から値を削除するため、ラムダ計算に 基数の問題を 導入するステップであるため、演繹におけるラムダ 計算の健全性は示されません ( カリーのパラドックス を参照)。
ラムダリフティングはコンパイラの処理時間を増大させます。ラムダリフティングの効率的な実装は コンパイラの処理時間を増大させます。 [2]
お （
ん
2
）
{\displaystyle O(n^{2})}
型なしラムダ計算 では、基本型は関数ですが、リフティングによって ラムダ式の ベータ削減 の結果が変わることがあります。結果として得られる関数は数学的には同じ意味を持ちますが、型なしラムダ計算では同じ関数とは見なされません。内包 的等価性と外延的等価性 も参照してください。
ラムダリフティングの逆の操作はラムダドロップである。 [3]
ラムダドロップにより、コンパイラーによるプログラムのコンパイルが高速化される可能性があり、パラメーターの数を減らし、スタック フレームのサイズを縮小することで、結果のプログラムの効率も向上する可能性があります。ただし、関数の再利用は難しくなります。ドロップされた関数はそのコンテキストに結び付けられ、最初に解除された場合にのみ、別のコンテキストで使用できます。
アルゴリズム 次のアルゴリズムは、クロージャをファーストクラスオブジェクト としてサポートしていない言語で任意のプログラムをラムダリフトする 1 つの方法です 。
各関数に一意の名前が付くように関数の名前を変更します。 各自由変数を囲む関数への追加引数に置き換え、その引数を関数を使用するたびに渡します。 自由変数を持たないすべてのローカル関数定義を、同一のグローバル関数に置き換えます。 すべての自由変数とローカル関数が削除されるまで、手順 2 と 3 を繰り返します。 言語に、引数として渡したり、他の関数から返したりできるファーストクラス オブジェクトとしてクロージャがある場合、クロージャは、自由変数のバインディングをキャプチャするデータ構造によって表現する必要があります。
例 次の OCaml プログラムは、1 から 100 までの整数の合計を計算します。
rec sum n = とします 。n = 1 の場合 は 1 、それ 以外の場合は f x = n + x と します 。f ( sum ( n - 1 )) の場合は 合計 100とします。 ( は、自分自身を呼び出す可能性のある関数として let rec宣言されています sum。) sum の引数を引数より小さい数値の合計に追加する関数 f は、ローカル関数です。 f の定義内では、n は自由変数です。まず、自由変数をパラメーターに変換します。
rec sum n = とします 。n = 1 の場合は 1 、それ 以外の場合は f w x = w + x と します。f n ( sum ( n - 1 ) ) の場合は 合計 100とします。 次に、f をグローバル関数に持ち上げます。
rec f w x = w + x とし、 合計 n = if n = 1 then 1 else f n ( sum ( n - 1 )) in sum 100 と する。 以下は同じ例ですが、今回は JavaScript で書かれています。
// 初期バージョン 関数 sum ( n ) { 関数 f ( x ) { return n + x ; } if ( n == 1 ) の場合は 1 を 返します 。 そうでない場合は f ( sum ( n - 1 )) を返します 。 } // 自由変数nを仮パラメータwに変換した後 関数 sum ( n ) { 関数 f ( w , x ) { return w + x ; } n == 1 の 場合は 1 を返します 。 それ以外の場合は f ( n 、 sum ( n - 1 ) ) を 返します 。 } // 関数fをグローバルスコープに持ち上げた後 関数 f ( w , x ) { 戻り値 w + x ; } 関数 sum ( n ) { if ( n == 1 ) return 1 ; else return f ( n , sum ( n - 1 )); }
ラムダリフティングとクロージャ ラムダ リフトと クロージャは、どちらも ブロック構造の プログラムを実装する方法です 。ブロック構造を排除することでブロック構造を実装します。すべての関数はグローバル レベルに持ち上げられます。クロージャ変換は、現在のフレームを他のフレームにリンクする「クロージャ」を提供します。クロージャ変換では、コンパイル時間が短縮されます。
再帰関数やブロック構造のプログラムは、リフティングの有無にかかわらず、 シンプルで効率的な スタックベースの実装を使用して実装できます。ただし、スタック フレーム ベースの実装は 厳密 (積極的) である必要があります。スタック フレーム ベースの実装では、関数のライフが 後入れ先出し (LIFO) である必要があります。つまり、計算を開始した最新の関数が最初に終了する必要があります。
一部の関数型言語 ( Haskell など )は、 遅延評価を 使用して実装されています。遅延評価では、値が必要になるまで計算を遅らせます。遅延実装戦略により、プログラマーに柔軟性がもたらされます。遅延評価では、関数によって計算された値が要求されるまで、関数の呼び出しを遅らせる必要があります。1 つの実装は、値の代わりに、計算を記述するデータの「フレーム」への参照を記録することです。後で値が必要になったときに、必要なときにちょうど間に合うように、フレームを使用して値が計算されます。計算された値が参照に置き換えられます。
「フレーム」は スタック フレーム に似ていますが、違いはスタックに保存されないことです。遅延評価では、計算に必要なすべてのデータをフレームに保存する必要があります。関数が「リフト」されている場合、フレームには 関数ポインタ と関数へのパラメータのみを記録する必要があります。最近の言語の中には、スタック ベースの割り当ての代わりに ガベージ コレクションを 使用して変数の寿命を管理するものがあります。管理されたガベージ コレクション環境では、クロージャは 値 を取得できるフレームへの参照を記録します。対照的に、リフトされた関数には、計算に必要な各値のパラメータがあります。
Let式とラムダ計算 Let 式は、 リフティングとドロップを記述する場合や、再帰方程式とラムダ式の関係を記述する場合に役立ちます。ほとんどの関数型言語には let 式があります。また、 ALGOL や Pascalなどのブロック構造化プログラミング言語も、制限された スコープ で使用するための関数のローカル定義を許可するという点で似ています 。
ここで使用されるlet 式は 、多くの関数型言語で実装されている
let rec の完全な相互再帰バージョンです。
let 式はラムダ計算 と関連しています 。ラムダ計算は構文とセマンティクスが単純で、ラムダ リフトの記述に適しています。ラムダ リフトを ラムダから let 式への変換として記述し 、ラムダ ドロップをその逆として記述すると便利です。これは、 let 式が相互再帰を許可しているためです。相互再帰は、ある意味では、ラムダ計算でサポートされているよりもリフトされています。ラムダ計算では相互再帰はサポートされておらず、最も外側のグローバル スコープで定義できる関数は 1 つだけです。
持ち上げずに平行移動を記述する 変換規則は、 Let 式の 記事に記載されています。
以下の規則は、lambda式とlet式の同等性を記述する。
ラムダのリフティングとドロップを説明するメタ関数が提供されます。メタ関数は、プログラムをパラメータとして受け取る関数です。プログラムはメタプログラムのデータです。プログラムとメタプログラムは異なるメタレベルにあります。
プログラムとメタプログラムを区別するために、以下の規則が使用されます。
角括弧 [] は、メタプログラム内の関数の適用を表すために使用されます。 メタプログラム内の変数には大文字が使用されます。プログラム内の変数は小文字で表されます。
≡
{\displaystyle \equiv}
メタプログラム内のequalsに使用されます。
_
{\displaystyle \_}
ダミー変数、つまり未知の値を表します。 簡単にするために、一致する最初のルールが適用されます。また、このルールでは、ラムダ式が前処理され、各ラムダ抽象化に一意の名前が付けられていることが前提となっています。
置換演算子は広範囲に使用されています。式は、 L 内の G を すべて S に置き換えて、式を返すことを意味します。使用される定義は、 ラムダ計算 ページにある定義から、式の置換をカバーするように拡張されています 。式のマッチングでは、式をアルファの等価性 (変数の名前変更) について比較する必要があります。
ら [ グ := S ]
{\displaystyle L[G:=S]}
ラムダ計算におけるラムダリフティング 各ラムダリフトは、ラムダ式のサブ式であるラムダ抽象化を取り、それを作成した関数への関数呼び出し (アプリケーション) に置き換えます。サブ式内の自由変数は、関数呼び出しへのパラメーターです。
ラムダ リフトは、コード リファクタリング で個々の関数に使用して 、関数が記述されたスコープ外でも関数を使用できるようにすることができます。また、プログラムを変換するために、式にラムダ抽象化がなくなるまで、このようなリフトを繰り返すこともできます。
ラムダリフト リフトは、式内の部分式をその式の先頭に持ち上げるものです。式は、より大きなプログラムの一部である場合があります。これにより、部分式が持ち上げられる場所を制御できます。プログラム内でリフトを実行するために使用されるラムダ リフト操作は、次のとおりです。
l 1つの メートル b d 1つの - l 私 ふ t - o p
[ S 、 ら 、 ポ ] = ポ [ ら :=
l 1つの メートル b d 1つの - l 私 ふ t
[ S 、 ら ] ]
{\displaystyle \operatorname {lambda-lift-op} [S,L,P]=P[L:=\operatorname {lambda-lift} [S,L]]}
サブ式は、ラムダ抽象化、またはパラメータに適用されたラムダ抽象化のいずれかになります。
2種類のリフトが可能です。
匿名リフトには、ラムダ抽象化のみのリフト式があります。これは匿名関数の定義とみなされます。関数の名前を作成する必要があります。
名前付きリフト式には、式に適用されたラムダ抽象化があります。このリフトは、関数の名前付き定義と見なされます。
匿名リフト 匿名リフトはラムダ抽象化 ( S と呼ばれる) を取ります。 S の場合;
S を 置き換える関数の名前 ( V ) を作成します。 V で識別される名前 が使用されていないことを確認します。 S 内のすべての自由変数のパラメータを V に追加して 、式 G を作成します( make-call を 参照)。 ラムダ リフトは、関数定義の追加とともに、関数適用を
ラムダ抽象化 Sに置き換えることです。
l 1つの メートル b d 1つの - l 私 ふ t
[ S 、 ら ] ≡ させて 五 :
d e - l 1つの メートル b d 1つの
[ グ = S ] で ら [ S := グ ]
{\displaystyle \operatorname {lambda-lift} [S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[S:=G]}
新しいラムダ式では、 G がS に置き換えられています。 L [ S := G ]は、 L 内の Gが S に置き換えられることを意味することに注意してください 。関数定義には、関数定義 G = S が追加されています。
上記の規則において、 Gは式 S に代入される関数適用であり 、次のように定義される。
グ =
メートル 1つの け e - c 1つの l l
[ 五 、 FV [ S ] ]
{\displaystyle G=\operatorname {make-call} [V,\operatorname {FV} [S]]}
ここで、 Vは 関数名です。これは新しい変数、つまりラムダ式でまだ使用されていない名前である必要があります。
五 ∉ 変数 [ させて ふ で ら ]
{\displaystyle V\not \in \operatorname {vars} [\operatorname {let} F\operatorname {in} L]}
ここで、 は E で使用される変数のセットを返すメタ関数です 。
変数 [ え ]
{\displaystyle \operatorname {vars} [E]}
呼び出しの構築 関数呼び出し G は、 自由変数セット（ V で表される）内の各変数のパラメータを関数 H に追加することによって構築されます。
バツ ∈ 五 →
メートル 1つの け e - c 1つの l l
[ H 、 五 ] ≡
メートル 1つの け e - c 1つの l l
[ H 、 五 ∩ ¬ { バツ } ]
バツ
{\displaystyle X\in V\to \operatorname {make-call} [H,V]\equiv \operatorname {make-call} [H,V\cap \neg \{X\}]\ X}
メートル 1つの け e - c 1つの l l
[ H 、 { } ] ≡ H
{\displaystyle \operatorname {make-call} [H,\{\}]\equiv H}
名前付きリフト 名前付きリフトは、関数名 V が提供される点を除いて、匿名リフトと似ています。
l
a
m
b
d
a
-
l
i
f
t
[
(
λ
V
.
E
)
S
,
L
]
≡
let
V
:
d
e
-
l
a
m
b
d
a
[
G
=
S
]
in
L
[
(
λ
V
.
E
)
S
:=
E
[
V
:=
G
]
]
{\displaystyle \operatorname {lambda-lift} [(\lambda V.E)\ S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[(\lambda V.E)\ S:=E[V:=G]]}
匿名リフトに関しては、式 G は S の自由変数を適用して V から構築されます 。これは次のように定義されます。
G
=
m
a
k
e
-
c
a
l
l
[
V
,
FV
[
S
]
]
{\displaystyle G=\operatorname {make-call} [V,\operatorname {FV} [S]]}
ラムダリフト変換は、ラムダ式を取り、すべてのラムダ抽象を式の先頭に持ち上げます。次に、抽象は 再帰関数 に変換され、ラムダ抽象が削除されます。結果は、次の形式の関数型プログラムになります。
let
M
in
N
{\displaystyle \operatorname {let} M\operatorname {in} N}
ここで、 M は 一連の関数定義であり、 N は 返される値を表す式です。
例えば、
l
a
m
b
d
a
-
l
i
f
t
-
t
r
a
n
[
λ
f
.
(
λ
x
.
f
(
x
x
)
)
(
λ
x
.
f
(
x
x
)
)
]
≡
let
p
f
x
=
f
(
x
x
)
∧
q
p
f
=
(
p
f
)
(
p
f
)
in
q
p
{\displaystyle \operatorname {lambda-lift-tran} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\equiv \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p}
その後、 de-let メタ関数 を使用して、結果をラムダ計算に戻すことができます。
d
e
-
l
e
t
[
l
a
m
b
d
a
-
l
i
f
t
-
t
r
a
n
[
λ
f
.
(
λ
x
.
f
(
x
x
)
)
(
λ
x
.
f
(
x
x
)
)
]
]
≡
(
λ
p
.
(
λ
q
.
q
p
)
λ
p
.
λ
f
.
(
p
f
)
(
p
f
)
)
λ
f
.
λ
x
.
f
(
x
x
)
{\displaystyle \operatorname {de-let} [\operatorname {lambda-lift-tran} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]]\equiv (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)}
ラムダ式の変換処理は一連のリフトである。各リフトには、
関数 lift-choice によって選択されたサブ式。サブ式は、ラムダのない方程式に変換できるように選択する必要があります。 リフトは、次のセクションで説明する lambda-lift メタ関数の呼び出しによって実行されます。
{
l
a
m
b
d
a
-
l
i
f
t
-
t
r
a
n
[
L
]
=
d
r
o
p
-
p
a
r
a
m
s
-
t
r
a
n
[
m
e
r
g
e
-
l
e
t
[
l
a
m
b
d
a
-
a
p
p
l
y
[
L
]
]
]
l
a
m
b
d
a
-
a
p
p
l
y
[
L
]
=
l
a
m
b
d
a
-
p
r
o
c
e
s
s
[
l
i
f
t
-
c
h
o
i
c
e
[
L
]
,
L
]
l
a
m
b
d
a
-
p
r
o
c
e
s
s
[
none
,
L
]
=
L
l
a
m
b
d
a
-
p
r
o
c
e
s
s
[
S
,
L
]
=
l
a
m
b
d
a
-
a
p
p
l
y
[
l
a
m
b
d
a
-
l
i
f
t
[
S
,
L
]
]
{\displaystyle {\begin{cases}\operatorname {lambda-lift-tran} [L]=\operatorname {drop-params-tran} [\operatorname {merge-let} [\operatorname {lambda-apply} [L]]]\\\operatorname {lambda-apply} [L]=\operatorname {lambda-process} [\operatorname {lift-choice} [L],L]\\\operatorname {lambda-process} [\operatorname {none} ,L]=L\\\operatorname {lambda-process} [S,L]=\operatorname {lambda-apply} [\operatorname {lambda-lift} [S,L]]\end{cases}}}
リフトが適用されると、レットは 1 つのレットに結合されます。
{
m
e
r
g
e
-
l
e
t
[
let
V
:
E
in
let
W
:
F
in
G
]
=
m
e
r
g
e
-
l
e
t
[
let
V
,
W
:
E
∧
F
in
G
]
m
e
r
g
e
-
l
e
t
[
E
]
=
E
{\displaystyle {\begin{cases}\operatorname {merge-let} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]=\operatorname {merge-let} [\operatorname {let} V,W:E\land F\operatorname {in} G]\\\operatorname {merge-let} [E]=E\end{cases}}}
次に、パラメータ削除が適用され、「let」式で不要なパラメータが削除されます。let 式では関数定義が相互に直接参照できますが、ラムダ抽象化は厳密に階層化されており、関数は自身を直接参照することはできません。
リフティングの表現を選択する 式をリフト対象として選択する方法は 2 つあります。1 つ目は、すべてのラムダ抽象化を匿名関数の定義として扱います。2 つ目は、パラメーターに適用されたラムダ抽象化を関数の定義として扱います。パラメーターに適用されたラムダ抽象化には、関数を定義する let 式として、または匿名関数を定義するものとして、2 つの解釈があります。どちらの解釈も有効です。
これら 2 つの述語は、両方の定義に必要です。
lambda-free - ラムダ抽象化を含まない式。
{
l
a
m
b
d
a
-
f
r
e
e
[
λ
F
.
X
]
=
false
l
a
m
b
d
a
-
f
r
e
e
[
V
]
=
true
l
a
m
b
d
a
-
f
r
e
e
[
M
N
]
=
l
a
m
b
d
a
-
f
r
e
e
[
M
]
∧
l
a
m
b
d
a
-
f
r
e
e
[
N
]
{\displaystyle {\begin{cases}\operatorname {lambda-free} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-free} [V]=\operatorname {true} \\\operatorname {lambda-free} [M\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-free} [N]\end{cases}}}
lambda-anon - 匿名関数。X がラムダフリーであるような式。
λ
x
1
.
.
.
.
λ
x
n
.
X
{\displaystyle \lambda x_{1}.\ ...\ \lambda x_{n}.X}
{
l
a
m
b
d
a
-
a
n
o
n
[
λ
F
.
X
]
=
l
a
m
b
d
a
-
f
r
e
e
[
X
]
∨
l
a
m
b
d
a
-
a
n
o
n
[
X
]
l
a
m
b
d
a
-
a
n
o
n
[
V
]
=
false
l
a
m
b
d
a
-
a
n
o
n
[
M
N
]
=
false
{\displaystyle {\begin{cases}\operatorname {lambda-anon} [\lambda F.X]=\operatorname {lambda-free} [X]\lor \operatorname {lambda-anon} [X]\\\operatorname {lambda-anon} [V]=\operatorname {false} \\\operatorname {lambda-anon} [M\ N]=\operatorname {false} \end{cases}}}
持ち上げのためだけに匿名関数を選択する 最も深い匿名抽象化を検索します。これにより、リフトが適用されたときに、リフトされた関数は単純な方程式になります。この定義では、パラメーターを持つラムダ抽象化は関数を定義するものとして認識されません。すべてのラムダ抽象化は、匿名関数を定義するものとしてみなされます。
lift-choice - 式を走査して見つかった最初の匿名関数、または 関数がない場合は
none 。
l
a
m
b
d
a
-
a
n
o
n
[
X
]
→
l
i
f
t
-
c
h
o
i
c
e
[
X
]
=
X
{\displaystyle \operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X}
l
i
f
t
-
c
h
o
i
c
e
[
λ
F
.
X
]
=
l
i
f
t
-
c
h
o
i
c
e
[
X
]
{\displaystyle \operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]}
l
i
f
t
-
c
h
o
i
c
e
[
M
]
≠
none
→
l
i
f
t
-
c
h
o
i
c
e
[
M
N
]
=
l
i
f
t
-
c
h
o
i
c
e
[
M
]
{\displaystyle \operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]}
l
i
f
t
-
c
h
o
i
c
e
[
M
N
]
=
l
i
f
t
-
c
h
o
i
c
e
[
N
]
{\displaystyle \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]}
l
i
f
t
-
c
h
o
i
c
e
[
V
]
=
none
{\displaystyle \operatorname {lift-choice} [V]=\operatorname {none} }
例えば、
持ち上げるための名前付き関数と無名関数の選択 最も深い名前付きまたは匿名関数の定義を検索します。これにより、リフトが適用されると、リフトされた関数は単純な方程式になります。この定義は、実際のパラメーターを持つラムダ抽象化を関数の定義として認識します。適用のないラムダ抽象化のみが匿名関数として扱われます。
ラムダ名 名前付き関数。Mはラムダフリー、N はラムダフリー、または匿名関数
のような式。
(
λ
F
.
M
)
N
{\displaystyle (\lambda F.M)\ N}
l
a
m
b
d
a
-
n
a
m
e
d
[
(
λ
F
.
M
)
N
]
=
l
a
m
b
d
a
-
f
r
e
e
[
M
]
∧
l
a
m
b
d
a
-
a
n
o
n
[
N
]
l
a
m
b
d
a
-
n
a
m
e
d
[
λ
F
.
X
]
=
false
l
a
m
b
d
a
-
n
a
m
e
d
[
V
]
=
false
{\displaystyle {\begin{array}{l}\operatorname {lambda-named} [(\lambda F.M)\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-anon} [N]\\\operatorname {lambda-named} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-named} [V]=\operatorname {false} \end{array}}}
リフト選択 式を走査して見つかった最初の匿名関数または名前付き関数 。関数がない場合は
none になります。
l
a
m
b
d
a
-
n
a
m
e
d
[
X
]
∨
l
a
m
b
d
a
-
a
n
o
n
[
X
]
→
l
i
f
t
-
c
h
o
i
c
e
[
X
]
=
X
{\displaystyle \operatorname {lambda-named} [X]\lor \operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X}
l
i
f
t
-
c
h
o
i
c
e
[
λ
F
.
X
]
=
l
i
f
t
-
c
h
o
i
c
e
[
X
]
{\displaystyle \operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]}
l
i
f
t
-
c
h
o
i
c
e
[
M
]
≠
none
→
l
i
f
t
-
c
h
o
i
c
e
[
M
N
]
=
l
i
f
t
-
c
h
o
i
c
e
[
M
]
{\displaystyle \operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]}
l
i
f
t
-
c
h
o
i
c
e
[
M
N
]
=
l
i
f
t
-
c
h
o
i
c
e
[
N
]
{\displaystyle \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]}
l
i
f
t
-
c
h
o
i
c
e
[
V
]
=
none
{\displaystyle \operatorname {lift-choice} [V]=\operatorname {none} }
例えば、
例 例えば、 Yコンビネータは 、
λ
f
.
(
λ
x
.
f
(
x
x
)
)
(
λ
x
.
f
(
x
x
)
)
{\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}
次のように持ち上げられる。
let
x
f
y
=
f
(
y
y
)
∧
q
x
f
=
f
(
(
x
f
)
(
x
f
)
)
in
q
x
{\displaystyle \operatorname {let} x\ f\ y=f\ (y\ y)\land q\ x\ f=f\ ((x\ f)\ (x\ f))\operatorname {in} q\ x}
パラメータを削除した後、
let
x
f
y
=
f
(
y
y
)
∧
q
f
=
f
(
(
x
f
)
(
x
f
)
)
in
q
{\displaystyle \operatorname {let} x\ f\ y=f\ (y\ y)\land q\ f=f\ ((x\ f)\ (x\ f))\operatorname {in} q}
ラムダ式として（ let式からラムダ式への変換 を参照）、
(
λ
x
.
(
λ
q
.
q
)
λ
f
.
f
(
x
f
)
(
x
f
)
)
λ
f
.
λ
y
.
f
(
y
y
)
{\displaystyle (\lambda x.(\lambda q.q)\ \lambda f.f\ (x\ f)\ (x\ f))\ \lambda f.\lambda y.f\ (y\ y)}
匿名関数のみを持ち上げる場合、Yコンビネータは、
let
p
f
x
=
f
(
x
x
)
∧
q
p
f
=
(
p
f
)
(
p
f
)
in
q
p
{\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p}
パラメータを削除した後、
let
p
f
x
=
f
(
x
x
)
∧
q
f
=
(
p
f
)
(
p
f
)
in
q
{\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ f=(p\ f)\ (p\ f)\operatorname {in} q}
ラムダ式として、
(
λ
p
.
(
λ
q
.
q
)
λ
f
.
(
p
f
)
(
p
f
)
)
λ
f
.
λ
x
.
f
(
x
x
)
{\displaystyle (\lambda p.(\lambda q.q)\ \lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)}
リフトのために選択される最初のサブ式は です 。これにより、ラムダ式が に変換され 、方程式 が作成されます 。
λ
x
.
f
(
x
x
)
{\displaystyle \lambda x.f\ (x\ x)}
λ
f
.
(
p
f
)
(
p
f
)
{\displaystyle \lambda f.(p\ f)\ (p\ f)}
p
f
x
=
f
(
x
x
)
{\displaystyle p\ f\ x=f(x\ x)}
リフトのために選択される 2 番目のサブ式は です 。これにより、ラムダ式が に変換され 、方程式 が作成されます 。
λ
f
.
(
p
f
)
(
p
f
)
{\displaystyle \lambda f.(p\ f)\ (p\ f)}
q
p
{\displaystyle q\ p}
q
p
f
=
(
p
f
)
(
p
f
)
{\displaystyle q\ p\ f=(p\ f)\ (p\ f)}
そしてその結果は、
let
p
f
x
=
f
(
x
x
)
∧
q
p
f
=
(
p
f
)
(
p
f
)
in
q
p
{\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\ }
驚くべきことに、この結果は、名前付き関数の持ち上げから得られる結果よりも単純です。
実行 関数を K に適用し、
{
λ
f
.
(
λ
x
.
f
(
x
x
)
)
(
λ
x
.
f
(
x
x
)
)
K
let
p
f
x
=
f
(
x
x
)
∧
q
p
f
=
(
p
f
)
(
p
f
)
in
q
p
K
(
λ
x
.
K
(
x
x
)
)
(
λ
x
.
K
(
x
x
)
)
let
p
f
x
=
f
(
x
x
)
∧
q
p
f
=
(
p
f
)
(
p
f
)
in
p
K
(
p
K
)
K
(
(
λ
x
.
K
(
x
x
)
)
(
λ
x
.
K
(
x
x
)
)
)
let
p
f
x
=
f
(
x
x
)
∧
q
p
f
=
p
f
(
p
f
)
in
K
(
p
K
(
p
K
)
)
{\displaystyle {\begin{cases}\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\ K&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} \ q\ p\ K\\(\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} \ p\ K\ (p\ K)\\K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x)))&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=p\ f\ (p\ f)\ \operatorname {in} \ K\ (p\ K\ (p\ K))\\\end{cases}}}
それで、
(
λ
x
.
K
(
x
x
)
)
(
λ
x
.
K
(
x
x
)
)
=
K
(
(
λ
x
.
K
(
x
x
)
)
(
λ
x
.
K
(
x
x
)
)
)
)
{\displaystyle (\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))=K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))))\ }
または
p
K
(
p
K
)
=
K
(
p
K
(
p
K
)
)
{\displaystyle p\ K\ (p\ K)=K\ (p\ K\ (p\ K))}
Y-コンビネータは、そのパラメータ (関数) を自身に対して繰り返し呼び出します。関数に 固定点 がある場合、その値は定義されます。ただし、関数が終了することはありません。
ラムダ計算におけるラムダドロップ ラムダドロップ [4] は関数のスコープを小さくし、縮小されたスコープのコンテキストを使用して関数のパラメータ数を減らすことです。パラメータ数を減らすと関数が理解しやすくなります。
ラムダ リフティングのセクションでは、最初にリフティングを行い、次に結果のラムダ式を再帰方程式に変換するメタ関数について説明しました。ラムダ ドロップ メタ関数は、最初に再帰方程式をラムダ抽象に変換し、次に結果のラムダ式をラムダ抽象へのすべての参照をカバーする最小のスコープにドロップすることで、逆の処理を実行します。
ラムダドロップは2つのステップで実行されます。
ラムダドロップ ラムダ ドロップは、プログラムの一部である式に適用されます。ドロップは、ドロップが除外される一連の式によって制御されます。
l
a
m
b
d
a
-
d
r
o
p
-
o
p
[
L
,
P
,
X
]
=
P
[
L
:=
d
r
o
p
-
p
a
r
a
m
s
-
t
r
a
n
[
s
i
n
k
-
t
e
s
t
[
L
,
X
]
]
]
{\displaystyle \operatorname {lambda-drop-op} [L,P,X]=P[L:=\operatorname {drop-params-tran} [\operatorname {sink-test} [L,X]]]}
どこ、
L は 削除されるラムダ抽象化です。 P はプログラムです X は 削除から除外される式のセットです。
ラムダドロップ変換は、式内のすべての抽象化をシンクします。シンクは、式のセット内の式からは除外されます。
l
a
m
b
d
a
-
d
r
o
p
-
t
r
a
n
[
L
,
X
]
=
d
r
o
p
-
p
a
r
a
m
s
-
t
r
a
n
[
s
i
n
k
-
t
r
a
n
[
d
e
-
l
e
t
[
L
,
X
]
]
]
{\displaystyle \operatorname {lambda-drop-tran} [L,X]=\operatorname {drop-params-tran} [\operatorname {sink-tran} [\operatorname {de-let} [L,X]]]}
どこ、
L は 変換される式です。 X は ドロップから除外されるサブ式のセットです。 sink-tranは 各抽象化を最も内側から順にシンクし、
{
s
i
n
k
-
t
r
a
n
[
(
λ
N
.
B
)
Y
,
X
]
=
s
i
n
k
-
t
e
s
t
[
(
λ
N
.
s
i
n
k
-
t
r
a
n
[
B
]
)
s
i
n
k
-
t
r
a
n
[
Y
]
,
X
]
s
i
n
k
-
t
r
a
n
[
λ
N
.
B
,
X
]
=
λ
N
.
s
i
n
k
-
t
r
a
n
[
B
,
X
]
s
i
n
k
-
t
r
a
n
[
M
N
,
X
]
=
s
i
n
k
-
t
r
a
n
[
M
,
X
]
s
i
n
k
-
t
r
a
n
[
M
,
X
]
s
i
n
k
-
t
r
a
n
[
V
,
X
]
=
V
{\displaystyle {\begin{cases}\operatorname {sink-tran} [(\lambda N.B)\ Y,X]=\operatorname {sink-test} [(\lambda N.\operatorname {sink-tran} [B])\ \operatorname {sink-tran} [Y],X]\\\operatorname {sink-tran} [\lambda N.B,X]=\lambda N.\operatorname {sink-tran} [B,X]\\\operatorname {sink-tran} [M\ N,X]=\operatorname {sink-tran} [M,X]\ \operatorname {sink-tran} [M,X]\\\operatorname {sink-tran} [V,X]=V\end{cases}}}
抽象化の沈没 シンクとは、ラムダ抽象化を可能な限り内側に移動して、変数へのすべての参照の外側に留まるようにすることです。
応用例 - 4件。
{
E
∉
FV
[
G
]
∧
E
∉
FV
[
H
]
→
sink
[
(
λ
E
.
G
H
)
Y
,
X
]
=
G
H
E
∉
FV
[
G
]
∧
E
∈
FV
[
H
]
→
sink
[
(
λ
E
.
G
H
)
Y
,
X
]
=
s
i
n
k
-
t
e
s
t
[
G
s
i
n
k
-
t
e
s
t
[
(
λ
E
.
H
)
Y
,
X
]
]
E
∈
FV
[
G
]
∧
E
∉
FV
[
H
]
→
sink
[
(
λ
E
.
G
H
)
Y
,
X
]
=
(
s
i
n
k
-
t
e
s
t
[
(
λ
E
.
G
)
Y
,
X
]
)
H
E
∈
FV
[
G
]
∧
E
∈
FV
[
H
]
→
sink
[
(
λ
E
.
G
H
)
Y
,
X
]
=
(
λ
E
.
G
H
)
Y
{\displaystyle {\begin{cases}E\not \in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=G\ H\\E\not \in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=\operatorname {sink-test} [G\ \operatorname {sink-test} [(\lambda E.H)\ Y,X]]\\E\in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\operatorname {sink-test} [(\lambda E.G)\ Y,X])\ H\\E\in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\lambda E.G\ H)\ Y\end{cases}}}
抽象化 。名前の変更を使用して、変数名がすべて異なるようにします。
V
≠
W
→
sink
[
(
λ
V
.
λ
W
.
E
)
Y
,
X
]
=
λ
W
.
s
i
n
k
-
t
e
s
t
[
(
λ
V
.
E
)
Y
,
X
]
{\displaystyle V\neq W\to \operatorname {sink} [(\lambda V.\lambda W.E)\ Y,X]=\lambda W.\operatorname {sink-test} [(\lambda V.E)\ Y,X]}
変数 - 2 件。
E
≠
V
→
sink
[
(
λ
E
.
V
)
Y
,
X
]
=
V
{\displaystyle E\neq V\to \operatorname {sink} [(\lambda E.V)\ Y,X]=V}
E
=
V
→
sink
[
(
λ
E
.
V
)
Y
,
X
]
=
Y
{\displaystyle E=V\to \operatorname {sink} [(\lambda E.V)\ Y,X]=Y}
シンクテストは式をドロップから除外します。
L
∈
X
→
s
i
n
k
-
t
e
s
t
[
L
,
X
]
=
L
{\displaystyle L\in X\to \operatorname {sink-test} [L,X]=L}
L
∉
X
→
s
i
n
k
-
t
e
s
t
[
L
,
X
]
=
sink
[
L
,
X
]
{\displaystyle L\not \in X\to \operatorname {sink-test} [L,X]=\operatorname {sink} [L,X]}
例
パラメータの削除 パラメータドロップとは、関数内の位置に合わせて関数を最適化することです。ラムダリフトでは、関数をコンテキスト外に移動するために必要なパラメータが追加されました。ドロップでは、このプロセスが逆転し、自由な変数を含む余分なパラメータが削除されることがあります。
パラメータの削除とは、関数から不要なパラメータを削除することです。関数に渡される実際のパラメータは常に同じ式です。式の自由変数も、関数が定義されている場所では自由である必要があります。この場合、削除されたパラメータは、関数定義の本体の式に置き換えられます。これにより、パラメータは不要になります。
例えば、
λ
m
,
p
,
q
.
(
λ
g
.
λ
n
.
(
n
(
g
m
p
n
)
(
g
q
p
n
)
)
)
λ
x
.
λ
o
.
λ
y
.
o
x
y
{\displaystyle \lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y}
この例では、仮パラメータ o の実パラメータは常に p です。 p は式全体で自由変数なので、パラメータは削除できます。仮パラメータ y の実パラメータは常に n です。ただし、 n は ラムダ抽象化でバインドされています。そのため、このパラメータは削除できません。
パラメータを削除した結果は、
d
r
o
p
-
p
a
r
a
m
s
-
t
r
a
n
[
λ
m
,
p
,
q
.
(
λ
g
.
λ
n
.
n
(
g
m
p
n
)
(
g
q
p
n
)
)
λ
x
.
λ
o
.
λ
y
.
o
x
y
{\displaystyle \operatorname {drop-params-tran} [\lambda m,p,q.(\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n))\ \lambda x.\lambda o.\lambda y.o\ x\ y}
≡
λ
m
,
p
,
q
.
(
λ
g
.
λ
n
.
n
(
g
m
n
)
(
g
q
n
)
)
λ
x
.
λ
y
.
p
x
y
{\displaystyle \equiv \lambda m,p,q.(\lambda g.\lambda n.n\ (g\ m\ n)\ (g\ q\ n))\ \lambda x.\lambda y.p\ x\ y}
主な例としては、
d
r
o
p
-
p
a
r
a
m
s
-
t
r
a
n
[
λ
f
.
(
λ
p
.
(
p
f
)
(
p
f
)
)
(
λ
f
.
λ
x
.
f
(
x
x
)
)
]
{\displaystyle \operatorname {drop-params-tran} [\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]}
≡
λ
f
.
(
λ
p
.
p
p
)
(
λ
x
.
f
(
x
x
)
)
{\displaystyle \equiv \lambda f.(\lambda p.p\ p)\ (\lambda x.f\ (x\ x))}
drop-params-tran の定義は 、
d
r
o
p
-
p
a
r
a
m
s
-
t
r
a
n
[
L
]
≡
(
d
r
o
p
-
p
a
r
a
m
s
[
L
,
D
,
F
V
[
L
]
,
[
]
]
)
{\displaystyle \operatorname {drop-params-tran} [L]\equiv (\operatorname {drop-params} [L,D,FV[L],[]])}
どこ、
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
[
L
,
D
,
V
,
_
]
{\displaystyle \operatorname {build-param-list} [L,D,V,\_]}
パラメータリストを作成する 関数を定義する抽象化ごとに、名前を削除するかどうかの決定に必要な情報を構築します。この情報は、各パラメータ、パラメータ名、実際の値の式、およびすべての式が同じ値を持つことを示す情報について説明します。
例えば、
λ
m
,
p
,
q
.
(
λ
g
.
λ
n
.
(
n
(
g
m
p
n
)
(
g
q
p
n
)
)
)
λ
x
.
λ
o
.
λ
y
.
o
x
y
{\displaystyle \lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y}
関数g のパラメータ は、
各抽象化は一意の名前に変更され、パラメータ リストは抽象化の名前に関連付けられます。たとえば、 g にはパラメータ リストがあります。
D
[
g
]
=
[
[
x
,
false
,
_
]
,
[
o
,
_
,
p
]
,
[
y
,
_
,
n
]
]
{\displaystyle D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]}
build-param-lists は、 式を走査して、式のすべてのリストを構築します。4 つのパラメーターがあります。
分析対象のラムダ式。 名前のテーブルパラメータリスト。 パラメータの値の表。 返されるパラメータリストは、 抽象化 - 形式のラムダ式 が分析され、関数のパラメータの名前が抽出されます。
(
λ
N
.
S
)
L
{\displaystyle (\lambda N.S)\ L}
{
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
(
λ
N
.
S
)
L
,
D
,
V
,
R
]
≡
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
S
,
D
,
V
,
R
]
∧
b
u
i
l
d
-
l
i
s
t
[
L
,
D
,
V
,
D
[
N
]
]
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
λ
N
.
S
,
D
,
V
,
R
]
≡
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
S
,
D
,
V
,
R
]
{\displaystyle {\begin{cases}\operatorname {build-param-lists} [(\lambda N.S)\ L,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\land \operatorname {build-list} [L,D,V,D[N]]\\\operatorname {build-param-lists} [\lambda N.S,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\end{cases}}}
名前を見つけて、その名前のパラメータリストの構築を開始し、仮パラメータ名を入力します。また、式の本体から実際のパラメータリストを受け取り、それをこの式の実際のパラメータリストとして返します。
{
b
u
i
l
d
-
l
i
s
t
[
λ
P
.
B
,
D
,
V
,
[
X
,
_
,
_
]
::
L
]
≡
b
u
i
l
d
-
l
i
s
t
[
B
,
D
,
V
,
L
]
b
u
i
l
d
-
l
i
s
t
[
B
,
D
,
V
,
[
]
]
≡
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
B
,
D
,
V
,
_
]
{\displaystyle {\begin{cases}\operatorname {build-list} [\lambda P.B,D,V,[X,\_,\_]::L]\equiv \operatorname {build-list} [B,D,V,L]\\\operatorname {build-list} [B,D,V,[]]\equiv \operatorname {build-param-lists} [B,D,V,\_]\end{cases}}}
変数 - 関数の呼び出し。
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
N
,
D
,
V
,
D
[
N
]
]
{\displaystyle \operatorname {build-param-lists} [N,D,V,D[N]]}
関数名またはパラメータの場合は、この名前のパラメータ リストを出力することによって、実際のパラメータ リストの入力を開始します。
アプリケーション - アプリケーション (関数呼び出し) が処理され、実際のパラメータの詳細が抽出されます。
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
E
P
,
D
,
V
,
R
]
≡
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
E
,
D
,
V
,
T
]
∧
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
P
,
D
,
V
,
K
]
{\displaystyle \operatorname {build-param-lists} [E\ P,D,V,R]\equiv \operatorname {build-param-lists} [E,D,V,T]\land \operatorname {build-param-lists} [P,D,V,K]}
∧
T
=
[
F
,
S
,
A
]
::
R
∧
(
S
⟹
(
equate
[
A
,
P
]
∧
V
[
F
]
=
A
)
)
∧
D
[
F
]
=
K
{\displaystyle \land T=[F,S,A]::R\land (S\implies (\operatorname {equate} [A,P]\land V[F]=A))\land D[F]=K}
式のパラメータ リストとパラメータを取得します。式のパラメータ リストからパラメータ レコードを取得し、現在のパラメータ値がこのパラメータと一致するかどうかを確認します。後で確認するときに使用するために、パラメータ名の値を記録します。
{
equate
[
A
,
N
]
≡
A
=
N
∨
(
def
[
V
[
N
]
]
∧
A
=
V
[
N
]
)
if
N
is a variable.
equate
[
A
,
E
]
≡
A
=
E
otherwise.
{\displaystyle {\begin{cases}\operatorname {equate} [A,N]\equiv A=N\lor (\operatorname {def} [V[N]]\land A=V[N])&{\text{if }}N{\text{ is a variable.}}\\\operatorname {equate} [A,E]\equiv A=E&{\text{otherwise.}}\end{cases}}}
上記のロジックは、その動作方法が非常に微妙です。同じ値インジケーターが true に設定されることはありません。すべての値が一致しない場合にのみ、 false に設定されます。値は、 S を使用して S に許可されるブール値のセットを構築することによって取得されます 。 true がメンバーである場合、このパラメーターのすべての値は等しく、パラメーターは削除される可能性があります。
ask
[
S
]
≡
S
∈
{
X
:
X
=
S
}
{\displaystyle \operatorname {ask} [S]\equiv S\in \{X:X=S\}}
同様に、 def は 集合論を使用して、変数に値が与えられているかどうかを照会します。
def
[
F
]
≡
|
{
X
:
X
=
F
}
|
{\displaystyle \operatorname {def} [F]\equiv |\{X:X=F\}|}
Let - Let 式。
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
[
let
V
:
E
in
L
,
D
,
V
,
_
]
≡
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
[
E
,
D
,
V
,
_
]
∧
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
[
L
,
D
,
V
,
_
]
{\displaystyle \operatorname {build-param-list} [\operatorname {let} V:E\operatorname {in} L,D,V,\_]\equiv \operatorname {build-param-list} [E,D,V,\_]\land \operatorname {build-param-list} [L,D,V,\_]}
そして - 「let」で使用します。
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
E
∧
F
,
D
,
V
,
_
]
≡
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
E
,
D
,
V
,
_
]
∧
b
u
i
l
d
-
p
a
r
a
m
-
l
i
s
t
s
[
F
,
D
,
V
,
_
]
{\displaystyle \operatorname {build-param-lists} [E\land F,D,V,\_]\equiv \operatorname {build-param-lists} [E,D,V,\_]\land \operatorname {build-param-lists} [F,D,V,\_]}
例 たとえば、パラメータリストを構築する場合、
λ
m
,
p
,
q
.
(
λ
g
.
λ
n
.
(
n
(
g
m
p
n
)
(
g
q
p
n
)
)
)
λ
x
.
λ
o
.
λ
y
.
o
x
y
{\displaystyle \lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y}
与える、
D
[
g
]
=
[
[
x
,
false
,
_
]
,
[
o
,
true
,
p
]
,
[
y
,
true
,
n
]
]
{\displaystyle D[g]=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]}
パラメータoは省略され、
λ
m
,
p
,
q
.
(
λ
g
.
λ
n
.
(
n
(
g
m
n
)
(
g
q
n
)
)
)
λ
x
.
λ
y
.
p
x
y
{\displaystyle \lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ n)\ (g\ q\ n)))\ \lambda x.\lambda y.p\ x\ y}
もう一つの例は、
λ
f
.
(
(
λ
p
.
f
(
p
p
f
)
)
(
λ
q
.
λ
x
.
x
(
q
q
x
)
)
{\displaystyle \lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x))}
ここでxはfに等しい。パラメータリストのマッピングは、
D
[
p
]
=
[
[
q
,
_
,
p
]
,
[
x
,
_
,
f
]
]
{\displaystyle D[p]=[[q,\_,p],[x,\_,f]]}
パラメータxは省略され、
λ
f
.
(
(
λ
q
.
f
(
q
q
)
)
(
λ
q
.
f
(
q
q
)
)
{\displaystyle \lambda f.((\lambda q.f\ (q\ q))\ (\lambda q.f\ (q\ q))}
ドロップパラメータ ビルドパラメータリストによって得られた情報を使用して、不要になった実際のパラメータを削除します。drop -params には、
パラメータを削除するラムダ式。 変数名とパラメータ リスト (ビルド パラメータ リストに組み込まれている) のマッピング。 ラムダ式内の自由な変数のセット。 返されるパラメータ リスト。アルゴリズム内で内部的に使用されるパラメータ。 抽象化
d
r
o
p
-
p
a
r
a
m
s
[
(
λ
N
.
S
)
L
,
D
,
V
,
R
]
≡
(
λ
N
.
d
r
o
p
-
p
a
r
a
m
s
[
S
,
D
,
F
,
R
]
)
d
r
o
p
-
f
o
r
m
a
l
[
D
[
N
]
,
L
,
F
]
{\displaystyle \operatorname {drop-params} [(\lambda N.S)\ L,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])\ \operatorname {drop-formal} [D[N],L,F]}
どこ、
F
=
F
V
[
(
λ
N
.
S
)
L
]
{\displaystyle F=FV[(\lambda N.S)\ L]}
d
r
o
p
-
p
a
r
a
m
s
[
λ
N
.
S
,
D
,
V
,
R
]
≡
(
λ
N
.
d
r
o
p
-
p
a
r
a
m
s
[
S
,
D
,
F
,
R
]
)
{\displaystyle \operatorname {drop-params} [\lambda N.S,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])}
どこ、
F
=
F
V
[
λ
N
.
S
]
{\displaystyle F=FV[\lambda N.S]}
変数
d
r
o
p
-
p
a
r
a
m
s
[
N
,
D
,
V
,
D
[
N
]
]
≡
N
{\displaystyle \operatorname {drop-params} [N,D,V,D[N]]\equiv N}
関数名またはパラメータの場合は、この名前のパラメータ リストを出力することによって、実際のパラメータ リストの入力を開始します。
アプリケーション - アプリケーション（関数呼び出し）が処理され、
(
def
[
F
]
∧
ask
[
S
]
∧
F
V
[
A
]
⊂
V
)
→
d
r
o
p
-
p
a
r
a
m
s
[
E
P
,
D
,
V
,
R
]
≡
d
r
o
p
-
p
a
r
a
m
s
[
E
,
D
,
V
,
[
F
,
S
,
A
]
::
R
]
{\displaystyle (\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]}
¬
(
def
[
F
]
∧
ask
[
S
]
∧
F
V
[
A
]
⊂
V
)
→
d
r
o
p
-
p
a
r
a
m
s
[
E
P
,
D
,
V
,
R
]
≡
d
r
o
p
-
p
a
r
a
m
s
[
E
,
D
,
V
,
[
F
,
S
,
A
]
::
R
]
d
r
o
p
-
p
a
r
a
m
s
[
P
,
D
,
V
,
_
]
{\displaystyle \neg (\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]\ \operatorname {drop-params} [P,D,V,\_]}
Let - Let 式。
d
r
o
p
-
p
a
r
a
m
s
[
let
V
:
E
in
L
]
≡
let
V
:
d
r
o
p
-
p
a
r
a
m
s
[
E
,
D
,
F
V
[
E
]
,
[
]
]
in
d
r
o
p
-
p
a
r
a
m
s
[
L
,
D
,
F
V
[
L
]
,
[
]
]
{\displaystyle \operatorname {drop-params} [\operatorname {let} V:E\operatorname {in} L]\equiv \operatorname {let} V:\operatorname {drop-params} [E,D,FV[E],[]]\operatorname {in} \operatorname {drop-params} [L,D,FV[L],[]]}
そして - 「let」で使用します。
d
r
o
p
-
p
a
r
a
m
s
[
E
∧
F
,
D
,
V
,
_
]
≡
d
r
o
p
-
p
a
r
a
m
s
[
E
,
D
,
V
,
_
]
∧
d
r
o
p
-
p
a
r
a
m
s
[
F
,
D
,
V
,
_
]
{\displaystyle \operatorname {drop-params} [E\land F,D,V,\_]\equiv \operatorname {drop-params} [E,D,V,\_]\land \operatorname {drop-params} [F,D,V,\_]}
drop-formalは ドロップリストの内容に基づいて仮パラメータを削除します。そのパラメータは、
ドロップリスト、 関数定義（ラムダ抽象化）。 関数定義からの自由変数。 ドロップフォーマル は次のように定義されます。
(
ask
[
S
]
∧
F
V
[
A
]
⊂
V
)
→
d
r
o
p
-
f
o
r
m
a
l
[
[
F
,
S
,
A
]
::
Z
,
λ
F
.
Y
,
V
]
≡
d
r
o
p
-
f
o
r
m
a
l
[
[
F
,
S
,
A
]
::
Z
,
Y
[
F
:=
A
]
,
L
]
{\displaystyle (\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \operatorname {drop-formal} [[F,S,A]::Z,Y[F:=A],L]}
¬
(
ask
[
S
]
∧
F
V
[
A
]
⊂
V
)
→
d
r
o
p
-
f
o
r
m
a
l
[
[
F
,
S
,
A
]
::
Z
,
λ
F
.
Y
,
V
]
≡
λ
F
.
d
r
o
p
-
f
o
r
m
a
l
[
[
F
,
S
,
A
]
::
Z
,
Y
,
V
]
{\displaystyle \neg (\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \lambda F.\operatorname {drop-formal} [[F,S,A]::Z,Y,V]}
d
r
o
p
-
f
o
r
m
a
l
[
Z
,
Y
,
V
]
≡
Y
{\displaystyle \operatorname {drop-formal} [Z,Y,V]\equiv Y}
それは次のように説明できる。
すべての実際のパラメータが同じ値を持ち、その値のすべての自由変数が関数の定義に使用できる場合は、パラメータを削除し、古いパラメータをその値に置き換えます。 それ以外の場合はパラメータを削除しないでください。 それ以外の場合は関数の本体を返します。
例 Yコンビネータの関数定義から始めると、
let
p
f
x
=
f
(
x
x
)
∧
q
p
f
=
(
p
f
)
(
p
f
)
in
q
p
{\displaystyle \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\ }
Yコンビネータを 返す 。
λ
f
.
(
λ
x
.
f
(
x
x
)
)
(
λ
x
.
f
(
x
x
)
)
{\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}
参照
参考文献
^ Johnsson, Thomas (1985). 「ラムダリフティング: プログラムから再帰方程式への変換」。Jouannaud, JP (編) 関数型プログラミング言語とコンピュータアーキテクチャ。FPCA 1985 。コンピュータサイエンスの講義ノート。第 201 巻。Springer。CiteSeerX 10.1.1.48.4346 。doi : 10.1007 / 3-540-15975-4_37。ISBN 3-540-15975-4 。 ^ Morazán, Marco T.; Schultz, Ulrik P. (2008)、「2次時間での最適ラムダリフティング」、 関数型言語の実装と応用 - 改訂選定論文 、pp. 37–56、 doi :10.1007/978-3-540-85373-2_3、 ISBN
978-3-540-85372-5
^ Danvy, O.; Schultz, UP (1997). 「ラムダドロップ」. ACM SIGPLAN Notices . 32 (12): 90. doi : 10.1145/258994.259007 . ^ Danvy, Olivier; Schultz, Ulrik P. (2000 年 10 月). 「ラムダドロップ: 再帰方程式をブロック構造のプログラムに変換する」 (PDF) . 理論計算機科学 . 248 (1–2): 243–287. CiteSeerX 10.1.1.16.3943 . doi :10.1016/S0304-3975(00)00054-2. BRICS-RS-99-27.
外部リンク Stack Overflow での説明 (JavaScript の例付き) Slonneger, Ken; Kurtz, Barry. 「5. let 式に関するいくつかの考察」 (PDF) 。 プログラミング言語の基礎 。アイオワ大学。 
![{\displaystyle L[G:=S]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7716db852899ef7e3eb2a00dbbea76bc11279afb)
![{\displaystyle \operatorname {lambda-lift-op} [S,L,P]=P[L:=\operatorname {lambda-lift} [S,L]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/86a9b305960adb74498604e9c37f66bbfcf05d3e)
![{\displaystyle \operatorname {lambda-lift} [S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[S:=G]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3635846f62855487eb4767ca61b049b1f4a4f756)
![{\displaystyle G=\operatorname {make-call} [V,\operatorname {FV} [S]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2f7cf6397a95ead3958ae3c2c46546c68090c8c1)
![{\displaystyle V\not \in \operatorname {vars} [\operatorname {let} F\operatorname {in} L]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/264dd7b3cb4c9c193be8086f22d1aaeea28b8d7c)
![{\displaystyle \operatorname {vars} [E]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/831fb83e65f1c55c14cda53cd64d3408a839eb32)
![{\displaystyle X\in V\to \operatorname {make-call} [H,V]\equiv \operatorname {make-call} [H,V\cap \neg \{X\}]\ X}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b19b6de06e3a1f6ae843c08c9b9b3051a06aed38)
![{\displaystyle \operatorname {make-call} [H,\{\}]\equiv H}](https://wikimedia.org/api/rest_v1/media/math/render/svg/38e285ad933a5c82fdd5e26059133cd963bc8c08)
![{\displaystyle \operatorname {lambda-lift} [(\lambda VE)\ S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[(\lambda VE)\ S:=E[V:=G]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/74df9bb76d1099ff595a3f035db5b3c5e2999de5)
![{\displaystyle \operatorname {lambda-lift-tran} [\lambda f.(\lambda xf\ (x\ x))\ (\lambda xf\ (x\ x))]\equiv \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3180efefe33e798accd80f1b2ec7be7e14e01e8c)
![{\displaystyle \operatorname {de-let} [\operatorname {lambda-lift-tran} [\lambda f.(\lambda xf\ (x\ x))\ (\lambda xf\ (x\ x))]]\equiv (\lambda p.(\lambda qq\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda xf\ (x\ x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7df5f5d483268c59fa6fa79c3291877531d23666)
![{\displaystyle {\begin{cases}\operatorname {lambda-lift-tran} [L]=\operatorname {drop-params-tran} [\operatorname {merge-let} [\operatorname {lambda-apply} [L]]]\\\operatorname {lambda-apply} [L]=\operatorname {lambda-process} [\operatorname {lift-choice} [L],L]\\\operatorname {lambda-process} [\operatorname {none} ,L]=L\\\operatorname {lambda-process} [S,L]=\operatorname {lambda-apply} [\operatorname {lambda-lift} [S,L]]\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/66491254fcaf9e2540a6e8944ba8ad98e6d3c456)
![{\displaystyle {\begin{cases}\operatorname {merge-let} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]=\operatorname {merge-let} [\operatorname {let} V,W:E\land F\operatorname {in} G]\\\operatorname {merge-let} [E]=E\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e505711245b478b575915872a22846d5b8032a90)
![{\displaystyle {\begin{cases}\operatorname {lambda-free} [\lambda FX]=\operatorname {false} \\\operatorname {lambda-free} [V]=\operatorname {true} \\\operatorname {lambda-free} [M\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-free} [N]\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/43bce522c7908af771da74a390297711e77d894a)
![{\displaystyle {\begin{cases}\operatorname {lambda-anon} [\lambda FX]=\operatorname {lambda-free} [X]\lor \operatorname {lambda-anon} [X]\\\operatorname {lambda-anon} [V]=\operatorname {false} \\\operatorname {lambda-anon} [M\ N]=\operatorname {false} \end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1b95ecbd473b221f697c239b21255a62ea02297)
![{\displaystyle \operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0127c36abd044ce9c24b2ddada7c3b5676cd1f86)
![{\displaystyle \operatorname {lift-choice} [\lambda FX]=\operatorname {lift-choice} [X]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c1b747013d23868d55fec0c0168a315be52ee66d)
![{\displaystyle \operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b8ebc4ea96a74fb8a0da9f0e439e366216c461f4)
![{\displaystyle \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e1fa298cb12dfcfe8cc2a80e1980d93960b43ce4)
![{\displaystyle \operatorname {lift-choice} [V]=\operatorname {none} }](https://wikimedia.org/api/rest_v1/media/math/render/svg/fb3ca4e4969c8a2484d9918a4dc7d58aea486cb1)
![{\displaystyle {\begin{array}{l}\operatorname {lambda-named} [(\lambda FM)\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-anon} [N]\\\operatorname {lambda-named} [\lambda FX]=\operatorname {false} \\\operatorname {lambda-named} [V]=\operatorname {false} \end{array}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f6c89ff75776ec9a758cb5dfe023ecaf05b46d32)
![{\displaystyle \operatorname {lambda-named} [X]\lor \operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bc690650c2d14ce90cb3e2ccb5468377b9e7d4f2)
![{\displaystyle \operatorname {lambda-drop-op} [L,P,X]=P[L:=\operatorname {drop-params-tran} [\operatorname {sink-test} [L,X]]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/27de3976b9b43faf9c172323272b713186d81dc6)
![{\displaystyle \operatorname {lambda-drop-tran} [L,X]=\operatorname {drop-params-tran} [\operatorname {sink-tran} [\operatorname {de-let} [L,X]]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9a9af29cdb89755330111813a37d101b105d0d93)
![{\displaystyle {\begin{cases}\operatorname {sink-tran} [(\lambda NB)\ Y,X]=\operatorname {sink-test} [(\lambda N.\operatorname {sink-tran} [B])\ \operatorname {sink-tran} [Y],X]\\\operatorname {sink-tran} [\lambda NB,X]=\lambda N.\operatorname {sink-tran} [B,X]\\\operatorname {sink-tran} [M\ N,X]=\operatorname {sink-tran} [M,X]\ \operatorname {sink-tran} [M,X]\\\operatorname {sink-tran} [V,X]=V\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97513c2fecfb9eacba686eff9b7e945795632429)
![{\displaystyle {\begin{cases}E\not \in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda EG\ H)\ Y,X]=G\ H\\E\not \in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda EG\ H)\ Y,X]=\operatorname {sink-test} [G\ \operatorname {sink-test} [(\lambda EH)\ Y,X]]\\E\in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda EG\ H)\ Y,X]=(\operatorname {sink-test} [(\lambda EG)\ Y,X])\ H\\E\in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda EG\ H)\ Y,X]=(\lambda EG\ H)\ Y\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d2049873e2315208fad245e5e430fcc185d786e5)
![{\displaystyle V\neq W\to \operatorname {sink} [(\lambda V.\lambda WE)\ Y,X]=\lambda W.\operatorname {sink-test} [(\lambda VE)\ Y,X]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/04db7c9bce9b7cc6f9392aedb8f74ec20322a386)
![{\displaystyle E\neq V\to \operatorname {sink} [(\lambda EV)\ Y,X]=V}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c514513bf5cefbd8c7f3e57ef82453c3d320caa5)
![{\displaystyle E=V\to \operatorname {シンク} [(\lambda EV)\ Y,X]=Y}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a393d1e4583899566ee0e11224e5d5c9e9bf92e5)
![{\displaystyle L\in X\to \operatorname {sink-test} [L,X]=L}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a2ed0d8d66482f29a5dbf8f2a0e72f99e6ad102b)
![{\displaystyle L\not \in X\to \operatorname {sink-test} [L,X]=\operatorname {sink} [L,X]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/008bb1f25d290d88c5079ef9abb796bb6307faa0)
![{\displaystyle \operatorname {drop-params-tran} [\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda xf\ (x\ x))]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fa67127ffd3481a55d52b254ead36bdd5bf2d8a2)
![{\displaystyle \operatorname {drop-params-tran} [L]\equiv (\operatorname {drop-params} [L,D,FV[L],[]])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7159e7b56a1b8f5bd9bb6b77d2d30d7b507467b8)
![{\displaystyle \operatorname {build-param-list} [L,D,V,\_]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7705cccf60d29665a881caf7680895ba27b39afa)
![{\displaystyle D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e0a09568d8c330802df4aa1853b329e3c7f36173)
![{\displaystyle {\begin{cases}\operatorname {build-param-lists} [(\lambda NS)\ L,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\land \operatorname {build-list} [L,D,V,D[N]]\\\operatorname {build-param-lists} [\lambda NS,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fe3fca310614795b43de1fcb0113e22885dd7aae)
![{\displaystyle {\begin{cases}\operatorname {build-list} [\lambda PB,D,V,[X,\_,\_]::L]\equiv \operatorname {build-list} [B,D,V,L]\\\operatorname {build-list} [B,D,V,[]]\equiv \operatorname {build-param-lists} [B,D,V,\_]\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6a8d939f9d1309cfafc0ae13a9ecc5fee8aeb4eb)
![{\displaystyle \operatorname {パラメータリストの作成} [N,D,V,D[N]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b23041cdcb8a8157801202a20ee90032721144af)
![{\displaystyle \operatorname {build-param-lists} [E\ P,D,V,R]\equiv \operatorname {build-param-lists} [E,D,V,T]\land \operatorname {build-param-lists} [P,D,V,K]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9ada884dd8d7c6fef85f5aaa7f34dec35c65b1e1)
![{\displaystyle \land T=[F,S,A]::R\land (S\implies (\operatorname {equate} [A,P]\land V[F]=A))\land D[F]=K}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9db5ac4c7e6d52eda80d5f35ce7c20de390f32ab)
![{\displaystyle {\begin{cases}\operatorname {equate} [A,N]\equiv A=N\lor (\operatorname {def} [V[N]]\land A=V[N])&{\text{if }}N{\text{ is a variable.}}\\\operatorname {equate} [A,E]\equiv A=E&{\text{otherwise.}}\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/362ae7798b92be1ea6ce821106ecb06a88806aa5)
![{\displaystyle \operatorname {ask} [S]\equiv S\in \{X:X=S\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2182d11819218934dde6797fb27fae7e90765a89)
![{\displaystyle \operatorname {def} [F]\equiv |\{X:X=F\}|}](https://wikimedia.org/api/rest_v1/media/math/render/svg/435272b0981b4a5a8349725b4108adf7ba9fd13f)
![{\displaystyle \operatorname {build-param-list} [\operatorname {let} V:E\operatorname {in} L,D,V,\_]\equiv \operatorname {build-param-list} [E,D,V,\_]\land \operatorname {build-param-list} [L,D,V,\_]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c0df3ab20a70b95844dd32192ccd7460f9032c79)
![{\displaystyle \operatorname {build-param-lists} [E\land F,D,V,\_]\equiv \operatorname {build-param-lists} [E,D,V,\_]\land \operatorname {build-param-lists} [F,D,V,\_]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/027b8521db6a82f697e9b6c3d90c8fda5a5d5011)
![{\displaystyle D[g]=[[x,\operatorname {偽} ,\_],[o,\operatorname {真} ,p],[y,\operatorname {真} ,n]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/27f5c0b372250a852802c2279113b4617c5b0b34)
![{\displaystyle D[p]=[[q,\_,p],[x,\_,f]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1da991103c8d1a0ecdda1808fdfe8c50855bb402)
![{\displaystyle \operatorname {drop-params} [(\lambda NS)\ L,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])\ \operatorname {drop-formal} [D[N],L,F]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/99aba550f80eeb0680206c6d210784af5086f33a)
![{\displaystyle F=FV[(\lambda NS)\ L]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/823a8c75779698f7e8d3bb31433d87ffe41e7f29)
![{\displaystyle \operatorname {drop-params} [\lambda NS,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e323ea82ded175bec1079f368d89a8c1c5faace9)
![{\displaystyle F=FV[\lambda NS]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dd6fc1c379ca519dac82d228b2174aff1c42f8a6)
![{\displaystyle \operatorname {drop-params} [N,D,V,D[N]]\equiv N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/69aee36ec7d514017ed0614d3220339f024f5a04)
![{\displaystyle (\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d6c6dec4e775ccfd57eb9cc96ec7c39261e6c1e9)
![{\displaystyle \neg (\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]\ \operatorname {drop-params} [P,D,V,\_]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c6820b50410d5cd2dac84a803212b9ab4be839b5)
![{\displaystyle \operatorname {drop-params} [\operatorname {let} V:E\operatorname {in} L]\equiv \operatorname {let} V:\operatorname {drop-params} [E,D,FV[E],[]]\operatorname {in} \operatorname {drop-params} [L,D,FV[L],[]]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e317339f316247242bd7581321e7596cb54ce7bf)
![{\displaystyle \operatorname {drop-params} [E\land F,D,V,\_]\equiv \operatorname {drop-params} [E,D,V,\_]\land \operatorname {drop-params} [F,D,V,\_]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e363abba3dd6d7dc20ba91036a9dd6a88145165f)
![{\displaystyle (\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda FY,V]\equiv \operatorname {drop-formal} [[F,S,A]::Z,Y[F:=A],L]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8a6c960f47a989fd6137a31cef8c44d56d69f3b0)
![{\displaystyle \neg (\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda FY,V]\equiv \lambda F.\operatorname {drop-formal} [[F,S,A]::Z,Y,V]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94cdd9a6017b3540edf73ca993c1adf3a517ce78)
![{\displaystyle \operatorname {drop-formal} [Z,Y,V]\equiv Y}](https://wikimedia.org/api/rest_v1/media/math/render/svg/854482d904bbd4418f04a70213ea6dcac7b58174)