K-user mailing list

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

Interesting that you mention this, Mike, because this is a HW exercise in my 
PL design course:

https://github.com/kframework/k/tree/master/k-distribution/tutorial/1_k/1_lambda/lesson_8/exercises/SK-combinators

Since I know you are not a student taking a PL class, I can send you the 
solution :) I will do it in a private message; it may need to be updated to 
work with K 4.0, though, because the last time I used it was with K 3.6.

Grigore



________________________________________
From: Mike Stay 
[stay AT pyrofex.net]
Sent: Friday, July 21, 2017 2:13 PM
To: 
k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] How to model combinator calculi?

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.