Числа Хаскеля Пеано и лень в умножении

Question

Я начал изучать Haskell недавно, и прямо сейчас в моем классе мы создали класс чисел Peano и создали его в классе типов Num.

Во время лекции мой профессор утверждал, что в зависимости от того, рассматривали ли вы функцию преемника как S x = x + 1 или же S x = 1 + xсоответствующий случай преемника для определения умножения будет другим. Соответственно:

x * S y = x * y + x
x * S y = x + x * y

Более того, он утверждал, что использование первого из этих двух вариантов предпочтительнее, потому что оно ленивее, но мне трудно понять, как это происходит.

Мы рассмотрели пример, в котором определение сложения

x + S y = S (x + y)

лучше, чем

x + S y = S x + y

потому что оценивая x + y == z происходит намного быстрее, но я не могу найти аналогичный случай для умножения.

Лекционные заметки находятся здесь: http://cmsc-16100.cs.uchicago.edu/2014/Lectures/lecture-02.php

Answer 1

Лень не о скорости, а о том, что будет доступно в ближайшее время.

С x * S y = x * y + x тогда вы можете ответить infinity * 2 > 5 очень быстро, потому что он будет расширяться так:

infinity * (S (S Z)) > 5
infinity * (S Z) + infinity > 5
infinity * Z + infinity + infinity > 5
infinity + infinity > 5

(оттуда все остальное тривиально)

Однако я не думаю, что все так хорошо, как утверждал ваш профессор! Попробуйте расширить 2 * infinity > 5 в этом формализме и вы будете разочарованы (или заняты очень долго:-P). С другой стороны, с другим определением умножения, вы получите ответ там.

Теперь, если у нас есть "хорошее" определение сложения, я думаю, что именно в этом случае вы можете получить ответ с бесконечностью в любой позиции. И действительно, я проверил источник нескольких пакетов на Haskell, которые определяют Nats, и они действительно предпочитают x * S y = x + x * y а не то, как утверждал твой профессор, было лучше.