CafeOBJ cmmdc и рациональные числа

Question

В целочисленном модуле я попытался определить операцию cmmdc, чтобы найти наибольшее общее кратное число. Проблема в том, что я делаю что-то не так, потому что код не работает для 2 простых чисел, таких как 5 и 3.

Это мой код целочисленного модуля:

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) .



}

И так как я импортирую натуральные числа, вот естественный модуль:

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) .




}

---

Также меня попросили сделать модуль для рациональных чисел (Q). Это то, что я написал до сих пор, но, похоже, это как-то не так:

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)) .


}

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

Answer 1

попробуйте "установить шаг" затем «уменьшить cmmdc (5,3)». и на каждом шаге нажмите «n», чтобы продолжить. проверяйте каждый шаг и смотрите, делает ли он то, что вы ожидаете

перевод: Incearca cu "установить шаг" Апой "уменьшить Cmmdc (5,3)." si la fiecare pas apasa "n" (n de la next) si verifica atent daca se intampla ceea ce te astepti.

удачи

Answer 2

(я предполагаю, что мы говорим о "наибольшем общем делителе" как о "наибольшем общем кратном", просто не имеет смысла.)

Я не знаю, что это за язык, но, похоже, у вас нет условия для случая, когда аргументы cmmdc равны.

Кстати, каков результат cmmdc (5,3)? А чего ты ожидал?

(Обратите внимание, что вместо того, чтобы спрашивать «Почему cmmdc (5,3) неправильный?», Лучше спросить: «cmmdc (5,3) возвращает x, но я ожидал y. Почему это так?»)