Можно ли случайным образом порождать теоремы, которые трудно доказать?

Question

Если я правильно понимаю изоморфизм Карри-Говарда, каждый зависимый тип соответствует теореме, для которой реализующая ее программа является доказательством. Это означает, что любая математическая проблема, например a^n + b^n = c^n, может быть как-то выражена как тип.

Теперь предположим, что я хочу создать игру, которая генерирует случайные типы (теоремы) и на которых пьесы должны пытаться реализовать программы (доказательства) этих типов (теорем). Возможно ли контролировать сложность этих теорем? I., простой режим будет генерировать тривиальные теоремы, в то время как жесткий режим будет генерировать гораздо более сложные теоремы.

Answer 1

Односторонняя функция - это функция, которая может быть рассчитана в полиномиальное время, но не имеет правильного обратного, который может быть рассчитан в полиномиальное время. Если f является однонаправленной функцией, вы можете выбрать аргумент x, размер которого определяется настройкой сложности, рассчитать y = f x и попросить пользователя доказать конструктивно, что y находится на изображении f.

Это не так просто. Никто не знает, есть ли какие-либо односторонние функции. Большинство людей считают, что есть, но доказательство того, что, если это правда, известно как минимум так же сложно, как и доказывает P /= NP. Однако есть луч света! Людям удалось построить функции со странным свойством: если любые функции являются однонаправленными, то это должно быть. Таким образом, вы можете выбрать такую ​​функцию и быть достаточно уверенным, что будете предлагать достаточно сложные проблемы. К сожалению, я считаю, что все известные универсальные односторонние функции довольно неприятны. Поэтому вам, скорее всего, будет сложно их кодировать, и ваши пользователи, скорее всего, найдут даже самые простые доказательства слишком сложными. Итак, с практической точки зрения, вам может быть лучше выбрать что-то вроде криптографической хеш-функции, которая не настолько полно, чтобы быть по-настоящему односторонней, но это наверняка будет трудно для человека взломать.

Answer 2

Если вы создаете только типы, большинство из них будут изоморфны ⊥. ∀ n m -> n + m ≡ m + n имеет смысл, но ∀ n m -> n + m ≡ n, ∀ n m -> n + m ≡ suc m, ∀ n m -> n + m ≡ 0, ∀ n m xs -> n + m ≡ length xs и другие, а не другие. Вы можете попытаться создать хорошо типизированные термины, а затем проверить, используя что-то вроде Djinn, что тип сгенерированного термина не заселен гораздо более простым термином. Однако многие сгенерированные термины будут либо слишком простым, либо бессмысленным мусором даже с clever strategy. Типовая настройка содержит меньше терминов, чем непечатаемых, но тип одной переменной может быть A, A -> A, A -> B, B -> A, A -> ... -> E и все эти переменные типа могут быть свободными или количественно оцениваться по всему объему. Кроме того, ∀ A B -> A -> B -> B и ∀ B A -> A -> B -> B являются по сути одними и теми же типами, поэтому ваше равенство не просто αη, а нечто более сложное. Пространство поиска просто слишком велико, и я сомневаюсь, что случайный генератор может создать что-то действительно нетривиальное.

Но, может быть, могут быть интересны условия определенной формы. Bakuriu в комментариях предложенных теорем, предоставляемых параметризмом: вы можете просто взять Data.List.Base или Function или любой другой базовый модуль из стандартной библиотеки Agda и создать много теорем из воздуха. Проверьте также статью A computational interpretation of parametricity, которая дает алгоритм вывода теорем из типов в зависимости от типизированной настройки (хотя я не знаю, как это связано с Theorems for free, и они не дают правил для типов данных). Но я не уверен, что большинство выпущенных теорем не будет доказано простой индукцией. Хотя, теоремы о функциях, которые являются экземплярами левых складок, обычно сложнее, чем о тех, которые являются примерами правильных складок - это может быть один критерий.

Answer 3

Это относится к интересному и сложному полю доказывания нижних границ сложности доказательства. Во-первых, это очень зависит от силы используемой логической системы и каких доказательств она позволяет. Предложение может быть трудно доказать в одной системе и легко доказать в другом.

Следующая проблема заключается в том, что для случайного предложения (в достаточно сильной логической системе) даже невозможно решить, является ли это доказуемым или нет (например, множество доказуемых предложений в логике первого порядка есть только recursively enumerable). И даже если мы знаем, что это доказуемо, решение сложной сложности теста может быть чрезвычайно трудным или неразрешим (если вы найдете доказательство, это не значит, что это самый короткий).

Интуитивно похоже на Kolmogorov complexity: Для общей строки мы не можем сказать, что является самой короткой программой, которая ее производит.

Для некоторых систем доказательств и конкретных типов формул известны нижние границы. Хакен доказали в 1989 году:

При достаточно больших п, любое разрешение доказательство PHP^п {п-1} _ (Pigeon принцип дырка) требует длины 2^{\ Omega (п)} ,

These slides дайте обзор теоремы. Таким образом, вы можете создавать предложения, используя такую ​​схему, но это, вероятно, не будет очень интересно для игры.