haskell - 是否可以随机生成任意难以证明的定理？

Question

如果我正确理解了 Curry-Howard 的同构，那么每个依赖类型都对应一个定理，实现它的程序就是一个证明。这意味着任何数学问题，例如 a^n + b^n = c^n可以以某种方式表示为一种类型。

现在，假设我想设计一个生成随机类型(定理)的游戏，并且游戏必须尝试实现这些类型(定理)的程序(证明)。是否有可能控制这些定理的难度？即，简单模式会产生微不足道的定理，而困难模式会产生更难的定理。

Answer 1

单向函数是可以在多项式时间内计算的函数，但它没有可以在多项式时间内计算的右逆。如果 f是单向函数，那么你可以选择一个参数x其大小由难度设置决定，计算y = f x ，并要求用户 build 性地证明 y在 f 的图像中.

这不是很简单。没有人知道是否有单向函数。大多数人都相信有，但证明如果是真的，至少和证明 P /= NP 一样难。 .然而，有一丝光亮!人们已经设法构造了具有奇怪属性的函数，即如果任何函数是单向的，那么它们一定是单向的。所以你可以选择这样一个函数，并且非常有信心你会提供足够困难的问题。不幸的是，我相信所有已知的通用单向函数都非常讨厌。因此，您可能会发现很难对其进行编码，并且您的用户可能会发现即使是最简单的证明也太难了。因此，从实际的角度来看，您最好选择像加密哈希函数这样的东西，它不太可能是真正的单向函数，但人类肯定很难破解。