• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Бакалавриат 2019/2020

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

Направление: 01.03.02. Прикладная математика и информатика
Когда читается: 4-й курс, 3 модуль
Формат изучения: Full time
Язык: русский
Кредиты: 4

Программа дисциплины

Аннотация

Настоящая дисциплина относится к профессиональному циклу, дисциплинам базовой части профиля. Для специализации «Распределенные системы» настоящая дисциплина является базовой. Изучение данной дисциплины базируется на знании курса “Сложность вычислений и логика в теоретической информатике”.
Цель освоения дисциплины

Цель освоения дисциплины

  • Освоение теоретической базы функционального программирования (начала теории типов, лямбда-исчисление, начала теории категорий).
  • Овладение техникой программирования на языке Haskell.
Планируемые результаты обучения

Планируемые результаты обучения

  • Студент знает теоретические основы функционального программирования (лямбда-исчисление, начала теории категорий и проч.).
  • Студент владеет общей информацией об императивном и функциональном стилях программирования, их сильных и слабых сторонах, умеет выбирать правильный стиль в зависимости от задачи.
  • Студент решает задачи на программирование на языке Haskell.
  • Студент разрабатывает новые библиотеки на языке Haskell.
  • Студент создает код на функциональном языке, корректность которого формально доказана (верифицирована).
Содержание учебной дисциплины

Содержание учебной дисциплины

  • Типизованное лямбда-исчисление
    Это теоретический вводный раздел курса. В нём на лекции излагаются основные понятия лямбда-исчисления, понятия, теории типов и их применения в программировании. На семинаре обсуждаются задачи на типизацию и преобразования лямбда-термов.
  • Нормализуемость и конфлюэнтность
    На лекции даются формулировки основных свойств лямбда-исчисления (точнее, отношений бета- и ита-редукций): свойства сильной и слабой нормализуемости и свойство Чёрча - Россера (конфлюэнтности). Доказательства этих свойств выходят за рамки курса. На семинаре обсуждаются примеры нормализации лямбда-термов, а также нарушения нормализуемости (как слабой, так и сильной, при сохранении слабой) в нетипизируемом случае.
  • Императивное и функциональное программирование. Элементы функционального программирования в императивных языках
    На лекции даётся сравнение двух парадигм программирования - императивной и функциональной. Практическое занятие и домашняя работа посвящены реализации некоторых мотивов функциональной парадигмы во в целом императивном языке Python.
  • Язык и среда разработки Haskell: установка и настройка
    Практическое занятие: демонстрация работы с интерпретатором Haskell (GHC или иным).
  • Основы программирования на языке Haskell
    Практическое занятие: простейшие программы на Haskell.
  • Типы данных в Haskell
    Даётся обзор стандартных типов данных в Haskell. Обсуждаются возможности индуктивного построения новых типов (на примере натуральных чисел по Пеано). Обсуждается алгоритм Хиндли-Дамаса-Милнера для выведения типов (type inference).
  • "Ленивые" и "ретивые" вычисления
    На лекции обсуждается различие между "ленивыми" вычислениями (когда значение подтерма вычисляется только по необходимости) и "ретивыми" вычислениями (когда рекурсивно вычисляется всё). На практическом занятии даются примеры, когда "ленивые" вычисления справляются с ситуациями, где "ретивые" входят в бесконечный цикл.
  • Монады и их использование для ввода-вывода
    На лекции рассказывается введение в теорию категорий и даётся понятие монады. На практическом занятии обсуждается применение монад для реализации функций с состояниями и побочных эффектов.
  • Соответствие Карри - Говарда. Верификация программ и математических утверждений. Система Coq
    Необязательная часть курса. Рассказывается о соответствии Карри - Говарда между типами и высказываниями и термам и доказательствами высказываний. В практической части демонстируются возможности формального доказательства математических теорем, в том числе о правильности работы программ (верификация).
Элементы контроля

Элементы контроля

  • неблокирующий Домашние задания
    Программистские домашние задания (4-6 заданий в течение модуля). <br />Домашние задания могут раздаваться и приниматься по электронной почте, посредством системы Github или каким-либо иным удобным для преподавателя и студентов способом. В ходе текущего контроля (домашние задания) студент должен продемонстрировать владение техниками программирования, обсуждёнными к настоящему моменту.
  • неблокирующий Контрольная работа
    Контрольная работа (60 мин) в середине курса.
  • неблокирующий Экзамен
    Письменный экзамен (90 мин).<br />На итоговом экзамене студент должен показать владение теоретическими основами функционального программирования, посредством решения задач.
Промежуточная аттестация

Промежуточная аттестация

  • Промежуточная аттестация (3 модуль)
    Итоговая оценка формируется следующим образом: <br />0,7*(накоп.) + 0,3*(экзамен), <br />где (экзамен) - оценка за итоговый экзамен, а (накоп.) - накопленная оценка за семестр, определяемая следующим образом: <br /> (накоп.) = 0,72*(прог.) + 0,28*(контр.), <br />где (прог.) - суммарная оценка за программистские домашние задания, (сам.) - оценка за контрольную работу.
Список литературы

Список литературы

Рекомендуемая основная литература

  • Barendregt, H., Dekkers, W., Statman, R. Lambda calculus with types. – Cambridge University Press, 2013. – 856 pp.

Рекомендуемая дополнительная литература

  • Lipovaca M. Learn you a Haskell for great good!: a beginner's guide. – No Starch Press, 2011. – 404 pp.