WWW.DOC.KNIGI-X.RU
БЕСПЛАТНАЯ  ИНТЕРНЕТ  БИБЛИОТЕКА - Различные документы
 

«14.02.2014 Денис Николаевич Москвин Лямбда-исчисление План лекции Функциональное vs императивное программирование Введение в -исчисление ...»

Функциональное программирование

Лекция 1. Лямбда-исчисление

Денис Николаевич Москвин

Computer Science Center

14.02.2014

Денис Николаевич Москвин Лямбда-исчисление

План лекции

Функциональное vs императивное программирование

Введение в -исчисление

Подстановка и преобразования

Расширения чистого -исчисления

Денис Николаевич Москвин Лямбда-исчисление

План лекции

Функциональное vs императивное программирование

Введение в -исчисление

Подстановка и преобразования

Расширения чистого -исчисления Денис Николаевич Москвин Лямбда-исчисление Императивное программирование Императивное программирование: вычисление описывается в терминах инструкций, изменяющих состояние вычислителя.

В императивных программах:

Состояние изменяется инструкциями присваивания: v = E Есть механизм условного исполнения: инструкции if, switch Есть механизм циклов: инструкции while, for Инструкции исполняются последовательно C1; C2; C3 Иногда говорят про стиль фон Неймана (Джон Бэкус) Денис Николаевич Москвин Лямбда-исчисление Императивное программирование: пример Скалярное произведение двух n-мерных векторов для фон-нейманновского языка res = 0;

for (i = 0; i n; i++) res = res + a[i] * b[i];

Как здесь формируется состояние и какие изменения с ним происходят?

Денис Николаевич Москвин Лямбда-исчисление Императивное программирование: пример Скалярное произведение двух n-мерных векторов для фон-нейманновского языка res = 0;

for (i = 0; i n; i++) res = res + a[i] * b[i];

Как здесь формируется состояние и какие изменения с ним происходят?

Абстрактное представление (пока забываем про I/O):

0 = 1 = 2 =... = n Выполнение программы: переход вычислителя из начального состояния в конечное с помощью последовательных инструкций.

Денис Николаевич Москвин Лямбда-исчисление Функциональное программирование Функциональная программа выражение, её выполнение вычисление (редукция) этого выражения.

Нет состояний нет переменных Нет переменных нет присваивания Нет циклов, поскольку нет различий между итерациями Последовательность не важна, поскольку выражения независимы

Вместо этого есть:

Рекурсия вместо циклов Функции высших порядков (HOF) Денис Николаевич Москвин Лямбда-исчисление Функциональное программирование: пример Скалярное произведение для функционального языка innerProduct = (sum.). zipWith (*)

Абстрактное представление:

fn (fn1 (... f2 (f1 (0 ))...)) Выполнение программы – вычисление выражения.

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Функциональное программирование: преимущества и недостатки

Преимущества ФП:

Более точная семантика Большая свобода при исполнении (например, поддержка параллельности) Большая выразительность Лучшая параметризация и модульность Удобство при работе с бесконечными структурами данных

Недостатки ФП:

Ввод-вывод и прочая интерактивность: нужен специальный инструментарий Быстродействие (исполнение в чуждой архитектуре)

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Чистота и побочные эффекты (2) Функция f не является чистой (pure) математической функцией. Говорят о нарушении ссылочной прозрачности (reference transparency).

Результат вызова f зависит от внешних факторов, а исполнение приводит к возникновению побочного эффекта (side eect). Причина: глобально доступное состояние + разрушающее присваивание.

В чистом функциональном программировании такие функции не используются (в Хаскелле живут в гетто IO, в других допустимы, но не рекомендуются).

Денис Николаевич Москвин Лямбда-исчисление План лекции Функциональное vs императивное программирование Введение в -исчисление Подстановка и преобразования Расширения чистого -исчисления Денис Николаевич Москвин Лямбда-исчисление

-исчисление

-исчисление формальная система, лежащая в основе функционального программирования.

Разработано Алонзо Чёрчем в 1930-х для формализации и анализа понятия вычислимости.

Имеет бестиповую и множество типизированных версий.

Позволяет простым образом описывать семантику вычислительных процессов.

