Введение в функциональное программирование (стр. 3 )

Другое важное свойство (=) состоит в том, что если Е1 = Е2 и если Е1′ и E2′– два л-выражения, которые отличаются только тем, что в той части где E1′ содержит E1, у E2′ содержится E2, тогда E1′ = E2′. Данное свойство получило название свойства Лейбница. Это свойство выполняется, поскольку можно использовать одинаковую последовательность редукций как для перехода от Е1 к Е2 , так и для перехода от Е1′  к  E2′. Например, если E1 = E2 , тогда по правилу Лейбница лV. E1 = лV. E2.

Необходимо, чтобы замена в  α- и  β-редукциях  была эффективной.  Требование эффективности не выполняется, например, при  α-редукции

лx. (лy. x)  к  лy.  (лy. y)  (т. к. y становится связанной после  замены  на  x  в  лy. x). Если была бы произведена такая “некорректная” замена, тогда из определения  (=)  следовало  бы,  что:

  лx.  лy. x =  лy.  лy. y

Но тогда так как

  (лx. (лy. x)) 1 2 → (лy. 1) 2 → 1

  β  β

и

  (лy. (лy. y)) 1 2 → (лy. y) 2 → 2

  β  β

и получается, что 1 = 2. В общем случае, если подставить вместо 1 и 2 любые два выражения, можно доказать, что  они  равны!

Упражнение 3

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

Пример : 

Если V1, V2 , … , Vn не равны друг другу и не имеют свободных вхождений в E1, E2, … , En, тогда

  (лV1 V2 … Vn. E) E1 E2 … En

  = (( лV1. (лV2 … Vn. E)) E1) E2 … En

  → (( лV2 … Vn. E)[E1/V1])E2 … En

  β

  = ( лV2 … Vn. E [E1/V1]) E2 … En 

  . 

  . 

  . 

  = E[E1/V1] [E2/V2] … [En/Vn] 

Упражнение 4

Где было, в последнем примере, сделано предположение что V1, V2, … , Vn различны и не имеют свободных вхождений  в  E1, E2, … , En? 

Упражнение 5

Покажите на примере, что если V1= V2, то тогда даже если V2 имеет свободные вхождения в E1, необязательно будет выполняться

  (лV1V2. E) E1 E2 = E [E1/V1][E2/V2] 

Упражнение 6

Покажите на примере, что если V1 ≠ V2, но V2 имеет свободные вхождения

в  E1 ,  необязательно  будет выполняться

  (лV1V2. E) E1 E2 = E [E1/V1][E2/V2] 

1.6 Отношение →

В предыдущем разделе, было определено, что при Е1 = Е2 , Е2 можно получить из Е1 последовательностью прямых или обратных конверсий. Особый случай этого отношения – когда Е2 можно получить из Е1 только последовательностью прямых конверсий. Записывается это как Е1 → Е2.

  Определение →

Если Е и E’ – л-выражения, тогда Е → E' , если E ≡ E' или существуют выражения Е1, Е2, … , En такие что:

  1.  Е ≡ Е1

  2.  Е′ ≡ En

  3.  Для каждого  i  либо  Ei → Ei+1 ,  либо  Ei → Ei+1 ,  либо  Ei → Ei+1 .

  α  β  η

Обратите внимание, что определение (→) аналогично определению (=), отличие лишь в отсутствии части (b). 

Упражнение 7

Найти Е, Е′ , такие что  Е=E′ ,  но не  E → E′. 

Упражнение 8(повышенной сложности)

Показать, что  если Е1 = Е2 , тогда  существует  такое  Е, что Е1 → Е и Е2 → Е.

( Это свойство называется  теоремой  Чёрча –  Россера.  Некоторые  из следствий  из  этой  теоремы будут обсуждаться в 2.9.)

1.7 Экстенсиональность

Предположим, что V не имеет свободных вхождений в Е1 или Е2 и

  Е1 V = E2 V

Тогда по правилу Лейбница

  лV. E1 V = лV. E2 V

И  после  применения  η-редукции  к  обеим  частям выражения получаем

  Е1 = Е2

Часто  бывает  удобным, используя это свойство, доказать, что два л-выражения эквивалентны,  т. е. доказать  что  Е1 = Е2. Это можно  сделать  доказав,  что Е1 V = E2 V  для  какого-либо  V,  не  имеющего  свободных  вхождений  в  Е1  или Е2. Это  свойство  называется  экстенсиональностью. 

Упражнение 9

Показать что

  (лf g x. f x (g x )) (лx y. x) (лx y. x) = лx. x

1.8 Замена

В начале 1.4 , мы определили E[E′/V] как результат замены E′ на каждое свободное вхождение V в E. Было сказано, что такая замена будет эффективной, если ни одно из свободных E′ не становится связанным в E[E′/V]. В определениях α- и β-конверсий было оговорено, что замены должны быть эффективными. Так, например

  ( лV. E1) E2 → E1[E2/V]

  β

