我的消费券

Andrej 邀请我写一些令人惊讶的函数式程序。第一个程序，由于Ulrich Berger (1990)，在无限二进制数字序列的“康托空间”上执行穷举搜索。我在最后包括了参考资料。穷举搜索的弱形式相当于检查总谓词是否对康托空间的所有元素都成立。因此，这相当于对康托空间的普遍量化。这可能在有限的时间内通过算法完成吗？
一个更强的相当于找到一个例子，使得谓词成立，如果这样的例子存在，并说不存在任何其他例子。

我将使用Haskell语言，但可以将程序快速翻译为 ML 或OCaml 等。此处显示的源代码附加为看似不可能的.hs。

我们可以使用布尔值来表示二进制数字，甚至是整数，但我更喜欢使用不同的类型来避免混淆：

> 数据位 = 零 | 一
> 推导（方程）
在获得子句告诉哈斯克尔弄清楚如何自动决定位的平等。

对于无限序列的类型，我们可以为这里考虑的大多数算法使用内置类型的惰性列表。但是，为了说明某些点，我将采取数学观点并将序列视为定义在自然数上的函数。Haskell 定义的下一个版本将有一个内置的自然数类型。目前，我将它实现为整数类型：

> 类型自然 = 整数
> 类型康托 = 自然 -> 位
运算符(#)接受一个位x和一个序列a并产生一个新的序列x # a ，其中 x作为头部，a作为尾部（非常类似于列表的内置操作(:)）：

> (#) :: Bit -> Cantor -> Cantor
> x # a = \i -> if i == 0 then x else a(i-1)
请注意，符号\i -> ...代表[数学处理错误].

接下来，我们来到问题的核心，即在 Cantor 空间上执行穷举搜索的函数。函数find的规范是，对于任何总p，应该有find p始终是康托空间的总元素，而且，如果康托空间中存在a且 pa = True，则a = find p就是这种a 的一个例子 。

> 永远，永远 :: (Cantor -> Bool) -> Bool
> 查找 :: (Cantor -> Bool) -> Cantor
因为我会有多个find实现，所以我必须选择一个才能编译和运行程序。规范选择是第一个，

> 查找 = find_i
但你被邀请去尝试其他的。为了使find_i的以下定义有意义，您必须采取上述选择。

函数find在康托空间上有一个谓词，因此它通常有一个[数学处理错误] [数学处理错误]- 表达式作为参数。在下面的定义中，这是没有必要的，因为（\一- > PA）= P由规则。但是为了清楚起见，我采用了它，因为这样我们就可以将“ find(\a -> pa) ”大声读为“find a such that p(a) ”：

> forsome p = p(find(\a -> pa))
> 永远 p = not(forsome(\a -> not(pa)))
请注意，函数forsome（普遍量化）是通过德摩根定律从函数forsome（存在量化）中获得的。该函forsome 和find_i由相互递归定义：

> find_i :: (Cantor -> Bool) -> Cantor
> find_i p = if forsome(\a -> p(Zero # a))
> 然后零 # find_i(\a -> p(Zero # a))
> else One # find_i(\a -> p(One # a))
算法find_i的直观思路很明确：如果有一个从零开始的例子，则取结果从零开始，否则就必须从一开始。然后我们使用相同的想法递归地构建尾部。可能不清楚的是递归是否最终产生一个数字，因为通过调用forsome的间接递归调用 。数学证明通过对p的均匀连续性模数进行归纳来进行，定义如下。

仅当有一个示例时才返回一个示例可能更自然，否则告诉没有任何示例：

> 搜索 :: (Cantor -> Bool) -> 可能是 Cantor
> 搜索 p = if forsome(\a -> pa) then Just(find(\a -> pa)) else Nothing
该也许类型构造是由哈斯克尔预定义为

数据 也许 a = Just a | 没有

类型论注解：类型Maybe a对应 sum 类型[数学处理错误] [数学处理错误] [数学处理错误]，其中唯一的元素 被称为 Nothing而Just是插入.

练习：假设我们首先定义了搜索，那么forsome和find都可以直接从搜索中定义 。

常识告诉我们，函数类型没有可判定的相等性。事实上，例如众所周知，函数类型Integer -> Integer由于停机问题而没有可判定的相等性 。然而，常识并不总是正确的，事实上，其他一些函数类型确实具有可判定相等性，例如类型Cantor -> y表示具有可判定相等性的任何类型y，而不与图灵相矛盾：

> 等于 :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
> 等于 fg = 永远（\a -> fa == ga）
这看起来很奇怪，甚至有点可疑，因为康托空间在某种意义上比整数大。在后续文章中，我将解释这与康托空间拓扑紧凑而整数不是这一事实有关。

让我们运行一个例子：

> 强制 :: 位 -> 自然
> 强制零 = 0
> 强制一 = 1

> f, g, h :: Cantor -> 整数

> fa = coerce(a(7 * coerce(a 4) + 4 * (coerce(a 7)) + 4))

> ga = coerce(a(coerce(a 4) + 11 * (coerce(a 7))))

> ha = if a 7 == 0
> then if a 4 == Zero then coerce(a 4) else coerce(a 11)
> else if a 4 == One then coerce(a 15) else coerce(a 8)

现在我们调用ghci解释器：

> 加载包基础...链接...完成。
[1 of 1] 编译 Main（看似不可能的.lhs，已解释）
好的，模块加载：Main。
*主要>

在这一点上，我们可以在解释器的提示下评估表达式。首先，我要求它在每次评估后打印时间和空间使用情况：

> *主> :set +s

在运行频率为 1.73GHz 的戴尔 410 笔记本电脑上，我测试了以下表达式：

> *主>等于fg
错误的
（0.10 秒，3490296 字节）

> *Main> 等于 fh
真的
（0.87 秒，36048844 字节）

> *主>等于gh
错误的
（0.09 秒，3494064 字节）

> *主要>等于ff
真的
（0.91 秒，38642544 字节）

> *主>等于gg
真的
（0.15 秒，6127796 字节）

> *主>等于hh
真的
（0.83 秒，32787372 字节）

通过更改find的实现，我将使其更快，并且还能够运行更大的示例。但是让我们暂时继续当前的实现。
以下是伯杰考虑上述结构的主要动机：

> 模数 :: (Cantor -> Integer) -> 自然
> 模数 f = 最少(\n -> 永远(\a -> 永远(\b -> eq nab --> (fa == fb))))

这有时被称为Fan Functional，可以追溯到 Brouwer (1920's) 并且它在更高类型的可计算性理论社区中是众所周知的（参见下面的 Normann (2006)）。它找到均匀连续性的 模数，定义为最小自然数[数学处理错误] 以至于

> [数学处理错误]

在哪里
> [数学处理错误]

这里发生的事情是可计算的泛函是连续的，这相当于说有限数量的输出仅取决于有限数量的输入。但是康托空间是紧空间的，在分析和拓扑学中，有一个定理表明定义在紧空间上的连续函数是一致 连续的。在这种情况下，这相当于存在一个单一的 [数学处理错误] [数学处理错误] 这样对于所有输入，查看深度就足够了 得到答案（在这种情况下总是有限的，因为它是一个整数）。我将在另一篇文章中解释所有这些。在这里，我将通过在一些示例中运行该程序来说明这一点。

请注意，Haskell 定义与数学定义相同，前提是我们定义了所有其他需要的成分：

> 最少 :: (Natural -> Bool) -> Natural
> 最少 p = if p 0 then 0 else 1 + least(\n -> p(n+1))

> (-->) :: 布尔 -> 布尔 -> 布尔
> p --> q = 不是 p || q

> eq :: Natural -> Cantor -> Cantor -> Bool
> eq 0 ab = 真
> eq (n+1) ab = an == bn && eq nab

要在实践中理解模函数，请按如下方式定义投影：

> proj :: Natural -> (Cantor -> Integer)
> proj i = \a -> coerce(ai)

然后我们得到：

> *主> 模数 (\a -> 45000)
0
（0.00 秒，0 字节）

> *主>模数（项目1）
2
（0.00 秒，0 字节）

> *主>模数（项目2）
3
（0.01 秒，0 字节）

> *主>模数（项目3）
4
（0.05 秒，820144 字节）

> *主>模数（项目4）
5
（0.30 秒，5173540 字节）

> *主>模数（项目5）
6
（1.69 秒，31112400 字节）

> *主>模数（项目6）
7
（9.24 秒，171456820 字节）

因此，直观地说，模数是函数使用的输入的最后一个索引加一。对于一个常量函数，像上面一样，模数为零，因为没有使用索引。

**技术评论。**证明find_i终止所需的均匀连续性模数的概念 与上面的字面上不同，而是一种轻微的变体（有时称为均匀连续性的内涵模量，而我们的称为外延模量 ）。但我不会在这里讨论这些数学上的微妙之处。主要思想是，当模量为[数学处理错误] [数学处理错误] [数学处理错误]递归终止并遵循find_i定义的一个分支 ，并开始新的递归，以生成示例的下一位。当p的模量 为，谓词\a -> p(Zero # a)的模数是或更小，因此递归调用总是以较小的模数进行，因此最终终止。结束发言。

现在我将尝试更快地实现find。我将分几个阶段修改原始实现。首先，我会通过扩大函数的定义中删除的相互递归forsome在函数的定义find_i：

> find_ii p = if p(Zero # find_ii(\a -> p(Zero # a)))
> 然后零 # find_ii(\a -> p(Zero # a))
> else One # find_ii(\a -> p(One # a))

这应该具有基本相同的速度。现在请注意，如果我们将 0 和 1 放入参数h 中，则条件的分支是相同的。因此，可以按如下方式“分解”条件：

> find_iii :: (Cantor -> Bool) -> Cantor
> find_iii p = h # find_iii(\a -> p(h # a))
> where h = if p(Zero # find_iii(\a -> p(Zero # a))) then Zero else One

对于某些示例，这（指数级！）更快。对此的一个线索是，只有当h被“使用”时才会被评估（我们的语言是惰性的）。让我们运行一个例子，取代的上述定义查找通过查找= find_iii：

> *Main> 等于 fh
真的
（0.00 秒，522668 字节）

> *Main> 等于 (proj 1000) (proj 1000)
真的
（0.00 秒，0 字节）

> *Main> 等于 (proj 1000) (proj 4000)
错误的
（0.03 秒，1422680 字节）

> *Main> 等于 (proj 1000) (proj(2^20))
错误的
（7.02 秒，336290704 字节）

如您所见，我们尝试的投影函数越大，比较的时间就越长。为了看看第一个算法有多糟糕，让我们切换回find = find_i：

> *Main> 等于 (proj 10) (proj 10)
真的
（0.05 秒，1529036 字节）

> *Main> 等于 (proj 10) (proj 15)
错误的
（1.61 秒，72659036 字节）

> *Main> 等于 (proj 10) (proj 20)
错误的
（60.62 秒，2780497676 字节）

前面的例子不能用这个算法运行，除非我们有比可观测宇宙中的原子更多的可用位，并且我们愿意等待几十亿年，因为该算法在连续性模数上是指数级的。

您可能注意到了从find_ii开始的另一个明显改进：

> find_iv :: (Cantor -> Bool) -> Cantor
> find_iv p = let leftbranch = Zero # find_iv(\a -> p(Zero # a))
> in if p(leftbranch)
> 然后左分支
> else One # find_iv(\a -> p(One # a))

其实，我从来没有想过这个算法的性能，也没有试验过。让我们看看我们得到了什么（你需要替换 find = find_iv）：

> *Main> 等于 (proj 10) (proj 20)
错误的
（0.00 秒，522120 字节）

> *Main> 等于 (proj 10) (proj 200)
错误的
（0.04 秒，1550824 字节）

> *Main> 等于 (proj 10) (proj 2000)
错误的
（3.71 秒，146039744 字节）

> *Main> 等于 (proj 10) (proj 20000)
中断了。

比find_i 好得多，但比find_iii差得多 ！我在最后一个例子中放弃了，因为它在一分钟左右后开始减慢我对这篇文章的编辑速度。

但是有一个更好的算法，我现在介绍。我不会试图在这篇文章中解释这个算法的工作（如果你真的感兴趣，请参阅下面我的 LICS'2007 论文），但我在下面包括一些评论：

> find_v :: (Cantor -> Bool) -> Cantor
> find_v p = \n -> if qn (find_v(qn)) then Zero else one
> where qna = p(\i -> if i < n then find_v pi else if i == n then Zero else a(in-1))

除了这个算法之外，上述所有算法都可以很容易地重写为使用惰性列表而不是定义在自然数上的函数。该算法利用了这样一个事实，即要访问表示为函数的序列的元素，不必扫描所有前面的元素。以一种可能神秘的方式，该算法隐式地计算出其参数p使用的条目，并仅显式构造那些条目 。如果你愿意，你可以访问其他的，但算法find_v不会强制他们评估。查看find_v是否正确的一种方法是通过对n的归纳证明find_i pn = find_v pn，这不是太难，尽管如果不仔细引入合适的辅助符号，在某些阶段计算会变得很大。更好的方法是直接理解这一点，如上面的论文中所做的那样（您需要寻找产品功能，它概括了这一点）。

现在这变得非常快（取find = find_v）：

> *Main> 等于 (proj (2^300)) (proj (2^300))
真的
（0.00 秒，522148 字节）
*Main> 等于 (proj (2^300)) (proj (2^400))
错误的
（0.00 秒，525064 字节）

但是，如果函数使用多个参数，而不仅仅是一个（请参见下面的示例），这将不再那么好。为了解决这个问题，首先将上面的程序重写如下，引入一个辅助变量b来命名结果，并将递归调用之一（有两个）替换为使用b代替：

> find_vi :: (Cantor -> Bool) -> Cantor
> find_vi p = b
> where b = \n -> if qn (find_vi(qn)) then Zero else one
> qna = p(\i -> if i < n then bi else if i == n then Zero else a(in-1))

惰性求值在这里无济于事，因为b是一个函数，实际上这会使程序稍微变慢。现在，为了使其更快，我们将恒等函数应用于b的定义。或者更确切地说是恒等函数的一个精心实现，它 以广度优先的方式将b存储到一个无限二叉树中，然后将其检索回来（这个技巧实现了对数开销的记忆）：

> find_vii :: (Cantor -> Bool) -> Cantor
> find_vii p = b
> where b = id'(\n -> if qn (find_vii(qn)) then Zero else one)
> qna = p(\i -> if i < n then bi else if i == n then Zero else a(in-1))

> 数据 T x = B x (T x) (T x)

> 代码 :: (Natural -> x) -> T x
> 代码 f = B (f 0) (代码(\n -> f(2*n+1)))
> (代码(\n -> f(2*n+2)))

> 解码 :: T x -> (自然 -> x)
> 解码 (B xlr) n | n == 0 = x
> | 奇数 n = 解码 l ((n-1) `div` 2)
> | 否则 = 解码 r ((n-2) `div` 2)

> id' :: (自然 -> x) -> (自然 -> x)
> id' = decode.code

现在取find = find_vii，然后测试：

> f',g',h' :: Cantor -> 整数

> f' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(5^80)) 其中 a' i = coerce(ai)

> g' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(6^80)) 其中 a' i = coerce(ai)

> h' a = a' k
> where i = if a'(5^80) == 0 then 0 else 1000
> j = if a'(3^80) == 1 then 10+i else i
> k = if a'(4^80) == 0 then j else 100+j
> a' i = 强制（ai）

> *Main> 等于 f' g'
错误的
（6.75 秒，814435692 字节）

> *Main> 等于 f' h'
真的
（3.20 秒，383266912 字节）

> *Main> 等于 g' h'
错误的
（6.79 秒，813083216 字节）

> *Main> 等于 f' f'
真的
（3.20 秒，383384908 字节）

> *Main> 等于 g' g'
真的
（3.31 秒，400711084 字节）

> *Main> 等于 h' h'
真的
（3.22 秒，383274252 字节）

以上所有算法中，只有find_vii可以应付上面的例子。一个更有趣的例子是这个。两个有限序列[数学处理错误] [数学处理错误] 和 的自然数具有相同的元素集，如果这两个函数

> [数学处理错误] [数学处理错误] 和

是相等的，其中上述符号表示投影的逐点逻辑与（合取），并且其中 [数学处理错误] [数学处理错误] 是长度 . 这是这个想法的一个实现：

> pointwiseand :: [Natural] -> (Cantor -> Bool)
> pointwiseand [] = \b -> 真
> pointwiseand (n:a) = \b -> (bn == One) && pointwiseand ab

> 相同元素 :: [自然] -> [自然] -> 布尔值
> 相同元素 ab = 相等 (pointwiseand a) (pointwiseand b)

> *主要>相同元素
  [6^60, 5^50, 1, 5, 6, 6, 8, 9, 3, 4, 6, 2, 4,6, 1, 6^60, 7^700, 1, 1, 1, 3, 3^30]
  [1, 2, 3, 4, 5, 6, 7, 8, 9, 3^30, 5^50, 6^60, 7^70]
错误的
（0.14 秒，21716248 字节）

> *主要>相同元素
  [6^60, 5^50, 1, 5, 6, 6, 8, 9, 3, 4, 6, 2, 4,6, 1, 6^60, 7^70, 1, 1, 1, 3, 3^30]
  [1, 2, 3, 4, 5, 6, 7, 8, 9, 3^30, 5^50, 6^60, 7^70]
错误的
（0.10 秒，14093520 字节）
*主要>相同元素
  [6^60, 5^50, 1, 5, 6, 6, 8, 9, 3, 4, 6, 2, 4,6, 1, 6^60, 7^70, 1, 1, 1, 3, 3^30]
  [1, 2, 3, 4, 5, 6, 8, 9, 3^30, 5^50, 6^60, 7^70]
真的
（0.10 秒，12610056 字节）
*主要>相同元素
 [6^60, 5^50, 1, 5, 6, 6, 8, 9, 3, 4, 6, 2, 4,6, 1, 6^60, 7^70, 1, 1, 1, 3, 3^30]
 [1, 2, 3, 4, 5, 6, 8, 9, 3^30, 5^50, 6^60, 7^700]
错误的
（0.12 秒，17130684 字节）
*主要>相同元素
[6^60, 5^50, 1, 5, 6, 6, 8, 9, 3, 4, 6, 2, 4,6, 1, 6^60, 7^700, 1, 1, 1, 3, 3^30]
[1, 2, 3, 4, 5, 6, 8, 9, 3^30, 5^50, 6^60, 7^700]
真的
（0.12 秒，17604776 字节）

很自然地会问是否有应用程序验证。我不知道，但Dan Ghica和我推测有，我们正计划对此进行调查。

下面的第一条评论提供了更快的搜索算法。

##### 有评论的参考资料
乌尔里希·伯杰。面积论中的总对象和集合。博士论文，慕尼黑 LMU，1990。
MH 埃斯卡多。 允许快速穷举搜索的无限集。在 LICS'2007，波兰，弗罗茨瓦夫，7 月。下载配套的 Haskell 程序。本文研究了哪些无限集可以进行穷举搜索。它提供了几种算法，用于从旧系统构建新的可搜索集。它还表明，对于丰富的类型集合，任何接受量词的子集也接受搜索者。从量词构造搜索器的算法很慢，所以目前这个结果只具有理论意义。但其他算法很快。
MH 埃斯卡多。 数据类型和经典空间的合成拓扑。ENTCS，Elsevier，第 87 卷，第 21-156 页，2004 年 11 月。我现在将这种程序类型的算法拓扑称为程序类型，而不是数据类型的合成拓扑，在以后的文章中我将这样称呼它。它展示了如何将一般拓扑中的概念和定理直接映射到编程语言中（我再次使用 Haskell）。但它也显示了如何将其映射回经典拓扑。详尽可搜索的集合在那里作为紧凑集合的计算表现形式。
MH Escardo 和 WK Ho。 顺序编程语言的操作域理论和拓扑. 在 Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS)，2005 年 6 月，第 427-436 页。观点。我们没有使用领域理论和拓扑来定义指称语义，而是直接从语言的操作语义（PCF，它可以被视为 Haskell 的忠实子集）中提取它们，回避指称语义。领域理论和指称语义的许多定义在这里作为定理出现。有一个 Berger 程序的证明，包括证明所需的均匀连续性模数的适当概念。
达格诺曼。 用泛函计算——可计算性理论还是计算机科学？. Bulletin of Symbolic Logic, 12(1):43-59, 2006. 这是一篇关于高级可计算性理论的简短历史和综述（该主题是在 1950 年代后期由 Kleene 和 Kreisel 的工作建立的，但有一些先驱）。这个理论在函数式程序员中并不广为人知，但它可能应该是，至少在那些有理论倾向的人中是这样。总有一天有人应该为计算机科学家写一篇说明性的文章。
亚历克斯·辛普森。用于精确实函数的惰性函数算法。在Mathematical Foundations of Computer Science 1998 , Springer LNCS 1450, pp. 456-464, 1998.One 可以使用无限序列来精确表示实数。使用通用量化泛函，Alex Simpson 开发了一种用于黎曼积分的算法。结果证明该算法效率低下，但这不是全称量词的错误：Haskell 分析器告诉我集成程序每秒执行大约 10000 次全称量化，其中 3000 次返回 True。

##### 注释

###### 马丁·埃斯卡多
2007 年 10 月 1 日 16:28
我找到了一种方法，通过避开树并将函数视为树来使最快的算法快 40：

> 查找 = find_viii
> findBit :: (位 -> Bool) -> 位
> findBit p = 如果 p 为零则零否则为一
> 分支 :: Bit -> Cantor -> Cantor -> Cantor
> 分支 xlrn | n == 0 = x
> | 奇数 n = l ((n-1) `div` 2)
> | 否则 = r ((n-2) `div` 2)
> find_viii :: (Cantor -> Bool) -> Cantor
> find_viii p = 分支 xlr
> where x = findBit(\x -> forsome(\l -> forsome(\r -> p(branch xlr))))
> l = find_viii(\l -> forsome(\r -> p(branch xlr)))
> r = find_viii(\r -> p(branch xlr))

这不需要记忆，因为人们需要记住的事情绑定到 where 子句中的变量。使用该算法，比较 f' 和 g' 以及 f' 和 h' 的相等性从 6.75 和 3.20 秒分别移动到 0.14 和 0.09 秒（在所有情况下都使用格拉斯哥解释器）。

###### 为了计算一个函数的定积分，我们必须知道什么？« 异或之锤
2008 年 8 月 21 日 06:54
[...] 实际上这个算法并不完全有效，因为我省略了一些细节，但它基本上是正确的。有关更多信息，请参阅 Alex Simpson 的论文，以及有关 Berger 工作的更多信息，请参阅 Martin EscardÃ³ 的博客文章。[...]

###### 一天的咆哮 - 函数的力量或：我敢打赌你不能用 Java 做到这一点
2008 年 12 月 10 日 04:53
[...] 使用惰性求值，表达式不会在创建后立即求值；相反，它会延迟到需要该表达式的值为止。惰性求值提供的巧妙技巧之一是处理无限集的能力——例如，您实际上可以拥有一个变量，其中包含所有自然数、所有素数或所有斐波那契数。这有时会提供相当令人惊讶的结果 - 例如在无限空间中进行详尽搜索的能力。[...]

###### 杰森·奥伦多夫
2009 年 12 月 9 日 20:06
马丁，整篇文章都很吸引人，但即便如此，最后两句话也是最大的冲击。我应该在哪里寻找后续行动？

###### 马丁·埃斯卡多
2009 年 12 月 16 日 11:29
承诺的后续博客文章还没有写，虽然有一个相关的

http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/

然而，有几篇论文开发/应用了这些想法，可以从我的网页上找到，写在这篇文章之后：

高级计算中的可穷集
（与 P. Oliva）选择函数、条形递归和向后归纳。
在更高类型的设置中可能、必须和概率测试的半可判定性。
高级方程连续解的可计算性。

###### 可搜索的数据类型 « Luke Palmer
2010 年 11 月 17 日 18:13
[...] 几年前，Martín Escardó 写了一篇关于一个看似不可能的程序的文章，该程序可以详尽地搜索不可数的无限 [...]

###### 并非所有可数无限集都相等| 业余拓扑学家
2011 年 1 月 10 日 21:57
[...] 帖子的灵感来自我读过的一篇名为“看似不可能的函数式程序”的有趣帖子，该帖子是关于如何编写搜索无限空间的程序（我称之为 [...]

###### 博多丛林
2011 年 7 月 14 日 01:58
说我疯了，但我打赌“你不能用 Java 做到这一点”。

它来了：看似不可能的功能问题的看似不可能的 Java 实现：https : //github.com/untoldwind/seemingly_impossible

好的，我刚刚实现了前三个 find，我承认这个实现是很容易耗尽 Java-Stack 的可靠方法（如果你让 StackOverflow 运行这些东西，你可能必须使用 -Xss512m 或其他东西）。为了完整起见，我添加了我自己的 find-variant (FindJ)，即您将如何解决“常规 Java”中的这个小问题，无论这意味着什么（咳，它正在 <1ms咳嗽中执行上述示例）。
现在，在西红柿飞起来之前：这是一个黑客！这也不是关于“我的语言比你的好”。函数式编程语言有其吸引力，并且能够以非常自然的方式解决某些类型的问题，Java 实现是一种句法混乱。但是：我严重怀疑有些问题只能用函数式编程语言来解决。毕竟 Haskell 编译器不能变魔术，即使有时看起来如此。

###### 用于在有限时间内无限搜索的 Haskell monad « 数学与计算
2011 年 10 月 18 日 11:26
[...] 无限搜索算法，而且确实可以免费获得。这是我博客文章看似不可能的功能程序的后续。在两篇论文中，允许快速穷举搜索 (LICS07) 的无限集和 [...]

###### 如何让“不可能”的泛函运行得更快 « 数学与计算
2011 年 12 月 6 日 16:27
[...] 位于荷兰莱顿的洛伦兹中心。我解释了如何使用计算效果来加速 Martin Escardo 的不可能的泛函。2011 年 12 月 6 日 | 类别：会谈，[...]

###### 拉尔夫装载机
2012 年 1 月 26 日 05:05
这些对有状态的函数有用吗？为了准确地说明想要什么，人们必须注意外延性（尽管您掩盖了它，就像您需要注意纯功能设置中的整体性一样）。

[即使上述特定程序不适用于有状态函数，但 Kreisel-Lacombe-Shoenfield 定理使人们认为可以对有状态函数执行相同的操作。]

###### 安德烈·鲍尔
2012 年 1 月 26 日 09:11
@Ralph：这篇文章是在纯函数式程序的上下文中编写的，即没有状态，并且所有函数都被假定为（世袭的）全部。有了状态，事情就更复杂了（全局状态、局部状态，扩展函数使用状态意味着什么？）。

###### 马丁·埃斯卡多
2012 年 1 月 26 日 12:22
是的，正如安德烈所说，这里的一切都是外延的和整体的，没有任何影响。但是 Andrej 在洛伦兹中心的 MAP'2011 中做了一个很好的演讲，展示了如何使用效果更快地做到这一点。但在这种情况下，正如你所说，很难严格对待外延性。

拉尔夫装载机
2012 年 1 月 28 日 03:28
事实证明，你可以对我的问题给出一个明智的、否定的答案。find 可以很容易地使用 monad 进行参数化，例如，[将 Bit 和 Bool 合并以节省输入]。

>模块 MFind where
导入 Control.Monad.State
findM :: Ord i => Monad m => ((i -> m Bool) -> m Bool) -> (i -> m Bool)
findM pn = do { x <- q (findM q) ; 返回（不是 x）} 在哪里
   qa = p (\i -> 如果 i == n 然后返回 False else
                 如果 i < n 然后 findM pi else ai)

-- 对 (cx) 进行一次虚拟调用，每次调用时 x 递增 1。
-- 然后返回 (c 5)。
FifthWithDummy :: (Integer -> State Integer Bool) -> State Integer Bool
FifthWithDummy c = 做
  x <- 得到
  放 (x + 1)
  b <- cx
  如果 b 则 c 5 否则 c 5

-- 现在比较
-- findM ($ 5) 0
-  和
-- 运行状态 (findM (fifthWithDummy) 0) 0

永远不会回来。

###### 安德烈·鲍尔
2012 年 1 月 28 日 09:14
@Martin：我关于使用效果更快的函数的讨论是在线的。

###### 所有类型集合的拓扑 « 数学与计算
2012 年 3 月 30 日 00:04
[...] 空间和函数是秘密连续的。我之前在帖子中利用了这一点，看似不可能的函数式程序和使用 Haskell 语言在有限时间内进行无限搜索的 Haskell monad。在语言中 [...]

###### 看似不可能的证明| 数学与计算
2014 年 5 月 9 日 03:26
[...] 这篇看似不可能的函数式程序，我编写了越来越高效的 Haskell 程序来实现数学 [...]

###### 安德鲁·扎巴夫尼科夫
2015 年 8 月 30 日 09:46
Martin，请考虑回答以下问题：http://cs.stackexchange.com/q/45683/37997

预先感谢您的关注:-)

###### 函数式编程：链接、新闻和资源 (16) | 天使“Java”洛佩兹在博客上
2015 年 9 月 23 日 12:11
[…] 看似不可能的函数式程序| 数学和计算 http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ […]

###### 滥用延续 monad——过时的华尔街
2016 年 9 月 22 日 15:41
[…] Escardó 和 Paulo Oliva 关于选择函数。对于 Haskell 程序员来说，最好的起点是看似不可能的函数式程序和序列游戏、Tychonoff 定理和双否定移位的共同点。一世 […]

###### [已解决]：图灵完备性+数据流统一=任意可逆（纯非递归）函数？– 伊格诺集团
2017 年 3 月 3 日 17:16
[...] 还可以在无限惰性数据结构上反转函数。作为这种情况的一个特例，我们有看似不可能的功能程序。如您所见，从某种意义上说，在包含无限 [...] 的域上对函数求逆更容易