SupGenが近づいてきたので、AI関連のコンテンツではないので失敗するかもしれないが、とにかくやりたいと思う技術関連のコンテンツを投稿しようと思う。 皆既日食と終結についての考察をいくつか述べます。 Agda（そしてLean？）では、「構造的再帰」によって終了性が保証されます。つまり、引数は「辞書順」に減少する可能性があるということです。これが何を意味するのかお分かりですか？ええ、私も分かりませんでした。でも、実際には非常にシンプルです。例えば、次のような節があるとします。 foo : Nat → Nat foo (S a) (S b) (S c) (S d) = foo (S a) (S b) c (S (S (S d))) foo x = x 終了していますか？ 終了していませんか？ どうすればわかりますか？ Agda では次のようになります: ステップ0: - 左辺の引数0: (S a) - 右辺の引数0: (S a) - これは*同一*なので、次の引数を確認してください (注: LHS/RHS は式の左側/右側を意味します) ステップ1: - LHSの引数1: (S b) - 右辺の議論1: (S b) - これは*同一*なので、次の引数を確認してください ステップ2: - LHSの引数2: (S c) - 右辺の引数2: c - これは*小さい*ので、この節は終了します。 これで完了です。 つまり、簡単に言うと、右側に再帰呼び出しがある場合は、その引数を左側の対応するパターンと 1 つずつ比較し、どちらかが小さくなるまで続けます。 簡単ですよね？ （そのように説明してもらえればよかったのですが…） さて、次のことを考えてみましょう。 foo : ペア -> ペア foo (ペア (S a) (S b)) = foo (P a (S (S (S b)))) foo x = x この機能は終了していますか? ええと、Agdaによれば…違います！しかし、同じ論理で明らかにそうです。最初の要素が小さいので、2番目の要素が大きいことは無関係です。Agdaのチェッカーは引数をチャンクに分割するようにハードコードされているようです。つまり、この節は、そのままでは終了するにもかかわらず、チェッカーを通過しません。 なぜこのことについて話しているのでしょうか? そこで、SupGenの再帰生成器をレビューしていたところ、いくつか変更を加えることでよりクリーンかつ高速化できることに気づきました。しかし、これらの変更は有効なのでしょうか？テストしてみたところ、なんとSupGenはAgdaによると停止しないプログラムを生成していました。最初は自分のアプローチが間違っていると思いましたが、Agdaが間違っていたことが判明しました。 今、あなたは新しい知識を得ました。 きっとこれはあなたにとって役に立つはずです!
SupGen が終了再帰呼び出しを生成するために使用する新しいアルゴリズムは、はるかに単純かつより汎用的です。
