= n-1 (по определению n-1)
Упражнение 19
Используя результаты предыдущего упражнения показать, что
(i) pre (suc n) = n
(ii) pre 0 = 0
Система чисел в следующем упражнении, используется в [2] и имеет ряд преимуществ над системой Черча (например легче определить функцию предшествования).
Упражнение 20
^
LET 0 = лx. x
^ ^
LET 1 = (false, 0)
^ ^
LET 2 = (false, 1)
.
.
--^-- ^
LET n+1 = (false, n)
.
.
. --^-- - --^--- --^--
Придумайте такие л-выражения suc, iszero, pre, чтобы для всех n выполнялось:
--^--- ^ ---^--
suc n = n+1--^---- ^ ---^----
iszero 0 = true---^---- -^-- ^
iszero (suc n) = false-^-- -^-- ^ ^
pre (suc n) = nРекурсивные определения
Чтобы представить функцию умножения в л-исчислении, нам нужно определить л-выражение ( скажем mult ), такое что:
mult m n = add n (add n (… (add n 0 ) … ))
m adds
Этого можно достигнуть, если mult будет определено таким образом, чтобы выполнялось равенство :
mult m n = ( iszero m → 0│add n ( mult ( pre m) n ))
Если это равенство выполняется, тогда, например:
Mult 2 3 = (iszero 2 → 0 | add 3 (mult (pre 2) 3)) ( из равенства )
= add 3 (mult 1 3) ( из свойств iszero, условного
высказывания и pre )
= add 3 (iszero 1 → 0 | add 3 ( mult ( pre 1) 3)) (из равенства)
= add 3 ( add 3 (mult 0 3)) ( из свойств iszero, условного
высказывания и pre )
= add 3 ( add 3 (iszero 0 → 0 | add 3 (mult (pre 0) 3)))
( из равенства )
= add 3(add 3 0) ( из свойств iszero и
условного высказывания )
Равенство, приведенное выше, предполагает, что mult должно быть определено следующим образом:
Mult = лm n. (iszero m → 0 | add n ( mult (pre m) n ))
↑
N. B.
К сожалению, данное выражение нельзя использовать как определение mult, потому что, как показано стрелкой, mult должно быть уже определено, чтобы л-выражение имело смысл.
К счастью, существует способ создания л-выражения, которое удовлетворяет произвольным равенствам. Когда этот способ применяется к описанному выше равенству, он даёт желаемое определение mult. Сначала определим л - выражение Y так, чтобы для любого выражения Е, оно имело такое свойство:
Y E = E ( Y E )
Это значит, что выражение Y E остаётся неизменным, когда к нему применяется функция Е. В общем случае, если E E′ = E′ , тогда E′ называется неподвижной точкой Е. л-выражение Fix со свойством Fix E = E(Fix E) для любого Е, называется оператором неподвижной точки.
Существует бесконечное множество различных операторов неподвижной точки [28]; Y – самый известный из них. Он определяется следующим способом:
LET Y = лf. (лx. f(x x)) (лx. f(x x))
Легко показать, что Y на самом деле – оператор неподвижной точки :
Y E = (лf. (лx. f(x x)) (лx. f(x x))) E ( по определению Y )
= (лx. E(x x)) (лx. E(x x)) ( β-конверсия )
= (лx. E(x x)) (лx. E(x x)) ( β-конверсия )
= (лx. E(x x)) (лx. E(x x)) ( β-конверсия )
= E (Y E) (предпоследняя строчка)
Эти вычисления показывают, что у любого л-выражения E есть неподвижная точка. Вооружившись Y, мы теперь можем вернуться к проблеме решения уравнения для mult.
Предположим, что multfn определяется так:
LET multfn = лf m n. ( iszero m → 0 ) | add n ( f (pre m) n))
- ↑
и multfn определяется так:
LET mult = Y multfn
Тогда:
mult m n = (Y multfn ) m n ( по определению mult )
= multfn ( Y multfn ) m n (свойство неподвижной точки Y)
= multfn mult m n ( по определению mult )
= (лf m n, ( iszero m → 0 | add n ( f (pre m ) n))) mult m n
( по определению multfn )
= (iszero m → 0 | add n (mult ( pre m) n )) ( β-конверсия )
Уравнение вида f x1 … xn = E называется рекурсивным, если f имеет свободные вхождения в E. Y даёт общий способ решения таких уравнений. Начнем с уравнения вида:
f x1 … xn = ~ f ~ ,
где ~f~ - л-выражение, содержащее f. Чтобы получить f, при условии корректности данного уравнения, определим:
LET f = Y (лf x1 … xn. ~ f ~ )
Тот факт, что равенство выполняется, может быть показано следующим образом:
f x1 … xn = Y (лf x1 … xn . ~ f ~ ) x1 … xn ( по определению f )
= (лf x1 … xn . ~ f ~ ) ( Y ((лf x1 … xn . ~ f ~ )) x1 … xn
( свойство неподвижной точки)
= (лf x1 … xn . ~ f ~ ) f x1 … xn ( по определению f )
= ~ f ~ ( β-конверсия )
Упражнение 21
Придумайте такое л-выражение eq, чтобы выполнялось:
eq m n = ( iszero m → iszero n | (iszero n → false | eq (pre m)(pre n)))
Упражнение 22
Показать, что если Y1 определяется так:
LET Y1 = Y (лy f. f(y f))
Тогда Y1 – оператор неподвижной точки, т. е. для любого Е :
Y1 E = E (Y1 E)
Оператор неподвижной точки в следующем упражнении определен Тьюрингом ( Барендрехт [2]).
Упражнение 23
Показать, что (лx y. y (x x y)) (лx y. y ( x x y )) – оператор неподвижной точки.
Следующее упражнение также из книги Барендрехта, где оно приписывается Клопу.
Упражнение 24
Показать, что Y2 , оператор неподвижной точки, где
LETЈ = лabcde f ghijklmnopqstuvwxyzr.
r(thisisa fixedpointcombinator)
LET Y2 = ЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈЈ
Упражнение 25
Верно ли, что Y f → f ( Y f)? Если да, то докажите это; если нет - найдите такое л-выражение Ŷ, что Ŷ f → f (Ŷ f).
В чистом л-исчислении, л-выражения могут быть применены только к одному аргументу; однако этот аргумент может быть и кортежом. Таким образом, можно написать :
E (E1, … , En)
Что фактически обозначает:
E(E1,(E2,( …(En-1,En)…)))
Например, E(E1,E2) означает E(лf. f E1 E2).
2.5 Функции нескольких аргументов
Традиционно, в математике применение функции n-аргументов f к аргументам x1 … xn записывается так: f(x1 … xn). Существуют два способа представления таких аппликаций в л-исчислении:
как (f x1 … xn) , или как применение f к n-кортежу (x1 … xn).
В первом случае, функция f применяется к аргументам по одному, и называется каррированной, по имени логика Карри ( впервые идея каррирования была создана Шонфинкелем[31]). Функции and, or и add, определенные выше, все являются каррированными функциями. Одно из преимуществ каррированных функций, это то, что они могут быть “частично применены”; например, add 1 – результат частичного применения add к 1 и соответствует функции n → n+1.
Несмотря на то, что часто бывает удобно представлять функции n-аргументов каррировнными, бывает также полезно представить их как во втором случае (ii), описанном выше, л-выражением, предполагающим единственный аргумент n-кортеж.
Например, вместо представления “ +” и ''х'' л-выражениями add и mult скажем так :
add m n = m+n
mult m n = mxn
может быть более удобно представить их функциями sum и prod, например такими:
sum (m, n) = m+n
prod (m, n) = mxn
Это уже больше похоже на традиционные математические обозначения, и имеет применения, которые мы рассмотрим позже. Можно сказать, что sum и prod – некаррированные версии add и mult соответственно.
Определим:
LET curry = лf x1 x2. f (x1,x2)
LET uncurry = лf p. f (fst p)(snd p)
затем, если мы определим
sum = uncurry add
prod = uncurry mult
мы видим, что sum и prod обладают желаемыми свойствами; например:
sum(m, n) = uncurry add (m, n)
= (лf p. f (fst p) (snd p)) add (m, n)
= add(fst (m, n))(snd (m, n))
= add m n
= m+n
Упражнение 26
Показать, что для любого E:
curry ( uncurry E) = E
uncurry ( curry E) = E
и что отсюда следует:
add = curry sum
mult = curry prod
Теперь мы можем определить любую n-арную функцию как каррированную
и некарриванную. Для n>0 определим:
LET curryn = лf x1 … xn. f (x1 … xn)
n n
LET uncurryn = лf p. f ( p↓1) … ( p↓n)
Если Е представляет функцию с n-кортежом в качестве аргумента, тогда curryn E представляет каррированную функцию, которая применяется к аргументам по одному. Если Е – каррированная функция n аргументов, тогда uncurryn E представляется собой некаррированную версию, предполагающую единственный аргумент : n-кортеж.
Упражнение 27
Показать, что
curryn (uncurryn E) = E uncurryn (curryn E) = E
Упражнение 28
Придумайте л-выражения En1 и En2 на основе curry и uncurry такие что,
curryn = En1 и uncurryn = En2.
Следующая нотация предоставляет удобный способ записи л-выражений, в которых в качестве аргумента ожидаются n-кортежи.
|
Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6 7 8 9 10 11 |
