用語の書き換え 項書き換えシステム では、書き換え戦略によって、項内のすべての還元可能な部分項（リデックス ）のうち、どれを還元（縮約）するかが指定されます。
用語書き換えのためのワンステップ戦略には以下が含まれます。[ 5 ]
左端-内側: 各ステップで、最も内側のredexの左端が縮約されます。ここで、最も内側のredexは、redexを含まないredexです[ 6 ] 左端-最外側: 各ステップで、最外側のredexの左端が縮約されます。ここで、最外側のredexは、どのredexにも含まれていないredexです[ 6 ]。 右端内側、右端外側：同様に 多段階戦略には以下が含まれます: [ 5 ]
parallel-innermost: すべての最内側のredexを同時に削減します。redexはペアごとに互いに素であるため、これは適切に定義されます。 平行最外端: 同様に グロス・クヌース還元[ 7 ] [ 5 ] 並列最外縮約とグロス・クヌース縮約は、ほぼ直交する項書き換えシステムすべてに対してハイパー正規化を 行う。つまり、これらの戦略は、連続する戦略の適用間に（有限個の）任意の縮約を実行しても、正規形が存在する場合は最終的に正規形に到達する。[ 8 ]
Strategoは、項書き換え戦略のプログラミングのために特別に設計されたドメイン固有言語です。 [ 9 ]
ラムダ計算 ラムダ計算 の文脈では、正規順序簡約は、 上記 の意味での最も左から最も外側の簡約を指します。[ 10 ] [ 11 ] [ 12 ]
左端削減は 、通常の順序削減を指す場合にも使用されることがあります。これは、先行順 走査の場合、概念が一致するためです。同様に、ラムダ項を文字列とみなした場合、最左端外側のリデックスは、開始文字が最も左にあるリデックスです。[ 13 ] [ 14 ] 中順走査 を使用して「左端」が定義される場合、概念は異なります。たとえば、次の用語では（ λ x 。 x Ω ） （ λ y 。 私 ） {\displaystyle (\lambda xx\Omega )(\lambda yI)} Ω 、 私 {\displaystyle \Omega ,I} ここで 定義されるように、順序通りの走査の最も左のredexはΩ {\displaystyle \Omega } [ 15 ]
適用順序簡約 とは、最も左から最も内側への簡約を指します。[ 10 ] [ 10 ] （ λ x 。 z ） （ （ λ w 。 w w w ） （ λ w 。 w w w ） ） → （ λ x 。 z ） （ （ λ w 。 w w w ） （ λ w 。 w w w ） （ λ w 。 w w w ） ） → （ λ x 。 z ） （ （ λ w 。 w w w ） （ λ w 。 w w w ） （ λ w 。 w w w ） （ λ w 。 w w w ） ） → （ λ x 。 z ） （ （ λ w 。 w w w ） （ λ w 。 w w w ） （ λ w 。 w w w ） （ λ w 。 w w w ） （ λ w 。 w w w ） ） … {\displaystyle {\begin{aligned}&(\mathbf {\lambda } xz)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}}
しかし、正規位簡約を用いると、同じ出発点からすぐに正規形に簡約できる。 （ λ x 。 z ） （ （ λ w 。 w w w ） （ λ w 。 w w w ） ） {\displaystyle (\mathbf {\lambda } xz)((\lambda w.www)(\lambda w.www))} → z {\displaystyle \rightarrow z}
完全β還元 とは、各ステップで任意のredexを還元できる非決定論的な1ステップ戦略を指します。[ 3 ] 並列β還元は 、項内のすべてのredexを同時に還元する戦略です。[ 16 ]
弱い還元 通常の順序削減と適用順序削減は、ラムダ抽象化の下で削減を可能にする点で強力です。対照的に、弱い 削減はラムダ抽象化の下で削減しません。[ 17 ] 名前による呼び出し削減 は、ラムダ抽象化内にない最も左の最も外側のredexを削減する弱い削減戦略であり、値による呼び出し削減 は、ラムダ抽象化内にない最も左の最も内側のredexを削減する弱い削減戦略です。これらの戦略は、名前による呼び出しと値による呼び出しの評価戦略 を反映するように考案されました。[ 18 ] 実際、適用順序削減は、もともとAlgol 60 や現代のプログラミング言語に見られる値による呼び出しパラメータ渡し技術をモデル化するために導入されました。弱い削減の考え方と組み合わせると、結果として得られる値による呼び出し削減は確かに忠実な近似となります。[ 19 ]
残念ながら、弱還元は合流 的ではなく、[ 17 ] [ 19 ] [ 17 ] λ x .(λ y . x ) z は 、redex (λ y . x ) z が λ x .(λ y . y ) z (λ y . y ) z が x [ 20 ]
最適な削減 最適な削減は、重複作業をせずに削減する一連の削減が存在しないラムダ項の存在によって動機付けられます。たとえば、次のことを考えてみましょう。
((λg.(g(g(λx.x)))) (λh.((λf.(f(f(λz.z)))) (λw.(h(w(λy.y))))))) これは、a=((λg. ... ) (λh.b)) 、b=((λf. ...) c) 、c=(λw. ...) の 3 つの入れ子になった項から構成されています。ここで実行できる β 簡約は、a と b の 2 つだけです。外側の a 項を先に簡約すると、内側の b 項が複製され、それぞれのコピーを簡約する必要がありますが、内側の b 項を先に簡約すると、引数 c が複製され、h と w の値がわかったときに作業が重複することになります。[ a ]
最適還元は、狭義のラムダ計算の還元戦略ではありません。なぜなら、β還元を実行すると、共有される置換されたリデックスに関する情報が失われるからです。代わりに、最適還元は、ラベル付きラムダ計算 、つまり共有されるべき作業の正確な概念を捉えた注釈付きラムダ計算に対して定義されます。[ 21 ] :
ラベルは、可算無限個 の原子ラベルと連結から構成されます。1 b {\displaystyle ab} 1 ¯ {\displaystyle {\overline {a}}} 1 _ {\displaystyle {\underline {a}}} [ 21 ] : [ 22 ] （ （ λ x 。 M ） α N ） β → β α ¯ ⋅ M [ x ↦ α _ ⋅ N ] {\displaystyle ((\lambda xM)^{\alpha }N)^{\beta }\to \beta {\overline {\alpha }}\cdot M[x\mapsto {\underline {\alpha }}\cdot N]}
どこ⋅ {\displaystyle \cdot } β ⋅ T α = T β α \displaystyle \beta \cdot T^{\alpha }=T^{\beta \alpha }} M [ x ↦ N ] {\displaystyle M[x\mapsto N]} は次のように定義されます（ Barendregt 規約 を使用）：[ 22 ] x α [ x ↦ N ] = α ⋅ N （ λ y 。 M ） α [ x ↦ N ] = （ λ y 。 M [ x ↦ N ] ） α y α [ x ↦ N ] = y α （ M N ） α [ x ↦ P ] = （ M [ x ↦ P ] N [ x ↦ P ] ） α {\displaystyle {\begin{aligned}x^{\alpha }[x\mapsto N]&=\alpha \cdot N&\quad (\lambda yM)^{\alpha }[x\mapsto N]&=(\lambda yM[x\mapsto N])^{\alpha }\\y^{\alpha }[x\mapsto N]&=y^{\alpha }&\quad (MN)^{\alpha }[x\mapsto P]&=(M[x\mapsto P]N[x\mapsto P])^{\alpha }\end{aligned}}} [ 23 ] [ 24 ]
最適削減の実用的なアルゴリズムは 、最適削減が最初に定義された1974年から10年以上経った1989年に初めて記述されました。 [ 25 ] [ 26 ] 相互作用ネット に拡張したプロトタイプ実装です。[ 21 ] : 362 [ 27 ] [ 28 ] [ b ]
ニーズ削減による呼び出し 呼び出しによる削減は、 わずかに異なるラベル付きラムダ計算に対して、同じラベルを持つ redex の並列削減を使用した弱い左端最外側削減として、最適削減と同様に定義できます。[ 17 ] [ 29 ] 遅延評価として知られる 評価戦略 の動作を模倣するように考案されました。
注記 ↑ ちなみに、上記の項は恒等関数(λy.y) に帰着し、恒等関数をバインダーg=λh... 、 f=λw... 、 h=λx.x (最初は)、 w=λz.z (最初は) に利用できるようにラッパーを作成することによって構築され、これらはすべて最も内側の項λy.y に適用されます。 ↑ 最適な削減に関する最近の研究の概要は、短い記事「ラムダ項の効率的な削減について」に記載されています。
参考文献 1 2 キルヒナー、エレーヌ（2015年8月26日）「書き換え戦略と戦略的書き換えプログラム」。マルティ＝オリエ、ナルシソ、オルヴェツキー、ピーター・チャバ、タルコット、キャロリン（編）『論理、書き換え、並行性：ホセ・メセゲルの65歳の誕生日を記念するエッセイ集』 。シュプリンガー。ISBN 978-3-319-23165-5 2021年8月14日 に取得 。 ↑セリンジャー、ピーター ；ヴァリロン、ブノワ （ 2009）。 「 量子ラムダ計算」 （PDF） 。 量子計算における意味論的手法 ：23。doi ： 10.1017/CBO9781139193313.005。ISBN 9780521513746 2021年8月21日 に取得 。1 2 ピアース、ベンジャミン C. (2002). 型とプログラミング言語 . MIT Press . p. 56. ISBN 0-262-16209-1 。↑ クロップ、ヤン・ウィレム。ヴァン・オストロム、ヴィンセント。ファン・ラームスドンク、フェムケ (2007)。 「削減戦略と非循環性」 (PDF) 。 書き換え、計算、証明 。コンピューターサイエンスの講義ノート。 Vol. 4600。89 ～ 112 ページ 。CiteSeerX 10.1.1.104.9139 。 土井 : 10.1007/978-3-540-73147-4_5 。 ISBN 978-3-540-73146-7 。1 2 3 4 5 Klop, JW 「項書き換えシステム」 (PDF) . Nachum Dershowitz と学生による論文 . テルアビブ大学。p. 77 . 2021 年 8 月 14 日 取得 。 1 2 Horwitz, Susan B. "ラムダ計算" . CS704 ノート . ウィスコンシン大学マディソン校. 2021 年 8 月 19 日 取得 . ↑ バレンドレグト、HP;エーケレン、MCJD。グラウアート、JRW。 JRケナウェイ。プラスマイヤー、MJ。眠れ、MR (1987)。 グラフの書き換えという用語 。ヨーロッパの並列アーキテクチャと言語。 Vol. 259. pp. 141–158 . 土井 : 10.1007/3-540-17945-3_8 。 hdl : 2066/17285 。 ↑ Antoy, Sergio; Middeldorp, Aart (1996 年 9 月). "逐次削減戦略" (PDF) . Theoretical Computer Science . 165 (1): 75– 95. doi : 10.1016/0304-3975(96)00041-2 . 2021 年 9 月 8 日 取得. ↑ Kieburtz, Richard B. (2001年11月). "書き換え戦略のための論理" . Electronic Notes in Theoretical Computer Science . 58 (2): 138– 154. doi : 10.1016/S1571-0661(04)00283-X . 1 2 3 マッツォーラ、ゲリーノ；ミルマイスター、ジェラール；ヴァイスマン、ジョディ（2004年10月21日）。 コンピュータ科学者のための総合数学2。 シュプリンガー・サイエンス＆ビジネス・メディア。323 ページ 。ISBN 978-3-540-20861-7 。↑ カリー、ハスケル B. ; フェイズ、ロバート (1958). 組み合わせ論理学 . 第 I 巻. アムステルダム: ノース ホランド. pp. 139–142 . ISBN 0-7204-2208-6 。↑ 鹿島亮. 「λ-計算における標準化定理の証明」 （PDF） . 東京工業大学. 2021年 8月19日 取得 . ↑ ピエールの小瓶（2017 年 12 月 7 日）。 非冪等型付け演算子、λ-微積分を超えたもの (PDF) (PhD)。ソルボンヌ大学パリ・シテ。 p. 62. ↑ Partain, William D. (1989年12月). Graph Reduction Without Pointers (PDF) (PhD). ノースカロライナ大学チャペルヒル校. 2022年 1月10日 取得 . ↑ Van Oostrom, Vincent; Toyama, Yoshihito (2016). Normalisation by Random Descent (PDF) . 1st International Conference on Formal Structures for Computation and Deduction. p. 32:3. doi : 10.4230/LIPIcs.FSCD.2016.32 . ↑ 高橋正人（1995年4月） 「λ計算における並列削減」 情報 と計算 118 （ 1）： 120–127 . doi ： 10.1006/inco.1995.1057 . 1 2 3 4 Blanc, Tomasz; Lévy, Jean-Jacques; Maranget, Luc (2005). "弱ラムダ計算における共有". Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday . Springer. pp. 70–87 . CiteSeerX 10.1.1.129.147 . doi : 10.1007/11601548_7 . ISBN 978-3-540-32425-6 。↑ Sestoft, Peter (2002). "ラムダ計算の簡約の実証" (PDF) . In Mogensen, T; Schmidt, D; Sudborough, IH (eds.). The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones . Lecture Notes in Computer Science. Vol. 2566. Springer-Verlag. pp. 420–435 . ISBN 3-540-00326-6 。1 2 Felleisen, Matthias (2009). Semantics engineering with PLT Redex . Cambridge, Mass.: MIT Press. p. 42. ISBN 978-0262062756 。↑ Sestini, Filippo (2019). 型付き弱ラムダ還元に対する評価による正規化 (PDF) . 第24回証明とプログラムのための型に関する国際会議 (TYPES 2018). doi : 10.4230/LIPIcs.TYPES.2018.6 . 1 2 3 Asperti, Andrea; Guerrini, Stefano (1998). 関数型プログラミング言語の最適実装 . ケンブリッジ、英国: Cambridge University Press. ISBN 0521621127 。1 2 Fernández, Maribel; Siafakas, Nikolaos (2010年3月30日). "明示的なコピーと消去を伴うラベル付きラムダ計算". 理論計算機科学の電子論文集 . 22 : 49– 64. arXiv : 1003.5515v1 . doi : 10.4204/EPTCS.22.5 . S2CID 15500633 . ↑レヴィ、ジャン＝ジャック （ 1987年11月9日～11日）。 ラムダ式の評価における共有 （PDF） 。次世代コンピュータのプログラミングに関する第2回日仏シンポジウム。フランス、カンヌ。p. 187。ISBN 0444705260 。↑ テレーズ（2003）。 用語書き換えシステム 。ケンブリッジ、英国：ケンブリッジ大学出版局。518 ページ 。ISBN 978-0-521-39115-3 。↑ Lamping, John (1990). 最適なラムダ計算削減のためのアルゴリズム (PDF) . 第 17 回 ACM SIGPLAN-SIGACT プログラミング言語の原理に関するシンポジウム - POPL '90. pp. 16–30 . doi : 10.1145/96709.96711 . ↑ レヴィ、ジャン＝ジャック (1974 年 6 月)。 Réductionssures dans le lambda-calcul (PDF) (PhD) (フランス語)。パリ第7大学。 81 ～ 109 ページ 。OCLC 476040273 。 2021 年 8 月 17 日 に取得 。 ↑ Asperti, Andrea. "Bologna Optimal Higher-Order Machine, Version 1.1" . GitHub . ↑ ヴァン・オストロム、ヴィンセント;ファン・デ・ローイ、キース・ジャン。ツヴィツァーロード、マリジン (2004)。 (Lambdascope): ラムダ計算の別の最適な実装 (PDF) 。プログラミング システムの代数と論理に関するワークショップ (ALPS)。 2017 年 7 月 6 日の オリジナル (PDF) からアーカイブされました 。 2021年8月18日 閲覧 。 ↑ Chang, Stephen; Felleisen, Matthias (2012). "The Call-by-Need Lambda Calculus, Revisited" (PDF) . Programming Languages and Systems . Lecture Notes in Computer Science. Vol. 7211. pp. 128– 147. doi : 10.1007/978-3-642-28869-2_7 . ISBN 978-3-642-28868-5 . S2CID 6350826 . 
![{\displaystyle ((\lambda xM)^{\alpha }N)^{\beta }\to \beta {\overline {\alpha }}\cdot M[x\mapsto {\underline {\alpha }}\cdot N]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/65b81c12597142ae87e4a7c04ac6ef09e9e6b6b3)
![{\displaystyle M[x\mapsto N]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9d9853bc08de420d94889f3bfa2f189ed45a90ab)
![{\displaystyle {\begin{aligned}x^{\alpha }[x\mapsto N]&=\alpha \cdot N&\quad (\lambda yM)^{\alpha }[x\mapsto N]&=(\lambda yM[x\mapsto N])^{\alpha }\\y^{\alpha }[x\mapsto N]&=y^{\alpha }&\quad (MN)^{\alpha }[x\mapsto P]&=(M[x\mapsto P]N[x\mapsto P])^{\alpha }\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/22eb723da875a61394cf740d41e255468c52d725)