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! SIMULATOR
{ pr( 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! SIMULATOR { pr( 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) .
SIMULATOR> red eval(t3,Lcons) .
|