Доклад на SPbHUG 19.09.2008
Sep. 20th, 2008 10:44 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
deniokСделал вчера на очередной встрече SPbHUG доклад про лямбда-куб Барендрегта (подробности см. на юзерпике).
Народ (которого было как селедок в бочке, ну то есть неожиданно много) сильно повеселила чудесная аксиома:
Выложил на сайте SPbHUG слайды к докладу и мой перевод на русский (с комментариями) первого раздела пятой главы замечательного обзора Хенка Барендрегта: Henk Barendregt, Lambda calculi with types, в Handbook of Logic in Computer Science. Угощайтесь на здоровье, кто в английском не столь искушен как в русском.
Народ (которого было как селедок в бочке, ну то есть неожиданно много) сильно повеселила чудесная аксиома:
Выложил на сайте SPbHUG слайды к докладу и мой перевод на русский (с комментариями) первого раздела пятой главы замечательного обзора Хенка Барендрегта: Henk Barendregt, Lambda calculi with types, в Handbook of Logic in Computer Science. Угощайтесь на здоровье, кто в английском не столь искушен как в русском.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2008-09-21 07:36 pm (UTC)no subject
Date: 2008-09-22 05:05 am (UTC)Кстати, ты к вычитке перевода TAPL не присоединился?
no subject
Date: 2008-09-22 09:49 am (UTC)Выкрою - поучаствую...
no subject
Date: 2008-09-22 12:14 pm (UTC)no subject
Date: 2009-01-18 01:23 pm (UTC)no subject
Date: 2010-01-16 11:13 pm (UTC)Есть вопрос не по переводу, а по сабжу. Может, вы попробуете помочь... Касается таблицы приписывания типа для λ2 (стр. 5 вашего перевода в последней версии). А именно последнего её правила, введения квантора всеобщности. Вопрос: там справа написано α \not\in FV(Г) — непонятно, какой в этом смысл, ведь Г это просто набор типизированных переменных. Гипотеза: должно быть FV(A). Как вы думаете, нет ли там опечатки?
no subject
Date: 2010-01-17 01:55 pm (UTC)И вообще в этой науке все свободные переменные справа от |- описываются слева от |- (в том числе и типовые). Скажем у Пирса в TAPL так сделано уже для System F, а у Барендрегта - в следующих системах. То, что здесь типы описываются слегка неформально - недостаток, оставленный скорее из педагогических соображений.
no subject
Date: 2010-01-18 08:29 am (UTC)