Оглавление [Скрыть]
- 1 Лямбда-исчисление
- 1.1 История и происхождение
- 1.2 Основные понятия
- 1.3 Лямбда-термины и абстракции
- 1.4 Применение и приложения
- 1.5 Происхождение символа λ
- 1.6 Функциональное применение
- 1.7 Определение функций с помощью лямбда-терминов
- 1.8 Примеры лямбда-терминов
- 1.9 Функции, работающие с функциями
- 1.10 Эквивалентность и редукция лямбда-терминов
- 1.11 β-редукция
- 1.12 Формальное определение лямбда-выражений
- 1.13 Обозначение лямбда-выражений
- 1.14 Свободные и связанные переменные
- 1.15 Сокращение лямбда-выражений
- 1.16 α-преобразование
- 1.17 Подстановка
- 1.18 β-редукция
- 1.19 η-сокращение
- 1.20 Нормальные формы и слияние
- 1.21 Кодирование типов данных
- 1.22 Арифметика в лямбда-исчислении
- 1.23 Логика и предикаты
- 1.24 Предикаты и выражения “если-то-еще”
- 1.25 Пары и связанные списки
- 1.26 Дополнительные методы программирования
- 1.27 Рекурсия и фиксированные точки
- 1.28 Стандартные условия и устранение абстракции
- 1.29 Типизированное лямбда-исчисление
- 1.30 Стратегии сокращения выбросов
- 1.31 Вычислимость
- 1.32 Определение вычислимости через лямбда-исчисление
- 1.33 Сложность лямбда-исчисления
- 1.34 Лямбда-исчисление и языки программирования
- 1.35 Семантика лямбда-исчисления
- 1.36 Вариации и расширения лямбда-исчисления
- 1.37 Связанные темы
- 1.38 Описание артикула
- 1.39 Идентификаторы и блоки
- 1.40 Оформление и стили
- 1.41 Библиографическое описание
- 1.42 Дополнительные ресурсы
- 1.43 Полный текст статьи:
- 2 Лямбда-исчисление
Лямбда-исчисление
-
История и происхождение
- Лямбда-исчисление введено Алонсо Черчем в 1930-х годах.
- В 1936 году Черч выделил нетипизированное лямбда-исчисление.
- В 1940 году Черч представил просто типизированное лямбда-исчисление.
-
Основные понятия
- Лямбда-исчисление — формальная система для выражения вычислений.
- Лямбда-термины строятся с использованием переменных, лямбда-абстракций и приложений.
- Операции сокращения включают α-преобразование и β-редукцию.
-
Лямбда-термины и абстракции
- Лямбда-термины определяются формальным синтаксисом.
- Лямбда-абстракция — это определение функции, принимающей один входной сигнал.
- Лямбда-термины могут быть расширены арифметическими операциями.
-
Применение и приложения
- Лямбда-исчисление используется в математике, философии, лингвистике и компьютерных науках.
- Лямбда-исчисление играет важную роль в теории языков программирования и теории категорий.
-
Происхождение символа λ
- Черч выбрал символ λ для обозначения функциональной абстракции.
- Происхождение символа остается предметом споров.
-
Функциональное применение
- Лямбда-исчисление упрощает семантику вычислений.
- Функции обрабатываются анонимно и принимают только один входной сигнал.
- Каррирование используется для реализации функций нескольких переменных.
-
Определение функций с помощью лямбда-терминов
- Лямбда-термины связывают переменные с терминами.
- Определение функции с помощью лямбда-терминов настраивает функцию, но не вызывает её.
- Приложение функции к входным данным представляет действие вызова функции.
-
Примеры лямбда-терминов
- Пример 1: λx.B определяет функцию, которая добавляет входные данные к неизвестному y.
- Пример 2: M N применяет функцию M к входным данным N.
-
Функции, работающие с функциями
- Функции в лямбда-исчислении считаются “значениями первого класса”.
- Пример: λx.y представляет постоянную функцию, которая всегда возвращает y.
- Композиция функций может быть определена как λf.λg.λx.(f(gx)).
-
Эквивалентность и редукция лямбда-терминов
- Альфа-эквивалентность: λx.x и λy.y представляют одну и ту же функцию.
- Свободные переменные: переменные, не связанные абстракцией.
- Подстановки: замена переменных в лямбда-терминах.
-
β-редукция
- Правило β-сокращения: (λx.t)s → t[x:=s].
- Примеры: (λx.x)s → s, (λx.y)s → y.
- Лямбда-исчисление может не завершиться, как в примере Ω.
-
Формальное определение лямбда-выражений
- Лямбда-выражения состоят из переменных, абстрактных символов λ и ., круглых скобок.
- Набор лямбда-выражений Λ определяется индуктивно.
-
Обозначение лямбда-выражений
- Удаляются крайние круглые скобки
- Приложения считаются левоассоциативными
- Пробел в приложениях опускается, если все переменные состоят из одной буквы
- Основная часть абстракции простирается вправо
- Последовательность абстракций сокращается
-
Свободные и связанные переменные
- Оператор абстракции λ связывает переменные в теле абстракции
- Связанные переменные входят в область абстракции
- Свободные переменные не входят в область абстракции
- Набор свободных переменных обозначается как FV(M)
-
Сокращение лямбда-выражений
- α-преобразование изменяет связанные переменные
- β-редукция применяет функции к аргументам
- η-сокращение отражает расширяемость
-
α-преобразование
- Переименовывает связанные переменные
- Не может привести к захвату переменной другой абстракцией
- Используется для упрощения разрешения имен
-
Подстановка
- Замена свободных вхождений переменной на выражение
- Определяется рекурсией структуры терминов
- Может привести к α-эквивалентности
-
β-редукция
- Отражает идею функционального применения
- Определяется через подстановку
- Можно рассматривать как локальную сводимость
-
η-сокращение
- Выражает идею расширяемости
- Преобразует λx.fx в f, если x не свободен в f
- Можно рассматривать как локальную полноту
-
Нормальные формы и слияние
- β-редукция не является сильно или слабо нормализующей
- β-восстановление непрерывно при α-преобразовании
- Сильно нормализующие термины имеют уникальную нормальную форму
-
Кодирование типов данных
- Лямбда-исчисление используется для моделирования арифметики, логики, структур данных и рекурсии
-
Арифметика в лямбда-исчислении
- Церковные числительные определяются как функции более высокого порядка
- Сложение и умножение определяются через повторяющиеся композиции
- Возведение в степень и предыдущая функция определяются через индукцию
-
Логика и предикаты
- Логические значения TRUE и FALSE определяются как функции
- Логические операторы определяются через лямбда-термины
- Предикаты, такие как ISZERO и LEQ, используются для проверки условий
-
Предикаты и выражения “если-то-еще”
- Предикаты TRUE и FALSE упрощают написание выражений типа “если-то-еще”.
- Функция-предшественница может быть определена индуктивно.
-
Пары и связанные списки
- Пара (2-кортеж) определяется через TRUE и FALSE.
- Связанный список может быть определен как NIL или пара элемента и списка меньшего размера.
- Предикат NULL проверяет наличие NIL.
-
Дополнительные методы программирования
- Существует множество идиом программирования для лямбда-исчисления.
- Именованные константы имитируются с помощью абстракции.
-
Рекурсия и фиксированные точки
- Рекурсия в лямбда-исчислении требует использования комбинатора FIX.
- FIX возвращает самовоспроизводящееся лямбда-выражение.
-
Стандартные условия и устранение абстракции
- Некоторые термины имеют общепринятые названия.
- Функция преобразования T удаляет абстракцию из лямбда-терминов.
-
Типизированное лямбда-исчисление
- Типизированное лямбда-исчисление использует лямбда-символ для обозначения абстракции.
- Типизированные лямбда-вычисления важны для разработки систем типов.
-
Стратегии сокращения выбросов
- Нормализация терминов зависит от используемой стратегии сокращения.
- Слабые стратегии сокращения не приводят к сокращению при лямбда-абстракциях.
-
Вычислимость
- Не существует алгоритма для определения сводимости двух лямбда-выражений.
- Вычислимость означает вычислимость с помощью любой модели вычислений, полной по Тьюрингу.
-
Определение вычислимости через лямбда-исчисление
- Функция F: N → N является вычислимой, если существует лямбда-выражение f, такое, что f x =βy для всех x и y в N.
- Доказательство невычислимости Черча основано на определении нормальной формы лямбда-выражений.
-
Сложность лямбда-исчисления
- Стоимость β-редукции зависит от реализации.
- Наивный поиск местоположения переменных требует O(n) времени.
- Директорные строки и явная замена улучшают производительность.
- Оптимальное сокращение сокращает вычисления за один шаг, но требует линейного времени.
-
Лямбда-исчисление и языки программирования
- Лямбда-исчисление предоставляет базовые механизмы для процедурной абстракции.
- Анонимные функции, такие как лямбда-выражения, используются в Python и других языках.
- Параллелизм и совместимость поддерживаются лямбда-исчислением, но не явными конструкциями.
-
Семантика лямбда-исчисления
- Лямбда-термины действуют как функции на другие термины и на себя.
- Дана Скотт показала, что непрерывные функции могут быть использованы для создания модели лямбда-исчисления.
-
Вариации и расширения лямбда-исчисления
- Типизированное лямбда-исчисление, System F, исчисление конструкций.
- Двоичное лямбда-исчисление, лямбда-мю-исчисление, каппа-исчисление.
- Комбинаторная логика, SKI combinator calculus.
-
Связанные темы
- Математический портал, прикладные вычислительные системы.
- Декартова замкнутая категория, категориальная абстрактная машина.
- Clojure, изоморфизм Карри-Говарда, индекс Де Брейна.
- Теория предметной области, стратегия вычисления, явная подстановка.
- Формула Харропа, сети взаимодействия, парадокс Клини-Россера.
- Рыцари лямбда-исчисления, Krivine machine, определение лямбда-исчисления.
- Пусть выражение, минимализм, переписывание, SECD machine.
- Теорема Скотта-Карри, чтобы поиздеваться над пересмешником, универсальная машина Тьюринга.
- Unlambda, функциональный эзотерический язык программирования.
-
Описание артикула
- Артикул MW-парсер-выход используется для цитирования и оформления цитат.
- Включает различные стили и цвета для цитат и идентификаторов.
-
Идентификаторы и блоки
- Идентификаторы включают различные типы блокировок, такие как “бесплатно”, “общество”, “регистрация” и “подписка”.
- Блокировки имеют различные цвета и размеры.
-
Оформление и стили
- Включает различные стили для оформления цитат и идентификаторов.
- Используются различные цвета и размеры для различных элементов.
-
Библиографическое описание
- Включает ссылки на книги и статьи по лямбда-исчислению.
- Упоминаются ключевые авторы и их работы.
-
Дополнительные ресурсы
- Включает ссылки на видео, учебные пособия и графические материалы.
- Упоминаются различные реализации лямбда-исчисления и его применение.