強函數式編程

強函數式編程（也稱為全函數式編程），與之相對的是普通的或者說弱函數式編程。是一種編程範式，它將程序的範圍限制為可證明停機的程序。

限制

在滿足下列限制的條件時，程序一定會終止：

1. 受限制的遞歸。僅對其參數的「簡化」形式進行操作，例如Walther 遞歸、子結構遞歸或通過代碼的抽象解釋證明的「強規範化」。
2. 每個函數都必須是全函數（而非偏函數）。也就是說，它必須對定義域內的所有取值均有定義。
   • 有很多方式可以將常用的偏函數（例如除法）擴展為全函數：當函數未定義時指定一個特殊值（例如可擴展除法為$\forall x\in \mathbb {N} .x\div 0=0$）；添加一個參數來指定這些輸入的結果；或通過類型系統對定義域進行限制（例如細化類型）來排除它們。

這些限制意味著強函數式編程不是圖靈完備的。但是，我們仍然可以使用很多算法。例如，任何可以計算漸近上限的算法（僅使用 Walther 遞歸的程序）都可以將上限作為額外的參數，從而在每次遞歸中遞減該參數，使其變為子結構遞歸的形式。

例如，通常的快速排序並不是以子結構遞歸的形式編寫的，但它的遞歸深度不會超過數組的長度（最壞情況時間複雜度O(n²)）。下面是用Haskell實現的一個不滿足子結構遞歸的快速排序：

import Data.List (partition)

qsort []       = []
qsort [a]      = [a]
qsort (a:as)   = let (lesser, greater) = partition (<a) as
                 in qsort lesser ++ [a] ++ qsort greater

利用數組的長度信息來限制函數，我們可以將其改寫為子結構遞歸的形式：

import Data.List (partition)

qsort x = qsortSub x x
-- 数组为空的情况
qsortSub []     as     = as -- 返回本身
-- 数组非空的情况
qsortSub (l:ls) []     = [] -- 空数组，不需要递归
qsortSub (l:ls) [a]    = [a] -- 只有一个元素，不需要递归
qsortSub (l:ls) (a:as) = let (lesser, greater) = partition (<a) as
                            -- 发生递归，但是每次递归的参数中，as都是ls的子集
                         in qsortSub ls lesser ++ [a] ++ qsortSub ls greater

有一些算法沒有理論上的上限，但可以設定一個實際的上限（例如，一些基於啟發式的算法可以在多次遞歸後「放棄」，從而確保終止）。

強函數式編程會導致立刻求值和懶惰求值的行為在理論上是一致的。當然，二者實際執行時由於性能原因還是有一定的差別的，有時仍然需要選擇其中一個。

在強函數式編程中，數據和輔助數據是有區別的——前者是有限的，而後者可能是無限的。無限的數據可以表示諸如I/O這樣的資源，而使用這些輔助數據則需要諸如共遞歸之類的操作。但是，具有依賴類型的強函數式語言也可以在沒有輔助數據的情況下來操作I/O。

Epigram和Charity都可以被認為是強函數式程式語言，即使它們的工式與特納在他的論文中指定的那樣不同。這樣的語言可以直接在系統F、直覺類理論或構造演算中進行編程。