CafeOBJ supports reduction of terms. An input term is reduced by applying equations where each equation is regarded as a left-to-right rewrite rule. A term which no equation can be applied to is called a normal form.

The `red`

command reduces a term.

`red `

*<term>*` .`

Example:

Let us reduce Term `s(s(0)) + s(s(s(0)))`

in Module `NAT+`

.

First, select Module `NAT+`

.

CafeOBJ>select NAT+NAT+>

Then, reduce Term `s(s(0)) + s(s(s(0)))`

by the `red`

command:

NAT+>red s(s(0)) + s(s(s(0))) .-- reduce in NAT+ : s(s(0)) + s(s(s(0))) s(s(s(s(s(0))))) : Nat (0.000 sec for parse, 3 rewrites(0.010 sec), 5 matches) NAT+>

In the above, the `red`

command reduced Term `s(s(0)) + s(s(s(0)))`

into its normal form `s(s(s(s(s(0)))))`

. Reduction guarantees that the input term is equivalent with the output term in the specification. So, the above example is a proof of 2 + 3 = 5.

To show a trace of reduction, set the `trace`

switch on as follows.

NAT+>set trace onNAT+>red s(s(0)) + s(s(s(0))) .-- reduce in NAT+ : s(s(0)) + s(s(s(0))) 1>[1] rule: eq s(N:Nat) + M:Nat = s(N + M) { N:Nat |-> s(0), M:Nat |-> s(s(s(0))) } 1<[1] s(s(0)) + s(s(s(0))) --> s(s(0) + s(s(s(0)))) 1>[2] rule: eq s(N:Nat) + M:Nat = s(N + M) { N:Nat |-> 0, M:Nat |-> s(s(s(0))) } 1<[2] s(0) + s(s(s(0))) --> s(0 + s(s(s(0)))) 1>[3] rule: eq 0 + M:Nat = M { M:Nat |-> s(s(s(0))) } 1<[3] 0 + s(s(s(0))) --> s(s(s(0))) s(s(s(s(s(0))))) : Nat (0.000 sec for parse, 3 rewrites(0.020 sec), 5 matches) NAT+>

There is another trace mode: the `trace whole`

switch:

NAT+>set trace whole onNAT+>red s(s(0)) + s(s(s(0))) .-- reduce in NAT+ : s(s(0)) + s(s(s(0))) [1]: s(s(0)) + s(s(s(0))) ---> s(s(0) + s(s(s(0)))) [2]: s(s(0) + s(s(s(0)))) ---> s(s(0 + s(s(s(0))))) [3]: s(s(0 + s(s(s(0))))) ---> s(s(s(s(s(0))))) s(s(s(s(s(0))))) : Nat (0.000 sec for parse, 3 rewrites(0.020 sec), 5 matches) NAT+>

In this mode, only the whole terms in the trace are shown simply.

Original Copyright © Takahiro Seino, all rights reserved.