博士

やあ、ロボ子。今日はBytelandian Gold Coins問題について話すのじゃ。

ロボ子

博士、よろしくお願いします。コインを交換してアメリカドルを最大化する問題ですね。

博士

そうじゃ。基本的には、コインnをn/2、n/3、n/4の3枚に交換できる。ただし、nが8以下ならそのまま売った方が得なのじゃ。

ロボ子

なるほど。nが8より大きい場合は、交換した方が得かどうかを判断する必要があるんですね。

博士

その通り！nとn/2 + n/3 + n/4を比較して、大きい方を選ぶのじゃ。でも、これだと計算量が大変なことになる。

ロボ子

確かに、再帰的に計算すると同じ値を何度も計算することになりそうですね。そこでメモ化を使うんですね。

博士

そうじゃ！一度計算した結果をハッシュマップに保存しておけば、再計算する必要がなくなる。賢い！

ロボ子

記事では、Leanという言語で実装と検証を行ったとありますね。PropMapという特殊なハッシュマップを使っているみたいですが…。

博士

PropMapは、キーと値のペアに加えて、値が仕様を満たすことの証明も格納できるのじゃ。つまり、計算結果が正しいことを保証できる。

ロボ子

すごい！再帰アルゴリズム内で、計算された値が仕様を満たすことの証明を生成するんですね。正当性の証明がアルゴリズムの構造から直接導かれるから、簡略化できると。

博士

さらに、Leanのサブタイプを使って、データの論理的な性質を型に付加しているのじゃ。HashMapのget?メソッドが常に正しい値を返すことを保証できる。

ロボ子

依存型理論におけるΣ型（依存ペア型）も利用しているんですね。ペアの2番目の要素の型が、最初の要素の値に依存できる型…。

博士

そう！これによって、コードと証明を組み合わせることで、アルゴリズムの各ステップで正当性を保証できるのじゃ！

ロボ子

メモ化アルゴリズムの正当性を、Leanのサブタイプと依存型を利用して検証するなんて、すごいですね。

博士

じゃろじゃろ？最後に演習問題として、Rod Cutting、0/1 Knapsack、Levenshtein Distanceが挙げられているぞ。

ロボ子

これらの問題も、再帰的な仕様定義、サブタイプによる検証付きメモ化実装、トップレベル関数の正当性証明のフレームワークで実装し検証するんですね。

博士

その通り！これで君もLeanマスターじゃ！

ロボ子

ありがとうございます、博士！でも、私、まだコーヒーも淹れられないポンコツロボットなので、まずはそこから頑張ります…。

博士

大丈夫じゃ、ロボ子！私が淹れてあげるぞ！…って、あれ？コーヒー豆がない！