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

Правила л-конверсии.

●  α-конверсия.

  Любая абстракция вида лV. E может быть преобразована в

  лV'. E [V'/V]  при условии, что замена V'  на V  является 

  эффективной.

● β-конверсия.

  Любая  аппликация  вида  (лV. E1) E2  может  быть  преобразована 

  в  E1[ E2/V] ,  при условии, что замена E2  на  V  в  E1  является

  эффективной.

● η-конверсия

  Любая  абстракция  вида  лV. ( E V ) , в  которой  нет  свободных

  вхождений  V  в  E, может  быть  преобразована  в  E.

Мы будем использовать следующие нотации:

● E1 → E2, означает  α-конверсию  E1  в  E2.

  α 

● E1 → E2, означает β-конверсию  E1  в  E2.

  β

● E1 → E2, означает η-конверсию  E1  в  E2.

  η

В 1.4.4 эти нотации будут расширены.

Самым важным типом конверсии является β-конверсия; именно её можно использовать для моделирования механизма случайных вычислений.

α-конверсия используется для технической манипуляции связанными переменными, η-конверсия иллюстрирует тот факт, что две функции которые при одинаковых аргументах всегда выдают одни и тоже результаты, являются эквивалентными. ( см. 1.7). Следующие три подраздела, дают более развернутое описание и примеры всех трёх типов конверсий ( обратите внимание, что “конверсия” и ”редукция” используются как синонимы).

1.4.1 α-конверсия

л-выражение ( обязательно абстракция ), к  которому  может  быть  применена  α-конверсия,  называется  α-редексом.  “Редекс”  расшифровывается  как  “ выражение, допускающее  уменьшение ” ( от английского “reducible expression”). Правило  α-конверсии  утверждает, что связанные  переменные могут  быть  переименованы  при  отсутствии  “коллизий”. 

Пример:

  лx. x → лy. y

  α

  лx. f x → лy. f y

  α

Неверно, что

  лx. лy. add x y → лy. лy. add y y

  α

потому  что  замена  (лy. add x y) [y/x]  не является эффективной, т. к. у, который заменяет  х, становится  связанным.  € 

1.4.2 β-конверсия 

л-выражение ( обязательно аппликация ), к которому можно применить β-конверсию, называется β-редексом. Правила β-конверсии аналогично вызову функции в языках программирования: тело Е1 функции  лV. E1 вычисляется в  окружении, в  котором  “формальный параметр ” V привязан  к  “фактическому параметру” E2.

Пример:

  (лx. f x ) E → f E

  β

  (лx. (лy. add x y)) 3 → лy. add 3 y

  β

  (лy. add 3 y) 4 → add 3 4

  β

Неверно что

  (лx. (лy. add x y)) ( square y) → лy. add (square y) y

потому что замена  ( лy. add x y )[( square y)/x]  не является эффективной  т. к.  y свободна  в (square y) ,но становится связанной после замены на х в (лy. add x y ).

Требуется практика, для того что правильно проанализировать

л-выражение, следуя соглашениям, приведенным в 1.2, для того чтобы определить β-редексы. Например, рассмотрим аппликацию:

  (лx. лy. add x y) 3 4.

расстановка скобок, согласно соглашениям, приводит выражение к такому  виду:

  (((лx. (лy. (( add x) y ))) 3) 4)

Это выражение можно переписать в виде:

  ((лx. E) 3) 4  ,  где  E = (лy. add x y)

(лx. E) 3  является  β-редексом  и  может  быть  приведено  к  E[3/x].

1.4.3 η-конверсия

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

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

η-конверсия, обеспечивает, что лx. (sin x) и sin соответствуют одной и той же функции. В общем виде,  лV. (E V)  представляет собой функцию, которая будучи  применена  к  аргументу  E' ,  даёт

