Sigma Calculus Interpreter

Santiago M. Pericas-Geertsen
Boston University

Introduction

Sigma is an interpreter for the Sigma calculus with lambdas [AbaCar 96]. In addition to the pure object calculus, abstractions and applications as in the Lambda calculus were included in the source language, i.e. there is no need to use encodings to support these constructs. Sigma is implemented in SML/ML and the sources are available here . For instructions on how to install and run Sigma see Compiling and Installing the Interpreter .  

Using the Interpreter

Start the interpreter by typing sigma (if executing the interpreter outside the SML/NJ environment) or by typing Sigma.run() at the SML/NJ prompt. At the Sigma prompt (>>) you can type either a command to be executed or a term to be evaluated. Both commands and terms must be terminated by a semicolon. Commands are used to introduce definitions, read in a file with definitions, write out definitions to a file, etc. In what follows, <string> refers to a sequence of characters enclosed in double quotes.
 

x = a Binds to x the result of evaluating the term a; any previous value bound to x is discarded. 
read <string> Reads defintions from the file denoted by <string>.
write <string> Writes all the definitions in the current environment to the file <string>. 
eval a Evaluates the term a and prints the result with all macro definitions expanded.
exit Terminates execution of the interpreter.
Table 1. Description of Commands

There are two predefined identifiers, namely evaluation and type_inference, which are used to turn on/off evaluation and type inference. Both are initially set to true. To turn off type inference, for example, you may type:

 >> type_inference=false;

Turning off type inference is useful to evaluate untypable terms (specially those that require subtyping). The type inference algorithm used in Sigma is described in [KfoPer99]. Turning off evaluation is useful to see the types inferred for divergent terms. Notice that the Abadi and Cardelli Calculus (even without fix ) is a not a normalizing calculus, i.e. typable terms do not necessarily converge. Morever, the type system used in Sigma is based on recursive types and, as a result, every pure Lambda term (with or without a normal form) becomes typable.  

Syntax of Terms

Let x range over a set of variables and m over the set of integers. The syntax accepted by the interpreter, ranged by the meta-variables a,b and c, is summarized below. 
 a, b, c ::= x                    (Variables) 
           | m                    (Integers)
           | true                 (True)
           | false                (False)
           | [li=@(xi)bi]         (Object)
           | a.l                  (Selection)
           | a.l <= @(x)b         (Update)
           | \(x)b                (Abstraction)
           | b(a)                 (Application)
           | fix x.a              (Fix-Point)
           | (a)                  (Parenthesized Exp)
           | a + b                (Addition)
           | a - b                (Substraction)
           | a * b                (Multiplication)
           | a / b                (Division)
           | a > b                (Greater Than)
           | a < b                (Less Than)
           | a == b               (Equality)
           | not a                (Negation)
           | if a then b else c   (Conditional)

The syntactic extensions for method definition and method update when x (self) is not free in b are also supported. Thus, we can write [..., l=b, ...] and o.l := b if x is not a free variable in b . Variables are defined syntactically as sequences of an alphabetic character (including "'" and "_") followed by any number of alphanumeric characters. Integer constants, following ML's convention, are interpreted as negative if prefixed by the character "~". 

Semantics

For the pure Sigma calculus (no lambdas) evaluation of terms is based on the operational semantics described in [AbaCar 96]. For the Lambda calculus fragment, evaluation proceeds according to the call-by-value semantics. Method names are not forced to be distinct; if an object contains more than one method with the same name, the first from the left is chosen as a result of an invocation.
 
Primitive operations are always eager with respect of their arguments and work on the expected types. That is, arithmetic functions and ordering predicates work on intergers and equality (==) works on both integers and booleans. Finally, if-then-else always evaluates its first argument (of type boolean) and exactly one of the other two (which must be of the same type if type inference is turned on).

Definitions (i.e. bindings) are carried throughout the evaluation process in order to print meaningful results. The eval command can be used to expand any definitions in the final result of an evaluation.  

Compiling and Installing the Interpreter

Open the tar file in a new directory by typing gunzip -cd sigma.tar.gz | tar xvf -   at your shell prompt. Edit the file sources.cm and set the paths to library files ml-yacc-lib.cm and smlnj-lib.cm . Start SML/NJ by typing sml-cm and then compile the sources by calling CM.make(). If the compilation succeeds then you can start running the interpreter by typing Sigma.run(). You can also generate an SML/NJ image that can be executed without running sml-cm first. An SML/NJ image can be generated as follows:

 - SMLofNJ.exportFn("sigma", Sigma.exportSigma);

Next, you may want to install a shell script to execute the SML/NJ runtime on the image you created. The procedure varies from one installation to the other. This is the script file I use to run sigma on my SGI running IRIX 6.5:

 # Run the sigma interpreter on quasar.bu.edu
 exec /usr/local/sml/bin/.run/run.mipseb-irix5
      @SMLload=/usr/people/local/bin/sigma.mipseb-irix

Upon startup, Sigma reads and loads the definitions found in the file $HOME/.sigma . You can use this file to define your initial environment and/or to change the default values for the identifiers evaluation and type_inference.

Sample Session

Sigma Calculus Version 0.7 - S.M.Pericas 

>> origin1 = [ x=0, mv_x=@(s)\(dx) s.x := s.x + dx ]; 
[x=0, mv_x=@(s)\(dx)s.x := s.x + dx] : u(t0)[x:int, mv_x:int -> t0^]

>> origin1.x; 
0 : int

>> origin1.mv_x(1).x; 
1 : int

>> stack = [isempty = true,
            top = @(s)s.top,
            pop = @(s)s,
            push = @(s)\(x)((s.pop := s).isempty := false).top := x];
[isempty=true, top=@(s)s.top, pop=@(s)s, push=@(s)\(x)s.pop := s.isempty := false.top := x] : u(t1)[isempty:bool, top:t0, pop:t1^, push:t0 -> t1^]

>> stack.push(1).push(2).top;
2 : int

>> fac = fix fac.\(n)if n==0 then 1 else n*fac(n-1);
\(n)if n == 0 then 1 else n * fac(n - 1) : int -> int

>> fac(5);
120 : int

>> o = [retrieve=@(s1)s1,
        backup=@(s1)s1.retrieve := s1];
[retrieve=@(s1)s1, backup=@(s1)s1.retrieve := s1] : u(t0)[retrieve:t0^, backup:t0^]

>> o' = o.backup;
[retrieve=o, backup=@(s1)s1.retrieve := s1] : u(t0)[retrieve:t0^, backup:t0^]

>> o'.retrieve;
o : u(t0)[retrieve:t0^, backup:t0^]

>> exit;

Sample files

Movable Points From section 6.5.1 in [AbaCar96]
Backup Methods From section 6.5.2 in [AbaCar 96]
Object-Oriented Natural Numbers From section 6.5.3 in [AbaCar 96]
Polymorphic Stacks From section 1 in [KfoPer99]

References

[AbaCar 96]  Abadi, M., and Cardelli, L., "A Theory of Objects", Monographs in Computer Science, Springer-Verlag, New York, 1996.

[KfoPer 99]   Kfoury, A., and Pericas-Geertsen, S., "Type Inference for Recursive Definitions", Logic in Computer Science (LICS) '99.