John Harrison - Введение в функциональное программирование (1108517), страница 6
Текст из файла (страница 6)
Наконец, если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. На первый взгляд, рекуррентноеопределение понятия подстановки выглядит так:x[t/x]y[t/x]c[t/x](s1 s2 )[t/x](λx. s)[t/x](λy. s)[t/x]======ty, если x 6= ycs1 [t/x] s2 [t/x]λx. sλy. (s[t/x]), если x 6= y14Глава 2. Лямбда-исчисление2.3. Лямбда-исчисление как формальная системаК сожалению, это определение не совсем верно. Например, подстановка (λy. x +y)[y/x] = λy. y + y не соответствует интуитивным ожиданиям от ее результата.3Исходный λ-терм интерпретировался как функция, прибавляющая x к своемуаргументу, так что после подстановки мы ожидали получить функцию, котораяприбавляет y, а на деле получили функцию, которая свой аргумент удваивает.Источником проблемы служит захват переменной y, которую мы подставляем,операцией λy.
. . ., которая связывает одноименную переменную. Чтобы этого непроизошло, связанную переменную требуется предварительно переименовать:(λy. x + y) = (λw. x + w),а лишь затем производить подстановку:(λw. x + w)[y/x] = λw. y + wСуществуют два подхода к решению этой проблемы. С одной стороны, можноусловиться, что подстановка недопустима в ситуации захвата переменной, а сдругой — расширить формальное определение подстановки таким образом, чтобытребуемое переименование переменных происходило автоматически. Мы остановимсяна последнем варианте:x[t/x]y[t/x]c[t/x](s1 s2 )[t/x](λx. s)[t/x](λy.
s)[t/x](λy. s)[t/x]=======ty, если x 6= ycs1 [t/x] s2 [t/x]λx. sλy. (s[t/x]), если x 6= y и либо x 6∈ F V (s), либо y 6∈ F V (t)λz. (s[z/y][t/x]) в противном случае, причём z 6∈ F V (s) ∪ F V (t)Единственное отличие этого определения заключается в двух последнихправилах. Мы следуем предыдущему определению в двух безопасных ситуациях,когда либо переменная x не свободна в терме s, так что подстановка оказываетсятривиальной, либо когда y не свободна в t, так что захват переменной не произойдет(на данном уровне). Однако, в случае, когда оба эти условия не выполняются, мыпредварительно переименовываем переменную y в z, выбранную так, чтобы она небыла свободной ни в терме s, ни в терме t, после чего продолжаем, как описано выше.Для определенности, переменная z может выбираться некоторым фиксированнымспособом, например, как первая в лексикографическом порядке имен переменная измножества всех переменных, не имеющих свободных вхождений ни в s, ни в t.43Строго говоря, нам следовало бы писать + x y, нежели x + y, но мы будем, как прежде,использовать стандартные операции в инфиксной форме.4Знатоки могут быть обеспокоены тем, что последнее правило не позволяет считатьэто определение примитивно-рекурсивным.
Однако, его легко преобразовать в примитивнорекурсивную множественную параллельную подстановку. Подобная процедура напоминаетусиление индуктивного предположения в ходе доказательства. Отметим, что по построению параподстановок в последнем правиле может осуществляться как параллельно, так и последовательнобез ущерба для результата.152.3.
Лямбда-исчисление как формальная система2.3.4Глава 2. Лямбда-исчислениеПреобразованияЕщё одной из основ λ-исчисления служат три «преобразования» — операцииполучения по заданному терму другого, равного ему в интуитивном смысле.Традиционно их обозначают буквами греческого алфавита: α (альфа), β (бета) и η(эта).5 Приведём формальные определения этих операций, обозначив каждую из нихпомеченной стрелкой.• Альфа-преобразование: λx. s −→λy. s[y/x], при условии, что y 6∈ F V (s).αНапример, λu. u v −→ λw. w v, но λu.
u v 6−→ λv. v v. Такое ограничениеααустраняет возможность еще одного случая захвата переменной.• Бета-преобразование: (λx. s) t −→ s[t/x].β• Эта-преобразование: λx. t x −→t, если x 6∈ F V (t). Например, λu. v u −→v,ηηно λu. u u 6−→u.ηСреди этих трех операций наиболее важной для нас является β-преобразование,поскольку оно соответствует вычислению функции для заданного аргумента. В тоже время, α-преобразование играет роль вспомогательного средства переименованиясвязанных переменных, а η-преобразование представляет собой разновидностьэкстенсиональности, в силу чего интересно главным образом с точки зрения логика,а не программиста.2.3.5Равенство λ-выраженийИспользуя приведённые выше правила преобразований, мы можем определитьформально условия, при которых два λ-терма считаются равными.
В общих чертах,два терма равны, если один из них может быть получен из другого в ходеконечной последовательности α, β либо η-преобразований, которые применяютсяк произвольным подтермам как в прямом, так и в обратном направлении.Другими словами, отношение λ-равенства представляет собой congruence closureтрёх преобразований и обладает свойствами рефлексивности, симметричности,транзитивности и заменяемости. Ниже приводится формальное индуктивноеопределение, правила которого трактуются следующим образом: если утверждениенад горизонтальной чертой выполняется, то справедливо и утверждение под ней.s −→ t или s −→ t или s −→ tαβηs=tt=ts=tt=ss=tиt=us=u5Такие имена преобразований были введены Карри.
Первоначально Чёрч называл α- и βпреобразования «правило действий I» и «правило действий II» соответственно.16Глава 2. Лямбда-исчисление2.3. Лямбда-исчисление как формальная системаs=tsu=tus=tus=uts=tλx. s = λx. tОтметим, что использование обычного знака равенства (=) в данном контекстеможет ввести в заблуждение. В самом деле, мы задаём некоторое отношениеλ-равенства, взаимосвязь которого с понятием равенства соответствующихматематических объектов остаётся неясной.6 В то же время очевидно, что следуетотличать λ-равенство от синтаксического. Последнее будем называть «тождеством»и обозначим символом ≡.
Например, λx. x 6≡ λ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. На этом мызавершаем обсуждение сущности η-преобразования и его влияния на теорию в целом,чтобы уделить больше внимания более перспективному с точки зрения вычислимостиβ-преобразованию.6Действительно, ведь мы не определяем достаточно точно, каково это соответствие само по себе.Тем не менее, существуют модели λ-исчисления, в которых λ-равенство трактуется как обычное.172.3.
Лямбда-исчисление как формальная система2.3.7Глава 2. Лямбда-исчислениеλ-редукцияОтношение λ-равенства, как и следовало ожидать, является симметричным. Онодостаточно хорошо соответствует интуитивному понятию эквивалентности λ-термов,но с алгоритмической точки зрения более интересен его несимметричный аналог.Определим отношение редукции −→ следующим образом:s −→t или s −→ t или s −→tαηβs −→ tt −→ ts −→ t и t −→ us −→ us −→ ts u −→ t us −→ tu s −→ u ts −→ tλx. s −→ λx. tВ действительности слово «редукция» (в частности, термин β-редукция, которыминогда называют β-преобразования) не отражает точно сути происходящего,поскольку в процессе редукции терм может увеличиваться, например:(λx. x x x) (λx. x x x) −→ (λx. x x x) (λx.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
