John Harrison - Введение в функциональное программирование

Введение в функциональноепрограммированиеJohn Harrisonjrh@cl.cam.ac.uk3rd December 1997iiiПредисловиеЭта книга основана на конспектах лекций по курсу Введение в функциональноепрограммирование, который я читал в университете Кембриджа в 1996/7 учебномгоду.Курс читался студентам последнего курса и аспирантам первого года обучения.К тому времени они уже свободно владели императивным программированием наязыке Modula-3, a параллельно с этим курсом им читался курс по C. Этот курсопределённо является курсом по функциональному программированию, а не курсомпо программированию с использованием функциональных языков. Я попыталсясделать упор на необычные свойства функциональных языков программирования,а также показать естественную область применения языка ML.

Я не рассматриваюмного важных аспектов, которые не присущи функциональному программированию,например абстрактные типы. В разделах помеченных звёздочкой размещёндополнительный материал, который не входит в экзамены, и который можнопропустить без потери понимания курса. Однако, я надеюсь, что некоторыезаинтересуются более глубоким изучением отдельных частей курса и эти людиубедятся, что разделы, помеченные звёздочкой, являются естественным дополнениемк основному тексту.В предыдущие годы этот курс преподавался Майком Гордоном (Mike Gordon).

Ясохранил структуру его курса, которая являет собой смесь теории и практики, и былазаимствована из его собственных лекционных материалов, доступных в части PartII книги (Gordon 1988). На меня также оказали сильное влияние те люди, которыечитали здесь сопутствующие курсы – Andy Gordon, Larry Paulson, и, в главе о типах –курс, созданный Andy Pitts.Большая глава с примерами не требуется на экзаменах. Она предназначена дляулучшения понимания предыдущих частей, а также для того, чтобы показать какML может быть использован.Большая часть глав включает примеры, либо созданные специально для данногокурса, либо заимствованные из других курсов. Обычно они требуют некоторогоразмышления, вместо того, чтобы быть стандартными задачами.

Те, которые япосчитал сложными, отмечены знаком (*).Эти материалы не были интенсивно протестированы, и без сомнения содержатразличные ошибки и неясности. Я буду благодарен за конструктивную критику состороны любого читателя.John Harrison (jrh@cl.cam.ac.uk).iiiivПлан лекцийЭтот раздел описывает как материал распределён по 12 лекциям курса, каждаяиз которых длиться немногим меньше часа.1. Введение и обзор Функциональное и императивное программирование:различия, «за» и «против». Общая структура курса: как λ-исчислениепревратилось в язык программирования общего назначения. λ-нотация: какразъясняет связывание переменных и как предоставляет средства общегоанализа математической записи. Каррирование.

Парадокс Рассела.2. λ-исчисление как формальная система Свободные и связанныепеременные. Подстановка. Правила преобразования. Эквивалентность λтермов. Экстенсиональность. Редукция и её стратегии. Теорема Чёрча-Россера:формулировка и следствия. Комбинаторы.3. λ-исчисление как язык программирования Становление теорииалгоритмов; полнота по Тьюрингу (без доказательства). Представление данныхи основные операции: логические значения, пары и кортежи, натуральныечисла. Вычисление предшествующего числа. Определение рекурсивныхфункций: комбинаторы неподвижной точки. Let-выражения.

λ-исчисление какдекларативный язык.4. Типы Зачем нужны типы? Ответы из программирования и логики. Простоетипизированное λ-исчисление. Типизация по Чёрчу и Карри. Let-полиморфизм.Наиболее общие типы и алгоритм Милнера. Сильная нормализация (бездоказательства), и её негативное влияние на полноту по Тьюрингу. Добавляемоператор рекурсии.5. ML ML как типизированное λ-исчисление с энергичным вычислением.Подробности стратегии вычисления. Условное выражение.

Семейство языковML. Практика работы с ML. Создание функций. Связывания и объявления.Рекурсивные и полиморфные функции. Сравнение функций.6. Более подробно о ML Загрузка кода из файлов. Комментарии. Основныетипы данных: процедурный, логические, числа и строки. Встроенныеоперации. Конкретный синтаксис и инфиксные операции. Дополнительныепримеры. Рекурсивные типы и сопоставление с образцом. Примеры: списки ирекурсивные функции для работы со списками.7. ДоказательствоТестирование икорректности программ Проблемаверификация. Область применимостиvкорректности.верификации.Функциональные программы как математические объекты. Примерыдоказательства свойств программ: вычисление степени и НОД, конкатенацияи обращение списков.8.

