`

СПЕЦІАЛЬНІ
ПАРТНЕРИ
ПРОЕКТУ

Чи використовує ваша компанія ChatGPT в роботі?

BEST CIO

Определение наиболее профессиональных ИТ-управленцев, лидеров и экспертов в своих отраслях

Человек года

Кто внес наибольший вклад в развитие украинского ИТ-рынка.

Продукт года

Награды «Продукт года» еженедельника «Компьютерное обозрение» за наиболее выдающиеся ИТ-товары

 

λ-исчисление

Статья опубликована в №47 (615) от 11 декабря

+66
голосов

В этой статье пространных вступлений и отступлений не будет. Поэтому приступаем незамедлительно.

λ-исчисление

Бертран Артур Уильям Рассел (1872–1970).
Англичанин, наверное, первый и последний выдающийся универсальный мыслитель XX столетия – математик, философ, активный общественный деятель мирового уровня, лауреат Нобелевской премии по литературе. Был сторонником превращения философии в строгую науку привлечением в философию методов математической логики

λ-исчисление

Альфред Норт Уайтхед (1861 – 1947).
Английский математик, соавтор одной из самых значительных математических работ XX века, «Начала математики». Уайтхед отдал много сил философии и передовым для своего времени разделам физики

λ-исчисление

Алонзо Черч (1903 – 1995).
Автор теории лямбда-исчислений и соавтор знаменитых тезисов Черча-Тьюринга – интуитивного и физического. Физический тезис Черча-Тьюринга утверждает, что любая функция, которая может быть вычислена физическим устройством, может быть вычислена машиной Тьюринга или «машиной Черча» (методом лямбда-исчисления)

Лямбда-исчисление, один из ключевых, если так можно сказать, «механизмов» функционального программирования, является не чем иным, как моделью абстрактного вычислителя, эквивалентного машине Тьюринга. То есть это тоже абстрактная машина. Правда, весьма специфическая, и механические аналогии (каретки, считывающие и печатающие головки и ленты), которые помогают представить себе подобную машину, тут совершенно бесполезны. Здесь только чистая математическая абстракция, но в дальнейшем не следует забывать, что речь идет именно об универсальной машине. Точно так же не следует забывать, что эквивалентных машине Тьюринга абстрактных вычислителей создано немало, и в их перечне есть такие шедевры специфического математического юмора, как легендарный Brainfuck! – придуманная Урбаном Мюллером абстрактная машина всего с восемью командами, столь популярная, что для нее даже создают аппаратные «овеществления». И наконец, не стоит забывать о том, что такое «эквивалентность машине Тьюринга», или полнота по Тьюрингу. Не вдаваясь в детали и теорию, это означает, что эквивалентная машине Тьюринга машина принципиально способна выполнить вычисление всего, что можно вычислить с помощью любого программируемого компьютера (так как до сих пор ведутся дебаты о вычислимости посредством машины Тьюринга событий квантовой механики, неясно, можно ли под любым программируемым компьютером понимать квантовый вычислитель).

Синтаксически (и, что вовсе уж забавно, даже названием) лямбда-исчисление обязано в том числе и тем, которые «страшно далеки от народа» (чистым математикам, само собой, а «народ» в данном случае – полиграфисты). Это и шутка, и не шутка, мы ее еще вспомним. Причем это не анекдот, а исторически подтвержденный факт, сохранившийся в дебрях новостных групп Usenet благодаря воспоминаниям Брюса МакЛеннана о его встрече с Алонзо Черчем в 1982 г. на конференции по функциональному программированию и Lisp. Так как URL записи МакЛеннана непозволительно длинный для бумажного журнала, желающие могут отыскать этот исторический пост с помощью Google в архивах comp.lang.functional (автор – Bruce MacLennan, название – «origin of lambda symbol», 27 февраля 1991 г.).

В фундаментальном трехтомном труде «Начала математики» (Principia Mathematica, авторы – величайшие философы и математики XX столетия Бертран Рассел и Альфред Норт Уайтхед) использовалась специфическая форма записи для функций, которую лучше всего объяснить на примере, скажем, функции, в привычном для нас «школьном» виде выглядящей как f(x) = 2x + 3:

2x^+3.

Математики, это общеизвестно, обожают богатство стилей, роскошные греческие символы и т. п. (но не только из эстетических соображений), вот и в данном случае циркумфлекс («крыша домика» над именем переменной) на самом деле является весьма специфическим оператором. Так как термин «оператор» в IT-мире уже «заезженный» и многозначный, здесь придется тяжело вздохнуть и привести следующее пояснение – в дальнейшем под «оператором» будет пониматься математический оператор, в самом общем виде являющийся отображением некоторого множества X в другое множество Y (а уж от того, чем являются элементы этих множеств, и чем – сами эти множества, зависит и специфика конкретных операторов, которых в разных разделах математики предостаточно). Названный «оператором абстракции» циркумфлекс отображал множество, образованное функциями и значениями для переменных, отмеченных циркумфлексом, в множество результатов вычислений этих функций после подстановки значений переменных вместо отмеченных оператором символов. Человеческими словами это лучше всего объяснить на примере следующего отображения:

(2x^+3) 3 → 7.

То есть вместо x, отмеченного циркумфлексом, мы подставили 3 и получили, что 2 • 3 + 1 равняется семи, короче, отобразили элемент одного множества (образованного парами «функция – значение») в элемент другого. Математика Алонзо Черча, автора λ-исчисления, такая форма записи функций не устроила, он хотел более ярко выраженного «операторного» характера и решил использовать следующую, «линейную», а не «двухмерную» форму записи:

^x. 2x + 1

Здесь в части до точки явно указывается переменная, вместо которой будут подставляться значения, а после точки – собственно алгоритм (если так можно сказать) вычисления результата. Но типография не могла напечатать такой странный циркумфлекс, а если его «опустить» на уровень всей строки, получается символ «λ», который уже «занят» (математики очень любят символы!) и вносит путаницу. Чтобы не править рукописи, Черч принял решение заменить занятый символ на относительно свободный похожий греческий – «λ». Так и возникло название «λ-исчисление». От момента появления традиционной алгебраической записи, которую ввел в «математический обиход» еще один великий математик и мыслитель Франсуа Виет, прошло, в общем, не так уж и много времени – около 250 лет (до нотации Виета математики вообще вместо описывали словесно процесс получения результата).

В λ-исчислении используются две ключевые формы записи – для выражений и функций. Первые принято представлять строго в префиксной форме (обратной польской), используя скобки только для необходимой группировки, например, традиционно sin(x) в λ-исчислении записывается просто как sin x, x + 4 становится + 4 x, а более сложное sin(x) + 4 приобретает следующий вид: + (sin x) 4.

Функция записывается в форме, на самом деле весьма похожей на запись функций в традиционных, императивных языках программирования. Например, функция λx. + 4 x весьма похожа на C-функцию int add4(int x) { return x+4; }, но с некоторыми нюансами. Во-первых, здесь используется операторный синтаксис описания «параметров» – λимя_переменной, во-вторых, для отделения выражения от описания параметров используется символ «.», в-третьих, в λ-исчислении функция не имеет имени (об обратной польской записи выражений мы уже говорили).

Шаблон прочтения для такой формы записи может быть следующим: «λ» читается как «функция с формальным параметром», затем следующий за ней символ, а «.» читается как «и с телом, являющимся» и дальше – выражение. То есть (λx. + 4 x) можно прочесть как «функция c формальным параметром x и c телом, являющимся выражением 4+x». Мы можем применить эту функцию к некоторому значению (или же отобразить элемент одного множества на элемент другого), например так: (λx. + 4 x) 3 (скобки в этой записи используются только для того, чтобы избежать возможных разночтений и явно отделить функцию от значения).

Если теперь добавить к уже сказанному то, что описанные в таком виде функции могут сами использоваться и в качестве значения для параметров, и в выражениях тела функции, мы получим почти завершенный... да, именно тот самый абстрактный вычислитель Алонзо Черча, который эквивалентен машине Тьюринга.

Давайте рассмотрим такой пример: λt.( λx. • t x). Воспользуемся предложенным ранее способом прочтения: «функция с формальным параметром t и с телом, являющимся функцией с формальным параметром x и с телом, являющимся выражением t • x». Что будет, если мы применим такую функцию, например, к числу 3? Мы получим функцию. А именно, функцию c формальным параметром x и с телом, являющимся выражением 3 • x. И если мы применим ее к числу 5, то получим в результате значение выражения 3 • 5, или 15. То есть мы нашли, что ( ( λt.( λt. • t x) ) 3 ) 5 ) есть 15. Этот простой пример на самом деле весьма непрост. С одной стороны, мы в нем фактически описали функцию от двух переменных и унифицированный подход к описанию функций от N переменных. С другой же – механизм описания целого класса параметризованных функций (если считать t параметром).

Мы использовали при прочтении λ-форм функций несложный язык («функция с формальным параметром» и т. п.) не только для удобства, но и для намека на то, что такой язык действительно существует, у него есть формальная грамматика, которая применяется разработчиками трансляторов функциональных языков. Ну а степень близости последних к оригинальному λ-исчислению можно оценить на примерах записи функции λy. + 1 y на самых модных языках программирования:

Haskell: (y -> (1 + y))
Scheme: (lambda (y) (+ 1 y))
SML: (fn y => 1 + y)

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

До завершения ознакомительного описания «машины Черча» осталась одна важная деталь – мы уже знаем, как записывать функции, теперь надо понять, что с этими записями можно и нужно делать. К счастью, «машина Черча» может выполнять, по сути, всего одну операцию – редукцию (если вы собираетесь ввязываться с «функциональными маньяками» в горячие дискуссии, используйте в них более точный термин – β-редукцию, на ознакомительном уровне детали нам не важны, но маньяки за них могут и покусать).

Собственно, редукция – это правило вычислений, выполняемых «машиной Черча» (и процесс применения того самого оператора, о котором мы говорили раньше), и заключается оно в замене формального параметра актуальным значением (буквально только что мы неформально говорили о том же – «применить функцию к...»). Редукция даже не требует непосредственно выполнения вычислений, когда функцию уже не к чему применять; так, в предыдущем примере, где получался результат «15», работа «машины Черча» завершается по достижению выражения • 3 5 потому, что в нем больше нет ни одного формального параметра, следовательно, заменять в нем нечего. Но отсутствие формальных параметров в выражении не является достаточным условием остановки работы «машины Черча». В качестве больше забавы, чем головоломки, попробуйте редуцировать следующий вариант применения функции к значению параметра: (λx. x x) (λx. x x). Вы получите... то же самое. Подобные сочетания функции и значения параметра получили название нормальной формы, которая (редуцируй ее, если можно – не редуцируй, если не получается) все равно не меняется.

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

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

λ-исчисление
Редукция λf.( λx. f ( f x )) (λx. •( • x x) x) дает предсказуемый результат – x9, потому что (x3)3 = x9

Начнем с констатации факта – пока мы говорили о работе «машины Черча», о редукции, мы, по сути, говорили о формальном преобразователе символьных цепочек, за которыми ничего не стоит. Иными словами, «машина Черча» понятия не имеет о традиционных для языков программирования типах данных, она просто подставляет то, что нужно подставить, туда, куда это нужно подставить, и прекращает работу, когда или подстановки невозможны, или они не приводят к изменениям. А это значит, что всем, что существует в «λ-мире», можно оперировать на основании правил «λ-мира» (т. е. редукции). Что, в свою очередь, означает, например, правомочность следующей записи: λf.( λx. f ( f x )). Учитывая тот факт, что для «машины Черча» все равно, что подставлять, мы можем утверждать – перед нами описание процедуры применения некоторой функции f к результату применения этой же функции к x, в школьной записи – f(f(x)), вот только переменной здесь является... сама функция f. Для простоты попробуем в качестве f использовать функцию λx. • x x, которая, очевидно, описывает возведение в квадрат, а для еще большей простоты не будем проводить редукцию вручную, и воспользуемся для этого подходящим инструментом, благо он доступен, бесплатен и не зависим от платформы. Таким инструментом будет Lambda Calculator, крохотная Java-программка, делающая в точности то, что нам нужно. А именно, после ввода в поле интерфейса «as» задачи, подлежащей редукции, Lambda Calculator выполняет редукцию и показывает пошаговый ее результат. Нюансов всего два – вместо символа λ при вводе используйте «» (программа заменит его на «λ» сама), а актуальное значение параметра отделяйте пробелом. То есть вводите с клавиатуры следующую последовательность символов: (f.(x.f (f x))) (x.* x x). Результат редукции – функция λx. •( • x x) ( •x x). Если «прочитать» эту запись с помощью использованного ранее правила и не забыть об обратной польской записи, мы получим: «функция с формальным параметром x и с телом, являющимся выражением x4». Что, в принципе, и требовалось доказать, потому что (x²)² – не что иное, как x4. Попробуйте самостоятельно вместо функции λx. • x x использовать любую другую и убедитесь в том, что «машина Черча» работает как часы (на самом деле вы убедитесь только в том, что ее симулятор, Lambda Calculator, выполняет эти задания корректно, но ведь никто не запрещает взять лист бумаги, ручку и проверить результат вручную).

Давайте теперь посмотрим на исследованную нами только что функцию λf.( λx. f ( f x )) по-другому, а именно, как на некоторый оператор, допускающий применение к другим функциям (мы уже в этом убедились) и... к самому себе, ведь он – такая же равноправная функция. Подобным операторам (функциям), применимым к функциям, принято присваивать титул «высшего порядка».

Вернемся опять к фундаментальному свойству «машины Черча», к ее сугубо синтаксическому характеру. Оно означает, в том числе, что процессом редукции могут порождаться не только всякие полезные нормальные формы, но и вовсе бесполезные ненормальные мутанты – хотя бы потому, что ничто не запрещает им появляться, так как для «машины Черча» символы ровным счетом ничего не значат. Чтобы избежать появления таких бесполезных созданий, вводится понятие типа. На принятом нами уровне детализации оно означает всего лишь, что λ-функция сопровождается дополнительной информацией о двух фундаментальных для нее множествах (еще раз вспоминаем о том, что такое оператор абстракции) – множестве допустимых аргументов и множестве отображаемых ею значений. Более «околокомпьютерными» словами – информацией о допустимых входе и выходе. Для характеристик этих множеств можно использовать как теоретико-множественное описание (например, «множество всех целых чисел, бoльших -2N-1 и меньших 2N-1») , так и сокращенные обозначения, которые принято использовать в языках программирования (типа Int). Соответственно, теперь λ-функция (или оператор абстракции) может описываться и на уровне преобразования Tin → Tout, где Tin – тип «входа», Tout – тип «выхода». Что особенно интересно, на основании хорошо известных и наиболее часто используемых множеств чисел и понятия функции создан стройный и элементарный язык описания системы простых типов (на самом деле даже не один, но нам это не важно) со своей формальной грамматикой. Фундаментальным понятием системы типов является термин «хорошо типизованный», который применим практически ко всем описанным составляющим «машины Черча», например:

  • любая переменная любого типа является хорошо типизованной;
  • для любого выражения N, приводящего к типу A, и любой переменной x типа B, λx. N является хорошо типизованной и имеет тип B → A.

В сочетании с несложной «механикой» редукции это позволяет не только формально доказать ряд теорем, не только ввести понятие и механизм «вычисления типа», но и доказать главное утверждение – любая хорошо типизованная λ-функция имеет нормальную форму. Иными словами, «машина Черча», умеющая оперировать типами, всегда находит решение.

Собственно говоря, базовые понятия на этом не исчерпываются, но и остаток их не так уж и страшен. Вне нашего внимания остались вопросы, требующие более углубленного изучения λ-исчисления, в первую очередь все, что связано с изменением потока исполнения и с рекурсией. К смежным, но также базовым понятиям, следует отнести «ленивое исполнение» – такую реализацию потока вычислений, при которой на каждом этапе выполняется только то, что необходимо для получения результата. В одних функциональных языках (Scheme) механизмы управления «ленивым исполнением» открыты программисту, для них есть специальные языковые конструкции, другие же языки «ленивы от природы» (Haskell).

Наконец мы можем сказать, что такое «функциональное программирование» – это построение такого множества таких функций и такого порядка приложения их к результатам их редукции, что окончательным результатом редукции (и вычислений) является то, что требовалось получить.

Заметьте, мы ни слова не говорили о ячейках памяти, регистрах, в общем, обо всем том, что может хранить в себе что-то и что характеризуется разными состояниями в разные моменты времени, что мы неявно используем в любой операции присваивания любого императивного языка программирования, например в такой: x = x + 1. В ней фактически описывается новое состояние ячейки, хранящей переменную x, после выполнения операции над предыдущим состоянием этой ячейки. Ничего подобного в функциональном программировании нет и не должно быть. В идеале. Для реальных же задач функциональная цепочка должна и начинаться с чего-то реального (например, с данных от датчика температуры или с команд мыши), и заканчиваться чем-то не менее реальным. Для всех функциональных языков, особенно нежных «ленивых от природы», такие нюансы суровой реальности совершенно ужасны и порождают адекватные защитные механизмы. Но о них в следующий раз.

Ready, set, buy! Посібник для початківців - як придбати Copilot для Microsoft 365

+66
голосов

Напечатать Отправить другу

Читайте также

Дякую за непоганий вступ в λ-обчислення. Написано доступно, чекаю продовження.

можно купить журнал и не ждать :)

Журнал лежить і вже прочитаний. В статті обіцяли продовження, то я і назвав статтю вступом ;)

понял, тогда ждите, будет :)

А я только позавчера добрался до журнальной статьи, а уже и тут появилась :)

Да Андрей Зубинский как всегда на высоте, и действительно
вступление аддрессованого полиграфистам (или типографистам) нету.

Помнится когда-то в одной из стран Скандинавии в LISP скобки совпадали со скандинавскими буквами втиснутыми в кодовый набор,
из первых 127-символов.
Хоть сам язык и нерегламентировал такой неразберихи,
в результате, получилось весьма колоритно.
А когда пытались описать по Англиски суть проблемы,
то получалось вообще нечто.
Хотя λ в LisP пишется как lambda.

У лично меня была идея вернуться к первой машине
(Deus Ex Machina).
Придумали такое полезное приспособление
не во времена Древнего Рима и
даже не во Времена Древней Греции,
а где-то так в сренднем Царстве Египта,
и уже после того которую почему-то изобразили
на обложке к недавно вышедьшему Русскоязычному
изданию известной книги.
До этого на подобных приспособлениях Древние Египтяне
воду качали.

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

Но нет, как показала история графические символы
которые не подтверждаются - теряют смысл,
а машина, это машина.
Разве не так?

--DawnON

Теперь серьезно.

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

Так говорят о машине Тюринга или о архитектуре фон Неймана,
как о чем-то что исключае одно другое.

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

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

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

Теперь представим себе, что мы имеем некий микропроцессор,
архитектуры von Neumann'а. Пускай он имеет некий указатель команд,
и с другой стороны некие регистры которые содердат некие данные,
некий процеессор (или АЛУ) и некий дешифратор команд,
(который в сущьности тоже есть АЛУ).
Пускай в начале дается некоторое начальное значение для счетчика команд, и он перебирая их последовательно,
доходит до некого значения которое можно считать конечным.
Пускай магазином есть сам щетчик команд а значения регистров его интересуют поскольку постольку они могут изменить его значение.
Теперь если регистры (включительно с регистром команды или регистровой очередью команд)
могут изменять его значение тогда что-бы до von Neumann'овского
процессора дорисовать упущеные елементы машины Тюрингы
структуру магазина и свойство вычислителя и ленту команд надо определить исходя из виртуальных свойств, остальных устройств,
микропроцессорной системы.
(То есть определить, что именно из деятельности дешифраторов,
арифметических логических процессоров, памяти, и регистров,
относится к рекурсивным свойствам, а что к свойствам вычислителя.
Вычеслитела который в свою чоередь тоже производит дешифрирование
и арифметические и логические операции.
)
Это сделать трудно технически,
но не значит что невозможно теоретически.
Теперь что бы постостроисть машину которая объеденяла в себе свойства, и функционального, и императивного программирования
в их чистом виде осталось сделать малое - найти где сходится то и другое.

--DawnON.com

Кстати вот вспомнилось у меня был знакомый который,
рассказывал что формальные грамматики, часто описуются именно посредством некой рекурсивной машины.
(Собственно это теория.)

Причем тот мой знакомый писал на нескольких языкахю,
и даже разрабатывал компиляторы (или как он говорил Compilant'ы).

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

Чем не решение?

Если он это читает то хотелось бы что-бы он сам как-то отреагировал.
И еще небольшей отступление личного характера, там где он раньше работал поменялось начальство, и очень добрым оказался руководитель всей компании. Руководитель даже предлагал предлагал вернуться если упомянутый добрый человек изъявит желание (хотя не на ту же самую должность.) Но пусть поспешит, ато где-то через пол года добрый начальник переходит на другую работу. Хотя мужик хороший, тоже пишет на нескольких языках, тоже как-то работал в Европе, и даже музыку в чем-то похожую слушает (правда немного сложнее). А что про него в форумах говорят - так закрой уши Вспомни песенку "Alexander the Great".

--DawnON

Если я хоть чуток секу в математике, то (2x^+3) 3 → 9!

Говорили балакали посідали тай й заплакали.

В данном случае автор рассказывает об некоторой автоматической системе
которая позволяет определять значение тех или иных знаков.
(По крайней мере это я себе так понял.)

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

--DawnON

 

Ukraine

 

  •  Home  •  Ринок  •  IТ-директор  •  CloudComputing  •  Hard  •  Soft  •  Мережі  •  Безпека  •  Наука  •  IoT