Математическое введение в декларативное программирование. Зюзысов В.М. - 61 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

add <m> <n> = <m+n> (для всех натуральных чисел m и n);
iszero <0> = true
iszero (suc <n>) = false
Определим натуральные числа, следуя Чёрчу. Будем использовать обозначение f
n
x
чтобы представить n–кратное применение f к x. Например, f
3
x ≡ f (f (f x))). Для удобства
f
0
x представляет просто x. В общем виде,
E
0
E
1
≡ E
1
E
n
E
1
≡ (E (E (…(E E
1
)…)))
n раз
Легко видеть, что E
n
(E E
1
) = E
n+
1
E
1
= E (E
n
E
1
).
<0> ≡ λf x. x
<1> ≡ λf x. f x
<2> ≡ λf x. f (f x)
…
<n> ≡ λf x. f
n
x
…
Такое представление чисел позволяет легко определить примитивные арифметиче-
ские функции.
suc ≡ λn f x. n f (f x)
add ≡ λ m n f x. m f ( n f x)
iszero ≡ λn. n (λ x. false) true
Проверим, что введенные комбинаторы обладают нужными свойствами:
suc <n> ≡ (λn f x. n f (f x)) (λf x. f
n
x)
= λf x.((λf x. f
n
x) f (f x))
= λf x.((λx. f
n
x) (f x))
= λf x. f
n
(f x)
= λf x. f
n
+1
x
= <n+1>
iszero <0> ≡ (λn. n (λx. false) true) (λf x. x)
= (λf x. x) (λx. false) true
= (λx. x) true
= true
add <p> <q> ≡ (λ m n f x. m f ( n f x)) <p> <q>
= (λ n f x. <p> f ( n f x)) <q>
61

Страницы