nextupprevious
Next:About this document Up:Operational Semantics of Rewriting Previous:References

Operational Semantics of Rewriting with the On-demand E-strategy in CafeOBJ


We present the full of the operational semantics of rewriting using the on-demand E-strategy in CafeOBJ.
mod! LIST (DAT :: TRIV) {
  pr(NAT)
  [List]
  op nil : -> List
  op __ : Elt.DAT List -> List {r-assoc}
  op _++_ : List List -> List
  op take : List Nat -> Elt.DAT
  op replace : List Nat Elt.DAT -> List
  vars E E1 : Elt.DAT
  vars L L1 : List
  eq nil ++ L1 = L1 .
  eq (E L) ++ L1 = E (L ++ L1) .
  eq take(E L,0) = E .
  eq take(E L,X:NzNat) = take(L,sd(X,1)) .
  eq replace(E L,0,E1) = E1 L .
  eq replace (E L,X:NzNat,E1) = E replace(L,sd(X,1),E1) .
}

mod! PAIR (FST :: TRIV,SND :: TRIV) {
  [Pair]
  op <__> : Elt.FST Elt.SND -> Pair
  op 1st : Pair -> Elt.FST
  op 2nd : Pair -> Elt.SND
  eq 1st(< X:Elt.FST Y:Elt.SND >) = X .
  eq 2nd(< X:Elt.FST Y:Elt.SND >) = Y .
}

mod! TRIPLE (FST :: TRIV,SND :: TRIV,TRD :: TRIV) {
  [Triple]
  op <___> : Elt.FST Elt.SND Elt.TRD -> Triple
  op 1st : Triple -> Elt.FST
  op 2nd : Triple -> Elt.SND
  op 3rd : Triple -> Elt.TRD
  var X : Elt.FST
  var Y : Elt.SND
  var Z : Elt.TRD
  eq 1st(< X Y Z >) = X .
  eq 2nd(< X Y Z >) = Y .
  eq 3rd(< X Y Z >) = Z .
}

mod! VARIABLE principal-sort Var {
  pr(STRING)
  [Var]  op var_ : String -> Var 
}

mod! LOCALSTRATEGY { pr(LIST(INT)*{sort List -> LStrat}) }

mod! FSYMBOL principal-sort FSym {
  pr(STRING + NAT + LOCALSTRATEGY)
  [FSym]
  op op___ : String Nat LStrat -> FSym
  op arity : FSym -> Nat
  op strat : FSym -> LStrat
  op top : FSym -> String
  var S : String 
  var N : Nat
  var L : LStrat
  eq arity(op S N L) = N .
  eq strat(op S N L) = L .
  eq top(op S N L) = S .
} 

mod! VARLIST principal-sort VarList
{ pr(LIST(VARIABLE)*{sort List -> VarList}) }

mod! FSYMLIST principal-sort FSList {
  pr(LIST(FSYMBOL)*{sort List -> FSList})
  op st2Fsym : FSList String -> FSym
  var O : FSym
  var Os : FSList
  var Sym : String
  eq st2Fsym((O Os),Sym)
     = if top(O) == Sym then O else st2Fsym(Os,Sym) fi .
}

mod! SIGNATURE principal-sort Signature {
  pr(PAIR(VARLIST,FSYMLIST)*{sort Pair -> Signature})
  op st2Fsym : Signature String -> FSym
  eq st2Fsym(< Vs:VarList Os:FSList >,Sym:String)
     = st2Fsym(Os,Sym) .
}

mod* QUASIPATTERN principal-sort Pattern {
  pr(VARIABLE + STRING)
  [Var < Pattern]
}

mod! PATTERN principal-sort Pattern {
  pr(LIST(QUASIPATTERN)*{sort List -> PList})
  op _{_} : String PList -> Pattern
  op arg : Pattern NzNat -> Pattern
  eq arg(Sym:String{Args:PList},X:NzNat)
     = take(Args,sd(X,1)) .
}