(E V)[E'/V].  Если  у  V  нет  свободных  вхождений  в  E,  тогда

(E V)[E'/V] = (E E'). Таким  образом,  лV. E V  и  E  дают один и тот же результат – E E' , когда применяются к одинаковым аргументам, из этого следует, что они соответствуют одной функции.

Пример:

  лx. add x → add

  η

  лy. add x y → add x

  η

Неверно что

  лx. add x x → add x

  η

потому что переменная х – свободна  в  add x.   

1.4.4 Обобщенные конверсии

Определения →  ,  →  и  → могут быть сведены к следующему:

  α  β  η

● E1 → E2 , если Е2 можно получить из Е1, α-конверсией какого - либо

  α  подвыражения.

● E1 → E2 , если Е2 можно получить из Е1, β-конверсией какого - либо

  β  подвыражения.

● E1 → E2 , если Е2 можно получить из Е1, η-конверсией какого - либо

подвыражения. 

Примеры 

  ((лх. лy. add х у) 3) 4 → (лy. add 3 y) 4 

  β

  (лy. add 3 y) 4 → add 3 4   

  β

Первое из этих выражений представляет собой β-конверсию в обобщенном виде, т. к.  (лy. add 3 y) 4  получено из  выражения 

((лx. лy. add  x y) 3 4  (которое само по себе не является β-редексом), сокращением подвыражения (лx. лy. add x y) 3 . Иногда мы будем записывать последовательность конверсий. Тогда пример, описанный выше будет выглядеть так: 

  ((лx. лy. add x y) 3) 4 → (лy. add 3 y) 4 → add 3 4

  β  β

Упражнение 2

Какие из трех данных β-конверсий являются обобщенными конверсиями ( т. е. редукциями подвыражений ) и какие являются конверсиями, по определению данному в 1.4? 

(i)  (лx. x ) 1 → 1

  β

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

  β  β 

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

β

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

Важным свойством β-редукций является то, что неважно в какой последовательности их проводить – результат всегда будет один и тот же. Если есть несколько отдельных редексов в выражении, редукцию можно выполнять параллельно. Необходимо заметить, что некоторые последовательности редукций, могут никогда не завершиться. Это будет обсуждаться в связи  с  Теоремой Нормализации в 2.9. В настоящее время, разработка процессора, используещего  параллельные вычисления для ускорения работы функциональных программ является важной научно-исследовательской  задачей  в  “вычислительной  технике  пятого поколения”.

1.5 Эквивалентность л-выражений

Три правила конверсии определяют значение л-выражений, т. е. если Е1 можно преобразовать в Е2, то Е1 и Е2 соответствуют одной и той же функции. Это свойство конверсий должно быть интуитивно понятно. Можно дать математическое определение функции соответствующей л-выражению и затем доказать,  что она остаётся неизменной при α-, β- и  η-конверсиях. Как показала практика, сделать это оказалось достаточно трудно [33] и мы оставим это за рамками данной книги.

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

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

лx. x эквивалентно лy. y, но не тождественно. Будем использовать следующие обозначения:

● E1 ≡ E2, означает тождественность  E1  и  E2.

● E2 = E2, означает эквивалентность  E1  и  Е2.

Эквивалетность (=) можно определить в терминах тождественности (≡) и конверсий ( → , → и → ) следующим образом.

  α  β  η

  Эквивалентность л-выражений

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

1. Е ≡ Е1

2. Е' ≡ En

3. Для каждого i  либо

(а)  Ei →Ei+1  или  Ei →Ei+1  или  Ei → Ei+1 ,  либо

  α  β  η

  (b)  Ei+1 → Ei  или  Ei+1 → Ei  или  Ei+1 → Ei

  α  β  η

Примеры

  (лx. x) 1 = 1

  (лx. x) (( лy. y) 1) = 1

  (лx. лy. add x y) 3 4 = add 3 4

Из  определения  (=)  следует,  что:

  (i)  Для любого  Е,  верно что  Е = Е  (эквивалентность рефлексивна).

  (ii)  Если  Е = Е' , тогда  E' = E  (эквивалентность  симметрична).

Если  Е = Е' и E' = E'' , тогда E = E''  (эквивалентность транзитивна).

Если отношение  рефлексивно, симметрично и транзитивно, то оно называется отношением эквивалентности. Таким образом, (=) – отношение эквивалентности.