Discreet and not discrete.

Тут случилась ветка с критикой Хаскеля и разбором стиля кодирования.

К ней я и хочу добавить несколько слов.

( Collapse )

Упоминавшийся уже Лузин, который был не только математиком, но и философом (и даже его избрание в 1929 году в Академию наук СССР произошло “по кафедре философии”), так высказывался на эту тему: “По-видимому, натуральный ряд чисел не представляет из себя абсолютно объективного образования. По-видимому, он представляет собой функцию головы того математика, который в данном случае говорит о натуральном ряде”.

Про красоту математики.

У кого утащил, уже не помню, три дня назад это было. ;)

Primitive recursive functions.

Начал читать в попытке разобраться, как строить функции из не-Тьюринг-полного подмножества лямбда-исчисления с типами.

Что-то мне не очень нравится этот подход.

Мне больше нравится подход с определением порядка на аргументах.

A Taste of Rewrite Systems содержит некоторое число определений порядка на термах. Например, количество термов-не-переменных C(t): для (x:xs), (Just x) и Nothing это будет C(t)=1, для x и xs - C(t)=0.

Таким образом, получается, что мы можем выписывать прямую рекурсию, если C(t) аргументов рекурсивного вызова меньше или равно C(t) аргументов текущего определения:

map f (x:xs) = f x :map f xs

C(xs) < C((x:xs)). Что делать с взаимной рекурсией, непонятно.

По идее, класс функций можно расширить.

Например, функция Аккермана:

ack Z n = S n                            -- ack 0 n = n+1
ack (S m') Z = ack m (S Z)                -- ack m 0 = ack (m-1) 1
ack m@(S m') n@(S n') = ack m' (ack m n') -- ack m n = ack (m-1) (ack m (n-1))

Здесь, по идее, есть порядок. Первый аргумент ack всегда уменьшается, если не равен Z. Такой же порядок должен быть и у функций с аккумулятором - аккумуляторы только увеличиваются, остальные аргументы увеличиваться не могут.

Как быть со взаимной рекурсией, все равно непонятно. ;)