K-user mailing list

[Mike Stay <stay AT pyrofex.net>]

On Fri, Jul 21, 2017 at 2:24 PM, Everett Hildenbrandt
<hildenb2 AT illinois.edu>
 wrote:
> Hope this helps! Let me know if you have more questions,

I'm working towards implementing a concurrent combinator calculus.  As
an experiment, I've added a "par" combinator | to SKI, a bag of
processes (denoted by <p>...</p>), and a rule

   rule <p> ((| T:Term) U:Term) </p> => <p> T </p> <p> U </p>

that runs T and U concurrently.  Even though I've marked Apply as
functional, it's getting stuck.  The term

   ((| one) (((s ((s two) three)) four) five))

reduces to

   <T> <processes> <p> one </p> <p> ( ( ( ( s two ) three ) five ) (
four five ) ) </p> </processes> <k> empty </k> </T>

which is correct as far as it goes, but it should continue and reduce
( ( ( s two ) three ) five ) to ((two five) (three five)).


What am I doing wrong?


module SKIC-SYNTAX
  syntax Par ::= "|"
  syntax SComb ::= "s"
  syntax KComb ::= "k"
  syntax IComb ::= "i"
  syntax Comb ::= Par | SComb | KComb | IComb
  syntax Apply ::= "(" Term Term ")" [functional]
  syntax Term ::= Id | Comb | Apply
  syntax Empty ::= "empty"
endmodule

module SKIC
  imports SKIC-SYNTAX

  configuration
    <T>
      <processes>
        <p multiplicity="*"> . </p>
      </processes>
      <k> $PGM:Term </k>
    </T>

  rule
    <k> T:Term => empty </k>
    <processes> Ps => (Ps <p> T </p>) </processes>

  rule <p> (i X:Term) => X </p>
  rule <p> ((k X:Term) Y:Term) => X </p>
  rule <p> (((s X:Term) Y:Term) Z:Term) => ((X Z) (Y Z)) </p>

  rule <p> ((| T:Term) U:Term) </p> => <p> T </p> <p> U </p>
endmodule

-- 
Mike Stay
CTO, Pyrofex Corp.