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

[deni_ok]

  Возьмём терм
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 (Рассказывают, что идея подобного предесессора

Comments

[deni_ok]

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

[deni_ok]

Вроде условие ясно написано:
придумать более простой ... терм, обладающий таким ... свойством: (\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)
не типизируем.

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

[nivanych]

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

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

[deni_ok]

Грех! Грех!

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

[nivanych]

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

[thesz]

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