Michael Norrish wrote: > Tom Ridge wrote: > > > I am using EVAL to evaluate some operational semantics. EVAL often > > seems to hang, when I would have expected it to simply stop. This > > often seems to be the case when it doesn't know how to evaluate some > > constant. Why should EVAL hang, rather than e.g. just failing? > > EVAL works with equational definitions, so I'm curious how you're > using it with an operational semantics. In particular, if you've made > an inductive definition with Hol_reln, what equations are you using > from this definition to do your evaluation? >
The opsem is phrased essentially as a map from a state to a list of states. > If you're using the cases (or inversion theorem), you will almost > certainly be putting your system into an infinite loop. > No, I'm just using basic rewrites which should terminate on ground clauses. I shall track down some concrete examples. Thanks Tom > That's my best guess as to what you are seeing. Feel free to send me > additional information if that doesn't cut it. > > Best, > Michael. > ------------------------------------------------------------------------- This SF.net email is sponsored by the 2008 JavaOne(SM) Conference Register now and save $200. Hurry, offer ends at 11:59 p.m., Monday, April 7! Use priority code J8TLD2. http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
