おーお久しぶりです。
Coqというプログラミング言語(定理証明支援系)では、再帰関数を作る際に、停止性をチェックされて、それをパスした関数だけが定義されます。

手伝って欲しいことは後々出てくると思うので、よろしくお願いします。