Conversation

普通の再帰関数の方が帰納法で性質を示しやすいので出番がある。効率を気にする場合は末尾再帰版との等価性を証明できればよい。

ただ、末尾再帰関数の性質について直接証明をする方法もそれはそれで重要なため両方のスタイルで証明ができた方がよいと下記の練習問題の回答にあった(ものによっては末尾再帰でないバージョンと等しいことを示すのが難しい場合もある)。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____INTRODUCTORY-CHALLENGE-PROBLEM-4

まあ、ともかく ACL2 なら末尾再帰版でない関数にも出番があるのだ。