ADT NumTh[] /* Extension to NAT */ INITIALS CONSTRUCTORS SELECTORS genInt: NAT*NAT -> LNAT /* Generates an interval of naturals */ gcd: NAT*NAT -> NAT /* Greatest common divisor (Euclid Algorithm) */ isPrime: NAT(i) -> BOOL /* Decides if a natural number is prime */ isPrime2: NAT*NAT -> BOOL /* Helps to decide */ relativePrimes: NAT * NAT ->BOOL /* Decides if two numbers are relative primes */ phi: NAT -> NAT /* The Euler phi function. phi(m) is the amount of positive numbers bellow m that are relative primes with m */ phi2: NAT*NAT(i)->NAT /* Helps to calculate phi */ ack: NAT(i) * NAT -> NAT /* Ackerman function, this shows that ManTa can express more than primitive recursive functions */ AXIOMS genInt(x,y)=if GE(x,y) then nil_NAT else cons_NAT(x,genInt(SUC(x),y)) fi gcd(a,b)=if ISZERO(MOD(b,a)) then a else gcd(MOD(b,a),a) fi isPrime(ZERO)=FALSE isPrime(SUC(x))=isPrime2(SUC(x),x) isPrime2(x,n)= if EQUAL(n,SUC(ZERO)) then TRUE else if ISZERO(MOD(x,n)) then FALSE else isPrime2(x,PRED(n)) fi fi relativePrimes(x,y)=EQUAL(gcd(x,y),SUC(ZERO)) phi(x)=phi2(x,PRED(x)) phi2(x,ZERO)=ZERO phi2(x,SUC(n))= ADD(phi2(x,n), if relativePrime(x,SUC(n)) then SUC(ZERO) else ZERO fi) ack(ZERO,y)=SUC(y) ack(SUC(x),y)= if ISZERO(y) then ack(x,SUC(ZERO)) else ack(x,ack(SUC(x),PRED(y))) fi