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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

If false E
1
E
2
= E
2
Существуют бесконечно много различных способов для представления истинностных
значений и отрицания; здесь предлагаются традиционные определения.
true ≡ λx. λy. x
false ≡ λx. λy. y
not ≡ λt. t false true
Легко использовать правила конверсии, чтобы показать, что данные комбинаторы обла-
дают желаемыми свойствами. Так, например,
not true ≡ (λt. t false true) true
→
β
true false true ≡ (λx. λy. x) false true
→
β
(λy. false) true
→
β
false
Условное выражение можно определить следующим образом
If ≡ λx. λy. λz. x y z
Проверим, что данное определение обладает требуемыми свойствами:
If true E
1
E
2
≡ (λx. λy. λz. x y z) true E
1
E
2
≡ (((λx. λy. λz. x y z) true) E
1
) E
2
→ true E
1
E
2
≡ (λx.
λy. x) E
1
E
2
→
β
(λy. E
1
) E
2
→
β
E
1
If false E
1
E
2
≡ (λx. λy. λz. x y z) false E
1
E
2
≡ (((λx. λy. λz. x y z) false) E
1
) E
2
→ false E
1
E
2
≡
(λx. λy. y) E
1
E
2
→
β
(λy. y) E
2
→
β
E
2
Легко проверить, что конъюнкцию и дизъюнкцию можно определить так:
and ≡ λx. λy. x y false
or ≡ λx. λy. (x true) y
9.2.2 Пары и кортежи
Следующие комбинаторы используются для представления пар в λ–исчислении.
fst ≡ λx. x true
snd ≡ λx. x false
(E
1
, E
2
) ≡ λf. f E
1
E
2
Выражение (E
1
, E
2
) представляет упорядоченную пару, причем доступ к первой компо-
ненте осуществляется с помощью функции fst, а вторую компоненту возвращает функция
snd. Проверим:
fst (E
1
, E
2
)
59

Страницы