Просто типизированное лямбда-исчисление

[deni_ok]

Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите. Originally posted at http://deniok.dreamwidth.org/47521.html. Feel free to comment here or there.

Comments

[ulysses4ever]

Я вот за годы знакомства с сабжем как-то незаметно пришёл к выводу, что правильный перевод названия: «лямбда-исчисление с простыми типами». Но это так, мысли вслух. А по существу: спасибо за вашу работу!

[ulysses4ever]

Если бы у меня были лекции по ЛИ, я бы к ним с первого числа готовился, а у меня лекции по такой гадости, что я начну, наверное, ближе к февралю… :(

[nivanych]

Годно. Опечаток не заметил.
Хотя и чем дальше, чем больше, я лично к лямбдам отношусь всё более не очень хорошо ;-)

[nivanych]

Ну вот ещё, к чему этот экстремизм, это расжигание! ;-)

[ex_juan_gan]

Бета-редуцируй.

Спасибо за статью.

[nponeccop]

Исчисление с * -> * -> * забыли, которое упоминается в Барендрегте, емнип

[ext_4199]

Из этих правил типизации не получится вывести (\x:a.\x:b.x) : a->b->b

(Я предполагаю, что в контексте все переменные различны.)

[ext_4199]

Да, я там явно не сказал про операцию расширения контекста: в контекст можно добавлять "свежую" для этого контекста переменную.
Да. То есть надо ввести правило
(Г |- M:t) => (Г,x:t' |- M:t)

А с этим правилом аксиому для переменной можно упростить таким образом:
x:t |- x:t.

При типизации лямбды, кстати, эта возможность используется без явной оговорки.
Не понял, о чем ты, честно говоря. Типизация какой лямбды?

Ну я, конечно, пользуюсь ещё Thinning Lemma: если один контекст является подмножеством другого, то утверждения о типизации, сделанные в более узком контексте, верны в более широком.

Чтобы это было леммой, оно должно доказываться из аксиом :)

[deni_ok]

Блин, поганый ЖЖ!
Случайно, одним движением, удалил весь десяток своих комментов к посту.