The Jivaro head reduction machine |
Jivaro is a small evaluator for the λc-calculus, an extension of λ-calculus with control operators. Inside the Jivaro toplevel, you can build and evaluate programs written in the λc-calculus, while defining new instructions and testing them interactively. Jivaro can also be used in batch mode to compile source files and build libraries, or to inspect the contents of compiled files.
Jivaro is copyright © 2009 Alexandre Miquel.
Jivaro is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or any later version.
You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/.
Jivaro is distributed on the author's web page at
http://perso.ens-lyon.fr/alexandre.miquel/jivaro/
The Jivaro head reduction machine has been designed and written by Alexandre Miquel (Alexandre.Miquel@{ens-lyon.fr|pps.jussieu.fr}).
The λc-calculus has been introduced by Jean-Louis Krivine to extend the theory of realizability to classical logic. The idea of enriching λ-calculus with control primitives comes from Matthias Felleisen, and its connection to classical logic is due to Timothy Griffin. Finally, the λ-calculus itself is the great invention of Alonzo Church.
Usage: jivaro [options …] file …
where options are:
Anonymous arguments that appear in the command line are treated as file arguments of -include or -load options depending on their file extension: .lc (lambda-calculus) for source files, .lco (lambda-calculus object) for compiled files.
At startup time, an initialization file of primitive definitions is automatically loaded unless the option -no-init is given. The default location of this file (that can be overriden with option -init) is $JIVARO/init.lco, where $JIVARO is the installation directory of Jivaro. When Jivaro is run in batch mode only using -compile and/or -dump options, no initialization file is loaded.
A comment is introduced by the two-character sequence (* and terminated by the two-character sequence *). Comments can be nested, but are never parsed inside string literals. A comment is lexically treated as a blank.
An identifier (ident) is any non-empty sequence of characters that contains no space, no delimiter (parentheses, square brackets and curly braces), no backslash, no semi-colon and no double quote. As a special case, a non-empty sequence of digits possibly preceded by a plus (+) or minus (-) sign is not considered as an identifier, but as an integer literal.
An integer literal (int) is any non-empty sequence of digits possibly preceded by a plus (+) or minus (-) sign.
A string literal (string) is any sequence of printable characters surrounded by double quotes ("). As usual, double quote (") and backslash (\) need to be escaped using a backslash within a string literal, thus being written \" and \\. Other characters can be accessed via the escape sequences \n (newline), \r (carriage return), \t (tabulation), \b (bell), etc.
Reserved tokens are ; (semicolon), ;; (double semicolon), = (equal) and \ (backslash, for the λ). The character sequences Define, Environ, Eval, Extern, Help, Include, Load, On, Off, Print, Quit, Reset and Save are treated as keywords when involved in the formation of a command, but one can still use them as regular identifiers in terms.
Terms of the λc-calculus are typed using the following BNF:
|
|
Application is left-associative and has higher precedence than abstraction.
Each command starts with a capitalized keyword followed by zero, one or several arguments and is terminated by a double semicolon (;;).
defines a new instruction ident as an alias for the term term.
Note that defined instructions are only unfolded when they appear in head position, never in argument position. This design choice may cause some misunderstandings. For instance the sequence of commands
Define foo = 100 ;; Eval int_succ ; foo ; print ; stop ;;
is incorrect, since the primitive int_succ expects an integer literal on the top of the stack, not an instruction. Rule of the thumb: never use Define to define aliases for int or string literals. Instead, do:
Define foo = int 100 ;; (* same as \x x 100 *) Eval foo ; int_succ ; print ; stop ;;
(On the other hand, string and integer literals are handled correctly when they are bound to an ident using a λ-abstraction.)
defines a new instruction ident that takes n arguments on the top of the stack and binds them to the identifiers ident1 ⋯ identn before evaluating the term term. This command merely acts as the command
Define ident = \ident1 ⋯ \identn term ;;
except that the defined constant ident is not unfolded when it is evaluated in a stack containing less than n elements.
lists all the symbols that are declared in the current environment.
evaluates term term in an empty stack.
evaluates term term in a stack containing n terms term1 ⋯ termn.
defines a new instruction ident as an alias for the internal primitive string.
displays a help message on topic, where topic is one of Syntax, Commands or one of the commands Define, Environ, Eval, Extern, Help, Include, Load, Print, Quit, Reset or Save.
performs a textual inclusion of file string in the evaluator.
loads a set of declarations from a binary object file string. Each declaration of a symbol in the file silently overwrites the (possibly) existing declaration of this symbol in the current environment.
prints the declaration of instruction ident.
exits the evaluator. This command has the same effect as Control-D.
resets the environment to its initial state. All the declarations of symbols that were not already present in the initial state are lost.
saves the current environment in the object file string.
Evaluation implements head reduction, a.k.a. the standard (or normal) strategy of the λ-calculus. At each evaluation step, the evaluated process consists of a term called the head in front of a stack formed by zero, one or several terms, called the arguments. Evaluation proceeds depending on the shape of the head:
Note that instructions that have been introduced using Define (4.1) are only unfolded when coming in head position. Using Define to introduce an alias for an integer or string literal is in general a mistake. See the discussion about this point in 4.1. On the other hand, string and integer literals are handled correctly when they are bound to an ident using a λ-abstraction.
The Jivaro head reduction machine comes with a number of primitives that can be bound to instruction names using the command Extern (4.4). Many instructions are bound to primitives in the initialization file .init.lco. Primitives are listed using the presentation:
prim_name * input args // output head * output args (short textual description)
The head is separated from its arguments using an asterisk (*) rather
than using a semicolon (;) for better readability.
callcc * obj // obj * cont (call obj with current continuation cont)
stop * // stop * (stop evaluation)
Primitives that implement arithmetic operations take one or two int argument(s) on the top of the stack, plus an object obj the result of the operation is passed to.
int_neg * int ; obj // obj * int (opposite)
int_succ * int ; obj // obj * int (successor)
int_pred * int ; obj // obj * int (predecessor)
int_plus * int ; int ; obj // obj * int (addition)
int_minus * int ; int ; obj // obj * int (subtraction)
int_mult * int ; int ; obj // obj * int (multiplication)
int_div * int ; int ; obj // obj * int (Euclidian division)
int_mod * int ; int ; obj // obj * int (Euclidian remainder)
Primitives that implement arithmetic comparisons take one or two int
argument(s) on the top of the stack, plus two objects obj1 and
obj2 that respectively represent the `then' and `else' branches of
the conditional.
When the test succeeds (resp. fails), obj1 (resp. obj2)
comes into head position.
int_null * int ; obj1 ; obj2 // obj1|2 * (nullity)
int_eq * int ; int ; obj1 ; obj2 // obj1|2 * (equality)
int_ne * int ; int ; obj1 ; obj2 // obj1|2 * (inequality)
int_le * int ; int ; obj1 ; obj2 // obj1|2 * (less than or equal)
int_lt * int ; int ; obj1 ; obj2 // obj1|2 * (less than)
int_ge * int ; int ; obj1 ; obj2 // obj1|2 * (greater than or equal)
int_gt * int ; int ; obj1 ; obj2 // obj1|2 * (greater than)
int_print * int ; obj // obj * (print int)
int_read * obj // obj * int (read int)
int_userfun * string ; int ; obj // obj * int (pass to obj the image of int argument by the user function of name string. User is prompted to give values of the function at first request)
string_make * int ; int ; obj // obj * string (string creation)
string_length * string ; obj // obj * int (string length)
string_get * string ; int ; obj // obj * int (successor)
string_sub * string ; int ; int ; obj // obj * string (substring)
string_concat * string ; string ; obj // obj * string (concatenation)
string_eq * string ; string ; obj1 ; obj2 // obj1|2 * (equality)
string_ne * string ; string ; obj1 ; obj2 // obj1|2 * (inequality)
string_le * string ; string ; obj1 ; obj2 // obj1|2 * (less than or equal)
string_lt * string ; string ; obj1 ; obj2 // obj1|2 * (less than)
string_ge * string ; string ; obj1 ; obj2 // obj1|2 * (greater than or equal)
string_gt * string ; string ; obj1 ; obj2 // obj1|2 * (greater than)
string_print * string ; obj // obj * (print string)
string_read * obj // obj * string (read string)
print * obj1 ; obj2 // obj2 * (print obj1 on standard output)
flush * obj // obj * (flush standard output)
This document was translated from LATEX by HEVEA.