我们可以构造一个满足给定位谓词的无限列表吗？

Question

如果我们有一个给定的谓词p :: [Bool] -> Bool，它接受无限列表作为参数并返回True或False基于某些未知条件，并且我们不知道这个谓词是什么。

我们能否设计一个函数f :: ([Bool] -> Bool) -> [Bool]，采用这样的谓词并返回一个无限列表 l where p l == True，假设谓词是可满足的。

Answer 1

您可以将无限列表视为[Bool]最低有效位在前的二进制数：

0 = repeat False
1 = True : repeat False
2 = False : True : repeat False
3 = True : True : repeat False

依此类推直至无穷大。

所以如果你构造一个像这样的函数：

intToBools :: Integer -> [Bool]

那么你可以写

f p = head $ filter p $ map intToBools [0..]

这适用于每个谓词吗p？好吧，如果我们将自己限制在总函数上，那么必须p检查其参数的有限前缀，如果任何有限前缀是可接受的，那么最终必须到达该前缀。

如果p不是全部，但可以返回True至少一个参数（例如谓词“参数至少包含一个True”），那么这个问题就不能像所写的那样解决，因为我们不知道是否p x会终止。然而，如果p可以表示为状态机：

newtype BoolPredicate = BoolPredicate (Bool -> Either Bool BoolPredicate)

那么您可以通过在广度优先搜索中递归地将True和False应用于上一步的输出来枚举每个可能的输入，直到找到Left True。