Разговор о сути лямбда-теории [не задача, не просьба]

[mclaudt]

Уважаемые участники, недавно начал вникать в предмет. Возник следующий фундаментальный вопрос.

Работа с каким наглядным осязаемым объектом привела математиков к созданию бестиповой λ-теории и пониманию необходимости абстрагирования до двух базовых понятий "абстракции" и "аппликации"?

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

Сразу скажу, что цвет диплома и статус вуза не даёт права страдать ГСМ. Однако формулировка околофилософская какая-то получилась...

-- Чт янв 14, 2010 22:48:26 --

Я продублировал вопрос на ЛОРе, но там всё-таки не так много специалистов.

Ничего конкретного там не подсказали пока. Лишь один алгебраист указал на ненужность осязаемости образов, а также отметилась пара ленивых троллей.

[Xaositect]

Википедия говорит:

Цитата:

In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. It was introduced by Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics. After the original system was shown to be logically inconsistent (the Kleene–Rosser paradox), Church isolated and published in 1936 just the portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker but logically consistent system, known as the simply typed lambda calculus.

И отсылают к Cardone, Hindley."History of Lambda-calculus and Combinatory Logic" за историей вопроса.

[mclaudt]

Цитата:

Википедия говорит:

Да уж были там. И Барендрегта читал но ответа не нашёл.

Запись a+b — это итог многолетнего употреблния человечеством записи 1+4, 3+12, 7+2 и т.д.

Теория групп — результат обобщения многолетней истории пересечения человечества с различными ассоциативными структурами.

Результатом многолетнего употребления чего стала запись вида (λx.M)N = M[x:=N] ?

(Ну если исключить очевидные алгебраические подстановки типа (λx.x²+1)3=10 — других примеров у Барендрегта нету)

[Свободный Художник]

mclaudt в сообщении #280577 писал(а):

Уважаемые участники, недавно начал вникать в предмет. Возник следующий фундаментальный вопрос.

Работа с каким наглядным осязаемым объектом привела математиков к созданию бестиповой λ-теории и пониманию необходимости абстрагирования до двух базовых понятий "абстракции" и "аппликации"?

Работа с такими наглядными и осязаемыми объектами как функция и ее аргумент.

Только чего это Вам сразу бестиповости захотелось?
Типизированные лямбда-исчисление и комбинаторная логика проще для понимания.
Мне там особенно вот это нравится: $((Bx)y)z = x(yz)$.

[mclaudt]

Цитата:

Работа с такими наглядными и осязаемыми объектами как функция и ее аргумент.

Ну это вроде бы понятно, просто изначально у Баредрегда акцентируется внимание именно на бестипности.

Цитата:

... функция может применяться к самой себе. При обычном понимании функции в математике (скажем, в теории множеств Цермело-Френкеля) это невозможно (из-за аксиомы фундирования).

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

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

Но если это так, значит образом предмета изучения бестиповой лямбда-теории в реальную действительность являются имено записи действия неймановской машины. Почему об этом не говорится с самого начала? Есть ли другие образы?

Получается, что пример (λx.x²+1)3=10 неудачен, ибо как только у x появляется размерность, то все летит к чертям.

Цитата:

Только чего это Вам сразу бестиповости захотелось?

Нужно было настроить один сверхудобный оконный менеджер xmonad под замечательную операционную систему Linux, а он написан на Haskell.

[mclaudt]

mclaudt в сообщении #280633 писал(а):

, а он написан на Haskell.

Разумеется я не утверждаю что он как-то связан с бестипностью, типизация там статическая, просто ссылки по теме сразу вывели именно на это направление.

[Xaositect]

mclaudt в сообщении #280633 писал(а):

Но если это так, значит образом предмета изучения бестиповой лямбда-теории в реальную действительность являются имено записи действия неймановской машины. Почему об этом не говорится с самого начала? Есть ли другие образы?

Когда создавалось $\lambda$-исчисление, фон-неймановской машины еще не было. Так что изначально была все-таки идея преобразования.

mclaudt в сообщении #280633 писал(а):

Нужно было настроить один сверхудобный оконный менеджер xmonad под замечательную операционную систему Linux, а он написан на Haskell.

Ну, строго говоря, для этого не обязательно знать о бестиповом исчислении.

[mclaudt]

Цитата:

Когда создавалось $\lambda$-исчисление, фон-неймановской машины еще не было. Так что изначально была все-таки идея преобразования.

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

