Пляжное чтение

Масару Ибука. После трех уже поздно.

Автор - мудрый японец, один из основателей корпорации Сони и отец ребенка, отставшего в умственном развитии (изначально, - потом с ребенком, судя по книге все хорошо). Книга про воспитание детей.
После прочтения данной книги вы захотите:

• Отдать ребенка в класс игры на скрипке доктора Сузуки.
• Научить ребенка плавать во младенчестве.
• Купить ему нестандартный лист бумаги и карандаши.

Jon Barwise, Lawrence S. Moss. Vicious circles: on the mathematics of non-wellfounded phenomena. 

Джон Барвайс - очень известный американский математик. В 1982 году его "Handbook of Mathematical Logic" даже перевели на русский. Книга повсвящена гипермножествам (нефундированным множествам), - гипермножество может содержатся само в себе. Книга начинается с очень плотного и сильного (и немного нестандартного) введения в классическую аксиоматическую теория множеств - настолько плотную, что начав читать первую главу где-то полгода назад, я отложил Барвайса и прочитал книгу Шеня. На самом деле для прочтения дальнейших вводных (философских) глав знание аксиоматической теории множеств не особо требуется. Поэтому, если вы хотите без напряжения ознакомится с тем, про что книга, пропустите вторую главу и пробегите по главам части 2 "Vicious Circles". (Для чтения дальнейших частей - "Basic Theory", "Elementary Applications", "Further Theory" и "Further Applications" знание классической теории множеств все-таки потребуется.) Часть "Vicious Circles" очень познавательна - в ней рассматривается несколько теорий на стыке философии и логики, которые могут быть формализованы в теории гипермножеств. На меня очень сильное впечатление произвел парадокс Конвея (как неявное мое знание о том, что ты знаешь, что я знаю, влияет на принятие решений).

Познавательно, что теория гипермножеств получила свое развитие только в конце 1980-х под влиянием информатики  - классический труд Non-Well-Founded Sets by Peter Aczel (pdf) - именно в теоретической computer science мощь теории гипермножеств становится очевидной: бисимуляция, коалгебры, коданные, корекурсия, наибольшие неподвижные точки, самоприменимые программы, системы переходов (labeled transition systems), потоки (streams), модальные логики (используются в model checking). - Обо всем это рассказывается  в остальной части книги Барвайса.

Напомню, что аксиома регулярности (foundation axiom) звучит так: В любом непустом множестве A есть элемент B, непересекающийся с A.

Барвайс формулирует аксиому нерегулярности (anti-foundation axiom) так: любая плоская система уравнений имеет ровно одно решение. Поразительно, что аксиома нерегулярности звучит более математично и менее интуитивно. Собственно, весь материал книги основан на изучении аксиомы нерегулярности.

Книжка также доступна здесь.

(Вообще некоторые вещи основаны на аксиоме регулярности, но явным образом это не не проговаривается. Например, когда система типов - простое типизированное лямбда исчисление или система F - не разрешает иметь тип a = x → a, - это следствие неявно принятой аксиомы регулярности.)

После прочтения книги меня взволновал вопрос (в свете моих занятий суперкомпиляцией), - как много вещей в гипермножествах имеем "каноническое" представления и как там проработана проблема эквивалентности.

Саша Соколов. Школа для дураков

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

Нужно читать на одном дыхании.

(Последний раз я получал такое удовольствие от прозы, читая Михаила Шишкина. А у него вышла новая книжка - Письмовник.)

Э. Хант, Д. Томас. Программист-прагматик. Путь от подмастерья к мастеру

MUST READ. Однако, возможно, первые две главы покажутся скучными и слишком "общими местами" (композиционное сходство с книжкой Барвайса). Нужно немного потерпеть. Начиная с третьей главы мне было сложно оторваться от книжки.

Как несложно догадаться, продолжением данной книжки является ресурс The Pragmatic Bookshelf.

Я надеюсь, что под влиянием книжки курс моего движения развернется эдак на 90° в прагматическую сторону.

