Предложение метрики на лямбда-термах

Ниже будут использованы обозначения, ранее введенные кратко, но доступен также комментарий к бессловесному определению. Мотивацией вводимого ниже метрического пространства послужил замечательный доклад Ю. И. Манина «Ренормализация и теория вычислимости» на общеинститутском математическом семинаре Санкт-Петербургского отделения Математического института им. В. А. Стеклова РАН.

Определим метрику ρ(Μ, Ν) на лямбда-термах Μ, Ν ∈ Λ (можно ограничиться и комбинаторами Λ⁰) следующим образом:

ρ(M, N) = {0, если M = N, иначе 1 + min{ρ(Fˡ(Μ), Ν), ρ(Μ, Fˡ(Ν))}.

Для термов, не являющихся βη-конвертируемыми, допустим значение ∞ в стиле нестандартного анализа, обозначая им ситуацию, когда вычисление расстояния не завершается вовсе.

Теперь покажем, что метрика корректна:

1) ρ(M, Μ) = 0 по определению;
2) симметричность тривиальна;
3) для случая термов, не являющихся βη-конвертируемыми, свойство треугольника очевидно [а для случая экстенсионально равных это интуитивно верное утверждение, но пока оставшееся без доказательства, напоминает свойство ромба у редукции, то есть свойство Черча-Россера].

Если разрешить проблему с экстенсиональностью в определении «n-равенства», то для некоторых термов, не равных экстенсионально, но при этом достаточно осмысленных, значение расстояния ∞, можно вычислять, обнаруживая первое несовпадение в префиксных кодах. Разумеется, в каждом подпространстве, состоящем из βη-конвертируемых термов, метрика всегда вычислима и конечна.

Счетность в конструктивизме

Исходные объекты для построения теорий всегда выбраны из счетного множества: например, из имен; имена счетны ввиду счетности языка как множества текстов. Далее, при попытке ввести множество всех подмножеств такого или некоторого производного счетного множества возникает проблема континуума. Однако, конструктивно доказать, что континуальные множества вообще существуют, не представляется возможным.

Проблема с континуальными множествами довольно остро проявилась в прошлом веке при развитии теории вычислимости, где требовалась математическая модель для счетных множеств, которые бы состояли из отображений внутри него. Разрешилась она тогда, когда Скотт предложил топологию дерева и урезал отображения до непрерывных. С другой стороны, привести конструктивный пример функции, которая вне такого множества, невозможно, так как язык описывает в точности частично-рекурсивные функции.

Возникает логичный вопрос о том, как же быть с вещественными числами, и до какого множества следует их урезать, чтобы описать именно те, которые можно определить конструктивно. Такие числа есть в конструктивном вещественном анализе, и называются рекурсивными вещественными числами [вольный перевод с англ.].

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

Наконец, учитывая, что система λβη соответствует максимальным непротиворечивым теориям и при этом в виду тезиза Черча–Тьюринга имеет максимальную выразительность, любые мыслимые конструкции оказываются возможными для определения внутри нее. И это может, в свою очередь, служить дополнительным аргументом в сторону ее использования и большей концентрации внимания на эквивалентных системах и на теории вычислимости вообще.

Хакерская самозащита

zhengxi @ 2010-10-27 13:28:00:

odmin> нахера ты там стока файлов создал? твой акк уже 5 часов удаляется (
user> зато акк до сих пор работает
user> хакеру на заметку - как сделать, чтобы быстро не снесли акк
user> а если постоянно файлы создавать - то его вообще не снесут
user> они создаются достаточно быстро
user> не 5 часов