codedot | Entries tagged with lambda calculus

Профессор Jan Willem Klop переслал набросок статьи Vincent van Oostrom, формально описывающей одношаговую рекурсивную стратегию для "Micro Lambda Calculus" с доказательством ее нормализующего свойства. Кроме уже упомянутых математиков, в списке "carbon copy" полученного недавно ответа стоял также адрес профессора Hendrik Pieter Barendregt:

( Текст письма )

После повторного отправления спустя месяц вопроса о корректности построения одношаговой стратегии для "Micro Lambda Calculus", профессор Jan Willem Klop ответил следующим образом:

( Ответ )

Возможно, Vincent van Oostrom окажет помощь в разрешении данного вопроса.

На вопрос о корректности построения одношаговой стратегии для "Micro Lambda Calculus" профессор Клоп, к сожалению, не ответил. В письме предлагалась стратегия, определяемая в виде библиотеки языка Python с использованием лишь цепочек if-elif-else и рекурсии.

Коротко стратегию можно определить следующим образом. Если тело функции в самом левом ("leftmost outermost") редексе имеет форму \a. \b. ... \z. M, где M - редекс, то выбирать для редукции следует редекс M. В противном случае, выбирать для редукции самый левый редекс.

Стратегия была построена похожей на многошаговую стратегию, описанную в статье "Axioms for the Theory of Lambda-Conversion" (Gyorgy Revesz). Полученный алгоритм был проанализирован очень поверхностно, причем рассмотривалась эквивалентность оригинальному алгоритму Gyorgy Revesz, так что вопросы о корректности построения и нормализующего свойства тогда не были разрешены. Был бы признателен за помощь в определении корректности построения одношаговой стратегии и доказательстве или опровержении еe нормализующего свойства.

На вопрос о существовании эквивалента бета-эта-редукции для комбинаторной логики профессор Барендрегт ответил ссылкой на рассмотрение сильной редукции в работах Curry, Hindley, Seldin. В статье "Axioms for Strong Reduction in Combinatory Logic" (Roger Hindley) приводится, по сути, доказательство невозможности существования сильной редукции для CL-теории, а точнее, доказывается, что набор правил сильной редукции всегда бесконечен. Такое свойство, следовательно, оказывается и у комбинаторной логики с одноточечным базисом.

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

Наивная попытка показать, что функция revesz(), определяемая ниже на языке Python, являющаяся рекурсивной одношаговой стратегией, является эквивалентной рекурсивной многошаговой стратегии Gyorgy Revesz, введенной в его статье "Axioms for the Theory of Lambda-Conversion", провалилась. Стратегия Gyorgy Revesz действительно должна использовать больше информации, чем само вычисляемое выражение. Об этом, впрочем, говорится в "J. Klop's Ustica notes", но, к сожалению, без доказательств.

После написания небольшой библиотеки функций на языке Python попытка вычислить выражение (1 - 1) в арифметике Черча привела к зацикливанию и переполнению стека из-за рекурсивной природы комбинатора PRED:

alexo@codedot:~/Projects/micro$ python
Python 2.5.2 (r252:60911, Mar 12 2008, 13:39:09) 
[GCC 4.2.3 (Ubuntu 4.2.3-2ubuntu4)] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from micro import *
>>> term = ('@', pred, one)
>>> normal(term)
[...]
RuntimeError: maximum recursion depth exceeded
>>>
alexo@codedot:~/Projects/micro$

( Определение стратегии )

Таким образом, пока вопрос о том, существует ли одношаговая стратегия для "Micro Lambda Calculus", остается открытым.

В переписке Барендрегт показал несколько страниц из "J. Klop's Ustica notes", где говорится о существовании многошаговых рекурсивных нормализующих стратегий для "Micro Lambda Calculus" - именно так называется на самом деле редукция из заметки "The Delayed Beta Reduction".

Одна из многошаговых стратегий для "Micro Lambda Calculus" определена в статье "Axioms for the Theory of Lambda-Conversion" (Gyorgy Revesz) - предложенная там стратегия является многошаговой потому, что для выбора редекса используется не только само вычисляемое выражение, но и информация о предыдущих шагах вычисления.

К сожалению, по словам Барендрегта, вопрос о том, существует ли одношаговая стратегия для "Micro Lambda Calculus", остается открытым. Возможно, стоит заняться этой темой и попытаться доказать возможность (например, конструктивно) или невозможность существования такой стратегии.

