K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

> 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.

Rules describe a single step which modifies several cells. There's not
a generally useful way to consider affected cells as premises.
Rather, in every cell with an =>, the part to the left is a pattern that
has to match for the rule to apply, and the part to the right is what
it will be replaced with after applying the rule. (the effects stop at
parentheses, ellipses, or the edge of a cell).

A cell without an
arrow has to be present and match the contents as described,
so those can be usefully read as preconditions or side conditions.

If k, env, store, and nextLoc are the only cells in your configuration,
a fully explicit version of the computation step described by that
rule might look like this:

rule

(<k> var (X:#Id,Xl:Ids) ; ~> Rest:K</k>
<env> Rho:Map </env>
<store>L:Map .Map R:Map</store>
<nextLoc> N:#Int </nextLoc>)

==>

(<k> var Xl ; ~> Rest</k>
<env> Rho[N/X] </env>
<store>L (N |-> 0) R</store>
<nextLoc> N +Int 1 </nextLoc>)


> 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>

It looks like this is aiming for a big-step style, while K is based on 
operational semantics.

The main effect of the rules would be expressed with something like

rule <k> (lambda X:#Id.P:Exp) N:Exp => P[N/X] ...</k>

Reducing P[N/X] to a value would be handled by applying more rules 
afterwards, and
getting M to reduce to a lambda would be handled by making sure application 
is strict
in at least the first argument.

Brandon