(Как) Можем ли мы обнаружить / проанализировать проблемы NP в отсутствие модели вычисления Тьюринга?

15

С чисто абстрактной математической / вычислительной точки зрения (как) можно даже узнать или рассуждать о таких проблемах, как 3-SAT, сумма подмножества, коммивояжер и т. Д.,? Сможем ли мы хоть как-то осмыслить их с функциональной точки зрения? Будет ли это вообще возможно?

Я размышлял над этим вопросом исключительно с точки зрения самоисследования как части изучения модели вычисления лямбда-исчисления. Я понимаю, что это «неинтуитивно», и поэтому Годель предпочел модель Тьюринга. Тем не менее, я просто хотел бы знать, каковы известные теоретические ограничения этого функционального стиля вычислений и насколько это мешает анализу класса задач NP?

кандидат наук
источник
Это не вопрос исследовательского уровня для кого-то, кто профессионально занимается теорией языка программирования, но я все еще не думаю, что qasting заслуживает всех отрицательных ответов. Могут ли дауншоттеры рассказать нам, что их беспокоит? Возможно, вопрос можно улучшить.
Андрей Бауэр
2
@AndrejBauer: я понизил голос, потому что (1) я думаю, что (полиномиальная) эквивалентность между машинами Тьюринга и лямбда-исчислением довольно хорошо известна, и (2) пост содержит много пуха, который маскирует это как основной вопрос. Однако ваш ответ показывает, что происходит больше, чем я думал, поэтому я могу поменять свой голос.
Гек Беннетт
Я согласен, что пух принадлежит каналу Discovery.
Андрей Бауэр
2
@AndrejBauer, HuckBennet: Сначала я решил разместить это на портале информатики, но не смог найти соответствующие теги и поэтому разместил его здесь. Я убрал пух, чтобы помочь понять, что именно я хочу знать. Я оставил свою «причину» для того, чтобы задать вопрос, и поэтому отметил его как мягкий вопрос. Я искренне заинтересован в том, чтобы узнать, как можно анализировать проблемы NP исключительно с функциональной точки зрения, и есть ли в этом какая-то ценность - с надеждой, что я пойму что-то более глубокое в лямбда-исчислении
кандидат наук от
Я думаю, что суть вашего вопроса в том, можно ли сложность развить с помощью лямбда-исчисления. Ответ - да, и есть старый вопрос, спрашивающий об этом на сайте iirc.
Каве

Ответы:

16

Возможно, вы захотите взглянуть на семантику стоимости для функциональных языков . Это различные меры вычислительной сложности для функциональных языков, которые не проходят ни через какую-либо машину Тьюринга, машину ОЗУ и т. Д. Хорошее место, чтобы начать поиск - это сообщение Lambda the Ultimate , в котором есть несколько хороших ссылок.

Раздел 7.4 « Практических основ языка программирования» Боба Харпера объясняет семантику затрат.

В статье Об относительной полезности огненных шаров Аккаттоли и Коэна показано, что -calculus имеет самое большее линейное разрушение по отношению к модели машины RAM.λ

Таким образом, на этой другой планете все было бы примерно так же в отношении NP, но было бы меньше переполнений буфера, и не было бы столько мусора, лежащего вокруг.

Андрей Бауэр
источник
Я полагаю, что нетипизированный -калькулус люди по-прежнему изобретают (чистую) схему. Ну что ж. λ
Андрей Бауэр
Это хорошая ссылка на пост LtU. Но есть ли какие-либо ссылки на конкретные примеры доказательства этого класса "NP" с такими проблемами, как 3Sat? Любопытно увидеть «доказательство» в лямбда-исчислении
PhD
Дамиано, вы можете опубликовать свои комментарии как правильный ответ, который демонстрирует, что можно сделать теорию, связанную с NP, непосредственно в -calculus. λ
Андрей Бауэр
@DamianoMazza - я согласен с Андреем и считаю, что ваш комментарий должен быть ответом
кандидат наук
@ Андрей: Готово! Я удалил свои предыдущие комментарии.
Дамиано Мазза
14

По просьбе Андрея и доктора наук я превращаю свой комментарий в ответ с извинениями за саморекламу.

Недавно я написал статью, в которой я смотрю, как доказать теорему Кука-Левина ( -полнота SAT), используя функциональный язык (вариант λ-исчисления) вместо машин Тьюринга. Резюме:Nп

  • ключевым понятием является понятие аффинных приближений, то есть приближение произвольных программ аффинными (которые могут использовать свои входные данные не более одного раза); интуиция заключается в том, что поэтому аффинные термины аппроксимируют произвольные вычисления произвольно так же, как булевы схемы;
    Булевы схемыМашины Тьюрингазнак равноаффинное λ-условияλ-условия
    λ
  • в результате, в мире -calculus доказательство является гораздо более «высокоуровневым», оно использует теорию порядка, непрерывность по Скотту и т. д. вместо взлома логических схем; в частности, лозунг «вычисления локальны» (который задается многими как сообщение, лежащее в основе теоремы Кука-Левина), становится «вычисление непрерывным», как и ожидалось;λ
  • однако «естественная» -полная проблема - это не CIRCUIT SAT, а HO CIRCUIT SAT, своего рода «разрешимость» линейных λ-членов или, точнее, линейных логических сетей доказательства (которые подобны сеткам более высокого порядка) Булевы схемы);Nп
  • конечно, можно затем уменьшить HO CIRCUIT SAT до CIRCUIT SAT, доказав тем самым обычную теорему Кука-Левина, и все детали низкоуровневого уровня будут перемещены в построение такого сокращения.

