deniok: (typed lambda)
[personal profile] 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).

This account has disabled anonymous posting.
If you don't have an account you can create one now.
No Subject Icon Selected
More info about formatting

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 3rd, 2025 05:22 am
Powered by Dreamwidth Studios