Обобщенные л-абстракции
LET л(V1, … , Vn). E = uncurryn (лV1 … Vn. E)
Пример : л (x, y). mult x y означает:
2 2
uncurry2 (лx y. mult x y ) = (лf p. f (p↓1)(p↓2))( лx y. mult x y)
= (лf p. f ( fst p)(snd p)) (лx y. mult x y)
= лp. mult (fst p)(snd p)
Таким образом:
(л(x, y). mult x y)(E1,E2) = (лp. mult (fst p) (snd p)) (E1,E2)
= mult (fst(E1,E2))(snd(E1,E2))
= mult E1 E2
Этот пример показывает правило обобщенной β-конверсий, приведенное ниже в таблице. Это правило можно получить из оригинальной
β-конверсии, определения картежей и обобщенной л-абстракции. Идея состоит в том, что кортеж аргументов последовательно подходит к каждой позиции аргументов в теле обобщенной абстракции; затем каждый отдельный аргумент может быть извлечен из кортежа не затрагивая остальные.
Обобщенная β-конверсия
(л(V1, … , Vn) . E)(E1, … , En) = E[E1, … , En/V1, … ,Vn]
где E[E1, … , En/V1, … ,Vn] – одновременная подстановка E1, … , En на V1, … , Vn соответственно, и ни одна из этих переменных не имеет свободных вхождений в E1, … , En.
Удобно расширить нотацию лV1 V2… Vn. Е, описанную в начале книги,
так чтобы каждое Vi было либо идентификатором, либо кортежем идентификаторов. лV1 V2… Vn. Е всё ещё значит лV1.( лV2.(…( лVn. E) … )), но теперь если Vi – кортеж идентификаторов, тогда выражение является обобщенной абстракцией.
Пример: лf (x, y). f x y означает лf. (л(x, y). f x y) , что в свою очередь значит лf. uncurry (лx y. f x y) равное лf. (лp. f (fst p)(snd p)).
Упражнение 29
Показать, что если единственные свободные переменные в E это x1 , … , xn и f, тогда, если
f = Y (лf ( x1 , … , xn).E)
тогда
f(x1 , … , xn) = E[f/f]
Упражнение 30
Определить л-выражение div со свойством:
div (m, n) = (q, r)
где q и r – частное и остаток деления n на m.
2.6 Взаимная рекурсия
Для решения набора взаимно рекурсивных выражений таких как следующие:
f1 = F1 f1 … fn
f2 = F2 f1 … fn
.
.
.
fn = Fn f1 … fn
мы просто определим для 1 ≤ i ≤ n
fi = Y (л(f1, … fn).(F1 f1, … fn, … , Fn f1, … fn))↓ i
Это выполняется, поскольку если
→
f = Y (л(f1, … fn).(F1 f1, … fn, … , Fn f1, … fn))
→
тогда fi = f↓i, и отсюда следует что:
→ →
f = (л(f1, … fn).(F1 f1, … fn, … , Fn f1, … fn)) f
→ → → →
= (F1(f↓1)…(f↓n), … , Fn(f↓1) … (f↓n))
→
= (F1 f1 … fn, … , Fn f1 … fn) (т. к. f↓i = fi).
Отсюда:
fi = Fi f1 … fn
2.7 Представление рекурсивных функций
Важный класс числовых функций – рекурсивные функции. Вскоре после того, как Чёрч придумал л-исчисление, Клин доказал, что в л-исчислении может быть представлена любая рекурсивная функция. Это послужило доказательством тезиса Чёрча – гипотезы о том, что любая интуитивно вычислимая функция может быть представлена л-исчислением. Было показано, то другие вычислительные модели определяют тот же класс функций, что и л-исчисление.
В этом разделе будет описано что означает представление арифметических функций л-исчислением. Будут определены два класса функций, примитивно - рекурсивные функции и рекурсивные функции, и будет показано, что все функции этих классов могут быть представлены л-исчислением.
В разделе 2.3 было объяснено, как число n представляется с помощью л-выражения n. Говорят, что л-выражение f представляет математическую функцию f, если для всех чисел x1 , … , xn :
f (x1 , … , xn) = y если f (x1 , … , xn) = y
2.7.1 Примитивно-рекурсивные функции
Функция называется примитивно рекурсивной, если её можно создать из 0 и функций S и Uin (определенные ниже) конечной последовательностью применений операторов подстановки и примитивной рекурсии ( также определенных ниже). Функция наследования S и функция проектирующая Uin ( где все n и i – числа), определяются следующим образом:
S(x) = x + 1 Uin(x1 , … , xn) = xi
Подстановка
Предположим, g – функция r аргументов, а h1, … , hr – r - функций с
n аргументами каждая. Мы считаем, что f определяется из g и h1, … , hr подстановкой, если :
f (x1 , … , xn) = g ( h1(x1 , … , xn), … , hr (x1 , … , xn))
Примитивная рекурсия
Предположим, g – функция n-1 аргумента и h – функция n+1 аргументов. Мы считаем, что f определяется из g и h примитивной рекурсией, если:
f(0, x2 , … , xn) = g (x2 , … , xn)
f(S(x1), x2 , … , xn) = h (f(x1 , … , xn), x1 , x2, … , xn)
g называется базовой функцией, а h – ступенчатой функцией. Можно доказать, что для любых базовой и ступенчатой функции всегда существует уникальная функция, определенная из них примитивной рекурсией. Этот результат называется рекурсивной теоремой; доказательство теоремы можно найти в книгах по математической логике.
Пример
Функция сложения sum – примитивно рекурсивная, поскольку:
sum(0, x2) = x2
sum(S(x1), x2) = S(sum(x1, x2))
Теперь покажем, что любая примитивно рекурсивная функция может быть представлена л-выражениями.
n
Очевидно, что л-выражения 0, suc, лp. p↓i представляют исходные функции 0, S и Uin соответственно.
Предположим, что функции g r - переменных представляется как g, а функции hi ( 1 ≤ i ≤ r ) n - переменных представляются как hi. Тогда, если функция f n - переменных определятся подстановкой :
f(x1 , … , xn) = g(h1(x1 , … , xn), … , hr(x1 , … , xn))
тогда f представляется f, где :
f = л(x1 , … , xn). g(h1(x1 , … , xn), … , hr(x1 , … , xn)).
Предположим функция f n - переменных индуктивно определяется из базовой функции g n-1- переменных и из индуктивного шага функции h n+1- переменной. Тогда
f(0, x2 , … , xn) = g(x2 , … , xn)
f(S(x1), x2 , … , xn) = h (f (x1 , … , xn), x1 , … , xn)
Таким образом, если g представляет g, а h представляет h, тогда f будет представлять f если
f(x1,x2, … , xn) = (iszero x1 → g(x2 , … , xn)|
h(f(pre x1,x2, … , xn), pre x1,x2, … , xn))
Используя метод неподвижной точки, функция f, чтобы удовлетворять
этому уравнению, должна быть создана следующим способом :
Y (лf. л (x1,x2, …, xn ).
( iszero x1 → g ( x2, …, xn) |
h (f (pre x1, x2, …, xn), pre x1, x2, …, xn )))
Таким образом, любая примитивно рекурсивная функция может быть представлена λ-выражением.
2.7.2 Рекурсивные функции
Функция называется рекурсивной, если она может быть создана из 0, функции наследования и проектирующей функции последовательностью подстановок, примитивных рекурсий и минимизаций.
Минимизация
Предположим функция g – функция n - аргументов. Мы считаем, что f определяется из g минимизацией, если :
f(x1 , … , xn) = “наименьшее y, такое что g(y, x2 , … , xn ) = x1”
Обозначение MIN(f) используется для обозначения минимизации функции f. Функции, определенные минимизацией, могут быть неопределенны при некоторых аргументах. Например, если one есть функция которая всё время возвращает 1, т. е. one(x) = 1 для любого x, тогда MIN(one) определена только для аргумента со значением 1. Это очевидно потому, что если f (x) = MIN(one)(x), тогда :
f(x) = “наименьшее y, такое что one(y) = x”
и очевидно что это выражение определено только для x= 1 . Таким образом:
MIN(one)(x) = 0 если x = 1
иначе неопределенно
Чтобы показать, что любую рекурсивную функцию можно представить в
λ-исчислении, необходимо показать как представить минимизацию произвольной функции. Предположим g представляется функцию g
n - переменных, а f определятся так :
f = MIN(g)
Тогда, если можно придумать такое λ-выражение min, что min x f (x1 , … , xn) представляет собой наименьшее число y больше чем x такое, что
f(y, x2 , … , xn) = x1
тогда g представляет g, где :
g = λ( x1 , … , xn). min 0 f (x1 , … , xn)
min будет точно обладать желаемым свойством если:
min x f (x1 , … , xn) =
(eq (f(x, x2 , … , xn)) x1 ) → x | min (suc x) f (x1 , … , xn))
где eq m n принимает значение true, если m = n, иначе - false. Таким образом min можно просто определить так:
Y(λm. λx f (x1 , … , xn). (eq (f(x, x2 , … , xn)) x1 → x | m ( suc x ) f (x2 , … , xn)))
Таким образом, любая рекурсивная функция может быть определена
λ-выражением.
Примитивные рекурсии старших порядков
Существуют рекурсивные функции, которые не являются примитивно рекурсивными. Ниже представлена одна из версий функции Акермана ψ,
|
Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6 7 8 9 10 11 |
