https://funprog-ru.github.io/
Это пособие представляет собой конспект лекций по курсу Введение в функцио-
нальное программирование, который преподавался мной в университете Кембриджа
в 1996/7 учебном году.
Структура курса, в основе которой лежит чередование теории с практикой, со-
хранилась с прошлых лет в том виде, в котором она была предложена моим предше-
ственником Майком Гордоном. Его лекционные материалы [27, часть II] послужили
важным источником заимствований. Существенное влияние также оказали авторы
смежных курсов: Энди Гордон, Ларри Полсон, Энди Питтс (теория типов).
Отдельная глава полностью посвящена реализации нескольких примеров. В силу
своего объёма, она не рассматривается на экзамене и предназначена для самостоя-
тельного изучения. Её цель — закрепление пройденного материала и демонстрация
возможностей ML на практике.
Author(s): Харрисон Д.
Publisher: web
Year: 2015
Введение
Достоинства функционального программирования
План
Лямбда-исчисление
Преимущества лямбда-нотации
Парадокс Рассела
Лямбда-исчисление как формальная система
Лямбда-термы
Свободные и связанные переменные
Подстановка
Преобразования
Эквивалентность лямбда-выражений
Экстенсиональность
Лямбда-редукция
Стратегии редукции
Теорема Чёрча-Россера
Комбинаторы
Лямбда-исчисление как язык программирования
Представление данных в лямбда-исчислении
Логические значения и условия
Пары и кортежи
Натуральные числа
Рекурсивные функции
Let-выражения
Достижение уровня полноценного языка программирования
Дополнительная литература
Типы
Типизированное лямбда-исчисление
Множество допустимых типов
Типизация по Чёрчу и Карри
Формальные правила типизации
Сохранение типа
Полиморфизм
Проблемы let-полиморфизма
Наиболее общий тип
Сильная нормализация
Знакомство с ML
Энергичное вычисление
Результаты энергичного вычисления
Семейство языков ML
Запуск ML
Взаимодействие с ML
Связывания и объявления
Полиморфные функции
Равенство функций
Более подробно о ML
Основные типы данных и операции
Дальнейшие примеры
Определения типов
Сопоставление с образцом
Рекурсивные типы
Древовидные структуры
Тонкости рекурсивных типов
Доказательство корректности программ
Функциональные программы как математические объекты
Вычисление степени
Вычисление НОД
Конкатенация списков
Обращение списков
Эффективный ML
Полезные комбинаторы
Создание эффективного кода
Хвостовая рекурсия и аккумуляторы
Минимизация операций cons
Принудительное вычисление
Императивные возможности
Исключения
Ссылки и массивы
Последовательность вычислений
Работа с системой типов
Примеры
Символьное дифференцирование
Термы первого порядка
Печать
Дифференцирование
Упрощение
Синтаксический анализ
Метод рекурсивного спуска
Комбинаторы синтаксического анализа
Лексический анализ
Анализатор термов
Автоматический учёт приоритетов
Недостатки метода
Точная арифметика вещественных чисел
Выбор представления вещественных чисел
Целые числа произвольной разрядности
Основные операции
Умножение: общий случай
Обратные числа
Отношения порядка
Кэширование
Пролог и доказательство теорем
Термы Пролога
Лексический анализ
Синтаксический анализ
Унификация
Поиск с возвратом
Примеры
Доказательство теорем
