«Введение в функциональное программирование John Harrison jrh 3rd December 1997 i ii Предисловие Эта книга основана на конспектах лекций по курсу Введение в функциональное программирование, который я читал в ...»

Введение в функциональное

программирование

John Harrison

[email protected]

3rd December 1997

i

ii

Предисловие

Эта книга основана на конспектах лекций по курсу Введение в функциональное

программирование, который я читал в университете Кембриджа в 1996/7 учебном

году.

Курс читался студентам последнего курса и аспирантам первого года обучения.

К тому времени они уже свободно владели императивным программированием на

языке Modula-3, a параллельно с этим курсом им читался курс по C. Этот курс определённо является курсом по функциональному программированию, а не курсом по программированию с использованием функциональных языков. Я попытался сделать упор на необычные свойства функциональных языков программирования, а также показать естественную область применения языка ML. Я не рассматриваю много важных аспектов, которые не присущи функциональному программированию, например абстрактные типы. В разделах помеченных звёздочкой размещён дополнительный материал, который не входит в экзамены, и который можно пропустить без потери понимания курса. Однако, я надеюсь, что некоторые заинтересуются более глубоким изучением отдельных частей курса и эти люди убедятся, что разделы, помеченные звёздочкой, являются естественным дополнением к основному тексту.

В предыдущие годы этот курс преподавался Майком Гордоном (Mike Gordon). Я сохранил структуру его курса, которая являет собой смесь теории и практики, и была заимствована из его собственных лекционных материалов, доступных в части Part II книги (Gordon 1988). На меня также оказали сильное влияние те люди, которые читали здесь сопутствующие курсы – Andy Gordon, Larry Paulson, и, в главе о типах – курс, созданный Andy Pitts.

Большая глава с примерами не требуется на экзаменах. Она предназначена для улучшения понимания предыдущих частей, а также для того, чтобы показать как ML может быть использован.

Большая часть глав включает примеры, либо созданные специально для данного курса, либо заимствованные из других курсов. Обычно они требуют некоторого размышления, вместо того, чтобы быть стандартными задачами. Те, которые я посчитал сложными, отмечены знаком (*).

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

John Harrison ([email protected]).

iii iv План лекций Этот раздел описывает как материал распределён по 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: Пролог и доказательство теорем Выражения в Прологе. Лексический анализ с учётом регистра. Разбор и печать, включая списочный синтаксис. Унификация. Поиск с возвратом. Примеры выражений в Пролог. Доказательство теорем в стиле Пролог. Работа с формулами; отрицательная нормальная форма. Базовое средство доказательства; использование продолжений. Примеры: проблемы Пельетьера и программа, расследующая преступления.

Оглавление Глава Введение Программы, написанные на традиционных языках программирования, таких как FORTRAN, Algol, C и Modula-3, в своей работе опираются на изменение значений набора переменных, называемого состоянием. Если мы пренебрежём операциями ввода-вывода и вероятностью того, что программа будет работать постоянно (например, управляющая система для производства), то мы можем прийти к следующей абстракции. Первоначально состояние имеет некоторое значение, представляющее собой входные данные для программы, а после завершения её исполнения новое значение, представляющее результаты. Выполнение отдельных операторов сводится к изменению ними состояния, которое последовательно проходит через конечное число значений:

Например, в программе сортировки состояние первоначально включает в себя массив значений, а после того, как программа завершается, состояние модифицируется таким образом, что эти значения становятся упорядоченными, в то время как промежуточные состояния представляют собой ход достижения данной цели.

Состояние обычно изменяется с помощью операторов присваивания, часто записываемых в виде v = E или v := E, где v – переменная, а E – некоторое выражение.

Последовательность выполнения таких операторов задаётся в тексте программы их размещением друг за другом (при этом часто в качестве разделителя применяется точка с запятой). С помощью составных операторов, таких как if и while, можно выполнять операторы в зависимости от условия или циклически, часто полагаясь на другие свойства текущего состояния. В результате программа превращается в набор инструкций по изменению состояния, и поэтому данный стиль программирования часто называется императивным или процедурным. Соответственно, традиционные языки программирования, поддерживающие такой стиль, также известны как императивные или процедурные языки.

Функциональное программирование радикально отличается от этой модели. По существу, функциональная программа представляет собой просто выражение, а выполнение программы процесс его вычисления.1 В общих чертах мы можем понять, как это возможно, используя следующие рассуждения. Предположим, что императивная программа (вся целиком) детерминирована, т.е. выход полностью определяетФункциональное программирование часто называют аппликативным программированием, поскольку основной его механизм – это аппликация (применение) функции к аргументам.

ся входом; мы можем сказать, что конечное состояние или тот его фрагмент, который нас интересует, являются функцией начального состояния, например = f ().2 В функциональном программировании эта точка зрения имеет особое значение: программа – это выражение, которое соответствует математической функции f. Функциональные языки поддерживают создание таких выражений за счет того, что позволяют использовать мощные функциональные конструкции.

Функциональное программирование может противопоставляться императивному как c хорошей, так и в плохой стороны. К недостаткам ФП можно отнести то, что функциональные программы не используют переменные – то есть не имеют состояния. Соответственно, они не могут использовать присваивание, поскольку нечему присваивать. Кроме того, идея последовательного выполнения операторов также бессмысленна, поскольку первый оператор не имеет никакого влияния на второй, так как нет никакого состояния, передаваемого между ними. К достоинствам функционального подхода можно отнести то, что функциональные программы могут использовать функции более изящным способом. Функции могут рассматриваться точно так же, как и более простые объекты, такие как целые числа: они могут передаваться в другие функции как аргументы и возвращаться в качестве результатов, а также применяться в вычислениях. Вместо последовательного выполнения операторов и использования циклов, функциональные языки программирования предлагают рекурсивные функции, т.е. функции, определённые в терминах самих себя. Большинство традиционных языков программирования обеспечивают весьма скудные возможности в этих областях. Язык C имеет некоторые ограниченные возможности работы с функциями при помощи указателей, но не позволяет создавать новые функции динамически, а язык FORTRAN вообще не поддерживает рекурсию.

Продемонстрируем разницу между императивным и функциональным программированием на примере функции вычисления факториала. Она может быть записана императивно на языке C как:

в то время как на языке ML (функциональном языке программирования, который мы обсудим позже) она может быть реализована в виде рекурсивной функции:

Можно отметить, что такое определение достаточно просто реализовать и на языке C. Однако, при необходимости более сложной работы с функциями функциональные языки не имеют себе равных.

Сравните это с замечанием Наура (Raphael 1966) о том, что мы можем записать любую программу в виде одного выражения Output = P rogram(Input).

Глава 1. Введение 1.1. Достоинства функционального программирования 1.1 Достоинства функционального программирования На первый взгляд, язык без переменных или возможности последовательного выполнения инструкций кажется совершенно непрактичным. Это впечатление не может быть разрушено с помощью нескольких слов, написанных тут. Но мы надеемся, что изучая материал, приведённый далее, читатель получит представление о том, какое разнообразие задач можно решить, программируя в функциональном стиле.

Имеративный стиль программирования не является нерушимой догмой. Многие свойства императивных языков программирования развились в процессе абстрагирования от типового компьютерного оборудования, от машинного кода к ассемблерам, затем к макроассемблерам, языку FORTRAN и так далее. Нет оснований утверждать, что такие языки представляют собой наиболее удобный способ взаимодействия человека и машины. В самом деле, последнее слово в развитии компьютерных архитектур еще не сказано, и компьютеры должны служить нашим нуждам, а не наоборот. Вероятно, что правильный подход не в том, чтобы начать с оборудования и продвигаться вверх, а наоборот – начать работу с языка программирования, как средства для описания алгоритмов, и затем двигаться вниз к оборудованию (Dijkstra 1976). В действительности, данная тенденция может быть обнаружена и в традиционных языках программирования. Даже FORTRAN позволяет записывать арифметические выражения обычным способом. Программист не обеспокоен задачей линеаризации вычисления подвыражений и выделения памяти для хранения промежуточных результатов.

Из этих соображений можно сделать вывод, что идея разработки языков программирования, сильно отличающихся от традиционных, императивных языков, является вполне законной. Однако, для того, чтобы показать, что мы не просто предлагаем изменения ради изменений, мы должны сказать несколько слов о том, почему мы могли бы предпочесть функциональные языки программирования императивным.

Возможно, главной причиной является то, что программы на функциональных языках более точно соответствуют математическим объектам, и их свойства легче доказывать. Для того, чтобы показать, что программа означает, мы можем связать абстрактный математический смысл с программой или оператором это цель денотационной семантики (семантика = значение, смысл). В императивных языках это должно делаться скорее побочным способом, из-за неявной зависимости от состояния. Для простых императивных языков можно связать оператор с функцией, где – множество допустимых состояний. Таким образом, оператор получает некоторое состояние и порождает другое. Однако, не каждый оператор всегда завершает свою работу (например, while true do x := x), так что эта функция, вообще говоря, является частичной. Иногда более предпочтительными являются альтернативные средства формализации семантики, например, преобразователи предикатов (Dijkstra 1976). Но если мы добавим возможности, которые могут сложным образом изменить последовательность выполнения операторов, например, goto, или конструкции break и continue языка C, то даже такие решения перестанут работать, поскольку один оператор может привести к пропуску выполнения других операторов, следующих за ним в тексте программы. Вместо этого обычно используют более сложные семантики, основанные на продолжениях (continuations).

В противоположность сказанному выше, функциональные программы, по словам 1.1. Достоинства функционального программирования Глава 1. Введение Хенсона Henson (1987), носят свою семантику с собой.3 Мы можем показать это на примере ML. Основные типы напрямую могут рассматриваться как математические объекты. Используя стандартную запись [[X]] для семантики X, мы можем сказать, например, что [[int]] = Z. Например, функция ML fact, определённая выражением:

имеет один аргумент типа int, и возвращает значение типа int, так что она просто является связанной с абстрактной частичной функцией Z Z:

