K-user mailing list

[Mike Stay <stay AT pyrofex.net>]

I'm having trouble defining the SK combinator calculus.

module SK-SYNTAX
  syntax Comb ::= "s" | "k"
  syntax Apply ::= "(" Term Term ")" [strict]
  syntax Term ::= Comb | Apply
endmodule

module SK
  imports SK-SYNTAX

  rule ((k X:Term) Y:Term) => X
  rule (((s X:Term) Y:Term) Z:Term) => ((X Z) (Y Z))
endmodule

If I leave off the [strict] annotation, then a term like
   (((k k) s) k)
never reduces to (k k).

If I have the [strict] annotation, then
   (s ((k s) k))
queues up s as a term to evaluate and stores the continuation as the next 
task.

If I add
   syntax KResult ::= Comb
then
   ((s s) ((k s) k))
 queues up (s s) as a term to evaluate and stores the continuation as
the next task.

Is there an annotation that says "reduce the argument as far as you
can, then move to the next one", or a way to say that rewrite rules
apply anywhere in an abstract syntax tree?

The other confusing thing was that if I defined the K combinator to be
a capital K, then the rewrite rules confused it with the K type.  Is
there a way to use capital K as a term in a rewrite rule?
-- 
Mike Stay
CTO, Pyrofex Corp.