остаётся верным, пока замена E1[E2/V] остаётся эффективной.

Было бы удобно расширить значение E[E′/V] , таким образом, чтобы нам не надо было заботиться об эффективности замены. Этого можно достигнуть введением следующих свойств для всех выражений Е, Е1 и Е2 и всех переменным V и V' :

  (лV. E1) E2 → E1[E2/V]  и  лV. E → лV′. E[V′/V] 

Для того, чтобы обеспечить выполнение этого свойства,  E[E′/V] определяется  рекурсивно на  основе  структуры  E  следующим образом:

E	E[E'/V]
V V′  ( где V ≠ V′) E1 E2 лV. E1 лV′.E1  ( где V ≠ V′ и V′ не   имеет свободных   вхождений в E′) лV′.E1  (где V ≠ V′ и V′ не   имеет свободных   вхождений в E′)	E′ V′ E1[E'/V]  E2[E′/V] лV. E1 лV′. E1[E′/V] лV′′. E1[V′′/V′] [E′/V′] , где V′′ –   переменная, не имеет   свободных вхождений   в E′  или  E1

Такое  подробное  определение  E[E′/V]  основано (но не совпадает ) с определением  из  Appendix C  [2].

Для того, чтобы показать как это работает, рассмотрим (лy. y x)[y/x]. Т. к. y свободна в  y,  применяется последний случай из таблицы. Т. к.  z  не  встречается в  y x  или  y  имеем:

  (лy. y x)[y/x] ≡ лz. (y x)[z/y][y/x] ≡ лz. (z x) [y/x] ≡ лz. z y

В последнем случае из таблицы, выбор V′′ не определен. Подойдет любая переменная, не имеющая свободных вхождений E′ или Е1.

Замена хорошо освещена в книге Хиндей и Селдина[19], где приведены формулировки и доказательства различных технических свойств. Следующее упражнение взято из этой книги.

Упражнение 10

Используйте таблицу для решения

(i)  (лy. x (лx. x)) [( лy. y x) /x].

(ii)  (y (лz. x z)) [(лy. z y) /x]. 

Довольно очевидно ( хотя и несколько утомительно ), доказательство

того, что из определения E[E’/V], приведенного выше, действительно : 

  (лV. E1) E2 → E1 [E2/V]  и  (лV. E → лV′. E[ V′/V] 

для всех выражений E, E1 и E2 и для всех переменных V и V′.

В Главе 3 будет показано, как теорию комбинаторов можно использовать для разложения достаточно сложных замен на более простые операции. Вместо комбинаторов можно использовать так называемые безымянные элементы Де Брейна[6]. Его идея состоит в том, что переменные можно представить как “указатели” на л, которые связывают их. Вместо того, чтобы “помечать” л именами (т. е. связанными переменными) и затем указывать на них через эти имена, можно указывать на соответствующую л, определяя количество уровней  “вверх”  которых  нужно  пройти,  чтобы  достичь их. Например,  лx. лy. x y  будет  представлено  как  лл2 1.  В  качестве  более  сложного примера, рассмотрим следующее выражение, в котором мы определяем количество уровней, разделяющих переменную и  л,  к  которой  она  привязана.

  3

  2

  лx. лy. x y (лy. x y y)

  1  1

В нотации Де Брейна  лл2 1 л3 1 1. 

Свободная переменная в выражении, представляется числом, большим, чем глубина лs  над ней; различные свободные переменные задаются различными числами. Например,

  лx. (лy. y x z) x y w

будет представлено как

  л (л1 2 3) 1 2 4

Т. к. есть лишь две л, над вхождением 3, это число обозначает свободную переменную; похожим образом, есть лишь одна л над вторым вхождением 2 и вхождением 4, значит они тоже должны соответствовать свободным переменным. Заметим, что 2 нельзя использовать для отображения w, т. к. оно уже было использовано для отображения свободной переменной y; таким образом, мы выбираем первое свободное число больше чем 2 ( 3  уже используется для отображения z).

Следует быть внимательным, и назначать достаточно большие числа свободным  переменным. Например,  первое  вхождение  z  в

лx. z (лy. z)  можно  представить 2, но второму вхождению нужно 3 ; так как, это одна  и та же переменная, мы  должны  использовать  3. 

Пример : 

По схеме Де Брейна  лx. x (лy. x y y)  будет  представлено  л1(л2 1 1). 

Упражнение 11

Каким  л-выражением  представляется  л2(л2) ?   

Упражнение 12

Опишите алгоритм вычисления по Де Брейну представления выражения E[E′/V]  из  представления  E  и  E′. 

Глава 2

Различные  представления  в  л-исчислении.

На первый взгляд, л-исчисление может показаться очень примитивным языком. Но его можно использовать для представления большинства объектов и структур нужных в современном программировании. Для этого следует задать эти объекты и структуры таким способом, чтобы у них были необходимые свойства. Например, для того чтобы представить значения истинности  true  и  false  булевской  функции ¬ (“не”),