Заміна логічного-конструктивного з комбінаторсько-конструктивним?

Логіки дуже точно інтерпретують слово "конструктивне": вони вважають це більш-менш "обчислюваним". Сприймаючи конструктивність всерйоз і працюючи в світі, де все повинно бути конструктивним, веде до інтуїціоністської логіки, яка була дуже продуктивним і захоплюючою підполею логіки.

З іншого боку, комбінатори використовують "конструктивні" в іншому сенсі. Вони використовують це для означення "краще, ніж груба сила". Наприклад, теорема Ремзі неконструктивна з POV комбінатори, оскільки її доказ не дає жодного методу краще, ніж просто перерахування підграфів, поки ви не знайдете повного монохроматичного. З іншого боку, з логічного POV він конструктивний - просто перелічіть підграфів, поки не знайдете повний монохроматичний! (І ще простіше, принцип голубці має той самий смак.)

Тому:

  1. Хто-небудь дивився на логіку, в якій тільки комбінатори-конструктивні методи добре?
  2. Якщо ні, чи хтось зробив офіційний аналіз того, що означає "краще, ніж груба сила"? (Це здається інакше, ніж питання, які зазвичай задаються в алгоритміці, але я б не був би шокований, якщо про це теж подумали).
12
2. Це головна проблема, я вважаю. Чи "груба сила мінус 10 випадків, які можна тривало виключати заздалегідь" краще, ніж груба сила? Я думаю, що річ, що йде поруч з вашим "комбінатористом-конструктивним", є P (на відміну від NP).
додано Автор James Fee, джерело

7 Відповіді

Ви запитаєте про логіку, що стосується ресурсів. Ви можете подивитися на роботу Сам Бус та його логіку, які характеризують різні класи складності. Існує також безліч подальших робіт з неявних характеристик класів складності . В іншому рядку роботи ви можете подивитися на підструктурну логіку, таку як лінійна логіка.

Я підозрюю, що ми можемо характеризувати "пошук грубої сили" з точки зору обчислюваної складності. Наприклад, якщо розмір стану має розмір $ N $, і пошук займає $ O (\ log N) $, то, мабуть, це не груба сила. Якщо це $ \ omega (N) $, то, мабуть, це груба сила.

8
додано

тому, щоб бути зрозумілим, причина того, що кінцеві версії теореми Ремзі та принцип pigeonhole є інтуїціоністичними, це означає, що у вас є чітке обмеження в просторі пошуку. Якщо пошуковий простір був апріорним необмеженим (як у нескінченних варіантах цих теорем), ці докази будуть застосовувати принцип Маркова. У цьому випадку для того, щоб заборонити такі "комбінаторно неконструктивні" докази, я впевнений, що ви повинні перейти до ультрафізичної логіки, тобто заперечувати існування дуже великих чисел. Тому що кожного разу, коли у нас є один, ми можемо поспілкуватися з ним, щоб виконати конструктивний пошук над дуже великим простором.

Я думаю, що проблема з використанням класичних класів складності для підходу до цього полягає в тому, що існує алгоритм Р-часу (дійсно постійного часу) для обчислення числа Ремсея R (6,6), який не буде припинятися в життєвий час Всесвіту .

6
додано
Заборона комбінаторно неконструктивних доказів не вимагає заперечення наявності дуже великих чисел. Це вимагає лише послаблення схеми індукції арифметики Peano в першому порядку, щоб ви більше не могли довести, що функції надмірно швидко зростаючої визначено скрізь. Дивіться книгу Кука і Нгуєна, про яку я згадую у своєму відповіді.
додано Автор Joel Brown, джерело
Ну, я думаю, ви могли б сказати це так, але я вважаю за краще висловлювати це таким чином: ви пишете визначення того, що, як передбачається, є функцією для всіх натуральних чисел, але ви не можете довести, що це визначено скрізь Справа в тому, що немає конкретної великої кількості, яку ви не можете довести існувати. Обмеження на те, що ви можете довести про функції, які ростуть занадто швидко. Це цілком аналогічно тому, що теорема Уоркестана неможлива в П., оскільки ця функція зростає надто швидко. З цієї причини я б не назвав ПА "ультрафінітним".
додано Автор Joel Brown, джерело
Дякуємо за посилання, і так, можливо, не обов'язково згадати про ультрафінітізм, який не є чітко визначеною математичною концепцією. Це - ефект ослабленої індукційної схеми, правда, чи не так? І.е., це заважає вам надавати докази існування дуже великих чисел?
додано Автор Noam Zeilberger, джерело

