K code can be nested inside Markdown using annotated code blocks. Use the tag k to tell the compiler which blocks to select.

Inside .k files, C/Java-like comments are available.

k
// Single line comment
/* Multiline
comments */

Tutorial 1 --- LAMBDA

Author: Grigore Roșu (grosu@illinois.edu)
Organization: University of Illinois at Urbana-Champaign

Abstract

This file defines a simple functional language in K, called LAMBDA, using a substitution style. The explicit objective here is to teach some K concepts and how they work in the K tool, and not to teach λ-calculus or to argue for one definitional style against another (e.g., some may prefer environment/closure-based definitions of such languages).

Note that the subsequent definition is so simple, that it hardly shows any of the strengths of K. Perhaps the most interesting K aspect it shows is that substitution can be defined fully generically, and then used to give semantics to various constructs in various languages.

Note: K follows the literate programming approach. The various semantic features defined in a K module can be reordered at will and can be commented using normal comments like in C/C++/Java. While comments are useful in general, they can annoy the expert user of K. To turn them off, you can do one of the following (unless you want to remove them manually):
(1) Use an editor which can hide or highlight Markdown and conventional C-like comments; or
(2) Run kompile --debug <def>. Inside ./.kompiled-xxx/.md2.k/ you will find all the K code extracted from the markdown files as used for compilation.

Substitution

We need the predefined substitution module, so we require it with the command below. Then we should make sure we import its module called SUBSTITUTION in our LAMBDA module below.

k
module LAMBDA-SYNTAX
  imports DOMAINS-SYNTAX
  imports ID-SYNTAX

Basic Call-by-value λ-Calculus Syntax

We first define the syntax of conventional call-by-value λ-calculus, making sure we declare the lambda abstraction construct to be a binder, the lambda application to be strict, and the parentheses used for grouping as a bracket.

Note: Syntax in K is defined using the familiar BNF notation, with terminals enclosed in quotes and nonterminals starting with capital letters. K actually extends BNF with several attributes, which will be described in this tutorial.

Note: The strict constructs can evaluate their arguments in any (fully interleaved) order.

The initial syntax of our λ-calculus:

k
  syntax Val ::= Id
               | "lambda" Id "." Exp
  syntax Exp ::= Val
               | Exp Exp              [left, strict]
               | "(" Exp ")"          [bracket]

Integer and Boolean Builtins Syntax

The LAMBDA arithmetic and Boolean expression constructs are simply rewritten to their builtin counterparts once their arguments are evaluated. The annotated operators in the right-hand side of the rules below are builtin and come with the corresponding builtin sort. Note that the variables appearing in these rules have integer sort. That means that these rules will only be applied after the arguments of the arithmetic constructs are fully evaluated to K results; this will happen thanks to their strictness attributes declared as annotations to their syntax declarations (below).

k
  syntax Val ::= Int | Bool
  syntax Exp ::= "-" Int
               > Exp "*" Exp          [strict, left]
               | Exp "/" Exp          [strict]
               > Exp "+" Exp          [strict, left]
               > Exp "<=" Exp         [strict]

Conditional Syntax

Note that the if construct is strict only in its first argument.

k
  syntax Exp ::= "if" Exp "then" Exp "else" Exp    [strict(1)]

Let Binder

The let binder is a derived construct, because it can be defined using λ.

k
  syntax Exp ::= "let" Id "=" Exp "in" Exp [macro]
  rule let X = E in E':Exp => (lambda X . E') E

Letrec Binder

We prefer a definition based on the μ construct. Note that μ is not really necessary, but it makes the definition of letrec easier to understand and faster to execute.

k
  syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
               | "mu" Id "." Exp
  rule letrec F:Id X:Id = E in E' => let F = mu F . lambda X . E in E'
endmodule

LAMBDA module

k
module LAMBDA
  imports LAMBDA-SYNTAX
  imports DOMAINS

  syntax KResult ::= Val

β-reduction

k
  syntax Set ::= freeVars( Exp ) [function]
  rule freeVars( _ )            => .Set [owise]
  rule freeVars( V:Id )         => SetItem(V)
  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
  rule freeVars( if B then E1 else E2) => freeVars(B) freeVars(E1) freeVars(E2)

  syntax Id ::= freshVar(Id, Int, Set) [function]
  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi

  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]

  rule X:Exp [_ / _] => X [owise]
  rule X [V / X] => V

  rule (lambda Y . E) [_ / Y] => lambda Y . E
  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
    requires Y =/=K X andBool Y in freeVars(V)

  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])

  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])

  rule (if C then E1 else E2) [V / X] => if C[V / X] then E1[V / X] else (E2[V / X])

  rule (lambda X:Id . E:Exp) V:Val => E[V / X]

Integer Builtins

k
  rule - I => 0 -Int I
  rule I1 * I2 => I1 *Int I2
  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
  rule I1 + I2 => I1 +Int I2
  rule I1 <= I2 => I1 <=Int I2

Conditional

k
  rule if true  then E else _ => E
  rule if false then _ else E => E

Mu

k
  rule mu X . E => E[(mu X . E) / X]
endmodule