UMA Forum is a logic programming language based on linear logic. Actually, it is an implementation of a subset of Dale Miller's Forum Specification Language developed at the University of Málaga (UMA). UMA Forum is part of a research project concerning linear logic, logic programming, object orientedness and concurrency. Being a research programming language, most of UMA Forum features are subject to change; although it intends to be an efficient implementation of a large portion of Forum.
Currently, the main differences between UMA Forum and Forum are:
This means that UMA Forum is not as well-suited as Forum to support abstractions and higher-order programming; but it could support these features in a future. In spite of this, UMA Forum retains a large amount of expressiveness from linear logic.
The main contribution of UMA Forum is a new stack-based resource management system based on the Lolli resource management system, previously developed by Iliano Cervesato, Frank Pfenning and Joshua S. Hodas. The key idea of the new resource management system is that linear logic sequent contexts (i.e. logic programs and goals) can be manipulated as stacks, just as in hereditary Harrop formula based languages like lambda Prolog. In particular, the UMA Forum resource management system represents sequent contexts as stacks instead of multisets, replacing costly union and intersection multiset operations by simple, inexpensive push and pop stack operations. Similarly to the single data structure used in the Lolli implementation, clause order (an important topic in a logic programming language execution model) is preserved by using a single stack to store both linear and classical clauses. This new stack-based approach to resource management simplifies the implementation, providing an efficient linear logic proof search strategy at a very low cost. In addition, the single formula identifier used in the Lolli system is no longer needed. As the original Lolli resource management system, the new UMA Forum system can be easily applied to the implementation of linear logic theorem provers and programming languages, either single or multiple-conclusion. On the other hand, the current UMA Forum resource management system is not complete in the sense it manages additive truth (i.e. top) through backtracking. It will be extended to manage top soon.
UMA Forum is written in (fairly standard) Prolog, so all you need is a Prolog implementation. I have used SICStus Prolog 3 #5 (commercial) under Unix and BinProlog 5.75 (free, by Paul Tarau) under Windows 95/NT and Unix.
It should also be possible to use another Prolog implementation with little or no change.
*** Note to BinProlog 5.75 users:
I have experienced some problems with BinProlog
dynamic predicates. In particular, the interpreter
switches do not switch well. For example, the user command
eager switches to the eager proof search; but
sometimes it does not. To solve this, simply repeat the switching
user command until the switch is accomplished. This problem does
not occur under SICStus Prolog 3 #5.
The current release of UMA Forum is version 0.1. The files comprising the UMA Forum version 0.1 distribution are contained in the compressed archive umaforum01.tar.gz. To install UMA Forum version 0.1 simply copy this file onto any directory and then ungizp and untar it as follows:
$ ungzip umaforum01.tar.gz$ sicstus
?- [forumsu].
?- forum.
$ bp
?- [forumbu].
?- forum.
Alternatively, you can compile the files to obtain better performance. For example, under SICStus Prolog:
?- fcompile([sicstus_unix,forum]).
?- load([sicstus_unix,forum]).
?- forum.
In any case, after entering the goal forum you will see the banner and prompt below:
UMA Forum 0.1Now you can enter user commands to execute and goals to solve.
UMA Forum is a small but expressive programming language based on a few basic concepts; namely modules, operator declarations, clauses and predefined predicates. Most of its lexical elements are borrowed from Prolog, including variable and functor names, allowed symbols and comments. The anonymous variable _ is also supported (and encouraged through singleton variable warnings). Formal syntax of UMA Forum is available as a BNF-style grammar.
UMA Forum code is organized into modules. A module is a container of operator declarations and clauses. Be aware that real modular programming is not supported yet. UMA Forum modules are mainly intended to distinguish loaded from used clauses. A loaded module is just a module which has been (re)consulted and stored in memory. A used module is a loaded module whose clauses will be used along the proof search of a goal.
As an example, consider a file lists containing the two modules shown below (a source file can contain more than one module):
module one. infix (::) : 400. append(nil,Y,Y). append(X::Xs,Y,X::Z) <= append(Xs,Y,Z). module two. length(nil,0). length(_::Xs,N1) <= length(Xs,N) <= N1 is N+1.
Now, load both modules by reconsulting the file lists:
Forum> [lists].and try to solve the goal
Forum> append(X,Y,a::b::c::nil).UMA Forum will respond
no solution
since modules one and two are loaded, but not used. Now, use module one as follows: Forum> use(one).Since the clauses defining predicate append are visible, the previous goal can be solved
Forum> append(X,Y,a::b::c::nil). X = nil Y = a::b::c::nil -> X = a::nil Y = b::c::nil -> X = a::b::nil Y = c::nil -> X = a::b::c::nil Y = nil -> 4 solutions. no more solutions.
Contrary to most logic programming languages, successive solutions are obtained typing intro, while typing ';' halts proof search. On the other hand, module two remains loaded, but it is not used, so a goal like
Forum> append(X,Y,a::b::c::nil) x length(X,Lx) x Lx<3.cannot be solved. To solve it, both modules must be used
Forum> use(two).Hence, by using certain loaded modules you decide the actual logic program used to solve a given goal. This simple mechanism is particularly useful in the presence of linear clauses.
UMA Forum supports user defined operators. Operator declarations include position (prefix, infix and postfix), associativity (left, right and non-associative) and precedence level (1..1200, being 1 the highest and 1200 the lowest). As an example, consider the operator declarations below:
prefix pre : 700. % prefix operator declaration infixl il : 750. % infix left associative operator declaration infixr ir : 750. % infix right associative operator declaration infix i : 750. % infix non associative operator declaration postfix post : 800. % postfix operator declaration
In addition to user defined operators and connectives, UMA Forum has the following predefined operators:
\ : , = \= == \== =..
< =< > >= + - * /
mod is . []
The precedence level of the predefined operators and its semantics are inherited from the underlying Prolog system (except for '\' and ':', standing for abstraction and operator declaration respectively). Predefined operators and connectives cannot be redeclared.
UMA Forum clauses are freely generated from the linear logic asynchronous connectives. The ASCII rendering of these connectives is shown in the table below.
| Linear Logic | ASCII |
|---|---|
| additive true | top |
| multiplicative false | bot |
| multiplicative disjunction | # |
| additive conjunction | & |
| linear implication | -* , *- |
| intuitionistic implication | => , <= |
| why not exponential | ? |
| universal quantifier | forall |
On the other hand, the level of precedence of these connectives from higher to lower is:
| Connective | Precedence Level |
|---|---|
| top, bot | 1 |
| & | 550 |
| # | 600 |
| -*, => | 650 |
| *-, <= | 750 |
UMA Forum clauses are implicitly universally quantified and must be followed by a full stop. Examples of syntactically valid UMA Forum clauses are:
p(s(X)) # q(s(s(Y))) *- p(X) & q(s(X)) <= q(Y). goal(G) # s(on)*- s(off) -* G. go <= forall X \ forall Y \ p(x) => q(y).
Note that the universal quantifier forall and the abstraction '\' are not supported yet; but they are reserved.
Linear logic synchronous connectives are supported through second-order predicates as well. Refer to the UMA Forum module sync.
UMA Forum has the following predefined predicates:
/2
>=/2
\=/2
\==/2
arg/3
atomic/1
atom/1
copy_term/2
float/1
functor/3
ground/1
integer/1
is/2
name/2
nonvar/1
number/1
printf/1
printf/2
read/1
var/1
Except for printf/1 and printf/2, predefined predicates are taken from the underlying Prolog implementation, so their documentation is available in any Prolog manual or textbook. The predicate printf/2 is modelled after the C printf() standard output function, and works as follows:
printf(format_string,list_of_terms)The format string contains plain characters, escape sequences and format specifiers. Plain characters are written to the current output stream "as is". Escape sequences are formed by a backslash '\' followed by one of the plain characters below:
| character | written as |
|---|---|
| \n | new line |
| \t | tabulate |
| \\ | \ |
| \" | " |
Format specifiers are formed by a percentage symbol '%' followed by a plain character. The ith format specifier affects the way the ith term of the list of terms is written in the current output stream as follows:
| format specifier | written as |
|---|---|
| %w | built in predicate write/1 |
| %d | built in predicate display/1 |
| %q | built in predicate writeq/1 |
| %s | built in predicate put/1 (term must be a list of characters) |
The printf/1 predicate is similar to printf/2, but it has no list of terms attached, and hence its format contains no format specifier.
Following the prompt Forum> you can enter either a user command to be executed or a goal to be solved. Any UMA Forum term not being a user command is considered to be a goal.
User commands are classified into three categories: configuration commands, module commands and miscellaneous commands. These are described below.
| Command | Description |
|---|---|
| lazy | sets lazy proof search; i.e. the stack-based resource management system is applied, avoiding backtracking through context splits |
| eager | sets eager proof search; i.e. the resource management system is not active but the interpreter backtracks through all possible context splits. |
| showtime | shows execution time of every solution founded. |
| hidetime | execution time is not shown. |
| trace | displays the sequent before applying the next inference rule. |
| notrace | switchs off tracing. |
| setedit(name) | sets name as default editor command. |
| switches | lists current switches. |
| reset | resets the UMA Forum interpreter to its initial state. First default settings are taken, then the configuration file forum.ini is read to complete the initial configuration of the interpreter, overriding any default setting. |
| Command | Description |
|---|---|
| [file,...] | reconsults the source files [file,...], loading the contained modules. |
| modules | lists the currently loaded modules. |
| use(name) | the clauses contained in module mame will be used to solve any goal. This way, you can set the logic program currently used. |
| unuse(name) | the clauses contained in module name will not be used to solve a goal. This way, you can set the logic program currently used. |
| uses | lists currently used modules; i.e. the current logic program. |
| delete(name) | deletes module name from memory. |
| list(name) | lists contents of module name. |
| listing | lists contents of all modules. |
| edit(name) | edits the source file containing module name. The actual editing command involved depends on the value of setedit. |
| edit | edits most recently reconsulted source file. |
| Command | Description |
|---|---|
| dir | lists current directory contents. |
| system(cmd) | invokes system command cmd. |
| halt | halts the UMA Forum interpreter, returning control to the Prolog environment. |
| help | shows a help screen. |
Both eager and lazy proof search strategies are supported in order to compare the performance of the new resource management method. The examples below are solved in a few milliseconds by the lazy proof search, while they take minutes or even hours to complete when using the eager proof search, clearly showing the appropriateness of the method.
tensor
switch1
perm1
perm2
yale
urn
pcumb
paths1
paths2
fold
The source code of these and other examples is contained in the distribution archive.