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

Зачем это записывать?

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

Почему Маленький испытатель?

Я всегда думал о средствах доказательства теорем. У меня была возможность пройти курс, который использует его еще в NUS, но я пропустил его через две недели. Поступок, о котором я сожалею по сей день. Класс в NUS обучает логике и формальным системам, а также использует coq для закрепления понятий. Код модуля для этого класса - CS3234, и я думаю, что его до сих пор преподает Аквинский Хобор. Во всяком случае, вернемся к книге.

Книга использует Джей-Боб в качестве помощника по доказательству. Это шепелявка, и она реализована в обеих схемах. Излишне говорить, что вам нужно немного шепелявить, чтобы понимать примеры в книге. Однако не требуется большого опыта программирования на Scheme или lisp. Вам просто нужно знать, что lisp использует префиксную нотацию и его выражения оцениваются наизнанку. Другими словами, вы сначала оцениваете или решаете внутренние скобки, прежде чем решать внешние. Например, для выражения (+ 1 2 (- 2 3) вы сначала решаете (- 2 3), вычитание, а затем решаете сложение во внешних скобках.

Помимо использования такого эзотерического языка, как лисп, в книге также используется уникальный стиль вопросов и ответов для обучения концепциям. Не ждите от этой книги длинных абзацев текста и больших участков кода. В большинстве вопросов и ответов используется менее 50 слов. Думайте об этом так, как если бы вы подслушивали разговор двух остроумных профессоров за завтраком (да, в книге в качестве примеров используется завтрак). Как конфессиональному христианину, он напоминает мне катехизаторов, в частности Женевский катехизис. Вот пример того, как учение преподается в Катехизисе:

Q1: Что является главной целью человеческой жизни?

A: Чтобы познать Бога, Который создал людей.

Q2. По какой причине вы так говорите?

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

Q3. Что является высшим благом в человеке?

A: То же самое.

Но я отвлекся, и, конечно же, это не пост о христианских катехизаторах. Хотя, возможно, я напишу об этом в будущем. ;)

Глава 1 - Старые игры, новые правила

Глава начинается с введения в основные функции схемы. А именно cons, car, cdr и atom?.

cons создает ячейку cons. Обычно он используется для соединения начала и конца списка.

(cons 'ham '(eggs))
=> '(ham eggs).

Список в lisp - это, по сути, набор cons ячеек, объединенных cons. '(ham spam eggs) эквивалентно (cons 'ham (cons 'spam (cons '(eggs))).

car возвращает первый элемент cons ячейки.

(car (cons 'ham '(eggs))
=> 'ham

cdr возвращает вторую часть cons ячейки. Обычно он используется для получения списка без первого элемента.

(cdr (cons 'ham '(eggs))
=> '(eggs)

atom? возвращает 't, если аргумент не является пустой cons ячейкой. 't - это просто версия схемы истинного значения.

(atom? a)
=> 't
(atom? '())
=> 't
(atom? (cons 'ham '(eggs))
=> 'nil

После знакомства с основными операциями или функциями Scheme в главе вводятся аксиомы для определения вещей, которые считаются истинными независимо от аргументов. Например, (car (cons a b)) всегда будет возвращать a независимо от значений a и b. Затем он вводит dethm для определения этих аксиом.

(defthm atom/cons (x y)
  (equal (atom (cons x y)) 'nil)
(defthm car/cons (x y)
  (equal (car (cons x y)) x)
(defthm equal-same (x)
  (equal (equal x x) 't)
(defthm equal-swap (x y)
  (equal (equal x y) (equal y x))

defthm означает определение теоремы. Это похоже на определение функции, но оно используется для определения выражений, которые можно переписать. Интересно то, что теоремы могут использоваться в обоих направлениях в результате equal-swap. Например,

(car (cons a b))

равно a, и кроме этого, есть также бесконечно разные способы переписать это выражение. Например, это также равно

(car (cons
       (car (cons a '(ham)))
       b))

Это потому, что a можно переписать в (car (cons a '(ham)) из-за equal-swap.

Вот и все, ребята!

Это все для этой главы.