lysa/ru/chapters/1-introduction.ltx

\ch{Вступление}

Прежде чем заскучать от кучи хлама до которого вам нет дела, давайте немного
поговорим о математике?

Есть всего три основных понятия, с которыми вы должны быть знакомы,
чтобы делать что-либо интересное в математике. Это {\it множества}, {\it функции} и {\it доказательства}.
К несчастью, чтобы понимать одно из них, вы должны быть знакомы с
оставшимися.\footnote{Потом вы поймете, что когда математики используют такие понятия как
  {\it множество}, {\it функция}, {\it доказательство}, {\it группа}, {\it непрерывный} или
  {\it замкнутый}, они обычно имеют ввиду что-то, похожее по смыслу на общепринятое
  значение понятия, но с дополнениями. Это обычное дело для науки (например, \xti{теория},
  \xti{гипотеза}, \xti{эксперимент}).}
% ENG
% There are basically three notions with which you need to be familiar in order to
% do anything interesting in math. Those three things are {\it sets}, {\it
%   functions}, and {\it proofs}. Unfortunately, to be familiar with one, you have
% to be familiar with the other two.\footnote{You'll learn as we go along, when
%   math people use a common term like {\it set}, {\it function}, {\it proof},
%   {\it group}, {\it continuous} or {\it closed}, they usually mean something
%   similar in concept to the colloquial term, but there are some strings
%   attached. This is usually the case in the sciences too (e.g. \xti{theory},
%   \xti{hypothesis}, \xti{experiment}).}

Итак, что означает каждое из этих понятий?
% ENG
% So, what are each of those things?

\begin{itemize}
\item \xti{Множество} – это неупорядоченая коллекция чего-либо. Кроме того без повторений.
  Например, $\mset{2, 5}$ – то же самое, что $\mset{5, 2}$ (потому что порядок не важен).
  $\mset{2, 5, 5}$ будет тем же самым множеством потому, что там нет понятия многочисленности.
