Home

deniok

Get your own code!
Locations of visitors to this page

May. 14th, 2008

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

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

Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine.


Интерактивная сессия неофита... )


Читаю крэш-курс Coq in a Hurry.

May. 13th, 2008

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

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

May. 8th, 2008

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

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

Apr. 27th, 2008

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


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

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

Apr. 21st, 2008

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

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

Tags:

Apr. 17th, 2008

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

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

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

Apr. 14th, 2008

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

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


Стырено у [info]avva

Apr. 3rd, 2008

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

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

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

FM = MF


(2) Сконструируйте лямбда-терм G, такой что для любых термов M и N выполнялось бы
GMN = NG(NMG)


Ответы не скринятся, так что если хотите думать сами - не смотрите в комменты.

Mar. 31st, 2008

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

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

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

Mar. 28th, 2008

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

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

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

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

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

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

Mar. 21st, 2008

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

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



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

via

Mar. 6th, 2008

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


отсюда

Mar. 2nd, 2008

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



[info]photo_polygon , отсюда

Feb. 16th, 2008

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

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



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

Feb. 15th, 2008

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

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






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

Feb. 13th, 2008

05:40 pm

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

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

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

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

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

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

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


UPD. По совету друзей приобрел автомобиль "Москвич" подкорректировал перевод. Фактически у [info]avva не очень ясно указано лишь, что статистика 100/900 неизвестна островитянам. Ну и подсказка "каждый знает, что каждый знает, ..." про общее знание опущена ;) Англоязычный оригинал.

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)
Найдено тут.

Feb. 10th, 2008

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

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

f :: Int -> a -> a
причём разные параметры Int задают разные элементы семейства f 1, f 2, f 3. При этом требуемая свёртка имеет вид
f n ( ... (f 3 (f 2 (f 1 x)))) ... )
Техника такая
chain_bad f n = foldl' (flip (.)) id $ map f [1..n]
Мэп делает список функций типа a->a, после чего идёт свёртка по композиции, ну и, скажем,
*Tst> chain_bad (+) 10 0
55
монтирует
(10+).(9+).(8+). ... .(1+).id $ 0
и вычисляет его.

Неприятности и их преодоление... )
И остается вопрос из заголовка: фолдить композицией список функций порожденный мэппингом - это таки антипаттерн из-за space leak?

Jan. 26th, 2008

12:19 am - Recycling Continuations

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

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

Tags: ,

Jan. 24th, 2008

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

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


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

льно

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


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

Navigate: (Previous 20 Entries)