User loginNavigation |
simpler representation of operational semantics?While trying to learn the formal notation used in TAPL (and many other papers), I found this paper ... Syntactic Theories of Sequential COntrol and State by Matthias Felleisen. I didn't find this mentioned in any previous discussion on LTU (even though it is from 1992). This paper, as far as I can tell, seems to represent the same idea of TAPL notation in a much more concise manner. For example (horrible 'summary' follows), in Pierce's book (page 72), some rules are listed as follows: Syntax: For t -> t' t1 -> t1' | t1 t2 -> t1' t2 [E-APP1] According to Felleisen's paper, these rules could be written as: For t -> t' C[t] -> C[t'] If we extend the syntax with the following: In other words, we don't have to have such verbose rules because 'C' can represent a 'hole' for a term or its reduction. Ok, this is obviously not a summary of the paper but a question. Is my understanding correct? Is it of any value? I would think so, if one is trying to build 'executable' operational semantics. No? by the way, I found this article through another paper on Operational Semantics for Scheme. This paper (I haven't attempted reading it yet) has further discussion of Felleisen's paper. By shahbaz at 2005-08-08 22:06 | LtU Forum | previous forum topic | next forum topic | other blogs | 8210 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 1 day ago
16 weeks 1 day ago
16 weeks 1 day ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 2 hours ago
51 weeks 4 days ago
51 weeks 4 days ago