K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Of course, Robby, no bad feelings here.  In fact, you are helping us a lot.  
We had to do this anyway; it was on our "to do" list, but somewhere lower; 
now we are moving it higher.  At its core ("in theory"), K is very simple: 
context insensitive rewriting, with two types of rules, structural 
(unobservable in the transition system) and computational (observable).  The 
rest is definitional methodology, syntactic sugar and kompilation and krun 
options.

The overall design was driven by user needs.  Our users define languages like 
C, Java, Python, Ruby, Haskell, OCaml, etc., and most of them are interested 
in just plain execution.  So we made that as fast as we could.  Once in a 
while (very rarely) they are interested in exhaustive analysis of all 
behaviors, so we came up with the --search option.  However, in all these 
languages, for any given strict language construct c, its arguments first 
(potentially non-deterministically) evaluate and then the semantic rules for 
c are tried.  This is why we gave the heating/cooling rules priority (and 
also to keep the state-space smaller, for performance reasons).

But, you are right.  We lose behaviors right now in some cases, so we need to 
fix this.  Please continue to report such issues, they really help 
(particularly now, when we are doing the full transition of kompile to Java, 
because it is a good time to fix things and do them properly)!

Thanks,
Grigore



________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Robby Findler 
[robby AT eecs.northwestern.edu]
Sent: Wednesday, October 03, 2012 6:26 AM
To: Patrick Meredith
Cc: 
k-user AT cs.uiuc.edu
Subject: Re: [K-user] ambiguity & seqstrict

I'm sorry for this reply. I should have read ahead in my inbox!

Thanks Traian and Grigore! And just to be clear, I don't mean to
slight your design decisions or K or anything like that! I merely want
to understand what a K program does. (Altho, as you can see, my past
experience brings certain expectations to the table in ways that can
be unhelpful!)

Robby

On Wed, Oct 3, 2012 at 6:22 AM, Robby Findler
<robby AT eecs.northwestern.edu>
 wrote:
> What would this mean from the standpoint of the rules that seqstrict
> generates? (I understand the seqstrict annotation as a shorthand for
> generating rules, but I'm not sure that's right.)
>
> I thought it would generate a rule something like
>
>   A:KResult and B:BExp ~> everythingelse => A ~> (hole and B) ~> 
> everythingelse
>
> (apologies for my bad notation here "(hole and B)" is really something
> with a freezer around it and some substitutions and I'm not sure how
> to write "everythingelse" properly)
>
> Such a rule should fire!
>
> And indeed, if I just remove the 'and' shortcircuiting rule, then I do
> see the heating rule fire.
>
> Robby
>
> On Tue, Oct 2, 2012 at 10:36 PM, Patrick Meredith 
> <pmeredit AT gmail.com>
>  wrote:
>> Actually, that is a good point, and I'm not sure.  This is the behavior you
>> would normally want, but I'm not sure why it is working.  My best guess is
>> that seqstrict always plugs the heated value back in (cool) before it heats
>> the second value, deterministically, and that is where it is reducing your
>> short circuit (which doesn't care about the sort of the second argument).
>> This is what we'd want, so my guess is that is how it works.  I haven't 
>> used
>> seqstrict in any of my definitions.  Someone more knowledgeable can 
>> probably
>> confirm if I am correct.
>>
>> -Patrick
>>
>> On Oct 2, 2012 10:27 PM, "Robby Findler" 
>> <robby AT eecs.northwestern.edu>
>> wrote:
>>>
>>> But why should that preclude the heating/cooling from applying?
>>>
>>> Robby
>>>
>>> On Tue, Oct 2, 2012 at 10:26 PM, Patrick Meredith 
>>> <pmeredit AT gmail.com>
>>> wrote:
>>> > One definite issue is bool is in your syntax, so false and _ can be
>>> > applied
>>> > before any heating or cooling ever occurs.
>>> >
>>> > -Patrick
>>> >
>>> > On Oct 2, 2012 10:20 PM, "Robby Findler" 
>>> > <robby AT eecs.northwestern.edu>
>>> > wrote:
>>> >>
>>> >> Yes, but the left is already a KResult so the heating (or is it
>>> >> cooling?) rule should still fire. No?
>>> >>
>>> >> Robby
>>> >>
>>> >> On Tue, Oct 2, 2012 at 10:16 PM, Patrick Meredith 
>>> >> <pmeredit AT gmail.com>
>>> >> wrote:
>>> >> > Hi Robby,
>>> >> >
>>> >> > Replace seqstrict with strict.  Seqstrict is deterministic
>>> >> > sequentially
>>> >> > (left to right)
>>> >> >
>>> >> > -Patrick
>>> >> >
>>> >> > On Oct 2, 2012 7:12 PM, "Robby Findler" 
>>> >> > <robby AT eecs.northwestern.edu>
>>> >> > wrote:
>>> >> >>
>>> >> >> Hi all: I'm having trouble understanding a K program's behavior and
>>> >> >> I
>>> >> >> wondered if I could get some help.
>>> >> >>
>>> >> >> Here's the program:
>>> >> >>
>>> >> >> module IMP
>>> >> >>   syntax AExp ::= Int
>>> >> >>                 | "(" AExp ")"    [bracket]
>>> >> >>                 | AExp "/" AExp   [seqstrict, left]
>>> >> >>   syntax BExp ::= Bool
>>> >> >>                 | "(" BExp ")"    [bracket]
>>> >> >>                 | AExp "<=" AExp  [seqstrict]
>>> >> >>                 > BExp "and" BExp [seqstrict]
>>> >> >>
>>> >> >>   syntax KResult ::= Bool | Int
>>> >> >>
>>> >> >>   rule <k> I1:Int / 0 ...</k> => <k> "div0" </k>
>>> >> >>   rule I1:Int <= I2:Int => I1 <=Int I2
>>> >> >>   rule true and B:BExp => B
>>> >> >>   rule false and _ => false
>>> >> >> endmodule
>>> >> >>
>>> >> >>
>>> >> >> and here's the IMP program I run:
>>> >> >>
>>> >> >>    false and (1/0 <= 3)
>>> >> >>
>>> >> >> I would have expected it to produce two out comes ("div0" and false)
>>> >> >> because of the seqstrict annotation on the "and" production in the
>>> >> >> grammar.
>>> >> >> Specifically, I thought I'd get a heating/cooling rule that would
>>> >> >> apply
>>> >> >> to
>>> >> >> the program above that would move the (1/0 <= 3) expression to the
>>> >> >> front of
>>> >> >> the K cell, and the the 1/0 would move to the front and then I'd get
>>> >> >> the
>>> >> >> div0 result. But instead I get this:
>>> >> >>
>>> >> >> $ ../k/bin/krun --do-search --maude-cmd search x.impSearch results:
>>> >> >>
>>> >> >> Solution 1, state 0:
>>> >> >>
>>> >> >> <k>
>>> >> >>  false
>>> >> >> </k>
>>> >> >>
>>> >> >> I do see that if I remove the short-circuiting 'and' rule that I get
>>> >> >> the
>>> >> >> div0, but I cannot seem to get them both at once.
>>> >> >>
>>> >> >> tia,
>>> >> >> Robby
>>> >> >>
>>> >> >> _______________________________________________
>>> >> >> k-user mailing list
>>> >> >> k-user AT cs.uiuc.edu
>>> >> >> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>> >> >>
>>> >> >
>>> >> _______________________________________________
>>> >> k-user mailing list
>>> >> k-user AT cs.uiuc.edu
>>> >> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user