Также хотелось бы построить абстрактную машину, скомбинировав подход "Micro Lambda Calculus" с такими идеями, как однородная память-куча ("The Heap Lambda Machine"), нерекурсивный обход дерева лямбда-выражения ("Функциональное программирование" Филда и Харрисона), а также "Lazy Evaluation" и "Garbage Collection".

Запрос "Micro Lambda Calculus" в Google однозначно приводит к статье "A two-level approach to logic plus functional programming integration". После покупки PDF с данной статьей за $25 с помощью ресурса SpringerLink практически сразу нашлось упоминание тех же правил, что и в статье "The Delayed Beta Reduction". В свою очередь, статья "A two-level approach to logic plus functional programming integration" ссылается на "Axioms for the Theory of Lambda-Conversion", где и был впервые введен подход к вычислению лямбда-выражений, на который похожи полученные недавно четыре правила.

Меньше чем через двадцать минут после отправления вопроса по поводу "The Delayed Beta Reduction" профессору Барендрегту был получен от него ответ. Он указал на "Micro Lambda Calculus" и "Explicit Substitution" как на темы, где стоит искать похожий подход к вычислению лямбда-выражений.

Так как довольно продолжительный поиск в литературе упоминания четырех правил или похожего подхода к вычислению лямбда-выражений, а также вопрос в usenet-группе sci.math.research не привели к результатам, идея была оформлена в стиле "Theoretical Pearls" журнала "Journal of Functional Programming". Статья доступна по следующему адресу:

http://pygx.sourceforge.net/betad.pdf

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

Используемые обозначения:

1) <var> - переменная;
2) <var>: <expr> - абстракция;
3) (<expr> @ <expr>) - аппликация;
4) A = B - A и B сводятся к одному и тому же терму с помощью бета-редукции.

Известно классическое определение бета-редукции:

(x: M @ A) -> M[x := A], (*)

где подстановка определяется четырьмя правилами:

1) x[x := A] = A;
2) y[x := A] = y;
3) (y: M)[x := A] = y: M[x := A];
4) (M @ N)[x := A] = (M[x := A] @ N[x := A]).

Можно заметить, что

(x: x @ A) = A; (1)

(x: y @ A) = y; (2)

ввиду (*)

(x: y: M @ A) -> (y: M)[x := A] =
= y: M[x := A] <- y: (x: M @ A),

таким образом

(x: y: M @ A) = y: (x: M @ A); (3)

ввиду (*)

(x: (M @ N) @ A) -> (M @ N)[x := A] =
= (M[x := A] @ N[x := A]) <- ((x: M @ A) @ (x: N @ A)),

таким образом

(x: (M @ N) @ A) = ((x: M @ A) @ (x: N @ A)). (4)

Полученные выше правила (1), (2), (3) и (4) приводят вычислимые выражения к нормальной форме за большее число шагов, чем "мгновенная" подстановка. Но "мгновенная" подстановка предполагает обход дерева в случае представления выражений графами. "Замедленная" же редукция с помощью правил (1)-(4) дает на каждом шаге самостоятельное выражение, равное с точностью до бета-редукции предыдущему, но более близкое к нормальной форме. Такой набор правил мог бы упростить создание машины для автоматического упрощения лямбда-выражений, основанной на представлении выражений графами, "ленивых" вычислениях и "сборке мусора", дав возможность после каждого такта работы (при условии, что любое из правил занимает один такт) иметь в памяти самостоятельное лямбда-выражение.

Комбинаторная логика предлагает представление лямбда-выражений с помощью одной базисной функции (здесь и далее используется вариант записи, используемый в языке Python):

X = lambda f: f (lambda x: lambda y: lambda z: x (z) (y (z))) (lambda x: lambda y: lambda z: x)

С помощью этой функции можно ввести еще три:

K = X (X)
S = X (K)
I = S (K) (K)

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

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

Так, например, ноль определяется в лямбда-исчислении как функция (здесь и далее используется вариант записи, используемый в языке Python)

lambda x: lambda y: y,

а оператор увеличения на единицу вводится как функция

lambda n: lambda f: lambda x: f ((n (f)) (x)).

Нетрудно убедиться, что тогда 1 соответствует выражению

lambda x: lambda y: x (y),

2 соответствует

lambda x: lambda y: x (x (y)),

и так далее.

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