算法与计算机科学math.andrej.com
看似不可能的函数式程序（2007）
Seemingly impossible functional programs (2007)
2015 — 2021，它一次次回到首页
黑点是上首页（≥ 50 分）的那次投稿，空心点是没冲上去的投稿，点越大分数越高。
导读
Martin Escardó 的经典博文，展示如何在 Haskell 中对看似不可数的康托空间（无限二进制序列）上的全函数进行“穷举搜索”，从而可判定某些函数类型的相等性。这看似违背直觉，实则依赖于全函数只能读取有限前缀这一事实。
为什么经久不衰：它以优雅的函数式编程技巧颠覆了“函数相等不可判定”的常识，多年间反复登上 HN 首页，至今仍是理解惰性求值与拓扑学联系的绝佳入门。
HN 评论精选
这篇文章对读者的学术道路产生了深远影响，作者本人是该领域的活跃数学家。
三年前发现这篇文章时，它彻底改变了我的人生。我此前不理解计算机能以有意义的方式处理无限集合的抽象逻辑，它把我引向了在依赖类型语言 Agda 中进行数学形式化的世界——这正是作者 Martin Escardó 目前的研究方向之一。
mycroftiv查看英文原文
I found this post and the code and math so fascinating it changed my life when I found it three years ago. I did not previously understand the capability of computers to work with the abstract logic of infinite sets in a meaningful way and it led me into the world of formalization of mathematics in the dependently typed programming language Agda, which is one of the current activities of the mathematician (Martin Escardo) who wrote this guest blog post.
用通俗语言解释了原理：全函数只读有限位，惰性求值让搜索可以在恰当时候终止。
我的理解：p 是一个接受无限位串、返回真假的 Haskell 函数。关键在于 p 只能查看有限个位，否则对某个输入它永远不会返回。命令式程序员会写循环穷举，但不知道何时停止以返回“未找到”。如果能检测 p 何时索要超出已生成的位，搜索就能终止——Haskell 的惰性求值正好能“驱动这个循环”。
ridiculous_fish查看英文原文
Here's my attempt to translate. I think it's probably wrong and welcome corrections. You have a function `p` which accepts an "element of the Cantor space" (infinite sequence of bits) and returns true or false. You want to find some value where it returns true, or prove that it returns false for every value. Crucially `p` is not a math function, it is a Haskell function. So you can't say "p is true iff its argument is pi" because you can't write that in Haskell. In fact, all `p` can do is look at finitely many bits - if it looks at infinite bits, there is an input for which it will never return. And because it looks at finitely many bits, there is necessarily a largest bit-index which it looks at. Now a generic-imperative programmer might attempt: for (bignum x = 0; x < infinity; x++) if (p(x)) return x; return NotFound; but the problem is knowing when to stop, so as to return NotFound. However, if we could detect when `p` demands more bits than we have produced, then the search will terminate: int bits = 0; bignum x = 0; while (x < (1 << bits)) { try { if (p(x)) return x; x++; } catch (BitAccessOutOfBounds) { bits++; } } return NotFound; Haskell's laziness enables it to "drive the loop" but the idea is not so different.
质疑性评论：认为这只是有限前缀上的平凡搜索，并对可判定相等性的结论表示怀疑。
这看起来不过是雕虫小技。真正的穷举搜索不可能存在，因为康托空间不可数。文章只是通过只看序列前 n 位绕开了这一点，搜索 2^7 个元素当然很快。另外我怀疑“某些函数类型有可判定相等性”的说法，似乎可以用整数编码构造反例。
anfelor查看英文原文
This seems like little more than a parlor trick. First, a true "exhaustive search" is actually impossible. The cantor space is uncountable (which can be seen by prepending '0.' before every binary sequence which gives the real number interval [0,1).) But an exhaustive search will visit all elements in some order which provides an ordering. Thus its existence implies that the cantor space is countable. Contradiction. The post gets around this by only looking at the first n elements of every binary sequence: f,g and h evaluate little more than the 7th digit. Sure, exhaustively searching 2^7 elements can be done in less than a second, why is this new? > In fact, e.g. the function type Integer -> Integer doesn’t have decidable equality because of the Halting Problem, as is well known. However, common wisdom is not always correct, and, in fact, some other function types do have decidable equality, for example the type Cantor -> y for any type y with decidable equality, without contradicting Turing. I fail to see how this can be true. We can set y = Integer, since integers have decidable equality. Then we can encode every integer as an element of cantor space by converting it into binary with the least significant digit first (and using the 0th element of the sequence to distinguish positive and negative integers) and padding the sequence with zeros towards infinity. Then two functions f,g : Integer -> Integer are equal iff their transformed representations f . p, g . p : Cantor -> Integer are equal. Thus functions from the cantor space having decidable equality implies functions from the integers having decidable equality which "solves" the halting problem. Again the post gets around this by only looking at the first few elements... but equality of functions f,g : Integer -> Integer is trivially decidable if f and g are zero for integers bigger than some N, so how is this new?
从拓扑学紧性角度解释为什么全函数必然有运行时间上界。
我的粗浅理解：如果全函数 f 的运行时间没有上界，那它其实不是全函数。看似可以构造一列输入使运行时间趋于无穷，但由紧性，这列点有收敛子列，其极限点 y 与前面的点在越来越长的前缀上无法区分，导致 f 处理 y 时要做越来越多的工作，即 f 在 y 上不终止。
cvoss查看英文原文
I think I have a half-baked understanding of what's going on here. Let me talk through it. Take a function f : unit_interval -> bool. I believe that if there is no bound on the execution time of f, then f must not be a total function. (So conversely, if f is total, then it has bounded execution time, and is therefore only considering prefixes of the digit streams of up to some bounded length. From there, searching for an example input x s.t. f(x) = true is easy.) Naively, it would seem plausible that there exists a total function which, nevertheless, takes longer and longer to run on a particular sequence of inputs. So let such a sequence be given, where the runtime of f(x_i) tends to infinity, even though it is finite for each x_i. But from topology, we know that a sequence of points in a compact space, like the unit interval, has a convergent subsequence. The interesting thing happens when you look at f(y) where y is the limit point of such a subsequence. It is the case that as i increases, x_i and y increasingly look the same for longer and longer prefixes of their decimal (binary) expansions. Therefore, f has to do more and more work to tell apart x_i and y, which gives us an argument that there is no bound on the runtime of f(y); i.e., f doesn't terminate for that particular input. (Except, you have to get nitpicky about redundant representations of reals like 0.0099999... vs 0.010000..., but we can always choose the representation of y that suits us: the one that looks more like the x_i's.)
历次讨论
同类还值得读
位运算技巧集
Bit Twiddling Hacks
斯坦福页面上的经典位运算技巧合集，收录了 popcount、前导/尾随零、位反转、交换、舍入等大量技巧，并附有解释和性能讨论。
算法与计算机科学上首页 8 次 · 2011–2024graphics.stanford.edu编辑精选如何不按平均评分排序
How Not To Sort By Average Rating
经典文章解释了为什么按平均评分排序不可靠：只有少量评价的条目（比如仅一条五星）会轻易排到最前，而评价数量的差异被忽略。
算法与计算机科学上首页 7 次 · 2009–2024evanmiller.org编辑精选数据结构可视化
Data Structure Visualizations
旧金山大学 David Galles 教授制作的数据结构与算法交互式可视化网站，涵盖 B 树、红黑树、排序、图算法等，可逐步操作观察其运行过程。
算法与计算机科学上首页 6 次 · 2011–2021cs.usfca.edu编辑精选1996 年以来的计算机科学最佳论文奖
Best Paper Awards in Computer Science since 1996
Jeff Huang 维护的一个汇总页面，收录了自 1996 年以来计算机科学各主要会议的“最佳论文奖”获奖名单，并按年份和会议整理，方便读者一站式浏览历届获奖论文。
算法与计算机科学上首页 6 次 · 2010–2018jeffhuang.com编辑精选算法（Jeff Erickson）
Algorithms, by Jeff Erickson
伊利诺伊大学 Jeff Erickson 教授的算法课教材，免费在线开放。
算法与计算机科学上首页 5 次 · 2018–2022jeffe.cs.illinois.edu编辑精选