osa1

Quick rant (K Framework)

September 19, 2013 - Tagged as: en, kframework.

In this short rant I’ll demonstrate how K Framework is broken and how you can avoid the problem. If you don’t know what is K Framework or don’t use it, you probably want to ignore this post.

Let’s think this completely useless K module:

module TEST

  syntax Exp ::= "nilExp"
               | return(Exp) [strict]

  syntax Val ::= "nil"

  syntax KResult ::=  Val

  rule nilExp => nil ... [nil]

endmodule

and this TEST program:

return(nilExp)

what do you think this program has in K cell when it gets stuck? It’s not really hard to guess. Since we annotate return(Exp) syntax with strict, it’s argument gets evaluated according to our nil rule and then it gets stuck. At this point K cell will be:

<k>
    return ( nil )
</k>

which may not be very surprising for you, but there’s something wrong going on here. In our syntax declaration we defined argument or return to be an Exp, but in the term in our K cell it’s Val.

At this point you can say that this is how heating/cooling works an there’s nothing wrong here but then we have another problem: there’s no way for the user to write rules that does exactly what heating/cooling rules do. In our example above you’d expect from strictness annotation to generate rules like this:

rule return(E:Exp) => E ~> return(HOLE)
rule V:Val ~> return(HOLE) => return(V)

but this is not a valid rule and it fails with the this error message:

[Error] Critical: type error: unexpected term 'V:Val ' of sort 'Val', expected sort 'Exp'.
        File: /home/omer/K/lua-semantics/test/test.k
        Location: (11,35,11,36)

and what’s more confusing is that even though K generated rule somehow generates the term return(Val), you cannot match it in your rules because this term is actually ill-typed:

rule return(V:Val) => .
...
[Error] Critical: type error: unexpected term 'V:Val ' of sort 'Val', expected sort 'Exp'.
        File: /home/omer/K/lua-semantics/test/test.k
        Location: (11,10,11,15)

which means there’s no way for you to work on this term. This time you’re stuck :-p

We discussed this on k-user mailing list a bit but there isn’t really a solution – we only have a workaround. Here’s the reason of this problem(quoted from mailing list discussion):

Your grammar is only enforced during parsing.

After the definition is compiled, return is just a label that may be applied to a list of children.

In particular, the automatically generated cooling rule only puts a side condition that enforces IsKResult, which nil passes.

Wow, this sounds like really broken to me. Anyway, only solution I could find to this is to add Val syntactic category to a member of Exp syntactic category. This is an obvious solution, but very bad one also. Because by having distinguished Val and Exp syntactic categories what I’m trying to do is to force my program to get stuck as soon as possible when something went wrong, instead of continuing evaluation and get stuck at a point where very very far from where the error actually occured.

Rest of this post is also sent to k-list mailing list and contains my ideas on implementing strictness annotations. These ideas may be wrong – I’m only a beginner K user.

This is how I’d design strictness annotations(but I’m probably wrong since I’m just a beginner in K).

Let’s say I have this syntax:

syntax Exp ::= P(Exp, Exp, Exp) [strict]

for intermediate steps while fully evaluating this expression, I’d design the K framework so that these syntax and rules would be automatically generated:

syntax K ::= P__rw_1(Val, Exp, Exp) [strict]
           | P__rw_2(Exp, Val, Exp) [strict]
           | P__rw_3(Exp, Exp, Val) [strict]

rule P(E1, E2, E3) => E1 ~> P__rw_1(HOLE, E2, E3)
rule P(E1, E2, E3) => E2 ~> P__rw_1(E1, HOLE, E3)
rule P(E1, E2, E3) => E3 ~> P__rw_1(E1, E2, HOLE)

rule V:Val ~> P__rw_1(HOLE, E2, E3) => P__rw_1(V, E2, E3)
rule V:Val ~> P__rw_2(E1, HOLE, E3) => P__rw_2(E1, V, E3)
rule V:Val ~> P__rw_3(E1, E2, HOLE) => P__rw_3(E1, E2, V)

and then same rule generation scheme applies to P__rw_1, P__rw_2, P__rw_3 too. In the end we’ll end up with:

syntax K ::= P__rw(Val, Val, Val)

and this would give the user full control of evaluation with strongly typed manner. (ie. without fighting with K framework parser)

(strict[n], seqstrict etc. rules are specialized cases of this general strictness rule generation scheme)

(Show comments)