deniok: (Default)
deniok ([personal profile] deniok) wrote2011-02-18 09:35 am
Entry tags:

Анонс

Буду со следующего воскресенья (27.02.2011) читать в Computer Science клубе при ПОМИ РАН читать курс Системы типизации лямбда-исчисления.



Лекция 1. Система лямбда-исчисления без типов

Применение и абстракция. Свободные и связанные переменные. Комбинаторы. Функции нескольких переменных, каррирование. Подстановка, лемма подстановки. Бета-преобразование. Теорема о неподвижной точке, Y-комбинатор.

Лекция 2. Программирование в лямбда-исчислении и лямбда-определимость

Лямбда-исчисление как язык программирования. Булевы значения, пары. Числа Чёрча, операции над ними. Примитивная рекурсия. Списки. Лямбда-определимость и вычислимость по Тьюрингу. Неразрешимость бестипового лямбда-исчисления.

Лекция 3. Отношение редукции

Редексы. Одношаговая и многошаговая $\beta$-редукция, $\beta$-эквивалентность. $\beta$-нормальная форма. Редукционные графы. Теорема Чёрча-Россера. Следствия: редуцируемость к нормальной форме, единственность нормальной формы. Нормальная и аппликативные стратегии редукции. Теорема о нормализации.

Лекция 4. Просто типизированное лямбда-исчисление

Система $\lambda_{\rightarrow}$. Предтермы. Отношение типизации. Контексты. Правила типизации по Карри и по Чёрчу. Деревья вывода типов. Система минимальной пропозициональной логики. Соответствие Карри-Говарда. Леммы о контекстах. Типизируемость подтермов, нетипизируемые предтермы.

Лекция 5. Свойства просто типизированной системы

Лемма подстановки. Редукция субъекта. Незамкнутость относительно экспансии. Уникальность типов для типизации по Чёрчу. Связь между системами Карри и Черча. Вывод типов для $\lambda_{\rightarrow}$ в стиле Карри. Главный (наиболее общий) тип. Унификация. Алгоритм Хиндли-Милнера.


Дальше пока приблизительно:

Лекция 6. Слабая и сильная нормализация. Расширение систем константами.

Лекция 7. Полиморфная типизация. System F
Let-полиморфизм

Лекция 8. Параметричность. Свободные теоремы

Лекция 9 Операторы над типами. Зависимые типы

Лекция 10 Лямбда-куб. PTS

Лекция 11 Рекурсивные типы

Лекция 12 Рекурсивные типы

Литература:
LCWT
Henk Barendregt, Lambda calculi with types,
Handbook of logic in computer science (vol. 2), Oxford University Press, 1993

ITT
Herman Geuvers, Introduction to Type Theory
Alfa Lernet Summer school 2008, Uruguay
http://www.cs.ru.nl/H.Geuvers/Uruguay2008SummerSchool.html/

TAPL
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002
http://www.cis.upenn.edu/~bcpierce/tapl

ATTAPL
Benjamin C. Pierce, editor. Advanced Topics in Types and Programming Languages,
MIT, 2005

ЛИСС
Х. Барендрегт, Ламбда-исчисление, его синтаксис и семантика,
М:Мир, 1985



Обратите внимание, что лекции будут некоторое время в Академическом университете, на Фонтанке - ремонт (подробности - по первой ссылке).

[identity profile] yantayga.livejournal.com 2011-02-18 06:29 am (UTC)(link)
А планируется ли снимать видео?

[identity profile] deni-ok.livejournal.com 2011-02-18 06:41 am (UTC)(link)
Да, планируется.

[identity profile] yantayga.livejournal.com 2011-02-18 07:03 am (UTC)(link)
Спасибо, будем ждать :)

[identity profile] kurilka.livejournal.com 2011-02-18 08:44 am (UTC)(link)
засмотрим обязательно

[identity profile] cadadr.livejournal.com 2011-02-18 01:45 pm (UTC)(link)
Всё снимает lektorium.tv, но порой дичайше тормозит с выкладыванием...

[identity profile] udpn.livejournal.com 2011-02-18 07:02 pm (UTC)(link)
Урррааааа

[identity profile] nealar.livejournal.com 2011-02-18 06:36 am (UTC)(link)
Если лекции не на английском, то ссылку на TAPL лучше дать на перевод.

[identity profile] deni-ok.livejournal.com 2011-02-18 06:44 am (UTC)(link)
я думаю, что те, кому надо, легко сами найдут.

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

[identity profile] nealar.livejournal.com 2011-02-18 07:04 am (UTC)(link)
Тады пусть они сами сюда придут и объяснят.

[identity profile] deni-ok.livejournal.com 2011-02-18 08:31 am (UTC)(link)
Подождём :)

