модуль скелета примитива рекурсия

Question

Я пытаюсь создать функцию модуля в haskell, используя примитивные рекурсивные функции.Я знаю, что это возможно (потому что оно есть в списке примеров функций в Википедии)

И я знаю, как я мог бы логически сделать это тоже ... Но я просто не могу реализовать это!

IE, логика (не примитивная рекурсия или haskell)

function mod(a, b){
  while(a > b)
    a -= b
  return a;
}

которую я могу определить с помощью рекурсии (опять же не haskel)

function mod(a, b){
  if(a < b) return a;
  return mod(a - b, b);
} 

Но я просто не могу реализоватьэто с помощью примитивных рекурсивных функций.Я думаю, что я не могу сделать, это логика . Я думаю, чтобы действительно решить мою проблему, мне нужна какая-то определенная логика, такая как (опять же не haskel)

reduce(a, b)
    = a >= b -> a-b 
    otherwise x

Если бы кто-нибудь мог помочь мне с какой-либо частью этого, я был бы очень признателен, спасибо

Edit :: Я подумал о потенциальном определении функции модуля с использованием деления, то есть mod (a, b) = a- (a / b) * b, но так как моя примитивная рекурсивная функция для деления основана на модуле, я не могу этого сделать, ха-ха

Answer 1

Взгляните на это для некоторых указателей: http://www.proofwiki.org/wiki/Quotient_and_Remainder_are_Primitive_Recursive

Также обратите внимание, что определение в Википедии несколько узкое.Любая функция, построенная по индукции над одной конечной структурой данных, является примитивно-рекурсивной, хотя требуется немного времени, чтобы показать, что это приводит к инструментам, приведенным в Википедии.И обратите внимание, что мы можем представлять натуральные вещества в классическом стиле Пеано.Вы не должны делать это, конечно, но это делает рассуждения об индукции намного более естественными.См. Вики agda для цитирования этого понятия примитивной рекурсии: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality#Primitiverecursion

На следующей странице также есть, как мне кажется, несколько более ясное изложение примитивной рекурсии: http://plato.stanford.edu/entries/recursive-functions/#1.3

Answer 2

Решение этого вопроса

mod(0, y)
        = zero(y)
mod(x, 0)
        = zero(x)
mod(x + 1, y)
        = mult3(succ(mod(x, y)), sign(y), notsign(eq(mod(x, y), diff(y, 1))))