John Harrison - Введение в функциональное программирование (1108517), страница 5
Текст из файла (страница 5)
Этоможет сбивать с толку, например, f 0 (g(x)) обычно означает что-то отличное отdf (g(x)). Внимательные писатели, особенно в многомерных (FIXME multivariate)dxработах, часто явно показывают это отличие, записывая:|d 2x |x = 2xdxилиd 2z |x = 2xdzОдной из составляющей привлекательности λ-нотации является то, что всеоперации связывания переменных, такие как суммирование, дифференцированиеи интегрирование, могут рассматриваться как функции, применяемые к λвыражениям. Обобщение всех операций связывания переменных с помощьюλ-абстракции, позволяет нам сконцентрироваться на технических проблемахсвязанных переменных в конкретной ситуации. Например, мы можем рассматриватьd 2x как синтаксическую обвязку (syntactic sugaring) для D (λx. x2 ) x где D : (R →dxR) → R → R является оператором дифференцирования, производящий производнуюпервого аргумента (функции) в точке, указанной вторым аргументом.
Преобразуяобычный синтаксис в λ-нотацию, мы получим D (λx. EXP x 2) x для некоторойконстанты EXP, представляющей экспоненциальную функцию.Таким образом, λ-нотация очень привлекательна для математиков в качествеобщего ‘абстрактного синтаксиса’; все что нам нужно – соответствующий наборконстант с которыми мы начнем работать. λ-абстракция выглядит, ретроспективно,|10Глава 2. Лямбда-исчисление2.2.
Парадокс Расселакак подходящий примитив в терминах которого проводится анализ связыванияпеременных. Эта идея уходит корнями к записи логики высшего порядка в λнотации, использованной Чёрчем, а также, как мы увидим в следующей главе,Landin указывал на то, как много конструкций в языках программирования имеетаналогичную интерпретацию. В последнее время, идея использования λ-нотации вкачестве универсального абстрактного синтаксиса была введена Martin-Löf, и частона нее ссылаются как на ‘теорию Martin-Löf для выражений и арности (arity)’.12.2Парадокс РасселаКак мы уже упоминали, одной из привлекательных сторон λ-нотации является то,что она разрешает анализ почти всего математического синтаксиса.
Первоначально,Чёрч надеялся продвинуться дальше, и затронуть теорию множеств, которая,как хорошо известно, является достаточно мощным средством для формированияоснования для большей части современной математики. Взяв любое множество S, мыможем сформировать для него так называемый параметрический предикат (characteristic predicate) χS , такой, что:(χS (x) =true if x ∈ Sf alse if x 6∈ SИ наоборот, для любого унарного предиката (т.е.
функции одного аргумента) P ,мы можем рассмотреть множество всех x удовлетворяющих P (x) — мы будем простозаписывать P (x) для P (x) = true. Таким образом, мы видим, что множества ипредикаты являются лишь различными способами обсуждения одних и тех же вещей.Вместо рассмотрения S как множества, и записи x ∈ S, мы можем рассматриватьего как предикат, и записывать как S(x).Это позволяет проведение обычного анализа в λ-нотации: мы можем допуститьчто произвольные λ-выражения являются функциями, и косвенным образом, имножествами. К сожалению, это приводит к несовместимости.
Простейшим способомубедиться в этом, является рассмотрение парадокса Рассела про множество всехмножеств, которые не содержат сами себя:R = {x | x 6∈ x}У нас имеется R ∈ R ⇔ R 6∈ R, сильное противоречие. В терминах функций,определенных с помощью λ-нотации, мы задаем R = λx. ¬(x x), а затем находим,что R R = ¬(R R), рассчитывая на интуитивное понимание операции отрицания ¬.Для того, чтобы избежать таких парадоксов, Church (1940) развивает идеюРассела путем добавления в λ-нотацию понятия типа; мы должны рассмотретьэто в следующей главе. Однако сам парадокс предлагает некоторые интересныевозможности в стандартной, не типизированной системе, в чем мы убедимся позже.1Она была представлена на симпозиуме в Brouwer в 1981 году, но не попала в печатныематериалы симпозиума.112.3.
Лямбда-исчисление как формальная система2.3Глава 2. Лямбда-исчислениеλ-исчисление как формальная системаНекоторые очевидные факты принимались нами без обоснования, например,что (λy. 1 + y) 2 = 1 + 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, а ихсоставные части называть «ратор» и «ранд» соответственно.24. Абстракция произвольного λ-терма s по переменной x (которая может каквходить свободно в s, так и нет) имеет вид λx. s.Формально, этот набор правил представляет собой индуктивное определениемножества λ-термов, т. е. последние могут конструироваться только так, какописано выше. Благодаря этому, мы получаем основания для2Сокр.
«оператор» и «операнд ».12Глава 2. Лямбда-исчисление2.3. Лямбда-исчисление как формальная система• определения функций над λ-термами при помощи примитивной рекурсии;• доказательства утверждений о свойствах λ-термов методом структурнойиндукции.Формальное изложение понятий индуктивного построения, а также примитивнойрекурсии и структурной индукции доступно из многих источников. Мы надеемся,что читатель, не знакомый с этими формализмами, сможет получить достаточноепредставление об их базовых идеях на основе примеров, которые приводятся ниже.Подобно языкам программирования, синтаксис λ-термов может быть задан припомощи БНФ (форм Бэкуса-Наура):Exp = V ar | Const | Exp Exp | λ V ar. Expпосле чего мы можем трактовать их, как это принято в теории формальныхязыков, не просто как цепочки символов, а как абстрактные синтаксические деревья.Это значит, что соглашения наподобие левоассоциативности операции примененияфункции либо интерпретации λx y.
s как λx. λy. s, а также неразличимостьпеременных и констант по именам не являются неотъемлемой частью формализма λисчисления, а имеют смысл исключительно в момент преобразования терма в форму,подходящую для восприятия человеком, либо в обратном направлении.В завершение упомянем ещё одно соглашение, принятое в данном пособии.Будем использовать в λ-термах односимвольные имена не только для константи переменных, но и для так называемых метапеременных, обозначающих любыетермы.
Например, выражение λx. s может представлять как константную функциюсо значением s, так и произвольную λ-абстракцию по переменной x. Дляпредотвращения путаницы, условимся применять буквы s, t и u в качествеметапеременных. Устранить неоднозначность полностью возможно, например, засчёт потери компактности записи: введением имён переменных вида Vx вместо x,а констант — Ck вместо k, после чего исчезает необходимость приписывать именамособый статус.2.3.2Свободные и связанные переменныеВ этом разделе мы формализуем интуитивное понятие свободных и связанныхпеременных, которое, между прочим, служит хорошим примером определенияпримитивно-рекурсивных функций.
Интуитивно, вхождение переменной в заданныйтерм считается свободным, если оно не лежит в области действия соответствующейабстракции. Обозначим множество свободных переменных в терме s через F V (s) идадим его рекурсивное определение:F V (x)F V (c)F V (s t)F V (λx. s)===={x}∅F V (s) ∪ F V (t)F V (s) − {x}Аналогично вводится и понятие множества связанных переменных BV (s):BV (x) = ∅132.3. Лямбда-исчисление как формальная системаГлава 2. Лямбда-исчислениеBV (c) = ∅BV (s t) = BV (s) ∪ BV (t)BV (λx.
s) = BV (s) ∪ {x}Например, если s = (λx y. x) (λx. z x), то F V (s) = {z} и BV (s) = {x, y}. Отметим,что в общем случае переменная может быть одновременно и свободной, и связаннойв одном и том же терме, как это было показано выше. Воспользуемся структурнойиндукцией, чтобы продемонстрировать доказательство утверждений о свойствах λтермов на примере следующей теоремы (аналогичные рассуждения применимы и комножеству 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) также конечно, как объединение двух конечных множеств.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
