Лямбда-исчисление

• Курс посвящен функциональному программированию.  

• Обсуждение лямбда-исчисления и его отличия от императивного программирования.  

• План лекции: теория, содержательный материал.  

• Взаимодействие с вычислителем через инструкции.  

• Изменение состояния вычислителя через инструкции.  

• Основные инструкции: присваивание, ветвление, циклы.  

• Инструкции выполняются последовательно.  

• Программы требуют удержания состояния в голове.  

• Примеры языков программирования, работающих в рамках императивной парадигмы.  

• Описание скалярного произведения двухмерных векторов.  

• Использование цикла для перемножения элементов и обновления состояния.  

• Программа развивается через последовательные состояния.  

• Функциональная программа как выражение.  

• Вычисление выражения без изменения состояния.  

• Отсутствие изменяемых переменных, присваиваний и циклов.  

• Рекурсия и функции высших порядков.  

• Простота описания семантики программы.  

• Свобода при исполнении и возможность распараллеливания.  

• Проблемы с вводом-выводом и быстродействием.  

• Необходимость специальной прослойки для выполнения функциональных программ.  

• Современные императивные языки также используют виртуальные машины.  

• Пример кода на языке Си, иллюстрирующий проблемы с глобальными переменными.  

• Функция "тест" инициализирует значение флага и вызывает функцию "ф" четыре раза.  

• Функция "ф" умножает возвращаемое значение на два в зависимости от значения флага и переключает флаг.  

• Функция "ф" не является чистой, так как зависит от глобального состояния.  

• В императивном программировании такие функции приводят к потере вариантов и ссылочной прозрачности.  

• В функциональном программировании чистые функции предпочтительнее, но нечистые функции также допустимы.  

• Лямбда-исчисление является основой функционального программирования.  

• Оно было разработано для формализации понятия вычислимости и анализа вычислительных процессов.  

• Лямбда-исчисление имеет бес типовые и типизированные версии и позволяет описывать свойства вычислительных процессов.  

• Применение функции к аргументу обозначается как "ф икс".  

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

• Лямбда-выражения определяют функции, которые сопоставляют каждому значению аргумента соответствующее значение выражения.  

• Лямбда-функция представляет собой неименованную функцию.  

• Применение лямбда-функции к числу семнадцать подставляет это число вместо переменной икс.  

• Лямбда-функция исчезает после применения, оставляя результат.  

• Лямбда-терм подставляется вместо иксов в выражении.  

• В лямбда-исчислении умножение не принадлежит лямбда-исчислению, поэтому используется другое правило.  

• Дельта-равенство будет обсуждаться в конце лекции.  

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

• Подстановка заменяет иксы на выражения.  

• В функциональном программировании отсутствуют изменяемые переменные.  

• Лямбда-термы строятся индуктивно, начиная с переменных.  

• Применение и абстракция также являются лямбда-термами.  

• Лямбда-термы могут быть заключены в скобки для ясности.  

• Переменная икс является лямбда-термом.  

• Применение переменной к другой переменной также является лямбда-термом.  

• Абстракция по переменной икс создает новый лямбда-терм.  

• Внешние скобки можно опускать.  

• Применение ассоциативно влево.  

• Лямбда-абстракция простирается вправо, насколько это возможно.  

• Примеры показывают, как можно опустить избыточные скобки.  

• Лямбда-абстракция применяется к игреку, что требует скобок.  

• Опускание скобок делает выражения более читабельными.  

• Переменные делятся на свободные и связанные.  

• Связанные переменные локальны для выражения.  

• Свободные переменные видны снаружи и могут быть заменены.  

• Пример с лямбда-термом показывает, как переменные становятся связанными.  

• Связывание происходит при написании лямбды.  

• Пример с функцией показывает, как аргументы становятся связанными.  

• Пример с тремя переменными показывает коллизии связанных переменных.  