Денис Николаевич Москвин Лямбда-исчисление Неформальное введение в -исчисление

В -исчислении имеются две операции:

применение (аппликация, application);

абстракция (abstraction).

Нотация применения F к X:

–  –  –

С точки зрения программиста: F (алгоритм) применяется к X (входные данные).

Однако явного различия между алгоритмами и данными нет, в частности допустимо самоприменение:

–  –  –

где M[x := N] обозначает подстановку N вместо x в M.

Денис Николаевич Москвин Лямбда-исчисление Термы чистого -исчисления Определение Множество -термов строится из переменных

V = {x, y, z,...} c помощью применения и абстракции:

–  –  –

Соглашение. Произвольные термы пишем заглавными буквами, переменные строчными.

Денис Николаевич Москвин Лямбда-исчисление Термы (примеры) Примеры -термов

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Термы (соглашения)

Общеприняты следующие соглашения:

Внешние скобки опускаются.

Применение ассоциативно влево:

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Свободные и связанные переменные Абстракция x. M[x] связывает дотоле свободную переменную x в терме M.

Пример 1

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Свободные и связанные переменные (2) Определение

Множество FV(T ) свободных (free) переменных в -терме T :

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Комбинаторы Определение M замкнутый -терм (или комбинатор), если FV(M) =. Множество замкнутых -термов обозначается 0.

Классические комбинаторы:

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Функции нескольких переменных, каррирование Шонфинкель (1924): функция нескольких переменных может быть описана как конечная последовательность функций одной переменной.

Пусть (x, y) терм, содержащий свободные x и y.

Введём, путём последавательных абстракций

–  –  –

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

Денис Николаевич Москвин Лямбда-исчисление Тождественное равенство термов

–  –  –

Иногда такое переименование называют

-преобразованием и пишут P Q.

Денис Николаевич Москвин Лямбда-исчисление План лекции Функциональное vs императивное программирование Введение в -исчисление Подстановка и преобразования Расширения чистого -исчисления Денис Николаевич Москвин Лямбда-исчисление Подстановка терма Определение M[x := N] обозначает подстановку N вместо свободных вхождений x в M.

Правила подстановки:

–  –  –

Денис Николаевич Москвин Лямбда-исчисление Проблема захвата переменной Неприятность: (y. x y)[x := y] (y FV(N) в четвёртом правиле).

Соглашение Барендрегта Имена связанных переменных всегда будем выбирать так, чтобы они отличались от имён свободных переменных.

–  –  –

Тогда можно использовать подстановку без оговорки о свободных и связанных переменных.

Денис Николаевич Москвин Лямбда-исчисление Лемма подстановки Лемма подстановки Пусть M, N, L. Предположим x y и x FV(L). Тогда

–  –  –

Доказательство Нудная индукция по всем 5 случаям.

Денис Николаевич Москвин Лямбда-исчисление

Преобразования (конверсии):

Основная схема аксиом для -исчисления Для любых M, N

–  –  –

Денис Николаевич Москвин Лямбда-исчисление

Преобразования (конверсии):

Для рассуждений достаточно соглашения Барендрегта, но для компьютерной реализации -преобразование полезно:

Пример Пусть x. x x и 1 y z. y z. Тогда

–  –  –

Денис Николаевич Москвин Лямбда-исчисление

Преобразования (конверсии):

Индексы Де Брауна (De Bruijn) представляют альтернативный способ представления термов.

Переменные не именуются, а нумеруются (индексируются), индекс показывает, сколько лямбд назад переменная была связана:

–  –  –

При таком представлении проблемы захвата переменной нет.

Денис Николаевич Москвин Лямбда-исчисление

Преобразования (конверсии):

-преобразование обеспечивает принцип экстенсиональности: две функции считаются экстенсионально эквивалентными, если они дают одинаковый результат при одинаковом вводе:

–  –  –

В Хаскелле так называемый бесточечный стиль записи основан на -преобразовании.

Денис Николаевич Москвин Лямбда-исчисление План лекции Функциональное vs императивное программирование Введение в -исчисление Подстановка и преобразования Расширения чистого -исчисления Денис Николаевич Москвин Лямбда-исчисление Расширения чистого -исчисления

