K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

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?