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. |
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.
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 "~".
- 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.
Sigma Calculus Version 0.7 - S.M.Pericas
>> origin1 = [ x=0, mv_x=@(s)\(dx)
s.x := s.x + dx ]; >> origin1.x;
>> origin1.mv_x(1).x;
>> stack = [isempty = true,
>> stack.push(1).push(2).top;
>> fac = fix fac.\(n)if n==0 then
1 else n*fac(n-1); >> fac(5);
>> o = [retrieve=@(s1)s1,
>> o' = o.backup;
>> o'.retrieve;
>> exit; |
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] |
[KfoPer 99] Kfoury, A., and Pericas-Geertsen, S., "Type Inference
for Recursive Definitions", Logic in Computer Science (LICS) '99.