CafeOBJ cmmdc et les nombres rationnels

Question

Dans le module entier j'ai essayé de définir l'opération cmmdc pour trouver le plus grand multiple commun. Le problème est que je fais quelque chose de mal parce que le code ne fonctionne pas pour 2 nombres premiers comme 5 et 3.

Ceci est mon code pour le module entier:

module integer 

{ 

    protecting (natural) 

    [nat < int] 



    op s_ : int -> int     
    op _+_ : int int -> int { assoc comm idr: 0 } 
    op _-_ : int int -> int    
    op _*_ : int int -> int { assoc comm idr: (s 0) } 
    op _/_ : int int -> int  
    op _<_ : int int -> int  
    op _>_ : int int -> int  
    op _<=_ : int int -> int  
    op cmmdc : int int -> int 




    op p_ : int -> int     -- Predecesor (pentru numere negative) 

    op -_ : int -> int     -- Minusul 



-- -----------------------------------Variable------------------------------------------------- 



    vars x y z a b : int 



-- -----------------------------------Ecuatii--------------------------------------------------- 


-- definirea modului de functionare al lui p fata de s 


    eq s p x = x . 

    eq p s x = x . 


-- definirea lui - ca semn 


    eq - - x = x . 

    eq - 0 = 0 . 

    eq - p x = s - x . 

    eq - s x = p - x . 

-- Adunarea 


    eq x + p y = p(x + y) . 


-- Scaderea 


    eq x - y = x + (- y) . 

-- Inmultirea 

    eq x * p y = x * y - x . 

-- cmmdc 

    eq cmmdc(0, x) = x . 
    eq cmmdc(x, 0) = x . 
    eq cmmdc(s 0, s 0) = s 0 . 
    ceq cmmdc(x, y) = cmmdc(x - y , y) if (x > y) . 
    ceq cmmdc(x, y) = cmmdc(y - x , x) if (y > x) . 



} 

Et puisque j'importe la nombres naturels, voici le module naturel:

module natural 

{ 

    [nat] 

    [nznat] 

    [nznat < nat] 



    op 0 : -> nat 

    op s_ : nat -> nznat 

    op toBool_ : nat -> Bool 



    op _+_ : nat nat -> nat { assoc comm idr: 0 prec: 33} 
    op _-'_ : nat nat -> nat 
    op _*_ : nat nat -> nat { assoc comm idr: (s 0) prec: 31} 
    op _/'_ : nat nznat -> nat 
    op _<_ : nat nat -> Bool 
    op _>_ : nat nat -> Bool 
    op _<=_ : nat nat -> Bool 

    op mod : nat nznat -> nat 



-- ---------------------------Variabile------------------------- 

    var x : nat 

    var y : nat 

    var z : nat 

    var a : nznat 


-- ---------------------------Ecuatii---------------------------  

    -- eq x + 0 = x . 

    -- eq 0 + x = x . 


-- Suma: 


    eq x + s y = s (x + y) . 


-- Diferenta: 


    eq x -' 0 = x . 

    eq 0 -' x = 0 . 

    eq s x -' s y = x -' y . 


-- Inmultirea 

    eq x * 0 = 0 . 
    eq x * s y = x * y + x . 

-- Impartirea:  [parte intreaga] 


    eq 0 /' a = 0 . 

    eq x /' a = ((x -' a) /' a) + s 0 . 


-- ? 


    -- eq 0 < z = true . 

    -- eq x < y = toBool (x -' y) . 

    -- ceq x < y = true if toBool (x -' y) . 

    -- ceq x < y = false if toBool (x -' y) == false . 


-- Conversie de la integer la Bool 

    eq toBool 0 = true . 

    eq toBool z = false . 

-- Mai mic 


    eq x < y = toBool (x -' y) . 


-- Mai mic sau egal 

    ceq x <= y = true if (x < y) or (x == y) . 

    ceq x <= y = false if (y < x) . 


-- Mai mare 


    ceq x > y = true if (y < x) . 

    ceq x > y = false if (x < y) . 

-- mod 

    ceq mod(x, a) = x if (x < a) . 
    ceq mod(x, a) = mod(x -' a, a) if (x > a) . 




} 

---

de plus, on m'a demandé de faire un module pour les nombres rationnels (Q). C'est ce que je l'ai écrit jusqu'à présent, mais il semble qu'il est en quelque sorte de mal:

module rational 
{ 
    protecting (integer) 
    [integer < rational]  
    [rational* < rational] 

    op _|_ : int nznat -> rational 
    op _||_ : nznat nznat -> rational* 

    op _+"_ : rational rational -> rational 
    op _-"_ : rational rational -> rational 
    op _*"_ : rational rational -> rational 
    op _/"_ : rational rational* -> rational 

    op reducere_ : rational -> rational 

-- -----------------------------------Variabile-------------------------------------------------  
    var x : int 
    var y : int 
    var z : int 

    var a : nznat 
    var b : nznat 
    var c : nznat 

-- -----------------------------------Ecuatii--------------------------------------------------- 

-- Adunarea 

    ceq (x | a) +" (y | b) = (x + y) | a if (a == b) . 
    ceq (x | a) +" (y | b) = (x * b + y * a) | (a * b) if (a > b) or (a < b) . 

-- Scaderea 

    ceq (x | a) -" (y | b) = (x - y) | a if (a == b) . 
    ceq (x | a) -" (y | b) = (x * b - y * a) | (a * b) if (a > b) or (a < b) . 

-- Inmultirea 

    eq (x | a) *" (y | b) = (x * y) | (a * b) . 

-- Impartirea 

    eq (x | a) /" (b || c) = (x * c) | (a * b) . 

-- Aducere la acelasi numitor 

    eq reducere x | a = (x/cmmdc(x, a)) | (a/cmmdc(x, a)) . 


} 

Pourriez-vous s'il vous plaît me dire où je reçois des choses mauvaises? Je n'arrive pas à comprendre par moi-même.

Answer 1

(je suppose que nous parlons du « plus grand diviseur commun » comme le « plus grand commun multiple » n'a aucun sens.)

Je ne sais pas quelle langue cela est, mais il vous semble ne pas avoir une clause pour le cas où les arguments de cmmdc sont égaux.

BTW, quel est le résultat de cmmdc (5,3)? Et qu'attendiez-vous?

(Notez qu'au lieu de demander "Pourquoi cmmdc (5,3) est-il faux?", Il vaut mieux demander: "cmmdc (5,3) renvoie x, mais je m'attendais à y." Pourquoi? ")

Answer 2

essayez "set step on" puis "réduire cmmdc (5,3)." et à chaque étape, appuyez sur "n" pour continuer. vérifier chaque étape et voir si elle fait ce que vous attendez

incearca cu "mettre étape sur" apoi "réduire cmmdc (5,3)." si la fiecare pas apasa "n" (n de la prochaine) si verifica atent daca se intampla ceea ce te astepti.

bonne chance