プッシュ値による呼び出し

プログラミング言語理論において、call-by-push-value (CBPV) は、call-by-value (CBV) とcall-by-name (CBN)の評価戦略を組み込んだ中間言語です。CBPV は、2 つの主な型、「値」(+) と「計算」(-) を持つ極性化λ 計算として構成されています。 ^{[1] 2 つの型間の相互作用の制限により、}モナドやCPSと同様に、制御された評価順序が強制されます。計算には、非終了性、可変状態、非決定性などの計算効果を組み込むことができます。CBV と CBN から CBPV への自然な意味論保存変換があります。つまり、CBPV の意味論を与え、そのプロパティを証明すると、CBV と CBN の意味論とプロパティも暗黙的に確立されます。Paul Blain Levy は、いくつかの論文と博士論文で CBPV を定式化し、開発しました。^{[2] [3] [4]}

CBPV パラダイムは、「値が存在すると、計算が行う」というスローガンに基づいています。プレゼンテーションの 1 つの複雑な点は、値型にまたがる型変数と計算型にまたがる型変数を区別することです。この記事では、Levy に従って、計算を示すために下線を使用しています。したがって、(任意の) 値型ですが、計算型でもあります。^[4]一部の著者は、文字の異なるセットなど、他の規則を使用しています。^[5]${\displaystyle B}$${\displaystyle {\underline {B}}}$

正確な構成要素のセットは著者や微積分の目的によって異なりますが、次の構成要素が典型的です：^{[2] [4]}

• ラムダは、およびであるλx.M型の計算です。ラムダ アプリケーションまたは は、 およびである型の計算です。let バインディング構造は、計算内で、一致する型の値を値にバインドします 。${\displaystyle A\to {\underline {B}}}$${\displaystyle x:A}$${\displaystyle M:{\underline {B}}}$F VV'F${\displaystyle {\underline {B}}}$${\displaystyle V:A}$${\displaystyle F:A\to {\underline {B}}}$let { x_1 = V_1; ... }. Mx_1V_1${\displaystyle A_{1}}$M${\displaystyle {\underline {B}}}$
• サンクは、型の計算から構築されたthunk M型の値です。サンクの強制は計算です。サンク : の場合、 :です 。${\displaystyle U{\underline {A}}}$M${\displaystyle {\underline {A}}}$force X${\displaystyle {\underline {A}}}$X${\displaystyle U{\underline {A}}}$
• V型の値を計算 :としてラップすることもできます。このような計算は、 : として別の計算内で使用できます。ここで、 :  、および :は計算です。${\displaystyle A}$return V${\displaystyle FA}$M to x. N${\displaystyle {\underline {B}}}$M${\displaystyle FA}$N${\displaystyle {\underline {B}}}$
• 値には、タグと 0 個以上のサブ値から構成される代数データ型も含めることができます。一方、計算には分解パターン マッチが含まれますmatch V as { (1,...) in M_1, ... }。プレゼンテーションに応じて、ADT はバイナリの合計と積、ブール値のみに制限されるか、完全に省略される場合があります。

プログラムは型 の閉じた計算であり、 は基底ADT型である。^[4]${\displaystyle FA}$${\displaystyle A}$

のような式は、not true : bool表示的には意味をなします。しかし、上記の規則に従うと、notはパターンマッチングを使用してのみエンコードすることができ、それは計算になります。したがって、全体の式も計算でなければならず、 となります。同様に、計算を構築せずにからnot true : F boolを得る方法はありません。 CBPV を等式またはカテゴリ理論でモデル化する場合、このような構成は不可欠です。したがって、Levy は拡張された IR、「複素値を持つ CBPV」を定義します。この IR は、let バインディングを拡張して、値式内で値をバインドし、各節が値式を返すように値をパターンマッチングします。^[3]モデル化に加えて、このような構成により、CBPV でのプログラムの記述がより自然になります。^[2]1(1,2)

複素数値は操作意味論を複雑にし、特に複素数値を評価するタイミングを任意に決定する必要があります。複素数値の評価には副作用がないため、このような決定は意味論的な意味を持ちません。また、任意の計算または閉じた式を、複素数値のない同じ型と表記に構文的に変換することも可能です。^[3]そのため、多くのプレゼンテーションでは複素数値が省略されています。^[4]

CBV変換は、各式に対してCBPV値を生成します。CBV関数λx.M :は :に変換されます。CBVアプリケーション :は、評価の順序を明示的にするタイプの計算に変換されます。パターンマッチはに変換されます。値は必要に応じて でラップされますが、それ以外の場合は変更されません。^[2]一部の変換では、に変換するなど、順序付けが必要になる場合があります。^[4]${\displaystyle A\to _{v}B}$thunk λx.Mv${\displaystyle U(A^{v}\to FB^{v})}$M N${\displaystyle A}$Mv to f in Nv to x in x'(force f)${\displaystyle FA}$match V as { (1,...) in M_1, ... }Vv to z in match z as { (1,...) in M_1v, ... }returninl MM to x. return inl x

CBN変換は各式に対してCBPV計算を生成する。CBN関数λx.M :は変更されずに:を変換する 。CBNアプリケーション :は型 の計算に変換される。パターンマッチはCBNと同様に に変換される。ADT値は で囲まれるが、内部構造ではとも必要である。Levyの変換は を仮定しており、これは実際に成り立つ。^[2]${\displaystyle A\to B}$λx.MN${\displaystyle (UA^{n})\to X^{n}}$M N${\displaystyle C}$Mv (thunk Nv)${\displaystyle C^{n}}$match V as { (1,...) in M_1, ... }Vn to z in match z as { (1,...) in M_1n, ... }returnforcethunkM = force (thunk M)

CBPVを拡張して、可視的な共有を可能にする構造を導入することで、call-by-needをモデル化することも可能ですM need x. N。この構造は と似た意味を持ちますが、構造では のサンクが最大で1回評価される点がM name x. N = (λy.N[x ↦ (force y)])(thunk M)異なります。 ^[6]needM

一部の著者は、U 型コンストラクタ (サンク) ^[7]または F 型コンストラクタ (値を返す計算) のいずれかを削除することで、CBPV を簡素化できると指摘しています。^[8] Egger と Mogelberg は、合理化された構文と、計算から値への推論可能な変換の煩雑さを回避するという理由で、U を省略することを正当化しています。この選択により、計算型は値型のサブセットになり、関数型を値間の完全な関数空間に拡張することが自然になります。彼らは、この計算を「強化効果計算」と呼んでいます。この修正された計算は、双方向の意味保存変換を介して CBPV のスーパーセットに相当します。^[7] Ehrhard は対照的に、F 型コンストラクタを省略し、値を計算のサブセットにします。Ehrhard は、計算の意味をよりよく反映するために、計算を「一般型」に改名します。この修正された計算である「半極性化ラムダ計算」は、線形論理と密接な関係があります。^{[8] [9]}これは、CBPVの完全分極変異体のサブセットに双方向に翻訳することができる。^[10]

• 計算可能な関数のプログラミング