ВУЗ:
Составители:
= λ f x. <p> f (<q> f x)
= λ f x. (λg y. g
p
y) f (<q> f x)
= λ f x. (λ y. f
p
y) (<q> f x)
= λ f x. (λ y. f
p
y) ((λh z. h
q
z) f x)
= λ f x. (λ y. f
p
y) ((λ z. f
q
z) x)
= λ f x. (λ y. f
p
y) (f
q
x)
= λ f x. f
p
(f
q
x)
≡ λ f x. f
p
+
q
x ≡ <p+q>
Функция предшествования pre определяется с большим трудом, чем предыдущие
функции. Сам Алонсо Чёрч бился несколько месяцев над тем, чтобы определить эту
функцию. Чёрч так и не справился с этой задачей и уже уверился в неполноте своего вы-
числения, но в 1932 г. Стефен Клини, тогда молодой аспирант, нашел решение, и это было
его первым математическим результатом.
Трудность в определения функции предшествования состоит в том, что, имея терм
λf x. f
n
x, надо избавиться от первой аппликации f в f
n
. Чтобы достигнуть этого, предва-
рительно определим функцию prefn, оперирующую с парами и обладающую следующими
свойствами:
1) prefn f (true, x) = (false, x)
2) prefn f (false, x) = (false, f x)
Из этого следует, что
3) (prefn f )
n
(false, x) = (false, f
n
x)
4) (prefn f )
n
(true, x) = (false, f
n–
1
x) (если n>0)
Таким образом, последнее равенство, показывает, как можно получить n–1–кратную ап-
пликацию f к x. Определим prefn следующим образом:
prefn ≡ λ f p.(false, (If (fst p) (snd p) (f (snd p))))
Из определения следует, что prefn f (b, x) = (false, (If b x (f x)), и, следовательно:
prefn f (true, x)
= (false, (If true x (f x)))
= (false, x)
prefn f (false, x)
= (false, (If false x (f x)))
= (false, f x)
Равенство 3 докажем по индукции:
Базис индукции, n=0:
(prefn f )
0
(false, x)
≡ (false, x)
≡ (false, f
0
x)
62
Страницы
- « первая
- ‹ предыдущая
- …
- 60
- 61
- 62
- 63
- 64
- …
- следующая ›
- последняя »
