Я вот за годы знакомства с сабжем как-то незаметно пришёл к выводу, что правильный перевод названия: «лямбда-исчисление с простыми типами». Но это так, мысли вслух. А по существу: спасибо за вашу работу!
Исчисление с * -> * -> * забыли, которое упоминается в Барендрегте, емнип.
В английской википедии интересно написано - говорится, что базовые типы - не синтаксические конструкции, а элементы некоего базового множества. Таким образом, "исчисление со звёздочками" получается автоматически при выборе одноэлементного множества базовых типов, и его не надо упоминать отдельно.
В-общем, хотелось бы видеть какое-то уточнение о структуре "набора переменных".
Далее, надо уточнить структуру контекста. Записи "x : a in Г" и "Г, x : a" - это исторически сложившееся недоразумение. Первая запись пришла из теории множеств, а вторая - из исчисления секвентов. Проблема тут в том, что секвенты, в отличие от множеств, - синтаксические конструкции, и чтобы "запятая" работала, в исчислении секвентов используются структурные правила. Думаю, надо унифицировать запись. Т.к. x in Г на языке секвентов формулируется громоздко, предлагаю сделать Г официально множеством и заменить эту пугающую запятую на Г U { x : a }.
Можно отдельно дописать что часто используется запись Г, x : a. Ну и дать ссылку на истоки нотации (естественную дедукцию и исчисление секвентов).
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
carisma_sensei
no subject
Date: 2013-01-06 08:32 pm (UTC)(no subject)
From:no subject
Date: 2013-01-07 01:48 am (UTC)Хотя и чем дальше, чем больше, я лично к лямбдам отношусь всё более не очень хорошо ;-)
(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2013-01-07 11:45 am (UTC)В английской википедии интересно написано - говорится, что базовые типы - не синтаксические конструкции, а элементы некоего базового множества. Таким образом, "исчисление со звёздочками" получается автоматически при выборе одноэлементного множества базовых типов, и его не надо упоминать отдельно.
В-общем, хотелось бы видеть какое-то уточнение о структуре "набора переменных".
Далее, надо уточнить структуру контекста. Записи "x : a in Г" и "Г, x : a" - это исторически сложившееся недоразумение. Первая запись пришла из теории множеств, а вторая - из исчисления секвентов. Проблема тут в том, что секвенты, в отличие от множеств, - синтаксические конструкции, и чтобы "запятая" работала, в исчислении секвентов используются структурные правила. Думаю, надо унифицировать запись. Т.к. x in Г на языке секвентов формулируется громоздко, предлагаю сделать Г официально множеством и заменить эту пугающую запятую на Г U { x : a }.
Можно отдельно дописать что часто используется запись Г, x : a. Ну и дать ссылку на истоки нотации (естественную дедукцию и исчисление секвентов).
no subject
Date: 2013-01-10 11:03 pm (UTC)(\x:a.\x:b.x) : a->b->b(Я предполагаю, что в контексте все переменные различны.)
(no subject)
From:(no subject)
From:(no subject)
From:(no subject)
From:no subject
Date: 2013-01-11 08:22 pm (UTC)Случайно, одним движением, удалил весь десяток своих комментов к посту.