Tutorial 3--- LAMBDA++

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

Abstract

This file contains an environment-based K semantic definition of LAMBDA++, an extension of the LAMBDA language (defined in Tutorial 1) with a callcc construct. The objective here is to further disseminate some of the features of the K framework, in particular to illustrate how popular environment-based and closure-based semantics can be defined in K.

For notational/kompilation/krun simplicity and to avoid OS errors, we continue to write LAMBDA and lambda as names for modules and program extensions, respectively, in the sequel.

To restrict the default program parser invoked by krun, namely kast, to only parse proper LAMBDA++ programs no matter what other syntactic constructs we add to Exp later on in the semantics, we put the actual program syntax in a module with the suffix -SYNTAX. This issue was discussed in more detail in Lesson 2 of this tutorial. In short, the parser generated by kompile to be used by kast will be by default built only based on the syntax in this module. Type kompile --help to see how to tell the parser which syntax to use.

k
module LAMBDA-SYNTAX
  imports DOMAINS-SYNTAX

Syntax

We move all the LAMBDA++ syntax here.

k
  syntax Val ::= Int | Bool
  syntax Exp ::= Val
// Basic lambda-calculus syntax
               | Id
               | "lambda" Id "." Exp
               | Exp Exp              [strict, left]
               | "(" Exp ")"          [bracket]
// Arithmetic
               > "-" Int
               | Exp "*" Exp          [strict, left]
               | Exp "/" Exp          [strict]
               > Exp "+" Exp          [strict, left]
               > Exp "<=" Exp         [strict]
// Other functional constructs
  syntax Exp ::= "if" Exp "then" Exp "else" Exp  [strict(1)] // Conditional
               | "let" Id "=" Exp "in" Exp [macro]           // Let binder
               | "letrec" Id Id "=" Exp "in" Exp [macro]     // Letrec
               | "mu" Id "." Exp                             // Mu
               | "callcc" Exp  [strict]                      // Callcc

One thing you may want to do, now that the entire syntax is in one place, is to play with precedences. This way, you can make kompile generate the parser you want for your programs, so that you won't have to put lots of parentheses in your programs.

k
endmodule


module LAMBDA
  imports LAMBDA-SYNTAX
  imports DOMAINS

Semantics

The next module contains the semantics of all the LAMBDA++ constructs, in the order in which their syntax was declared above.

The K Results

We should not forget to define the results of our computations. Here is a rule of thumb: whenever you have any strictness attributes, your should also define some K results. Or even simpler: always define your results! (unless you define a theoretical semantics, for analysis but not for execution purposes, you will need to define your results)

k
  syntax KResult ::= Val

Configuration

Since LAMBDA++ is such a simple language, its configuration is minimal for an environment-based semantics: it only contains the k cell, an environment cell, and a store cell. An environment binds variable names to locations, and a store binds locations to values.

k
  configuration <T color="yellow">
                  <k color="green"> $PGM:Exp </k>
                  <env color="blue"> .Map </env>
                  <store color="red"> .Map </store>
                </T>

Recall that $PGM is where the program is placed by krun after parsing.

Closures

In environment-based definitions of lambda-calculi, λ-abstractions evaluate to closures. A closure is like a λ-abstraction, but it also holds the environment in which it was declared. This way, when invoked, a closure knows where to find in the store the values of all the variables that its body expression refers to. To invoke a closure, we need to switch to closure's environment, then create a new binding for closure's parameter, then evaluate the closure's body, and then switch back to caller's environment.

k
  syntax Val ::= closure(Map,Id,Exp)

  rule <k> lambda X:Id . E => closure(Rho,X,E) ...</k>
       <env> Rho </env>
  rule <k> closure(Rho,X,E) V:Val => E ~> Rho' ...</k>
       <env> Rho' => Rho[X <- !N] </env>
       <store>... .Map => (!N:Int |-> V) ...</store>
  rule <k> X => V ...</k>
       <env>... X |-> N ...</env>
       <store>... N |-> V ...</store>

Environment Recovery

The environment-recovery computation item defined below is useful in many semantics, like it was above. It is so useful, that there are discussions in the K team to add it to the set of pre-defined K features.

k
  rule <k> _:Val ~> (Rho => .K) ...</k> <env> _ => Rho </env>

Arithmetic Constructs

Not much to say here. They have exactly the same semantics as in LAMBDA and IMP. Note that we let it in programmer's hands to check that the denominator of a division is different from zero. If a division-by-zero is issued, then completely non-deterministic result can happen depending upon what back-end one uses for the K tool. Currently, Maude is used and Maude gets stuck with a term of the form I /Int 0, but one should not rely on that. If you want to catch division-by-zero in the semantics, instead of letting the back-end do whatever it wants, you should add a side condition to the division rule.

k
  rule - I => 0 -Int I
  rule I1 * I2 => I1 *Int I2
  rule I1 / I2 => I1 /Int I2
  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

Let Binder

k
  rule let X = E in E':Exp => (lambda X . E') E

Letrec Binder

We define letrec in term of mu, whose semantics is below.

k
  rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E'

Mu

To save the number of locations needed to evaluate μ X . E, we replace it with a special closure which binds X to a fresh location holding the closure itself. This has the same effect as binding X to a reference that points back to the fixed-point.

k
  syntax Exp ::= muclosure(Map,Exp)
  rule <k> mu X . E => muclosure(Rho[X <- !N], E) ...</k>
       <env> Rho </env>
       <store>... .Map => (!N:Int |-> muclosure(Rho[X <- !N], E)) ...</store>
  rule <k> muclosure(Rho,E) => E ~> Rho' ...</k>
       <env> Rho' => Rho </env>

Callcc

For callcc, we need to create a new closure-like value which wraps both the remaining computation, and the environment in which it is supposed to be executed. Forget the environment, and you get a wrong callcc.

k
  syntax Val ::= cc(Map,K)
  rule <k> (callcc V:Val => V cc(Rho,K)) ~> K </k> <env> Rho </env>
  rule <k> cc(Rho,K) V:Val ~> _ =>  V ~> K </k> <env> _ => Rho </env>
endmodule