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

определённая так :

  ψ(0,n) = n+1

  ψ(m+1,0) = ψ(m,1)

  ψ(m+1,n+1) = ψ(m,ψ(m+1,n))

Однако, если позволить функциям принимать роль аргументов, тогда гораздо больше рекурсивных функций можно определить с помощью примитивной рекурсии. Например, если функция  старшего порядка  rec  определяется примитивной рекурсией следующим образом:

  rec(0, x2, x3) = x2

  rec (S (x1), x2, x3) = x3 (rec (x1 , x2 , x3))

тогда ψ определяется так:

  ψ (m, n) = rec (m, S, f → ( x → rec ( x, f(1),f))) (n)

где x → θ(x) соответствует функции ( обратите внимание, что λx.θ(x) –

λ-выражение, где x → θ(x) – обозначение неформализованной математики) , которая отображает x в θ(x). Обратите  внимание  на  то, что  третий  аргумент  функции  rec, а  именно  x3  должен быть  функцией.

В определении ψ  мы также использовали x2 как  функцию, т. е. S.

Упражнение 31

Показать, что определение ψ  через rec работает, т. е. что с определением ψ, данным  выше:

  ψ(0,n) = n+1

  ψ(m+1,0) = ψ(m,1)

  ψ(m+1,n+1) = ψ(m,ψ(m+1,n))

Функция, которая использует другие функции в качестве аргументов, или возвращает другую функцию в качестве результата, называется функцией старшего порядка. Пример ψ показывает, что примитивная рекурсия старшего порядка сильнее, чем обычная примитивная рекурсия ( примитивная рекурсия, определенная в 2.7.1 называется примитивной рекурсией первого порядка). Использование  операторов  наподобие  rec  делает  функциональное программирование  могучим  инструментом.

2.7.3 Частично рекурсивные функции

Частичные  функции -  функции, определенные  не  для  всех  аргументов. Например, функция MIN(one), описанная выше – частичная. Другим примером может  служить  функция  деления, поскольку  деление  на  0  неопределенно. Функции, определенные  для  всех  аргументов  называются  полными.

Частичная функция называется частично рекурсивной если она может быть создана из 0, функции наследования и функции отображения  с  помощью последовательности  подстановок, примитивных рекурсий и минимизаций. Таким образом, рекурсивные функции – это частично рекурсивные функции, оказавшиеся полными. Можно показать, что любая частично  рекурсивная функция f может быть представлена λ-выражением  f  таким  что:

f(x1 , … , xn) = y,  если f (x1 , … , xn) = y если f (x1 , … , xn)  неопределена, тогда  f (x1 , … , xn)  не  имеет

  нормальной  формы.

Обратите внимание  на то, что  несмотря  на  (ii) , в общем случае неверно считать  “неопреденными”  выражения  без  нормальной  формы.

Упражнение 32

Напишите λ-выражение которое представляет MIN(f) , где f(x)= 0 для всех x.

2.8 Расширенное λ-исчисление.

Несмотря на возможность представления объектов данных и структур данных с помощью λ-выражений, часто это бывает неэффективно. Например, большинство компьютеров приспособлены для арифметических вычислений, и  будет разумнее  использовать  для  вычисления  чисел  именно их, нежели

λ-конверсию.  Математически ясный  способ  представления  правил  в 

λ-исчислении – это представление с  помощью  так  называемых  δ-правил.

Идея  заключается  в  том, чтобы добавить  набор  новых  констант  и  потом

определить  так  называемые δ-правила  для  того, чтобы редуцировать  выражения с этими  константами. Например, можно  было  бы  добавить числа  и  “ +“  как  новые  константы и, вместе  с δ-правилом, было  бы: 

  + m n → m+n

  δ

(E1→E2 означает, что Е2 – результат применения δ-правил к подвыражению Е1).

  δ

Добавляя такие константы и правила в λ-исчисления, следует быть внимательным, чтобы не нарушить прекрасные свойства этого исчисления,

например  Теорему Чёрча-Россера.

Можно показать, что δ-правила безопасны, если они представлены в форме:

  c1 c2 … cn  → e

  δ

где c1 ,c2 …, cn – константы, а e – либо константа, либо закрытая абстракция

( такие λ-выражения иногда называют значениями).

Например, можно добавить Suc, Pre, IsZero, Δ0, Δ1, Δ2, … как  константы