Можно расширить множество -термов константами:

–  –  –

И всё равно, помимо констант нужны дополнительные правила, описывающие работу с ними. Какие?

Денис Николаевич Москвин Лямбда-исчисление

-преобразование: пример

–  –  –

Внешние функции над константами порождают новые правила преобразований.

Денис Николаевич Москвин Лямбда-исчисление

-преобразование: обобщение Если на множестве термов X (обычно X C) задана внешняя функция f : Xk (C), то для неё добавляем

-правило:

выбираем незанятую константу f ;

для M1,..., Mk X добавляем правило сокращения

Похожие работы:

«Отзыв официального оппонента на диссертационную работу Дутовой Светланы Вячеславовны "Фармакологические и фармацевтические аспекты иммунотропного действия извлечений из сырья эфирномасличных растений", представленную на соискание ученой...»

«0 МОЛОДЕЖНЫЙ НАУЧНЫЙ ФОРУМ: ЕСТЕСТВЕННЫЕ И МЕДИЦИНСКИЕ НАУКИ Электронный сборник статей по материалам VIII студенческой международной заочной научно-практической конференции № 1 (8) Январь 2014 г. Издается с марта 2013 года Москва УДК 50+61 ББК 20+5 М 75 М 75 Молодежный научный форум: Естественные и медицинчкие науки. Эле...»

«АННОТАЦИЯ РАБОЧЕЙ ПРОГРАММЫ УЧЕБНОЙ ДИСЦИПЛИНЫ ЕН.01 Математика Специальность СПО: 14.02.01 Атомные электрические станции и установки Нормативный срок освоения ППССЗ: 3года 10 месяцев Уровень подготовки: базовый Наименование квалификации: техник Цель и задачи учебной дисци...»

«Часть II Последовательности КМАТ 04 N-граммы. Моделирование локального контекста Компьютерные методы анализа текста Кирилл Александрович Маслинский НИУ ВШЭ Санкт-Петербург 14.02.2014 / 04 КМАТ 04 Outline Контекст Предсказание слова Модель контекста: N-граммы Языков...»

«ХИМИЯ РАСТИТЕЛЬНОГО СЫРЬЯ. 2011. №3. С. 137–142. УДК 547.972 ФЛАВОНОИДЫ НАДЗЕМНОЙ ЧАСТИ И КОРНЕЙ PSEUDOSOPHORA ALOPECUROIDES (L.) SWEET Э.Х. Ботиров1*, М.М. Тожибоев2, В.М. Боначева1, А.А. Дренин1 Сургутский государственный униве...»

«Химия растительного сырья. 2000. № 3. C. 85–94. УДК 547.913:543.544.45 СОСТАВ ЭФИРНОГО МАСЛА СИБИРСКИХ ПОПУЛЯЦИЙ ARTEMISIA PONTICA L. ПЕРСПЕКТИВНОГО ЛЕКАРСТВЕННОГО РАСТЕНИЯ а а б в М.А. Ханина, Е.А. Серых, А.Ю. Королюк,...»

«МИНИСТЕРСТВО ЗДРАВООХРАНЕНИЯ РЕСПУБЛИКИ БЕЛАРУСЬ УТВЕРЖДАЮ Первый заместитель министра Д.Л. Пиневич 28.11.2012 г. Регистрационный № 155-1112 МЕТОД ЛЕЧЕНИЯ ДИСТАЛЬНОГО ПРИКУСА, СФОРМИРОВАННОГО ЗА СЧЕТ РЕТРОПОЛОЖЕНИЯ НИЖНЕЙ ЧЕЛЮСТИ, НЕСЪЕМНЫМИ АППАРАТАМИ ФУНКЦИОНАЛЬНОГО ДЕЙСТВИЯ инструкция по пр...»

«Государственное бюджетное образовательное учреждение высшего профессионального образования "Красноярский государственный медицинский университет имени профессора В.Ф. Войно-Ясенецкого" Министерства здравоохранения Российской Фед...»

















 
2017 www.doc.knigi-x.ru - «Бесплатная электронная библиотека - различные документы»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.