K-user mailing list

[Yilong Li <yilongl AT cs.stanford.edu>]

Everett,

"rule X:Int + Y:Int => X +Int Y" only applies to the top of k cell.

Russell,

Disclaimer: I haven't worked on the K framework for quite some time and my view is probably outdated/inaccurate.

Based on your examples of what you mean by runtime state, I would say the runtime state of K is just a many-sorted term. A term is just K label applied to zero or more terms. There are some terms that have special meaning in K (e.g. cell, KItem, KList, KSequence) but they are just terms in the end. There are also builtin data-structures like map, set, and list (which can also be represented in the form of labelled terms). I believe they are currently generic in the sense that their keys, values, or elements are just generic terms. Hope it helps.

Yilong

On Tue, Sep 5, 2017 at 12:56 PM, Everett Hildenbrandt <hildenb2 AT illinois.edu> wrote:

Only some languages have an `<env>` cell which maps names to values (and several of the tutorial languages do have this feature).

But the configuration can specify any state it wants, one cell can be a map like the `<env>` cell, but other cells can store any runtime information they want (a list of active processes for example).

It all boils down to patterns in the Matching Logic sense of pattern (and even in most cases, just plain terms in a term algebra).

Execution in K is done via rewriting the terms, so for example if you have the rule:

```k
    syntax Exp ::= Int | Exp "+" Exp
 // --------------------------------
    rule X:Int + Y:Int => X +Int Y
```

What this means is "take any occurance of the term `_+_(var(X, Int), var(Y, Int))` and replace it with an occurance of the term `_+Int_(var(X,Int), var(Y,Int))`.

So you can think of terms as labelled trees, where the label on each node is the operator that holds the sub-trees (eg. the label in the above example is `_+_` and gets changed by the rewrite to `_+Int_`).

A more interesting example would be:

```k
    syntax Stmt ::= "if" Bool "then" Stmt "else" Stmt
 // -------------------------------------------------
    rule if true  then S1 else S2 => S1
    rule if false then S1 else S2 => S2
```

This pair of rules states "replace any occurance of `if_then_else_(const(true, Bool), var(S1, Stmt), var(S2, Stmt))` with just `var(S1,Stmt)`" and similarly for the `const(false, Bool)` case.

Thus, we represent both programs (and program fragments) as terms, so that execution can just be term rewriting (replacing subterms that match the left-hand-side of a rule with the right-hand-side).

I'd recommend the book "Algebraic Semantics of Imperative Programs" by Goguen if you are able to get ahold of a copy.
It's based on OBJ, which has a very similar syntax to Maude (was a predecessor to Maude), and should help clarify what terms, rewriting, and algebras are.
The semantics of K is given in terms of Reachability Logic and Matching Logic, but execution (at the moment) pretty much follows standard rewriting.

Everett H.

On Mon, Sep 04, 2017 at 01:27:05AM +0100, Russell Wallace wrote:
> I'm still trying to get my head around exactly how the runtime model of K
> works, so trying to boil it down to a concrete question:
>
> Per the tutorials, a K runtime contains, or at least may contain, a 'state'
> cell which is a map of names to values. What exactly is the type of this map?
>
> The keys are strings, right?
>
> What about the values? Are they dynamic as in Lisp or Python? In which case,
> would it be accurate to say K uses a dynamic type system similar to those
> languages?