Предложение метрики на лямбда-термах
Oct. 27th, 2010 01:10 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codedotНиже будут использованы обозначения, ранее введенные кратко, но доступен также комментарий к бессловесному определению. Мотивацией вводимого ниже метрического пространства послужил замечательный доклад Ю. И. Манина «Ренормализация и теория вычислимости» на общеинститутском математическом семинаре Санкт-Петербургского отделения Математического института им. В. А. Стеклова РАН.
Определим метрику ρ(Μ, Ν) на лямбда-термах Μ, Ν ∈ Λ (можно ограничиться и комбинаторами Λ⁰) следующим образом:
ρ(M, N) = {0, если M = N, иначе 1 + min{ρ(Fˡ(Μ), Ν), ρ(Μ, Fˡ(Ν))}.
Для термов, не являющихся βη-конвертируемыми, допустим значение ∞ в стиле нестандартного анализа, обозначая им ситуацию, когда вычисление расстояния не завершается вовсе.
Теперь покажем, что метрика корректна:
1) ρ(M, Μ) = 0 по определению;
2) симметричность тривиальна;
3) для случая термов, не являющихся βη-конвертируемыми, свойство треугольника очевидно [а для случая экстенсионально равных это интуитивно верное утверждение, но пока оставшееся без доказательства, напоминает свойство ромба у редукции, то есть свойство Черча-Россера].
Если разрешить проблему с экстенсиональностью в определении «n-равенства», то для некоторых термов, не равных экстенсионально, но при этом достаточно осмысленных, значение расстояния ∞, можно вычислять, обнаруживая первое несовпадение в префиксных кодах. Разумеется, в каждом подпространстве, состоящем из βη-конвертируемых термов, метрика всегда вычислима и конечна.
Определим метрику ρ(Μ, Ν) на лямбда-термах Μ, Ν ∈ Λ (можно ограничиться и комбинаторами Λ⁰) следующим образом:
ρ(M, N) = {0, если M = N, иначе 1 + min{ρ(Fˡ(Μ), Ν), ρ(Μ, Fˡ(Ν))}.
Для термов, не являющихся βη-конвертируемыми, допустим значение ∞ в стиле нестандартного анализа, обозначая им ситуацию, когда вычисление расстояния не завершается вовсе.
Теперь покажем, что метрика корректна:
1) ρ(M, Μ) = 0 по определению;
2) симметричность тривиальна;
3) для случая термов, не являющихся βη-конвертируемыми, свойство треугольника очевидно [а для случая экстенсионально равных это интуитивно верное утверждение, но пока оставшееся без доказательства, напоминает свойство ромба у редукции, то есть свойство Черча-Россера].
Если разрешить проблему с экстенсиональностью в определении «n-равенства», то для некоторых термов, не равных экстенсионально, но при этом достаточно осмысленных, значение расстояния ∞, можно вычислять, обнаруживая первое несовпадение в префиксных кодах. Разумеется, в каждом подпространстве, состоящем из βη-конвертируемых термов, метрика всегда вычислима и конечна.
