如果我正确理解Curry-Howard的同构，则每个依赖类型都对应一个定理，实现该定理的程序就是一个证明。这意味着任何数学问题(例如a^n + b^n = c^n)都可以某种方式表示为一种类型。
现在，假设我要设计一个生成随机类型(定理)的游戏，并且在游戏上必须尝试实现这些类型(定理)的程序(证明)。是否有可能控制这些定理的难度？即，简单模式将产生平凡的定理，而困难模式将产生更困难的定理。
最佳答案
单向函数是可以在多项式时间内计算出的函数，但是没有可以在多项式时间内计算出的右逆函数。如果f是单向函数，则可以选择一个参数x，其大小由难度设置确定，计算y = f x，并要求用户以 build 性的方式证明y在f的图像中。
这并非十分简单。没有人知道是否有任何单向功能。大多数人都相信，但事实证明，如果为真，至少与证明P /= NP一样困难。但是，有一束光!人们设法用奇怪的特性来构造函数，如果有任何一种函数是单向的，那么它们必定是单向的。因此，您可以选择这样的功能，并且非常有信心将提供足够困难的问题。不幸的是，我相信所有已知的通用单向功能都是令人讨厌的。因此，您可能会发现很难对它们进行编码，并且您的用户也可能会发现即使是最简单的证明也太困难了。因此，从实际的角度来看，您最好选择像密码散列函数之类的东西，虽然这种可能性不太可能是真正的单向方式，但是对于人类来说，这肯定很难破解。