Что такое лямбда? 11-я буква греческого алфавита
В настоящее время древнегреческий язык утратил многие признаки категории живого языка. Однако до сих пор на страницах школьных учебников, монастырских и церковных книг можно обнаружить древнегреческие слова и символы, используемые в качестве обозначения определенных величин.
За время своего существования древнегреческий язык сыграл большую роль в развитии мировой письменности и предопределил развитие некоторых мировых языков.
Интерес к языку подпитывается нередкими исследованиями алфавита, правил правописания и произношения. В данной статье узнаем, что представляет собой 11-я буква греческого алфавита – лямбда.
Наука и Греция
Алфавит, изобретенный греками, основан на финикийской и древнегреческой азбуке. Его основная особенность заключается в содержании двух типов букв – согласных и гласных. Прошло более двух десятков веков, но алфавит сохранился.
В научной среде греческий алфавит занимает прочное место. Во многих отраслях знаний его буквы можно обнаружить в качестве обозначения некоторых показателей. В математике синус угла обозначается α, используется знак суммы Σ. В астрономии в названии самых крупных звезд ярких созвездий упоминается α (альфа Большого Пса). В биологии при изучении групп особей активно используются понятия омега-самка и альфа-самец. В разделе ядерной физики можно встретиться с понятиями гамма-частицы и альфа-излучения. На страницах учебников химии и физики в качестве постоянных величин фигурируют ρ и λ, которыми обозначают плотность материала и длину волны соответственно. О последней букве расскажем подробнее, то есть ответим на вопросы о том, как пишется лямбда, откуда берет происхождение и где применяется.
Правописание
В первых версиях греческого алфавита внешний вид лямбды отличался от современного представления, хотя общее сходство наблюдалось. Большинство вариаций написания были представлены двумя прямыми линиями, одна из которых незначительно короче другой, а их концы сходятся. В восточном алфавите угол соединения находился в верхнем углу, в западном – в левом нижнем. Впоследствии римляне определились, что угол у них будет внизу слева, а греки решили, что он будет сверху. Последующий вариант содержал в себе вертикальный штрих с наклонной линией, уходящей вправо. В настоящее время букву лямбду прописную пишут согласно последнему описанному варианту, а заглавная выглядит в виде перевернутого знака V. На основе греческой лямбды образовалась латинская лямбда, заглавный символ которой представлен в виде перевернутого Y.
Значение
Лямбда образовалась от буквы финикийского алфавита – ламед. Данному символу в числовой алфавитной системе соответствовало число 30, которое в Греции приписывали справа сверху около вертикальной линии символа. На основании буквы лямбды образовались кириллическая Л и латинская L, а после и производные последних.
Использование прописной буквы
Области применения прописной версии буквы довольно обширны. Раньше символ можно было обнаружить на щитовых узорах спартанских войск. Сейчас он сохранился при обозначении вида частиц в физике, а в математике он представляет собой диагональную матрицу из собственных значений и выступает вводимыми операторами. Такое описание поясняет, что такое лямбда прописная и где она используется.
Строчная лямбда
Строчная буква λ закрепилась и занимает прочное место в физических формулах алгебры, физики, химии, информатики. Удельная теплота плавления, постоянная распада, длина волны, значение Ламе, линейная плотность электрического заряда – это те переменные, которые для простоты заменены этим символом. В биологии изучается вирус фаг лямбда. В информатике функциональные выражения производят в λ-исчислении. В самолетостроении при удлинении крыла вводится буква лямбда. В линейной алгебре найденные корни дифференциального уравнения также обозначаются через нее.
Каждый современный автомобилист знаком с лямбда-зондом, установленным в его транспортном средстве. Прибор измеряет количество образуемого углекислого газа в выхлопе. Оснащение автомобиля данным датчиком произошло по причине того, что власти многих стран заботятся об экологической составляющей и здоровье нации и таким образом регулируют количество выделяемого автомобилем СО2. В случае критичности значения этого показателя, то есть его превышения относительно допустимой величины, в качестве жесткой меры выписывается штраф. Этот датчик также необходим для соблюдения оптимального и экономного расхода топлива.
Связь с культурной сферой
Что такое лямбда в культурной среде? В известном кинофильме «Звездные войны» путешествовал космический корабль класса лямбда. Буква также используется в компьютерных играх под эмблемой «Комплекс Лямбда». По мере развития сюжета игры она применяется в качестве знака противоборства между населением и альянсом. Символ существует и в эмблеме игр, строчная буква лямбда нередко фигурирует в слове Half-Life, в итоге получается Hλlf-Life.
В романтической песне под названием «Австралия» Михаила Щербакова герой мечтал завести кенгуру, муравьеда или жирафа по имени Лямбда.
В 1970 году, когда регулярно стали проходить гей-парады, значок лямбда был впервые использован в Нью-Йорке в качестве обозначения правозащитной организации «Альянс гей-активистов». Через четыре года в Шотландии Международным конгрессом прав геев «λ» признана интернациональным знаком движения за свободу и права людей с нетрадиционной ориентацией.
В настоящее время под знаком лямбды в культуре понимают объединение именно таких людей. Активисты при объяснении, почему именно этот символ выбран ключевым для описания их движения, ссылаются на физическое понятие длины волны. Они видят аналогию с волной, направленной в пространство и бесконечность, и считают, что лямбда является удачным обозначением для описания предстоящих изменений в социуме, в котором лиц нетрадиционной ориентации должны принять.
Сакральное значение
Что такое лямбда в эзотерическом плане? Лямбда заключает в себе принцип органического роста и переход системы на возвышенный уровень. Это подтверждается примерами двух видов прогрессий, ключевых числовых последовательностей древнегреческой математики, где используется знак. В теоретическом плане буква символизирует возрастание числовых рядов, которыми описывается любая система физических явлений. Каждый, рассматривая руны, обозначающие возвышение и означающие звук «Л» или древнееврейский знак ламед, обнаружит сходство с исследуемой буквой.
В данной статье было рассмотрено, что такое лямбда, и где ее можно встретить в окружающем мире.
Как написать лямбду в ворде? Какой код Лямбда в ворде?
В программе ворд можно поставить разнообразные символы, в т.ч. лямбду. Так как с её написанием нередко возникают вопросы, то рассмотрим подробную инструкцию, как написать лямбду в программе ворд.
Первый шаг. Выберем на листе место, куда поставим символ лямбды, после перейдем на верхней панели настроек в закладку «Вставка» и нажмем в блоке «Символы» на иконку с аналогичным названием.
Второй шаг. В появившемся меню, нажмите на самую последнюю строчку «Другие символы».
Третий шаг. Появится подробное меню выбора различных символов, в строке набор из выпадающего списка, необходимо выбрать «греческие и коптские символы». Там можно найти маленькую и большую лямбду.
В итоге мы поставили в программе символы лямбда.
Некоторые пользователи вставляют символы через коды. Чтобы поставить символ большая лямбда, нужно вести код «039B», а для маленькой «03BB». Для преобразования кода в символ, поле его введения, нужно нажать сочетания клавиш «ALT+X».
Лямбда-исчисление: описание теоремы, особенности, примеры
Лямбда-исчисление — это формальная система в математической логике для выражения подсчетов на основе абстракции и применения функций с использованием привязки и подстановки переменных. Это универсальная модель, которую можно применять для проектирования любой машины Тьюринга. Впервые введена лямбда-исчисления Черчем, известным математиком, в 1930-х годах.
Система состоит из построения лямбда-членов и выполнения над ними операций сокращения.
Пояснения и приложения
Вам будет интересно: Какие элементы входят в социальную структуру общества, виды и функции социальных групп
Греческая буква lambda (λ) используется в лямбда-выражениях и лямбда-терминах для обозначения связывания переменной в функции.
Лямбда-исчисление может быть нетипизировано или напечатано. В первом варианте функции могут быть применены только в том случае, если они способны принимать данные этого типа. Типизированные лямбда-исчисления слабее, могут выражать меньшее значение. Но, с другой стороны, они позволяют доказывать больше вещей.
Одной из причин того, что существует много разных типов — это желание ученых сделать больше, не отказываясь от возможности доказывать сильные теоремы лямбда-исчислений.
Вам будет интересно: Семейный этикет: основы и правила, особенности отношений с близкими родственниками
Система находит применение во многих различных областях математики, философии, лингвистики, и компьютерных наук. В первую очередь, лямбда-исчисления — это расчет, который сыграл важную роль в развитии теории языков программирования. Именно стили функционального создания реализуют системы. Они также являются актуальной темой исследований в теории этих категорий.
Для чайников
Лямбда-исчисление была введена математиком Алонзо Черчем в 1930-х годах в рамках исследования основ науки. Первоначальная система была показана как логически несовместимая в 1935 году, когда Стивен Клин и Дж. Б. Россер разработали парадокс Клини-Россера.
В последствии, в 1936 году Черч выделил и опубликовал только ту часть, которая имеет отношение к расчетам, то, что сейчас называется нетипизированным лямбда-исчислением. В 1940 он также представил более слабую, но логически непротиворечивую теорию, известную как система простого типа. В свое работе он объясняет всю теорию простым языком, поэтому, можно сказать, что Черч опубликовал лямбду исчисления для чайников.
Вам будет интересно: Профессии железнодорожников: перечень, описание, необходимое образование
До 1960-х годов, когда выяснилось его отношение к языкам программирования, λ стала лишь формализмом. Благодаря применениям Ричарда Монтегю и других лингвистов в семантике естественного языка, исчисление стало занимать почетное место как в лингвистике, так и в информатике.
Происхождение символа
Лямбда не обозначает слово или аббревиатуру, она возникла, благодаря ссылки в «Принципиальной математике» Рассела, за которой следуют два типографских изменения. Пример обозначения: для функции f с f (y) = 2y + 1 равно 2ŷ + 1. И здесь используется символ каретки («шляпа») над y для пометки входной переменной.
Церковь изначально намеревалась использовать аналогичные символы, но наборщики не смогли разместить символ «шляпа» над буквами. Поэтому вместо этого они напечатали его изначально как «/y.2y+1». В следующем эпизоде редактирования наборщики заменили «/ » на визуально похожий символ.
Введение в лямбда исчисление
Система состоит из языка терминов, которые выбираются определенным формальным синтаксисом, и набора правил преобразования, которые позволяют манипулировать ими. Последний пункт можно рассматривать как эквациональную теорию или как операционное определение.
Все функции в лямбда-исчислении являются анонимными, то есть не имеющими имен. Они принимают только одну входную переменную, при этом каррирование используется для реализации графиков с несколькими непостоянными.
Лямбда-термины
Синтаксис исчисления определяет некоторые выражения как допустимые, а другие — как недействительные. Также, как различные строки символов являются допустимыми программами на Си, а какие-то — нет. Действительное выражение лямбда-исчисления называется «лямбда-термином».
Следующие три правила дают индуктивное определение, которое можно применять для построения всех синтаксически допустимых понятий:
Переменная x сама по себе является действительным лямбда-термином:
Ничто другое не является лямбда-термином. Таким образом, понятие действительно тогда и только тогда, когда оно может быть получено повторным применением этих трех правил. Тем не менее некоторые скобки могут быть опущены в соответствии с другими критериями.
Определение
Вам будет интересно: Виды контроля качества продукции при производстве
Лямбда-выражения состоят из:
Множество Λ, может быть определено индуктивно:
Обозначение
Чтобы сохранить нотацию лямбда-выражений в незагроможденном виде, обычно применяются следующие соглашения:
Свободные и связанные переменные
Оператор λ соединяет свою непостоянную, где бы он ни находился в теле абстракции. Переменные, попадающие в область, называются связанными. В выражении λ x. М, часть λ х часто называют связующим. Как бы намекая, что переменные становятся группой с добавлением Х х к М. Все остальные неустойчивые называются свободными.
Множество свободных переменных M обозначается как FV (M) и определяется рекурсией по структуре терминов следующим образом:
Формула, которая не содержит свободных переменных, называется закрытой. Замкнутые лямбда-выражения также известны как комбинаторы и эквивалентны терминам в комбинаторной логике.
Сокращение
Значение лямбда-выражений определяется тем, как они могут быть сокращены.
Существует три вида урезания:
Здесь речь также идет о полученных эквивалентностях: два выражения являются β-эквивалентными, если они могут быть β-преобразованы в одно и то же составляющее, а α / η-эквивалентность определяется аналогично.
Термин redex, сокращение от приводимого оборота, относится к подтемам, которые могут быть сокращены одним из правил. Лямбда исчисление для чайников, примеры:
(λ x.M) N является бета-редексом в выражении замены N на x в M. Составляющее, к которому сводится редекс, называется его редуктом. Редукция (λ x.M) N есть M [x: = N].
Если x не является свободной в M, λ х. М х также ет-REDEX с регулятором М.
α-преобразование
Альфа-переименования позволяют изменять имена связанных переменных. Например, λ x. х может дать λ у. у. Термины, которые отличаются только альфа-преобразованием, называются α-эквивалентными. Часто при использовании лямбда-исчисления α-эквивалентные считаются взаимными.
Точные правила для альфа-преобразования не совсем тривиальны. Во-первых, при данной абстракции переименовываются только те переменные, которые связаны с одной и той же системой. Например, альфа-преобразование λ x.λ x. x может привести к λ y.λ x. х, но это может не ввергнуть к λy.λx.y Последний имеет иной смысл, чем оригинал. Это аналогично понятию программирования затенения переменных.
Во-вторых, альфа-преобразование невозможно, если оно приведет к захвату непостоянной другой абстракцией. Например, если заменить x на y в λ x.λ y. x, то можно получить λ y.λ y. у, что совсем не то же самое.
В языках программирования со статической областью видимости альфа-преобразование можно использовать для упрощения разрешения имен. При этом следя за тем, чтобы понятие переменной не маскировало обозначение в содержащей области.
В нотации индекса Де Брюйна любые два альфа-эквивалентных термина синтаксически идентичны.
Замена
y [x: = N] ≡ y, если x ≠ y
(M 1 M 2) [x: = N] ≡ (M 1 [x: = N]) (M 2 [x: = N])
(λ y.M) [x: = N] y λ y. (M [x: = N]), если x ≠ y, при условии, что y ∉ FV (N).
Для подстановки в лямбда-абстракцию иногда необходимо α-преобразовать выражение. Например, неверно, чтобы (λ x. Y) [y: = x] приводило к (λ x. X), потому что замещенный x должен был быть свободным, но в итоге был связанным. Правильная замена в этом случае (λ z. X) с точностью до α-эквивалентности. Стоит обратить внимание, что замещение определяется однозначно с верностью до лямбды.
β-редукция
Бета-редукция отражает идею применения функции. Бета-восстановительный определяется в терминах замещения: ((X V. E) Е ‘) является Е [V: = Е’].
Например, предполагая некоторое кодирование 2, 7, ×, имеется следующее β-уменьшение: ((λ n. N × 2) 7) → 7 × 2.
Бета-редукция может рассматриваться как то же самое, что и концепция локальной сводимости при естественной дедукции через изоморфизм Карри – Ховарда.
η-преобразование
Эта-конверсия выражает идею экстенсиональности, которая в этом контексте заключается в том, что две функции равны тогда, когда они дают одинаковый результат для всех аргументов. Эта конвертация обменивает между λ x. (F x) и f всякий раз, когда x не кажется свободным в f.
Вам будет интересно: Откуда появились славяне: определение, описание и история
Данное действие может рассматриваться как то же самое, что и концепция локальной полноты в естественной дедукции через изоморфизм Карри – Ховарда.
Нормальные формы и слияние
Для нетипизированного лямбда-исчисления β-редукция как правило переписывания не является ни сильно нормализующей, ни слабо.
Тем не менее можно показать, что β-редукция сливается при работе до α-преобразования (т. е. можно считать две нормальные формы равными, если возможно α-преобразование одной в другую).
Поэтому и сильно нормализующие члены, и слабо налаживающие понятия имеют единственную нормальную форму. Для первых терминов любая стратегия сокращения гарантированно приведет к типичной конфигурации. Тогда как для слабо нормализующих условий некоторые стратегии сокращения могут не найти ее.
Дополнительные методы программирования
Существует большое количество идиом создания для лямбда-исчисления. Многие из них были первоначально разработаны в контексте использования систем в качестве основы для семантики языка программирования, эффективно применяя их в качестве создания низкого уровня. Поскольку некоторые стили включают лямбда-исчисление (или что-то очень похожее) в качестве фрагмента, эти методы также находят применение в практическом создании, но затем могут восприниматься как неясные или чужие.
Именованные константы
В лямбда-исчислении библиотека принимает форму набора ранее определенных функций, в которой термины являются просто конкретными константами. Чистое исчисление не имеет понятия именованных неизменных, поскольку все атомные лямбда-термины являются переменными. Но их также можно имитировать, выделив непостоянную в качестве имени константы, используя лямбда-абстракцию для связывания этой изменчивой в основной части, и применить эту абстракцию к намеченному определению. Таким образом, если использовать f для обозначения M в N, можно сказать,
Авторы часто вводят синтаксическое понятие, такое как let, чтобы разрешить писать все в более интуитивном порядке.
Объединяя в цепочку такие определения, можно написать «программу» лямбда-исчисления как ноль или более дефиниций функций, за которыми следует один лямбда-член, используя те определения, которые составляют основную часть программы.
Заметным ограничением этого let является то, что имя f не определено в M, поскольку M находится вне области привязки лямбда-абстракции f. Это означает, что атрибут рекурсивной функции не может использоваться как M с let. Более продвинутая синтаксическая конструкция letrec, которая позволяет писать рекурсивные определения функций в этом стиле, вместо этого дополнительно использует комбинаторы с фиксированной точкой.
Печатные аналоги
Данный тип является типизированным формализмом, который использует символ для обозначения анонимной функции абстракция. В этом контексте типы обычно являются объектами синтаксической природы, которые присваиваются лямбда-терминам. Точная натура зависит от рассматриваемого исчисления. С определенной точки зрения, типизированные ЛИ можно рассматривать как уточнения нетипизированного ЛИ. Но с другой стороны, их также можно считать более фундаментальной теорией, а нетипизированное лямбда-исчисление — особым случаем только с одним типом.
Типизированные ЛИ являются основополагающими языками программирования и основой функциональных, таких как ML и Haskell. И, более косвенно, императивных стилей создания. Типизированные лямбда-исчисления играют важную роль в разработке систем типов для языков программирования. Здесь типизируемость обычно захватывает желательные свойства программы, например, она не вызовет нарушения доступа к памяти.
Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри – Говарда, и их можно рассматривать как внутренний язык классов категорий, например, который просто является стилем декартовых замкнутых.
Лямбда-исчисление состоит из построения лямбда-членов и выполнения над ними операций редукции. В простейшей форме лямбда-исчисления термины строятся с использованием только следующих правил:
Операции восстановления включают:
СОДЕРЖАНИЕ
Объяснение и приложения
История
До 1960-х годов, когда было выяснено его отношение к языкам программирования, лямбда-исчисление было всего лишь формализмом. Благодаря приложениям Ричарда Монтегю и других лингвистов к семантике естественного языка лямбда-исчисление стало занимать почетное место как в лингвистике, так и в информатике.
Происхождение символа лямбда
Существует некоторая неопределенность в отношении причины использования Черчем греческой буквы лямбда (λ) в качестве обозначения абстракции функции в лямбда-исчислении, возможно, частично из-за противоречивых объяснений самого Черча. Согласно Кардоне и Хиндли (2006):
Об этом происхождении также сообщалось в [Россер, 1984, с.338]. С другой стороны, в последние годы своей жизни Черч сказал двум вопрошающим, что выбор был более случайным: нужен был символ и просто случайно был выбран λ.
Дана Скотт также обращалась к этому вопросу в различных публичных лекциях. Скотт вспоминает, что однажды он задал вопрос о происхождении лямбда-символа зятю Черча Джону Аддисону, который затем написал своему тестю открытку:
По словам Скотта, весь ответ Черча состоял в том, чтобы вернуть открытку со следующей пометкой : « Ини, миини, мини, мо ».
Неформальное описание
Мотивация
можно переписать в анонимной форме как
можно переписать в анонимной форме как
где ввод просто сопоставляется сам с собой.
Второе упрощение состоит в том, что лямбда-исчисление использует только функции одного входа. Обычная функция, для которой требуются два входа, например, функция, может быть преобразована в эквивалентную функцию, которая принимает один вход, а при выходе возвращает другую функцию, которая, в свою очередь, принимает один вход. Например, s q ты а р е _ s ты м <\ textstyle \ operatorname <квадрат \ _sum>> 
может быть переработан в
Функция применения в функции аргументов (5, 2), дает сразу s q ты а р е _ s ты м <\ textstyle \ operatorname <квадрат \ _sum>>
тогда как оценка каррированной версии требует еще одного шага
чтобы прийти к тому же результату.
Лямбда-исчисление
Как описано выше, все функции в лямбда-исчислении являются анонимными функциями, не имеющими имен. Они принимают только одну входную переменную, а каррирование используется для реализации функций с несколькими переменными.
Лямбда-термины
Следующие три правила дают индуктивное определение, которое можно применять для построения всех синтаксически правильных лямбда-терминов:
Ничто иное не является лямбда-термином. Таким образом, лямбда-член действителен тогда и только тогда, когда он может быть получен повторным применением этих трех правил. Однако некоторые скобки можно опустить по определенным правилам. Например, крайние круглые скобки обычно не пишутся. См. Обозначения ниже.
Функции, которые работают с функциями
В лямбда-исчислении функции считаются « значениями первого класса », поэтому функции могут использоваться в качестве входных данных или возвращаться в качестве выходных данных из других функций.
Существует несколько понятий «эквивалентности» и «редукции», которые позволяют «свести» лямбда-термины к «эквивалентным» лямбда-членам.
Альфа-эквивалентность
Для определения β-редукции необходимы следующие определения:
Бесплатные переменные
Замены с избеганием захвата
β-редукция
Формальное определение
Определение
Лямбда-выражения состоят из:
Набор лямбда-выражений Λ можно определить индуктивно :
Обозначение
Чтобы не загромождать нотацию лямбда-выражений, обычно применяются следующие соглашения:
Свободные и связанные переменные
Набор свободных переменных лямбда-выражения M обозначается как FV ( M ) и определяется рекурсией по структуре терминов следующим образом:
Снижение
Значение лямбда-выражений определяется тем, как выражения могут быть сокращены.
Есть три вида сокращения:
α-преобразование
В обозначении индекса Де Брёйна любые два α-эквивалентных термина синтаксически идентичны.
Замена
β-редукция
η-редукция
Нормальные формы и слияние
Однако можно показать, что β-восстановление сливается при работе до α-преобразования (т. Е. Мы считаем две нормальные формы равными, если возможно α-преобразовать одну в другую).
Следовательно, как сильно нормализующие члены, так и слабо нормализующие члены имеют единственную нормальную форму. Для строго нормализующих членов любая стратегия редукции гарантированно дает нормальную форму, тогда как для слабо нормализующих членов некоторые стратегии редукции могут не найти ее.
Кодирование типов данных
Арифметика в лямбда-исчислении
и так далее. Или используя альтернативный синтаксис, представленный выше в Обозначении :
Изменяя то, что повторяется, и варьируя аргумент, к которому применяется эта повторяющаяся функция, можно достичь множества различных эффектов.
PLUS можно рассматривать как функцию, принимающую в качестве аргументов два натуральных числа и возвращающую натуральное число; можно проверить, что
являются β-эквивалентными лямбда-выражениями. Поскольку прибавление m к числу n может быть выполнено добавлением 1 m раз, альтернативное определение:
Точно так же умножение можно определить как
Логика и предикаты
По соглашению для логических значений ИСТИНА и ЛОЖЬ используются следующие два определения (известные как логические значения Черча) :
Затем с помощью этих двух лямбда-терминов мы можем определить некоторые логические операторы (это всего лишь возможные формулировки; другие выражения также верны):
Теперь мы можем вычислять некоторые логические функции, например:
Следующий предикат проверяет, меньше ли первый аргумент второму или равен ему:
Доступность предикатов и приведенное выше определение ИСТИНА и ЛОЖЬ делают удобной запись выражений «если-то-иначе» в лямбда-исчислении. Например, функцию-предшественницу можно определить как:
что позволяет нам дать, пожалуй, наиболее прозрачную версию функции-предшественника:
PRED: = λ n. ПЕРВЫЙ ( n Φ (PAIR 0 0)).
Дополнительные техники программирования
Именованные константы
Объединив такие определения, можно написать «программу» лямбда-исчисления как ноль или более определений функций, за которыми следует один лямбда-член, использующий те функции, которые составляют основную часть программы.
Рекурсия и фиксированные точки
Рассмотрим факториальную функцию F ( n ), рекурсивно определяемую формулой
Самоприложение выполняет здесь репликацию, передавая лямбда-выражение функции следующему вызову в качестве значения аргумента, делая его доступным для ссылки и вызова.
Это решает проблему, но требует перезаписи каждого рекурсивного вызова как самостоятельного приложения. Мы хотели бы иметь общее решение без необходимости переписывать:
Стандартные условия
У некоторых терминов есть общепринятые названия:
Устранение абстракции
Типизированное лямбда-исчисление
Стратегии сокращения
Является ли термин нормализующим или нет, и сколько работы необходимо сделать для его нормализации, если это так, в значительной степени зависит от используемой стратегии сокращения. Общие стратегии сокращения лямбда-исчисления включают:
Слабые стратегии сокращения не сводятся к лямбда-абстракциям:
Стратегии с совместным использованием сокращают количество параллельных вычислений, которые «одинаковы»:
Оптимальное сокращение В обычном порядке, но вычисления с одинаковой меткой сокращаются одновременно. Звоните по необходимости Как вызов по имени (следовательно, слабый), но приложения-функции, которые будут дублировать термины, вместо этого называют аргумент, который затем сокращается только «тогда, когда это необходимо».
Вычислимость
Сложность
Необоснованная модель не обязательно означает неэффективность. Оптимальное сокращение сокращает все вычисления с одной и той же меткой за один шаг, избегая дублирования работы, но количество параллельных шагов β-редукции для приведения данного члена к нормальной форме приблизительно линейно по размеру члена. Это слишком мало, чтобы быть разумной мерой затрат, поскольку любая машина Тьюринга может быть закодирована в лямбда-исчислении в размере, линейно пропорциональном размеру машины Тьюринга. Истинная стоимость сокращения лямбда-членов связана не с β-редукцией как таковой, а с обработкой дублирования редексов во время β-редукции. Неизвестно, являются ли оптимальные реализации сокращения разумными при измерении относительно разумной модели затрат, такой как количество крайних левых шагов к нормальной форме, но для фрагментов лямбда-исчисления было показано, что алгоритм оптимального сокращения эффективен. и имеет не более чем квадратичные накладные расходы по сравнению с крайним левым. Вдобавок реализация оптимального сокращения прототипа BOHM превзошла Caml Light и Haskell по чистым лямбда-терминам.
Лямбда-исчисление и языки программирования
Как указано в статье Питера Ландина 1965 года «Соответствие между АЛГОЛОМ 60 и лямбда-нотацией Черча», последовательные процедурные языки программирования можно понимать в терминах лямбда-исчисления, которое обеспечивает основные механизмы процедурной абстракции и процедуры (подпрограммы) заявление.
Анонимные функции
Например, в Лиспе «квадратная» функция может быть выражена как лямбда-выражение следующим образом:
Параллелизм и параллелизм
Семантика
В 1970-х Дана Скотт показала, что, если бы рассматривались только непрерывные функции, можно было бы найти набор или область D с требуемым свойством, тем самым предоставив модель лямбда-исчисления.
Эта работа также легла в основу денотационной семантики языков программирования.
Варианты и расширения
Эти расширения находятся в лямбда-кубе :
Эти формальные системы являются расширениями лямбда-исчисления, которых нет в лямбда-кубе:
Эти формальные системы представляют собой разновидности лямбда-исчисления:
Эти формальные системы связаны с лямбда-исчислением:
Смотрите также
Примечания
использованная литература
дальнейшее чтение
Монографии / учебники для аспирантов: