deniok

04:19 pm - Знакомство с Coq

Скачал и поставил COQ. Это, если кто не знает, СУФД - система управления формальными доказательствами :-) Так у них на сайте написано

09:00 pm - Похоже действительно пора

На одном из вечеров Юлий Ким обратился к присутствующим: "В апреле 2008 года нас ожидает знаменательное событие: сороколетие первого выпуска "Хроники текущих событий". Надо бы подумать, как лучше это отпраздновать".
Из зала тут же ответили: "Начать выпускать снова".

04:13 pm - Попивая прекрасный аргентинский мальбек...

....осознаю себя националистом. То есть, если Латинская Америка, то я - аргентинец без вопросов. Ненавижу Перона, как положено аргентинскому интеллектуалу. Готов дать в морду всякому, кто скажет, что Борхес вторичен.
Но это - если Латинская Америка. А если Кавказ - то я, наверное, армянин. Наполовину. А на вторую - абхаз. Хотя вина на Кавказе только грузины умеют делать, такая вот загогулина :)))

02:53 pm - Пальмовое масло

Авария на масложирокомбинате: 10 тонн пальмового масла вылилось в реку в Santa Marta, Colombia.

с фотополигона

09:03 pm - Безтемное

Совершенно медитативная хрень. Сижу, щёлкаю.

07:05 pm - 10 простых правил выбора вина в магазине

Не могу не порекомендовать 10 простых правил выбора вина в магазине от человека, знающего толк в этом деле. Как впрочем и его регулярные обзоры вин.

[по наводке yorool_gui]

12:54 am - Тим Минчин

Давно не слушал правильного рок'н'ролла :)


Стырено у avva

03:06 pm - Лямбда, которую мы потеряли

Пара задачек по лямбда-исчислению.

(1) Сконструируйте лямбда-терм F, такой что для любого терма M выполнялось бы

FM = MF

GMN = NG(NMG)

01:55 am - Наблюдение за политикой именования языков

В 1997 небезызвестные Simon Peyton Jones и Erik Meijer предложили промежуточный внутри-компиляторный богато-типизированный язык Henk. Сегодня я понял причину, почему язык так назван. Механизм - тот же, что и в Хаскелле.

Henk Barendregt - голландский логик,  изобретатель лямбда-куба (1991), автор штудируемого мною нынче Lambda Calculi with Types. "Восхищайтесь" (с)thesz

08:52 pm - О сколько нам открытий чудных...

О сколько нам открытий чудных дарит изучение просто типизированной чистой лямбды.

Пусть есть лямбда-терм, который может быть редуцирован к другому лямбда-терму с помощью цепочки обычных бета-редукций:

Сохраняется ли при этом тип? То есть верно ли утверждение

(Двойная стрелочка читается "бета-редуцируемо к")

( Ответ под катом... )

05:31 pm - 50 лет пацифику

Впервые "пацифик" появился на публике ровно полвека назад, в холодную страстную пятницу, когда тысячи британских активистов борьбы против ядерного оружия отправились с лондонской Трафальгарской площади в 50-мильный марш на оружейный завод в Олдермастон.



Житель Лондона Джералд Холтом, дизайнер и отказник от военной службы времен Второй мировой, убедил DAC в том, что акция будет гораздо более действенной, если у нее появится собственная эмблема. И на свет появился символ "Запретить бомбу". Холтом подумывал над применением христианского креста, но в конце концов остановился на использовании символов английской мореходной семафорной азбуки - букв N (Nuclear - ядерный) и D (Disarmament - разоружение) - и заключил их в круг, символизирующий Землю.

via

01:11 pm - Мультик, которому 5000 лет

отсюда

12:41 pm - Здорово снято

photo_polygon , отсюда

01:08 pm - Всё под контролем :)

Перед поездкой в командировку в Новгород искал карту Новгорода. Сегодня в GMail вижу рекламную ссылку:



Скоро ни один наш шаг не останется незамеченным. Как тут.

12:12 pm - Материал к завтрашнему обсуждению

Материал к завтрашнему обсуждению на SpbHUG "Устройство компилятора GHC"






Стырено из первоисточника.

05:40 pm

Прекрасная логическая задачка с подробным обсуждением у avva. Формулировка там чуть-чуть неясная (допустимы формальные придирки), ниже, в комментах, vik_rud  дал более точный перевод (который я слегка причесал):

Есть остров, на котором проживает одно племя. Племя состоит из 1000 человек, имеющих разный цвет глаз. Их религия запрещает им знать их собственный цвет глаз или обсуждать эту тему с другими. Таким образом, каждый житель может видеть (и видит) цвет глаз всех других жителей, но не имеет никакого способа выяснить цвет собственных глаз (отражающие поверхности отсутствуют). Если житель выясняет каким-то образом цвет собственных глаз, то, в соответствии с религией, он обязан совершить ритуальное самоубийство в полдень следующего дня на глазах у всех остальных жителей. Все жители очень логичны и набожны, и каждый знает, что все жители очень логичны и набожны (и каждый знает, что каждый знает, что все жители очень логичны и набожны и т.д.)

Из 1000 островитян 100 имеют голубые глаза, а остальные 900 имеют карие глаза, хотя островитяне первоначально не обладают этими статистическими данными (каждый из них может видеть только 999 из 1000 жителей).

Однажды голубоглазый иностранец посещает остров и завоевывает полное доверие племени.

Как-то вечером, он обращается ко всему племени, и благодарит их за гостеприимство.

Однако, не зная местных обычаев, иностранец делает ошибку, упоминая цвет глаз в своем обращении: "Как необычно видеть другого голубоглазого человека, такого как я, в этой части света".

Какое воздействие эта бестактность окажет на племя?

avva

12:32 am - Какой грязный хак :)

suminit :: [Int] -> Int -> Int -> (Int,[Int]) 
suminit xs len acc | len `seq` acc `seq` False = undefined -- :)))
                   | len == 0  = (acc,xs) 
                   | otherwise = case xs of []   -> (acc,[]) 
                                            x:xs -> suminit xs (len-1) (acc+x)

09:05 pm - Антипаттерн?

Некоторое время пользовался вычурной техникой для работы с индексированными семействами функций. Есть семейство (список)

f :: Int -> a -> a

f n ( ... (f 3 (f 2 (f 1 x)))) ... )

chain_bad f n = foldl' (flip (.)) id $ map f [1..n]

*Tst> chain_bad (+) 10 0
55

(10+).(9+).(8+). ... .(1+).id $ 0

12:19 am - Recycling Continuations

Сегодня на LtU ссылка на статью Recycling Continuations, Jonathan Sobel and Daniel P. Friedman. ICFP 1998. Сделано на LISP, но при беглом взгляде очень похоже на зипперы. Хотя, возможно, это обманчиво...

Надо не забыть попозже разобраться.

12:19 am - Думские выборы прошли без нарушений :)

Пара картинок по явке, построенных на основании данных ЦИК:


Количество участков считается по центилям.



отсюда и отсюда


Встретим праздник круглыми цифрами!