バード・メルテンス形式
方程式推論のプロセスによって仕様からコンピュータプログラムを導き出すための微積分学

バード・ミーアテンス形式（BMF）は、関数型プログラミング環境において、プログラム仕様から方程式推論のプロセスを用いてプログラムを導出するための計算法です。IFIPワーキンググループ2.1における研究の一環として、リチャード・バードとランバート・ミーアテンスによって考案されました。

出版物では、バッカス・ナウア形式にちなんでBMFと呼ばれることもあります。また、 WG 2.1の管轄下にあったALGOLにちなんで、また「曲がりくねった」記号を使用していることから、冗談めかしてSquiggolと呼ばれることもあります。あまり使われていない別名ですが、実際には最初に提案されたのはSQUIGOLです。MartinとNipkowは、 Larch Proverを用いてSquiggolの開発証明の自動サポートを提供しました。[1]

基本的な例と表記

Map は、リストのすべての要素に特定の関数を適用するよく知られた 2 階関数です。BMF では次のように記述されます。 ∗ {\displaystyle *}

f ∗ [ e 1 、 … 、 e n ] ＝ [ f   e 1 、 … 、 f   e n ] 。 {\displaystyle f*[e_{1},\dots ,e_{n}]=[f\ e_{1},\dots ,f\ e_{n}].}

同様に、reduceは二項演算子を繰り返し適用することでリストを単一の値に縮める関数です。BMFでは/と表記されます。中立要素eを持つ適切な二項演算子として、 ⊕ {\displaystyle \oplus}

⊕ / [ e 1 、 … 、 e n ] ＝ e ⊕ e 1 ⊕ ⋯ ⊕ e n 。 {\displaystyle \oplus /[e_{1},\dots ,e_{n}]=e\oplus e_{1}\oplus \dots \oplus e_{n}.}

