Уважаемые профессионалы, помогите разобраться.
Решил было вникнуть в лямбда-исчисление, да помешала собственная непроходимая тупость. Почитал википедию (http://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5) — что-то понял, но очень уж приблизительно. Затем — учебник Душкина по Хаскелю ("Функциональное программирование на языке Haskell") — мне понравилось, но из-за, как мне кажется, нестрогости изложения, ясности не добавилось, вместо этого немного расширился горизонт эрудиции. Если кратко, то применить полученные таким образом знания не получается. Далее, начал читать Харрисона "Введение в функциональное программирование" (http://funprog-ru.googlecode.com/files/intro2fp-20090518.pdf), но после первой и второй главы понял, что вновь потерял нить. Причиной всему — абсолютное непонимание основополагающих понятий "аппликация" и "лямбда-абстракция", а также их взаимоотношений. Поэтому снова пришлось попытаться копнуть глубже. На этот раз из Барендрегта "Ламбда-исчисление. Его синтаксис и семантика". И тут началось самое интересное. Непонимание стало просто махровым. Вначале — цитаты. (1) "Ламбда-исчисление — это бестиповая теория, рассматривающая функции как правила, а не как графики. Понятие функции как закона или правила кажется старомодным и подразумевает переход от аргумента к значению, процесс, закодированный неким определением. Приписываемая обычно Дирихле мысль о том, что функции можно рассматривать как графики, т.е. множества, состоящие из пар аргумент-значение, была важным вкладом в математику. Тем не менее ламбда-исчисление снова рассматривает функции как правила, чтобы подчеркнуть их вычислительные аспекты." (2) "Формальное (бестиповое) ламбда-исчисление — теория, обозначаемая через L,- изучает функции и их аппликативное поведение. Поэтому аппликация (применение функции к аргументу) — исходная операция системы L. Функция f в применении к аргументу a обозначается через fa. Операция, дополнительная к аппликации, называется абстракцией. Пусть t (тождественно равно t(x)) — выражение, содержащее, может быть, переменную x. Тогда Lx.t(x) — это такая функция f, которая сопоставляет аргументу a значение t(a). Иными словами, имеет место
(Lx.t(x))a = t(a)"
И вот теперь я воспроизвожу свои рассуждения.
Из (2) получается, с одной стороны, что под функцией f понимается правило сопоставления аргументу a значения f(a) (т.е. fa).
С другой стороны, пусть есть выражение t, содержащее, возможно, x. (Попутно вопрос: что такое "выражение"? это то же самое что функция? или, может быть, это такой оборот речи?) Так вот, из той же цитаты (2) следует, что функция f, понимаемая как некое правило, ставит некоему аргументу a в соответствие t(a). Эта f и называется абстракцией и обозначается через Lx.t(x). И вопрос такой: это ведь то же самое, что и раньше, т.е. что (Lx.t(x))(a) — это то же самое, что и f(a). То есть аппликация и абстракция — это одно и то же.
Прошу объяснить ошибку.
Здравствуйте, ShcheknItrch, Вы писали:
SI>(1) "Ламбда-исчисление — это бестиповая теория, рассматривающая функции как правила, а не как графики. Понятие функции как закона или правила кажется старомодным и подразумевает переход от аргумента к значению, процесс, закодированный неким определением. Приписываемая обычно Дирихле мысль о том, что функции можно рассматривать как графики, т.е. множества, состоящие из пар аргумент-значение, была важным вкладом в математику. Тем не менее ламбда-исчисление снова рассматривает функции как правила, чтобы подчеркнуть их вычислительные аспекты." SI>(2) "Формальное (бестиповое) ламбда-исчисление — теория, обозначаемая через L,- изучает функции и их аппликативное поведение. Поэтому аппликация (применение функции к аргументу) — исходная операция системы L. Функция f в применении к аргументу a обозначается через fa. Операция, дополнительная к аппликации, называется абстракцией. Пусть t (тождественно равно t(x)) — выражение, содержащее, может быть, переменную x. Тогда Lx.t(x) — это такая функция f, которая сопоставляет аргументу a значение t(a). Иными словами, имеет место SI> (Lx.t(x))a = t(a)"
SI>И вот теперь я воспроизвожу свои рассуждения. SI>Из (2) получается, с одной стороны, что под функцией f понимается правило сопоставления аргументу a значения f(a) (т.е. fa). SI>С другой стороны, пусть есть выражение t, содержащее, возможно, x. (Попутно вопрос: что такое "выражение"? это то же самое что функция? или, может быть, это такой оборот речи?)
Выражение -- синтаксически правильный набор термов. Какие термы допустимы, какой у нас синтаксис -- зависит от реализации. Например, могут быть допустимы числа, арифметические значки, ещё что-нибудь (определённые ранее имена и т.п.).
SI>Так вот, из той же цитаты (2) следует, что функция f, понимаемая как некое правило, ставит некоему аргументу a в соответствие t(a). Эта f и называется абстракцией и обозначается через Lx.t(x). И вопрос такой: это ведь то же самое, что и раньше, т.е. что (Lx.t(x))(a) — это то же самое, что и f(a). То есть аппликация и абстракция — это одно и то же. SI>Прошу объяснить ошибку.
Формально, аппликация это операция с двумя аргументами: функция и аргумент. Она применяет одно к другому так или иначе (тут нужна какая-то формальная система "применения" функций, например просто подстановка). По нормальному это вычисление функции.
Абстракция это не операция с какими-либо аргументами. Это возможность создать функцию. Которую потом можно будет "апплицировать".
Здравствуйте, ShcheknItrch, Вы писали:
SI>То есть аппликация и абстракция — это одно и то же.[/b] SI>Прошу объяснить ошибку.
Может, примеры немного помогут.
2 + x — выражение. x ↦ 2 + x — функция, полученная абстракцией (вместо λ я использовал стрелку-с-палочкой, другое широко используемое обозначение)
(x ↦ 2 + x) 3 — применение (аппликация) функции к аргументу (аргумент в скобки принято не заключать, как, например, для синусов и логарифмов)
SH>Формально, аппликация это операция с двумя аргументами: функция и аргумент. Она применяет одно к другому так или иначе (тут нужна какая-то формальная система "применения" функций, например просто подстановка). По нормальному это вычисление функции.
SH>Абстракция это не операция с какими-либо аргументами. Это возможность создать функцию. Которую потом можно будет "апплицировать".
Можно насчет абстракции подробнее? Лучше даже с примером. Пусть, скажем, есть ф-ия f(x) = 5*x*x + x*x*x. Аппликация в этом случае f к a=2 будет f(a) = 5*2*2 + 2*2*2 = 20+8 = 28.
Что в этом случае будет абстракцией?
Но ты не можешь дать имя этому процессу (тому общему, что есть в этих разных выражениях) и использовать этот процесс, подставляя в него аргументы. Возможность говорить о функциях, аргументах и т.п., возможность выражать их в синтаксисе -- это и есть абстракция.
Здравствуйте, ShcheknItrch, Вы писали:
SI>И вот теперь я воспроизвожу свои рассуждения. SI>Из (2) получается, с одной стороны, что под функцией f понимается правило сопоставления аргументу a значения f(a) (т.е. fa).
Это запись на мета-языке. Функция (точнее, комбинатор) -- это замкнутый терм, например \f . \a . f a. (Обратной косой чертой будем обозначать символ лямбды)
SI>С другой стороны, пусть есть выражение t, содержащее, возможно, x. (Попутно вопрос: что такое "выражение"? это то же самое что функция? или, может быть, это такой оборот речи?)
Выражение (или терм) — это мешанина из аппликаций и абстракций.
Изначально у нас есть куча переменных: x, y, z, ...
Дальше пробуем делать аппликации
x (y z)
x z (y z)
Получили незамкнутые термы.
Теперь можем делать абстракции, связывая переменные
Свяжем z
\z . x (y z)
\z . x z (y z)
потом y
\y . \z. x (y z)
\y . \z . x z (y z)
потом x
\x . \y . \z. x (y z)
\x . \y . \z . x z (y z)
Вышли замкнутые термы (это уже комбинаторы, то есть функции). Дальше можем применять термы друг к другу (связанные переменные можно свободно переименовывать), выполняя бета-редукцию по правилу (\x . M) N ~> M[x:=N]
(\x . \y . \z. x (y z)) (\x' . \y' . \z' . x' z' (y' z')) ~>
\y . \z. (\x' . \y' . \z' . x' z' (y' z')) y z ~>
\y . \z. (\y' . \z' . y z' (y' z')) z ~>
\y . \z. (\z' . y z' (z z'))
до тех пор, пока это возможно (до нормальной формы). Это всё и называется лямбда-исчисление.
Здравствуйте, SergH, Вы писали:
SH>Здравствуйте, ShcheknItrch, Вы писали:
SI>>Можно насчет абстракции подробнее? Лучше даже с примером. Пусть, скажем, есть ф-ия ...
SH>Нету! SH>Без абстракции нету функции. SH>Без абстракции ты можешь вычислять конкретные выражения типа
SH>5*1*1 + 1*1*1 = 5+1 = 6. SH>5*2*2 + 2*2*2 = 20+8 = 28. SH>...
SH>Но ты не можешь дать имя этому процессу (тому общему, что есть в этих разных выражениях) и использовать этот процесс, подставляя в него аргументы. Возможность говорить о функциях, аргументах и т.п., возможность выражать их в синтаксисе -- это и есть абстракция.
Т.е. я прошу подтвердить, что я правильно понял.
Пусть есть некое выражение t=t(x) (пусть для примера t(x)=5*x*x + x*x*x)
Лямбда-абстракция — это некий вычислитель, способный для каждого конкретного x=a вычислить t(a) (т.е. выполнить аппликацию t к a), тем самым поставив в соответствие некоему a значение t(a). Таким образом, поставив всем допустимым конкретным x-ам значения t(x), лямбда-абстракция создаст то, что называется функцией по Дирихле.
Так?
Здравствуйте, ShcheknItrch, Вы писали:
SH>>Но ты не можешь дать имя этому процессу (тому общему, что есть в этих разных выражениях) и использовать этот процесс, подставляя в него аргументы. Возможность говорить о функциях, аргументах и т.п., возможность выражать их в синтаксисе -- это и есть абстракция.
SI>Т.е. я прошу подтвердить, что я правильно понял. SI>Пусть есть некое выражение t=t(x) (пусть для примера t(x)=5*x*x + x*x*x) SI>Лямбда-абстракция — это некий вычислитель, способный для каждого конкретного x=a вычислить t(a) (т.е. выполнить аппликацию t к a), тем самым поставив в соответствие некоему a значение t(a). Таким образом, поставив всем допустимым конкретным x-ам значения t(x), лямбда-абстракция создаст то, что называется функцией по Дирихле. SI>Так?
Нет. Лямбда-абстракция сама и есть описание вычислительного процесса (\x . 5*x*x + x*x*x) без приписывания ему имени t. (в этом примере у нас не чистая лямбда, поскольку имеются дополнительные константы 5,* и +, которые требуют специальной интерпретации в рамках расширенного исчисления)
Здравствуйте, ShcheknItrch, Вы писали:
SI>Пусть есть некое выражение t=t(x) (пусть для примера t(x)=5*x*x + x*x*x) SI>Лямбда-абстракция — это некий вычислитель, способный для каждого конкретного x=a вычислить t(a) (т.е. выполнить аппликацию t к a), тем самым поставив в соответствие некоему a значение t(a).
Мне кажется, что считая так, ты не согрешишь против истины.
Но в этой области deniok меня умнее.
SI>Таким образом, поставив всем допустимым конкретным x-ам значения t(x), лямбда-абстракция создаст то, что называется функцией по Дирихле.
Про Дирихле в данном контексте слышу первый раз. Но, насколько я понял из твоих цитат, вычислитель это и есть "функция по Дирихле", т.е. некое овеществлённое "правило".
Есть другое определение понятия функция. Оно примерно так звучит:
F: A --> B это подмножество прямого произведения A*B, такое, что для любого a из A существует и одна и только одна пара (x,y) в F, такая, что x=a.
Тут ничего о правилах и способах вычисления не говорится.
Здравствуйте, SergH, Вы писали:
SH>Про Дирихле в данном контексте слышу первый раз. Но, насколько я понял из твоих цитат, вычислитель это и есть "функция по Дирихле", т.е. некое овеществлённое "правило".
Здравствуйте, deniok, Вы писали:
D>Нет. Лямбда-абстракция сама и есть описание вычислительного процесса (\x . 5*x*x + x*x*x) без приписывания ему имени t. (в этом примере у нас не чистая лямбда, поскольку имеются дополнительные константы 5,* и +, которые требуют специальной интерпретации в рамках расширенного исчисления)
Мнения разделились
Но, гм, если без имени (без которого ужасно неудобно, но которое с точки зрения математики не обязательно) -- то всё верно? Абстракция -- возможность как-то выделить процесс вычисления и что-то потом с ним делать?
Здравствуйте, Qbit86, Вы писали:
Q>Здравствуйте, ShcheknItrch, Вы писали:
SI>>Пусть есть некое выражение t=t(x)
Q>«t=t(x)» — это что-то, похожее на фрагмент лекции недалёких преподов по матанализу
Нужно было поставить тождественное равенство, но у меня на клавиатуре нет сразу трех горизонтальных черточек, пришлось ограничиться двумя. Я посчитал, что здесь не будет вопросов, поскольку об этом было в самом первом моем посте — (цитата) Пусть t (тождественно равно t(x)) — выражение, содержащее, может быть, переменную x.
Q>Ок, попробую издалека: что тебе напоминает эта последовательность символов: «ax² + bx + c»?
Ну, например, квадратное уравнение. Или частичную сумму.А что должно напоминать?
Здравствуйте, ShcheknItrch, Вы писали:
Q>>Ок, попробую издалека: что тебе напоминает эта последовательность символов: «ax² + bx + c»? SI>Ну, например, квадратное уравнение. Или частичную сумму.А что должно напоминать?
С чего вдруг? А по-моему это похоже на линейную относительно b функцию. В чём причина недопонимания? (А может, это вовсе функция от пары переменных c и x?)
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, ShcheknItrch, Вы писали:
SH>>>Но ты не можешь дать имя этому процессу (тому общему, что есть в этих разных выражениях) и использовать этот процесс, подставляя в него аргументы. Возможность говорить о функциях, аргументах и т.п., возможность выражать их в синтаксисе -- это и есть абстракция.
SI>>Т.е. я прошу подтвердить, что я правильно понял. SI>>Пусть есть некое выражение t=t(x) (пусть для примера t(x)=5*x*x + x*x*x) SI>>Лямбда-абстракция — это некий вычислитель, способный для каждого конкретного x=a вычислить t(a) (т.е. выполнить аппликацию t к a), тем самым поставив в соответствие некоему a значение t(a). Таким образом, поставив всем допустимым конкретным x-ам значения t(x), лямбда-абстракция создаст то, что называется функцией по Дирихле. SI>>Так? D>Нет. Лямбда-абстракция сама и есть описание вычислительного процесса (\x . 5*x*x + x*x*x) без приписывания ему имени t. (в этом примере у нас не чистая лямбда, поскольку имеются дополнительные константы 5,* и +, которые требуют специальной интерпретации в рамках расширенного исчисления)
Я опять теряю почву под ногами, пытаясь понять, есть ли отличия между описанием вычислительного процесса и самим вычислителем. И, если есть, то существенны ли они. Но я прошу не пинать меня пока что. Лучше было бы, наверное, действительно избавиться от 5, * и +, но давайте оставим, мне так будет проще.
Рискну предположить еще раз.
Есть некое выражение t(x) (=5*x*x + x*x*x)
Далее, у нас есть правило, каким образом вычислять t(x) для каждого конкретного x=a. Это правило и есть лямбда-абстракцией.
Так?
Если да, что такое тогда аппликация?
Здравствуйте, Qbit86, Вы писали:
Q>Здравствуйте, ShcheknItrch, Вы писали:
Q>>>Ок, попробую издалека: что тебе напоминает эта последовательность символов: «ax² + bx + c»? SI>>Ну, например, квадратное уравнение. Или частичную сумму.А что должно напоминать?
Q>С чего вдруг? А по-моему это похоже на линейную относительно b функцию. В чём причина недопонимания? (А может, это вовсе функция от пары переменных c и x?)
Я привел два варианта, а мог бы привести сто два. К сожалению, Ваши варианты не попали в список.
Здравствуйте, ShcheknItrch, Вы писали: SI>Рискну предположить еще раз. SI>Есть некое выражение t(x) (=5*x*x + x*x*x)
Ок
SI>Далее, у нас есть правило, каким образом вычислять t(x) для каждого конкретного x=a. Это правило и есть лямбда-абстракцией.
Да, и записывается абстракция так:
λx.5*x*x + x*x*x
SI>Если да, что такое тогда аппликация?
Запрос на подстановку конкретного выражения в лямбду вместо икса (не сама подстановка, сама подстановка произойдет в результате редукции):
(λx.5*x*x + x*x*x)1
Здравствуйте, ShcheknItrch, Вы писали:
Q>>>>Ок, попробую издалека: что тебе напоминает эта последовательность символов: «ax² + bx + c»? SI>>>Ну, например, квадратное уравнение. Или частичную сумму.А что должно напоминать?
Q>>С чего вдруг? А по-моему это похоже на линейную относительно b функцию. В чём причина недопонимания? (А может, это вовсе функция от пары переменных c и x?)
SI>Я привел два варианта, а мог бы привести сто два. К сожалению, Ваши варианты не попали в список.
Дело в том, что все эти варианты, строго говоря, неверны. Выражение «ax² + bx + c» — это просто месиво букв. Параболой оно может стать, когда мы применим к выражению абстракцию по x: «x ↦ ax² + bx + c» или, если угодно, «λx.ax² + bx + c». (Окончательно станет параболой, когда мы замкнём оставшиеся три свободные переменные.) Прямой линией оно может стать, когда мы применим абстракцию по b: «λb.ax² + bx + c». Иными словами, прежде чем выражение станет функцией, необходимо произвести абстракцию по свободным переменным. (Впрочем, «свободность» необязательна, так, например, из выражения «2» можно получить функцию «λx.2».)
SI>Рискну предположить еще раз. SI>Есть некое выражение t(x) (=5*x*x + x*x*x) SI>Далее, у нас есть правило, каким образом вычислять t(x) для каждого конкретного x=a. Это правило и есть лямбда-абстракцией. SI>Так? SI>Если да, что такое тогда аппликация?
Аппликация тогда тогда, видимо, будет применение правила вычисления для конкретного x=a.
Т.е., еще раз.
1. Есть выражение t(x) (=5*x*x + x*x*x)
2. Есть правило, каким образом вычислять t(x) для каждого конкретного x=a. Это правило и есть лямбда-абстракцией.
3. Аппликация — это применение правила вычисления для конкретного x=a.
Но тогда вопрос — что понимается под выражением t(x) (=5*x*x + x*x*x) еще до определения правила его использования?
Здравствуйте, ShcheknItrch, Вы писали:
SI>>Рискну предположить еще раз. SI>>Есть некое выражение t(x) (=5*x*x + x*x*x) SI>>Далее, у нас есть правило, каким образом вычислять t(x) для каждого конкретного x=a. Это правило и есть лямбда-абстракцией. SI>>Так? SI>>Если да, что такое тогда аппликация?
SI>Аппликация тогда тогда, видимо, будет применение правила вычисления для конкретного x=a.
SI>Т.е., еще раз. SI>1. Есть выражение t(x) (=5*x*x + x*x*x) SI>2. Есть правило, каким образом вычислять t(x) для каждого конкретного x=a. Это правило и есть лямбда-абстракцией.
тут не так. слово "вычислять" в этой науке нет. Мне кажутся неправильными попытки разобраться в лямбда-исчислении, начиная с грязного исчисления, расширенного сложением, умножением, символом 5.
SI>3. Аппликация — это применение правила вычисления для конкретного x=a.
Аппликация — это два лямбда-терма подряд — один из двух разрешенных способов построения термов.
SI>Но тогда вопрос — что понимается под выражением t(x) (=5*x*x + x*x*x) еще до определения правила его использования?
Ничего. Это набор констант (5, * и +) для которых подразумеваются традиционные правила редукции, лежащие вне лямбда-исчисления. Можно это записать в чистой лямбде
0 = λf x. x
SUC = λn f x. n f (f x)
PLUS = λ m n f x. m f (n f x)
MULT = λ m n f x. m (n f) x
FIVE = (SUC (SUC (SUC (SUC (SUC 0)))))
T = PLUS (MULT (MULT FIVE x) x) (MULT (MULT x x) x)
Здесь комбинаторы, набранные большими буквами, играют роль чисто синтаксических "сокращателей" записи. От них легко можно избавится прямой подстановкой. Терм T содержит одну свободную переменную (x) по которой мы его можем абстрагировать:
λx. T
получив замкнутый комбинатор. Применив его, скажем, к двойке
