Cat's cradle

Моя собака болеет: у него загноились глаза и белки красные. Вид, конечно, ужасный. И сегодня в первый раз за долгое время он заскулил, когда я ушел и оставил его одного. Такой протяжный вой, в котором куча досады и непонимания.

P.S. Собака закрыла дверь с той стороны на щеколду. Сидел в интернете через домашний вайфай, ждал мастера около двери. Задумался о пользе вайфая.

Скинули тут хорошую мантру. Завораживет.

Навелосипедил простую переключалку между буферами текущего major-mode.
Потому что не нашел из сотни переключалок буферов нужную с простым решением.

https://github.com/4DA/emacs-stuff/blob/master/mode-cycle.el

Завел себе собаку. Назвал его Люк. В честь кого - должно быть понятно.
 

Реализация зависимых типов в Shen.

Итак, продолжим заниматься исследованием языка Shen, а частности его системы типов, основанной на sequent calculus.


( Read more... )

http://cs.ioc.ee/ewscs/2012/

Френды, кто-нибудь поедет?

Взял напоиграться язык shen (продолжение идеи Qi).

shen/Qi - этакий lisp с pattern-matching'ом, статической типизацей, и оригинальной системой типов, основанной на sequent calculus.

Реализовал быструю сортировку.
Замечу, что остуствуют сигнатуры функций, которые записываются так:
    {typeA -> typeB}

Стандартная библиотека еще не готова, а filter в базовый язык, к сожалению,
не входит.

Язык пока оставляет приятное впечатление, но без достаточного пула библиотек - всего лишь игрушка.


(define filter
    _ [] -> []
    T? [A] -> [A] where (T? A)
    T? [A|B] -> (append [A] (filter T? B)) where (T? A)
    T? [_|B] -> (filter T? B))

(define left-par
    S EN -> (filter (> (nth EN S) ) S)
    [] _ -> _)

(define right-par
    S EN -> (filter (< (nth EN S) ) S)
    [] _ -> _)

(define q-sort
    [] -> []
    [A|B]-> (append (q-sort (left-par [A|B] 1))
                            [A]
                            (q-sort (right-par [A|B] 1))))

Напросился на телефонное интервью в Microsoft.

Ну что же, позвонили=)

По сути это был простой sanity check: Спрашивали об опыте работы, проектах, была пара простых задач, как определение слова на палиндромичность.

Была одна интересная задача:

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

Есть у кого нетривиальные варианты?

Навыки разговрного английского, к сожалению, теряются, надо восстанавливать.


Upd. Написали, что не подхожу им.

Читал тут про Неймана, наткнулся на такую вещь:

…На протяжении всей жизни фон Нейман любил поражать друзей и учеников своей способностью производить в уме сложные вычисления (отсюда и название нашей статьи, повторяющее эпитеты, используемые во множестве статей о фон Неймане). Когда же приходилось писать на доске, он заполнял ее формулами, а потом стирал их настолько быстро, что однажды кто-то из коллег, понаблюдав за очередным объяснением, пошутил: «Понятно. Это доказательство методом стирания».

В виде примера его умения счёта можно привести такой полулегендарный случай. Во время работы в Лос-Аламасе над атомным проектом понадобилось срочно рассчитать какой-то процесс. За него сразу взялись трое, три безусловных гения: Ричард Фейнман, обложенный справочниками и с самым быстрым электрическим калькулятором, Энрико Ферми с логарифмической линейкой и листами бумаги и Джон фон Нейман, считавший в уме, без записей. Результаты они получают почти одновременно – все совпадают!

Считали они, конечно, совсем по разному. Тут будет уместно привести рассказ об одной задаче, который повторяется чуть ли не на половине сайтов о фон Неймане в интернете (их многие сотни!). Задача эта такова: два локомотива начинают двигаться навстречу друг другу с расстояния в 200 км со скоростью 50 км/час. С переднего стекла одного из локомотивов слетает муха (или птица) и летит ко второму со скоростью 75 км/час, затем от него поворачивает к первому и т.д. Спрашивается, какой путь она пролетит ко времени их сближения. Фон Нейман через секунду выдал ответ: 150 км и пояснил, что просто просуммировал бесконечный, но убывающий ряд отрезков, пролетаемых мухой.

Ответ, конечно, правильный, а метод решения характерен для математика с изощренной техникой счёта. Физик решал бы задачу совсем по-другому: локомотивы движутся до сближения два часа, муха всё это время в полете, поэтому она пролетает точно 150 км – почувствуйте разницу в стиле мышления: прямо, «в лоб», у математика, невзирая на счётные трудности, и более интуитивный, как бы взирая сверху, у физика.
Довольно занимательно. «Физическое» решение довольно тривиальное, а вот решение в лоб Неймана чуть сложнее…

Найдем, сколько времени будет лететь муха до «противоположного локомотива»:

Отсюда получим, что муха пролетела км

За время ч. локомотивы проехали каждый по 80 км,
получается, расстояние между ними сейчас – 40 км.
Муха пролетит его за ч.

Можно догадаться, что расстояние, которое в итоге пролетит муха равно

Это выражение – не что иное, как сумма бесконечно убывающей геометрической прогрессии, известной со школы.

(нужно вычесть первый член ряда, т.к он нас не интересует)

Вот такое, видимо, гениальный Нейман посчитал за одну секунду … =)

Хочу в магистратуру по математике.

Написал немцам в Гамбург, можно ли к ним поступить в математическую магистратуру с моим образованием (информационные системы)

Написали:

>Dear Mr. Cherkassov,
>an application is possible. Anyhow, you have to proof that you have >sufficient proficiency in mathematics.

Как, интересно, я должен подтвердить свою sufficient proficiency in mathematics?

В магистратуре ГУ ВШЭ, куда я думаю поступать этим летом хотя бы тематика задач на экзамен известны:

http://www.hse.ru/data/2010/01/29/1229771793/programVer2.pdf

Правда, от этого не легче, учитывая то, что курс анализа был у меня только на первом курсе, да и тот - дохленький;)