Математические основы функционального программирования. Лекция 2

1.

Лекция 2
Математические основы функционального программирования

2.

Процедурный стиль
Изменение состояний программы от начального к конечному
Состояния модифицируются с помощью команд присваивания, ход выполнения
команд меняется условными операторами

3.

Функциональная парадигма
•Не используется оператор присваивания для изменения состояний
•Не используются циклы
•Выполнение последовательности команд не имеет смысла, т.к. одна команда не
влияет на выполнение следующей
•Функции можно передавать в другие функции в качестве аргументов и
возвращать в качестве результата, результатом вычислений тоже может быть
функция
•Вместо циклов используется рекурсия

4.

Алонзо Чёрч
Алонзо Черч родился 14 июня 1903 года в городе
Вашингтон, США.
Известность пришла к Черчу после разработки
теории лямбда-исчислений. Данная теория
последовала за его знаменитой статьей 1936 года,
в которой показал существование так называемых
«неразрешимых задач».
Статья предшествовала знаменитому
исследованию Алана Тьюринга на тему проблемы
остановки, в котором также продемонстрировано
существование задач, неразрешимых
механическими способами.
Также Черчу принадлежит работа, в которой
доказал, что проблема для исчисления предикатов
неразрешима.

5.

Лямбда-исчисления
•Формализация, которая может быть использована для написания программ
•Простая модель для рекурсии и вложенных сред
•Большинство конструкций процедурных языков может отображено в
конструкции лямба-исчислений
•Функциональные языки в основном являются удобной формой синтаксической
записи для конструкций различных вариантов лямбда-исчислений

6.

Лямбда-выражение
E –некоторое выражение, возможно, использующую переменную x

7.

λ-термы

8.

Переменная

9.

Комбинация

10.

Абстракция

11.

Свободные и связанные переменные
Вхождение переменной V в выражение E свободно, если оно не принадлежит
области действия «λV» и связано в противном случае
В выражении подчеркнуты свободные переменные

12.

Подстановки
E
V
V’ (где V≠V’)
E1E2
λV.E1
λV’.E1 (где V≠V’ и V’ ∉ FV(E’))
λV’.E1 (где V≠V’ и V’ ∉ FV(E’))
E[V:=E’]
E’
V’
E1[V:=E’] E2[V:=E’]
λV.E1
λV’.E1[V:=E’]
λV’’.E1[V’:=V’’][V:=E’], где V’’ –
переменная такая, что V’’ ∉ FV(E’)
и ∉ FV(E1)

13.

Конверсии

14.

α-конверсия
Вспомогательный механизм для изменения имен связанных переменных ()

15.

β-конверсия
Вычисление значения функции от аргумента

16.

η-конверсия
Формализованное правило введения и удаления формального параметра

17.

Пример

18.

Обобщение определений

19.

Равенство лямбда-выражений
Два выражения равны, если от одного к другому можно перейти за конечное
число конверсий

20.

Редукция лямбда-выражений
Выражение редуцирумо от одного к другому, если можно перейти от одного к
другому за конечное число последовательных конверсий.

21.

Решить

22.

Спасибо за внимание