Reduce

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.

Trace

To show a trace of reduction, set the trace switch on as follows.

NAT+> set trace on
NAT+> 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 on
NAT+> 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.

[Next] Proof scores

Original Copyright © Takahiro Seino, all rights reserved.