Читая Джо Уэллса

[deniok]

Знаете ли вы, чем замечателен этот λ-терм?

λv.(λy.λz.v(yy)(yz))(λx.(λa.λb.a)x(x(xv)v))(λw.ww)

Он нормализуем, его нормальная форма

λv.v(λx.x)(λw.ww)

Более того он нормализуем сильно, то есть независимо от редукционной стратегии. Однако ему нельзя приписать никакого типа, даже в полной версии System F.

Первый такой терм придумали P. Giannini, F. Honsell и S. Ronchi Della Rocca из Миланского университета в 1987 году. А этот я взял из статьи J. B. Wells, Typability and Type Checking in System F Are Equivalent and Undecidable (1998).

Comments

[migmit.livejournal.com]

Так вот зачем нужна динамическая типизация...

[kodt-rsdn.livejournal.com]

А там нельзя налепить что-то с горой forall'ов?

Поскольку есть yy, то
y :: forall y1 . y1 -> y2
Поэтому и yy, и yz :: y2

ww
w :: forall w1 . w1 -> w2
ww :: w2

x xv v
x :: forall x1 . x1 -> v -> x3

Ну и так далее