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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

Индуктивный переход:
(prefn f )
n+1
(false, x) ≡
(prefn f )
n
((prefn f ) (false, x))
= (prefn f )
n
(false, f x)
= (по предположению индукции) (false, f
n
(f x))
≡ (false, f
n
+1
x)
Равенство 4 следует из равенства 3:
(prefn f )
n
(true, x) ≡ (если n > 0)
(prefn f )
n–
1
((prefn f ) (true, x))
= (prefn f )
n–
1
(false, x)
= (false, f
n–
1
x)
Функция предшествования сейчас может быть определена так:
pre ≡ λ n f x .snd (n (prefn f ) (true, x))
Проверим, что это правильное определение, используя экстенсиональность. Докажем, что
при n>0 выполнено pre <n> f x = <n–1> f x, откуда будет следовать, что pre <n> →
η
<n–1>.
Действительно,
<n–1> f x
≡ (λf x. f
n
–1
x) f x
= f
n
–1
x
pre <n> f x
≡ (λ n f x .snd (n (prefn f) (true, x))) <n> f x
= snd (<n> (prefn f) (true, x))
= snd ((λf x. f
n
x) (prefn f) (true, x))
= snd ( (prefn f)
n
(true, x))
= snd (false, f
n–
1
x)
= f
n
–1
x
Очевидно,
pre <0>
≡ (λ n f x .snd (n (prefn f ) (true, x))) <0>
= λ f x .snd (<0> (prefn f ) (true, x)) (по определению <0>)
= λ f x .snd ((λf x. x) (prefn f ) (true, x))
= λ f x .snd (true, x)
= λ f x .x
=<0>
9.2.4 Рекурсивные функции
Использование рекурсивных функций – одна из важнейших особенностей функ-
ционального программирования: все итерации заменяются рекурсивными вызовами. На
первый взгляд это невозможно сделать в ламбда–исчислении, поскольку в λ–исчислении
63

Страницы