强函数式编程

在满足下列限制的条件时，程序一定会终止：

1. 受限制的递归。仅对其参数的“简化”形式进行操作，例如Walther 递归、子结构递归或通过代码的抽象解释证明的“强规范化”。 ^[3]
2. 每个函数都必须是全函数（而非偏函数）。也就是说，它必须对定义域内的所有取值均有定义。
   • 有很多方式可以将常用的偏函数（例如除法）扩展为全函数：当函数未定义时指定一个特殊值（例如可扩展除法为${\displaystyle \forall x\in \mathbb {N} .x\div 0=0}$ ）；添加一个参数来指定这些输入的结果；或通过类型系统对定义域进行限制（例如细化类型）来排除它们。 ^[2]

这些限制意味着强函数式编程不是图灵完备的。但是，我们仍然可以使用很多算法。例如，任何可以计算渐近上限的算法（仅使用 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

有一些算法没有理论上的上限，但可以设定一个实际的上限（例如，一些基于启发式的算法可以在多次递归后“放弃”，从而确保终止）。

强函数式编程会导致立刻求值和懒惰求值的行为在理论上是一致的。当然，二者实际执行时由于性能原因还是有一定的差别的，有时仍然需要选择其中一个。 ^[4]

在强函数式编程中，数据和辅助数据是有区别的——前者是有限的，而后者可能是无限的。无限的数据可以表示诸如I/O这样的资源，而使用这些辅助数据则需要诸如共递归之类的操作。但是，具有依赖类型的强函数式语言也可以在没有辅助数据的情况下来操作I/O。 ^[5]

Epigram和Charity都可以被认为是强函数式编程语言，即使它们的工式与特纳在他的论文中指定的那样不同。这样的语言可以直接在系统F、直觉类理论或构造演算中进行编程。