K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Mike,

I think you may find the `function` tag useful for your purposes:

```k
module SK-SYNTAX
  syntax Comb ::= "s" | "k"
  syntax Apply ::= "(" Term Term ")" [function]
  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
```

This tells the rewrite engine to apply all rules with the given KLabel as its 
top symbol to completion before taking a "normal" rewriting step.
If you're familiar with Maude, you may think of this like an "equational 
rewrite", though we don't perform any checks that the resulting equational 
system is confluent/terminating.
This achieves the "rewrite anywhere in the AST" behavior you're looking for.

Given the above code, I'm getting:

```
(((k k) s) k) => (k k)

(s ((k s) k)) => (s s)

((s s) ((k s) k)) => ((s s) s)
```

These look like the correct reductions to me given the SK-calculus.

The attribute `strict` adds "heating" and "cooling" rules to the K 
definition, which is why you see the "freezer..." stuff show up in your 
configuration.
This can be useful when you have a (potentially deep) expression language 
with variables/sub-expressions at the leaves that need to be evaluated in 
isolation or in the surrounding environment.
I think for the SK calculus you won't need that functionality.
Also, if you do want to mess with `strict` eventually, you may also consider 
`seqstrict`, which does the heating and cooling of the arguments, but 
specifically from left to right.

As for the parsing, you could try using a different KLabel (specified in the 
attributes).
On initial testing, the following seems to give the correct reductions again 
(I only ran it on the above examples):

```
module SK-SYNTAX
  syntax Comb ::= "S" [klabel(scomb)] | "K" [klabel(kcomb)]
  syntax Apply ::= "(" Term Term ")" [function]
  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
```

This essentially tells it to build a `scomb` (`kcomb`) AST node instead of an 
`S` (`K`) AST node at parse-time.

Hope this helps! Let me know if you have more questions,
Everett H.

On Fri, Jul 21, 2017 at 01:13:28PM -0600, Mike Stay wrote:
> 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.