LiveMath IV

Дошли руки собрать очередную версию LiveMath.

LiveMath — это LiveDVD, содержащий большой набор свободного математического ПО. Предполагается для использования в основном в демонстрационных целях, но может также использоваться для постоянной работы.

Картинка для привлечения внимания:

(на картинке слева вверху FriCAS считает интегралы в специальных функциях, а справа R выводит графики по данным, включенным в поставку для примера).

В этот раз LiveMath основан на Ubuntu 12.10 (Quantal), плюс некоторое количество дополнительного софта. LiveMath IV содержит (среди прочего):

Системы компьютерной алгебры:

• Maxima 5.27 (http://maxima.sourceforge.net) - полнофункциональная система аналитических вычислений.
• Fricas 1.1.8 (http://fricas.sourceforge.net) и OpenAxiom 1.4.1 (http://open-axiom.org)  - обе актуальные версии мощной системы компьютерной алгебры Axiom.
• YaCas 1.3.2 (http://yacas.sourceforge.net) - еще одна система компьютерной алгебры.
• PARI/GP 2.5.1 (http://pari.math.u-bordeaux.fr/) - широко используемая компьютерно-алгебраическая система, разработанная для быстрых вычислений в теории чисел (факторизации, алгебраическая теория чисел, эллиптические кривые...).
• GAP 4r4p12 (http://www.gap-system.org/) - свободно распространяемый, открытый и расширяемый программный комплекс для применения в области вычислительной дискретной математики, в частности, теории групп.
• Mathomatic 15.8.2  (http://www.mathomatic.org/) - переносимая, универсальная программа, которая может решать, упрощать, группировать, дифференцировать, интегрировать и сравнивать алгебраические выражения.

Системы автоматизации доказательств:

• ACL2 4.3 (http://www.cs.utexas.edu/users/moore/acl2/) - язык программирования для моделирования компьютерных систем и средство, помогающее доказывать свойства этих моделей.
• Coq 8.3.pl4 (http://coq.inria.fr/) - система автоматизированного построения доказательств, с помощью которой, кроме всего прочего, была решена проблема четырех красок.
• Agda2 2.3.0 (http://wiki.portal.chalmers.se/agda/pmwiki.php) - язык программирования с зависимыми типами и система автоматизации доказательств.
•  Prover9/Mace4, Otter и пр.

Системы численных вычислений:

• SciLab 5.3.3  (http://www.scilab.org/) - пакет научных программ для численных вычислений, предоставляющий мощное открытое окружение для инженерных и научных расчетов.
• GNU Octave 3.6.2 (http://www.octave.org/) - язык высокого уровня, предназначенный для выполнения математических вычислений;
• FreeMat 4.0 (http://freemat.sourceforge.net/) - свободная среда для быстрой разработки, научного прототипирования и обработки данных, имеет интерфейс и синтаксис языка, подобные MatLab.
• Yorick 2.2.02 (http://yorick.sourceforge.net/) -специализированный С-подобный язык для создания симуляторов с упором на скорость вычислений.
•  Dynare 4.3.0 (http://www.dynare.org/).
  

Образовательные программы:

• Kig 4.9.2 (http://edu.kde.org/kig/), Geogebra 4.0.34.0 (http://geogebra.org), DrGeo 1.1.0  — интерактивная геометрия.
• KAlgebra 4.9.2
  
• KMPlot 4.9.2 — средство для построения графиков.

Обработка и визуализация данных:

• Gnuplot 4.6.0
• Mayavi2 4.1.0 (http://code.enthought.com/projects/mayavi/#Mayavi2) - открытый пакет научной 2D и 3D визуализации данных.
• OpenDX 4.4.4 (http://www.opendx.org/) - программное средство для анализа данных в графическом виде, визуализации научных данных.
• GGobi 2.1.10 (http://www.ggobi.org/) - среда визуализации многомерных данных;
• QtiPlot 0.9.8.8 - позиционируется как замена для Microcal Origin - программа для несложной статистической обработки данных, построения всяческих графиков.
• Grace 5.1.22 (http://plasma-gate.weizmann.ac.il/Grace/) - программа для подготовки двумерных графиков по численным данным.
• PAW 2.14.04 (http://cern.ch/paw/) - интерактивная программа анализа и графического представления результатов. Может применяться для анализа большого и очень большого объёма данных.
• ROOT 5.34.00 (http://cern.ch/root/) - наследник PAW, интерактивная система обработки и визуализации очень больших объёмов научных данных.
• GNU R 2.15.1 (http://r-project.org/) - мощный язык статистических вычислений, используемый профессиональными статистиками.
• GRETL 1.9.9 (http://gretl.sourceforge.net/) - система эконометрического анализа.
• Udav 0.7.1.2 (http://udav.sourceforge.net/) - инструмент визуализации данных.

Работа с графами

• Tulip 0.5.11
• GraphThing 1.3.2
• Cytoscape 2.8.3
• Rocs 1.7.2

Научные редакторы:

• TeXLive 2012.20120611 - полноценный дистрибутив TeX.
• TeXmacs 1.0.7.15  (http://texmacs.org) - текстовый редактор для набора математических и прочих научных текстов, также позволяет включать в документ сессии FriCAS, Maxima, Octave, SciLab и других систем компьютерной математики. Данная версия использует Qt, так что выглядит заметно приятнее старых, и работает несколько шустрее.
• Kile 2.1.2 (http://kile.sourceforge.net/) - интегрированная среда подготовки документов с помощью TeX.
• Texmaker 3.4 (http://www.xm1math.net/texmaker/) - интегрированная оболочка для LaTeX.
• TeXworks  0.5- лёгкая оболочка для LaTeX.
• LyX 2.0.3.

Также LiveMath IV содержит среду XFCE 4.10, LibreOffice 3.6.2. Для "больших" систем (ROOT, PAW, R, Octave) включена значительная часть имеющихся в репозиториях Ubuntu пакетов. Для многих изначально "консольных" систем включены GUI-обёртки, для некоторых по несколько, на выбор. К большинству программ есть документация. Возможна установка системы на жёсткий диск с помощью стандартного установщика Ubuntu.

Полный список установленных пакетов.

Загрузить образ ISO. (2 GB). Образ гибридный: можно записать на DVD или на флешку. Выложен образ на моём домашнем сервере, суперскоростей не обещаю.

Страница проекта.

К сожалению, у меня нет времени, чтобы тестировать все эти программы. То, что я протестировал - работает. Багрепорты принимаются в комментариях или на e-mail portnov at bk dot ru, но мгновенного исправления не обещаю.

LiveMath сделан с помощью Ubuntu Construction Kit (http://uck.sourceforge.net/), так что каждый, в принципе, может сделать себе нечто подобное. Вероятно, это окажется проще, чем качать моё изделие.

Haskell monads для физматовца. Краткое введение

Ну что, попробую пополнить ряды haskell newbies ;)

Я не уверен, что данная заметка сделает концепцию монад понятнее для профессиональных программистов на чём-нибудь типа Java. Но я надеюсь, что она поможет людям с некоторым математическим бэкграундом. Но даже им, думаю, эта заметка поможет в практическом программировании только в сочетании с другими monad tutorials.

АФАИК, во многих наших провинциальных вузах на физмат-специальностях теория категорий (вместе с современной теорией множеств) игнорируется полностью (т.е. о её существовании за 4-5-6 лет ни разу не упоминают даже, как это было у меня). Я не собираюсь излагать всю теорию — кому нужно, смотрите книжки или хотя бы википедию. Я изложу только то, что нужно для нашего применения.

Категории

Итак. Вводится понятие категории. Это некая очень абстрактная сущность (абстрактнее даже, чем множество). В некотором смысле, категория состоит из двух вещей: набора объектов и набора морфизмов. Относительно этих объектов и морфизмов выполняются какие-то там аксиомы. Из них следует, что категорию можно представлять в виде направленного графа, где вершины — это объекты категори, а дуги — это морфизмы категории. Существенно, что у морфизма, как у дуги графа, есть «начало» и «конец» (называемые домен и кодомен), и это объекты той же категории. Домен и кодомен морфизма (начало и конец дуги графа) могут совпадать. Такой морфизм называется эндоморфизмом.

Классический пример категории — Set. Объекты категории Set — это всевозможные множества, а морфизмы — это функции между этими множествами.

Более интересный для нас пример: категория Hask. Здесь объекты — это типы данных, возможные в языке Haskell, а морфизмы — функции языка Haskell.

Функторы

Следующее понятие: функтор. Функтор — это, условно говоря, отображение одной категории в другую. При этом функтор отображает объекты первой категории в объекты второй, а морфизмы первой — в морфизмы второй категории. К тому же накладываются определённые ограничения — аксиомы.

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

Возьмём нашу категорию Hask. Любой полиморфный тип данных языка Haskell с одним тИповым аргументом задаёт отображение, сопоставляющему каждому объекту категории Hask (т.е. типу языка Haskell) какой-то другой объект (другой тип). Например, конструктор типов [] сопоставляет любому типу a тип [a] (список элементов типа a). Конструктор типов Maybe сопоставляет каждому типу a другой тип — Maybe a (значение типа a или никакого значения). Таким образом, мы можем привести много примеров отображений класса объектов категории Hask в объекты той же категории. Пусть, например, у нас есть конструктор типов C (т.е. где-то написано data C a = …).

Если теперь такое отображение объектов (конструктор типов C с одним параметром) дополнить отображением морфизмов, то получим функтор, действующий из Hask в Hask (говорят «эндофунктор на категории Hask»). Напомню, морфизм категории Hask между объектами (типами) a и b — это любая функция типа a → b. Согласно аксиомам функторов, морфизм между объектами a и b должен отображаться в морфизм между объектами (C a) и (C b). Таким образом, отображение морфизмов должно быть функцией следующего вида:

    fmap :: (a -> b) -> (C a -> C b)

В модуле Prelude определён класс типов Functor:

    class Functor f where
     fmap :: (a -> b) -> (f a -> f b)

Итак, любой тип, являющийся экземпляром класса Functor, является эндофунктором на категории Hask (т.е., название класса Functor не вполне точное, его бы следовало назвать, скажем, HaskEndoFunctor). При этом сам конструктор типов задаёт отображение объектов (типов), а связанная с ним функция fmap задаёт отображение морфизмов (функций).

Моноиды

Моноид — это термин несколько из другой (хоть и смежной) области — из абстрактной алгебры. Моноид определяется следующими вещами:

• Множество M;

• Бинарная операция ⊕ на этом множестве; от неё требуется ассоциативность;

• Нейтральный элемент ε этой операции, входящий в множество (т.е. такой, что (∀a ∈ M) ε⊕a = a⊕ε = a).

Можно видеть, что моноид — это ослабление понятия группы. Благодаря этому, очень многие структуры являются моноидами. Ну, скажем, множество действительных чисел с операцией сложения. Или множество списков элементов какого-то одного типа с операцией (++).

Монады

Ну а теперь главное определение ;). Монада — это моноид в категории эндофункторов. Расшифровываю.

Пусть у нас есть какой-нибудь эндофунктор на категории Hask (т.е. тип f, являющийся экземпляром класса Functor). Дополним его структурой моноида. Для этого нам понадобится бинарная операция и её единичный элемент. Подходящая бинарная операция традиционно называется bind (и в haskell обозначается >>=). Подходящий единичный элемент традиционно называется return. В Haskell это выражается в следующее определение:

    class Monad m where
       (>>=) :: m a -> (a -> m b) -> m b  -- бинарная операция
       return :: a -> m a                 -- единичный элемент

В модуле Prelude объявлены экземпляры класса Monad для некоторых типов: [], Maybe, итп.

К чему это я всё

Из всего вышесказанного можно вывести очевидную вещь: монады — очень абстракная сущность. Настолько абстрактная, что чуть ли не всё на свете является монадой.

С другой стороны, это очень простая штука: некий аналог действия «композиция функций», только при композиции используется какая-то дополнительная информация.

Небольшая иллюстрация к предыдущему

Нашёл у Гейтинга [1] иллюстрацию к изоморфизму Карри-Ховарда. Что интересно: насколько я понял, эта иллюстрация была сформулирована до самого изоморфизма.

«Пусть A обозначает свойство натурального числа быть кратным 8, B — быть кратным 4, C — кратным 2. 8a мы можем записать как 4∙2a; благодаря этому математическому построению (P) мы видим, что свойство A влечёт свойство B, или A → B. Подобное построение (Q) показывает, что B → C. Употребляя сначала P, потом Q (суперпозиция P и Q), мы получаем 8a = 2∙(2∙2a), что доказывает A → C. Этот процесс остаётся пригодным, если вместо A, B, C мы подставим произвольные свойства. А именно, если построение P доказывает, что A → B, и построение Q доказывает, что B → C, то суперпозиция P и Q доказывает, что A → C».

Если считать «построения» функциями, то из этого рассуждения увидим, что существование операции суперпозиции двух функций (P и Q) доказывает транзитивность импликации:

(.) :: (b -> c) -> (a -> b) -> a -> c

[1] А. Гейтинг. Введение в интуиционизм. М.: Мир, 1965.

Вычислимость, λ-исчисление, теория типов, автоматизация доказательств

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

λ-исчисление

λ-исчисление было создано в начале 50-х гг. XX века для формализации понятий вычисления и вычислимости в математике. λ-исчисление оперирует символами и λ-выражениями. Символ — это одиночный абстрактный объект, иногда символы называют переменными. Символы обозначают маленькими латинскими буквами: x,y,z… λ-выражение определяется рекурсивно:

• Если x — это символ, то x — это λ-выражение;

• Если x — символ, а E — λ-выражение, то запись λx.E — тоже λ-выражение;

• Если E — λ-выражение, то (E) — λ-выражение;

• Если E1 и E2 — λ-выражения, то E1 E2 — тоже λ-выражение.

Выражения вида λx.E называют λ-функциями, или просто функциями. Если в таком выражении символ x встречается в выражении E, он называется связанным. Несвязанные символы, встречающиеся в λ-выражении, называются свободными.

Для любого λ-выражения E можно записать выражение λx.E, где x — свободный символ выражения E (и, таким образом, связать символ x). Эта операция называется λ-абстракцией.

Введём обозначение: записью E[x=T] будем обозначать выражение, полученное из E заменой всех вхождений символа x на T.

Над λ-выражениями можно производить следующие операции:

α-конверсия

E → E[x=y]; т.е. переменные можно переименовывать;

β-редукция

(λx.E1) E2 → E1[x=E2]; это подстановка;

η-редукция

λx.(E x) → E (избавление от лишней абстракции).

Видно, что α-конверсию можно применить к любому выражению, а редукции — только к выражениям определённого вида.

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

Теорема. Если у выражения есть нормальная форма, то она только одна. Любая последовательность редукций приведёт к этой нормальной форме.

Таким образом, выполняется единственность. Но существование выполняется не всегда: не у всех выражений есть нормальная форма.

Example 1: Пример.

ω = (λx.x x) (λx.x x)

ω = (λx.x x) (λy.y y) = (λy.y y) (λy.y y) = (λy.y y) (λz.z z) = (λz.z z) (λz.z z) = …

Последовательность редукций не изменяет это выражение.

Процесс применения редукций к выражению называется вычислением. Выражения, имеющие нормальную форму, называются вычислимыми.

Это вполне соответствует ситуации с программами для машины Тьюринга, среди которых есть как завершающиеся, так и не завершающиеся (работающие бесконечно).

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

Введём обозначение: λx.λy.λz.λ…E будем записывать как λx y z….E.

Натуральные числа.

За 1 примем выражение λx.x. Для каждого «числа» E следующим числом будем считать выражение λx.E. Таким образом, двойке будет соответствовать выражение λx y.y, тройке — λx y z.z, и т.д. Далее определения действий над числами вводятся как в аксиоматике Пеано. Такая запись чисел называется кодировкой Чёрча.

Выражения «если-то».

За логическую истину примем выражение λx y.x, за логическую ложь — λx y.y. Тогда выражение λc x y.c x y будет соответствовать конструкции «if-then-else». Действительно,

• if TRUE A B = (λc x y.c x y) (λx y.x) A B = (λx y.x) A B = A;

• if FALSE A B = (λc x y.c x y) (λx y.y) A B = (λx y.y) A B = B. Кроме того, оказывается, что можно ввести и обычные логические действия — and, or и т.д.

Пары (кортежи из двух элементов).

Пусть

pair = λf.λs.λb.b f s
fst = λp.p TRUE
snd = λp.p FALSE

Тогда выражение pair x y создаёт кортеж (x,y), функция fst возвращает первый элемент кортежа, snd — второй. Действительно,

pair x y = λb.b x y;
fst (pair x y) = (λp.p TRUE) (λb.b x y) = (λb.b x y) TRUE = TRUE x y = x;
snd (pair x y) = (λp.p FALSE) (λb.b x y) = (λb.b x y) FALSE = FALSE x y = y.

Кортежи из трёх и более элементов, очевидно, можно составлять из пар, например pair x (pair y z) — кортеж из трёх элементов.

Проблема останова

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

Теорема. Проблема останова в общем случае неразрешима.

Дальнейшее развитие теории вычислимости шло в направлении выяснения классов алгоритмов, для которых проблема останова разрешима. В случае с теорией машины Тьюринга такая задача не решена до сих пор. В случае с λ-исчислением решением стала теория типов.

Теория типов

Введём в λ-исчисление типизацию. Именно, кроме символов и выражений, теперь в теории будут фигурировать типы — тоже абстрактные объекты. Типы будем обозначать маленькими греческими буквами: τ, σ… Любое λ-выражение должно иметь тип, и при том только один. Это записывается как E : τ. Типы определяются также рекурсивно:

• Если τ — тип, то (τ) — тип;

• Если τ и σ — типы, то τ → σ — тип.

Типы без стрелок и других операций называются простыми типами. Все символы имеют простые типы.

Тип выражения определяется по следующим правилам:

• Если x : τ и E : σ, то (λx.E) : τ → σ;

• Если F : τ → σ и x : τ, то (F x) : σ.

При этом если в выражении F x окажется, что F : τ → σ и x : τ1, причём τ ≠ τ1, то говорят, что выражение неверно типизированное. В типизированном λ-исчислении рассматриваются только верно типизированные выражения.

Тип называется населённым, если существует хотя бы одно λ-выражение, имеющее такой тип.

Example 2: Пример.

Попробуем типизировать выражение λx.x x. Пусть x : τ. Тогда, чтобы к x, стоящему в выражении последним, можно было применить предыдущий x, этот предыдущий x должен иметь тип τ → σ, где σ — какой-то ещё тип. Но (x : τ) и (x : τ → σ) не может выполняться одновременно, т.к. у каждого символа может быть только один тип. Пришли к противоречию. Итак, рассматриваемое выражение неверно типизировано, а значит, неверно типизировано и упомянутое в предыдущем примере выражение ω. Таким образом, оказалось, что невычислимое выражение ω не входит в типизированное λ-исчисление.

Оказывается, что верна следующая

Теорема. Если λ-выражение верно типизировано, то оно вычислимо.

Таким образом, в рамках типизированного λ-исчисления проблема останова решается очень просто: все выразимые в этой системе алгоритмы завершаются.

Неудивительно, что при этом оказывается, что эта система не является тьюринг-полной. Т.е. существуют алгоритмы, которые можно представить в виде программы для машины Тьюринга, но нельзя записать в рамках типизированного λ-исчисления. Из этого можно сделать два замечания:

• Само по себе типизированное λ-исчисление не несёт большой практической ценности, т.к. не позволяет выразить многие алгоритмы;

• С другой стороны, т.к. множество типизированных выражений является подмножеством нетипизированных, появляется намёк на решение проблемы останова: чтобы выяснить, вычислимо ли данное выражение, нужно только проверить, является ли оно верно типизированным. Неудивительно, что как раз эта задача (проверить возможность типизации для произвольного выражения) оказывается неразрешимой.

Для возможности практического применения λ-исчисления разработаны системы типов, накладывающие меньше ограничений, чем вышеприведённая. Такие системы:

• достаточно выразительны, т.к. являются тьюринг-полными;

• вывод типов в них оказывается разрешимой задачей;

• но проблема останова, как и в случае нетипизированного λ-исчисления, неразрешима.

На таких "промежуточных" системах типов основаны имеющие практическое применения функциональные языки программирования.

Автоматизация доказательств

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

• Если τ и σ — типы, то τ*σ и τ+σ — тоже типы.

В λ-исчислении можно определить понятие пары (E1,E2) и понятие «одно из двух» E1|E2. При этом оказывается, что:

• Если E1 : τ, E2 : σ, то (E1,E2) : τ*σ,

• и E1 | E2 : τ+σ.

Оказывается, что между терминами теории типов и терминами логики высказываний существует естественное соответствие. Именно:

• Простой тип τ соответствует простому высказыванию;

• Сумма типов соответствует дизъюнкции;

• Произведение типов — коньюнкции;

• Стрелка — импликации.

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

Теорема (изоморфизм Карри-Ховарда). Теорема логики высказываний верна тогда и только тогда, когда соответствующий ей тип населён, т.е. любое λ-выражение, имеющее этот тип, можно рассматривать как доказательство теоремы.

Более сложные, чем вышеприведённая, системы типов позволяют записывать не только теоремы логики высказываний, но и теоремы логики более высоких порядков. При этом изоморфизм Карри-Ховарда остаётся в силе.

Задача «по данному типу найти выражение, имеющее такой тип, или доказать, что таких выражений нет» для многих классов типов решена. Таким образом, задача «по данной теореме найти её доказательство или опровержение» сводится к следующему:

• Записать данную теорему в виде типа в одной из систем типов;

• Найти выражение, населяющее этот тип;

• Записать это выражение на языке предметной области.

LiveMath III

Это продолжение к стародавнему посту: http://iportnov.blogspot.com/2007/09/livemath-livecd.html.

К сожалению, редко оказывается достаточно времени, чтобы собрать свежую версию LiveMath. Однако же вот, собрал. В этот раз LiveMath основан на Ubuntu 9.10 (Karmic) с добавлениями из Ubuntu Lucid и "Ubuntu Scientific Remix". LiveMath III содержит (среди прочего):

Системы компьютерной алгебры:
Maxima (http://maxima.sourceforge.net) - полнофункциональная система аналитических вычислений;
Fricas (http://fricas.sourceforge.net) - мощная система компьютерной алгебры;
YaCas (http://yacas.sourceforge.net) - еще одна система компьютерной алгебры;
PARI/GP (http://pari.math.u-bordeaux.fr/) - широко используемая компьютерно-алгебраическая система, разработанная для быстрых вычислений в теории чисел (факторизации, алгебраическая теория чисел, эллиптические кривые...);
GAP (http://www.gap-system.org/) - свободно распространяемый, открытый и расширяемый программный комплекс для применения в области вычислительной дискретной математики, в частности, теории групп;
Mathomatic (http://www.mathomatic.org/) - переносимая, универсальная программа, которая может решать, упрощать, группировать, дифференцировать, интегрировать и сравнивать алгебраические выражения;

Системы автоматизации доказательств:
ACL2 (http://www.cs.utexas.edu/users/moore/acl2/) - язык программирования для моделирования компьютерных систем и средство, помогающее доказывать свойства этих моделей;
Coq (http://coq.inria.fr/) - система автоматизированного построения доказательств, с помощью которой, кроме всего прочего, была решена проблема четырех красок;
Также Prover9/Mace4 и некоторые другие;

Системы численных вычислений:
SciLab (http://www.scilab.org/) - пакет научных программ для численных вычислений, предоставляющий мощное открытое окружение для инженерных и научных расчетов;
GNU Octave (http://www.octave.org/) - язык высокого уровня, предназначенный для выполнения математических вычислений;
FreeMat (http://freemat.sourceforge.net/) - свободная среда для быстрой разработки, научного прототипирования и обработки данных, имеет интерфейс и синтаксис языка, подобные MatLab;
Yorick (http://yorick.sourceforge.net/) - компактная программная среда, предназначенная для комплексного решения научно-инженерных вычислительных задач;

Образовательные программы:
Kig (http://edu.kde.org/kig/), Carmetal, DrGeo, GeoGebra - интерактивная геометрия;
KAlgebra;
Инструменты построения графиков - kmplot, gnuplot;

Обработка и визуализация данных:
Mayavi2 (http://code.enthought.com/projects/mayavi/#Mayavi2) - открытый пакет научной 2D и 3D визуализации данных;
OpenDX (http://www.opendx.org/) - программное средство для анализа данных в графическом виде, визуализации научных данных;
GGobi (http://www.ggobi.org/) - среда визуализации многомерных данных;
LabPlot (http://labplot.sourceforge.net/) - программа для анализа и визуализации различных данных;
QtiPlot - позиционируется как замена для Microcal Origin - программа для несложной статистической обработки данных, построения всяческих графиков;
Grace6 (http://plasma-gate.weizmann.ac.il/Grace/) - программа для подготовки двумерных графиков по численным данным;
PAW (http://cern.ch/paw/) - интерактивная программа анализа и графического представления результатов. Может применяться для анализа большого и очень большого объёма данных;
ROOT (http://cern.ch/root/) - наследник PAW, интерактивная система обработки и визуализации очень больших объёмов научных данных;
GNU R (http://r-project.org/) - мощный язык статистических вычислений, используемый профессиональными статистиками;
GRETL (http://gretl.sourceforge.net/) - система эконометрического анализа;

Научные редакторы:
TeXLive - полноценный дистрибутив TeX;
TeXmacs (http://texmacs.org) - текстовый редактор для набора математических и прочих научных текстов, также позволяет включать в документ сессии Axiom, Maxima, Octave, SciLab и других систем компьютерной математики;
Kile (http://kile.sourceforge.net/) - интегрированная среда подготовки документов с помощью TeX;
Texmaker (http://www.xm1math.net/texmaker/) - интегрированная оболочка для LaTeX;

Также LiveMath III содержит среду Gnome 2.28, OpenOffice.org 3.1, Gnumeric. Для "больших" систем (ROOT, PAW, R, Octave) включена значительная часть имеющихся в репозиториях Ubuntu пакетов. Для многих изначально "консольных" систем включены GUI-обёртки, для некоторых по несколько, на выбор. К большинству программ есть документация. Возможна установка системы на жёсткий диск с помощью стандартного установщика Ubuntu.

UPD. Полный список установленных пакетов: http://iportnov.ru/files/LiveMath.packages.txt

К сожалению, у меня нет времени, чтобы тестировать все эти программы. То, что я протестировал - работает. Багрепорты принимаются в комментариях или на e-mail portnov at bk dot ru, но мгновенного исправления не обещаю.

LiveMath сделан с помощью Ubuntu Construction Kit (http://uck.sourceforge.net/), так что каждый, в принципе, может сделать себе нечто подобное. Вероятно, это окажется проще, чем качать моё изделие.

Взять можно здесь: http://portnov.homelinux.net/LiveMath%20III.iso (размер образа - 2Gb), может быть удобнее окажется торрент: http://iportnov.ru/files/LiveMath%20III.iso.torrent (честно говоря, не знаю, заработает ли). У меня сейчас нет хостинга, на котором я бы мог размещать большие ISO-образы. Так что учтите, что portnov.homelinux.net - это мой домашний сервер, обычно бывает включён примерно с 8:00 до 22:00 MSK, суперскоростей не обещаю. Если кому-то позарез нужно скачать в другое время - пишите, так уж и быть, оставлю включённым на ночь :)

Обзор свободного математического ПО

Это конспект моего доклада на семинаре, организованном нашей LUG совместно с университетом. Соответственно, я не мог охватить всё - у меня на доклад было где-то 15 минут.

Вступление

Известные пакеты - это гиганты всё-в-одном

Когда мы говорим о математическом ПО, на ум приходят такие гиганты, как Maple, Mathematica, MatLAB… У них есть одно общее свойство: они пытаются охватить всё. Конечно, Mathematica известна прежде всего как система для символьных вычислений, а Matlab - для численных, но одновременно в Mathematica есть мощные алгоритмы для вычислений с плавающей точкой, а в Matlab - пакет для символьных вычислений. Причём эти второстепенные функции в программах по сравнению с программами, для этого предназначенными, выглядят убого и смешно. А небезызвестный MathCAD пытается включить в себя всё, при этом всё реализовано так себе. Причина проста: нельзя объять необъятное.

Свободные программы - делают одно дело хорошо

В противоположность этому, большинство свободных программ следует философии UNIX, гласящей: программа должна делать одно дело, но делать его хорошо. Свободного математического ПО очень много, при этом бóльшая часть их предназначена для какой-нибудь одной задачи. Например, есть программы, которые только и умеют, что строить сетку для метода конечных разностей. Или программа, которая предназначена для вычисления цифр числа Пи. Или программа, которая умеет только строить графики, но зато очень хорошо.

Однако, есть и программы, в той или иной степени являющиеся аналогами известных пакетов. Я расскажу о трёх.

Символьные вычисления: Maxima

История проекта

Начну я с истории этого проекта.

Сначала я напомню, что компьютеры - это, вообще-то, Электронные Вычислительные Машины, они создавались для вычислений над числами. Однако уже в конце 50-х появилась идея, что можно заставить компьютер работать не только с числами, но и с алгебраическими выражениями. В начале 60-х начали появляться первые системы компьютерной алгебры. И, конечно, такая система нужна была одному мирному американскому ведомству (департаменту энергетики, это практически подразделение Пентагона). Был объявлен тендер, и его выиграл проект под названием Macsyma (пишется через CS). В течение многих лет DOE Macsyma развивалась как коммерческий проект, финансируемый правительством. В 1982-м году Уильям Шелтер создал форк Macsyma, называемый Maxima. В начале 90-х распался СССР, кончилась холодная война, и косвенным следствием этого стало практически полное прекращение финансирования DOE Macsyma. К концу 90-х проект практически загнулся. Исходники Macsyma по кусочкам распродали, и они оказались в Maple и Mathematica. В 1998-м Уильям Шелтер добился от DOE разрешения на публикацию исходных текстов Maxima под лицензией GPL. Maxima стала свободной программой. В 2001-м Шелтер скончался, но к этому моменту над Maxima работало уже довольно много людей, и они подхватили проект.

Интерфейс: командная строка или wxMaxima

Maxima имеет традиционный для UNIX интерфейс командной строки, однако также умеет слушать сетевой порт, работая как сервер. Этот факт используют различные оболочки (фронтенды), предоставляющие графический интерфейс. Наиболее распространены TeXmacs и wxMaxima. TeXmacs - это научный текстовый редактор, в котором можно в документ вставить сессию Maxima. wxMaxima выглядит примерно так:

Последняя версия, 0.8.0, стала больше походить на Mathematica и Maple: раньше командная строка для ввода была отдельно, внизу.

Lisp-подобный язык

Язык Maxima берёт основные идеи из Lisp, так как Maxima написана на Lisp-e. При этом он похож одновременно на языки Mathematica и Maple, так как эти программы позаимствовали многие идеи и часть кода из Macsyma. Чтобы избежать долгого и нудного перечисления возможностей, я приведу пример решения типичных задач с первого курса.

Пример

Пусть дана функция

maxima>> f(x) := x*tanh(x) + x + 1/x + 2;

Проверим, не является ли она чётной или нечётной:

maxima>> f(-x);

Как видим, функция не является ни чётной, ни нечётной. Найдём пределы функции на плюс-минус бесконечности:

maxima>> limit(f(x),x,-inf);

maxima>> limit(f(x),x,inf);

Итак, на плюс бесконечности функция уходит в бесконечность. Нет ли у неё наклонной асимптоты?

maxima>> limit(f(x)/x, x,inf);

Наклонная асимптота есть - y=kx+b, причём k=2. Найдём b:

maxima>> limit(f(x)-2*x, x,inf);

Наконец, построим график:

maxima>> plot2d(f(x), [x,-5,5], [y,-10,10]);

Найдём производную нашей функции:

maxima>> diff(f(x),x);

И заодно - неопределённый интеграл:

maxima>> integrate(f(x), x);

Интеграл до конца "не взялся". Можно показать, что этот интеграл в элементарных функциях и не берётся. Однако Maxima умеет брать некоторые из таких интегралов, используя специальные функции:

maxima>> part: risch(x/(exp(2*x)+1), x);

(здесь я присваиваю результат интегрирования переменной part). Таким образом, интеграл f(x) будет равен

maxima>> ir: -2*part + log(x) + x^2 + 2*x;

Что-то ужасное. Раскроем скобки:

maxima>> expand(ir);

Дифференциальные уравнения

Или вот пример более сложных вычислений. Пусть надо решить дифференциальное уравнение:

maxima>> eq: 'diff(y,x) + x*y = 1-x^2;

Знак апострофа здесь используется, чтобы указать, что не надо сейчас вычислять производную, а сохранить обозначение.

maxima>> solution: ode2(eq,y,x);

Вот и решение. erf здесь - это специальная функция, известная как функция ошибки Лапласа. После раскрытия скобок получим вот что:

maxima>> expand(solution);

По Maxima есть некоторое количество русскоязычных руководств, которые можно найти в интернете. На мой взгляд, самое удачное введение с обзором возможностей содержится в цикле статей Тихона Тарнавского в журнале LinuxFormat. Сейчас эти статьи выложены в открытый доступ, в том числе на русском сайте Maxima. Документация по продвинутым возможностям maxima существует, к сожалению, только на английском языке. Официальная документация составляет 712 страниц.

Численные вычисления: Scilab

Scilab совместим с MatLAB-ом

Наиболее известный пакет для численных расчётов - это MatLAB. Scilab создавался как конкурент matlab-а, более скромный по ценовой политике. Однако коммерчески проект себя не оправдал, и исходные коды были открыты под лицензией, похожей на GNU GPL. Язык scilab сделан по возможности совместимым с матлабом, так что большинство ваших наработок из matlab заработают в scilab. Только вот, как известно, основная мощь matlab-a сосредоточена в его тулбоксах - отдельно поставляемых модулях. Модули для scilab-а тоже есть, однако их сильно меньше.

Octave - это GPL-аналог Matlab

Позже появился проект GNU Octave, нацеленный на создание аналога matlab-a, распространяемого по GNU GPL без всяких заморочек. Язык тоже практически совместим с матлабом, но здесь нет аналога Simulink - средства моделирования и симулирования динамических систем.

Зато Octave имеет чисто консольный интерфейс (конечно, графические фронтенды тоже есть, самый развитый - QtOctave), что позволяет использовать его в скриптах, для автоматизации расчётов, и упрощает встраивание в сложные программные комплексы. Для Octave написаны десятки пакетов расширений.

По Scilab есть статьи на русском языке, кроме того, не так давно в издательстве AltLinux вышла книга `Scilab: Решение инженерных и математических задач'. Книгу можно приобрести в интернет-магазине, кроме того, её электронная версия свободно доступна на сайте AltLinux.

Обработка данных: GNU R

Обзор

Формально, средства обработки данных относятся к программам для численных расчётов, ибо всё что они делают - это вычисления над числами. Однако, как известно, специализированный инструмент всегда лучше универсального. Под словами обработка данных скрывается довольно много различных видов деятельности: статистический анализ, статистическое моделирование, выборка только нужных данных, преобразование данных, построение различных графиков и гистограмм.

Программы для обработки данных можно разделить по типичному размеру выборки, для которого они предназначены. Для небольших выборок подойдёт, например, Statistica. Для средних по размеру выборок хорошо подходит GNU R (она хранит все данные в оперативной памяти, так что на типичном PC получим ограничение в 1-2-4 гигабайта). Для больших и очень больших объёмов данных (от сотен гигабайт до сотен терабайт) предназначены разработанные в CERN свободные системы PAW и ROOT.

GNU R - это интерпретируемый язык программироваммирования, предназначенный для статистического анализа и моделирования. R - это свободная реализация давно существующего языка S. Язык этот весьма эклектичен, он местами похож на C, местами - на Python, местами - на Haskell. Для GNU R существует почти полторы тысячи пакетов расширений (написанных на самом R, на C или Fortran), собранных в репозитории CRAN (Comprehensive R Archive Network).

Типы данных - числа, строки, факторы, векторы, списки и таблицы данных

Основные типы данных в языке - это числа, строки, факторы, векторы, списки и таблицы данных (data frames). Фактор - это данные, которые могут принимать одно из нескольких значений (пол; сорт дерева; логический тип и др). Векторы являются аналогами массивов - это набор из нескольких значений одного типа, размер вектора меняться не может. Тут же надо заметить, что в R нету скаляров; например, число - это, с точки зрения R, вектор из одного элемента. Списки - это обобщение векторов, они могут содержать объекты разных типов, и длина их может меняться. Кроме того, отдельным элементам списка можно присвоить имена, и обращаться к элементам не по номерам, а по именам. Пример:

R>> lst <- list(1,2,3)

(присваивание в R обозначается обычно знаком ←, хотя можно использовать и более привычное =; кроме того, есть форма value → variable). Для обращения к элементам списка по номеру используются двойные квадратные скобки:

R>> lst[[2]]

[1] 2

Назначим имена элементам списка:

R>> names(lst) <- c('first','second','third')

(функция c создаёт векторы). Теперь к элементам списка можно обращаться по именам:

R>> lst$third

[1] 3

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

Пример

Скажем, в файле airquality.dat находятся данные замеров качества воздуха:

"Ozone" "Solar.R" "Wind" "Temp" "Month" "Day"
"1" 41 190 7.4 67 5 1
"2" 36 118 8 72 5 2
"3" 12 149 12.6 74 5 3
"4" 18 313 11.5 62 5 4
"5" NA NA 14.3 56 5 5
"6" 28 NA 14.9 66 5 6
"7" 23 299 8.6 65 5 7
"8" 19 99 13.8 59 5 8
"9" 8 19 20.1 61 5 9
"10" NA 194 8.6 69 5 10
.......................

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

R>> air <- read.table('airquality.dat', sep=' ', header=TRUE)

Здесь мы указываем имя файла, разделитель (пробел), а также указываем, что в первой строке записаны имена полей. К полям таблицы мы можем теперь обращаться как к элементам списка - например, air$Ozone. Посмотрим, что R знает о структуре наших данных:

R>> str(air)

'data.frame':       153 obs. of  6 variables:
$ Ozone  : int  41 36 12 18 NA 28 23 19 8 NA ...
$ Solar.R: int  190 118 149 313 NA NA 299 99 19 194 ...
$ Wind   : num  7.4 8 12.6 11.5 14.3 14.9 8.6 13.8 20.1 8.6 ...
$ Temp   : int  67 72 74 62 56 66 65 59 61 69 ...
$ Month  : int  5 5 5 5 5 5 5 5 5 5 ...
$ Day    : int  1 2 3 4 5 6 7 8 9 10 ...

Теперь мы можем, например, посмотреть описательную статистику по всем полям таблицы:

R>> summary(air)

    Ozone           Solar.R           Wind             Temp
Min.   :  1.00   Min.   :  7.0   Min.   : 1.700   Min.   :56.00
1st Qu.: 18.00   1st Qu.:115.8   1st Qu.: 7.400   1st Qu.:72.00
Median : 31.50   Median :205.0   Median : 9.700   Median :79.00
Mean   : 42.13   Mean   :185.9   Mean   : 9.958   Mean   :77.88
3rd Qu.: 63.25   3rd Qu.:258.8   3rd Qu.:11.500   3rd Qu.:85.00
Max.   :168.00   Max.   :334.0   Max.   :20.700   Max.   :97.00
NA's   : 37.00   NA's   :  7.0
Month            Day
Min.   :5.000   Min.   : 1.00
1st Qu.:6.000   1st Qu.: 8.00
Median :7.000   Median :16.00
Mean   :6.993   Mean   :15.80
3rd Qu.:8.000   3rd Qu.:23.00
Max.   :9.000   Max.   :31.00

Для каждого поля показаны минимум, максимум, медиана и две квартили, среднее значение и количество пропущенных данных. Осталось только среднеквадратичное отклонение:

R>> sd(air)

Ozone  Solar.R     Wind     Temp    Month      Day
NA       NA 3.523001 9.465270 1.416522 8.864520

Как видим, R считает среднеквадратичное отклонение для полей Ozone и Solar.R неизвестным - из-за того, что в этих полях есть пропущенные данные. Мы можем явно указать, что на пропущенные данные не надо обращать внимание:

R>> sd(air, na.rm=TRUE)

    Ozone   Solar.R      Wind      Temp     Month       Day
32.987885 90.058422  3.523001  9.465270  1.416522  8.864520

Построим простейшую линейную модель - исследуем зависимость концентрации озона от температуры:

R>> ot <- lm(Ozone ~ Temp, data=air)

R>> ot

Call:
lm(formula = Ozone ~ Temp, data = air)

Coefficients:
(Intercept)         Temp
-146.995        2.429

То есть, если приближать зависимость линейной Ozone = k*Temp + b, то k=2.429, а b=-146.995, при увеличении температуры концентрация озона в среднем растёт.

По GNU R есть довольно много материалов на русском, в частности, методические рекомендации по лабораторным работам для вузов. Также есть хорошее введение в R, содержащееся в цикле статей А.Б. Шипунова и Е.М.Балдина в журнале LinuxFormat, сейчас эти статьи есть в открытом доступе. Продвинутая документация, к сожалению, только на английском, зато её много, включая толстые книги. Официальное руководство к R занимает 2541 страницу.