Я рекомендую вам прочитать Годель, Эшер, Бах =) Здесь обсуждается именно то, что вы здесь описываете.
В заключение, одно из предложенных решений состоит в том, чтобы найти инвариант для вашей системы: свойство, которое, если оно истинно в начале манипуляций, должно во всех случаях также будьте правдивыми в конце ваших манипуляций.
Если ваша первая строка обладает этим инвариантом, а ваша конечная строка - нет, то ваше правило подстановки никогда не сгенерирует вторую строку.
Ваше правило инварианта может быть более мощным ... например, оно может быть тогда и только тогда, когда отношение (инвариант истинен на конечном шаге, если и только если он истинен на первом шаг), так что вы можете доказать, что конечная строка недоступна, если есть инвариант, который не является истинным в первой строке. Обратите внимание, что это тогда и только тогда, когда отношения автоматически следуют из стандарта, если отношения, если все ваши правила работают в обоих направлениях (вы можете применять их в прямом и обратном направлении)
Например, вот возможный инвариант в вашей первой системе:
- Все смежные строки, не содержащие в себе непрерывную комбинацию строк «кошка» или «собака», также должны присутствовать в конечном состоянии
Учитывая это инвариантное правило, легко предоставить формулу принятия решения, чтобы решить, возможна ли строка с учетом начальной строки.
добавить
Надеюсь, вы не против, если я приму термины Хофштадтера, в которых:
- Заданная начальная строка будет называться «аксиомой»
- Аксиомы могут действовать в соответствии с набором правил
- Любая строка букв называется «теорема»; строка букв, которая может быть получена по правилам из данных аксиом, называется «действительной теоремой»
Итак, ваш вопрос переходит к "может ли X произвести Y?" на "Является ли Y верной теоремой, выводимой из X?"
Итак, давайте подойдем к вашей проблеме подстановки строк из более общих терминов. Мы будем называть A упорядоченным набором всех замещаемых строк, а A упорядоченным набором всех замещающих строк. Поэтому здесь у нас есть одно обобщенное правило:
"xA[n]y" => "xB[n]y"
Это говорит: «Если мы когда-нибудь увидим теорему со строкой в множестве A, окруженную строками x и y, то мы можем также вывести xB[n]y, где B[n] - это соответствующая замещающая строка.
Давайте найдем некоторые истинные инварианты независимо от того, что находится в наборах A и B.
- Вследствие того, что ваши замещающие строки всегда имеют ту же длину, что и их замещенная строка, любая буква в аксиоме, которая не найдена в
A, не должна двигаться
Например, если у нас есть аксиома abcdea и набор правил A=["cd",de"], легко увидеть, что буквы a и b не найдены в A. Поэтому можно сказать, что все теоремы в этой системе должны иметь вид ab##a. Это дает нам правило находить то, что не теорема.
Однако для очень длинных наборов A это может не сильно помочь нам, поскольку A может использовать все буквы.
Давайте попробуем сделать это более полезным ...
- Любая буква в конце аксиомы, которая не находится в конце строки в
A, не может двигаться. То же самое можно сказать о любой букве в начале аксиомы, которая не находится в начале строки в A.
Допустим, у нас есть A=["dog","cat","ton"], любое, если аксиома заканчивается любой буквой , которая не является g, t или c , всеми выводимыми теоремами , должны также заканчиваются на том же письме. Если аксиома начинается с любой буквы , а не с d, c или t , все выводимые теоремы должны также начинаться с той же буквы.
Это несколько более полезно, потому что для любого A с размером <26 у вас будут буквы, которые не заканчиваются или не начинаются.Однако для ваших аксиом становится гораздо менее вероятным начинать или заканчивать этими конкретными буквами. </p>
Однако мы обнаруживаем, что можем расширить это:
- Любая непрерывная строкабуквы в начале аксиомы, которые не являются непрерывной строкой в начале строки в
A, не должны двигаться;то же самое для непрерывной строки в конце аксиомы, которая не является непрерывной строкой в конце строки в A.
Мы обнаружим, что это намного полезнее!A должно быть не менее 26 ^ n элементов, чтобы мы могли отбросить этот инвариант как бесполезный.
Теперь, обратите внимание, мы тоже можем вернуться назад!То есть мы можем сказать:
- Любая непрерывная строка букв в начале теории, которая не является непрерывной строкой в начале строки в
B, также должна присутствовать во всех аксиомах.;то же самое для непрерывной строки в конце теоремы, которая не является непрерывной строкой в конце строки в B.
С этими правилами я собрал дерево решений для выяснения, какие случаи мы заблокировали, а какие не поддаются определению.Вы заметите, что у нас есть только два таких неопределимых случая.
Теперь осталось только найти инвариант этих двух случаев.Однако мы можем заметить одну вещь:
- Инвариантное правило к
CASE 2 может также применяться к CASE 1, при этом игнорируются начальные / конечные строки "not-in-A / B"
То есть, если у вас есть A=["cat","dog"],B=["dog","cut"] и аксиома-теорема boabcdut boablmut, то любые ваши инвариантные правила, которые вы можете применить к CASE 2, также могут быть применены кcdut => mlut, несоответствующая ведущая строка boab игнорируется.Это значительно упрощает ситуацию.
Итак, мы в основном разрешили оба неопределенных случая в одном;давайте посмотрим, что еще мы можем проанализировать ...
... в другой раз.Я вернусь к этому чуть позже.