Большое спасибо всем, кое-что прояснилось, но не все, поэтому, пожалуйста, не бросайте на произвол судьбы.
По совету deniok'а я больше не буду кивать на "грязное" исчисление.
Раньше я не мог понять, что такое лямбда-абстракция, а теперь вижу, что больше всего непонятна аппликация. Это, по определению, применение функции к аргументу. Ну вот объясните, что тогда понимается под функцией, есть ли такое понятие, как область определения, на которой задан аргумент, и во что отображает эта функция.
Вот смотрите, я беру определение лямбда-термов из Барендрегта.
"
2.1.1. Определение. (i) Ламбда-термы будут словами в следующем алфавите:
v0, v1, ... переменные
λ абстрактор
( , ) скобки.
(iii) Множество Λ ламбда-термов (или, что то же, λ-термов) индуктивно определяется следующим образом:
(1) x Є Λ;
(2) M Є Λ -> (λxM) Є Λ;
(3) M, N Є Λ -> (MN) Є Λ,
где x в (1) и (2) — произвольная переменная.
"
Ведь если у нас изначально есть только одни лишь лямба-термы, то мы можем только лишь их комбинировать, а вот под применением функции к аргументу можно понимать только лишь применение одного лямбда-терма к другому. Тут под применением нужно понимать простое комбинирование.
Но что меня смущает — так это то, что в определение лямбда-термов входит лямбда-абстрактор, который понимается как (см. первый пост):
"Формальное (бестиповое) ламбда-исчисление — теория, обозначаемая через λ,- изучает функции и их аппликативное поведение. Поэтому аппликация (применение функции к аргументу) — исходная операция системы λ. Функция f в применении к аргументу a обозначается через fa. Операция, дополнительная к аппликации, называется абстракцией. Пусть t (тождественно равно t(x)) — выражение, содержащее, может быть, переменную x. Тогда λx.t(x) — это такая функция f, которая сопоставляет аргументу a значение t(a). Иными словами, имеет место
(λx.t(x))a = t(a)"
Т.е. выходит так, что сначала дается определение лямбда-абстракции с использованием понятия аппликации, т.е. привлекая понятие функции (определения которого еще не было дано). Далее дается определения лямбда-термам и процессу их индуктивного построения. Ну и пока все. Я как-то не вижу совершенства в таком подходе.
Не уверен, что четко изложил суть непонимания.
Надеюсь, вы сможете прокомментировать.
Заодно еще один вопрос о (3) M, N Є Λ -> (MN) Є Λ
Правильно ли понимать MN просто как упорядоченный набор лямбда-термов M и N. И правильно ли это называть применением M к N?
Здравствуйте, ShcheknItrch, Вы писали:
SI>Большое спасибо всем, кое-что прояснилось, но не все, поэтому, пожалуйста, не бросайте на произвол судьбы. SI>По совету deniok'а я больше не буду кивать на "грязное" исчисление.
SI>Раньше я не мог понять, что такое лямбда-абстракция, а теперь вижу, что больше всего непонятна аппликация. Это, по определению, применение функции к аргументу. Ну вот объясните, что тогда понимается под функцией, есть ли такое понятие, как область определения, на которой задан аргумент, и во что отображает эта функция.
В бестиповом исчислении ни области определения ни множества значений нет. Что угодно может применяться к чему угодно. А функция — это синоним для терма; для этой теории это необязательный термин.
SI>Ведь если у нас изначально есть только одни лишь лямба-термы, то мы можем только лишь их комбинировать, а вот под применением функции к аргументу можно понимать только лишь применение одного лямбда-терма к другому. Тут под применением нужно понимать простое комбинирование.
Пока мы строим терм, это действительно так. Но лямбда-исчисление — это не только построение. Это ещё и правило бета-редукции. Построенные термы пошагово преобразуются по этому правилу, реализуя модель вычислений.
SI>Т.е. выходит так, что сначала дается определение лямбда-абстракции с использованием понятия аппликации, т.е. привлекая понятие функции (определения которого еще не было дано). Далее дается определения лямбда-термам и процессу их индуктивного построения. Ну и пока все.
В определении абстракции нет использования аппликации. Терм это либо переменная, либо абстракция над термом, либо аппликация (применение) терма к терму.
SI>Я как-то не вижу совершенства в таком подходе.
Получившееся исчисление равномощно машине Тьюринга. А так, да, в мире нет совершенства.
SI>Не уверен, что четко изложил суть непонимания. SI>Надеюсь, вы сможете прокомментировать.
SI>Заодно еще один вопрос о (3) M, N Є Λ -> (MN) Є Λ SI>Правильно ли понимать MN просто как упорядоченный набор лямбда-термов M и N. И правильно ли это называть применением M к N?
SI>>Раньше я не мог понять, что такое лямбда-абстракция, а теперь вижу, что больше всего непонятна аппликация. Это, по определению, применение функции к аргументу. Ну вот объясните, что тогда понимается под функцией, есть ли такое понятие, как область определения, на которой задан аргумент, и во что отображает эта функция.
D>В бестиповом исчислении ни области определения ни множества значений нет. Что угодно может применяться к чему угодно. А функция — это синоним для терма; для этой теории это необязательный термин.
Об этом чуть ниже.
SI>>Ведь если у нас изначально есть только одни лишь лямба-термы, то мы можем только лишь их комбинировать, а вот под применением функции к аргументу можно понимать только лишь применение одного лямбда-терма к другому. Тут под применением нужно понимать простое комбинирование.
D>Пока мы строим терм, это действительно так. Но лямбда-исчисление — это не только построение. Это ещё и правило бета-редукции. Построенные термы пошагово преобразуются по этому правилу, реализуя модель вычислений.
У Барендрегта определение бета-редукции дается страницей позже, поэтому я его и не хотел пока касаться.
SI>>Т.е. выходит так, что сначала дается определение лямбда-абстракции с использованием понятия аппликации, т.е. привлекая понятие функции (определения которого еще не было дано). Далее дается определения лямбда-термам и процессу их индуктивного построения. Ну и пока все.
D>В определении абстракции нет использования аппликации. Терм это либо переменная, либо абстракция над термом, либо аппликация (применение) терма к терму.
Ну как же нету? Вот ведь:
"Формальное (бестиповое) ламбда-исчисление — теория, обозначаемая через λ,- изучает функции и их аппликативное поведение. Поэтому аппликация (применение функции к аргументу) — исходная операция системы λ. Функция f в применении к аргументу a обозначается через fa. Операция, дополнительная к аппликации, называется абстракцией. Пусть t (тождественно равно t(x)) — выражение, содержащее, может быть, переменную x. Тогда λx.t(x) — это такая функция f, которая сопоставляет аргументу a значение t(a). Иными словами, имеет место
(λx.t(x))a = t(a)"
Т.е. определение абстракции дается через аппликацию. Разве нет?
SI>>Заодно еще один вопрос о (3) M, N Є Λ -> (MN) Є Λ SI>>Правильно ли понимать MN просто как упорядоченный набор лямбда-термов M и N. И правильно ли это называть применением M к N?
D>Именно. Это и есть применение.
Здравствуйте, ShcheknItrch, Вы писали:
SI>У Барендрегта определение бета-редукции дается страницей позже, поэтому я его и не хотел пока касаться.
Лямбда без редукции — это просто правила формирования правильных термов.
SI>>>Т.е. выходит так, что сначала дается определение лямбда-абстракции с использованием понятия аппликации, т.е. привлекая понятие функции (определения которого еще не было дано). Далее дается определения лямбда-термам и процессу их индуктивного построения. Ну и пока все.
D>>В определении абстракции нет использования аппликации. Терм это либо переменная, либо абстракция над термом, либо аппликация (применение) терма к терму.
SI>Ну как же нету? Вот ведь: SI> ... SI>Иными словами, имеет место SI>(λx.t(x))a = t(a)" SI>Т.е. определение абстракции дается через аппликацию. Разве нет?
Ещё раз: определение абстракции, вот оно
M Є Λ -> (λxM) Є Λ
А (λx.t(x))a = t(a) — это как раз правило бета-редукции.
D>А (λx.t(x))a = t(a) — это как раз правило бета-редукции.
Хорошо, спасибо.
Но разве можно считать нормальным, что в классической книге изложение проводится таким образом, что можно запутаться. Может, я не то читаю? Есть ли что-то более приближающееся к совершенству?
И еще один вопрос. Есть выражение
((λx(λy.yx))M)N
как можно получить, что оно равно
(λy.yM)N
а это, в свою очередь
MN
Здравствуйте, ShcheknItrch, Вы писали: SI>Но разве можно считать нормальным, что в классической книге изложение проводится таким образом, что можно запутаться. Может, я не то читаю? Есть ли что-то более приближающееся к совершенству?
Я читаю вот что: http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
Здравствуйте, ShcheknItrch, Вы писали:
SI>Но разве можно считать нормальным, что в классической книге изложение проводится таким образом, что можно запутаться. Может, я не то читаю? Есть ли что-то более приближающееся к совершенству?
Барендрегт — это монография, а не учебник. Лекции Харрисона считаются лучшим учебником
SI>И еще один вопрос. Есть выражение SI>((λx(λy.yx))M)N SI>как можно получить, что оно равно SI>(λy.yM)N SI>а это, в свою очередь SI>MN SI>Не могу понять, как это получается
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, ShcheknItrch, Вы писали:
SI>>Но разве можно считать нормальным, что в классической книге изложение проводится таким образом, что можно запутаться. Может, я не то читаю? Есть ли что-то более приближающееся к совершенству?
D>Барендрегт — это монография, а не учебник. Лекции Харрисона считаются лучшим учебником
SI>>И еще один вопрос. Есть выражение SI>>((λx(λy.yx))M)N SI>>как можно получить, что оно равно SI>>(λy.yM)N SI>>а это, в свою очередь SI>>MN SI>>Не могу понять, как это получается
D>Это просто неверно D>
D>((λx(λy.yx))M)N ~> (λy.yM)N ~> NM
D>
Это из Барендрегта, из псевдодоказательства леммы 2.1.10 на странице 37. Не знаю, что и сказать
Здравствуйте, ShcheknItrch, Вы писали:
SI>>>И еще один вопрос. Есть выражение SI>>>((λx(λy.yx))M)N SI>>>как можно получить, что оно равно SI>>>(λy.yM)N SI>>>а это, в свою очередь SI>>>MN SI>>>Не могу понять, как это получается
D>>Это просто неверно D>>
D>>((λx(λy.yx))M)N ~> (λy.yM)N ~> NM
D>>
SI>Это из Барендрегта, из псевдодоказательства леммы 2.1.10 на странице 37. Не знаю, что и сказать
Открыл: там написано ровно как у меня NM, а не MN как у тебя
Здравствуйте, Mr.Cat, Вы писали:
MC>Здравствуйте, ShcheknItrch, Вы писали: SI>>Но разве можно считать нормальным, что в классической книге изложение проводится таким образом, что можно запутаться. Может, я не то читаю? Есть ли что-то более приближающееся к совершенству? MC>Я читаю вот что: http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, ShcheknItrch, Вы писали:
SI>>>>И еще один вопрос. Есть выражение SI>>>>((λx(λy.yx))M)N SI>>>>как можно получить, что оно равно SI>>>>(λy.yM)N SI>>>>а это, в свою очередь SI>>>>MN SI>>>>Не могу понять, как это получается
D>>>Это просто неверно D>>>
D>>>((λx(λy.yx))M)N ~> (λy.yM)N ~> NM
D>>>
SI>>Это из Барендрегта, из псевдодоказательства леммы 2.1.10 на странице 37. Не знаю, что и сказать
D>Открыл: там написано ровно как у меня NM, а не MN как у тебя
Да, тут я неправ, но вопрос не снимается.
Как показать, что
((λx(λy.yx))M)N ~> (λy.yM)N
?
Здравствуйте, ShcheknItrch, Вы писали: SI>Ну вот объясните, что тогда понимается под функцией, есть ли такое понятие, как область определения, на которой задан аргумент, и во что отображает эта функция.
ЛИ — это, если можно так выразиться, символьная система. Она изучает символы, как из них можно записывать выражения и как эти выражения потом можно комбинировать и переписывать. Понятия "функция", "число" и т.п. к ЛИ не относятся — мы их применяем к определенным выражениям неформально, на основании интуитивного сходства.
SI>2.1.1. Определение. (i) Ламбда-термы будут словами в следующем алфавите: SI> v0, v1, ... переменные SI> λ абстрактор SI> ( , ) скобки. SI> (iii) Множество Λ ламбда-термов (или, что то же, λ-термов) индуктивно определяется следующим образом: SI> (1) x Є Λ; SI> (2) M Є Λ -> (λxM) Є Λ; SI> (3) M, N Є Λ -> (MN) Є Λ, SI>где x в (1) и (2) — произвольная переменная.
SI>Ведь если у нас изначально есть только одни лишь лямба-термы, то мы можем только лишь их комбинировать, а вот под применением функции к аргументу можно понимать только лишь применение одного лямбда-терма к другому. Тут под применением нужно понимать простое комбинирование. SI>... SI>Правильно ли понимать MN просто как упорядоченный набор лямбда-термов M и N. И правильно ли это называть применением M к N?
Какое такое простое комбинирование? Нет простого комбинирования и упорядоченных наборов. Есть три правила формирования термов.
SI>Т.е. выходит так, что сначала дается определение лямбда-абстракции с использованием понятия аппликации, т.е. привлекая понятие функции (определения которого еще не было дано). Далее дается определения лямбда-термам и процессу их индуктивного построения.
Забудь про функции. Все в ЛИ — набор символов. Абстракция — набор символов из правила (2) цитаты выше. Аппликация — набор символов из правила (3).
SI>Но что меня смущает — так это то, что в определение лямбда-термов входит лямбда-абстрактор, который понимается как (см. первый пост):
Нет, не входит (если ты имеешь в виду просто буковку "λ"). Он входит в алфавит, словами в котором являются термы.
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, ShcheknItrch, Вы писали:
SI>>Да, тут я неправ, но вопрос не снимается. SI>>Как показать, что SI>>((λx(λy.yx))M)N ~> (λy.yM)N SI>>?
D>Во внешних скобках стоит аппликация D>
D>(λx(λy.yx))M
D>
D>делаем над ней бета-редукцию, заменяя все вхождения переменной x в терм, абстрагированный по x, то есть (λy.yx), на M. Получаем D>
D>(λy.yM)
D>
Да, действительно, получается. Остальное — тоже. Большое спасибо за все.
Такое впечатление, что, в частности, мне не хватает техники. Нет ли где-то правильных упражнений с ответами для тренировки?
Здравствуйте, Mr.Cat, Вы писали:
MC>Здравствуйте, ShcheknItrch, Вы писали: SI>>Ну вот объясните, что тогда понимается под функцией, есть ли такое понятие, как область определения, на которой задан аргумент, и во что отображает эта функция. MC>ЛИ — это, если можно так выразиться, символьная система. Она изучает символы, как из них можно записывать выражения и как эти выражения потом можно комбинировать и переписывать. Понятия "функция", "число" и т.п. к ЛИ не относятся — мы их применяем к определенным выражениям неформально, на основании интуитивного сходства.
SI>>2.1.1. Определение. (i) Ламбда-термы будут словами в следующем алфавите: SI>> v0, v1, ... переменные SI>> λ абстрактор SI>> ( , ) скобки. SI>> (iii) Множество Λ ламбда-термов (или, что то же, λ-термов) индуктивно определяется следующим образом: SI>> (1) x Є Λ; SI>> (2) M Є Λ -> (λxM) Є Λ; SI>> (3) M, N Є Λ -> (MN) Є Λ, SI>>где x в (1) и (2) — произвольная переменная.
SI>>Ведь если у нас изначально есть только одни лишь лямба-термы, то мы можем только лишь их комбинировать, а вот под применением функции к аргументу можно понимать только лишь применение одного лямбда-терма к другому. Тут под применением нужно понимать простое комбинирование. SI>>... SI>>Правильно ли понимать MN просто как упорядоченный набор лямбда-термов M и N. И правильно ли это называть применением M к N? MC>Какое такое простое комбинирование? Нет простого комбинирования и упорядоченных наборов. Есть три правила формирования термов.
SI>>Т.е. выходит так, что сначала дается определение лямбда-абстракции с использованием понятия аппликации, т.е. привлекая понятие функции (определения которого еще не было дано). Далее дается определения лямбда-термам и процессу их индуктивного построения. MC>Забудь про функции. Все в ЛИ — набор символов. Абстракция — набор символов из правила (2) цитаты выше. Аппликация — набор символов из правила (3).
SI>>Но что меня смущает — так это то, что в определение лямбда-термов входит лямбда-абстрактор, который понимается как (см. первый пост): MC>Нет, не входит (если ты имеешь в виду просто буковку "λ"). Он входит в алфавит, словами в котором являются термы.
Спасибо. Все же тяжело разбираться, когда в явном виде не всегда указано, что именно используется неформально (на основании интуитивного сходства), а что следует воспринимать как определения или аксиомы. Впрочем, возможно, это проблемы моего восприятия.