Местами авторы пишут очень смачно: "Многие книги и учебные пособия относят процедуру сбора исходных требований к начальной фазе проекта. Термин «сбор» напоминает о племени счастливых аналитиков, занимающихся собирательством камней-самородков мудрости, разбросанных по земле на фоне приглушенного звучания «Пасторальной симфонии». Этот термин напоминает о том, что все требования уже имеются в наличии, нужно лишь отыскать их, положить в корзину и весело шагать дальше. Это не совсем так."

Scala in Action. Впечатление

Книга Scala in Action by Nilanjan Raychaudhuri пока доступна только в черновом варианте и завершена только наполовину (8 глав из 14), однако уже вполне читабельна. У самого автора познавательный твиттер.

---

На момент прочтения книги были доступны следующие главы:

1. Why Scala?
2. Getting started
3. Revitalizing your object oriented skills 
4. Having fun with functional data structures
5. Building a web application in functional style
6. Connecting to a database
7. Making concurrent programming easy
8. Building confidence with testing

---

Общее впечатление: книга познавательна и полезна, автор хорошо образован и знает о чем пишет. Где надо, смело используется (или по крайней мере, упоминается) необходимый термин из теории, что внушает уважение, ибо книга вроде бы написана "for masses" - например, описано, что передача функций реализована через eta-expansion, много ссылок на haskell-wiki.

Не знаю, насколько книга будет полезна как введение в Scala, но книга очень хороша как обзор инструментов/библиотек плюс занимательное чтиво. Вообще, занимательные врезки и любопытные замечания автора - достоинство книги.

Из практически полезного разобрано:
MongoDB,  SBT, Scalaz, Squeryl, H2, jQuery UI, ScalaCheck, Specs. (Был впечатлен как красиво для SBT пишется собственный task.)

Для расширения горизонта упоминаются (иногда поверхностно объясняются):
ScalaQuery, Querulous, Scalate, Functional Java, JetLang, Kilim, Guice, Awaitility.

Удачные места в книге:

• Прекрасно объяснены инвариантность, ковариантность и контрвариантность типов через рассмотрение данных с точки зрения изменяемости: мутабельные данные должны быть инвариантны, read-only данные могут быть ковариантными. (А write-only данные могут быть контрвариантными.)
• Объяснены higher-kinded types (в Scala in Depth они объясняются более подробно).
• В главе про Actors неплохо описаны Reactors.

Цитаты на заметку:

• "If you are used to meta-programming in Ruby, Groovy or other programming languages, implicit conversions are Scala’s way of doing meta-­programming but in more controlled way."
• "Only handful of programmers knows how to write a correct concurrent application or program. The correctness of the program is very important here."
• "When Alan Kay first thought about object oriented programming his big idea was message passing. So in fact working with actors is more object-­oriented than you think."

Из вкусностей, которые пока не описаны (но будут): Akka, Lift,  DSLs.

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

Apropos

Малоизвестная работа по суперкомпиляции:
Stephan Diehl, A Prolog Positive Supercompiler, 1995
файл ps

Перекрестное опыление

Robert S. Boyer

J Strother Moore

В 2005 году премия ACM за достижения в области программных систем была присуждена Роберту Бойеру, Джею Муру и Мэту Кауфману за "пионерскую разработку эффективного доказывателя теорем (известного как доказыватель Бойера-Мура)".

Эта разработка, по сути дела, началась с диссертации Мура 1973 под названием "Вычислительная логика", которую, кстати можно скачать. (Диссертация Бойера также доступна). Программной статьей считается текст Бойера и Мура 1975 года "Proving Theorems about LISP Functions",  которая и по сей день будоражит ум и легко читается.

Укрощение строптивого кода: "Taming Code Explosion in Supercompilation"

В последние два-три года суперкомпиляция набирает обороты. Отрадно, что статья шведов Питера Джонсона и Йохана Нордландера,  посвященная суперкомпиляции, принята на PEPM 2011. Саму статью можно взять отсюда.

Почему суперкомпиляция пока что не идет в массы как промышленная технология? По большому счету, по трем причинам:

