deniok: (typed lambda)
deniok ([personal profile] deniok) wrote2013-06-24 06:14 pm

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

Знаете ли вы, чем замечателен этот λ-терм?
λ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).

[identity profile] deni-ok.livejournal.com 2013-06-30 04:39 pm (UTC)(link)
> Каждой из них мы можем присвоить тип forall a.a

нет, не можем:
> let good = (\(y::forall a.a->a)->y y) (\x->x)
> :t good
good :: a -> a
> let bad  = (\(y::forall a.a   )->y y) (\x->x)
Второе не выводится в системе F: левый аппликанд имеет тип (∀α.α)→(∀β.β), а правый - несовместимый никоим образом ∀α.α→α.