Эффективный ML Использование стандартных комбинаторов. Проход посписку и другие полезные примеры использования комбинаторов. Хвостоваярекурсия и аккумуляторы; почему хвостовая рекурсия более эффективна.Принудительное вычисление. Минимизация операций cons. Более эффективнаяреализация обращения данных. Использование «as». Императивныевозможности: исключения, ссылки, массивы и последовательность вычислений.Императивные возможности и типы; ограничение значения.9.

Примеры на ML I: символьное дифференцирование Символьныевычисления. Представление данных. Приоритет операторов. Ассоциативныесписки. Форматированный вывод выражений. Устанавливаем принтер.Дифференцирование. Упрощение. Проблема «правильного» упрощения.10. Примеры на ML II: синтаксический анализ Понятие грамматики, задачасинтаксического анализа. Устранение неоднозначностей. Метод рекурсивногоспуска. Реализация синтаксического анализа на языке ML. Комбинаторысинтаксического анализа, примеры.

Лексический анализ. Анализатор термов.Автоматический учёт приоритетов операций. Устранение возвратов. Сравнениес другими методами.11. Примеры на ML III: арифметика вещественных чисел Вещественныечисла и конечные представления. Вещественные числа как программыили функции. Выбор представления вещественных чисел. Целые числапроизвольной разрядности. Преобразование целочисленных значений ввещественные. Операции смены знака и вычисления абсолютной величины.Сложение: важность деления с округлением. Умножение и деление на целоечисло. Умножение: общий случай. Обратные числа и деление. Отношенияпорядка и равенства.

Тестирование. Устранение избыточных вычислений припомощи функций с памятью.12. Примеры на ML IV: Пролог и доказательство теорем Выражения вПрологе. Лексический анализ с учётом регистра. Разбор и печать, включаясписочный синтаксис. Унификация. Поиск с возвратом. Примеры выраженийв Пролог. Доказательство теорем в стиле Пролог. Работа с формулами;отрицательная нормальная форма. Базовое средство доказательства;использование продолжений. Примеры: проблемы Пельетьера и программа,расследующая преступления.viОглавление1 Введение1.1 Достоинства функционального программирования .

. . . . . . . . . . .1.2 План . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2 Лямбда-исчисление2.1 Преимущества лямбда-нотации . . . . . . . .2.2 Парадокс Рассела . . . . . . . . . . . . . . . .2.3 Лямбда-исчисление как формальная система2.3.1 Лямбда-термы . . . . . . . . . .

. . . .2.3.2 Свободные и связанные переменные . .2.3.3 Подстановка . . . . . . . . . . . . . . .2.3.4 Преобразования . . . . . . . . . . . . .2.3.5 Равенство лямбда-выражений . . . . .2.3.6 Экстенсиональность . . . . . . . . . . .2.3.7 Лямбда-редукция . . . . . . . . . . .

.2.3.8 Стратегии редукции . . . . . . . . . . .2.3.9 Теорема Чёрча-Россера . . . . . . . . .2.4 Комбинаторы . . . . . . . . . . . . . . . . . . ......................................................................................................................3 Лямбда-исчисление как язык программирования3.1 Представление данных в лямбда-исчислении . . . . . . . . . .3.1.1 Логические значения и условия .

. . . . . . . . . . . .3.1.2 Пары и кортежи . . . . . . . . . . . . . . . . . . . . . .3.1.3 Натуральные числа . . . . . . . . . . . . . . . . . . . .3.2 Рекурсивные функции . . . . . . . . . . . . . . . . . . . . . . .3.3 Let-выражения . . . . . . . . . . .

. . . . . . . . . . . . . . . .3.4 Достижение уровня полноценного языка программирования3.5 Дополнительная литература . . . . . . . . . . . . . . . . . . .4 Типы4.1 Типизированное лямбда-исчисление . .4.1.1 Множество допустимых типов .4.1.2 Типизация по Чёрчу и Карри .4.1.3 Формальные правила типизации4.1.4 Сохранение типа . . . . . . .

. .4.2 Полиморфизм . . . . . . . . . . . . . .4.2.1 Проблемы let-полиморфизма .4.2.2 Наиболее общий тип . . . . . . .vii.........................................................................................................................................................................................................................................................135.............78111212131416161718181921........252727283032333536........373939404142434445Оглавление4.3ОглавлениеСильная нормализация .

. . . . . . . . . . . . . . . . . . . . . . . . . . . 475 Знакомство с ML5.1 Энергичное вычисление . . . . . . . .5.2 Результаты энергичного вычисления5.3 Семейство языков ML . . . . . . . . .5.4 Запуск ML . . . . . . . . . . . . . . .5.5 Взаимодействие с ML .