funcprog_2014_02_14_pr

50 %
50 %
Information about funcprog_2014_02_14_pr
Education
z x

Published on February 17, 2014

Author: compscicenter

Source: slideshare.net

Курс: Функциональное программирование Практика 1. Чистое лямбда-исчисление как язык программирования Разминка Выполните подстановку x y (λ z y. z x (w x) y) [x := w (λ x. w x)] x y (λ z y. z x (w x) y) [y := w (λ x. w x)] x y (λ z y. z x (w x) y) [z := w (λ x. w x)] x y (λ z y. z x (w x) y) [x := w (λ x. y x)] Определите, возможно ли в получшемся терме выполнить β-преобразование. Уберите лишние скобки и при возможности выполните β-преобразование ((λ z.(z (y z))) (z x) z) Булевы значения можно определить так: tru fls ≡ ≡ λ t f. t λ t f. f Cтандартные булевы операции кодируются так: iif not and or ≡ ≡ ≡ ≡ λ b x y. b x y λ b. b fls tru λ x y. x y fls ??? (упражнение) Проверьте, что ожидаемые свойства условного выражения выполняются: iif tru v w = v; iif fls v w = w. Проверьте, что ожидаемые свойства логического оператора «И» выполняются: and tru w = w; and fls w = fls. Попробуйте найти более «короткую» версию оператора «НЕ». Реализуйте оператор «ИЛИ». Пару (двухэлементный кортеж) можно определить так: pair ≡ λ x y f. f x y

Стандартные операции для пары (проекции): fst ≡ snd ≡ λ p. p tru λ p. p fls Проверьте, что ожидаемые свойства проекций выполняются: fst (pair a b) = a; snd (pair a b) = b. Числа (нумералы Чёрча) ≡ ≡ ≡ ≡ ≡ ... 0 1 2 3 4 λ s z. z λ s z. s z λ s z. s (s z) λ s z. s (s (s z)) λ s z. s (s (s (s z))) Выражение Fn (X), где n ∈ N, а F, X ∈ Λ, определим индуктивно: F0 (X) n+1 F (X) ≡ X; ≡ F(Fn (X)). Тогда n-ое число Чёрча : n ≡ λ s z. sn (z). Проверка числа на ноль (0 ≡ λ s z. z): iszro ≡ λ n. n (λ x. fls) tru Проверьте, что ожидаемые свойства iszro выполняются. Попробуйте найти более «короткую» версию iszro. Функция следования для чисел Чёрча succ ≡ λn s z. s (n s z) Проверьте, что ожидаемые свойства succ выполняются. Попробуйте найти другое определение succ. Функция сложения чисел Чёрча plus ≡ λm n s z. m s (n s z) Проверьте, что ожидаемые свойства plus выполняются. Попробуйте найти определение plus с использованием succ. 2

Функция умножения чисел Чёрча mult1 ≡ λm n. m (plus n) 0 mult2 ≡ λm n s z. m (n s) z Проверьте, что ожидаемые свойства умножения выполняются. Можно ли mult2 записать короче? Домашнее задание Выполните подстановку λ y z. x y w (z x) [x := λ y. y w] λ x y. x y (λ x. x y) x [x := λ z. z] x y (λ x z. x y z) y [y := x z] Определите, возможно ли в получшемся терме выполнить β-преобразование. (1 балл) Уберите лишние скобки и при возможности выполните β-преобразование (x (λ x.((x y) x)) y) ((λ p.(λ q.((q (p r)) s))) ((q (p r)) s)) (1 балл) Покажите, что для любых M и N выполняется λ x. M N = S (λ x. M) (λ x. N) (1 балл) Покажите, что SKK = I B = S (K S) K (2 балла) Реализуйте функцию возведения в степень для чисел Чёрча. (2 балла) 3

Add a comment

Related presentations

Related pages

Математическая статистика ...

Prepared for Name, Surname Семинар 9 Робастная регрессия. Логит регрессия. Грауэр Л.В., Архипова О ...
Read more