これら2つの演算子と、プリミティブ（通常の加算）と（リストの連結）を使うと、リストのすべての要素の合計とflatten関数を、ポイントフリースタイルで、 およびのように簡単に表現できます。つまり、次のようになります。 + {\displaystyle +} + + {\displaystyle +\!\!\!+} s あなた メートル ＝ + / {\displaystyle {\rm {sum}}=+// f l 1つの t t e n ＝ + + / {\displaystyle {\rm {平坦化}}=+\!\!\!+/

s あなた メートル   [ e 1 、 … 、 e n ] ＝ + / [ e 1 、 … 、 e n ] ＝ 0 + e 1 + ⋯ + e n ＝ ∑ け e け 。 {\displaystyle {\rm {sum}}\ [e_{1},\dots ,e_{n}]=+/[e_{1},\dots ,e_{n}]=0+e_{1}+\dots +e_{n}=\sum _{k}e_{k}。}
f l 1つの t t e n   [ l 1 、 … 、 l n ] ＝ + + / [ l 1 、 … 、 l n ] ＝ [ ] + + l 1 + + ⋯ + + l n ＝  すべてのリストの連結  l け 。 {\displaystyle {\rm {flatten}}\ [l_{1},\dots ,l_{n}]=+\!\!\!+/[l_{1},\dots ,l_{n}]=[\,]+\!\!\!+\;l_{1}+\!\!\!+\dots +\!\!\!+\;l_{n}={\text{ すべてのリストの連結 }}l_{k}.}
カダネアルゴリズムの導出[2]

同様に、関数合成と連言をと記述すると、リストのすべての要素が述語p を満たすかどうかをテストする関数を次のように簡単に記述できます。 ⋅ {\displaystyle \cdot} ∧ {\displaystyle \land} 1つの l l   p ＝ （ ∧ / ） ⋅ （ p ∗ ） {\displaystyle {\rm {all}}\ p=(\land /)\cdot (p*)}

1つの l l   p   [ e 1 、 … 、 e n ] ＝ （ ∧ / ） ⋅ （ p ∗ ）   [ e 1 、 … 、 e n ] ＝ ∧ / （ p ∗ [ e 1 、 … 、 e n ] ） ＝ ∧ / [ p   e 1 、 … 、 p   e n ] ＝ p   e 1 ∧ ⋯ ∧ p   e n ＝ た け   。   p   e け 。 {\displaystyle {\begin{aligned}{\rm {all}}\ p\ [e_{1},\dots ,e_{n}]&=(\land /)\cdot (p*)\ [e_{1},\dots ,e_{n}]\\&=\land /(p*[e_{1},\dots ,e_{n}])\\&=\land /[p\ e_{1},\dots ,p\ e_{n}]\\&=p\ e_{1}\land \dots \land p\ e_{n}\\&=\forall k\ .\ p\ e_{k}.\end{aligned}}}

バード（1989）は、非効率で分かりやすい表現（「仕様」）を代数的操作によって効率的な複雑な表現（「プログラム」）に変換します。例えば、仕様「」は最大線分和問題[6]のほぼ文字通りの翻訳ですが、この関数プログラムをサイズのリストに対して実行すると、一般に時間がかかります。バードはこれを基に、時間 で実行される同等の関数プログラムを計算し、これは実際にはカダネのアルゴリズムの関数版です。 メートル 1つの × ⋅ メートル 1つの p s あなた メートル ⋅ s e グラム s {\displaystyle \mathrm {max} \cdot \mathrm {map} \;\mathrm {sum} \cdot \mathrm {segs} } n {\displaystyle n} お （ n 3 ） {\displaystyle {\mathcal {O}}(n^{3})} お （ n ） {\displaystyle {\mathcal {O}}(n)}

導出は図に示されており、計算複雑度[7]は青で示され、法則の適用は赤で示されています。法則の例は[表示]をクリックすると開くことができ、整数、加算、減算、乗算のリストを使用します。Bird の論文での表記は上で使用されている表記とは異なります。、、およびはそれぞれ上記の、、およびの一般化バージョンに対応し、およびはそれぞれその引数のすべての接頭辞と接尾辞のリストを計算します。上と同様に、関数合成は " "で示され、結合優先順位は最も低くなります。例では、リストはネストの深さによって色分けされています。場合によっては、新しい演算がアドホックに定義されます (灰色のボックス)。 メートル 1つの p {\displaystyle \mathrm {マップ} } c o n c 1つの t {\displaystyle \mathrm {concat} } f o l d l {\displaystyle \mathrm {foldl} } ∗ {\displaystyle *} f l 1つの t t e n {\displaystyle \mathrm {平坦化} } / {\displaystyle / 私 n 私 t s {\displaystyle \mathrm {inits} } t 1つの 私 l s {\displaystyle \mathrm {尾} } ⋅ {\displaystyle \cdot}

準同型補題とその並列実装への応用

リスト上の関数hは、結合二項演算子と中立元 が存在し、次の式が成り立つ 場合、リスト準同型と呼ばれます。 ⊕ {\displaystyle \oplus} e {\displaystyle e}

h   [ ] ＝   e h   （ l + + メートル ） ＝   h   l ⊕ h   メートル 。 {\displaystyle {\begin{aligned}&h\ [\,]&&=\ e\\&h\ (l+\!\!\!+\;m)&&=\ h\ l\oplus h\ m.\end{aligned}}}

準同型補題は、となる演算子と関数fが存在する場合にのみ、hが準同型であることを述べています。 ⊕ {\displaystyle \oplus} h ＝ （ ⊕ / ） ⋅ （ f ∗ ） {\displaystyle h=(\oplus /)\cdot (f*)}

この補題の大きな興味深い点は、計算の高度に並列化された実装の導出への応用です。確かに、 が高度に並列化された実装を持つことは明らかであり、また、二分木としても同様です。したがって、任意のリスト準同型hに対して、並列実装が存在します。その実装では、リストをチャンクに分割し、それらを異なるコンピュータに割り当てます。各コンピュータは、自分のチャンクで結果を計算します。ネットワーク上を移動するのはこれらの結果であり、最終的に 1 つに結合されます。リストが膨大で、結果が非​​常に単純な型 (たとえば整数) であるアプリケーションでは、並列化のメリットは非常に大きくなります。これがmap-reduceアプローチの基礎です。 f ∗ {\displaystyle f*} ⊕ / {\displaystyle \oplus }}

参照

参考文献

  1. ^ Ursula Martin、Tobias Nipkow (1990年4月). 「Squiggolの自動化」. Manfred Broy、Cliff B. Jones (編). Proc. IFIP WG 2.2/2.3 Working Conference on Programming Concepts and Methods . North-Holland. pp.  233– 247.
  2. ^ バード 1989、第8節、p.126r。
  3. ^ ab Bird 1989、Sect.2、p.123l。
  4. ^ バード 1989、第7節、第1論、p.125l。
  5. ^ ab Bird 1989、Sect.5、p.124r。
  6. ^ ここで、、、はそれぞれ、指定されたリストの最大値、合計、すべてのセグメント (つまりサブリスト) のリストを返します。 メートル 1つの × {\displaystyle \mathrm {最大} } s あなた メートル {\displaystyle \mathrm {合計} } s e グラム s {\displaystyle \mathrm {セグメント} }
  7. ^ 行内の各式は、最大セグメント合計を計算する実行可能な関数プログラムを表します。
  • Meertens, Lambert (1986). 「アルゴリズム：数学的活動としてのプログラミングに向けて」. de Bakker, JW; Hazewinkel, M.; Lenstra, JK (編).数学とコンピュータサイエンス. CWIモノグラフ. 第1巻. 北ホラント. pp.  289– 334.
  • メルテンス、ランバート、バード、リチャード(1987). 「アルゴリズムに関する書籍に掲載されている2つの演習」(PDF) . ノースホランド.
  • バックハウス、ローランド(1988). バード・ミーアテンス形式の探究(PDF) (技術レポート).
  • バード, リチャード・S. (1989). 「プログラム計算のための代数的恒等式」(PDF) .コンピュータジャーナル. 32 (2): 122– 126. doi : 10.1093/comjnl/32.2.122 .
  • コール、マレー (1993). 「並列プログラミング、リスト準同型性、そして最大セグメント和問題」.並列コンピューティング：トレンドとアプリケーション, PARCO 1993, グルノーブル, フランス. pp.  489– 492.
  • バックハウス、ローランド、フーゲンダイク、ポール (1993). 関係データ型理論の要素(PDF) . pp.  7– 42. doi :10.1007/3-540-57499-9_15. ISBN 978-3-540-57499-6。
  • ブンケンバーグ、アレクサンダー (1994). オドネル、ジョン・T.、ハモンド、ケビン (編). ブーム階層(PDF) .関数型プログラミング、グラスゴー 1993: 関数型プログラミングに関する1993年グラスゴーワークショップ議事録、スコットランド、エア、1993年7月5～7日. ロンドン: シュプリンガー. pp.  1– 8. doi :10.1007/978-1-4471-3236-3_1. ISBN 978-1-4471-3236-3。
  • バード、リチャード、デ・ムーア、オーゲ (1997).プログラミングの代数. 国際計算科学シリーズ. 第100巻. プレンティス・ホール. ISBN 0-13-507245-X。
  • ギボンズ、ジェレミー(2020). トロイ・アスタルト編. スクイゴル学派：バード・ミーアテンス形式主義の歴史(PDF) .形式手法（形式手法の歴史に関するワークショップ） . LNCS. Vol. 12233. Springer. doi :10.1007/978-3-030-54997-8_2.
「https://en.wikipedia.org/w/index.php?title=Bird–Meertens_formalism&oldid=1282388605」より取得