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

[deniok]

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

Comments

[ulysses4ever.livejournal.com]

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

[ulysses4ever.livejournal.com]

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

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

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

[juan-gandhi.livejournal.com]

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

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

[thedeemon.livejournal.com]

А что вместо них? Пи и сигма?

[nivanych.livejournal.com]

;-) Алгорифм Маркова.

[nponeccop.livejournal.com]

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

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

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

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

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

[nponeccop.livejournal.com]

;-) Грамматики, конечно же

[thedeemon.livejournal.com]

Есть что почитать на эту тему?
Примерно в эту сторону у меня давно мысли крутятся, но не уверен, что мы об одном и том же.

[nivanych.livejournal.com]

Если я правильно понятно, то это всякие вариации rewriting'ов.
Если уже даже перепись строчки можно сделать Тьюринг-полной, то деревья и подавно.
Ну и плюс к тому, алгорифм Маркова, это по сути и есть грамматика нулевого типа.
Однако, я давно уже переболел ими ;-)

Я же хочу категорное.
По сравнению с лямбдами, разве что, для практики существеннен всякий scope.
А описание гораздо чище. И не надо приводить мне в сравнение хацкелевой бесточечный стиль.

[nponeccop.livejournal.com]

http://en.wikipedia.org/wiki/Chomsky_hierarchy
http://en.wikipedia.org/wiki/Rewriting

Можете почитать книгу parsing techniques (там, правда, совсем обзорно о тьюринг-полноте неограниченных грамматик) и про системы перезаписи в Plasmeier-Eckelen (системы перезаписи основаны на той же идее, что и грамматики, но эмуляция хаскеля более очевидна).

[thedeemon.livejournal.com]

А, это я читал уже.

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

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

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

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

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

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

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

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

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

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

Индукцией по генерации M вроде даказывается.
Я ж выше привел пример, когда это просто неверно.

Не предполагая этого правила ("в контекст можно добавлять "свежую" для этого контекста переменную"), тип (\x:a.\x:b.x) вывести нельзя.

Поэтому это правило надо формально добавить в набор правил типизации.

[deni-ok.livejournal.com]

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

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

Если связанных с ней переименований не предполагать, то перестаёт работать лемма генерации (у Пирса - лемма инверсии)

 (Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ (Γ,x:σ ⊢ M:τ ∧ ρ = σ → τ) 

поскольку мы не можем более предполагать, что x∉Γ.

Да, в таком виде, конечно, работать не будет. Но работает тривиальная модификация;

(Γ ⊢ λx:σ.M):ρ ⇒ ∃ τ: ∃ Γ' ⊆ Γ: (Γ',x:σ ⊢ M:τ ∧ ρ = σ → τ)

На самом деле, я ничего не имею против отождествления альфа-эквивалентных термов. Но оно не было оговорено в статье. Я всего лишь заметил, что исходя из того, что описано в статье, приведенный терм не типизируется.

[deni-ok.livejournal.com]

Согласен, без какой-то обработки альфа-эквивалентных термов или дополнительных правил типизации этот терм не типизируется. Но мне кажется, что это такой немножко маргинальный факт, касающийся скорее весьма свободной дисциплины именования переменных "пользователем", а не коренных свойств этой системы типов. Я думаю, что в небольшой энциклопедической статье его обсуждать было бы неуместно. К тому же в обоих АИ для статьи (Барендрегт и Пирс) простые типы типизируются именно так, с одной аксиомой (и подразумеваемым соглашением Барендрегта).