ATS：使用定理證明/尾呼叫和尾遞迴進行程式設計

尾遞迴對於 ATS 中的程式設計至關重要。

假設一個函式 foo 呼叫一個函式 bar，其中 foo 和 bar 可以是同一個函式。如果對 bar 的呼叫返回值也是 foo 的返回值，那麼此對 bar 的呼叫通常被稱為尾呼叫。如果 foo 和 bar 是同一個函式，那麼這就是一個（遞迴）自尾呼叫。例如，在如下定義的函式 f91 的主體中，有兩個遞迴呼叫

fun f91 (n: int): int = if n >= 101 then n - 10 else f91 (f91 (n+11))

外部遞迴呼叫是自尾呼叫，而內部呼叫則不是。

如果一個函式主體中的每個遞迴呼叫都是尾呼叫，那麼這個函式就是一個尾遞迴函式。例如，以下函式 sum2 是尾遞迴的

fun sum2 (n: int, res: int): int = if n > 0 then sum2 (n-1, n+res) else res

在 ATS 中，最重要的最佳化可能是將自尾呼叫轉換為（區域性）跳轉的最佳化。這種最佳化實際上將每個尾遞迴函式轉換為等效的迴圈。雖然 ATS 為構建 for 迴圈和 while 迴圈提供了直接的語法支援，但 ATS 中迴圈構建的首選方法是使用尾遞迴函式。