1. Масштабируемость -  в идеале суперкомпилятор должен выполнять работу за прогнозируемое время - практически любой нетривиальный суперкомпилятор рискует "зависнуть" (очень долго преобразовывать) какую-нибудь программу.
2. Риск взрывоопасного роста кода (code explosion) - некоторые хитрые программы могут в результате суперкомпиляции разбухать.
3. Как показала практика, суперкомпилированные программы с трудом поддаются другим оптимизациям. Например, отсуперкомпилированную программу с трудом пережевывает компилятор GHC.

Авторы исследуют способы решения первых двух проблем. Я не буду подробно описывать технические детали - их можно найти в статье. Опишу суть.

Эврика!! - "A Transformation System for Developing Recursive Programs" by Rod Burstall & John Darlington

Настоящая качественная научно-исследовательская работа не столько отвечает на все вопросы и ставит точки над всеми i (хотя без этого ее и не существует), сколько задает вопросы новые и открывает новые области исследований и горизонты. Ярким представителем такой науки является работа Рода Берстала и Джона Дарлингтона "A Transformation System for Developing Recursive Programs" 1977 года,  являющейся одной из самых часто цитируемых работ, посвященных преобразованиям программ. Текст статьи можно найти через citeseerx и google scholar, а заодно и посмотреть на другие работы, ссылающиеся на статью.

Немного об авторах. Авторы оставили большой след в информатике. Чего стоит то, что при документировании придуманного же ими языка NPL они придумали и использовали термин "set comprehension", ставший впоследствии "list comprehension" (link1, link2). Язык NPL и его потомок язык Hope были одними из первых языков, где использовались алгебраические типы данные и сопоставление с образцом ("History of Haskell" by Paul Hudak, John Hughes, Simon Peyton Jones, Philip Wadler). Род Берсталл считает главным своим интересом тибетский буддизм (автобиография), а Джон Дарлингтон последнее время занимается грид-вычислениями.

Как говорил Набоков в "Лекциях по зарубежной литературе", настоящее чтение - это перечитывание. Работу Берстала и Дарлингтона (БД) я пробежал года 3 назад без детального вглядывания, но читая различную литературу по методам преобразования программ, то там то сям натыкался на фразы, что это вот это вот соответствует тому, что БД называет "эврика" и что является самым главным шагом любого преобразования. Такое сравнение я встречал достаточно часто, поэтому у меня непроизвольно сложилось впечатление, что БД - некоторая магия, где самое главное - эврика. При перечитывании все оказалось более интересно.

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

1. Definition - добавить к системе новое уравнение (конечно, добавляется так, что нет противоречия с существующими).
2. Instantiation - специализация существующего уравнения. Например, есть уравнение f(x) = x. Можно добавить уравнение f(0) = 0; 
3. Unfolding - Пусть есть уравнение e1 = e2. Тогда в правой части некоторого уравнения e1 можно заменить на e2.
4. Folding - Обратное развертке - e2 можно заменить на e1.
5. Abstraction - ввести локальные определения (вроде let-выражений). Этот шаг позволяет избежать повторных вычислений. Например f(g(x), g(x)) можно заменить на f(y, y) where y = g(x).
6. Laws - встроенные в систему свойства ассоциативности, коммутативности и т.д. операций.

Затем говорится, что такое отношение частично корректно. - Если преобразованная функция завершается и выдает какой-то результат, то этот результат соответствует тому, что выдает исходная функция. Свойства завершаемости в общем случае не сохраняются - преобразованная функция может не завершаться, тогда как исходная завершается.

Дальше самое интересное - надо задать стратегию применения этих правил.

Авторы предлагают простую стратегию:

1. Make any necessary definitions.
2. Instantiate
3. For each instantiation unfold repeatedly. At each stage of unfolding execute 4, 5. 
4. Try to apply laws and where-abstraction
5. Fold repeatedly

Stages (1) and (2) require some invention from the user, (4) requires his discretion, but (3) and (5), unfolding and folding, are routine symbol manipulation.

Гарантия корректности преобразовании - тоже часть стратегии. Затем они описывают реальную работающую систему, которая умеет делать шаги 3, 4, 5 автоматически. Но шаги 1 и 2 остаются за пользователем.

И система работает. Кстати написание такой системы (по статье) было бы хорошим упражнением для дипломника или для аспиранта.