mod! RULE principal-sort Rule {
  pr(PAIR(PATTERN,PATTERN)*{sort Pair -> Rule})
  ops lhs rhs : Rule -> Pattern
  eq lhs(RR:Rule) = 1st(RR) .
  eq rhs(RR:Rule) = 2nd(RR) .
}

mod! RULELIST principal-sort RuleList 
{ pr(LIST(RULE)*{sort List -> RuleList}) }

mod! TRS {
  pr(PAIR(SIGNATURE,RULELIST)*{sort Pair -> Trs})
  op sig : Trs -> Signature
  op rules : Trs -> RuleList
  eq sig(System:Trs) = 1st(System) .
  eq rules(System:Trs) = 2nd(System) .
}

mod! NODE {
  pr(STRING)
  [Node]
  op _[__] : String Bool Bool -> Node
  op top : Node -> String
  op upODF? : Node -> Bool
  op eval? : Node -> Bool
  op upODF : Node -> Node
  op downODF : Node -> Node
  op setEFlag : Node -> Node
  vars OD EF : Bool
  var Sym : String
  eq top(Sym[OD EF]) = Sym .
  eq upODF?(Sym[OD EF]) = OD .
  eq eval?(Sym[OD EF]) = EF .
  eq upODF(Sym[OD EF]) = Sym[true EF] .
  eq downODF(Sym[OD EF]) = Sym[false EF] .
  eq setEFlag(Sym[OD EF]) = Sym[OD true] .
}

mod* QUASISUBJECT { [Subject] }

mod! SUBJECT principal-sort Subject {
  pr(SIGNATURE + NODE
               + LIST(QUASISUBJECT)*{sort List -> SList})
  op _{_} : Node SList -> Subject
  op top : Subject -> String
  op arity : Subject Signature -> Nat
  op strat : Subject Signature -> LStrat
  op upODF? : Subject -> Bool
  op eval? : Subject -> Bool
  op upODF : Subject -> Subject
  op upODF : SList -> SList
  op downODF : Subject -> Subject
  op setEFlag : Subject -> Subject
  op arg : Subject NzNat -> Subject
  op replace : Subject NzNat Subject -> Subject
  var Nd : Node  var T : Subject vars Args Ts : SList
  var Sig : Signature
  eq top(Nd{Args}) = top(Nd) .
  eq arity(Nd{Args},Sig) = arity(st2Fsym(Sig,top(Nd))) .
  eq strat(Nd{Args},Sig) = strat(st2Fsym(Sig,top(Nd))) .
  eq upODF?(Nd{Args}) = upODF?(Nd) .
  eq eval?(Nd{Args}) = eval?(Nd) .
  eq upODF(Nd{Args}) = upODF(Nd){upODF(Args)} .
  eq upODF(nil) = nil .
  eq upODF(T Ts) = upODF(T) upODF(Ts) .
  eq downODF(Nd{Args}) = downODF(Nd){Args} .
  eq setEFlag(Nd{Args}) = setEFlag(Nd){Args} .
  eq arg(Nd{Args},X:NzNat) = take(Args,sd(X,1)) .
  eq replace(Nd{Args},X:NzNat,T:Subject) 
     = Nd{replace(Args,sd(X,1),T)} .
}

mod! ASSIGN principal-sort Assign 
{ pr(PAIR(VARIABLE,SUBJECT)*{sort Pair -> Assign}) }

mod! SUBSTITUTION principal-sort Subst {
  pr(LIST(ASSIGN)*{sort List -> Subst})
  vars V V1 : Var
  var T : Subject
  var S : Subst
  op var2term : Var Subst -> Subject 
  eq var2term(V,< V1 T > S) 
     = if V == V1 then T else var2term(V,S) fi .
}

mod! MATCH 
{ pr(TRIPLE(BOOL,SUBSTITUTION,SUBJECT)
     *{sort Triple -> Match}) }

mod! CONTRACTUM 
{ pr(PAIR(BOOL,SUBJECT)*{sort Pair -> Contractum}) }

