関数の再帰呼び出しの回数の上界を Lean で証明する

[Seasawher]

Lean では２つの関数 f, g は f x = g x であるときに f = g です．つまり，関数 f に対してその計算量を返すような関数 T は作ることができないはずです．

しかし，関数の入力に「残りの計算資源」を与えてもいいなら，計算量を見積もることができるかもしれません．

たとえば，ユークリッドの互除法を表す次の関数を考えます．

def gcd : (a : Nat) -> (b : Nat) -> (fuel : Nat) -> Option Nat
| _, _, 0 => none -- 燃料切れ
| a, 0, _ => some a
| a, b, (fuel+1) => gcd b (a % b) fuel

これにより，たとえば fuel が ～より大きければ gcd の出力は none にならない，等の形で再帰呼び出しの回数の上界が証明できます．

この方法を Fibonacci 数列にも応用したいのですが, F (n + 2) の計算に F (n + 1) と F n の両方が呼び出されて，それらに fuel を分配しなければならず，それを行う自然（ canonical ）な方法がないように感じています．

この方法は一般にはうまくいかないのでしょうか？

[s-taiga]

Fという関数それぞれに与えていくのではなく、式自体に一つ値を与えて、式変形の回数で上限を決める方法を用いる方法があります。
今回の例でいえば、F (n + 2)にfuelとしてmが与えられた場合、F (n + 1) + F nへの式変形でm - 1に、(F n + F (n - 1)) + F nでm - 2にするという感じです。
この際式のどこから評価していくかは評価戦略次第になります。
Agdaの例になりますが、λ計算の評価でこのようなやり方が例示されています。
https://plfa.github.io/Properties/#evaluation

[Seasawher]

ありがとうございます．Agdaがわからないので詳細がつかめていないのですが，ラムダ計算を計算のモデルとして使って，評価していく過程をエミュレートできる，というような話でしょうか？

おそらく Lean4 でも可能なのでしょうが，調べた限りだとそういうことをしているサンプルコードが見つかりません…．

[s-taiga]

ご認識の通りだと思います。
上記内容をフィボナッチ数列に合わせてLeanで書き起こすと以下のような感じになるはずです。
通常のλ計算と異なり、環境や型を考えなくても多分大丈夫なため若干簡素な書き方で実現できています。
https://github.com/s-taiga/lean-test-files/blob/develop/fibonacci/test.lean

本当は評価の過程をevalしたときに見えるようにしたかったのですが、表示を行えるようにする型クラスの使い方がいまいちわからなかったため最終的な計算だけしています。

[Seasawher]

おお、ありがとうございます！

これで evalSteps がある程度大きなステップ数を与えればゼロにならないことを証明すれば、フィボナッチ数の計算ステップの上界を示したことになるわけでしょうか

こういう発想は全くなかったので、とても勉強になりました！他のアルゴリズムの評価にも応用できそうです

[Seasawher]

Lean ではありませんが、モナドを用いて計算量を見積もっている例がありました

https://openresearch-repository.anu.edu.au/bitstream/1885/177195/1/thesis.pdf