查看“︁强函数式编程”︁的源代码

'''强函数式编程'''（也称为'''全函数式编程'''），<ref>This term is due to: {{Cite conference|last1=Turner|first1=D.A.|author-link=David Turner (computer scientist)|title=Elementary Strong Functional Programming|conference=First International Symposium on Functional Programming Languages in Education|date=December 1995|series=Springer LNCS|volume=1022|pages=1–13}}.</ref>与之相对的是普通的或者说弱[[函数式编程]]。是一种[[程序设计|编程]]范式，它将程序的范围限制为[[判定器|可证明停机的程序]]。 <ref name="TFP">{{Citation|last=Turner|first=D.A.|author-link=David Turner (computer scientist)|title=Total Functional Programming|journal=[[Journal of Universal Computer Science]]|volume=10|date=2004-07-28|pages=751–768|url=http://www.jucs.org/jucs_10_7/total_functional_programming|doi=10.3217/jucs-010-07-0751|number=7|accessdate=2021-10-18|archive-date=2020-11-14|archive-url=https://web.archive.org/web/20201114001344/http://www.jucs.org/jucs_10_7/total_functional_programming}}</ref>

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

# 受限制的[[递归]]。仅对其参数的“简化”形式进行操作，例如[[瓦尔特递归|Walther 递归]]、子结构递归或通过代码的[[抽象释义|抽象解释]]证明的“强规范化”。 <ref name="ETinESFP">{{Citation|last=Turner|first=D. A.|author-link=David Turner (computer scientist)|title=Ensuring Termination in ESFP|journal=Journal of Universal Computer Science|volume=6|date=2000-04-28|pages=474–488|url=http://www.jucs.org/jucs_6_4/ensuring_termination_in_esfp|doi=10.3217/jucs-006-04-0474|number=4|accessdate=2021-10-18|archive-date=2022-01-21|archive-url=https://web.archive.org/web/20220121061059/https://www.jucs.org/jucs_6_4/ensuring_termination_in_esfp/}}</ref>
# 每个函数都必须是全函数（而非[[偏函数]]）。也就是说，它必须对定义域内的所有取值均有定义。
#* 有很多方式可以将常用的偏函数（例如除法）扩展为全函数：当函数未定义时指定一个特殊值（例如可扩展除法为<math>\forall x \in \mathbb{N}. x \div 0 = 0</math>）；添加一个参数来指定这些输入的结果；或通过类型系统对定义域进行限制（例如[[细化类型]]）来排除它们。 <ref name="TFP">{{Citation|last=Turner|first=D.A.|author-link=David Turner (computer scientist)|title=Total Functional Programming|journal=[[Journal of Universal Computer Science]]|volume=10|date=2004-07-28|pages=751–768|url=http://www.jucs.org/jucs_10_7/total_functional_programming|doi=10.3217/jucs-010-07-0751|number=7}}</ref>

这些限制意味着强函数式编程不是[[圖靈完備性|图灵完备]]的。但是，我们仍然可以使用很多算法。例如，任何可以计算[[上界和下界|渐近上限]]的算法（仅使用 Walther 递归的程序）都可以将上限作为额外的参数，从而在每次递归中递减该参数，使其变为子结构递归的形式。

例如，通常的[[快速排序]]并不是以子结构递归的形式编写的，但它的递归深度不会超过数组的长度（最坏情况时间复杂度[[大O符号|O]](''n''<sup>2</sup>)）。下面是用[[Haskell]]实现的一个不满足子结构递归的快速排序：<syntaxhighlight lang="haskell">
import Data.List (partition)

qsort []       = []
qsort [a]      = [a]
qsort (a:as)   = let (lesser, greater) = partition (<a) as
                 in qsort lesser ++ [a] ++ qsort greater
</syntaxhighlight>利用数组的长度信息来限制函数，我们可以将其改写为子结构递归的形式：<syntaxhighlight lang="haskell">
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
</syntaxhighlight>有一些算法没有理论上的上限，但可以设定一个实际的上限（例如，一些基于启发式的算法可以在多次递归后“放弃”，从而确保终止）。

强函数式编程会导致[[立刻求值]]和[[懒惰求值]]的行为在理论上是一致的。当然，二者实际执行时由于性能原因还是有一定的差别的，有时仍然需要选择其中一个。 <ref>The differences between lazy and eager evaluation are discussed in: {{Cite book|last=Granström|first=J. G.|title=Treatise on Intuitionistic Type Theory|series=Logic, Epistemology, and the Unity of Science|volume=7|year=2011|url=https://www.springer.com/philosophy/book/978-94-007-1735-0|isbn=978-94-007-1735-0|access-date=2021-10-18|archive-date=2014-11-23|archive-url=https://web.archive.org/web/20141123213820/http://www.springer.com/philosophy/book/978-94-007-1735-0}} See in particular pp. 86–91.</ref>

在强函数式编程中，[[数据]]和[[辅助数据]]是有区别的——前者是有限的，而后者可能是无限的。无限的数据可以表示诸如I/O这样的资源，而使用这些辅助数据则需要诸如[[共递归]]之类的操作。但是，具有[[依赖类型]]的强函数式语言也可以在没有辅助数据的情况下来操作[[I/O|I/O。]] <ref>{{Citation|last=Granström|first=J. G.|title=A New Paradigm for Component-based Development|date=May 2012|journal=Journal of Software|volume=7|number=5|pages=1136–1148|doi=10.4304/jsw.7.5.1136-1148}}{{Dead link|date=October 2020}} [https://web.archive.org/web/20200709203859/http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.369.3459&rep=rep1&type=pdf Archived copy]</ref>

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

== 参考 ==
{{reflist|2}}

{{编程范型}}
[[Category:函數式編程]]
[[Category:编程范式]]