с помощью δ-правил:

  Suc Δn  → Δn+1

  δ

  Pre Δn+1 → Δn

  δ

  IsZero Δ0 → true

  δ

  IsZero Δn+1 → false

  δ

Здесь Δn представляет число n, Suc, Pre, IsZero  это новые константы

( неопределенные λ-выражения наподобие suc, pre, iszero ), а true и false – ранее определенные выражения (оба – закрытые абстракции).

2.9 Теоремы λ-исчисления.

Если Е1 → Е2, тогда можно говорить, что Е2 получена из Е1 “вычислением”. Если в Е2 нет( β-  или  η-) редексов, тогда Е2 – “полностью вычисленное”.

Говорят, что λ-выражение  находится  в  нормальной  форме если в нем нет β-  или η- редексов ( т. е. единственная конверсия, которая может быть применена – это α-конверсия). Таким образом, λ-выражение в нормальной форме является  “полностью вычисленным”.

Примеры
Представление чисел находится в нормальной форме. ( λx. x) 0 – не является нормальной  формой.

Предположим, что λ-выражение  вычисляется  двумя разными способами применением двух различных последовательностей редукций  до  получения  двух  нормальных  форм  Е1 и Е2. Теорема Чёрча-Россера, приведенная ниже, показывает, что Е1 и Е2 будут одинаковыми, за исключением того, что у них могут быть различные имена связанных переменных.

Из-за того, что результат редукций не зависит от  последовательности  их

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

В настоящее время различные исследовательские проекты направлены на то, чтобы  использовать  этот  факт  путём  создания  мультипроцессорной архитектуры  для  вычисления  λ-выражений. Сейчас  ещё  слишком  рано говорить, насколько  успешны  эти  разработки. Может  оказаться, что проблемы, связанные с  распределением  редексов  на  разные процессоры  и последующим  сбором  результатов, сведут  на  нет  все  теоретические преимущества  данного  подхода.  Всё  же  будем  надеяться, что  эти 

пессимистичные  прогнозы  не  оправдаются. Замечательным фактом является то, что теорема Чёрча-Россера, являющаяся чисто математическим результатом  и  сформулированная  ещё  до  того  как  были  созданы компьютеры, может привести к созданию нового поколения компьютеров.

Ниже приведена формулировка теоремы Чёрча-Россера. На её примере хорошо видно, что есть весьма очевидные вещи, которые тем не менее очень трудно доказать. Многие свойства λ-исчисления имеют схожую природу.

  Теорема Чёрча-Россера

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

Теперь  видно,  каким  образом  теорема  Чёрча-Россера  показывает, что

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

разных последовательностей редукций до получения  двух  нормальных форм  Е1  и  Е2. Т. к. Е1 и Е2 получены из Е последовательностью конверсий, из определения =, следует что Е = Е1 и Е = Е2 и, следовательно, Е1 = Е2. Из теоремы Чёрча-Россера следует, что существует такое выражение Е′ , что

Е1 →Е′ и Е2 → Е′. Теперь, если Е1 и Е2 находятся в нормальной форме, тогда единственными редексами, которые в них содержатся будут α-редексами и поэтому единственным способом, которым Е1 и Е2 можно свести к  E′, будет изменение имен связанных  переменных (т. е. α-конверсия).

С помощью теоремы Чёрча-Россера также можно показать, что если m ≠ n, тогда λ-выражения, соответствующие m и n не эквивалентны, т. е. m ≠ n. Предположим, что m ≠ n, но m = n. Тогда по теореме Чёрча-Россера m → E и

n → E  для  какого-нибудь  Е. Но  это  очевидно из определений m  и  n, то  есть:

  m = λf x. fm x

  n =  λf x. fn x

очевидно, что такое Е не может существовать. Единственными конверсиями, которые могут быть применены к m и n являются α-конверсии, а они не могут изменить число аппликаций в выражении  (m содержит m аппликаций, а n содержит  n аппликаций).

λ-выражение Е  имеет нормальную форму, если  Е = Е′  для  какой  либо  Е′ в нормальной  форме. Следствие, приведенное  ниже,  показывает отношения выражений  в  нормальной  форме  и  имеющих  нормальную  форму. Оно обобщает  утверждения  приведенные  выше. 

  Следствие из теоремы Чёрча-Россера

Если Е имеет нормальную форму, тогда Е → Е′ , для Е′

  в  нормальной форме.