隨著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 用於產生終止遞歸呼叫的新演算法更簡單*而且*更通用!