И большую часть статьи авторы показывают, как такая стратегия работает. - На примерах, когда шаги 1 и 2 делаются "волшебным" образом.  В рабочей системе БД (наверное, ее уже не найти и не запустить) шаги 1 и 2 должны быть сделаны пользователем ДО ТОГО, КАК СИСТЕМА НАЧНЕТ РАБОТАТЬ.

Смысл статьи в следующем: такая система и стратегия очень хорошо работает, при условии, что кто-то сделает правильно шаги 1 и 2. Поэтому содержательная работа в данном контексте - научиться механически делать шаги 1 и 2. Еще раз подчеркну, что в системе БД шаги 1 и 2 делаются пользователем ДО ТОГО, КАК СИСТЕМА НАЧНЕТ ПРЕОБРАЗОВАНИЯ. Почему это важно? Позволяет сделать набор "хороших примеров" и показать, что стратегия работает. 

К сожалению, часто, когда ссылаются на БД (и из-за этого возникает непонимание) или когда сравнивают некоторую систему с БД, описывают, будто бы шаги 1 и 2 должны быть выполнены во время работы системы, ПОСЕРЕДИНЕ ПРЕОБРАЗОВАНИЙ.

Нет, шаги 1 и 2 выполняются до начала преобразований человеком - так в оригинальной статье.

Интересно изучить расширение системы БД, - метасистему по отношению к систему БД, которая по какой-то тактике или стратегии выполняет шаги 1 и 2 в автоматическом режиме, - наверное такие есть.

Так вот, работа Берстала и Дарлингтона как-раз и открывает новые области исследования - "как делать шаги 1 и 2, КАК ПРИДУМЫВАТЬ ЭВРИКИ?", и поэтому является настоящей наукой.

PS. В некоторой степени, система БД тестирует работоспособность эврик (под своим собственным углом зрения, конечно).

Развитие производительных сил или Типизация при помощи суперкомпиляции

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

http://www.evil-wire.org/~jacobian/Productive.pdf

Некоторые системы программирования, а именно доказыватели теорем типа Coq или Agda имеют ограничения на входную программу. Ограничения, конечно, появляются не на пустом месте. Например, рассматриваются только такие множества программ, о которых доказыватель теорем может хоть-что нибудь (конструктивное) сказать.

Некоторые из ограничений - можно сформулировать (оценка сверху) как синтаксические ограничения. Плюс: ограничение быстро проверяется. Минус: ограничения могут быть слишком жесткими (ограничивающими).

Coq и Agda могут работать с коданными и корекурсией, только если соответствующие функции являются производительными (productive - отсюда и название статьи).
Является ли функция производительной - задача в общем виде неразрешимая.
Но есть достаточное синтаксическое "условие осмотрительности" (guardedness condition), гарантирующее производительность функций. К сожалению, это синтаксическое ограничение слишком жесткое, и многие "очевидно производительные функции" не распознаются как производительные.

Если же преобразовать с помощью эквивалентных преобразований плохую программу, для которой не выполняется условие осмотрительности, в хорошую, для которой это условие выполняется, то отсюда делается вывод о производительности исходной программы.

В статье показывается, как это может быть сделано с помощью суперкомпиляции на примерах на языке Agda. Детали - в статье.

Статья Мендель-Глизона иллюстрирует более общий подход, известный как трансформационный анализ. Вместо того, чтобы анализировать исходную программу на предмет выполнения некоторого свойства, можно подвергнуть программу некоторому преобразованию (сохраняющего данное свойство) и анализировать получившуюся, преобразованную программу на предмет выполнения искомого свойства. В данном случае, рассматриваемое свойство - производительность. И есть простой синтаксический проверяльщик (делающий оценку сверху). Исходную программу проверяльщик не пропускает. Суперкомпилируем программу - рассматриваемый суперкомпилятор сохраняет свойство производительности. Рассматриваем преобразованную программу. Проверяльщик ее пропускает. Значит, для исходная программа обладает рассматриваемым свойством.

В данном контексте цель суперкомпилятора - привести программу к некоторому синтаксическому виду.

PS. Политико-экономический бэкграунд