プッシュ値呼び出し

プログラミング言語理論において、プッシュ値呼び出し（CBPV）は、値呼び出し（CBV）と名前呼び出し（CBN）の評価戦略を組み込んだ中間言語です。CBPVは、「値」（+）と「計算」（-）という2つの主要な型を持つ極性λ計算として構造化されています。 [ 1 ] 2つの型間の相互作用に対する制約は、モナドやCPSと同様に、制御された評価順序を強制します。この計算は、非停止性、可変状態、非決定性などの計算効果を組み込むことができます。CBVとCBNからCBPVへの自然な意味論保存変換があります。これは、CBPVの意味論を与え、その特性を証明すると、暗黙的にCBVとCBNの意味論と特性も確立されることを意味します。ポール・ブレイン・レヴィは、いくつかの論文と博士論文でCBPVを定式化し、開発しました[ 2 ] [ 3 ] [ 4 ]

定義

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

具体的な構成は著者や微積分の用途によって異なりますが、次のような構成が一般的です。[ 2 ] [ 4 ]

  • ラムダλx.Mは 型 の計算であり、と です。ラムダ適用または は型 の計算であり、と です。let バインディング構造は、計算内で、一致する型 の値を値 にバインドします 。A→B_{\displaystyle A\to {\underline {B}}}×：A{\displaystyle x:A}M：B_{\displaystyle M:{\underline {B}}}F VV'FB_{\displaystyle {\underline {B}}}V：A{\displaystyle V:A}F：A→B_{\displaystyle F:A\to {\underline {B}}}let { x_1 = V_1; ... }. Mx_1V_1A1{\displaystyle A_{1}}MB_{\displaystyle {\underline {B}}}
  • サンクは、型の計算から構築されたthunk M型 の値です。サンクを強制することは 、サンク : に対して :という計算です。UA_{\displaystyle U{\underline {A}}}MA_{\displaystyle {\underline {A}}}force XA_{\displaystyle {\underline {A}}}XUA_{\displaystyle U{\underline {A}}}
  • V型の値を計算 :としてラップすることも可能です。このような計算は、 : （  : 、 :は計算）のように別の計算内で使用できます。A{\displaystyle A}return VFA{\displaystyle FA}M to x. NB_{\displaystyle {\underline {B}}}MFA{\displaystyle FA}NB_{\displaystyle {\underline {B}}}
  • 値には、タグと0個以上のサブ値から構成される代数データ型も含めることができます。一方、計算には分解パターンマッチが含まれますmatch V as { (1,...) in M_1, ... }。表現によっては、ADTは2進数の和と積、ブール値のみに限定されるか、完全に省略される場合があります。

プログラムは型 の閉じた計算であり、は基底ADT型である。[ 4 ]FA{\displaystyle FA}A{\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 ]A→vB{\displaystyle A\to _{v}B}thunk λx.MvU(Av→FBv){\displaystyle U(A^{v}\to FB^{v})}M NA{\displaystyle A}Mv to f in Nv to x in x'(force f)FA{\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 ]A→B{\displaystyle A\to B}λx.MN(UAn)→Xn{\displaystyle (UA^{n})\to X^{n}}M NC{\displaystyle C}Mv (thunk Nv)Cn{\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型コンストラクタ（値を返す計算）[ 8 ]のいずれかを削除することで、CBPVを簡素化できることを指摘しています。EggerとMogelbergは、合理化された構文と、計算から値への推論可能な変換の煩雑さを回避するという理由で、Uを省略することを正当化しています。この選択により、計算型は値型のサブセットになり、関数型を値間の完全な関数空間に拡張することが自然になります。彼らはこの計算を「Enriched Effects Calculus（強化効果計算）」と呼んでいます。この修正された計算は、双方向の意味保存変換を介してCBPVのスーパーセットと同等です。[ 7 ]対照的に、EhrhardはF型コンストラクタを省略し、値を計算のサブセットにします。Ehrhardは、意味をよりよく反映するために、計算を「一般型」に改名しましたこの修正された計算法「半分極ラムダ計算」は線形論理と密接な関係がある。[ 8 ] [ 9 ]これは双方向にCBPVの完全分極変種のサブセットに変換することができる。[ 10 ]

賞

ポール・ブレイン・レヴィは、CBPVに関する研究により、 2025年のアロンゾ・チャーチ賞を受賞しました。 [ 11 ]

参照

参考文献

  1. ^ Kavvos, GA; Morehouse, Edward; Licata, Daniel R.; Danner, Norman (2020年1月). 「call-by-push-valueによる関数型プログラムの再帰抽出」 . ACM on Programming Languagesの論文集. 4 (POPL): 1– 31. arXiv : 1911.04588 . doi : 10.1145/3371083 . ISSN  2475-1421 .
  2. ^ a b c d eブレイン・レヴィ、ポール (1999年4月). Call-by-P​​ush-Value: A Subsuming Paradigm (PDF) . Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy. Lecture Notes in Computer Science. Vol. 1581. pp.  228– 242.
  3. ^ a b c Levy, Paul Blain (2003). Call-by-push-value: a functional/imperative synthesis (PDF) . ドルドレヒト; ボストン: Kluwer Academic Publishers. ISBN 978-1-4020-1730-8。
  4. ^ a b c d e f Levy, Paul Blain ( 2022年4月). 「call-by-push-value」. ACM SIGLOG News . 9 (2): 7–29 . doi : 10.1145/3537668.3537670
  5. ^ Pédrot, Pierre-Marie; Tabareau, Nicolas (2020年1月). 「The fire triangle: how to mix replacement, dependent elimination, and effects」. Proceedings of the ACM on Programming Languages . 4 (POPL): 1– 28. doi : 10.1145/3371126 .
  6. ^ McDermott, Dylan; Mycroft, Alan (2019). 「拡張されたCall-by-P​​ush-Value：効果的なプログラムと評価順序に関する推論」.プログラミング言語とシステム. Springer International Publishing. pp.  235– 262. doi : 10.1007/978-3-030-17184-1_9 . ISBN 978-3-030-17184-1。
  7. ^ a b Egger, J.; Mogelberg, RE; Simpson, A. (2014年6月1日). 「エンリッチド効果計算：構文と意味論」(PDF) . Journal of Logic and Computation . 24 (3): 615– 654. doi : 10.1093/logcom/ exs025
  8. ^ a b Ehrhard, Thomas (2016). 「線形論理の観点から見たCall-By-Push-Value」.プログラミング言語とシステム. コンピュータサイエンス講義ノート. 第9632巻. pp.  202– 228. doi : 10.1007/978-3-662-49498-1_9 . ISBN 978-3-662-49497-4。
  9. ^ Chouquet, Jules; Tasson, Christine (2020). Call-By-Push-Value のテイラー展開．ライプニッツ国際情報科学会誌．第152巻．ダグストゥール城 – ライプニッツ情報科学センター．pp. 16:1–16:16. doi : 10.4230/LIPIcs.CSL.2020.16 . ISBN 978-3-95977-132-0。
  10. ^エールハルト、トーマス（2015年7月）、プッシュ値呼び出しFPCと線形論理におけるその解釈
  11. ^ https://siglog.org/winner-of-the-2025-alonzo-church-award/
「 https://en.wikipedia.org/w/index.php?title=Call-by-push-value&oldid=1329130832」より取得