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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

≡ (λx. x true) (λf. f E
1
E
2
)
→
β
(λf. f E
1
E
2
) true
→
β
true E
1
E
2
→
β
(λx. λy. x) E
1
E
2
→
β
(λy.E
1
) E
2
→
β
E
1
Пара есть структура данных с двумя компонентами. Обобщенная структура с n
компонентами называется n–кой или кортежем и легко определяется через пары.
(E
1
, E
2
, …, E
n
) ≡ (E
1
, (E
2
, (…(E
n
–1
, E
n
)…)))
(E
1
, E
2
, …, E
n
) есть n–кортеж с компонентами E
1
, E
2
, …, E
n
и длиной n. Пары суть кортежи
длиной 2. С помощью следующих выражений получаем доступ к отдельным компонентам
кортежа.
E↓1 ≡ fst E
E↓2 ≡ fst (snd E)
E↓i ≡ fst (snd (snd (…(snd E)…))), если i меньше длины E
i–1 раз
E↓n ≡ snd (snd (…(snd E)…)), если n равно длине E
n–1 раз
Проверим, что эти определения правильно работают:
(E
1
, E
2
, …, E
n
)↓1
≡ fst (E
1
, (E
2
, (…(E
n
–1
, E
n
)…)))
→ E
1
(E
1
, E
2
, …, E
n
)↓2
≡ fst (snd (E
1
, (E
2
, (…(E
n
–1
, E
n
)…))))
→ fst (E
2
, (…(E
n
–1
, E
n
)…)))
→ E
2
В общем случае (E
1
, E
2
, …, E
n
)↓i = E
i
для 1 ≤ i ≤ n.
9.2.3 Числа
Существует много способов для определения чисел в виде λ–выражений; каждый
способ имеет свои преимущества и недостатки [1]. Нашей целью является определить
комбинатор <n> для представления натурального числа n. Необходимо определить также
примитивные арифметические операции в терминах λ–выражений. Например, нам необ-
ходимы λ–выражения suc, pre, add и iszero, представляющие функции следования n →
n+1, предшествования n → n–1, сложения и тест для нуля, соответственно. Эти λ–
выражения представляют числа корректно, если они обладают следующими свойствами:
suc <n> = <n+1> (для всех натуральных чисел n);
pre <n> = <n–1> (для всех натуральных чисел n>0);
60

Страницы