А вот, кстати, что у нас в CS Клубе будет в конце сентября. Джон Хариссон прочитает 5 лекций про автоматическое доказательство теорем. Я считаю, что это замечательно. Originally posted at http://deniok.dreamwidth.org/50747.html. Feel free to comment here or there.

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

( Из жизни шляп... )

К вопросу о заселении ⊥ при включенном type-in-type. Делается прямой реализацией парадокса Рассела

{-# OPTIONS --type-in-type --without-K ( Read more... )

К завтрашнему занятию задачку со звёздочкой сделал, а то некоторые больно умные последние 15 минут практики бьют баклуши, решив всё заданное.
Введём следующий трёхпараметрический типовый оператор, инкапсулирующий композицию однопараметрических конструкторов типов:
newtype Compose f g x = Compose {getCompose :: f (g x)} Каков кайнд этого ( Read more... )

Эти ваши интернеты бурлят:
ru-marazm.livejournal.com/3591670.html
lj.rossia.org/users/tiphareth/1685303.html
Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:
_*_ : ℕ → ℕ → ℕ zero * n = zero suc m * n = n + (m * n) Впрочем внучке стоило бы снять все вопросы, предоставив доказательство
*-commutative : ∀ m n → m * n ≡ n * m Взяв ( Read more... )

А вот, кстати, при проверке лямбда-калькуляторов, написанных студентами, возникла такая задачка.
Пускай мы реализовали на Хаскелле лямбда-термы
data Term = Var String | App Term Term | Lam String Term проверку их альфа-эквивалентности (можно и точное совпадение, для наших целей не важно):
alphaEq :: Term -> Term -> Bool и ( Read more... )

Тут вопрос возник (не в первый раз):
typeof λx.x x Отвечаем, например, так
> :set -XRankNTypes > let f = (\x -> x x) :: (forall a. a -> a) -> (forall a. a -> a) > f id 42 42 Или так
> let f' = (\x -> x x) :: (forall a. a) -> (forall a. a) > f' undefined *** Exception: Prelude.undefined
Originally posted at http://deniok.dreamwidth.org/49632 ( Read more... )

  Возьмём терм
pre = \m.m pf pz (\t f.t) pf = \p f.f(p(\t f.f))(\s z.s(p(\t f.f) s z)) pz = \f.f(\s z.z)(\s z.z) который работает в бестиповой лямбде предесессором для чисел Чёрча:
pre (\s z.s(s(s z))) ->> \s z.s(s z) pre (\s z.s(s z)) ->> \s z.s z pre (\s z.s z) ->> \s z.z pre (\s z.z) ->> \s z.z (Рассказывают, что идея подобного предесессора ( Read more... )

Я всегда говорил христиАнин, а тут вдруг обнаружил, что вроде как положено христианИн. 
Для исследования истории вопроса я воспользовался поэтическим подкорпусом нашего национального корпуса.
 ( Что же выясняется?... )