Итак, пост-отзыв по EOPL3 после первой неполной недели чтения.
Из двух глав осилил пока только первую, где в основном столкнулся с проблематикой задания различных наборов данных через индукцию, как и было обещано в названии 🙂
Обычно, множества предлагается задавать через т.н. list comprehensions, которые есть во многих ФП языках типа хаскеля, а так же есть в python, C#, Kotlin и т.д.
Примеры ниже (на python, C# и Kotlin соответственно):
[3 * n for n in natural_numbers()]from n in NaturalNumbers() select 3 * n;
// или аналогичное, но без Expression Syntax:
NaturalNumbers().Select(n => n * 3);naturalNumbers().map { n -> n * 3 }В EOPL3 авторы предлагают отойти от этого способа и определять множества индуктивно, через факты и предикаты как если бы мы оперировали неким логическим языком программирования.
Причём можно определить это двумя способами:
in_s (0) :- true.
in_s (n) :- in_s (n - 3).либо
in_s (0) :- true.
in_s (n + 3) :- in_s(n).Первый способ задаёт множество сверху-вниз. В этом случае, для того, чтобы узнать, входит ли некое натуральное число в множество, нам нужно либо уже знать о факте его наличия в множесте, либо вывести этот факт из другого числа. Можно прочитать это как:
n входит в множество S тогда и только тогда, если
1. n = 0,
2. n - 3 входит в множество S
Второй способ, наоборот, предлагает индуктивно расширять множество, и поэтому называется подходом с заданием множества снизу-вверх. Можно прочитать это как:
1. 0 входит в множество S,
2. если n входит в множество S, то n + 3 тоже в него входит
Далее авторы предлагают поделать упражнения по заданию различных интересных множеств. При этом, авторы не ограничиваются множествами натуральных чисел и вводят более интересные структуры данных (например, определяют стукруту функциональных списков)
После некоторого ряда примеров, предлагается ещё одит способ задания множеств, в этом случае через грамматики. Грамматики пишутся с использованием подобия BNF в подобном виде:
<List-of-Int> ::= ()
<List-of-Int> ::= ( <Int> . <List-of-Int> )
Тут <List-of-Int> является синтаксической категорией, и задаётся через две продукции.
Первая задаёт конечное условие о том, что пустой список это тоже список, причём пустой список записывается двумя терминальными символами ( и ).
Вторая продукция указывает, что <List-of-Int> является парой из другой синтаксической категории <Int>, являющейся головой списка и, собственно, другого <List-of-Int>, являющегося хвостом. При этом такой список опоясан парными терминальными символами ( и ), а голова и хвост разделены терминальным символом .
Далее в книге вводятся способы проверять структуры данных на соответствие грамматике через так называемые syntatic derivations, где мы последовательно применяем замену нетерминалов в грамматике на терминалы. Если в итоге остались только терминальные символы, структура соответствует грамматике. Переписывать примеры из книги не вижу особого смысла, так что двигаемся дальше.
Далее идут описания через грамматику упрощённых s-выражений, бинарных деревьев и лямбда-варажений, и попутно вводятся новые способы записывать грамматику более коротким способом. Для бинарных деревьев приводится пример, как можно по индукции доказывать теоремы о наборах данных, заданных грамматиками. Так, приводится доказательство, что у бинарного дерева всегда нечётное количество нод. Так же есть упражнение на доказательство теоремы о парности скобок в лямбда-выражении.
В следующем разделе предлагается подход по написанию рекурсивных функций, обрабатывающих наборы, заданные индуктивно. Самый главный принцип который запал мне в голову из данного раздела, это предложение "следовать грамматике", то есть на каждую отдельную синтаксическую категорию выделять по отдельной функции, и таким образом иметь возможность фокусироваться на одной сущности за раз.
Далее следует некоторое количество упражнений для того, чтобы читатель мог попрактиковаться в написании рекурсивных функций, и на этом глава подходит к концу