Таким образом, единственное, что могло бы измениться «на этой стороне планеты», это, возможно, то, что мы бы рассматривали проблему, связанную с λ-исчислением, а не проблему, связанную с булевыми контурами, как «изначальную» полная проблема.Nп

Примечание: вышеупомянутое доказательство может быть переформулировано в варианте калькулятора Аккаттоли с линейными явными заменами, упомянутыми в ответе Андрея, который, возможно, является более стандартным, чем -calculus, который я использую в своей статье.λλ


Позже отредактируйте: мой ответ был чуть больше, чем вырезка и вставка из моего комментария, и я понимаю, что следует сказать еще кое-что относительно сути вопроса, который, насколько я понимаю, таков: возможно ли будет разработать теория -полноты без машин Тьюринга?Nп

Я согласен с комментарием Каве: ответ - да , но, возможно, только в перспективе. То есть, когда речь идет о сложности (считая время и пространство), машины Тьюринга непревзойденны по простоте, модель затрат очевидна для времени и почти самоочевидна для пространства. В calculus все гораздо менее очевидно: модели стоимости времени, упомянутые Андреем и приведенные в книге Харпера, относятся к середине 90-х годов, модели стоимости пространства все еще практически не существуют (я знаю, по сути, одну работу опубликовано в 2008 году ).λ

Так что, конечно, мы можем делать все, используя чисто функциональную перспективу, но трудно представить альтернативную вселенную, в которой Хартманис и Стернс определяют классы сложности, используя -terms, и спустя 30-50 лет люди начинают адаптировать свою работу к Машины Тьюринга.λ

Затем, как отмечает Каве, есть «социальный» аспект: люди были убеждены, что -полнота важна, потому что Кук доказал, что проблема, которая считается центральной в широко изучаемой области (доказательство теорем), является -complete (или, в более современной терминологии, с использованием сокращений Карпа, ). Хотя вышеизложенное показывает, что это может быть сделано в -calculus, возможно, это будет не самая немедленная вещь (у меня есть резервы на этот счет, но давайте не будем делать этот пост слишком длинным).NпNпсоNпλ

И последнее, но не менее важное: стоит отметить, что даже в моей работе, упомянутой выше, когда я показываю, что HO CIRCUIT SAT может быть уменьшен до CIRCUIT SAT, я явно не показываю -term, вычисляющий сокращение, и доказываю, что он всегда нормализует за полиномиальное число крайних левых шагов редукции; Я просто показываю, что существует алгоритм, который, интуитивно, может быть реализован за полиномиальное время, точно так же, как любой теоретик сложности не будет явно строить машину Тьюринга и доказывать это за время (что, позвольте мне сказать, было бы даже безумнее, чем записывать - терм, не говоря уже проверку ошибок).λλ

Это явление широко распространено в теории логики и вычислимости, теория сложности просто наследует его: формальные системы и модели вычислений часто используются только для того, чтобы знать, что можно формализовать интуицию; после этого одной интуиции почти всегда достаточно (если ее использовать осторожно). Таким образом, рассуждения о сложности решения таких проблем, как SAT, TAUT, SUBSET SUM, GI и т. Д., И, следовательно, развитие теории -полноты, могут в значительной степени выполняться независимо от базовой вычислительной модели, если только Стоимость модели найдена. -исчисление, машины Тьюринга или программа BrainfuckNпλЭто не имеет значения, если вы знаете, что ваша интуиция здорова. Машины Тьюринга дали немедленный, работоспособный ответ, и люди не чувствовали (и все еще не чувствуют) необходимости идти дальше.

Дамиано Мазза
источник
2
Просто разъяснение, которое многие пропускают: Стив доказал NP-полноту для TAUT, там доказательство для SAT неявно. Понятие сокращения Карпа в то время не существовало. Также важно отметить, что TAUT был причиной, по которой Стив заинтересовался этой темой и занимает центральное место в автоматическом доказательстве теорем, будут ли люди так же заинтересованы в разрешимости линейных лямбда-членов? Альтернативное развитие возможно, но произойдет ли это без предвидения NP-полноты? Я нахожу это маловероятным, учитывая, что альтернативное развитие довольно недавно. :)
Kaveh
1
Я помню, как читал где-то, что частью мотивации Левина к разработке NP-полноты была неспособность решить проблему изоморфизма графов и минимального размера схемы (MCSP), и надежда показать, что они были (как мы теперь будем называть) NP-трудными. По крайней мере, Г.И. все еще существовал бы в мире лямбд ...
Джошуа Грохов
1
@Kaveh, спасибо за ваш комментарий, я добавил несколько абзацев, чтобы завершить ответ.
Дамиано Мазза
1
@ Джош, так будет ТАУ и САТ.
Каве