December 4th, 2007

with Cat The Cat

Замечательная статья.

with Cat The Cat

Определение примитивно-рекурсивных функций.

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. Такой же порядок должен быть и у функций с аккумулятором - аккумуляторы только увеличиваются, остальные аргументы увеличиваться не могут.

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