(Здесь обозначает неопределённость, поскольку для отрицательных аргументов программа не сможет завершиться). Однако этот способ простой интерпретации не работает для не-функциональных программ, поскольку, так называемые функции могут не быть функциями в математическом смысле. Например, в стандартной библиотеке языка C есть функция rand(), которая возвращает различные псевдослучайные значения при последовательных вызовах. Это может быть сделано с помощью локальных статических переменных, используемых для хранения предыдущих результатов, например, так:

rand ( void ) { Таким образом, мы можем рассматривать отказ от переменных и присваивания, как следующий шаг после отказа от goto, поскольку каждый следующий шаг делает семантику проще. Более простая семантика делает доказательство свойств программ более ясным. Это даёт нам больше возможностей для доказательства корректности программ и преобразований, используемых для их оптимизации.

У функциональных языков есть и другое потенциальное преимущество. Поскольку вычисление выражений не имеет побочных эффектов для любых состояний, то отдельные подвыражения могут вычисляться в произвольном порядке, не влияя друг на друга. Это означает, что функциональные программы хорошо поддаются распараллеливанию, т.е., компьютер может автоматически вычислять различные подвыражения на разных процессорах. В то же время, императивные программы часто задают жёсткий порядок вычислений, так что даже ограниченное перемешивание инструкций в современных процессорах с конвейерной обработкой ведёт к сложностям и возникновению технических проблем.

На самом деле, ML не является чисто функциональным языком программирования; в нём есть переменные и присваивания, если потребуется. Большую часть времени мы будем делать нашу работу, оставаясь в рамках чисто функционального подмножества языка. Но даже если мы и воспользуемся присваиваниями, потеряв Дополнительно: денотационную семантику можно рассматривать как попытку превратить императивные языки в функциональные, путём явного объявления состояний.

некоторые из ранее перечисленных достоинств, останется в силе большая гибкость в работе с функциями, свойственная языкам, подобным ML. Программы часто могут быть выражены очень кратко и элегантно при помощи функций высшего порядка (функций, которые оперируют другими функциями).4 Код может быть более общим, поскольку он может быть параметризован другими функциями. Например, программа, которая складывает список чисел, и программа, которая умножает список чисел, могут рассматриваться как экземпляры одной и той же программы, которая параметризуется арифметической операцией над парой чисел и единичным элементом. В первом случае это будут + и 0, а во втором – и 1.5 В заключение, функции могут использоваться для представления бесконечных наборов данных удобным способом, например, мы позже покажем как использовать функции для выполнения вычислений с вещественными числами, в отличие от использования приближений в виде чисел с плавающей запятой.

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

Читатели данной книги должны сами сделать заключение о достоинствах функционального стиля. Мы не хотим навязывать никакую идеологию, а лишь хотим показать, что существуют разные подходы к программированию, и что в соответствующих ситуациях функциональное программирование может иметь значительные достоинства. Большинство наших примеров выбрано из областей, которые могут быть определены как символьные вычисления. Мы верим, что функциональные программы успешно работают в таких приложениях. Однако, как всегда, человек должен использовать наиболее подходящие для работы инструменты. Возможно, что императивное, объектно-ориентированное или логическое программирование лучше подходят для определённых задач.

Для тех, кто использовал императивное программирование, переход к функциональному будет неизбежно тяжёл, независимо от используемого подхода. Хотя есть люди, которые сразу хотят перейти непосредственно к программированию, мы выбрали другой подход – мы начнём с -исчисления, и покажем как оно может быть использовано в роли теоретической основы функциональных языков. Такой подход обладает тем достоинством, что он хорошо соответствует реальной истории разработки функциональных языков.

Следовательно, сначала мы введём -исчисление, и покажем как оно, первоначально предназначенное на роль формальной логической основы математики, преЭлегантность субъективна, а краткость не самоцель. Функциональные языки, а также другие языки, такие как APL, часто создают соблазн создания очень короткого, хитроумного кода, который элегантен для знатоков, но непонятен для остальных.

Это напоминает абстракции, введенные в чистой математике; например, аддитивные и мультипликативные структуры над числами являются частными случаями абстрактного понятия моноид. Такое подобие помогает избегать дублирования и увеличивает элегантность.

вратилось в полноценный язык программирования. Затем мы обсудим, зачем мы хотим добавить типы в -исчисление, и покажем, как добиться требуемого. Это приведёт нас к языку ML, который по существу является оптимизированной реализацией типизированного -исчисления с определённой стратегией вычисления выражений.

Мы рассмотрим практические основы функционального программирования на ML, обсудим полиморфизм и понятие наиболее общего типа данных. Затем мы перейдём к более сложным темам, таким как исключения и императивные возможности ML. В заключение, мы приведём несколько реальных примеров, которые, как мы надеемся, подтвердят мощь ML.

Дополнительная литература Множество книг о функциональном программировании включают в себя общее введение и описание отличий от императивного программирования просмотрите несколько и выберите ту, которая вам нравится. Например, Henson (1987) предлагает хорошее вводное обсуждение и содержит такую же смесь теории и практики, как и в этом тексте. Детальная и спорная пропаганда функционального стиля программирования приведена в работе создателя FORTRAN Джона Бэкуса Backus (1978). Работа Gordon (1994) обсуждает проблемы введения ввода-вывода в функциональные языки, а также приводит некоторые решения. Читатели, заинтересовавшиеся денотационной семантикой для императивных и функциональных языков, могут прочитать Winskel (1993).

Глава -исчисление В основе -исчисления лежит идея представления функций в так называемой нотации. В неформальной математике, когда кто-то хочет сослаться на функцию, то обычно сначала даёт ей произвольное имя, а затем использует уже его, например:

Предположим, что функция f : R R определена выражением:

Тогда f (x) не интегрируема по Лебегу в пределах [0, 1].

Большинство языков программирования, например C, в этом отношении похожи:

мы можем определять только именованные функции. Например, для того, чтобы использовать функцию successor (которая добавляет 1 к своему аргументу) нетривиально (например, через указатель), то несмотря на её простоту, нам всё равно придётся предварительно задать определение, в которое входит имя:

С точки зрения традиционной математики либо программирования это выглядит естественно и, в общем случае, достаточно удобно. Однако, такой подход начинает причинять массу затруднений при необходимости работы с функциями высшего порядка (которые манипулируют другими функциями). В любом случае, если мы хотим рассматривать функции наравне с другими математическими объектами, то требование давать им имена будет нелогичным. При обсуждении арифметического выражения, построенного из более простых подвыражений, мы просто записываем их без каких-либо имён. Представим, что было бы, если бы мы всегда работали с арифметическими выражениями таким образом:

Определим x и y так, что x = 2 и y = 4. Тогда xx = y.

Применение -нотации позволяет задавать функции практически тем же способом, что и остальные виды математических объектов. Существуют общепринятые обозначения, которые иногда использовались в математике для этих целей, хотя 2.1. Преимущества лямбда-нотации Глава 2. Лямбда-исчисление обычно они встречаются в составе именованных определений. Мы могли бы записать для обозначения функции, отображающей любой аргумент x в некоторое произвольное выражение t[x], которое обычно, но не обязательно, содержит x (иногда полезно “отбросить” аргумент). Однако, мы будем использовать другую нотацию, разработанную Чёрчем Church (1941):

Это выражение имеет точно такой же смысл, как и предыдущее. Например, x. x является тождественной функцией, которая просто возвращает переданный аргумент, в то время как x. x2 обозначает функцию возведения в квадрат.

Выбор символа является произвольным и не несёт никакой смысловой нагрузки.

(Так, например, нередко встречается, особенно во французских текстах, обозначение [x] t[x].) Вероятно, что он возник в ходе сложного эволюционного процесса. Первоначально в известной книге Principia Mathematica (Whitehead and Russell 1910) использовалось обозначение t[] для функции от x, производящей t[x]. Чёрч изменил его на x. t[x], но поскольку наборщики текстов не могли поместить значокнад x, то оно вышло в свет как x. t[x], которое затем трансформировалось в x. t[x] в руках других наборщиков.

2.1 Преимущества -нотации Используя -нотацию мы можем прояснить некоторые неточности, присущие неформальным математическим обозначениям. Например, часто говорят о ‘f (x)’, подразумевая, что из контекста понятно, о чём идёт речь или о результате её применения к конкретному x. Дополнительной пользой будет то, что -нотация даёт нам возможности анализа почти всего языка математики.

Если мы начнём с переменных и констант и будем строить выражения, используя лишь -абстрацию и применение функций к аргументам, то сможем в конечном счёте представить очень сложные математические выражения.

Будем использовать общепринятое обозначение f (x) для операции применения функции f к аргументу x, за тем исключением, что в традиционной -нотации скобки могут быть опущены, позволяя тем самым записать это выражение в виде f x. По причинам, которые станут понятны в процессе чтения следующего абзаца, мы считаем, что применение функции ассоциативно слева, т. е. f x y означает (f (x))(y). В качестве сокращённой записи для x. y. t[x, y] будем использовать x y. t[x, y], и т. д.

Мы также предполагаем, что область действия -абстракции распространяется вправо, насколько это возможно. Например, x. x y означает x. (x y), а не (x. x) y.

На первый взгляд, нам необходимо введение специальных обозначений для функций нескольких аргументов. Однако, существует способ представления таких функций в обычной -нотации. Этот способ называется каррированием (currying), по имени математика-логика Карри Curry (1930). (В действительности, такой приём уже использовался и Фреге Frege (1893), и Шейнфинкелем Schnnkel (1924), но легко понять, почему соответствующие термины не получили общественного признания.) Идея заключается в особой трактовке выражений вида x y. x + y. Это выражение может рассматриваться как функция R (R R), так что можно сказать, что оно является ‘функцией высшего порядка (higher order function)’ или ‘функционалом (functional)’, поскольку в результате применения к другой функции производит новую функцию, которая получает второй аргумент. На самом деле, она получает аргументы по очереди, по одному, а не все сразу. Например, рассмотрим:

Заметим, что в -нотации применение функции считается левоассоциативной операцией, поскольку каррирование используется очень часто.

Возможности -нотации особенно полезны для унификации понятия связанных переменных. В математике переменные обычно выражают зависимость некоторого выражения от значения этой переменной; например, значение x2 + 2 зависит от значения x. В таком контексте мы будем говорить, что переменная является свободной.

Однако, существуют другие ситуации, где переменная просто используется в качестве обозначения, а не показывает зависимость от значения. В качестве примеров можно рассмотреть переменную m в выражении и переменную y в выражении Немалое количество подобных примеров доступно и в других областях. Так, в логике применяются кванторы x. P [x] (‘для всех x, справедливо P [x]’) и x. P [x] (‘существует такое значение x, для которого P [x] истинно’); в теории множеств абстрактные множества, наподобие {x | P [x]}, а также индексированные объединения и пересечения. В таких случаях говорят, что переменная должна быть связанной (bound). В определённых подвыражениях она является свободной, но в полном выражении связана операцией связывания переменных, такой как сложение. Часть, находящаяся ‘внутри’ этой операции связывания переменных, называется областью видимости (scope) связанной переменной.

Похожая ситуация возникает в большинстве языков программирования, по крайней мере, среди потомков Algol 60. Переменные имеют определённую область видимости, а формальные аргументы процедур и функций являются связанными переменными, например, n в приведённом выше определении функции successor на языке C.

Кто-то может рассматривать объявления переменных как операцию связывания для вложенных объектов соответствующих переменных. Отметим, что область видимости переменной не следует отождествлять с её временем жизни. В функции rand на языке C, которую мы привели во введении, переменная n имеет ограниченную область видимости, но сохраняет своё значение даже за пределами данного блока кода.

Мы можем свободно изменить имя связанной переменной, не затрагивая смысл выражения. Например, Аналогичным образом, при использовании -нотации выражения x. E[x] и y. E[y] являются эквивалентными; это называется альфа-эквивалентностью, а процесс преобразования одного выражения в другое альфа-преобразованием. Следует особо оговорить, что переменная y не должна быть свободной в выражении E[x], иначе его значение изменится, например, как в Также возможно использовать в одном выражении одинаковые имена для свободных и связанных переменных; хотя это может сбивать с толку, но с технической точки зрения неоднозначности не возникает, например В действительности, обычная нотация Лейбница для производных имеет то же самое свойство, например, в переменная x используется и как связанная для того, чтобы показать, что дифференцирование производится относительно x, и как свободная, чтобы показать, где будет происходить окончательное вычисление производной. Это может сбивать с толку, например, f (g(x)) обычно означает что-то отличное от dx f (g(x)). Авторы, стремящиеся к максимальной точности формулировок, особенно в работах, посвящённых функциям многих переменных, зачастую подчёркивают это различие специальными обозначениями, например, или Одной из привлекательных черт -нотации является возможность рассматривать все операции связывания переменных, такие как суммирование, дифференцирование или интегрирование, как функции, применяемые к -выражениям. Обобщение таких операций с помощью -абстракции позволяет нам сконцентрироваться на технических проблемах связанных переменных в конкретной ситуации. Например, мы можем рассматривать dx x2 как синтаксическую обвязку (syntactic sugaring) для D (x. x2 ) x где D : (R R) R R является оператором дифференцирования, результат применения которого производная первого аргумента (функции) в точке, указанной вторым аргументом. Преобразуя обычный синтаксис в -нотацию, мы получим D (x. EXP x 2) x для некоторой константы EXP, представляющей экспоненциальную функцию.

Таким образом, -нотация очень привлекательна для математиков в качестве общего ‘абстрактного синтаксиса’; всё что нам нужно – соответствующий набор констант, с которыми мы будем работать. В ретроспективе, -абстракция выглядит как подходящий примитив, в терминах которого проводится анализ связывания переменных. Эта идея уходит корнями к записи логики высшего порядка в -нотации, использованной Чёрчем, и ко мнению Лэндина, которое будет продемонстрировано в следующей главе, что множество конструкций различных языков программирования имеет аналогичную интерпретацию. В последнее время, идея использования -нотации в качестве универсального абстрактного синтаксиса была введена Мартином-Лёфом, и часто на неё ссылаются как на ‘теорию Мартина-Лёфа для выражений и арности (arity)’. 2.2 Парадокс Рассела Как мы уже упоминали, одной из привлекательных сторон -нотации является её пригодность для анализа почти всего математического синтаксиса. Первоначально, Чёрч надеялся продвинуться дальше и затронуть теорию множеств, которая, как хорошо известно, является достаточно мощным средством для формирования основания для большей части современной математики. Взяв любое множество S, мы можем задать для него так называемый характеристический предикат S такой, что:

И наоборот, для любого унарного предиката (т.е. функции одного аргумента) P, мы можем рассмотреть множество всех x, удовлетворяющих P (x) мы будем просто записывать P (x) для P (x) = true. Таким образом, мы видим, что множества и предикаты являются лишь различными способами обсуждения одних и тех же вещей.

Вместо трактовки S как множества и записи x S, мы можем рассматривать его как предикат и записывать как S(x).

Это позволяет проведение обычного анализа в -нотации: мы можем допустить что произвольные -выражения являются как функциями, так, косвенным образом, и множествами. К сожалению, это приводит к противоречиям. Простейшим способом убедиться в этом служит парадокс Рассела про множество всех множеств, которые не содержат сами себя:

У нас имеется R R R R, сильное противоречие. В терминах функций, определённых с помощью -нотации, мы задаём R = x. ¬(x x), а затем находим, что R R = ¬(R R), исходя из интуитивного понимания операции отрицания ¬.

Для того, чтобы избежать таких парадоксов, Church (1940) развивает идею Рассела путём добавления в -нотацию понятия типа, которое будет подробно рассмотрено далее. Однако, сам парадокс предлагает некоторые интересные возможности в стандартной, нетипизированной системе, в чём мы убедимся позже.

2.3 -исчисление как формальная система До сих пор некоторые очевидные факты принимались нами без обоснования, например, что (y. 1 + y) 2 = 1 + 2, поскольку это соответствует желаемым свойствам Она была представлена на симпозиуме в Brouwer в 1981 году, но не попала в печатные материалы симпозиума.

2.3. Лямбда-исчисление как формальная система Глава 2. Лямбда-исчисление операций применения и абстракции, которые считаются в определённом смысле взаимно обратными. Чтобы перейти от интуитивных действий к -исчислению, нам потребуется зафиксировать некоторые из основных принципов, объявив их (и только их) формальными правилами. Привлекательность этого шага в том, что правила в дальнейшем могут применяться механически, подобно тому, как преобразование уравнения x 3 = 5 x в равносильное ему 2x = 5 + 3 не требует каждый раз задумываться, почему допустимо такое перемещение слагаемых из одной части равенства в другую. Как писал Уайтхед в работе Whitehead (1919), формальная символика и правила действий...

[... ] вводились всякий раз, когда требовались что-либо упростить. [... ] используя формальные обозначения, мы можем переходить от одного этапа рассуждений к другому почти механически, зрительно, в противном же случае нам пришлось бы задействовать гораздо больше интеллектуальных ресурсов. [... ] Цивилизация прогрессирует, увеличивая количество важных операций, которые могут производиться, не задумываясь.

2.3.1 -термы Основой -исчисления служит формальное понятие -термов, которые строятся из переменных и некоторого фиксированного множества констант при помощи операций применения (аппликации) функций и -абстракции. Это значит, что всевозможные -термы разбиваются на четыре класса:

1. Переменные: обозначаются произвольными алфавитно-цифровыми строками; как правило, мы будем использовать в качестве имён буквы, расположенные ближе к концу латинского алфавита, например, x, y и z.

2. Константы: количество констант определяется конкретной -нотацией, иногда их нет вовсе. Мы будем также обозначать их алфавитно-цифровыми строками, как и переменные, отличая друг от друга по контексту.

3. Комбинации: применение функции s к аргументу t, где s и t представляют собой произвольные термы. Будем обозначать комбинации как s t, а их составные части называть ратор и ранд соответственно. 4. Абстракция произвольного -терма s по переменной x (которая может как входить свободно в s, так и нет) имеет вид x. s.

Формально, этот набор правил представляет собой индуктивное определение множества -термов, т. е. последние могут конструироваться только так, как описано выше. Благодаря этому, мы получаем основания для • определения функций над -термами при помощи примитивной рекурсии;

• доказательства утверждений о свойствах -термов методом структурной индукции.

Сокр. оператор и операнд.

Глава 2. Лямбда-исчисление 2.3. Лямбда-исчисление как формальная система Формальное изложение понятий индуктивного построения, а также примитивной рекурсии и структурной индукции доступно из многих источников. Мы надеемся, что читатель, не знакомый с этими формализмами, сможет получить достаточное представление об их базовых идеях на основе примеров, которые приводятся ниже.

Подобно языкам программирования, синтаксис -термов может быть задан при помощи БНФ (форм Бэкуса-Наура):

после чего мы можем трактовать их, как это принято в теории формальных языков, не просто как цепочки символов, а как абстрактные синтаксические деревья. Это значит, что соглашения наподобие левоассоциативности операции применения функции либо интерпретации x y. s как x. y. s, а также неразличимость переменных и констант по именам не являются неотъемлемой частью формализма -исчисления, а имеют смысл исключительно в момент преобразования терма в форму, подходящую для восприятия человеком, либо в обратном направлении.

В завершение упомянем ещё одно соглашение, принятое в данном пособии. Будем использовать в -термах односимвольные имена не только для констант и переменных, но и для так называемых метапеременных, обозначающих любые термы.

Например, выражение x. s может представлять как константную функцию со значением s, так и произвольную -абстракцию по переменной x. Для предотвращения путаницы, условимся применять буквы s, t и u в качестве метапеременных. Устранить неоднозначность полностью возможно, например, за счёт потери компактности записи: введением имён переменных вида Vx вместо x, а констант Ck вместо k, после чего исчезает необходимость приписывать именам особый статус.

2.3.2 Свободные и связанные переменные В этом разделе мы формализуем интуитивное понятие свободных и связанных переменных, которое, между прочим, служит хорошим примером определения примитивно-рекурсивных функций. Интуитивно, вхождение переменной в заданный терм считается свободным, если оно не лежит в области действия соответствующей абстракции. Обозначим множество свободных переменных в терме s через F V (s) и дадим его рекурсивное определение:

Аналогично вводится и понятие множества связанных переменных BV (s):

Например, если s = (x y. x) (x. z x), то F V (s) = {z} и BV (s) = {x, y}. Отметим, что в общем случае переменная может быть одновременно и свободной, и связанной 2.3. Лямбда-исчисление как формальная система Глава 2. Лямбда-исчисление в одном и том же терме, как это было показано выше. Воспользуемся структурной индукцией, чтобы продемонстрировать доказательство утверждений о свойствах термов на примере следующей теоремы (аналогичные рассуждения применимы и ко множеству BV ).

Теорема 2.1 Для произвольного -терма s множество F V (s) конечно.

Доказательство: Применим структурную индукцию. Очевидно, что для терма s, имеющего вид переменной либо константы, множество F V (s) конечно по определению (содержит единственный элемент либо пусто соответственно). Если терм s представляет собой комбинацию t u, то согласно индуктивному предположению, как F V (t), так и F V (u) конечны, в силу чего F V (s) = F V (t) F V (u) также конечно, как объединение двух конечных множеств. Наконец, если s имеет форму x. t, то по определению F V (s) = F V (t) {x}, а F V (t) конечно по индуктивному предположению, откуда следует, что F V (s) также конечно, поскольку его мощность не может превышать мощности F V (t).

2.3.3 Подстановка Одним из правил, которые мы хотим формализовать, является соглашение о том, что -абстракция и применение функции представляют собой взаимно обратные операции. То есть, если мы возьмём терм x. s и применим его как функцию к термуаргументу t, результатом будет терм s, в котором все свободные вхождения переменной x заменены термом t. Для большей наглядности это действие принято обозначать x. s[x] и s[t] соответственно.

Однако, простое на первый взгляд понятие подстановки одного терма вместо переменной в другой терм на самом деле оказалось весьма коварным, так что даже некоторые выдающиеся логики не избежали ложных утверждений относительно его свойств. Подобный грустный опыт разочаровывает довольно сильно, ведь как мы говорили ранее, одним из привлекательных свойств формальных правил служит возможность их чисто механического применения.

Обозначим операцию подстановки терма s вместо переменной x в другой терм t как t[s/x]. Иногда можно встретить другие обозначения, например, t[x:=s], [s/x]t, или даже t[x/s]. Мы полагаем, что предложенный нами вариант легче всего запомнить по аналогии с умножением дробей: x[t/x] = t. На первый взгляд, рекуррентное определение понятия подстановки выглядит так:

К сожалению, это определение не совсем верно. Например, подстановка (y. x + y)[y/x] = y.y+y не соответствует интуитивным ожиданиям от её результата.3 Исходный -терм интерпретировался как функция, прибавляющая x к своему аргументу, Строго говоря, нам следовало бы писать + x y, нежели x + y, но мы будем, как прежде, использовать стандартные операции в инфиксной форме.

Глава 2. Лямбда-исчисление 2.3. Лямбда-исчисление как формальная система так что после подстановки мы ожидали получить функцию, которая прибавляет y, а на деле получили функцию, которая свой аргумент удваивает. Источником проблемы служит захват переменной y, которую мы подставляем, операцией y...., которая связывает одноимённую переменную. Чтобы этого не произошло, связанную переменную требуется предварительно переименовать:

а лишь затем производить подстановку:

Существуют два подхода к решению этой проблемы. С одной стороны, можно условиться, что подстановка недопустима в ситуации захвата переменной, а с другой расширить формальное определение подстановки таким образом, чтобы требуемое переименование переменных происходило автоматически. Мы остановимся на последнем варианте:

(s1 s2 )[t/x] = s1 [t/x] s2 [t/x] Единственное отличие этого определения заключается в двух последних правилах. Мы следуем предыдущему определению в двух безопасных ситуациях, когда либо переменная x не свободна в терме s, так что подстановка оказывается тривиальной, либо когда y не свободна в t, так что захват переменной не произойдёт (на данном уровне). Однако, в случае, когда оба эти условия не выполняются, мы предварительно переименовываем переменную y в z, выбранную так, чтобы она не была свободной ни в терме s, ни в терме t, после чего продолжаем, как описано выше.

Для определённости, переменная z может выбираться некоторым фиксированным способом, например, как первая в лексикографическом порядке имён переменная из множества всех переменных, не имеющих свободных вхождений ни в s, ни в t. 2.3.4 Преобразования Ещё одной из основ -исчисления служат три преобразования операции получения по заданному терму другого, равного ему в интуитивном смысле. Традиционно Знатоки могут быть обеспокоены тем, что последнее правило не позволяет считать это определение примитивно-рекурсивным. Однако, его легко преобразовать в примитивно-рекурсивную множественную параллельную подстановку. Подобная процедура напоминает усиление индуктивного предположения в ходе доказательства. Отметим, что по построению пара подстановок в последнем правиле может осуществляться как параллельно, так и последовательно без ущерба для результата.

2.3. Лямбда-исчисление как формальная система Глава 2. Лямбда-исчисление их обозначают буквами греческого алфавита: (альфа), (бета) и (эта).5 Приведём формальные определения этих операций, обозначив каждую из них помеченной стрелкой.

• Альфа-преобразование: x. s y. s[y/x], при условии, что y F V (s). Например, u. u v w. w v, но u. u v v. v v. Такое ограничение устраняет возможность ещё одного случая захвата переменной.

• Бета-преобразование: (x. s) t s[t/x].

• Эта-преобразование: x. t x t, если x F V (t). Например, u. v u v, Среди этих трёх операций наиболее важной для нас является -преобразование, поскольку оно соответствует вычислению функции для заданного аргумента. В то же время, -преобразование играет роль вспомогательного средства переименования связанных переменных, а -преобразование представляет собой разновидность экстенсиональности, в силу чего интересно главным образом с точки зрения логика, а не программиста.

2.3.5 Эквивалентность -выражений Используя приведённые выше правила преобразований, мы можем определить формально условия, при которых два -терма считаются эквивалентными. В общих чертах, два терма эквивалентны, если один из них может быть получен из другого в ходе конечной последовательности, либо -преобразований, которые применяются к произвольным подтермам как в прямом, так и в обратном направлении. Другими словами, отношение -эквивалентности представляет собой congruence closure трёх преобразований и обладает свойствами рефлексивности, симметричности, транзитивности и заменяемости. Ниже приводится формальное индуктивное определение, правила которого трактуются следующим образом: если утверждение над горизонтальной чертой выполняется, то справедливо и утверждение под ней.

Такие имена преобразований были введены Карри. Первоначально Чёрч называл - и преобразования правило действий I и правило действий II соответственно.

Глава 2. Лямбда-исчисление 2.3. Лямбда-исчисление как формальная система Отметим, что использование обычного знака равенства (=) в данном контексте может ввести в заблуждение. В самом деле, мы задаём некоторое отношение -эквивалентности, взаимосвязь которого с понятием равенства соответствующих математических объектов остаётся неясной.6 В то же время очевидно, что следует отличать -эквивалентность от синтаксического равенства. Последнее будем называть тождеством и обозначим символом. Например, x. x y. y, хотя в то же время x. x = y. y.

Во многих случаях оказывается, что -преобразования не играют роли, в силу чего вместо строгого тождества применяется его вариант. Это отношение определяется подобно -эквивалентности, но исключительно для -преобразований. Например, (x.x)y (y.y)y. Многие авторы используют его как тождество -термов, тем самым разбивая множество термов на соответствующие классы эквивалентности. Существуют альтернативные системы обозначений, например (de Bruijn 1972), в которых связанные переменные не имеют имён. В таких системах традиционное понятие тождества совпадает с.

2.3.6 Экстенсиональность Мы уже упоминали ранее, что -преобразование воплощает принцип экстенсиональности. В рамках общепринятых философских понятий два свойства называются экстенсионально эквивалентными (либо коэкстенсивными), если этими свойствами обладают в точности одни и те же объекты. В теории множеств принята аксиома экстенсиональности, согласно которой два множества совпадают, если они состоят из одних и тех же элементов. Аналогично, будем говорить, что две функции эквивалентны, если области их определения совпадают, а значения функций для всевозможных аргументов также одинаковы.

Введение -преобразования делает наше понятие -эквивалентности экстенсиональным. В самом деле, пусть f x и g x равны для произвольного значения x; в частности, f y = g y, где переменная y выбирается так, чтобы она не была свободной как в f, так и в g. Согласно последнему из приведённых выше правил эквивалентности, y. f y = y. g y. Применив дважды -преобразование, получаем, что f = g. С другой стороны, из экстенсиональности следует, что всевозможные -преобразования не нарушают эквивалентности, поскольку согласно правилу -редукции (x. t x) y = t y для произвольного y, если переменная x не является свободной в терме t. На этом мы завершаем обсуждение сущности -преобразования и его влияния на теорию в целом, чтобы уделить больше внимания более перспективному с точки зрения вычислимости -преобразованию.

2.3.7 -редукция Отношение -эквивалентности, как и следовало ожидать, является симметричным. Оно достаточно хорошо соответствует интуитивному понятию эквивалентности Действительно, ведь мы не определяем достаточно точно, каково это соответствие само по себе. Тем не менее, существуют модели -исчисления, в которых -эквивалентность трактуется как обычное равенство.

2.3. Лямбда-исчисление как формальная система Глава 2. Лямбда-исчисление -термов, но с алгоритмической точки зрения более интересен его несимметричный аналог. Определим отношение редукции следующим образом:

В действительности слово редукция (в частности, термин -редукция, которым иногда называют -преобразования) не отражает точно сути происходящего, поскольку в процессе редукции терм может увеличиваться, например:

Однако, несмотря на это редукция имеет прямое отношение к процедуре вычисления терма, в ходе которой последовательно вычисляются комбинации вида f (x), где f -абстракция. Если на некотором этапе оказывается, что не могут быть применены никакие правила редукции, кроме -преобразований, то говорят, что терм имеет нормальную форму.

2.3.8 Стратегии редукции Отложив на время наши теоретические рассуждения, напомним их взаимосвязь с практикой функционального программирования. Программа на функциональном языке представляет собой выражение, а её выполнение вычисление этого выражения. То есть, в терминах, изложенных выше, мы собираемся начать процесс вычислений с соответствующего терма и применять к нему правила редукции до тех пор, пока это возможно. Возникает вопрос: какое из имеющихся правил следует применять на каждом этапе? Отношение редукции недетерминированное, то есть, для некоторых термов t найдётся множество термов ti таких, что t ti. Выбор того или иного варианта оказывается иногда принципиально важным, поскольку может привести как к конечной, так и к бесконечной последовательности редукций (выполнение соответствующей программы при этом либо завершается, либо зацикливается). Например, подвергая редукции наиболее глубокий редекс7 в выражении, приведённом англ. redex (reducible expression) редуцируемое выражение Глава 2. Лямбда-исчисление 2.3. Лямбда-исчисление как формальная система ниже, мы получаем бесконечную последовательность редукций:

В то же время, редукция самого внешнего редекса немедленно ведёт нас к желаемому результату.

Значение выбора стратегии редукции окончательно проясняется следующими теоремами, которые мы рассмотрим без доказательств, поскольку они слишком велики для данного учебника. Первая теорема утверждает, что ситуация, с которой мы столкнулись в последнем примере, и её решение достаточно общие, т. е. стратегия редукции самого левого редекса является наилучшей с точки зрения завершимости.

Теорема 2.2 Если справедливо s t, где терм t имеет нормальную форму, то последовательность редукций, которая начинается с терма s и состоит в применении правил редукции к самому левому редексу, всегда завершается и приводит к терму в нормальной форме.

Применение этой теоремы требует формального определения понятия самого левого редекса: для терма (x.s) t это он сам, для произвольного другого терма вида s t самым левым является самый левый редекс s, наконец, для абстракции x.s это тоже самый левый редекс s. В рамках принятых в данном пособии обозначений мы будем всегда выбирать такой редекс, чтобы соответствующий ему символ был расположен левее прочих.

2.3.9 Теорема Чёрча-Россера Следующее утверждение, которое мы рассмотрим, широко известно как теорема Чёрча-Россера. Оно гласит, что для двух конечных последовательностей редукций, начатых с терма t, всегда найдутся две другие последовательности, сводящие результаты предыдущих к одному и тому же терму (который, впрочем, может и не быть в нормальной форме).

Теорема 2.3 Если t s1 и t s2, то существует терм u такой, что s1 u и s2 u.

Важные следствия данного утверждения:

Corollary 2.4 Если t1 = t2 то найдётся терм u такой, что t1 u и t2 u.

Доказательство: Легко показать (при помощи структурной индукции), что отношение -равенства = представляет собой симметричное транзитивное замыкание отношения редукции. Дальнейшее следует по индукции согласно свойствам симметричного транзитивного замыкания. Приведённая ниже диаграмма может показаться читателям, не склонным к формальным построениям, более доходчивой:

Мы полагаем, что t1 = t2, т. е. существует некоторая последовательность редукций в обеих направлениях (зигзагообразная линия в верхней части рисунка), которая их объединяет. Теорема Чёрча-Россера позволяет нам заполнить недостающие участки на краях диаграммы, после чего требуемый результат достигается композицией этих редукций.

Corollary 2.5 Если t = t1 и t = t2, причём t1 и t2 имеют нормальную форму, то t1 t2, т. е. t1 и t2 равны с точностью до -преобразований.

Доказательство: Согласно изложенному выше, найдётся некоторый терм u такой, что t1 u и t2 u. Но так как t1 и t2 уже имеют нормальную форму, последовательность редукций, приводящая к терму u, может состоять лишь из -преобразований.

Таким образом, нормальные формы, если они существуют, являются единственными с точностью до -преобразования. Это даёт нам первое обоснование того, что отношение -эквивалентности нетривиально, т. е. что существуют неэквивалентные термы. Например, поскольку x y.x и x y.y несводимы друг к другу исключительно при помощи -преобразований, они не эквивалентны.

Подытожим важность полученных результатов в свете теории вычислимости.

Стратегия редукции, в которой на каждом шаге выбирается самый левый редекс, считается, в известном смысле, наилучшей, поскольку она применима всегда, когда применима любая другая стратегия. Такая стратегия получила название нормального порядка редукции. С другой стороны, любая другая конечная последовательность редукций будет всегда давать тот же самый результат; более того, всегда остаётся возможность прекратить применение этой стратегии, перейдя при необходимости к нормальному порядку. Мы увидим практическое применение этого принципа далее.

2.4 Комбинаторы Впервые понятие комбинатора и основанная на нём теория были сформулированы М.И. Шейнфинкелем в работе Schnnkel (1924) ещё до появления -исчисления.

Вскоре после этого аналогичные результаты были получены Карри, независимо от Шейнфинкеля и Чёрча. (Когда Карри ознакомился с работами Шейнфинкеля, он предпринял попытку с ним связаться, но к этому времени Шейнфинкель оказался в психиатрической лечебнице.) В данной работе мы позволим себе не соблюдать историческую достоверность, изложив теорию комбинаторов как один из аспектов -исчисления.

Будем называть комбинатором терм -исчисления без свободных переменных.

Такие термы также принято называть замкнутыми, поскольку их значение не зависит от значений каких-либо переменных. В дальнейшем в курсе функционального программирования мы встретимся с большим количеством полезных комбинаторов, но краеугольным камнем теории комбинаторов служит тот факт, что на самом деле достаточно лишь немногих из них. Оказывается, что произвольный терм может быть выражен при помощи определённого множества комбинаторов и всевозможных переменных, операция -абстракции становится ненужной. В частности, замкнутый терм может быть представлен исключительно через эти комбинаторы. Дадим их определения:

Чтобы легче их запомнить, можно воспользоваться простыми мнемоническими правилами.8 Комбинатор I представляет собой тождественную функцию ( идентичность ), комбинатор K порождает семейство константных9 функций: после применения к аргументу a он даёт функцию y. a. Наконец, S комбинатор совместного применения, который принимает в качестве аргументов две функции, применяемые к общему аргументу. Докажем следующее утверждение:

Лемма 2.6 Для произвольного -терма t, не содержащего -абстракций, найдётся терм u, который также не содержит -абстракций и представляет собой композицию S, K, I и переменных, причём F V (u) = F V (t) {x} и u = x. t, т. е. терм u -равен x. t.

Доказательство: Применим к терму t структурную индукцию. Согласно условию, он не может быть абстракцией, поэтому нам требуется рассмотреть лишь три случая.

• Если t представляет собой переменную, возможны два случая, из которых непосредственно следует требуемый вывод: при t = x мы получаем x. x = I, • Если t представляет собой комбинацию термов, например, s u, то согласно индуктивному предположению найдутся термы s и u, которые не содержат -абстракций и для которых справедливы равенства s = x. s и u = x. u. Из этого можно сделать вывод, что S s u является искомым выражением. В Мы не утверждаем, что эти правила имеют под собой историческую основу.

Шейнфинкель использовал обозначение C, но мы предлагаем своё, основанное на нем. Konstant, в честь его немецкого происхождения (автор ошибается, М. И. Шейнфинкель работал в Германии, но родился в России Прим. перев.) самом деле, Таким образом, применив -преобразование, мы получаем S s u = x. S s u x = x. t, поскольку согласно индуктивному предположению переменная x не является свободной в термах s либо u.

Теорема 2.7 Для произвольного -терма t существует не содержащий абстракций терм t, полученный композицией K, I и переменных, такой, Доказательство: Применим структурную индукцию к терму t и воспользуемся леммой 2.6. Например, если терм t имеет вид x. s, то мы сначала можем получить, согласно индуктивному предположению, терм s свободный от абстракций эквивалент s. Далее применим лемму к x. s. Прочие случаи очевидны.

Это примечательное утверждение может быть даже усилено, поскольку комбинатор I выражается через S и K. Отметим, что для произвольного A Отсюда, применив -преобразование, получаем, что I = S K A для любых A. Однако, по причинам, которые станут яснее после знакомства с понятием типа, наиболее удобно положить A = K. Таким образом, I = S K K, что даёт нам возможность устранить все вхождения I в комбинаторные выражения.

Заметим, что приведённые выше доказательства имеют конструктивный характер, поскольку предлагают конкретные процедуры получения по заданному терму эквивалентного комбинаторного выражения. Процесс его построения идёт в направлении снизу вверх, и для каждой -абстракции, которая по построению имеет тело, свободное от -абстракций, применяются сверху вниз преобразования, изложенные в лемме.

Несмотря на то, что мы рассматриваем комбинаторы как некоторые термы исчисления, на их основе можно сформулировать независимую теорию. Её построение начинается с определения формальных правил конструирования выражений, в которые не входит -абстракция, но входят комбинаторы. Далее вместо, и преобразований вводятся правила преобразования для выражений, включающих комбинаторы, например, K x y x. Такая теория будет иметь множество аналогий в традиционном -исчислении, например, теорема Чёрча-Россера оказывается справедливой и для приведённого выше определения редукции. Кроме того, полностью устраняются сложности со связыванием переменных. Тем не менее, мы считаем полученный формализм не слишком интуитивным, поскольку комбинаторные выражения нередко бывают весьма неясными.

Помимо важной роли, которую комбинаторы играют в логике, они также имеют и определённый практический потенциал. Как мы уже кратко упоминали (подробное изложение ожидается в следующих разделах), -исчисление может считаться простым функциональным языком, основой для более развитых и практически применимых языков, наподобие ML. Теорема о комбинаторной полноте даёт основание говорить, что выражения -исчисления могут быть скомпилированы в машинный код комбинаторов. Эта терминология из теории языковых процессоров оказывается на самом деле вполне уместной. Комбинаторы применялись как средство реализации функциональных языков, в том числе и на уровне аппаратного обеспечения, предназначенного для вычисления комбинаторных выражений.

Дополнительная литература Энциклопедическая, но при этом доступная работа по теории -исчисления Barendregt (1984). Другой популярный учебник Hindley and Seldin (1986). Обе эти книги содержат доказательства результатов, которые мы приводим без обоснования.

Вторая часть Gordon (1988) представляет собой упрощённое изложение предмета, ориентированное на его применение в прикладной математике. Существенная часть данного курса базируется на последней работе.

Упражнения 1. Найдите нормальную форму терма (x x x. x) a b c.

2. Пусть twice = f x. f (f x). Каков интуитивный смысл twice? Найдите нормальную форму twice twice twice f x. (Напомним, что операция применения функции левоассоциативна.) 3. Найдите терм t такой, что t t. Можно ли утверждать, что терм имеет нормальную форму тогда и только тогда, когда из t t следует t t ?

4. В каком случае справедливо s[t/x][u/y] s[u/y][t/x]?

5. Постройте выражение, равносильное f x. f (x x), используя лишь комбинаторы I, K и S.

6. Найдите единственный комбинатор X такой, что все -термы эквивалентны термам, построенным композицией X и переменных. Указание: положите A = p. p K S K, а затем рассмотрите A A A и A (A A).

7. Докажите, что терм X является комбинатором неподвижной точки тогда и только тогда, когда он представляет собой неподвижную точку комбинатора G такого, что G = y m. m(y m).

2.4. Комбинаторы Глава 2. Лямбда-исчисление Глава -исчисление как язык программирования Проблема разрешимости (также известная как Entscheidungsproblem) была одним из основных предметов изучения логиков 1930-х. Формулировка задачи такова:

существует ли некоторая систематическая (механическая) процедура определения истинности утверждения в логике первого порядка? Положительный ответ на этот вопрос имел бы фундаментальное философское и, возможно, практическое значение:

принципиальную возможность решить большое количество разнообразных сложных математических задач исключительно при помощи некоторого фиксированного метода (в настоящий момент используется термин алгоритм) без привлечения дополнительных творческих усилий.

Очевидно, что проблема разрешимости непроста, поскольку требует точного определения понятия систематической либо механической процедуры на языке математики. В работе Turing (1936) даётся, вероятно, лучший анализ этой задачи. В ней также утверждается, что механическими можно считать действия, которые могут быть в принципе выполнены достаточно умным клерком, не обладающим знаниями об объекте этих действий. Абстрагирование поведения такого клерка привело в дальнейшем к известному понятию машины Тьюринга. Вопреки тому, что эта концепция была чисто математической, а роль исполнителя действий первоначально предназначалась человеку, мы можем также рассматривать машину Тьюринга как очень простой компьютер. Несмотря на простоту, эта машина способна проделать любые вычисления, доступные реальным машинным исполнителям.1 Вычислительную модель, эквивалентную по своей полноте машине Тьюринга, принято называть полной по Тьюрингу либо Тьюринг-полной.

Почти одновременно с Тьюрингом, другими авторами были предложены независимые определения понятия механической процедуры, большая часть которых оказалась эквивалентной машине Тьюринга по своей вычислительной полноте. В частности, лямбда-исчисление, первоначально предназначенное на роль формальной основы математики, также возможно трактовать и как язык программирования, в котором исполнение программ сводится к последовательности бета-преобразований.

В действительности, машина Тьюринга обладает большей вычислительной полнотой за счёт отсутствия ограничений на объём доступной памяти. Строго говоря, любой существующий компьютер алгоритмически эквивалентен конечному автомату, но для удобства принято также полагать объём его памяти бесконечным.

В самом деле, Чёрч ещё до публикации работ Тьюринга сделал предположение, что множество операций, представимых в рамках лямбда-исчисления, является формальным эквивалентом интуитивного понятия механической процедуры. Этот постулат был в дальнейшем назван тезисом Чёрча. В работе Church (1936) показано, что из этого тезиса следует неразрешимость Entscheidungsproblem. Тьюринг впоследствии доказал, что множество функций, представимых в рамках лямбда-исчисления, в точности совпадает со множеством функций, вычислимых машиной Тьюринга.

Этот результат послужил ещё одним доводом в пользу справедливости тезиса Чёрча.

С точки зрения современных программистов, программы для машины Тьюринга могут считаться достаточно примитивной разновидностью машинных кодов. В самом деле, очень вероятно, что именно машины Тьюринга, в особенности так называемая универсальная машина,2 оказали решающее влияние на разработку современных компьютерных архитектур с хранимой программой; впрочем, степень этого влияния и его природа продолжают служить объектом дискуссий (Robinson 1994). Примечательно то, что некоторые другие альтернативные определения механической процедуры, часто сформулированные задолго до появления электронных компьютеров, достаточно точно соответствуют реальным методам программирования. Например, алгоритмы Маркова (формальная вычислительная модель, популярная в Советском Союзе) могут считаться основой языка программирования SNOBOL. В дальнейшем нас будет интересовать аналогичное влияние лямбда-исчисления на эволюцию функциональных языков.

Язык LISP, второй (после FORTRAN) старейший язык высокого уровня, использует некоторые понятия лямбда-исчисления, в частности, обозначение (LAMBDA · · ·) для безымянных функций, но в целом ему не соответствует. В самом деле, как ранние версии языка, так и некоторые его современные диалекты используют принцип динамического связывания имён переменных, несовместимый с лямбда-исчислением (подробное обсуждение см. ниже). Более того, в ранних версиях отсутствовала приемлемая поддержка понятия функций высших порядков, зато имелся существенный объём императивных конструкций. Но несмотря на это, LISP заслуживает внимания как первый функциональный язык программирования, в котором также впервые были реализованы многие сопутствующие возможности, такие как автоматическое распределение памяти и сборка мусора.

Влияние лямбда-исчисления на языки программирования приобрело реальный вес с появлением в 1960-х работ Лэндина и Стрейчи. В частности, Лэндин показал, что множество свойств распространённых в то время (императивных) языков может успешно анализироваться в терминах лямбда-исчисления, к примеру, понятие областей видимости переменных в Algol 60. В работе Landin (1966) было предложено использовать лямбда-исчисление как основу языков программирования, примером чего послужил функциональный язык ISWIM ( If you See What I Mean досл. Если вам понятно, о чём речь ). Эта публикация завоевала в дальнейшем широкую известность и стала отправной точкой в разработке многих других языков, нашедших практическое применение.

Язык ML ведёт свою историю с появления в роли метаязыка (откуда, собственно, и происходит его название ML, Meta Language) системы доказательства теорем Универсальной называется машина Тьюринга, способная воспроизводить работу любой другой, т. е. выполнять роль интерпретатора. Подробнее это будет рассмотрено в курсе Computation Theory.

Глава 3. Лямбда-исчисление как язык программирования Edinburgh LCF (Gordon, Milner, and Wadsworth 1979). Это значит, что язык был предназначен для реализации алгоритмов логического вывода в формальном дедуктивном исчислении. Определение языка обнаруживает существенное влияние ISWIM, но в отличие от последнего, ML был расширен такими возможностями, как новаторская полиморфная типизация, включающая абстрактные типы данных, либо система обработки ошибок на основе исключений. Эти черты языка были введены, исходя из реальных практических потребностей, что в итоге привело к целостному и точному дизайну. Подобная узкая специализация характерна для успешных языков (язык C может служить ещё одним хорошим примером) и резко их отличает от провальных попыток коллективного проектирования, таких как Algol 60, который оказался скорее источником важных идей, нежели практичным инструментом. Дальнейшее знакомство с ML состоится позже, а в данный момент мы рассмотрим, как в роли языка программирования может быть использовано чистое лямбда-исчисление.

3.1 Представление данных в -исчислении Программы для своей работы требуют входных данных, поэтому мы начнём с фиксации определённого способа представления данных в виде выражений лямбдаисчисления. Далее введём некоторые базовые операции над этим представлением.

Во многих случаях оказывается, что выражение s, представленное в форме, удобной для восприятия человеком, может напрямую отображаться в лямбда-выражение s.

Этот процесс получил жаргонное название синтаксическая глазировка ( syntactic sugaring ), поскольку делает горькую пилюлю чистой лямбда-нотации более удобоваримой. Введём следующее обозначение:

Будем говорить, что s = s по определению ; другая общепринятая форs =def s. При желании, мы можем всегда счима записи этого отношения тать, что вводим некоторое константное выражение, определяющее семантику операции, которая затем применяется к своим аргументам в обычном стиле лямбдаисчисления, абстрагируясь тем самым от конкретных обозначений. Например, выражение if E then E1 else E2 возможно трактовать как COND E E1 E2, где COND некоторая константа. В подобном случае все переменные в левой части определения должны быть связаны операцией абстракции, т. е. вместо (см. ниже) мы можем написать 3.1.1 Логические значения и условия Для представления логических значений true ( истина ) и false ( ложь ) годятся любые два различных лямбда-выражения, но наиболее удобно использовать следующие:

3.1. Представление данных в лямбда-исчислении Используя эти определения, легко ввести понятие условного выражения, соответствующего конструкции ? : языка C. Отметим, что это условное выражение, а не оператор (который не имеет смысла в данном контексте), поэтому наличие альтернативы обязательно.

В самом деле, мы имеем:

Определив условное выражение, на его базе легко построить весь традиционный набор логических операций:

3.1.2 Пары и кортежи Определим представление упорядоченных пар следующим образом:

Использование скобок не обязательно, хотя мы часто будем использовать их для удобства восприятия либо подчёркивания ассоциативности. На самом деле, мы можем трактовать запятую как инфиксную операцию наподобие +. Определив пару, как указано выше, зададим соответствующие операции извлечения компонент пары как:

Легко убедиться, что эти определения работают, как требуется:

Глава 3. Лямбда-исчисление как язык программирования Построение троек, четвёрок, пятёрок и так далее вплоть до кортежей произвольной длины n производится композицией пар:

Всё, что нам при этом потребуется определение, что инфиксный оператор запятая правоассоциативен. Дальнейшее понятно без введения дополнительных соглашений. Например:

В последнем выражении для удобства восприятия было произведено альфапреобразование. Несмотря на то, что кортежи представляют собой плоскую структуру данных, путём последовательной их композиции возможно представить произвольную конечную древовидную структуру. Наконец, если кто-то предпочитает традиционные функции, заданные на декартовом произведении, нашим каррированным функциям, преобразовать их друг в друга нетрудно:

Эти специальные операции над парами нетрудно обобщить на случай кортежей произвольной длины n. Например, мы можем задать функцию-селектор выборки i-го компонента из кортежа p. Обозначим эту операцию (p)i, и определим её как (p)1 = fst p, (p)i = fst (sndi1 p). Аналогичным образом возможно обобщение CURRY и UNCURRY:

Воспользуемся обозначением (x1,..., xn ). t как сокращённой формой записи для обеспечив тем самым естественную нотацию для функций над декартовыми произведениями.

3.1. Представление данных в лямбда-исчислении 3.1.3 Натуральные числа Представим натуральное число n в виде то есть, 0 = f x. x, 1 = f x. f x, 2 = f x. f (f x) и т. д. Такое представление получило название нумералов Чёрча, хотя его базовая идея была опубликована ранее в работе Wittgenstein (1922).4 Это представление не слишком эффективно, так как фактически представляет собой запись чисел в системе счисления по основанию 1: 1, 11, 111, 1111, 11111, 111111,.... С точки зрения эффективности можно разработать гораздо лучшие формы представления, к примеру, кортеж логических значений, который интерпретируется как двоичная запись числа. Впрочем, в данный момент нас интересует лишь принципиальная вычислимость, а нумералы Чёрча имеют различные удобные формальные свойства. Например, легко привести лямбда-выражения такой общеизвестной арифметической операции, как получение числа, следующего в натуральном ряду за данным, то есть, прибавление единицы к аргументу операции:

В самом деле, Аналогично, легко реализуется проверка числа на равенство нулю:

поскольку Сумма и произведение двух нумералов Чёрча:

Запись выражения f n x с параметром n применяется исключительно для удобства записи, а не в силу его цикличности.

См. 6.021 A number is the exponent of an operation.

Глава 3. Лямбда-исчисление как язык программирования В справедливости этих определений легко убедиться:

Несмотря на то, что эти операции на натуральных числах были определены достаточно легко, вычисление числа, предшествующего данному, гораздо сложнее. Нам требуется выражение P RE такое, что P RE 0 = 0 и P RE (n + 1) = n. Решение этой задачи было предложено Клини в работе Kleene (1935). Клини применил такой прим: для заданного f x.f n x требуется отбросить одно из применений f. В качестве первого шага введём на множестве пар функцию PREFN такую, что Предположив, что подобная функция существует, можно показать, что (PREFN f )n+1 (true, x) = (false, f n x). В свою очередь, этого достаточно, чтобы задать функцию PRE, не испытывая особых затруднений. Определение PREFN, удовлетворяющее нашим нуждам, таково:

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

3.2. Рекурсивные функции 3.2 Рекурсивные функции Возможность определения рекурсивных функций является краеугольным камнем функционального программирования, поскольку в его рамках это единственный общий способ реализовать итерацию. На первый взгляд, сделать подобное средствами лямбда-исчисления невозможно. В самом деле, именование функций представляется непременной частью рекурсивных определений, так как в противном случае неясно, как можно сослаться на функцию в её собственном определении, не зацикливаясь.

Тем не менее, существует решение и этой проблемы, которое, однако, удалось найти лишь ценой значительных усилий, подобно построению функции PRE.

Ключом к решению оказалось существование так называемых комбинаторов неподвижной точки. Замкнутый терм Y называется комбинатором неподвижной точки, если для произвольного терма f выполняется равенство f (Y f ) = Y f. Другими словами, комбинатор неподвижной точки определяет по заданному терму f его фиксированную точку, т. е. находит такой терм x, что f (x) = x. Первый пример такого комбинатора, найденный Карри, принято обозначать Y. Своим появлением он обязан парадоксу Рассела, чем объясняется его другое популярное название парадоксальный комбинатор. Мы определили после чего обнаружили справедливость Таким образом, R R представляет собой неподвижную точку операции отрицания. Отсюда, чтобы построить универсальный комбинатор неподвижной точки, нам потребуется лишь обобщить данное выражение, заменив ¬ произвольной функцией, заданной аргументом f. В результате мы получаем Убедиться в справедливости этого определения несложно:

Однако, несмотря на математическую корректность, предложенное решение не слишком привлекательно с точки зрения программирования, поскольку оно справедливо лишь в смысле лямбда-эквивалентности, но не редукции (в последнем выражении мы применяли обратное бета-преобразование). С учётом этих соображений альтернативное определение Тьюринга может оказаться более предпочтительным:

(Доказательство справедливости T f f (T f ) предоставляется читателю в качестве упражнения.) Однако, мы можем без особого ущерба для строгости изложения считать, что Y f может подвергаться бета-редукции в соответствии с последовательностью редукции для рекурсивных функций. Рассмотрим, как комбинатор неподвижной точки (например, Y ) может применяться для реализации рекурсии.

Воспользуемся в качестве примера вычислением факториала. Мы хотим определить функцию fact следующим образом:

Прежде всего, преобразуем эту функцию в эквивалентную:

которая, в свою очередь, эквивалентна Отсюда следует, что fact представляет собой неподвижную точку такой функции F :

В результате всё, что нам потребуется, это положить fact = Y F. Аналогичным способом можно воспользоваться и в случае взаимно рекурсивных функций, т. е. множества функций, определения которых зависят друг от друга. Такие определения, как могут быть при помощи кортежей преобразованы в одно:

Положив t = (f1, f2,..., fn ), видим, что каждая из функций в правой части равенства может быть вычислена по заданному t применением соответствующей функцииселектора: fi = (t)i. Применив абстракцию по переменной t, получаем уравнение в канонической форме t = F t, решением которого является t = Y F, откуда в свою очередь находятся значения отдельных функций.

3.3 Let-выражения Возможность использования безымянных функций была нами ранее преподнесена как одно из достоинств лямбда-исчисления. Более того, имена оказались необязательными даже при определении рекурсивных функций. Однако, зачастую всё же удобно иметь возможность давать выражениям имена с тем, чтобы избежать утомительного повторения больших термов. Простая форма такого именования может быть реализована как ещё один вид синтаксической глазури поверх чистого лямбдаисчисления:

3.3. LET-выражения Глава 3. Лямбда-исчисление как язык программирования Простой пример применения этой конструкции работает, как и ожидается:

Мы можем добиться как последовательного, так и параллельного связывания множества имён с выражениями. Первый случай реализуется простым многократным применением конструкции связывания, приведённой выше. Во втором случае введём возможность одновременного задания множества связываний, отделяемых друг от друга служебным словом and:

Будем рассматривать эту конструкцию как синтаксическую глазурь для Продемонстрируем различия в семантике последовательного и параллельного связывания на примере:

дают в результате 4 и 3 соответственно.

В дополнение к этому разрешим связывать выражения с именами, за которыми следует список параметров; такая форма конструкции let представляет собой ещё одну разновидность синтаксической глазури, позволяющую трактовать f x1 · · · xn = t как f = x1 · · · xn. t. Наконец, помимо префиксной формы связывания let x = s in t введём постфиксную, которая в некоторых случаях оказывается удобнее для восприятия:

Например, мы можем написать так: y < y 2 where y = 1 + x.

Обычно конструкции let и where интерпретируются, как показано выше, без привлечения рекурсии. Например, связывает x с уменьшенным на единицу значением, которое уже было связано с именем x в охватывающем контексте, а не пытается найти неподвижную точку выражения x = x 1.5 В случае, когда нам требуется рекурсивная интерпретация, это может быть указано добавлением служебного слова rec в конструкции связывания (т. е. использованием let rec и where rec соответственно). Например, Это выражение может считаться сокращённой формой записи let fact = Y F, где как было показано выше.

Неподвижная точка этого выражения существует, но соответствующий лямбда-терм не имеет нормальной формы, т. е. в известном смысле не определён. Семантика незавершимых термов достаточно сложна и не будет нами рассматриваться. В действительности, основной вопрос заключается в наличии у терма не нормальной, а так называемой головной нормальной формы, что подробнее рассматривается в работах Barendregt (1984) и Abramsky (1990).

Глава 3. Лямбда-исчисление как язык программирования языка программирования 3.4 Достижение уровня полноценного языка программирования На данный момент мы ввели достаточно обширный набор средств синтаксической глазировки, реализующих удобочитаемый синтаксис поверх чистого лямбдаисчисления. Примечательно то, что этих средств достаточно для определения функции факториала в форме, очень близкой к языку ML. В связи с этим возникает вопрос, уместно ли считать лямбда-исчисление, расширенное предложенными обозначениями, практически пригодным языком программирования?

В конечном счёте, программа представляет собой единственное выражение. Однако, использование let для именования различных важных подвыражений, делает вполне естественной трактовку программы как множества определений различных вспомогательных функций, за которыми следует итоговое выражение, например:

Эти определения вспомогательных функций могут трактоваться с математической точки зрения как уравнения. Подобная интерпретация не задаёт никаких ограничений ни на способ вычисления выражений, ни даже направление, в котором уравнения будут использоваться. Благодаря этому, функциональный подход к программированию часто называют декларативным наряду с логическим (примером последнего служит язык PROLOG).6 В рамках такого подхода программа не содержит явных инструкций, а лишь объявляет некоторые свойства соответствующих понятий, оставляя подробности своего выполнения компьютеру.

В то же время, программа бесполезна или, по крайней мере, неоднозначна, если для неё не определены некоторые содержательные действия компьютера. Следовательно, требуется понимание того, что внешне полностью декларативная программа должна быть выполнена неким определённым образом. В самом деле, вычисление выражения начинается с раскрытия всех входящих в него имён определений (т. е.

уравнения интерпретируются слева направо), после чего производится последовательность -преобразований. Это значит, что несмотря на отсутствие процедурной информации в программе, неявно подразумевается наличие некоторой конкретной стратегии выполнения. Таким образом, понятие декларативности относится в большей степени к восприятию программ человеком.

Кроме того, должны существовать определённые правила, касающиеся стратегии редукции, поскольку выбор различных -редексов, как мы знаем, может оказать решающее влияние на завершимость. Как следствие, полностью определённый язык программирования из лямбда-исчисления получается лишь тогда, когда мы зададим эту стратегию. В дальнейшем мы увидим, какие решения были приняты в ходе проектирования различных функциональных языков, но перед этим нам придётся прервать наше изложение и обсудить введение понятия типа.

По всей видимости, Лэндин предпочитал термин денотационный.

3.5. Дополнительная литература Лямбда-исчисление как язык программирования 3.5 Дополнительная литература Многие из упомянутых стандартных работ включают в себя подробный анализ вопросов, затронутых в этом разделе. В частности, в работе Gordon (1988) даётся строгое доказательство Тьюринг-полноты лямбда-исчисления, а также того, что задача проверки существования нормальной формы терма (аналог проблемы останова в лямбда-исчислении) алгоритмически неразрешим. Влияние лямбда-исчисления на полноценные языки программирования, а также на эволюцию функциональных языков в частности обсуждается в работе Hudak (1989).

Упражнения 1. Дайте обоснование обобщённого -преобразования, т. е. докажите, что 2. Пусть f g = x. f (g x). Приняв во внимание, что I = x. x, докажите, что CURRY UNCURRY = I. Верно ли также, что UNCURRY CURRY = I?

3. Какие арифметические операции соответствует заданным на множестве нумералов Чёрча функциям n f x. f (n f x) и m n. n m?

4. (Клоп) Докажите, что следующее выражение представляет собой комбинатор неподвижной точки:

= abcdef ghijklmnopqstuvwxyzr. r(thisisaf ixedpointcombinator) 5. Дайте рекурсивное определение операции вычитания натуральных чисел.

6. Пусть задано следующее представление списков Mairson (1991):

Почему автор этого представления Мэйрсон назвал его списками Чёрча ? Каково назначение каждой из приведённых функций?

Глава Типы Типы представляют собой удобное средство определения различных разновидностей данных, наподобие логических и целочисленных значений либо функций. Благодаря типизации оказывается возможным гарантировать соблюдение ограничений, порождаемых этими различиями (например, что функция не должна применяться к аргументам с неподходящими типами). Что побуждает нас ввести понятие типа в лямбда-исчисление и языки программирования на его основе? Основания для такого решения можно найти как в логике, так и в программировании.

С точки зрения логики, требуется преодолеть парадокс Рассела, который препятствует попыткам построить непротиворечивое расширение лямбда-исчисления теорией множеств. Источником противоречий служит необычная циклическая природа используемого при этом приёма применение функции к самой себе. Более того, если бы даже и не требовалось избежать парадокса, всё равно возникает интуитивное ощущение неясности формальной системы, в рамках которой разрешены подобные действия. Безусловно, самоприменение таких функций, как тождественная функция (x. x) и функция-константа (x. y), выглядит безобидно. В то же время, очевидна и потребность в более ясном описании того, какие именно семейства функций представимы в терминах лямбда-исчисления при условии, что нам точно известны области определения и значений этих функций, а также то, что мы их применяем лишь к аргументам, принадлежащим соответствующим областям определения.

Введение Расселом типов в своей работе Principia Mathematica было продиктовано приведёнными соображениями.

Ещё одной причиной, которая побуждает нас подробно рассмотреть возможность расширения лямбда-исчисления понятием типа, является применение типизации в других языках программирования. Понятие типов данных встречается уже в языке FORTRAN, в котором различаются целые числа и числа с плавающей точкой. Причины появления типов в данном контексте не были связаны с изложенными ранее аргументами из области логики. Одной из таких причин была, очевидно, эффективность порождаемого компилятором кода. Наличие информации о допустимых способах использования той или иной переменной позволяет как генерировать более эффективный код, так и рациональнее распределять память. Например, реализация адресной арифметики в духе языка C должна учитывать размер объектов, к которым происходит обращение. Если p представляет собой указатель на объект размером 4 байта, то выражение p + 1 при трансляции в машинный код на архитектурах с побайтовой адресацией памяти превращается в p + 4. Предшественник C, язык BCPL, был бестиповым, и в нём не делалось различий между целыми числами и указателями. Как следствие, соответствующие масштабирующие множители в каждой операции адресной арифметики задавались в программе явным образом, создавая тем самым существенные неудобства.

Дальнейшее развитие привело к тому, что типизация, оставаясь важным средством повышения эффективности, стала приобретать всё большее значение как инструмент ограниченной статической проверки корректности программ. Существенная доля ошибок, от очевидных опечаток до серьёзных концептуальных просчётов, проявляет себя нарушением правил типизации, благодаря чему эти ошибки могут быть выявлены непосредственно в ходе компиляции без запуска программы на исполнение. Более того, в ходе чтения исходных текстов типы зачастую играют роль документации. Наконец, типы данных могут применяться для улучшения модульности программ и скрытия информации при помощи таких определений различных структур данных, которые явно разделены на интерфейс и подробности реализации.

В то же время некоторые программисты выступают против использования типов, полагая, что для их стиля программирования ограничения, накладываемые типизацией, являются излишне утомительными. Как следствие, различается и уровень её поддержки языками программирования. Существуют бестиповые языки, как императивные (BCPL), так и функциональные (ISWIM, SASL и Erlang ???). Другие, подобно PL/I, имеют лишь слабую типизацию, которая допускает некоторые варианты совместного использования данных различных типов при помощи автоматических преобразований, реализуемых компилятором. Наконец, некоторые языки, такие как Lisp, осуществляют динамический контроль типов во время исполнения программы. Этот подход может, в принципе, существенно ухудшить производительность, поскольку требует дополнительных вычислительных ресурсов, подобно тому, как это происходит с другим известным источником накладных расходов проверкой корректности обращений к массивам. Статическая же типизация, напротив, может существенно снизить издержки. На практике важность тех или иных ограничений типизации существенно зависит от характера решаемых задач и стиля программирования. Разработка системы типов, обеспечивающей как возможность содержательного статического контроля, так и достаточный уровень гибкости, остаётся предметом активных исследований.

Типизация, реализованная в языке ML, представляет собой важное достижение, поскольку в ней допускается полиморфизм, благодаря которому одна и та же функция может применяться к аргументам различных типов. Такой подход сохраняет все выгоды сильной статической типизации, дополняя их некоторыми возможностями, присущими слабому или динамическому контролю типов2. Более того, программист как правило не обязан указывать типы явно транслятор ML способен самостоятельно вывести наиболее общий тип каждого выражения, отвергая те из них, которые не поддаются типизации. Роль полиморфизма в процессе вывода типов будет рассмотрена далее. Таким образом, несомненно, что система типов языка ML делает его подходящим инструментом для широкого класса задач. Тем не менее, мы не хотели бы создать у читателя ложного впечатления, что этот язык служит универсальным средством от всех проблем программирования.

Одним из направлений развития динамической типизации является её дополнение элементами статической, что зачастую позволяет добиться сравнимой эффективности. Прим. перев.

Возможно, также ценой дополнительных затрат.

4.1 Типизированное лямбда-исчисление В первом приближении расширение лямбда-исчисления понятием типа не представляет особого труда, но в итоге, как будет показано, потребуется куда больше усилий. Основная идея состоит в том, что каждому терму назначается тип, после чего выражение s t, т. е. применение терма s к терму t, допустимо исключительно для совместимых типов, то есть в случае, когда типы s и t имеют вид и соответственно. Результирующий терм будет иметь при этом тип. Такую типизацию принято называть сильной.3 Терм t обязан иметь тип, подтипы и преобразования не допускаются. Такой подход составляет резкий контраст с некоторыми языками программирования, например, с языком C, в котором функция, ожидающая аргумент типа float либо double, принимает также значения типа int, выполняя автоматическое преобразование. Аналогичные понятия подтипов и преобразований возможно задать и в рамках лямбда-исчисления, но их освещение завело бы нас слишком далеко.

Введём для отношения t имеет тип обозначение t :. Подобная запись традиционно используется математиками при работе с функциональными пространствами, поскольку f : обозначает функцию f, отображающую множество во множество. Будем считать типы множествами, которые содержат соответствующие объекты, и трактовать t : как t. Однако, несмотря на то, что мы предлагаем читателям также воспользоваться этой удобной аналогией, типизированное лямбдаисчисление будет в дальнейшем рассматриваться исключительно как формальная система, свободная от каких-либо интерпретаций.

4.1.1 Множество допустимых типов Начнём формализацию строгим определением понятия типа. Предположим, что у нас имеется некоторое множество примитивных типов, в которое входят, например, типы bool и int. Составные типы могут быть определены при помощи конструктора типа функции. Формально, индуктивное определение множества типов T yC, основанного на множестве примитивных типов C, выглядит так:

Например, в рамках данного определения допустимы типы int, bool bool либо (int bool) int bool. Будем считать операцию правоассоциативной, т. е.

полагать выражение равным ( ). Такая трактовка естественно согласуется с другими синтаксическими правилами, касающимися каррирования.

Следующим нашим шагом будет расширение системы типов в двух направлениях. Во-первых, введём наравне с примитивными типами (которые выполняют роль констант) так называемые переменные типа, которые впоследствии лягут в основу полиморфизма. Во-вторых, разрешим использование множества конструкторов других типов, помимо типа функции. Например, в дальнейшем нам понадобится Сильную типизацию также часто называют строгой. Прим. перев.

конструктор для типа декартова произведения. Как следствие, наше индуктивное определение должно быть дополнено ещё одним выражением: