John Harrison - Введение в функциональное программирование (1108517), страница 7
Текст из файла (страница 7)
x x x) (λx. x x x)−→ (λx. x x x) (λx. x x x) (λx. x x x) (λx. x x x)−→ . . .Однако, несмотря на это редукция имеет прямое отношение к процедуре вычислениятерма, в ходе которой последовательно вычисляются комбинации вида f (x), где f —λ-абстракция. Если на некотором этапе оказывается, что не могут быть примененыникакие правила редукции, кроме α-преобразований, то говорят, что терм имеетнормальную форму.2.3.8Стратегии редукцииОтложив на время наши теоретические рассуждения, напомним их взаимосвязьс практикой функционального программирования. Программа на функциональномязыке представляет собой выражение, а её выполнение — вычисление этоговыражения.
То есть, в терминах, изложенных выше, мы собираемся начать процессвычислений с соответствующего терма и применять к нему правила редукции дотех пор, пока это возможно. Возникает вопрос: какое из имеющихся правил следуетприменять на каждом этапе? Отношение редукции — недетерминированное, тоесть, для некоторых термов t найдётся множество термов ti таких, что t −→ti . Выбор того или иного варианта оказывается иногда принципиально важным,поскольку может привести как к конечной, так и к бесконечной последовательностиредукций (выполнение соответствующей программы при этом либо завершается,18Глава 2.
Лямбда-исчисление2.3. Лямбда-исчисление как формальная системалибо зацикливается). Например, подвергая редукции наиболее глубокий редекс7в выражении, приведённом ниже, мы получаем бесконечную последовательностьредукций:(λx. y) ((λx. x x x) (λx. x x x))−→ (λx. y) ((λx. x x x) (λx.
x x x) (λx. x x x))−→ (λx. y) ((λx. x x x) (λx. x x x) (λx. x x x) (λx. x x x))−→ · · ·В то же время, редукция самого внешнего редекса(λx. y) ((λx. x x x) (λx. x x x)) −→ yнемедленно ведёт нас к желаемому результату.Значение выбора стратегии редукции окончательно проясняется следующимитеоремами, которые мы рассмотрим без доказательств, поскольку они слишкомвелики для данного учебника.
Первая теорема утверждает, что ситуация, с котороймы столкнулись в последнем примере, и её решение достаточно общие, т. е.стратегия редукции самого левого редекса является наилучшей с точки зрения еёзавершимости.Теорема 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.Важные следствия данного утверждения:7англ. redex (reducible expression) — «редуцируемое выражение»192.3.
Лямбда-исчисление как формальная системаГлава 2. Лямбда-исчислениеCorollary 2.4 Если t1 = t2 то найдётся терм u такой, что t1 −→ u и t2 −→ u.Доказательство: Легко показать (при помощи структурной индукции), чтоотношение λ-равенства = представляет собой симметричное транзитивноезамыкание отношения редукции. Дальнейшее следует по индукции согласносвойствам симметричного транзитивного замыкания.
Приведённая нижедиаграмма может показаться читателям, не склонным к формальнымпостроениям, более доходчивой:t1t2@@@@R@R@R@R@@@@R@R@R@@@R@R@@R@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 несводимы друг к другу исключительно припомощи α-преобразований, они не равны.Подытожим важность полученных результатов в свете теории вычислимости.Стратегия редукции, в которой на каждом шаге выбирается самый левыйредекс, считается, в известном смысле, наилучшей, поскольку она применимавсегда, когда применима любая другая стратегия. Такая стратегия получиланазвание нормального порядка редукции. С другой стороны, любая другая конечнаяпоследовательность редукций будет всегда давать тот же самый результат; болеетого, всегда остаётся возможность прекратить применение этой стратегии, перейдяпри необходимости к нормальному порядку. Мы увидим практическое применениеэтого принципа далее.20Глава 2.
Лямбда-исчисление2.42.4. КомбинаторыКомбинаторыВпервые понятие комбинатора и основанная на нём теория были сформулированыМ.И. Шейнфинкелем в работе Schönfinkel (1924) ещё до появления λ-исчисления.Вскоре после этого аналогичные результаты были получены Карри, независимо отШейнфинкеля и Чёрча. (Когда Карри ознакомился с работами Шейнфинкеля, онпредпринял попытку с ним связаться, но к этому времени Шейнфинкель оказалсяв психиатрической лечебнице.) В данной работе мы позволим себе не соблюдатьисторическую достоверность, изложив теорию комбинаторов как один из аспектовλ-исчисления.Будем называть комбинатором терм λ-исчисления без свободных переменных.Такие термы также принято называть замкнутыми, поскольку их значениене зависит от значений каких-либо переменных.
В дальнейшем в курсефункционального программирования мы встретимся с большим количествомполезных комбинаторов, но краеугольным камнем теории комбинаторов служит тотфакт, что на самом деле достаточно лишь лишь немногих из них. Оказывается, чтопроизвольный терм может быть выражен при помощи определённого множествакомбинаторов и всевозможных переменных, операция λ-абстракции становитсяненужной. В частности, замкнутый терм может быть представлен исключительночерез эти комбинаторы. Дадим их определения:I = λx. xK = λx y. xS = λf g x. (f x)(g x)Чтобы легче их запомнить, можно воспользоваться простыми мнемоническимиправилами.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 = y, λx. y = K y.8Мы не утверждаем, что эти правила имеют под собой историческую основу.Шейнфинкель использовал обозначение C, но мы предлагаем своё, основанное на нем. Konstant,в честь его немецкого происхождения (автор ошибается, М. И. Шейнфинкель работал в Германии,но родился в России — Прим. перев.)9212.4.
КомбинаторыГлава 2. Лямбда-исчисление• Если t — константа c, то λx. c = K c.• Если t представляет собой комбинацию термов, например, s u, то согласноиндуктивному предположению найдутся термы s0 и u0 , которые не содержатλ-абстракций и для которых справедливы равенства s0 = λx.
s и u0 = λx. u. Изэтого можно сделать вывод, что S s0 u0 является искомым выражением. Всамом деле,S s0 u0 x ====S (λx. s) (λx. u) x((λx. s) x)((λx. u) x)sutТаким образом, применив η-преобразование, мы получаем S s0 u0 =λx. S s0 u0 x = λx. t, поскольку согласно индуктивному предположениюпеременная x не является свободной в термах s0 либо u0 .Теорема 2.7 Для произвольного λ-терма t существует не содержащий λабстракций терм t0 , полученный композицией K, I и переменных, такой,что F V (t0 ) = F V (t) и t0 = t.Доказательство: Применим структурную индукцию к терму t и воспользуемсялеммой 2.6. Например, если терм t имеет вид λx.
s, то мы сначала можемполучить, согласно индуктивному предположению, терм s0 — свободный от λабстракций эквивалент s. Далее применим лемму к λx. s0 . Прочие случаи очевидны.Это примечательное утверждение может быть даже усилено, посколькукомбинатор I выражается через S и K. Отметим, что для произвольного AS K A x = (K x)(A x)= (λy. x)(A x)= xОтсюда, применив η-преобразование, получаем, что I = S K A для любых A.Однако, по причинам, которые станут яснее после знакомства с понятием типа,наиболее удобно положить A = K. Таким образом, I = S K K, что даёт намвозможность устранить все вхождения I в комбинаторные выражения.Заметим, что приведённые выше доказательства имеют конструктивныйхарактер, поскольку предлагают конкретные процедуры получения по заданномутерму эквивалентного комбинаторного выражения. Процесс его построения идётв направлении снизу вверх, и для каждой λ-абстракции, которая по построениюимеет тело, свободное от λ-абстракций, применяются сверху вниз преобразования,изложенные в лемме.Несмотря на то, что мы рассматриваем комбинаторы как некоторые термыλ-исчисления, на их основе можно сформулировать независимую теорию.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
