Maude-help mailing list

[Brahim Nasraoui <brahim.nasraoui AT gmail.com>]

Hello everyone,

I want to simulate the calculation of the addition operation on binary numbers, I am restricted in this example with 2 bits only ,
numbers are given by e (e1, e2), ei can be T or F, T for true and F for false, but the problem is that it works very well with 2 numbers
plus (e (e1, e0), e (e'1, E0)) where plus( , ) is the operator of addition in our example, but for 3 numbers plus(plus (e (F, F ), e (F, F)), e (F, F)) does not work very well and generate unwanted terms.

The set of rewriting rules of the system of the addition of two binary numbers is described as follows:

  pluse(e(e1,e0),e(e'1,e'0)) => e(plusb(e1,e'1,F),plusb(e0,e'0,F)) .

  e(plusb(e1,e'1,F),plusb(F,F,F)) => e(plusb(e1,e'1,F),F) .

  e(plusb(e1,e'1,F),plusb(F,T,F)) => e(plusb(e1,e'1,F),T) .

  e(plusb(e1,e'1,F),plusb(T,F,F)) => e(plusb(e1,e'1,F),T) .

  e(plusb(e1,e'1,F),plusb(T,T,F)) => e(plusb(e1,e'1,T),F) .

  e(plusb(F,F,F),e0) => e(F,e0) .

  e(plusb(F,F,T),e0) => e(T,e0) .

  e(plusb(F,T,F),e0) => e(T,e0) .

  e(plusb(F,T,T),e0) => e(F,e0) .

  e(plusb(T,F,F),e0) => e(T,e0) .

  e plusb(T,F,T),e0) => e(F,e0) .

  eplusb(T,T,F),e0) => e(F,e0) .

  e(plusb(T,T,T),e0) => e(T,e0) .

These rules allow to calculate the sum of two terms e (e1, e0), e (e'1, e'0),

When I have two terms Maude gives: pluse (e (F, F), e (F, F)) => * e (F, F)

Maude> frew pluse(e(F,F),e(F,F)) .
frewrite in testtt : pluse(e(F, F), e(F, F)) .
*********** rule
rl pluse(e(e1, e0), e(e'1, e'0)) => e(plusb(e1, e'1, F), plusb(e0, e'0, F)) [label regle-yyyy] .
e1 --> F
e0 --> F
e'1 --> F
e'0 --> F
pluse(e(F, F), e(F, F))
--->
e(plusb(F, F, F), plusb(F, F, F))
*********** rule
rl e(plusb(e1, e'1, F), plusb(F, F, F)) => e(plusb(e1, e'1, F), F) [label regle-01] .
e1 --> F
e'1 --> F
e(plusb(F, F, F), plusb(F, F, F))
--->
e(plusb(F, F, F), F)
*********** rule
rl e(plusb(F, F, F), e0) => e(F, e0) [label regle-6] .
e0 --> F
e(plusb(F, F, F), F)
--->
e(F, F)

rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)

result exponent: e(F, F)
Maude>

Now if I take three terms Maude gives:

pluse (pluse (e (F, F), e (F, F)), e (F, F)) => * e (plusb (plusb (F, F, F), F, F), plusb (plusb (E, F, F), F, F))




Maude> frew pluse(pluse(e(F,F),e(F,F)),e(F,F)) .                                                                            
frewrite in testtt : pluse(pluse(e(F, F), e(F, F)), e(F, F)) .                                                         
*********** rule                                                                                                       
rl pluse(e(e1, e0), e(e'1, e'0)) => e(plusb(e1, e'1, F), plusb(e0, e'0, F)) [label regle-yyyy] .                       
e1 --> F                                                                                                               
e0 --> F                                                                                                               
e'1 --> F                                                                                                              
e'0 --> F                                                                                                              
pluse(e(F, F), e(F, F))
--->
e(plusb(F, F, F), plusb(F, F, F))
*********** rule
rl pluse(e(e1, e0), e(e'1, e'0)) => e(plusb(e1, e'1, F), plusb(e0, e'0, F)) [label regle-yyyy] .
e1 --> plusb(F, F, F)
e0 --> plusb(F, F, F)
e'1 --> F
e'0 --> F
pluse(e(plusb(F, F, F), plusb(F, F, F)), e(F, F))
--->
e(plusb(plusb(F, F, F), F, F), plusb(plusb(F, F, F), F, F))

rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)

result exponent: e(plusb(plusb(F, F, F), F, F), plusb(plusb(F, F, F), F, F))




--
Brahim NASRAOUI