![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Читая Джо Уэллса
Jun. 24th, 2013 06:14 pmЗнаете ли вы, чем замечателен этот λ-терм?
Первый такой терм придумали P. Giannini, F. Honsell и S. Ronchi Della Rocca из Миланского университета в 1987 году. А этот я взял из статьи J. B. Wells, Typability and Type Checking in System F Are Equivalent and Undecidable (1998).
λ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).
