Skip to content

Latest commit

 

History

History

tom-harding-peanos-forte

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 

Форте Пеано

Перевод статьи Tom Harding: Peano's Forte. Опубликовано с разрешения автора.

Сто лет назад, за долго до Покемонов и Slap Chop, жил умный парень по имени Джузеппе Пеано, придумавший изящный способ описать натуральные числа (0, 1, 2, 3, ...):

Первое — 0, которое мы будем писать как Z.

Число после любого x, его наследник, S x.

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

Обычное Пеано
0 Z
1 S Z
2 S (S Z)
3 S (S (S Z))
. . . . . .

Может быть, не самая красивая запись, но, мне кажется, довольно неплохо выглядит. Число или Z, или S другого числа, которое или Z, или S другого числа, которое… ну, вы поняли! Назовём это рекурсивное определение.

Благодаря этому, мы можем определить функции чисел Пеано, используя рекурсию! Вот функция для проверки эквивалентности:

A B A == B
Z Z true
S x Z false
Z S y false
S x S y x == y

Правило 3 может показаться дублем 2, но мы должны определить оба, как в случае, когда порядок аргументов важен (например, с вычитанием: 2 - 3 не тоже самое, что 3 - 2).

Правило 4 — кусочек рекурсивной магии: если x и y всё ещё наследники, мы проверяем правило 4 ещё раз, и мы продолжаем делать это, пока одно из других трёх условий не удовлетворим. Мы можем записать процесс определения 2 == 3 с нашими числами Пеано:

(S (S Z)) == (S (S (S Z)))
  => (S Z) == (S (S Z)) -- By rule 4
  => Z == (S Z)         -- By rule 4
  => false              -- By rule 2

Множество скобок, но, надеюсь, достаточно ясно, чтобы понять, что происходит: пока оба аргумента являются наследниками, мы убираем одну S на каждом шаге, пока не останется одна Z. Если с другой стороны тоже Z в то же самое время, тогда два числа равны! О, да.

Определить сложение тоже довольно просто:

A B A + B
Z Z Z
S x Z S x
Z S y S y
S x S y S (S (x + y))

правила 1, 2 и 3 определяют наши базовые сценарии: прибавляя Z к любому значению, получаем то же самое значение. Правило 4, конечно же, там мы определяем нашу рекурсию. Давайте посмотрим на пример с 3 + 2. Мы будем использовать квадратные скобки для наглядности, но будем думать о них, как об обычных скобках:

(S (S (S Z))) + (S (S Z))
  => S (S [(S (S Z)) + (S Z)]) -- By rule 3
  => S (S (S (S [(S Z) + Z]))) -- By rule 3
  => S (S (S (S (S Z))))       -- By rule 1

Получилось! Ещё один пример, который стоит упомянуть, прежде чем мы перейдём к конвертации наших Пеано чисел обратно в целые числа, которые мы знаем и любим:

A toInt A
Z 0
S x 1 + toInt x

Нам нужен всего один аргумент для этого, так что функция очень простая. Ура! Вот эта функция работает с числом 3:

toInt (S (S (S Z)))
  => 1 + toInt (S (S Z)) -- By rule 2
  => 1 + 1 + toInt (S Z) -- By rule 2
  => 1 + 1 + 1 + toInt Z -- By rule 2
  => 1 + 1 + 1 + 0       -- By rule 1
  => 3                   -- By addition

Итак, это может быть не самый крутой пример, но мы рассмотрели некоторые важные вещи:

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

  • Мы можем использовать индукцию чтобы показать, что если функция работает для Z (или другого базового случая) и S x, она может работать для любого числа Пеано!

  • Выполнение функции — просто подмена одного на другое! Функции не должны делать ничего - они должны менять входные данные на выходящие.

Это всё от меня на сегодня! Если вы хотите потренироваться, вы можете использовать try.purescript.org gist, чтобы поиграться с кодом. В противном случае, я надеюсь, было хоть немного интересно, и я ещё поговорю с тобой позже!

Берегите себя ♥


Слушайте наш подкаст в iTunes и SoundCloud, читайте нас на Medium, контрибьютьте на GitHub, общайтесь в группе Telegram, следите в Twitter и канале Telegram, рекомендуйте в VK и Facebook.

Статья на Medium