Алгоритмы представления деревьев линейными словами

[Профессор Снэйп]

Sashamandra в сообщении #294952 писал(а):

Если бы язык определи в конструктивной математике, а не на бумаге, то необходимости в гёделевской нумерации не возникло бы. Чувствуете разницу?

Глупость сие...

Причина гёделевской нумерации в том, что Гёделю надо было погрузить метаязык арифметики в саму арифметику. Теорему о неполноте доказывать, то да сё. Так что необходимость возникает по любому.

А алгоритмы в современном понимании работают с любыми типами конструктивных данных. И в современных статьях никто на гёделевские нумерации не заморачивается. Если видят конструктивный объект, видят явно описанный алгоритм, то функция вычислима и всё, дальше с ней работают без проблем.

[Sashamandra]

Цитата:

Глупость сие...

Ну и? Так в чем вы глупость усмотрели?

[Профессор Снэйп]

Объясните, как можно доказать теорему о неполноте без гёделевской нумерации.

Я вообще не понимаю, что значит "определить язык в конструктивной математике" и чем конструктивная математика отличается от бумаги. Глупость она и есть глупость!

[Sashamandra]

Цитата:

Объясните, как можно доказать теорему о неполноте без гёделевской нумерации.

Да, я считаю, что для доказательства теоремы Гёделя о неполноте нет необходимости в гёделевской нумерации. Достаточно любой подходящей нумерации. Вы считаете это глупостью?

Цитата:

Я вообще не понимаю, что значит "определить язык в конструктивной математике" и чем конструктивная математика отличается от бумаги.

Вы хотите об этом узнать?

[Xaositect]

Sashamandra в сообщении #295251 писал(а):

Да, я считаю, что для доказательства теоремы Гёделя о неполноте нет необходимости в гёделевской нумерации. Достаточно любой подходящей нумерации. Вы считаете это глупостью?

Вообще-то геделевская нумерация не фиксирована, это и есть "любая подходящая нумерация".

[Sashamandra]

Цитата:

Вообще-то геделевская нумерация не фиксирована, это и есть "любая подходящая нумерация".

Почему вы мне об этом говорите, а не Снэйпу? Это он, по-видимому, под гёделевской нумерацией понимает нумерацию, предложенную Гёделем.

Кто-нибудь что-нибудь подскажет насчет литературы относительно поставленной задачи?

[Xaositect]

Sashamandra в сообщении #295268 писал(а):

Почему вы мне об этом говорите, а не Снэйпу? Это он, по-видимому, под гёделевской нумерацией понимает нумерацию, предложенную Гёделем.

Потому что я уверен, что он об этом знает.

Давайте определимся, чего Вы хотите.
Я так понял, что Вы хотите:
Взять какую-то теорию, оперирующую с древовидными объектами, такими как формулы, выводы и т.п.
Закодировать эти деревья с помощью строк в алфавите из 2 букв каким-то естественным образом.
Записать алгоритмы над кодами, соответствующие логическим операциям, таким как подстановка вместо переменной, определение корректного вывода и др.
Так?

[Sashamandra]

Цитата:

Потому что я уверен, что он об этом знает.

Тогда объясните, в чем он увидел глупость? Если все выражения уже представлены двоичными числами, зачем ему нужна гёделевская нумерация?

Цитата:

Я так понял, что Вы хотите: Взять какую-то теорию, оперирующую с древовидными объектами, такими как формулы, выводы и т.п. Закодировать эти деревья с помощью строк в алфавите из 2 букв каким-то естественным образом. Записать алгоритмы над кодами, соответствующие логическим операциям, таким как подстановка вместо переменной, определение корректного вывода и др.
Так?

Абсолютно. А понятия "формула", "терм", "быть доказательством" и прочее должны быть определяемы соответствующими разрешающими алгоритмами. Также должны быть определены "система координат на дереве" для указания вхождения подформулы в данную формулу и операции подстановки подфорумл в указанных "местах".

Из общих соображений мне кажется, что это все уже где-то сделано. Но я не могу найти где.

[Xaositect]

Sashamandra в сообщении #295298 писал(а):

Из общих соображений мне кажется, что это все уже где-то сделано. Но я не могу найти где.

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

У всех, кто знаком с областью, есть некоторая интуиция насчет того, что алгоритмично, а что нет. Даже если что-то нигде не написано явно, никто не сомневается в конструктивности этих построений, а похожие алгоритмы даже используются на практике (pattern matching, например).

На мой взгляд, такая работа будет полезна как упражнение студенту 1-2 курса по формальным моделям вычислений и вряд ли представляет самостоятельный интерес.

[Sashamandra]

Цитата:

На мой взгляд, такая работа будет полезна как упражнение студенту 1-2 курса по формальным моделям вычислений и вряд ли представляет самостоятельный интерес.

Правильно ли я вас понял, что вы не знаете ни таких работ и ни таких студентов? Только про Мендельсона не надо. Книга ведь известная.

[Xaositect]

Sashamandra в сообщении #295306 писал(а):

Правильно ли я вас понял, что вы не знаете ни таких работ и ни таких студентов? Только про Мендельсона не надо. Книга ведь известная.

Работ не знаю. Машину Тьюринга для преобразования $\Phi\#t \mapsto \Phi[x/t]$ писал на первом курсе.
Про Мендельсона точно не помню, но помню, что там очень многое из того, что в других книгах прячут за фразой типа "существует алгоритм для этого преобразования, читатель может при желании описать его более строго", было расписано.

[Sashamandra]

Цитата:

Работ не знаю. Машину Тьюринга для преобразования $\Phi\#t \mapsto \Phi[x/t]$ писал на первом курсе.

Интересно. А формула $\Phi$ как была представлена? Какие алфавиты использовались для определения языка и машины Тьюринга? Скобки принадлежали алфавиту? А машина Тьюринга была традиционной?

[Xaositect]

Sashamandra в сообщении #295312 писал(а):

Интересно. А формула как была представлена? Какие алфавиты использовались для определения языка и машины Тьюринга? Скобки принадлежали алфавиту? А машина Тьюринга была традиционной?

Алфавит был $x,|,\&,\forall,(,),\#$, вспомогательные символы я ввел для замены скобок $<,>$ остальных связок не было для простоты. Переменные представлялись как $x||\dots|$. Машина Тьюринга была такой, как определялась на лекциях, одно из стандартных определений.
Основная проблема была в том, чтобы связанную $x$ переименовать.

[Sashamandra]

Как я понял, вы говорите об алфавите, на котором определена машина Тьютринга. А каков общий вид формулы и терма? Машина Тьюринга должна их тоже уметь читать.

[Xaositect]

Там были квантифицированные булевы формулы
$x$ - переменная
$V$ - переменная => $V|$ - переменная

$V$ - переменная => $(V)$ - формула
$F, G$ - формулы => $(F\& G)$ - формула
$F$ - формула, $V$ - переменная => $(\forall V F)$ - формула

$\Phi$ и $t$ были формулами (и назывались они единообразно, я просто уже плохо помню это дело). Требовалось подставить $t$ в $\Phi$ вместо переменной $x$. Проверки на правильность не было (за исключением той, что ломала алгоритм, например, несоответствия скобок).