• Переменные могут быть связаны несколько раз.  

• Свободные переменные остаются свободными, даже если они внутри выражения.  

• Свободные переменные видны снаружи и могут быть заменены.  

• Связанные переменные локальны для выражения.  

• Определение множества свободных переменных через индукцию.  

• Комбинатор — это замкнутый термин без свободных переменных.  

• Комбинаторы описывают функции, которые не зависят от внешних переменных.  

• Комбинаторы можно рассматривать как синтаксическую замену.  

• Комбинатор адент возвращает аргумент без изменений.  

• Комбинатор омега-маленькая абстрагируется по аргументу и применяет его к себе.  

• Комбинатор омега-большая применяется к самому себе и обладает смешными свойствами.  

• Комбинатор к возвращает первый аргумент из двух.  

• Комбинатор ка возвращает второй аргумент из двух.  

• Комбинаторы с и б также важны для дальнейшего изучения.  

• Комбинатор b описывает композицию двух функций f и g.  

• Комбинатор принимает три аргумента: две функции и икс.  

• Комбинатор c более сложен: функция f принимает два аргумента и применяется к иксу и результату применения g к иксу.  

• Комбинаторы k и c достаточны для построения тьюринг-полной системы.  

• Эти комбинаторы позволяют описать все вычисления, которые можно выполнить на машине Тьюринга.  

• Существует однокомбиаторный базис, но он не рассматривается в данном контексте.  

• Все функции в лямбда-исчислении являются функциями одной переменной.  

• Комбинатор k можно представить как лямбда-функцию, которая ожидает аргумент икс.  

• Применение комбинатора к значениям приводит к подстановке значений вместо икса.  

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

• Анкарирование — обратный процесс, который возвращает функцию с последовательным скармливанием аргументов.  

• Корирование названо в честь Хаскелла Карри, но придумано Шафинки.  

• Имена связанных переменных не важны.  

• Можно заменить все вхождения переменной на другую переменную.  

• Это преобразование не портит терм, так как переменная используется только в применении функции.  

• Пример с лямбда-выражением: замена всех вхождений икса на игрек.  

• Преобразование не меняет результат применения функции.  

• Это обобщается на более сложные термы.  

• Введение понятия альфа-эквивалентности.  

• Переход к формальному определению подстановки.  

• Подстановка: замена переменной на терм.  

• Рассматриваются три случая: переменная, лямбда-терм, аппликация.  

• Если терм м - переменная, результат подстановки - терм н.  

• Если терм м - другая переменная, подстановка не требуется.  

• Подстановка в аппликацию: замена в п и ку, затем применение.  

• Лямбда-абстракция: замена вхождений икса на н.  

• Если переменная лямбда-абстракции не совпадает с переменной подстановки, замена в п.  

• Коллизия переменных: обсуждение позже.  

• Подстановка осуществляется только для свободных вхождений переменной.  

• В терме п не может быть свободных вхождений икса, поэтому подстановка не меняет термин.  

• Подстановка как рефакторинг: переименование функции.  

• Замена свободных переменных в функциях.  

• Пример с функцией, где переменная "синус" используется в теле функции.  

• Замена переменных в теле функции не требуется.  

• Замена строк на выражения может вызвать проблемы.  

• Пример с заменой "синуса" на "косинус".  

• Важно, чтобы выражение имело смысл в контексте.  

• Пример с лямбда-термом, где икс присутствует трижды.  

• Замена свободного вхождения икса на выражение.  

• Связанные вхождения не подлежат замене.  

• Пример с термом, где икс и игрек являются свободными переменными.  

• Захват переменных при подстановке.  

• Важно, чтобы свободные переменные оставались свободными.  

• Альфа-преобразование для эквивалентных термов.  

• Правило, что связанная переменная не должна быть свободной в подставляемом термине.  

• Соглашение о различении связанных и свободных переменных.  

• Свободные переменные как интерфейс с внешним миром.  