mod* REWRITING {
  pr(TRS + SUBJECT + MATCH + CONTRACTUM)
  op pm : Subject Pattern Trs -> Match
  op pml : Subst NzNat Subject Pattern Trs -> Match
  op pml2 : Match Subst NzNat Subject Pattern Trs -> Match
  op match : RuleList Subject Trs -> Contractum 
  op match2 : Match RuleList Trs -> Contractum
  op eval : Subject Trs -> Subject
  op reduce : Subject LStrat Trs -> Subject
  op reduce2 : Contractum LStrat Trs -> Subject
  op evalArg : Subject NzNat Trs -> Subject
  op upODF : Subject NzNat -> Subject
  op instantiate : Pattern Subst -> Subject
  op instantiate : PList Subst -> SList
  vars T T1 : Subject
  vars N PI : NzNat
  vars V Sym : String
  var TRS : Trs
  var Ps : PList
  vars S S1 : Subst
  var P : Pattern
  var LS : LStrat
  var RR : Rule
  var RRs : RuleList
  var NI : NzInt
  ceq eval(T,TRS) = T if eval?(T) .
  ceq eval(T,TRS)
      = reduce(T,strat(T,sig(TRS)),TRS) if not eval?(T) .
  eq reduce(T,nil,TRS) = setEFlag(T) .
  eq reduce(T,(0 LS),TRS)
     = reduce2(match(rules(TRS),T,TRS),LS,TRS) .
  eq reduce(T,(PI LS),TRS)
     = reduce(evalArg(T,PI,TRS),LS,TRS) .
  ceq reduce(T,(NI LS),TRS)
      = reduce(upODF(T,(- NI)),LS,TRS) if NI < 0 .
  eq reduce2(< true T >,LS,TRS) = eval(T,TRS) .
  eq reduce2(< false T >,LS,TRS) = reduce(T,LS,TRS) .
  eq match(nil,T,TRS) = < false T > .
  eq match((RR RRs),T,TRS) 
     = match2(pm(T,lhs(RR),TRS),(RR RRs),TRS) .
  eq match2(< true S T >,(RR RRs),TRS) 
     = < true instantiate(rhs(RR),S) > .
  eq match2(< false S T >,(RR RRs),TRS) = match(RRs,T,TRS) .
  eq pm(T,(var V),TRS) = < true (<(var V) T > nil) T > .
  ceq pm(T,Sym{Ps},TRS) 
      = pml(nil,1,T,Sym{Ps},TRS) if top(T) == Sym .
  ceq pm(T,Sym{Ps},TRS) 
      = pm(eval(downODF(T),TRS),Sym{Ps},TRS) 
      if top(T) =/= Sym and upODF?(T) .
  ceq pm(T,Sym{Ps},TRS) = < false nil T > 
      if top(T) =/= Sym and (not upODF?(T)) .
  ceq pml(S,N,T,P,TRS) 
      = pml2(pm(arg(T,N),arg(P,N),TRS),S,N,T,P,TRS) 
      if N <= arity(T,sig(TRS)) .
  ceq pml(S,N,T,P,TRS) = < true S T > 
      if N > arity(T,sig(TRS)) .
  eq pml2(< true S1 T1 >,S,N,T,P,TRS) 
     = pml(S1 ++ S,N + 1,replace(T,N,T1),P,TRS) .
  eq pml2(< false S1 T1 >,S,N,T,P,TRS) 
     = < false nil replace(T,N,T1) > . 
  eq evalArg(T,N,TRS) 
     = replace(T,N,eval(downODF(arg(T,N)),TRS)) .
  eq upODF(T,N) = replace(T,N,upODF(arg(T,N))) .
  eq instantiate(var V,S) = var2term(var V,S) .
  eq instantiate(Sym{Ps},S) 
     = Sym[false false]{instantiate(Ps,S)} .
  eq instantiate(nil,S) = nil .
  eq instantiate(P Ps,S) 
     = instantiate(P,S) instantiate(Ps,S) .
}



nextupprevious
Next:About this document Up:Operational Semantics of Rewriting Previous:References


 


Kazuhiro Ogata

Mon Nov 29 13:47:22 JST 1999