K-user mailing list

[Traian Florin Șerbănuță <tserban2 AT illinois.edu>]

Hi Hossein,

Sorry for the unreadable error.  I have written code now to convert it into a more reasonable one.

The reason for which you see it like this is because nobody has encounter that error until now.

While on parsing errors we don't yet have a mechanism for reporting errors, we have devised one for compilation.  However, I am adding handlers one by one as errors are encountered.

Now, coming back to your problem,  the ''nicer'' error now says.

[ERROR]: Cell <heap> appears multiple times at the top level but its

multipliciy does not allow that. Check the initial configuration for the

definition matches the rule.

 Term:

<_>_</_>(heap,_=>_(GPlus:Map,_`[_/_`](DMinus:Map,Z:KItem,_`(_`)(#_(X:#Id),

.List`{K`}))),heap)

 Context:

Location: /Users/tserban2/Downloads/test/test.k:7-9

 Compilation phase: CONTEXT-TRANSFORMERS

Aborting the compilation

The main reason is that you are still trying to encode premises in K rules.

Maybe the previous mails were not clear about that, so I'll say this again, although it might disappoint you:

K does not support premises for rules.  At best, it allows for side conditions, but those cannot be used to encode premises.

Therefore, K is suitable for writing (small-step) operational semantics in the SOS style of reduction semantics (with evaluation contexts), or of the Chemical abstract machine (CHAM), or for describing abstract machines.  

We find this quite convenient, because for debugging, non-determinism and exploring the transition system, small-step SOS-like definitions are more appropriate than big-step ones.

Nevertheless, if you are interested in expressing big-step definitions using rewriting, you could use rewriting logic/Maude directly to express rules reasonably close to the definition on paper.

If you're interested on how we do this, you can take a look at the material we use for classes here at UIUC

http://fsl.cs.uiuc.edu/images/7/7b/CS422-Fall-2011-PL-book-bigstep.pdf

Towards the end it has a section on representing big-step SOS in rewriting logic/Maude.

Nevertheless, if you need a smaller-step SOS definitional style, then I would definitely recommend K for the longer run, and we would be more than glad to assist you.

best wishes,

- traian

2012/2/24 Seyed H. HAERI (Hossein) <hossein.haeri AT gmail.com>

Hi again,

Here is an update: Using the information you guys kindly gave me over
other threads, I came up with the following code:

 rule <k> X:#Id => Z ... </k> <heap> GPlus:Map => DMinus[Z/X] </heap>
      (<k> GPlus(X) </k> <heap> GPlus[undef/X] </heap> => <k> Z:Val
</k> <heap> DMinus:Map </heap>)

which unfortunately doesn't work either. Here is the frightening and
cryptic error message I get:

Advisory: could not find an operator R`{_`,_`,_`} with appropriate
domain in meta-module COMPILE-LOOP when trying to interprete metaterm
'R`{_`,_`,_`}['_`[_`][''__.Sort,'_`,_['_`[_`][''_=>_.Sort,'_`,_['_`[_`][''__.Sort,'_`,_['_`[_`][''<_>_</_>.Sort,'_`,_[''k.CellLabel.Constant,'_`[_`][''_`(_`).Sort,'_`,_[''GPlus:Map.Variable,'_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]]]],''k.CellLabel.Constant]],'_`[_`][''<_>_</_>.Sort,'_`,_[''heap.CellLabel.Constant,'_`[_`][''_`[undef/_`].Qid,'_`,_[''GPlus:Map.Variable,'_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]]]],''heap.CellLabel.Constant]]]],'_`[_`][''__.Sort,'_`,_['_`[_`][''<_>_</_>.Sort,'_`,_[''k.CellLabel.Constant,''Z:KItem.Variable,''k.CellLabel.Constant]],'_`[_`][''<_>_</_>.Sort,'_`,_[''heap.CellLabel.Constant,''DMinus:Map.Variable,''heap.CellLabel.Constant]]]]]],'_`[_`][''<_>_...</_>.Constant,'_`,_[''k.CellLabel.Constant,'_`[_`][''_=>_.Sort,'_`,_['_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]],''Z:KItem.Variable]],''k.CellLabel.Constant]],'_`[_`][''<_>_</_>.Sort,'_`,_[''heap.CellLabel.Constant,'_`[_`][''_=>_.Sort,'_`,_[''GPlus:Map.Variable,'_`[_`][''_`[_/_`].Qid,'_`,_[''DMinus:Map.Variable,''Z:KItem.Variable,'_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]]]]]],''heap.CellLabel.Constant]]]],'_`[_`][''_`(_`).Sort,'_`,_[''isVal.KLabel.Constant,''Z:KItem.Variable]],'klocation['"/home/hossein/Documents/KFram/Teachup/Launchbury/launchbury.k:34-35".String]].

And, in case you had difficulties finding the Ott rule I'm after
K'ification of, here it is:

 G : e --> D : z
 ------------------------------------------- :: var
 ( G , x |-> e ) : x --> ( D , x |-> z ) : z

Any idea now?

TIA,
--Hossein

P.S. As a heavy C++ metaprogrammer, for once when I saw the above
error message, I said to myself: Wow! So, there are tougher guys in
this world than C++? ;)