Although the question of finding explicit constructions was considered in combinatorics very early, theoretical computer science gives a fairly concrete way to say what "constructive" means. Lower bounds for Ramsey numbers is a good example. it was discussed in this MO question. Probabilistic methods shows that there are graphs with $2^{k/2}$ vertices without a complete subgraph or an empty subgraph on k vertices. Explicit constructions are constructions that can be described by a polynomial type (deterministic) algorithm. (But you can demand also a stronger requirement of log-space algorithms.) the best known explicit constructions (that can be described by a log space algorithm) gives such graphs with number of vertices proportional to $2^{k^C}$ vertices for every C>0. In combinatorics explicit constructions are usually related to derandomization. See also this post about derandomization.

Я не впевнений, яким є зв'язок між логічним-конструктивним, як описано у питанні, а також явним побудовою та дерендомізацією в комбінаториці. Схоже, що вони пов'язані з поняттям "ефективні та неефективні" докази, де неефективні докази є доказами, які так і не дають алгоритму. Відомим неефективним доказом є твердження (від Неша) про те, що перший гравець у російській г-ні HEX ​​має виграшну стратегію. (Використання аргументу стратегії викрадення.) Іншим прикладом подібного характеру є аргумент про те, що існують ірраціональні а і Ь так, щоб $ a ^ b $ було раціональним. (На основі $ (\ sqrt 2 ^ (\ sqrt 2)) ^ \ sqrt 2 = 2 $.) Я думаю, що відома сфера, де ефективні докази дуже бажані, є у контексті покращень теореми Лювла про транскендентні числа. Отже, може бути, відмінність між ефективними та неефективними доказами наближається до логічних питань, на які посилається це питання.

5
додано
Цікавий пост, але я не думаю, що приклад, як приклад неефективного або не явного доказу, є фальшивим. Це правда, що термін "неефективний доказ" не завжди точний або формальний.
додано Автор Pierre Spring, джерело
Вау, що алгоритм Goldwasser/Kilian дійсно дивовижний! Це "майже завжди" швидко закінчується, що акуратно. Чи існують будь-які швидкі "майже завжди" напів-алгоритми? (Тобто, ви не можете взагалі припинити використання "не багатьох" входів). Більшість напів-алгоритмів, які я знаю, походять від таких речей, як повнота логіки першого порядку, тому їх найгірший показник невизначеності. Чи є якісь алгоритми, які ви знаєте, швидко закінчаться, якщо вони закінчуються взагалі? (Причина, про яку я питаю, полягає в тому, що це спростувати думку, що комбінаторно-конструктивні методи підмножили інтуїціоністські методи.)
додано Автор Sekhat, джерело
Точка Нейла полягає в тому, що "неефективні докази" в сильному сенсі відсутності будь-якого алгоритму взагалі чудово схоплені інтуїціоністською логікою. Наприклад, теорема кінцевості Faltings не дає алгоритму для пошуку рішень, а інтуїціоніст висловлює це, сказавши, що набір рішень є "не нескінченним" (на відміну від "кінцевих"). Питання полягає в тому, чи існує аналогічний спосіб формально фіксувати той факт, що (наприклад) імовірнісний існування доказів графів Ремсея не дає жодної багатогранної конструкції? Відповідь так: доказ не формалізується в певній системі обмеженої арифметики.
додано Автор Joel Brown, джерело
Іноді конструктивний крок просто передбачає більш ретельне зазначення того, що це таке, що свідчить доказ. У Hex не може бути жеребкування, і це не той випадок, коли другий гравець має виграшну стратегію. Напевно, кожна цифра збігається з рівною частотою в Pi. Класично, принаймні, один з'являється нескінченно часто (насправді як мінімум два). Конструктивно, вони не всі з'являються звичайно. Деколи після цієї дисципліни фактично спрямовується на більш міцні докази (але це тема для іншого питання).
додано Автор CurseStacker, джерело
Приклад «ірраціональний до ірраціональний = раціональний» є фальшивим, див. math.andrej.com/2009/12/28/ …
додано Автор Andrej Bauer, джерело

Я думаю, найближче до того, що ви шукаєте, - це логічні системи, вивчені в недавній книзі Кука та Нгуєна Логічні основи складної доказності . Це системи, в яких сукупні функції, що доказуються, лежать в деяких чітко визначених класах складної математики. Зокрема, існування доказів у цих системах означає, що об'єкт, існування якого заявляється, може бути обчислено "легко".

