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

[deniok]

Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите.

Comments

[ulysses4ever.livejournal.com]

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

[nivanych.livejournal.com]

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

[nponeccop.livejournal.com]

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

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

В-общем, хотелось бы видеть какое-то уточнение о структуре "набора переменных".

Далее, надо уточнить структуру контекста. Записи "x : a in Г" и "Г, x : a" - это исторически сложившееся недоразумение. Первая запись пришла из теории множеств, а вторая - из исчисления секвентов. Проблема тут в том, что секвенты, в отличие от множеств, - синтаксические конструкции, и чтобы "запятая" работала, в исчислении секвентов используются структурные правила. Думаю, надо унифицировать запись. Т.к. x in Г на языке секвентов формулируется громоздко, предлагаю сделать Г официально множеством и заменить эту пугающую запятую на Г U { x : a }.

Можно отдельно дописать что часто используется запись Г, x : a. Ну и дать ссылку на истоки нотации (естественную дедукцию и исчисление секвентов).

[ro-che.info (from livejournal.com)]

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

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

[deni-ok.livejournal.com]

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