Действительно, какому объекту может соответствовать правило конверсии (λx.M)N=M[x:=N]?

Получается что обычная (графическая!) подстановка — единственное объяснение.

Ну так сказали бы сразу: "Ребята, мы столетиями рисовали мелками на доске и подставляли закорючки. В результате абстрагирования от предметной области мы создали теорию рисования закорючек вообще, основанную на операции `написания рядом` (аппликация) и `рассмотрения одной из закорючек как параметра` (абстракция) что порождает `вытирание и замену` (редукция). "

Зачем такое наукообразие? Называйте вещи своими именами!

ps Это я очевидно не вам лично, я создателям теории.

[Xaositect]

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

А в целом Вы правду пишете.

[mclaudt]

Цитата:

Всплывает она, как только определяется вложение натуральных чисел в лямбда-термы (нумералы Черча) и моделирование рекурсии с помощью комбинатора неподвижной точки.

Не сомневаюсь что всплывают, но тут оказывается первична именно графика.

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

Нет ли по вашему опыту учебника, который бы следовал духу арнольдовского (конструктивного и экспериментального) изложения, в простивовес душным алгебраистам?

[Xaositect]

mclaudt в сообщении #280711 писал(а):

Нет ли по вашему опыту учебника, который бы следовал духу арнольдовского (конструктивного и экспериментального) изложения, в простивовес душным алгебраистам?

Мне понравилась вот это популярное изложение: To dissect a mockingbird

[mclaudt]

Кстати вот подумалось, — если рассмотреть страницы формулировки аксиом лямбда-теории и разных выкладок, то ведь они тоже написаны с применением неких синтаксических правил вывода... Думаю, зловещая рекурсия уже видна...

Не возникает ли на этом месте некого подобия парадокса Рассела? Знаю что формулировка наивна, но думаю, что понятно о чём речь.

[Xaositect]

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

[mclaudt]

Цитата:

Нет, здесь возникает подобие универсальной машины Тьюринга.

Это как если на жёстком диске компьютера лежат все техдоки и даташиты по нему в виде PDF

За пересмешника спасибо.

[Circiter]

mclaudt

Цитата:

Работа с каким наглядным осязаемым объектом привела математиков к созданию бестиповой λ-теории

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

Цитата:

Результатом многолетнего употребления чего стала запись вида (λx.M)N = M[x:=N] ?

Результатом использования функций. Ведь, по-сути, $\lambda$-исчисление является исчислением безымянных функций.

Цитата:

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

Почему-же нельзя? Попробуйте, вдруг чего выйдет. Я, честно говоря, даже представить себе такое не могу... Поясните, если не сложно.

Цитата:

Так что рассматривать функцию в лямбда-теории как множество упорядоченных пар — неверно и противоречиво. Но других-то (как бы) мы и не знаем пока.

Хм, ну функции в $\lambda$-исчислении и функции из мат. анализа -- это совсем разные вещи. В лямбда-исчислении $\lambda$-абстракция и функция суть одно и то же. И никаких рекурсий, просто из-за отсутствия имен. Если нужна рекурсия, то нужно использовать $Y$-комбинатор или другие "извращения".

Цитата:

Действительно, какому объекту может соответствовать правило конверсии (λx.M)N=M[x:=N]?

Получается что обычная (графическая!) подстановка — единственное объяснение.

Ну так сказали бы сразу

Действительно, все эти, возможно излишние, конверсии нужны лишь для строгости системы. Если вы попробуете написать компилятор $\lambda$-выражений, то возможно обойдетесь просто подстановками, но если захотите показывать пользователю все этапы преобразования, всю "кухню", но возникнут проблемы с именованием "переменных", вот они-то и решаются всеми этими "лишними" (мета) правилами.

Цитата:

тут оказывается первична именно графика.

Лямбда-выражения могут быть смоделированы не только ведь формулами на бумаге. Они могут быть смоделированы списками (e.g., как в lisp'е), или, скажем, трубопроводом с системой задвижек. Графика здесь напричем, важны сами символы.

Цитата:

Кстати вот подумалось, — если рассмотреть страницы формулировки аксиом лямбда-теории и разных выкладок, то ведь они тоже написаны с применением неких синтаксических правил вывода... Думаю, зловещая рекурсия уже видна...

А представьте, что вы уже написали на некотором языке ранее упоминавшийся $\lambda$-компилятор, а потом перевели его исходники на его же входный язык. Все это будет вполне работоспособно и парадоксов не будет (внешенй системой станет не свод правил, а железо компьютера).