[identity profile] ulysses4ever.livejournal.com 2011-02-18 09:10 am (UTC)(link)
Им исходники сам Пирс давал вроде.

[identity profile] deni-ok.livejournal.com 2011-02-18 09:30 am (UTC)(link)
я не про то

у них, вроде, переговоры с издательством и сейчас не знаю, насколько лишняя публичность им нужна

[identity profile] ulysses4ever.livejournal.com 2011-02-18 09:31 am (UTC)(link)
А, понятно. Спасибо, что пояснили.

[identity profile] alexott.livejournal.com 2011-02-18 09:28 am (UTC)(link)
http://newstar.rinet.ru/~goga/tapl/ - все официально делается, сейчас идет заключительная вычитка и верстка, потом пойдет в типографию... Электронная версия вроде будет свободной и после релиза

[identity profile] deni-ok.livejournal.com 2011-02-18 09:30 am (UTC)(link)
о, тогда ok

[identity profile] udpn.livejournal.com 2011-02-18 07:04 pm (UTC)(link)
Русский перевод читается намного тяжелее. Некоторые предложения слишком дословно переведены с английского, и я впадаю в ступор. Это субъективно.
(deleted comment)
(deleted comment)

[identity profile] deni-ok.livejournal.com 2011-02-18 10:37 am (UTC)(link)
кто же мешает самому прорешать из Art of Coq ;-)

ну и понятно, что в ПОМИ традиционный академический формат. Практические занятия не предусмотрены, их качественная организация, кстати, не самое простое дело.

[identity profile] cadadr.livejournal.com 2011-02-18 01:38 pm (UTC)(link)
Обычно домашние задания и экзаменационные задачи лекторы по имейлу принимают. Можете выкладывать на какую-нибудь страничку, а потом собирать решения. Поначалу всегда желающих очень много (переписываться нереально), но надо подождать до конца семестра, когда 90% желающих отвалится :-)

Кстати, я в CS-клубе всё с удовольствием слушаю. Жалко, в этом семестре воскресенье полностью пересекается с физматклубом, а ваши лекции, судя по всему только по воскресеньям...

[identity profile] deni-ok.livejournal.com 2011-02-18 10:38 am (UTC)(link)
> всего одна лекция про зависимые типы

посмотрим, эта часть ещё в работе
(deleted comment)

[identity profile] alexott.livejournal.com 2011-02-18 12:35 pm (UTC)(link)
может взять Certified Programming with Dependent Types и на его основе построить отдельный курс?
(deleted comment)

[identity profile] deni-ok.livejournal.com 2011-02-18 08:08 pm (UTC)(link)
> никто ж реалные программы в Coq'е писать-то не умеет!

А ты умеешь? А то тут на Coq'еров проскакивал некоторый спрос.

[identity profile] kurilka.livejournal.com 2011-02-18 07:51 pm (UTC)(link)
Дак может пирсовский же http://www.seas.upenn.edu/~cis500/current/sf/html/index.html взять?

[identity profile] ulysses4ever.livejournal.com 2011-02-18 09:14 am (UTC)(link)
Кроме видео ещё бы записки лекций в pdf...

[identity profile] deni-ok.livejournal.com 2011-02-18 09:26 am (UTC)(link)
слайды будут, а записки - боюсь не успею сделать :(

[identity profile] alexott.livejournal.com 2011-02-18 09:31 am (UTC)(link)
по первым частям можно еще использовать https://code.google.com/p/funprog-ru/

в литературу я бы еще понапихал http://adam.chlipala.net/cpdt/, для развития. Ну и Cardelli тоже, хотя Пирс его покрывает

[identity profile] deni-ok.livejournal.com 2011-02-18 07:53 pm (UTC)(link)
Да, на первую я в слайдах кое-где ссылаюсь.

А вторая, Certified Programming with Dependent Types, это, конечно, для отдельного, специального курса.

[identity profile] http://users.livejournal.com/_slw/ 2011-02-24 03:10 pm (UTC)(link)
а вопрос по регламенту.
кто может прийти?
что надо что бы прийти?

[identity profile] deni-ok.livejournal.com 2011-02-24 03:57 pm (UTC)(link)
Вход свободный
http://logic.pdmi.ras.ru/csclub/faq
только лекции будут не на Фонтанке, а в Академическом университете
http://logic.pdmi.ras.ru/csclub/node/1084

[identity profile] http://users.livejournal.com/_slw/ 2011-02-24 04:03 pm (UTC)(link)
у них там кажется пропускной режим, если я ничего не путаю

[identity profile] deni-ok.livejournal.com 2011-02-24 04:43 pm (UTC)(link)
там пускают по фразе "я иду в Computer Science клуб", но всё же не помешает иметь с собой какой-нибудь документ.