courses:functional_programming:lectures
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
courses:functional_programming:lectures [2018/09/04 07:25] vnikolenko |
courses:functional_programming:lectures [2018/12/03 17:00] vnikolenko |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| * Свободные и связанные переменные | * Свободные и связанные переменные | ||
| * Комбинаторы | * Комбинаторы | ||
| + | * Каррирование | ||
| * Подстановка | * Подстановка | ||
| * Правила преобразования | * Правила преобразования | ||
| Line 16: | Line 17: | ||
| ===== Рекурсия и редукция ===== | ===== Рекурсия и редукция ===== | ||
| - | * Теорема о неподвижной точке | + | * Теорема о неподвижной точке, Y-комбинатор |
| - | * Редексы и нормальная форма | + | * Совместимые (с λ-исчислением) отношения, отношения редукции, отношения равенства(конгруэнтности) |
| - | * Редукция и её стратегии | + | * Одношаговая β-редукция, β-редукция, β-равенство |
| - | * Теорема Черча-Россера | + | * Редукционные графы |
| + | * Нормальная форма(nf) | ||
| + | * Ненормализуемые, слабо нормализуемые и сильно нормализуемые термы | ||
| + | * Теорема Чёрча-Россера, теорема об общем редукте, теорема о единственности nf | ||
| + | * Стратегии редукции | ||
| + | * Головная нормальная форма, слабая головная нормальная форма | ||
| + | * Теорема о нормализации | ||
| ===== Просто(е) типизированное лямбда-исчисление ===== | ===== Просто(е) типизированное лямбда-исчисление ===== | ||
| * Понятие типа (предназначение типов) | * Понятие типа (предназначение типов) | ||
| - | * Типы в логике и в программировании | + | * Просто(е) типизированное λ-исчисление (STLC) |
| - | * Просто(е) типизированное λ-исчисление | + | |
| * Типизация по Чёрчу и Карри | * Типизация по Чёрчу и Карри | ||
| + | * Множество типов, предтермы, утверждение о типизации, контекст | ||
| + | * Правила типизации | ||
| + | * Леммы генерации, о контекстах | ||
| + | * Теорема о редукции субъекта | ||
| + | * Теорема о единственности типа для типизации по Чёрчу | ||
| + | * Теорема о нормализации | ||
| + | | ||
| ===== Введение в язык Haskell ===== | ===== Введение в язык Haskell ===== | ||
| * Базовые типы | * Базовые типы | ||
| Line 35: | Line 48: | ||
| * Операторы и сечения | * Операторы и сечения | ||
| * Модули | * Модули | ||
| - | * Реализации языка Haskell и инфраструктура | + | * Реализации языка Haskell и инфраструктура (cabal, stack, hackage, hoogle) |
| ===== Основы программирования в Haskell ===== | ===== Основы программирования в Haskell ===== | ||
| Line 49: | Line 62: | ||
| * Классы типов | * Классы типов | ||
| * Сравнение с другими языками программирования | * Сравнение с другими языками программирования | ||
| - | * Обзор стандартных классов типов | + | * Обзор стандартных классов типов(Eq, Ord, Enum, Bounded, Show, Read, Num, Fractional, Integral) |
| - | * Особенности внутренней реализации классов типов | + | * Особенности внутренней реализации классов типов (реализация с помощью словарей) |
| ===== Свертки и моноиды ===== | ===== Свертки и моноиды ===== | ||
| - | * Левая и правая свертки | + | * Левая и правая свертки (foldr, foldl, foldl', foldr1, foldl1) |
| - | * Родственные сверткам функции | + | * Родственные сверткам функции (scanl, scanr, unfold) |
| - | * Моноиды | + | * Semigroup a, закон для полугруппы |
| - | * Законы моноидов | + | * Semigroup a => Monoid a, законы для моноида |
| + | * Стандартные моноиды ([a], Any, All, Product a, Sum a, Endo a, Dual a, Last a, First a) | ||
| + | * Foldable | ||
| ===== Функторы ===== | ===== Функторы ===== | ||
| Line 63: | Line 78: | ||
| * Аппликативные функторы | * Аппликативные функторы | ||
| * Законы для аппликативных функторов | * Законы для аппликативных функторов | ||
| + | * Функция как функтор, аппликативный функтор | ||
| + | * Список как аппликативный функтор, ZipList | ||
| + | <del> | ||
| ===== Использование аппликативных функторов ===== | ===== Использование аппликативных функторов ===== | ||
| * Аппликативные парсеры | * Аппликативные парсеры | ||
| Line 70: | Line 88: | ||
| * Класс типов Traversable | * Класс типов Traversable | ||
| * Законы класса Traversable | * Законы класса Traversable | ||
| + | </del> | ||
| ===== Монады ===== | ===== Монады ===== | ||
courses/functional_programming/lectures.txt · Last modified: 2022/12/10 09:08 (external edit)
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Share Alike 4.0 International
