k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] Rules with Premises of the Same Sort

From: "Seyed H. HAERI (Hossein)" <hossein.haeri AT gmail.com>
To: k-user AT cs.uiuc.edu
Subject: Re: [K-user] Rules with Premises of the Same Sort
Date: Wed, 22 Feb 2012 23:20:42 +0100
Authentication-results: mr.google.com; spf=pass (google.com: domain of hossein.haeri AT gmail.com designates 10.101.128.14 as permitted sender) smtp.mail=hossein.haeri AT gmail.com; dkim=pass header.i=hossein.haeri AT gmail.com
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user>
List-id: <k-user.cs.uiuc.edu>

Hi Brandon,

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

Yes, big-step operational semantics.

> while K is based on operational semantics.

Is there a "small-step" missing in your phrase above?

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

OK, things make more sense now. I'm happy I'm getting some K gravity. :)

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

[K-user] Rules with Premises of the Same Sort, Seyed H. HAERI (Hossein), 02/22/2012
- Re: [K-user] Rules with Premises of the Same Sort, Moore, Brandon Michael, 02/22/2012
  - Re: [K-user] Rules with Premises of the Same Sort, Seyed H. HAERI (Hossein), 02/22/2012
    - Re: [K-user] Rules with Premises of the Same Sort, Seyed H. HAERI (Hossein), 02/23/2012
      - Re: [K-user] Rules with Premises of the Same Sort, Seyed H. HAERI (Hossein), 02/23/2012
        
        Re: [K-user] Rules with Premises of the Same Sort, Seyed H. HAERI (Hossein), 02/24/2012
        
        Message not available
        
        Re: [K-user] Rules with Premises of the Same Sort, Traian Florin Șerbănuță, 02/24/2012