• Связанные переменные доступны только внутри лямбда-абстракции.  

• Соглашение Баррета позволяет избежать проблем при вычислениях.  

• Обсуждение основной схемы аксиом лямбда-исчисления.  

• Введение бета-преобразования: замена лямбды на эквивалентное выражение.  

• Введение вычислительного действия для выполнения бета-преобразования.  

• Введение рефлексивности, симметричности и транзитивности для отношения равенства.  

• Специфические правила для операций аппликации и абстракции.  

• Пример применения бета-преобразования к лямбда-термам.  

• Объяснение, как бета-преобразование работает с лямбда-термами.  

• Пример с лямбда-термом и его применением к аргументам.  

• Важность правил для вычислителя, который должен знать, как выполнять бета-преобразование.  

• Правила для выполнения бета-преобразования в левом и правом аппликадах.  

• Введение правила дзета для выполнения бета-преобразования внутри лямбда-абстракции.  

• Обсуждение редукций и правил, которым обучается вычислитель.  

• Введение альфа-преобразования и его запись на языке подстановки.  

• Условие, что игрек не должен быть свободен в м для выполнения альфа-преобразования.  

• Объяснение, почему альфа-преобразование всегда возможно.  

• Введение это-преобразования и его замена на м при отсутствии икса в м.  

• Объяснение, что эти два терма ведут себя одинаково в бета-преобразованиях.  

• Это-преобразование расширяет класс эквивалентных термов и имеет теоретическое значение.  

• Обсуждение соглашения Баррета и его выполнения.  

• Пример с термо-омегой и комбинатором единицы.  

• Применение альфа-преобразования для устранения коллизий.  

• Рассмотрение терма омега-единица.  

• Введение термина редокс и его использование.  

• Применение альфа-преобразования для устранения коллизий.  

• Возникновение коллизий при применении альфа-преобразования.  

• Переименование переменных для устранения коллизий.  

• Завершение вычислений и получение результата.  

• Введение индексов де Брауна для маркировки лямбда-термов.  

• Нумерация связанных переменных для устранения коллизий.  

• Преимущества и недостатки индексов де Брауна по сравнению с обычными лямбда-термами.  

• Обсуждение преобразования в лямбда-исчислении.  

• Принцип экстенсиональности: функции равны, если они дают одинаковый результат на всех возможных входах.  

• Преобразование позволяет доказать эквивалентность функций.  

• Правило дзета: если две функции равны, то их аргументы также равны.  

• Применение правила для доказательства равенства функций.  

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

• Преобразование в Haskell позволяет упростить запись функций.  

• Лямбда-исчисление рассматривается как вычислительная модель.  

• Цель - создать полноценный язык программирования на основе лямбда-исчисления.  

• Выполнение подстановок в лямбда-термах.  

• Правила подстановок и коллизии переменных.  

• Примеры подстановок и их применение.  

• Переименование связанных переменных для предотвращения коллизий.  

• Пример переименования и выполнения подстановки.  

• Завершение обсуждения подстановок и переименований.  

• Убираем лишние скобки и выполняем бета-преобразование.  

• Ищем редокс и выполняем его, если он найден.  

• Убираем внешние скобки и лямбда-тело.  

• Внутренние скобки в лямбда-выражении не убираем.  

• Лямбда-выражение применяется к двум аргументам.  

• Проверяем наличие редоксов.  

• Находим коллизии и устраняем их.  

• Объясняем, как возникают коллизии.  

• Проверяем, что лямбда-переменная не принадлежит свободным переменным.  

• Расписываем процесс подстановки.  

• Сначала пишем подстановку, затем ищем коллизии.  

• Коллизии возникают только при наличии лямбда-переменной.  

• Объясняем, откуда берутся лямбда-переменные.  

• Подстановка выполняется однократно.  

• Убираем лишние скобки и пишем зет-икс вместо зет.