edit 2 : Намек на то, что с индексами де Брейна легче работать, я переформулировал большую часть внутреннего представления формул, чтобы использовать смешанное представление де Брейна аля Бумага Коннора Макбрайда.Это значительно упростило некоторые алгоритмы, касающиеся синтаксиса, которые должны были иметь дело с α-эквивалентностью, но сделало другие более сложными.В любом случае это означает, что свободные переменные можно стандартизировать отдельно, а связанные переменные имеют канонические имена, представленные расстоянием их привязки.Это не совсем удовлетворительно, но это, по крайней мере, лучшее начало.
edit 1 : Я понял, что проблемных ограничений недостаточно, чтобы гарантировать стандартизацию переменных,В частности, итерация квантификаторов означает, что переменные в связующих должны быть сначала стандартизированы друг от друга.Так что, вероятно, нет выхода из решения, которое требует нескольких проходов по каждому абстрактному синтаксическому дереву.Предложение использовать индексы де Брейна в целом является довольно хорошим решением, но оно не даст легкой стандартизации без нарушения обозначений и их полезности.
original: Let V - бесконечный набор переменных, проиндексированных натуральными числами, fv (φ) обозначают свободные переменные φ, а bv (φ) обозначают связанные переменные φ, длялюбая формула первого порядка φ.Проблема, которую я пытаюсь решить, заключается в следующем.
Пусть φ и ψ - формулы первого порядка.Найдите замены θ 1 и θ 2 такие, что: (a) fv (θ 1 (φ)), fv (θ 2 (φ)), bv (θ 1 (φ)) и bv (θ * 1044)* 2 (ψ)) не пересекаются;(б) объединение фв (θ 1 (φ)), фв (θ 2 (φ)), bv (θ 1 (φ)) и bv (θ 2 (ψ)) изоморфны начальному сегменту натуральных чисел;и (в) все переменные в bv (θ 1 (φ)) меньше всех переменных в bv (θ 2 (ψ)) меньше всех переменных в fv (θ 1 (ψ)) меньше всех переменных в fv (θ 2 (ψ)).
Сложность состоит в том, что набор связанных и свободных переменных в формуле не обязательно является непересекающимся, и кванторы могут повторяться, что означает, что наивная замена приводит к случайному захвату переменных,и пр.
Неэффективным решением является следующее.Для заданных φ и ψ сначала стандартизируют отдельные свободные переменные φ и ψ так, чтобы все свободные переменные в стандартизированных терминах были больше, чем наибольшая связанная переменная плюс число операторов связывания в φ и ψ, давая φ 'и ψ'.Затем переименуйте связанные переменные φ ', начиная с x 0 .Тогда связанные переменные ψ '.Тогда свободные переменные ф '.Тогда свободные переменные ψ '.
То, что я хотел бы, - это более эффективный метод удовлетворения проблемных ограничений.То есть решение, которое не требует начальной стандартизации, которая переименовывает свободные переменные.Эффективная стандартизация переменных не является проблемой.Однако дополнительное ограничение доставляет мне неприятности.