Доклад на SPbHUG 19.09.2008

[deniok]

Сделал вчера на очередной встрече SPbHUG доклад про лямбда-куб Барендрегта (подробности см. на юзерпике).

Народ (которого было как селедок в бочке, ну то есть неожиданно много) сильно повеселила чудесная аксиома:


Выложил на сайте SPbHUG слайды к докладу и мой перевод на русский (с комментариями) первого раздела пятой главы замечательного обзора Хенка Барендрегта: Henk Barendregt, Lambda calculi with types, в Handbook of Logic in Computer Science. Угощайтесь на здоровье, кто в английском не столь искушен как в русском.

Comments

[deni-ok.livejournal.com]

Пожалуйста, пожалуйста!

[kurilka.livejournal.com]

Будем почитать...
Кстати, ты к вычитке перевода TAPL не присоединился?

[deni-ok.livejournal.com]

Я подписался, но времени нету :(
Выкрою - поучаствую...

[kurilka.livejournal.com]

Я тож не сильно пока вчитался, математики блин там многовато для меня :(

[vladiros.livejournal.com]

Хороший перевод.

[ulysses4ever.livejournal.com]

Спасибо вам за перевод, у нас товарищ воспользовался.

Есть вопрос не по переводу, а по сабжу. Может, вы попробуете помочь... Касается таблицы приписывания типа для λ2 (стр. 5 вашего перевода в последней версии). А именно последнего её правила, введения квантора всеобщности. Вопрос: там справа написано α \not\in FV(Г) — непонятно, какой в этом смысл, ведь Г это просто набор типизированных переменных. Гипотеза: должно быть FV(A). Как вы думаете, нет ли там опечатки?

[deni-ok.livejournal.com]

Нет, думаю что нету. Если одним и тем же именем (скажем x) обозвать термовую переменную из контекста и типовую переменную, то могут возникнуть непонятные аппликации в термах. Например, (f x) - это применение терма к терму x или терма к типу x?

И вообще в этой науке все свободные переменные справа от |- описываются слева от |- (в том числе и типовые). Скажем у Пирса в TAPL так сделано уже для System F, а у Барендрегта - в следующих системах. То, что здесь типы описываются слегка неформально - недостаток, оставленный скорее из педагогических соображений.

[ulysses4ever.livejournal.com]

Спасибо!