On 23 February 2012 16:58, Seyed H. HAERI (Hossein)

<hossein.haeri AT gmail.com> wrote:
> Hi there,
>
> My message below is waiting for approval because it's larger than
> 128K. This is due to its PDF attachment. In case you know Ott, please
> see the Ott source in the attachments instead. Hopefully, it won't be
> a lot of hassle to read through the Ott source for it's aimed to be a
> close ASCII transliteration of the operational semantics. I would
> appreciate it if you could help me.
>
> TIA,
> --Hossein
>
> On 23 February 2012 13:25, Seyed H. HAERI (Hossein)
> <hossein.haeri AT gmail.com> wrote:
>> Hi again,
>>
>> OK, now I'm stuck for the same basic reason, on a more complicated
>> example. See the attached PDF for Ott's output of the famous
>> (big-step) operational semantics of Launchbury for lazy evaluation.
>> Here is my attempt to model that so far:
>>
>> require /modules/substitution
>>
>> module LAUNCHBURY-SYNTAX
>>  syntax Val ::= "\\" #Id "." Exp [binder prec 100 latex "\lambda{#1}.{#2}"]
>>
>>  syntax Binding ::= #Id "=" Exp
>>  syntax Bindings ::= List{Binding, ","}
>>
>>  syntax Exp ::= #Id
>>              | Val
>>              | Exp #Id [strict(1) gather (E e)]
>>              | "let" Bindings "in" Exp
>> end module
>>
>> module LAUNCHBURY imports LAUNCHBURY-SYNTAX + SUBSTITUTION
>>
>>  syntax KResult ::= Val
>>
>>  configuration <k color = "green" multiplicity = "*"> $PGM:K </k>
>> <heap> .Map </heap>
>>
>>  rule <k> (\ Y:#Id.E':Exp) X:#Id => E'[X/Y] ... </k>
>>  rule <k> X:#Id => Z:Val ... </k> <heap> ... X |-> (_ => Z) ... </heap>
>> end module
>>
>> My very last rule above is my first unsuccessful attempt to model the
>> Var rule of the attached PDF. Upon kompilation of the above file,
>> Maude expresses its unhappiness about Z being used before being
>> introduced first. Whilst I think Maude is right, I don't seem to be
>> able to figure out how to tell K that: Z is what we get once we try
>> the evaluation of what X was bound to in the original heap with X's
>> binding removed. Here is another failed attempt:
>>
>>  rule <k> X:#Id ... </k> <heap> ... X |-> E:Exp ... </heap> => <k> Z
>> ... </k> <heap> D[X |-> Z] </heap>
>>       (<k> E ... </k> <heap> ... X |-> . ... </heap> => <k> Z:Val ...
>> </k> <heap> D:Map </heap>)
>>
>> This one fails with an error message that I can't decrypt:
>>
>> [ERROR]: Default terms accept open cells only for Bag cells.
>>  Term: <_>_</_>(heap,(.).Map,heap)
>>  Context:  -> __ -> _=>_ -> __ -> _=>_
>> Location:
>> /home/hossein/Documents/KFram/Teachup/Launchbury/launchbury.k:23-24
>>  Compilation phase: DEFAULT-TERMS
>> Aborting the compilation
>>
>> So, how do you guys do that? And, moreover, what's the story about
>> "default terms" and "Bag cells" here?
>>
>> 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/
>> --------------------------------------------------------------------------------------------------------------
>
>
>
> --
> --------------------------------------------------------------------------------------------------------------
>
> 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/
> --------------------------------------------------------------------------------------------------------------



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

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

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user