K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Mike,

There isn't a construct for saying "all the variables below this point are 
bound" as far as I know, but you can bind individual variables (eg. with 
lambda abstraction).
In the tutorial for LAMBDA (at <https://github.com/kframework/k> in directory 
k-distribution/tutorial/1_k/1_lambda/lesson_2/README.md) it talks about the 
`binder` attribute, which can be used to indicate that a construct binds the 
variables below (which builtin substitution pays attention to).

I can imagine a scheme like this:

```k
    syntax QuotedExp ::= "<<" Exp ">>"      [function]
                       | "quote" Id "." Exp [binder]

    rule << Exp >> => Exp                                 requires notBool 
hasVars(Exp)
    rule << Exp >> => quote findFirstVar(Exp) . << Exp >> requires 
hasVars(Exp)
```

You'll have to find out what `findFirstVar` and `hasVars` mean for your 
expressions (if your expression language only has a few constructs, it should 
be fine to build, but for any real-world language would be a pain).

Looking at lesson 9 of 1_k/5_types, it looks like there may have used to be a 
function called `freeVariables`, which would have been very useful here.
I can't seem to find it in any of the included builtin theories though, so 
perhaps support for it was lost along the way.

I'll ask around about it and let you know if I find anything else, but you 
may be stuck defining a term-traverser by hand.

Everett H.

On Mon, Jul 24, 2017 at 08:54:28AM -0600, Mike Stay wrote:
> I'd like to model the notion of a "quoted" program.  All variables
> inside a quotation context should be thought of as bound.  Is there a
> way to do that in K?
> -- 
> Mike Stay
> CTO, Pyrofex Corp.