== Теория Конечных Автоматов и Формальных Грамматик ==

{{courses:theory_of_computation:logo.jpg |"Development I", Escher, 1937}}

Курс читается для студентов 3го курса факультета ПМ-ПУ, СПбГУ, специальность "Информационные технологии".

Лектор: ((users:vi Иванов Владимир Витальевич))

Mailing list: ((http://groups.google.com/group/apmath_theory_of_computation/ apmath_theory_of_computation))

~~TOC~~


=== Содержание курса ===
  1 Регулярные языки [{{theory_of_computation/materials/slides/regular_languages.pdf|слайды}}]
    * конечные автоматы (DFA, NFA, ε-NFA)
    * регулярные выражения (RE)
    * свойства регулярных языков
    * эквивалентность и минимизация конечных автоматов
  1 Контекстно-свободные языки (CFL) [{{theory_of_computation/materials/slides/context_free_languages.pdf|слайды}}, p.1-119]
    * контекстно-свободные грамматики (CFG)
    * типы вывода и деревья разбора
    * неоднозначность в грамматиках и языках
    * недетерминированные конечные автоматы с магазинной памятью (%%PDA%%)
    * понятие распознавания для %%PDA%%
    * эквивалентность CFG и %%PDA%%
    * детерминированныe %%PDA%%
    * нормальные формы для CFG
      * нормальная форма Хомского (CNF)
      * нормальная форма Грейбах
    * свойства CFL
    * разрешимые проблемы для класса CFL
    * проблема принадлежности строки CFL
      * алгоритм CYK
  1 Синтаксический анализ [{{theory_of_computation/materials/slides/context_free_languages.pdf|слайды}}, p.119-174]
    * нисходящий(LL) разбор
    * восходящий(LR) разбор
    * моделирование недетерминированного преобразователя с магазинной памятью
    * детерминированный алгоритм нисходящего разбора с возвратами
    * ((http://en.wikipedia.org/wiki/SLR_Grammar SLR грамматики))
    * LL(k) грамматики
  1 Нетипизированное λ-исчисление [{{theory_of_computation/materials/slides/untyped_lambda_calculus.pdf|слайды}}, {{theory_of_computation/materials/FP_Foundations.pdf|article}}] 
    * λ-выражение
    * эквивалентность и нормализация λ-выражений
    * способы кодирования данных
    * рекурсивность в λ-исчислении
    * SECD-машина
    * комбинаторы и ((http://en.wikipedia.org/wiki/SKI_combinator_calculus SKI combinator calculus))
    * ((http://en.wikipedia.org/wiki/Graph_reduction graph reduction))
    * λ-исчисление и основные факты теории вычислений
  1 ((http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus λ-исчисление с простой типизацией)) ($ \lambda^{\rightarrow} $) [{{theory_of_computation/materials/slides/simply_typed_lambda_calculus.pdf|слайды}}, {{theory_of_computation/materials/IntroTT.pdf|article}}]
    * λ-исчисление с простой типизацией
    * изоморфизм Карри-Говарда: связь между формулами и типами
    * типизация по Чёрчу и типизация по Карри
    * наиболее общий тип выражения
    * свойства λ-исчисления с простой типизацией

=== Практические задачи ===
  * регулярные языки
    * переход от NFA к DFA
    * переход от ε-NFA к DFA
    * минимизация DFA
    * доказательство нерегулярности языка
  * контекстно-свободные языки
    * переход от CFG к %%PDA%%
    * переход от %%PDA%% к CFG
    * приведение CFG к CNF
    * определить принадлежность строки языку CFG с помощью алгоритма CYK
    * доказать, что язык не является контекстно-свободным
  * синтаксический анализ
    * нисходящий разбор
    * восходящий разбор
  * λ-исчисление
    * нормализация λ-выражения
    * типизированное λ-исчисление
    * вычисление типа выражения
    * построения выражения заданного типа
    * доказательство утверждения в логике PROP

((:computation Примеры))


=== Рекомендуемая литература ===
  1  ((http://www.amazon.com/Introduction-Automata-Theory-Languages-Computation/dp/0201441241 Hopcroft, Motwani, Ullman "Introduction to Automata Theory,
Languages, and Computation")) \\ ((http://www.ozon.ru/context/detail/id/3715578/ Хопкрофт, Мотвани, Ульман "Введение в теорию автоматов, языков и
вычислений"))
  1 ((http://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/0534950973 Sipser, "Introduction to the Theory of Computation"))
  1 ((http://www.amazon.com/G%25C3%25B6del-Escher-Bach-Eternal-Golden/dp/0465026567 Hofstadter, "Gödel, Escher, Bach: An Eternal Golden Braid")) \\ ((http://www.ozon.ru/context/detail/id/129157/ Хофштадтер "Гедель, Эшер, Бах. Эта бесконечная гирлянда"))



=== Материалы ===
  * слайды
    * {{theory_of_computation/materials/slides/regular_languages.pdf|Регулярные языки}}
    * {{theory_of_computation/materials/slides/context_free_languages.pdf|Контекстно-свободные языки и синтаксический анализ}}
    * {{theory_of_computation/materials/slides/untyped_lambda_calculus.pdf|Нетипизированное λ-исчисление}}
    * {{theory_of_computation/materials/slides/simply_typed_lambda_calculus.pdf|λ-исчисление с простой типизацией}}
  * {{theory_of_computation/materials/FP_Foundations.pdf|"Foundations of Functional Programming", Paulson}}
  * {{theory_of_computation/materials/IntroTT.pdf|"Introduction to Type Theory", Geuvers}}