Ця лінія досліджень іде, як мінімум, до Буса (як згадував Андрей Бауер), який визначив системи обмеженої арифметики, які тісно пов'язані з рівнями поліномиальної ієрархії (ієрархія класів складності, найнижчі рівні яких - $ P $ і $ NP $). У загальному випадку поле, відоме як "складність доказів", присвячене вивченню взаємозв'язку класів складної складності (особливо класів складності схеми) та формальних систем арифметики з відповідним чином ослабленими індукційними аксіомами.

Це все припускає, що ви задоволені ідеєю, що "краще, ніж груба сила" означає щось на кшталт "розсудливим до вподоби". Існує обмеження з поняттям розв'язності часу полиноми, зокрема його наголосом на асимптотичні поведінці та його зосередженню на найгіршому складності. (Хоча дослідження середньої складності було вивчено, природні питання там дуже важко відповісти, і теорія набагато менш розвинена.) Проте багато цікавих поглядів виникла з вивчення складної спроможності, і я думаю, що це дуже перспективний шлях для подальших досліджень.

5
додано

Я думаю, що весь предмет теорії обчислювальної складності з поняттями P, NP, PSPACE, EXPTIME і так далі, по суті, полягає в дослідженні різних точних почуттів про те, що може означати "краще, ніж груба сила".

Наприклад, комбінатори вважають багатогранні алгоритми принципово конструктивними, тоді як алгоритми грубої сили за своєю суттю є експоненціальним часом. Тонкий NP-клас допускає конструктивний, але недетерміністичний аромат, в тому, що розчини можна швидко перевірити, але важко їх побудувати. Існує цілий зоопарк класів складності , чиї взаємозв'язки інтенсивно вивчаються в теорії складності. (Див. Також зоопарк лайнів там, для початківців.)

3
додано
Ті тонкі відмінності, про які ви згадуєте, наприклад, різниця між середньою складністю випадку та складністю гіршого випадку, не знехтували і також добре вивчені. Наприклад, див. Розділ en.wikipedia.org/wiki/Generic-case_complexity .
додано Автор Dane O'Connor, джерело
Наприклад, рандомізовані алгоритми (див. en.wikipedia.org/wiki/Randomized_algorithm ) були колись розглянуті як нестандартні, але тепер цілком класичні методи, у порівнянні з більш езотеричними поточними міркуваннями, такими як квантові обчислення.
додано Автор Dane O'Connor, джерело
Існує безліч алгоритмів, які є найгіршими дворазово-експоненціальними, що на практиці часто закінчуються швидко (наочним прикладом - основи Грейбнера). Алгоритми в $ n ^ 17 $ для навіть помірних n фактично ніколи не закінчаться. Отже, на практиці корисні класи набагато тонші, ніж ті, які теоретики вирішили навчатися, IMHO. Аналогічно всі невичерпні проблеми мають (великі!) Вирішальні фрагменти [наприклад, "Заливання", які ви знаєте краще, ніж я].
додано Автор Mathias711, джерело

Я завжди розглядав роботу над логікою, де нормалізація характеризує певні класи складності (особливо: Робота Мейсона на PTIME та лінійної логіки ), щоб потрапити до цієї категорії. Я думаю (як зазначає Ноам коментар), це поняття на основі складності, яке, здається, не фіксує поняття "краще, ніж груба сила", яку ви шукаєте.

1
додано

Вирішення питання 1: Ви можете подивитися на Анотація кам'яної подвійності Пауля Тейлора, можливо, починаючи з Основи для обчислюваної топології . Він робить багато роботи, яка є дуже конструктивною за своєю природою, і він, здається, проходить дуже довгий шлях, суттєво переробляючи цілком навантаження математики та логіки з конструктивного кута.

1
додано
Моя мета з ASD полягає в тому, щоб розвинути мову, яка виглядає максимально як "звичайна математика", але яка має вирішальну основу замість теорії встановлення. Якби тільки люди знали формальне визначення обчислюваності, я вважаю, що це була сила традиційних основ, перш ніж почалася теорія встановлення, і що природна математика є обчислюваною. Крім того, Обчислення лямбда для реального аналізу може бути кращим місцем для початку з ASD.
Питання, однак, полягає в тому, що я думаю про різницю між обчислювальністю та здійсненністю (скажімо, поліноміальний час). Хоча є логіка ресурсів, про яку можна говорити про це, вони виглядають набагато сильніше, ніж звичайна математика, ніж ASD. Я думаю, що це потрібно перш за все розподілити на обчислюваному рівні, залишивши реальну версію іншому поколінню.
додано Автор fearphage, джерело