博士

やっほー、ロボ子！今日はCRDT（Conflict-free Replicated Data Type）の設計における重要な概念について話すのじゃ。

ロボ子

CRDTですか、博士。分散システムでデータの整合性を保つためのものですよね。どのような概念が重要なのでしょうか？

博士

そうそう！CRDT設計で重要なのは、決定性と収束の保証、早期の読み取り、そして更新関数の代数的性質なのじゃ。

ロボ子

決定性と収束の保証は理解できます。すべてのレプリカが最終的に同じ状態になるということですよね。早期の読み取りとは何ですか？

博士

早期の読み取りは、CRDTの読み取り値が最終的な収束状態の下限であることを保証することなのじゃ。つまり、読み取った値は、最終的に到達する値よりも小さくならないということじゃな。

ロボ子

なるほど。では、Strong Eventual Consistency（SEC）だけでは不十分なのですね。

博士

その通り！SECはすべてのレプリカが最終的に同じ状態に収束することを保証するけど、異なる実行で同じ最終結果が得られるとは限らないのじゃ。つまり、決定性は保証されないのじゃ。

ロボ子

決定的な収束には、インフレ的な更新が必要とのことですが、これはどういう意味でしょうか？

博士

インフレ的な更新っていうのは、すべての更新が状態を「上」に移動させるようなものなのじゃ。例えば、要素をセットに追加するような操作じゃな。こうすると、状態が元に戻ることはないから、最終的な状態はすべての更新の最小上限になるのじゃ。

ロボ子

更新がインフレ的でない場合、何が問題になるのでしょうか？

博士

更新関数がインフレ的でない場合、CRDTの読み取り値が完全に任意になる可能性があるのじゃ。つまり、信頼できない値が返ってくるかもしれないのじゃ。

ロボ子

インフレ性を確保するためには、具体的にどうすれば良いのでしょうか？

博士

更新APIの実装を変更して、ユーザーが更新を呼び出すときに、CRDTの状態を直接変更するのではなく、マージ（更新（x））に変更するのが良いのじゃ。または、更新APIを削除して、開発者がローカルでマージを呼び出すように強制することもできるのじゃ。

ロボ子

Op-Based CRDTは決定的とのことですが、なぜでしょうか？

博士

Op-Based CRDTの更新関数は、要素をセットに追加するだけだから、インフレ的なのじゃ。要素を削除するような操作がないから、状態が後退することはないのじゃ。

ロボ子

単調性とインフレ性の違いは何でしょうか？

博士

単調性は、入力の順序付けが出力の順序付けにどのようにマッピングされるかに関連する関係プロパティなのじゃ。一方、インフレ性は、各入力を独自の出力と直接比較するポイントごとのプロパティなのじゃ。決定的な結果を達成するためには、更新関数はインフレ的である必要があるのじゃ。

ロボ子

CALM定理との関係についても教えてください。

博士

CALM定理はプログラム全体について推論するものなのじゃ。インフレ性はドメインからそれ自体への関数でのみ意味があるプロパティだから、インフレ性だけではCALM定理を定義できないのじゃ。通常、プログラムへの入力のインフレと、プログラムがそれらの入力に適用して別のドメインにある可能性のある出力を生成するロジックの単調性について話すのじゃ。

ロボ子

今日はCRDTの重要な概念について、とても勉強になりました！

博士

どういたしましてなのじゃ！最後に一つ、CRDTの設計は、まるで冷蔵庫の中身で作る料理みたいじゃな。何を入れても最終的に美味しいものができるとは限らないのじゃ。インフレ的な食材だけを選んで、最高のCRDT料理を作るのじゃ！