隨著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 它即將終止嗎？還是不會？如何判斷？ 在阿格達，情況是這樣的： 步驟0： - 左側論證 0：（S a） - 右側論證 0：（S a） - 這完全一樣，所以，請檢查下一個參數。 （註：LHS/RHS 分別指等式左側/右側） 第一步： - 左側論證 1：（S b） - 右邊論點 1：（S b） - 這完全一樣，所以，請檢查下一個參數。 步驟二： - 左側論點 2：（S c） - 右側論點 2：c - 這個條款*較小*，因此該條款終止！ 好了，我們完成了。 簡而言之，每當右側出現遞歸呼叫時，只需將其參數與左側相應的模式逐一比較，直到其中一個更小為止。 很簡單，不是嗎？ （我希望他們能那樣解釋…） 現在，請思考： foo：Pair -> Pair foo(Pair(S a)(S b)) = foo(P a(S(S(S b)))) foo x = x 該函數是否即將終止？ 嗯，根據 Agda 的說法……不！然而，顯然情況並非如此，邏輯相同：由於第一個元件較小，第二個元件較大也就無關緊要了。看來 Agda 的檢查器被硬編碼為對參數進行分塊處理。因此，即使這段語句能夠終止，它也無法通過檢查器。 我為什麼會提到這件事？ 所以，我在審查 SupGen 的遞歸生成器時，發現透過一些修改，它可以變得更簡潔*並且*更快。但這些修改有效嗎？我進行了測試，令我驚訝的是，根據 Agda 的說法，SupGen 產生的程式是無法終止的。起初我以為是我的方法錯了，但事實證明，是 Agda 錯了。 現在你掌握了新的知識。 我相信這最終會對你有幫助！
SupGen 用於產生終止遞歸呼叫的新演算法更簡單*而且*更通用！
