K-user mailing list

["Seyed H. HAERI (Hossein)" <hossein.haeri AT gmail.com>]

Dear all,

In the K Primer, I see examples of rules where the premises include
entities of other sorts. For example, the following rule

rule <k> var (X:#Id,Xl:Ids => Xl) ; ···</k>
<env> Rho:Map => Rho[N/X] </env>
<store>··· . => N |-> 0 ···</store>
<nextLoc> N:#Int => N +Int 1 </nextLoc>

reads to me as if the last three lines (sorts) contain premises, and
the first line -- which applies on sort <k> -- being the result of the
rule. Whilst there are lots of such examples in the Primer, I don't
seem to be able to find examples on how to make K do semantics where
the premises are also of sort <k>. I also had a look into the examples
which ship with the K tool and didn't find anything. As an example of
what I need, you might want to take a look to the attached pdf's APP
rule. (This is the Ott output for the famous operational semantics of
Abramsky and Ong for lazy evaluation.)

My initial guess was something like

  rule <k> M:Exp N:Exp => Q:Val ... </k>
       <k> ... M => lambda X:#Id.P:Exp ... </k>
       <k> ... P[N / X] => Q ... </k>

But, I got the following kompile_error:

Warning: "abrong.maude", line 281 (mod ABRONG): didn't expect token ...</:
mb rule < k > M:Exp N:Exp => Q:Val ...</ k > < k >... M => lambda
X:#Id . P:Exp ...</ <---*HERE*
Warning: "abrong.maude", line 280 (mod ABRONG): no parse for statement
mb rule < k > M:Exp N:Exp => Q:Val ...</ k > < k >... M => lambda
X:#Id . P:Exp ...</ k > < k >... P [N / X] => Q ...</ k > : KSentence
[metadata 
"location=(/home/hossein/Documents/KFram/Teachup/AbramskyOng/abrong.k:18-20)"]
.

So, how would you guys do that in K?

TIA,
--Hossein

--------------------------------------------------------------------------------------------------------------

Seyed H. HAERI (Hossein)

Research Assistant
Institute for Software Systems (STS)
Technical University of Hamburg (TUHH)
Hamburg, Germany

ACCU - Professionalism in programming - http://www.accu.org/
--------------------------------------------------------------------------------------------------------------

Attachment: AbramskyOng.pdf
Description: Adobe PDF document