[Maude-users] some questions about the paper The rewriting logic semantics project

[Qi Zhengwei]

Hi,

I am a teacher from Shanghai JiaoTong Univ., China. I have seen the paper
from [1]José Meseguer, Grigore Rosu: The Rewriting Logic Semantics Project.
Electr. Notes Theor. Comput. Sci. 156(1): 27-56 (2006) and [2]José Meseguer,
Grigore Rosu: The rewriting logic semantics project. Theor. Comput. Sci.
373(3): 213-237 (2007)

I am very interested in Rewriting Logic and have some questions about this
project as follows,

1. In Page 20 of [1], there is the definition of ARITHMETIC-EXP-SYNTAX
 	ops _+_ _-_ _*_ : Exp Exp -> Exp [ditto] Generally speaking, * has
the higher priority than + and -. Why don't we define the different priority
for + and * like / and % in the Following definition:
	ops _/_ _%_ : Exp Exp -> Exp [prec 31]

2. In Page 34 of [1], there is the definition of ASSIGNMENT-SEMANTICS
	eq k(exp(X := E, Env) -> K)
		= k(exp(E, Env) -> writeTo(Env[X]) -> val(nothing) -> K)

What's usage of val(nothing)? I think is redundant because the rewrite rule
of WriteTo has no such value(see follow)
	rl t(k(val(V) -> writeTo(L) -> K) TS) mem(Mem)
		=> t(k(K) TS) mem(Mem[L <- V]) .

Additionally, I have seen the same situation in 
	eq k(exp((E ; E’), Env) -> K)
		= k(exp(E, Env) -> discard -> exp(E’, Env) -> K) .
But here 'discard' is deleted by the next equation :
	eq k(val(V) -> discard -> K) = k(K)

Thank you very much for your discussion!


Qi Zhengwei, Ph.D
School of Software, Shanghai JiaoTong Univ.
No. 800 Dongchuan Road, Shanghai, P.R. China 200240
Tel : +86-21-34205595
Fax: +86-21-34205145
Mobile: +86-13818307073
Email: qizhwei at sjtu.edu.cn