Skip to Content.
Sympa Menu

k-user - [[K-user] ] How to model combinator calculi?

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] How to model combinator calculi?


Chronological Thread 
  • From: Mike Stay <stay AT pyrofex.net>
  • To: k-user AT lists.cs.illinois.edu
  • Subject: [[K-user] ] How to model combinator calculi?
  • Date: Fri, 21 Jul 2017 13:13:28 -0600
  • Authentication-results: illinois.edu; spf=pass smtp.mailfrom=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.



Archive powered by MHonArc 2.6.19.

Top of Page