% ENG
% \item A \xti{set} is an unordered collection of things. There is also no
%   repetition. For instance, $\mset{2, 5}$ is the same as $\mset{5, 2}$ (because
%   order doesn't matter). $\mset{2, 5, 5}$ would be the same set, because there's
%   no notion of multiplicity.

\item \xti{Функция} – это математическая конструкция (что очевидно, раз мы говорим об этом).
  По сути, она принимает какие-то данные на вход, производит действия над ними и возвращает результат.
  Если вы даете функции одни и те же данные на вход несколько раз, каждый раз
  вы должны получать один и тот же результат на выходе. Это называется "чистотой" функции.
  Если функция не чистая, значит это не функция. Это что-то другое.
% ENG
% \item A \xti{function} is a mathematical construct (well, obviously, else I
%   wouldn't be talking about it). Basically, it takes some input, does something
%   to it, and spits out some output. If you give the function the same input a
%   bunch of times, you should get the same result each time. This concept is
%   called ``referential transparency.'' If the function is not referentially
%   transparent, then it's not a function. It's something else.

\item \xti{Доказательство} – это когда вы берете кучу простых фактов,
  называемых \xti{аксиомами}, и связываете их вместе, чтобы вывести \xti{теоремы}.
  Что-то вроде пазла, который вы собираете из маленьких кусочков, чтобы сформировать картину.
%ENG
% \item A \xti{proof} is basically where you take a bunch of simple facts, called
%   \xti{axioms}, and chain them together to make \xti{theorem}s. It's sort of like
%   sticking puzzle pieces together to form a picture.

  Кусочки пазла (в данном случае аксиомы) не особо интересны сами по себе. Но картинка,
  которая из них получается (в данном случае теорема), может быть очень крутой и информативной.
  Можно сказать, что доказательство --- это набор инструкций, разъясняющих, как собрать кусочки вместе.
% ENG
%   The puzzle pieces (in this case, the axioms) aren't usually very interesting
%   on their own. However, the picture they form (in this case, the theorem) can
%   be really cool and enlightening. The proof would be analogous to an explicit
%   set of instructions explaining how to put the pieces together.
\end{itemize}

Как только вы познакомитесь с каждым из этих понятий, мы сможем делать все, что
заблагорассудится. В этой книге мы докажем следующее:
% ENG
% Once you are familiar with each of those concepts, we can do all sorts of cool
% stuff.  Throughout the book, we will prove all of the following:

\begin{itemize}
\item Если вы постучите пальцем по мосту с определенной частотой, мост рухнет.
  (Резонанс)
% ENG
% \item If you tap your finger against a bridge at exactly the right frequency,
%   the bridge will collapse. (Resonance)
\item Формула для расчета процентной ставки по ипотеке – лишь частная форма
  коэффициентов углов треугольника. (Формула Эйлера)
% ENG
% \item The formula used to calculate the interest rate on your mortgage is
%   actually just a fancy form of the ratios of angles in a triangle. (Euler's
%   formula)
\item Логикой не всегда можно доказать то, что как мы знаем заведомо является правдой.
  (Теорема Гёделя о неполноте)
% ENG
% \item Logic can't be used to prove everything we know to be true. (Gödel's
%   incompleteness theorem)
\end{itemize}

\s{Вступление (теперь взаправду)}
% \s{Introduction (for real this time)}

Это книга по математике. Хм, мда. Зачем я написал ее?
% This is a math book. Well, duh. Why did I write it?

Большая часть книг по математике (и другим наукам) сегодня акцентируется на
академическом тоне, вместо заботы о том, что читатель понимает материал и --- что более важно
--- наслаждается чтением книги.
% ENG
% Most math (and science) books nowadays seem to value keeping an academic tone
% over ensuring that the reader understands the material, and --- more importantly
% --- enjoys reading the book.

Я решил поступить наоборот. Я хочу создать книгу, которую весело читать и легко понимать,
вместо того, чтобы показать как я крут.
% ENG
% I take the opposite approach. I want to create a book that is fun to read and
% easy to understand, while eschewing the practice of making myself look good.

Вдохновением для этой книги послужила книга Миран Липовача
\href{http://learnyouahaskell.com/}{\it Learn You a Haskell for Great Good!}
Haskell – это язык программирования, и LYAH – отличная книга для изучения этого языка.
Печатное издание LYAH можно заказать здесь: \cite{lyah}.
% ENG
% The inspiration for this book is \href{http://learnyouahaskell.com/}{{\it Learn
%     You a Haskell for Great Good!}, by Miran Lipovača}. Haskell is a programming
% language, and LYAH is a great book for learning Haskell. If you are interested
% in a print copy of LYAH, see \cite{lyah}.

\s{Сообщество}
%\s{The community}

Опуская тот факт, что я использую ``Я'' в первой части книги, LYSA является
проектом сообщества и довольно много людей участвуют в написании этой книги.
% ENG
% Despite the fact that I used ``I'' in the first part of the book, LYSA is
% actually a community project, and many people participate in the writing of this
% book.

Если вы хотите пообщаться с нами или другими математиками, приходите к нам в чат
{\tt \#lysa} на Freenode. Если вы не знаете, что такое IRC, или вы не знаете
как настроить клиент – вы можете зайти в чат через
\link{http://webchat.freenode.net/?channels=lysa}{вебчат Freenode}.
% ENG
% If you want to talk to us, or to other math people, come see us in {\tt \#lysa}
% on Freenode. If you don't know what IRC is, or you don't have a client set up,
% you can connect through
% \link{http://webchat.freenode.net/?channels=lysa}{Freenode's webchat}.

Если у вас возникли любые вопросы по LYSA (или математике), пожалуйста задавайте их в чате
({\tt \#lysa} на FreeNode, если вы забыли что-то из математики).
% If you have any questions about LYSA (or math), feel free to ask in the IRC
% channel ({\tt \#lysa} on FreeNode in case you forgot).

Если вы хотите исправить что-либо, или заметили какую-либо проблему, или хотите
добавить какой-то материал – что угодно, связаное с содержимым книги – вы можете зайти
на \link{https://github.com/gazay/lysa}{нашу русскоязычную GitHub страницу} или на
\link{https://gitlab.com/lysa/lysa}{оригинальную страницу книги}. У нас также есть
\link{https://lysa.reddit.com/}{сообщество на Reddit}.
% ENG
% If you want to submit a correction, or have some issue, or want to add some
% content, really anything having to do with the content of the book, you can
% visit \link{https://gitlab.com/lysa/lysa}{our GitLab page}. We also have a
% \link{https://lysa.reddit.com/}{community on Reddit}.

\s{Idris}\label{intro-idris}

В этой книге мы изучим кучу сложных вещей.\footnote{Это не совсем правда.
  Не математика сложная, а ты не вник.} Иногда очень полезно напрограммировать
решение проблемы. Каждый программист скажет вам, что программирование учит
думать иначе.
% ENG
% In this book, we cover a lot of hard stuff.\footnote{This isn't actually
%   true. Math isn't hard, stupid!} Sometimes, it's useful to program your way
% through a problem. Every programmer will tell you that programming teaches a
% manner of thinking.

Многие программисты процитируют известные слова Стива Джобса\footnote{Для вас, молодняка, Стив Джобс –
  основатель Apple. Он умер.}, относящиеся к программированию в его работе,
% ENG
% Many programmers will cite Steve Jobs\footnote{For you youngsters, Steve Jobs is
%   the former CEO of Apple. He's dead now.} famous quote, regarding the use of
% programming in his job,

\begin{iquote}
  [sic] \ldots что намного важнее, нет ничего общего с использованием (программ, что мы пишем)
  на практике. С другой стороны, это как отражение мыслительного процесса; по-настоящему учиться думать.
  Я думаю, каждый в этой стране должен знать как программировать на компьютере --- должен
  изучать компьютерный язык --- потому что это учит нас думать.
  % ENG
  % [sic] \ldots much more importantly, it had nothing to do with using [the
  % programs we wrote] for anything practical. It had to do with using them to be
  % a mirror of your thought process; to actually learn how to think. I think
  % everybody in this country should learn how to program a computer --- should
  % learn a computer language --- because it teaches you how to think.
\end{iquote}

\nocite{jobs-programming}

Первые пара предложений - на самом деле, отличное описание математики (и программирования).
Обе сферы невероятно полезны и имеют бесконечный потенциал практического применения.
Но это не самое важное. Самая полезная вещь – это побочный эффект. Учиться думать и
иметь строгий язык для выражения своих мыслей. Кроме того, строгость языка
помогает выдумывать все более крутые вещи.
Вот о чем математика.
% ENG
% That first sentence or two is actually a pretty good description of mathematics
% (and programming). Both are incredibly useful, and have endless practical
% applications. That's not the point, though. The whole usefulness thing is a side
% gig. It's about learning how to think, and having a rigorous language through
% which to express your thoughts. Furthermore, the rigor of the language helps you
% build upon your current thoughts to find out even cooler things. That's what
% math is about.

Программирование и математика идут рука об руку. Программисты и математики подтвердят это:
я точно могу. Поэтому вы встретите в этой книге упражнения на языке Idris. Idris – это
очень интересный язык программирования по многим причинам. Главная из которых заключается в том,
что он позволяет доказывать вещи математически. Большинство языков программирования не
могут этого. Idris может, поэтому он такой замечательный.\footnote{Кроме Idris
  доказывать вещи математически позволяют два других языка: Coq и Agda. Но, так как я наиболее
  знаком с Idris, и он, по-моему, наиболее пригоден лдя этого - будет Idris.
  Смиритесь.}
% ENG
% Programming and math go hand-in-hand. Programmers and mathematicians will attest
% to this; I certainly can. For that reason, throughout this book, there will be
% coding exercises in the programming language Idris. Idris is an interesting
% programming language for many reasons. The chief of which is that it can be used
% to prove things mathematically. Most programming languages can't do this. Idris
% can, which is why it is special.\footnote{There are other programming languages
%   that can prove things, namely Coq and Agda. However, I'm most familiar with
%   Idris, and Idris is probably the most useful, so I'm using Idris. Deal with
%   it.}


\ss{Установка Idris}
% \ss{Installing Idris}

Это довольно трудно описать, потому что процесс очень сильно зависит от
операционной системы. Я размещу инструкции для операционных систем, которые использую сам.
Если вы не найдете своей операционной системы ниже, пожалуйста, напишите об этом в
\link{https://github.com/gazay/lysa/issues/new}{issue tracker}. Еще лучше, если вы сможете
написать инструкции самостоятельно и попросить меня добавить это в саму книгу.
% ENG
% This is something that is actually rather difficult to summarize, because it
% varies from operating system to operating system. I will put down the
% instructions for the operating systems I use. If you come upon this and don't
% see your operating system, please report this on
% \link{https://gitlab.com/lysa/lysa/issues/new}{the issue tracker}. Better yet,
% you could add the instructions yourself, and ask me to merge your changes.

\sss{Mac}

Если у вас установлен пакетный менеджер \link{http://brew.sh/}{Homebrew}, то,
по идее, все должно быть очень просто:

\begin{shellsession}
# brew install idris
\end{shellsession}

После этого вы сможете запустить Idris командой \terminal{idris}.

Если же у вас возникли какие-либо проблемы с установкой напрямую,
попробуйте выполнить все шаги из
\link{https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew}{официальной вики по установке}
Idris на Mac.

% \sss{Linux}

% \pg{Gentoo}

Вам потребуется платформа Haskell и библиотека GMP. На момент 5 января 2015 платформа доступна
только в \code{\tilde x86} и \code{\tilde amd64} профилях. Если вы используете стабильный профиль,
добавьте в \filepath{/etc/portage/package.keywords}
% ENG
% You will need the Haskell platform, along with the GNU Multiple Precision (GMP)
% library. As of 5 January 2015, the Haskell platform is only available on
% \code{\tilde ARCH}, where \code{ARCH} is your processor architecture
% (e.g. \code{amd64}, \code{x86}). If you use \code{ARCH}, you can enable these by
% adding the following to \filepath{/etc/portage/package.keywords}:\footnote{If
%   you already use \code{\tilde ARCH}, you can ignore this}

\begin{plainfile}
dev-lang/ghc
dev-haskell/cabal-install
\end{plainfile}

Независимо от профиля надо задать флаг в \filepath{/etc/portage/package.use}:
% ENG
% Regardless of your \code{ACCEPT\_KEYWORDS} variable, you should add the
% following to \filepath{/etc/portage/package.use}:

\begin{plainfile}
dev-lang/ghc binary
\end{plainfile}

Иначе GHC (компилятор Хаскеля) будет компилироваться. А это долго. Очень.
% ENG
% Otherwise, you have to compile GHC (the Haskell compiler) from scratch, and that
% takes forever.

Затем выполнить с правами суперпользователя:
% ENG
% Once you have that all out of the way, you'll want to run the following command as root:

\begin{shellsession}
# emerge -jav dev-lang/ghc dev-haskell/cabal-install
\end{shellsession}

\xtb{Внимание}: флаг \terminal{-j} сделает установку многопоточной, ну вы знаете :)
% ENG
% \xtb{Warning}: \terminal{-j} will make the installation a lot faster, but is
% more resource-intensive. If your power usage is precious, omit it (i.e. use
% \terminal{-av} instead).

После установки выполните от своего пользователя:
% ENG
% Once GHC and cabal-install are installed, you'll want to run the following as a
% normal user:

\begin{shellsession}
% cabal update
% cabal install alex happy haddock hscolour
% cabal install idris
\end{shellsession}

Теперь в терминале можно запустить \terminal{idris}.
% ENG
% You can then get at the Idris shell by running \terminal{idris}.

\s{Лицензия}
% \s{Licensing}

Эта книга доступна всем без ограничений. Вы можете скопировать эту книгу и дать своему
другу. Вы можете даже напечатать эту книгу и продать ее своим друзьям,\footnote{Правда,
есть определенные ограничения, смотри \cref{gfdl}.}
% ENG
% This book is free, in the sense of freedom. You can copy this book and give it
% ENG
% to your friend. You can even print it out and sell it to your
% ENG
% friends.\footnote{There are some restrictions though, see \cref{gfdl}.}

Если вы, например, школный учитель и хотите использовать ее для своих занятий,
вы можете свободно изменять содержимое по своему усмотрению и раздавать копии своим
студентам.
% ENG
% If, for instance, you are a schoolteacher and want to use this for your class,
% you are free to edit it to your liking and give the modified copy to your
% students.

LYSA лецензирована по GNU Free Documentation License. \Cref{gfdl} содержит текст лицензии.
Пожалуйста, прочтите лицензию; вообще, она довольно проста и понятна.
% ENG
% LYSA is licensed under the GNU Free Documentation License. \Cref{gfdl} contains
% the license. Please read the license; it's actually pretty comprehensible.

Исходный код этой книги может быть скачан \link{https://github.com/gazay/lysa/archive/master.zip}{отсюда}.
Если вы хотите поучаствовать в написании книги – лучше, наверное, клонировать репозитарий.
Вы можете сделать это, выполнив \terminal{git clone https://github.com/gazay/lysa.git} в терминале.
% ENG
% The source for this book can be downloaded at
% \url{https://gitlab.com/lysa/lysa/repository/archive.tar.gz}. If you are looking
% to contribute, it's probably best to clone the git repository. You can clone the
% git repository by running \terminal{git clone https://gitlab.com/lysa/lysa.git}
% in a terminal.