Нищета и беспомощность просто типизированной лямбды

[deniok]

  Возьмём терм

pre = \m.m pf pz (\t f.t)
pf = \p f.f(p(\t f.f))(\s z.s(p(\t f.f) s z))
pz = \f.f(\s z.z)(\s z.z)

который работает в бестиповой лямбде предесессором для чисел Чёрча:

pre (\s z.s(s(s z))) ->> \s z.s(s z)
pre (\s z.s(s z)) ->> \s z.s z
pre (\s z.s z) ->> \s z.z
pre (\s z.z) ->> \s z.z

(Рассказывают, что идея подобного предесессора пришла в голову Клини, когда он находился под воздействием веселящего газа при удалении четырёх зубов мудрости.)

Предесессор этот типизируем в просто типизированной лямбде страшным и ужасным типом, который слишком бесчеловечен, чтобы приводить его здесь. Желающие могут find'n'replace точечку на стрелочку (->) и отдаться в руки GHCi. Также типизируемы все его аппликации к числам Чёрча, тип их (в отличие от) благообразен и приятен глазу, ибо ожидаем : (a -> a) -> a -> a.

Имея pre, хочется определить вычитание. Это легко делается в бестиповой системе

minus = \k l.l pre k

Работает ли такой подход в просто типизированной лямбде? На первый взгляд да, тип может быть приписан этому терму, желающие на него взглянуть опять-таки отсылаются в GHCi. К несчастью этот minus умеет, оставаясь типизированным, вычитать числа, не большие единицы. Скажем

minus (\s z.s(s(s z))) (\s z.s z) ->> \s z.s(s z)

ещё работает, обладая пристойным типом (a -> a) -> a -> a на всех 27 шагах редукции (счёт вёлся для нормальной стратегии). А вот вычитание из числа 3 числа 2 хоть и даёт 1 при редукциях, но не позволяет типизировать нередуцированный терм.

minus (\s z.s(s(s z))) (\s z.s(s z)) ->> \s z.s z

Кстати говоря, место где типизация волшебным образом возникает, находится почти в самом начале цепочки редукций. Из 43 шагов этого вычитания 40 последним может быть приписан тип (a -> a) -> a -> a, последний нетипизируемый терм

(\s z.s(s z)) pre (\s z.s(s(s z))) 

а следующий в редукционной цепочке

(\z.pre (pre z)) (\s z.s(s(s z))) 

уже согласен приписать себе обычный числовой тип.

Может кто-нибудь, кстати, придумать более простой, чем предесессор Клини, терм, обладающий таким же свойством: (\s z.s(s z)) term не имеет типа, а единожды редуцированный (\z.term (term z)) уже типизируем?

 

Comments

[codedot.livejournal.com]

(\s.s s) (\x.x).

[deni-ok.livejournal.com]

Ну да, если иллюстрировать ту идею, что переменные обязаны иметь один и тот же тип во всех вхождениях, а замещающие их при подстановке термы - не обязаны. Но задачка была про двойку Чёрча.

[codedot.livejournal.com]

Для меня загадка, почему вдруг речь стала идти о сохранении типов подвыражений терма, который в постановке задачи обязан до первой редукции никакого типа не иметь вовсе. Или же есть какие-то условия, не обозначенные явно?

[deni-ok.livejournal.com]

Вроде условие ясно написано:
придумать более простой ... терм, обладающий таким ... свойством: (\s z.s(s z)) term не имеет типа, а единожды редуцированный (\z.term (term z)) уже типизируем?

Если понимать ваш терм как ответ на эту задачу

term = (\s.s s)(\x.x)

то нет, единожды редуцированный

\z.(\s.s s)(\x.x)((\s.s s)(\x.x) z)

не типизируем.

Но я так понял, что вы написали максимально простой нетипизируемый терм, у которого типизация появляется после одной редукции. Моё замечание было про причину, по которой после редукции возникает типизируемость.

[codedot.livejournal.com]

Хм, тогда задача тривиальна, так как любой комбинатор M, имеющий тип, подходит на место term, в том числе I.

[deni-ok.livejournal.com]

Нет нетипизируемости до редукции (\s z.s(s z))(\x.x) : a -> a

[nivanych.livejournal.com]

> Нищета и беспомощность просто типизированной лямбды

Да! И приходится вводить индуктивные типы бесовские!

[deni-ok.livejournal.com]

Грех! Грех!

Потом некоторые в твиттере из-за бугра плюют, мол лямбда-то не ultimate!

[nivanych.livejournal.com]

Так и до топологии недалеко!

[thesz.livejournal.com]

И это хорошо, что не ultimate. ;)

[codedot.livejournal.com]

Должен сказать, что меня всегда настораживает упоминание цифр Черча вместо стандартной цифровой системы для λK. Едва ли кому-то в наши дни интересно λI-исчисление, где цифровые системы типа цифр Черча - единственная возможность.