Дерево Бема - Böhm tree

А Дерево Бема представляет собой (потенциально бесконечный) древовидный математический объект, который может использоваться для предоставления денотационная семантика («значение») для терминов лямбда-исчисление (и языки программирования в целом с использованием переводов в лямбда-исчисление). Он назван в честь Коррадо Бём.

Мотивация

Простой способ понять значение вычисления - это рассматривать его как механическую процедуру, состоящую из конечного числа шагов, которые по завершении дают результат. Однако эта интерпретация неадекватна для процедур, которые не завершаются после конечного числа шагов, но, тем не менее, имеют интуитивное значение. Рассмотрим, например, процедуру для вычисления десятичного разложения числа π; если реализован надлежащим образом, он может обеспечивать частичный вывод по мере "выполнения", и этот текущий вывод является естественным способом придать значение вычислению. Это контрастирует, скажем, с программой, которая бесконечно повторяет цикл без вывода результатов. Эти две процедуры имеют очень разные интуитивные значения.

Поскольку вычисление, описанное с помощью лямбда-исчисления, представляет собой процесс приведения лямбда-члена к его нормальной форме, эта нормальная форма сама по себе является результатом вычисления, и весь процесс можно рассматривать как «оценку» исходного члена. По этой причине Церкви исходное предложение заключалось в том, что значение вычисления (описываемого) лямбда-термином должно быть нормальной формой, к которой оно сводится, и что термины, не имеющие нормальной формы, бессмысленны.[1] Это как раз и страдает неадекватностью, описанной выше. Расширение π по аналогии, однако, если «попытка» привести термин к его нормальной форме даст «в пределе» бесконечно длинный лямбда-член (если такая вещь существует), этот объект можно считать этим результатом. Конечно, такого термина не существует в лямбда-исчислении, и поэтому здесь используются деревья Бема.

Неформальное определение

Бёмовское дерево - это (возможно, бесконечное) ориентированный ациклический граф с некоторыми вершинами, помеченными лямбда-членами вида λИкс1.λИкс2... λИксп.у (п может быть 0), где ровно одна вершина («корень») не имеет родителя, все остальные вершины имеют ровно одного родителя, каждая вершина имеет конечное число потомков, и каждая немеченная вершина не имеет потомков.

Для бёмовских деревьев будем иметь следующие понятия А, B:

  • λИкс.А является А с λИкс. добавлен к метке в ее корне
  • (λИкс А) B является А[Икс:=B] (Смотри ниже)
  • А B (где метка корневого узла А не имеет связующие ) - дерево, полученное из А добавляя B как новый крайний правый дочерний элемент корневого узла
  • На вершине с меткой λИкс1... λИксп.у, у свободна в этой вершине, если λу не появляется в метке этой вершины или любого из ее предков
  • Замена с избеганием захвата А[Икс:=B] является:
    1. (λИкс.А)[Икс:=B] есть λИкс.А
    2. (λу.А)[Икс:=B] (x и y разные) равно λz.А[у:=z][Икс:=B] куда z не в А и не бесплатно в B (может остаться у если у не бесплатно в B)
    3. Если корневой узел А имеет этикетку Икс и дети C1...Cп, А[Икс:=B] является ((B C1[Икс:=B]) C2[Икс:=B])...Cп[Икс:=B]
    4. Если корневой узел А не помечен Икс (может быть без метки), А[Икс:=B] является ((А C1[Икс:=B]) C2[Икс:=B])...Cп[Икс:=B]

Дерево Бема BT (M) лямбда-члена M затем можно "вычислить" следующим образом.[примечание 1]

  1. BT (Икс) - это единственный узел, помеченный Икс
  2. BT (λИкс.M) является λИкс.BT (M)
  3. BT (M N) есть BT (M) BT (N)

Отметим, что эта процедура подразумевает нахождение нормальной формы для M. Если M имеет нормальную форму, дерево Бема конечно и имеет простое соответствие нормальной форме. Если M не имеет нормальной формы, процедура может бесконечно «наращивать» некоторые поддеревья или может «застревать в цикле», пытаясь произвести результат для части дерева, которая является источником немаркированных конечных узлов. По этой причине процедуру следует понимать как применение всех шагов параллельно, с полученным деревом, заданным «в пределе» бесконечного применения процедуры.

Например, процедура вообще не выращивает деревья для BT (Ω ) или для BT (Ωя), что соответствует одному корневому узлу без метки.

Аналогичным образом процедура не завершается для BT (λИкс.ИксΩ), но дерево, тем не менее, отличается от предыдущих примеров.

Примечания

  1. ^ Представленное здесь представление избегает использования разрешимости или головных нормальных форм, но в остальном представляет собой представление "эффективного" дерева Бема.[2]

Рекомендации

  1. ^ Церковь, Алонсо (1941). Исчисления лямбда-преобразования. Принстон: Издательство Принстонского университета. п. 15. ISBN  0691083940.
  2. ^ Барендрегт, Хенк П. Лямбда-исчисление: его синтаксис и семантика. Лондон: публикации колледжа. С. 219–221, 486–487. ISBN  9781848900660.