Я вот за годы знакомства с сабжем как-то незаметно пришёл к выводу, что правильный перевод названия: «лямбда-исчисление с простыми типами». Но это так, мысли вслух. А по существу: спасибо за вашу работу!
Если я правильно понятно, то это всякие вариации rewriting'ов. Если уже даже перепись строчки можно сделать Тьюринг-полной, то деревья и подавно. Ну и плюс к тому, алгорифм Маркова, это по сути и есть грамматика нулевого типа. Однако, я давно уже переболел ими ;-)
Я же хочу категорное. По сравнению с лямбдами, разве что, для практики существеннен всякий scope. А описание гораздо чище. И не надо приводить мне в сравнение хацкелевой бесточечный стиль.
Можете почитать книгу parsing techniques (там, правда, совсем обзорно о тьюринг-полноте неограниченных грамматик) и про системы перезаписи в Plasmeier-Eckelen (системы перезаписи основаны на той же идее, что и грамматики, но эмуляция хаскеля более очевидна).
Исчисление с * -> * -> * забыли, которое упоминается в Барендрегте, емнип.
В английской википедии интересно написано - говорится, что базовые типы - не синтаксические конструкции, а элементы некоего базового множества. Таким образом, "исчисление со звёздочками" получается автоматически при выборе одноэлементного множества базовых типов, и его не надо упоминать отдельно.
В-общем, хотелось бы видеть какое-то уточнение о структуре "набора переменных".
Далее, надо уточнить структуру контекста. Записи "x : a in Г" и "Г, x : a" - это исторически сложившееся недоразумение. Первая запись пришла из теории множеств, а вторая - из исчисления секвентов. Проблема тут в том, что секвенты, в отличие от множеств, - синтаксические конструкции, и чтобы "запятая" работала, в исчислении секвентов используются структурные правила. Думаю, надо унифицировать запись. Т.к. x in Г на языке секвентов формулируется громоздко, предлагаю сделать Г официально множеством и заменить эту пугающую запятую на Г U { x : a }.
Можно отдельно дописать что часто используется запись Г, x : a. Ну и дать ссылку на истоки нотации (естественную дедукцию и исчисление секвентов).
Да, я там явно не сказал про операцию расширения контекста: в контекст можно добавлять "свежую" для этого контекста переменную. Да. То есть надо ввести правило (Г |- M:t) => (Г,x:t' |- M:t)
А с этим правилом аксиому для переменной можно упростить таким образом: x:t |- x:t.
При типизации лямбды, кстати, эта возможность используется без явной оговорки. Не понял, о чем ты, честно говоря. Типизация какой лямбды?
Ну я, конечно, пользуюсь ещё Thinning Lemma: если один контекст является подмножеством другого, то утверждения о типизации, сделанные в более узком контексте, верны в более широком.
Чтобы это было леммой, оно должно доказываться из аксиом :)
На самом деле, я ничего не имею против отождествления альфа-эквивалентных термов. Но оно не было оговорено в статье. Я всего лишь заметил, что исходя из того, что описано в статье, приведенный терм не типизируется.
Согласен, без какой-то обработки альфа-эквивалентных термов или дополнительных правил типизации этот терм не типизируется. Но мне кажется, что это такой немножко маргинальный факт, касающийся скорее весьма свободной дисциплины именования переменных "пользователем", а не коренных свойств этой системы типов. Я думаю, что в небольшой энциклопедической статье его обсуждать было бы неуместно. К тому же в обоих АИ для статьи (Барендрегт и Пирс) простые типы типизируются именно так, с одной аксиомой (и подразумеваемым соглашением Барендрегта).
![[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
Date: 2013-01-06 08:39 pm (UTC)no subject
Date: 2013-01-07 01:48 am (UTC)Хотя и чем дальше, чем больше, я лично к лямбдам отношусь всё более не очень хорошо ;-)
no subject
Date: 2013-01-07 04:44 am (UTC)no subject
Date: 2013-01-07 05:15 am (UTC)Спасибо за статью.
no subject
Date: 2013-01-07 11:23 am (UTC)no subject
Date: 2013-01-07 11:25 am (UTC)no subject
Date: 2013-01-07 11:51 am (UTC)no subject
Date: 2013-01-07 12:05 pm (UTC)Примерно в эту сторону у меня давно мысли крутятся, но не уверен, что мы об одном и том же.
no subject
Date: 2013-01-07 01:05 pm (UTC)Если уже даже перепись строчки можно сделать Тьюринг-полной, то деревья и подавно.
Ну и плюс к тому, алгорифм Маркова, это по сути и есть грамматика нулевого типа.
Однако, я давно уже переболел ими ;-)
Я же хочу категорное.
По сравнению с лямбдами, разве что, для практики существеннен всякий scope.
А описание гораздо чище. И не надо приводить мне в сравнение хацкелевой бесточечный стиль.
no subject
Date: 2013-01-07 01:11 pm (UTC)http://en.wikipedia.org/wiki/Rewriting
Можете почитать книгу parsing techniques (там, правда, совсем обзорно о тьюринг-полноте неограниченных грамматик) и про системы перезаписи в Plasmeier-Eckelen (системы перезаписи основаны на той же идее, что и грамматики, но эмуляция хаскеля более очевидна).
no subject
Date: 2013-01-07 03:02 pm (UTC)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
Date: 2013-01-11 09:10 am (UTC)Да. То есть надо ввести правило
(Г |- M:t) => (Г,x:t' |- M:t)А с этим правилом аксиому для переменной можно упростить таким образом:
x:t |- x:t.Не понял, о чем ты, честно говоря. Типизация какой лямбды?
Чтобы это было леммой, оно должно доказываться из аксиом :)
no subject
Date: 2013-01-11 10:33 am (UTC)Я ж выше привел пример, когда это просто неверно.
Не предполагая этого правила ("в контекст можно добавлять "свежую" для этого контекста переменную"), тип
(\x:a.\x:b.x)вывести нельзя.Поэтому это правило надо формально добавить в набор правил типизации.
no subject
Date: 2013-01-12 10:17 am (UTC)Да, в таком виде, конечно, работать не будет. Но работает тривиальная модификация;
(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ: ∃ Γ' ⊆ Γ: (Γ',x:σ ⊢ M:τ ∧ ρ = σ → τ)На самом деле, я ничего не имею против отождествления альфа-эквивалентных термов. Но оно не было оговорено в статье. Я всего лишь заметил, что исходя из того, что описано в статье, приведенный терм не типизируется.
no subject
Date: 2013-01-12 10:37 am (UTC)no subject
Date: 2013-01-11 08:22 pm (UTC)Случайно, одним движением, удалил весь десяток своих комментов к посту.