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-27 07:27 am (UTC)(link)
Если говорить очень грубо, то здесь возникает система неравенств на типы, в отличие от обычного Хиндли-Милнера, где мы имеем дело с системой уравнений. В последнем случае мы дальше делаем унификацию по Робинсону и все чики. А для неравенств дело дрянь. Джо Уэллс показал, что эта задача с помощью специальной тета-редукции сводится к SUP (Semiunification Problem), которая неразрешима. То есть ручками, конечно, можно терм перебирать, но важно понимать, что, даже составив правильную систему неравенств, мы не имеем универсального механизма решения.

[identity profile] kodt-rsdn.livejournal.com 2013-06-30 12:29 pm (UTC)(link)
Но мы ведь можем в любой момент спрыгнуть до галимой динамики.
Сказать: "чёрт его знает, что там за точный тип, но, как минимум, forall a b . a-> b на самом верхнем уровне".
Или сам момент принятия решения "пора валить" не определён, и получается, как с шампунем: намылить-смыть-повторить?

[identity profile] kodt-rsdn.livejournal.com 2013-06-30 12:45 pm (UTC)(link)
Про ручки - такой ещё момент.
Вот у нас есть куча переменных.
Каждой из них мы можем присвоить тип forall a.a или не присвоить, и посмотреть, как решатель будет выкручиваться.

Поскольку количество переменных конечно, то у нас есть 2n вариантов.
Какие-то из этих вариантов (v :: forall a . a) являются решениями-ловушками, оценкой снизу.

Остаётся только выбрать, что из всего этого подходит нам лучше всего.
Например, по количеству вынужденно задействованных кванторов. Чем меньше (или: чем глубже от корня), тем лучше.
Могут ли при этом возникать равнозначные варианты, между которыми мы просто не можем сделать выбор? Ну, скажем, forall a . a -> b и forall b . a -> b, при том, что xz -> yt у нас не получился.

Можно ли такое пространство равнозначных вариантов объединить в один надтип?
Я понимаю, что это, в любом случае, комбинаторный взрыв. Но, чисто теоретически, не?

(Извини, если задаю ламерские вопросы: в недра лямбда-куба не вкурил)

[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: левый аппликанд имеет тип (∀α.α)→(∀β.β), а правый - несовместимый никоим образом ∀α.α→α.