# Module Importing, Rules, Variables

We here learn how to include a predefined module (SUBSTITUTION), how to use it to define a K rule (the characteristic rule of lambda calculus), and how to make proper use of variables in rules.

Let us continue our `lambda.k`

definition started in the previous lesson.

The `requires`

keyword takes a `.k`

file containing language features that
are needed for the current definition, which can be found in the
k-distribution/include/kframework/builtin folder. Thus, the command

```
requires "substitution.k"
```

says that the subsequent definition of LAMBDA needs the generic substitution,
which is predefined in file `substitution.k`

under the folder
k-distribution/include/kframework/builtin. Note that substitution can be defined itself in K,
although it uses advanced features that we have not discussed yet in this
tutorial, so it may not be easy to understand now.

Using the `imports`

keyword, we can now modify LAMBDA to import the module
SUBSTITUTION, which is defined in the required `substitution.k`

file.

Now we have all the substitution machinery available for our definition.
However, since our substitution is generic, it cannot know which language
constructs bind variables, and what counts as a variable; however, this
information is critical in order to correctly solve the variable capture
problem. Thus, you have to tell the substitution that your lambda construct
is meant to be a binder, and that your `Id`

terms should be treated as variables
for substitution. The former is done using the attribute `binder`

.
By default, `binder`

binds all the variables occurring anywhere in the first
argument of the corresponding syntactic construct within its other arguments;
you can configure which arguments are bound where, but that will be discussed
in subsequent lectures. To tell K which terms are meant to act as variables
for binding and substitution, we have to explicitly subsort the desired syntactic
categories to the builtin `KVariable`

sort.

Now we are ready to define our first K rule. Rules are introduced with the
keyword `rule`

and make use of the rewrite symbol, `=>`

. In our case,
the rule defines the so-called lambda calculus *beta-reduction*, which
makes use of substitution in its right-hand side, as shown in `lambda.k`

.

By convention, variables that appear in rules start with a capital letter (the current implementation of the K tool may even enforce that).

Variables may be explicitly tagged with their syntactic category (also called
*sort*). If tagged, the matching term will be checked at run-time for
membership to the claimed sort. If not tagged, then no check will be made.
The former is safer, but involves the generation of a side condition to the
rule, so the resulting definition may execute slightly slower overall.

In our rule in `lambda.k`

we tagged all variables with their sorts, so we chose
the safest path. Only the `V`

variable really needs to be tagged there,
because we can prove (using other means, not the K tool, as the K tool is not
yet concerned with proving) that the first two variables will always have the
claimed sorts whenever we execute any expression that parses within our
original grammar.

Let us compile the definition and then run some programs. For example,

```
krun closed-variable-capture.lambda
```

yields the output

```
<k>
lambda y . ((lambda x . (lambda y . (x y))) y)
</k>
```

Notice that only certain programs reduce (some even yield non-termination,
such as `omega.lambda`

), while others do not. For example,
`free-variable-capture.lambda`

does not reduce its second argument expression
to `y`

, as we would expect. This is because the K rewrite rules between syntactic
terms do not apply anywhere they match. They only apply where they have been
given permission to apply by means of appropriate evaluation strategies of language
constructs, which is done using strictness attributes, evaluation contexts,
heating/cooling rules, etc., as discussed in the next lessons.

The next lesson will show how to add LAMBDA the desired evaluation strategies using strictness attributes.

Go to Lesson 3, LAMBDA: Evaluation Strategies using Strictness