nextupprevious
Next:Hint about Specifying Up:The On-demand E-strategyPrevious:Operational Semantics of

Operational Semantics as Interpreter

Since we can make use of the operational semantics as an interpreter thanks to the executability of CafeOBJ, we can observe the dynamic behavior of rewriting with the on-demand E-strategy using the operational semantics.

We describe the data structure for terms to be rewritten prior to observing the dynamic behavior of rewriting with the on-demand E-strategy. _{_} is a constructor for terms to be rewritten. The first and second arguments are a node and a list of arguments. The node consists of a function symbol name and two flags (i.e. an on-demand flag and an evaluated flag), and its constructor is _[__]. For example, "cons"[false false]{("a"[false false]{nil}) ("nil"[false false]{nil}) nil} denotes the term cons( a, nil). We write a TRS corresponding to TEST2 in the operational semantics.
The module SUBJECT imported into LCONSTERMS provides the data structure for terms to be rewritten.
Example 4 (The TRS Lcons corresponding to TEST2)
        mod! LCONS {
                pr(TRS)
                ops x y z l : -> Var
                op V : -> VarList
                op F : -> FSList
                ops cons tp tl 2nd 3rd a b c d nl : -> FSym
                op Sig : -> Signature
                ops r1 r2 r3 r4 : -> Rule
                op R : -> RuleList
                op Lcons : -> Trs
                eq x = var "X" .
                eq y = var "Y" .
                eq z = var "Z" .
                eq l = var "L" .
                eq V = x y z l nil .
                eq cons = op "cons" 2 (1 -2 0 nil) .
                eq tp = op "tp" 1 (1 0 nil) .
                eq tl = op "tl" 1 (1 0 nil) .
                eq 2nd = op "2nd" 1 (1 0 nil) .
                eq 3rd = op "3rd" 1 (1 0 nil) .
                eq a = op "a" 0 (0 nil) .
                eq b = op "b" 0 (0 nil) .
                eq c = op "c" 0 (0 nil) .
                eq d = op "d" 0 (0 nil) .
                eq nl = op "nl" 0 (0 nil) .
                eq F = cons tp tl 2nd 3rd a b c d nl nil .
                eq Sig = < V F > .
                eq r1 = < ("tp"{("cons"{x l nil}}) nil}}) x > .
                eq r2 = < ("tl"{("cons"{x l nil}}) nil}}) l > .
                eq r3 = < ("2nd"{("cons"{x ("cons"{y l nil}) nil}) nil}) y > .
                eq r4 = < ("3rd"{("cons"{x ("cons"{y ("cons"{z l nil}) nil}) nil}) nil}) z > .
                eq R = r1 r2 r3 r4 nil .
                eq Lcons = < Sig R > .
        }

The constructor for function symbols is op_ _ _ that takes the function symbol name (i.e. a string), the arity and the local strategy given to it as its arguments. For example, op "cons" 2 (1 -2 0 nil) corresponds to the function symbol cons in TEST2. The TRS Lcons has four rewrite rules r1, r2, r3 and r4 that conrresponds to tp(cons(X, L)) --> X, tl(cons(X, L)) --> X, 2nd(cons(X, cons(Y, L))) --> Y, and 3rd(cons(X, cons(Y, cons(Z, L)))) --> Z, respectively. The module TRS imported into LCONS provides the data structure for constructing TRSs such as variables, function symbols, patterns and rewrite rules.

We give some terms to be reduced.

Example 5 (Terms to be reduced w.r.t. Lcons).
        mod! LCONSTERMS {
                pr(SUBJECT)
                ops consN tpN tlN 2ndN 3rdN aN bN cN dN nlN : -> Node
                ops t0 t1 t2 t3 : -> Subject
                eq consN = "cons"[false false] .
                eq tpN = "tp"[false false] .
                eq tlN = "tl"[false false] .
                eq 2ndN = "2nd"[false false] .
                eq 3rdN = "3rd"[false false] .
                eq aN = "a"[false false] .
                eq bN = "b"[false false] .
                eq cN = "c"[false false] .
                eq dN = "d"[false false] .
                eq nlN = "nl"[false false] .
                eq t0 = consN{(cN{nil}) (consN{(dN{nil}) (nlN{nil}) nil}) nil} .
                eq t1 = tpN{t0 nil} .
                eq t2 = 2ndN{(consN{(bN{nil}) (tlN{t0 nil}) nil}) nil} .
                eq t3 = 3rdN{(consN{(aN{nil}) (consN{(bN{nil}) (tlN{t0 nil}) nil}) nil}) nil} .
        }

t1, t2 and t3 denote the following terms:

        t1 -- tp(cons(c, cons(d, nil)))
        t2 -- 2nd(cons(b, tl(cons(c, cons(d, nil)))))
        t3 -- 3rd(cons(a, cons(b, tl(cons(c, cons(d, nil)))))).

The module SUBJECT imported into LCONSTERMS provides the data structure for terms to be rewritten.

One more module is necessary in order to simulate rewriting with the on-demand E-strategy using the operational semantics.

Example 6 (Simulator for rewriting with the on-demand E-strategy).
        mod! SIMULATORpr( REWRITING + LCONS + LCONSTERMS ) }

The module SIMULATOR imports three modules together with module sum. The importation can be separated into three times of importation. The module SIMULATOR is equivalent to the following one:

        mod! SIMULATORpr( REWRITING )    pr( LCONS )    pr( LCONSTERMS ) } .

The module REWRITING provides the operational semantics of rewriting with the on-demand E-strategy.

We show the snapshot of simulating the rewrites of the three terms t1, t2 and t3 with the on-demand E-strategy in Fig.1.
 
SIMULATOR> red eval(t1,Lcons) .
-- reduce in SIMULATOR : eval(t1,Lcons)
("c" [ false true ]) { nil } : Subject
(0.000 sec for parse, 1821 rewrites(0.445 sec), 2378 matches)

SIMULATOR> red eval(t2,Lcons) .
-- reduce in SIMULATOR : eval(t2,Lcons)
("d" [ false true ]) { nil } : Subject
(0.008 sec for parse, 12338 rewrites(2.516 sec), 16363 matches)

SIMULATOR> red eval(t3,Lcons) .
-- reduce in SIMULATOR : eval(t3,Lcons)
("d" [ false true ]) { nil } : Subject
(0.000 sec for parse, 12523 rewrites(2.570 sec), 16583 matches)

Figure 1: Snapshot of the simulator


nextupprevious
Next:Hint about Specifying Up:The On-demand E-strategyPrevious:Operational Semantics of


 


Kazuhiro Ogata

Mon Nov 29 13:47:22 JST 1999