k-user AT lists.cs.illinois.edu
Subject: K-user mailing list
List archive
- 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.
- [[K-user] ] How to model combinator calculi?, Mike Stay, 07/21/2017
- Re: [[K-user] ] How to model combinator calculi?, Everett Hildenbrandt, 07/21/2017
- Re: [[K-user] ] How to model combinator calculi?, Mike Stay, 07/21/2017
- Re: [[K-user] ] How to model combinator calculi?, Mike Stay, 07/21/2017
- Re: [[K-user] ] How to model combinator calculi?, Mike Stay, 07/22/2017
- Re: [[K-user] ] How to model combinator calculi?, Christos Kloukinas, 07/22/2017
- Re: [[K-user] ] How to model combinator calculi?, Mike Stay, 07/22/2017
- RE: [[K-user] ] How to model combinator calculi?, Rosu, Grigore, 07/21/2017
- Re: [[K-user] ] How to model combinator calculi?, Mike Stay, 07/21/2017
- Re: [[K-user] ] How to model combinator calculi?, Everett Hildenbrandt, 07/21/2017
Archive powered by MHonArc 2.6.19.