In this chapter we try to answer the question: why did we use Prolog to develop the core of ProB, and in particular why do we use the commercial SICStus Prolog rather than an open-source alternative.
The short answer is that Prolog allows us to flexibly implement various specification formalisms as well as the analysis and verification tools that go along with it. At the same time, Prolog is very fast and SICStus Prolog is one of the fastest and most stable Prolog systems and allows access to more than 256 MB of heap even on 32 bit systems (important for model checking), and is easy to interate with other programming languages (so that the GUI does not have to be developed in Prolog).
cspm_trans('|'(X,_Y),tau,X).cspm_trans('|'(_X,Y),tau,Y).
The full operational semantics of CSP from Roscoe's book has been translated mostly one-to-one into Prolog rules (adding treatment for source location information,...).
2. Prolog is (one of) the most convenient languages to express program analysis (e.g., abstract interpretation or even dataflow analysis, see also last chapters of 2nd edition of the Dragon book), program verification (e.g., model checking), and program transformation (e.g., partial evaluation) in. Also, type inference and type checking are a "breeze" thanks to Prolog's unification.
3. Modern Prolog systems support a feature called "co-routining", also known as flexible computation rules or delay-declarations. These can be implemented by block-declarations or when-statements and they can stipulate conditions under which a Prolog goal should be expanded. For example, the following block declarations say that the goal less_than_equal should only be expanded when both of its arguments are known:
{{{
less_than_equal(X,Y) :- X=<Y. }}}
A nice aspect is that the block declarations do *not* influence the declarative semantics of a Prolog program, as we have the theorem that the declarative semantics of logic programs is independent of the selection rule. I believe this to be one of the "killer" feature of modern Prolog systems. We heavily use this in the ProB kernel to delay enumeration of values and to implement our own constraint solver over sets and relations. In my experience, this feature allows one to write much more declarative code than with traditional Prolog systems (an example is the transcription of Roscoe's operational semantics mentioned above), while often obtaining a dramatic increase in performance in generate-and-test scenarios.
4. Prolog is fast. This may be surprising to some, as Prolog sometimes has a reputation of being slow. On my laptop, SICStus Prolog can perfrom 33 Million logical inferences per second. As you see below, it can sometimes be faster than Java. Modern Prolog systems are well tuned and developed, and will outperform your own logical inference or unification mechanism by a considerable margin (I observed a factor of 10,000 between SICStus Prolog and the C implementation of a custom rule engine in a commercial product).
In summary, Prolog gives us both a flexible way to encode both the operational
semantics of many high-level formalisms (B, Z, CSP, ...) and various flexible
tools on top such as animation, type checking, model checking and refinement checking.
All of this comes with a respectable performance, despite the flexibility of the
approach.
There are of course still aspects with Prolog that, despite many years of research and development, are not ideal. Standardisation of Prolog and the libraries is not ideal (the ISO standard does not cover the module system for one). There is no standard static type checking tool.
Below is a short summary of some of the Prolog systems that to my knowledge are still being actively maintained (please email me corrections and additions).
SICStus:
* + Fast, good support * + Standalone binaries * + >256 MB Heap on 32 Bit systems * + C, Java, TclTk external interfaces, * + Good libraries (from Quintus) * + fast co-routines and constraint solving * - commercial product (with academic site licences available) * - no multi-threading
SWI
* + Actively maintained * + Large number of libraries and features * + Support for co-routines and constraint solving * - still slow
Ciao
* + comes with CiaoPP analyser for static analysis * + good module system * + relatively fast * + decent support for co-routines and constraint solving * - Long startup time
Gnu Prolog
* + good Constraint solving * - No co-routines * - limited features and libraries * - no BigInts
XSB Prolog:
* + Tabling * + Prolog facts can be used as efficient relational database * - non-standard built-ins (no print, ... quite ≠ from SWI, ...) * - no co-routines nor constraint solving * - no BigInts
Yap
* + fast * - no finite domain constraint solver * - no BigInts * - only C external language interface
LPA
* + good graphical tools, GUI generation, ... * - runs only Windows * - no modules * - no co-routines
BinProlog
* - no Bigints * - commercial
Other Prologs, I have not directly experimented with are: Visual Prolog and IF Prolog. It seems that maybe Yap and SWI are merging efforts. It would be nice to have a Prolog system with the features of SWI and the speed of YAP. This would be a serious (free) alternative to SICStus Prolog.
Below I have conducted a small experiment, to gauge the performance of various Prolog systems. I do not claim that this example is representative; it tests only a few aspects of performance (e.g., speed of recursive calls). I don't have the time to do a more extensive evaluation at the moment.
The benchmark is the Fibonacci function, written in the naive recursive way so as to quickly obtain a large number of recursive calls. The advantage is that the code can be easily transcribed into other programming languages. Below, I give you also a Python, Haskell and a Java version using BigInts. The benchmarks were run on a MacBook Pro Core2 Duo with 2.33 GHz. BinProlog does not have a demo licence for Mac; hence I had to run the Windows version in Parallels. LPA Prolog only runs on Windows; so it was also run using Parallels. Note, the purpose of the benchmark was to measure the performance of recursion. As such, I was trying to use the same datatypes on all platforms (BigInts). Also, note that this is actually not a typical Prolog "application", as no use is made of unification or non-determinism. But it is a good application for a functional programming language such as Haskell, Fibonacci being a pure function without side-effects.
Also, I do not claim that the benchmark shows that Prolog is faster than Java in general. My only claim is that, if an application is well suited to Prolog, its performance can be surprisingly good. I also have the feeling that Haskell has made great strides in performance recently, and that the Prolog community should be on its guard (so as not to be left behind).
{{{ System BigInts Fib(30) Fib(35) Java 1.5.0_16 NO (long) 0.020 0.231 GHC 6.10.1 yes 0.082 0.878 Yap 5.1.3 NO 0.193 2.112 SICStus 4.0.4 yes 0.240 2.640 Ciao 1.13.0 yes 0.312 3.461 BinProlog 11.38 NO 0.361 3.725 Java 1.5.0_16 yes 0.445 4.898 XSB 3.1 NO 0.456 5.064 Python 2.5.1 yes 0.760 8.350 Gnu 1.3.1 NO 1.183 13.139 SWI 5.6.52 yes 1.900 20.990 LPA 4.710 yes 1.736 36.250 }}}
The same table with only the BigInteger versions is: {{{ System BigInts Fib(30) Fib(35) GHC 6.10.1 yes 0.082 0.878 SICStus 4.0.4 yes 0.240 2.640 Ciao 1.13.0 yes 0.312 3.461 Java 1.5.0_16 yes 0.445 4.898 Python 2.5.1 yes 0.760 8.350 SWI 5.6.52 yes 1.900 20.990 LPA 4.710 yes 1.736 36.250 }}}
Note, that Gnu is the only system requiring tweaking of parameters: {{{ export TRAILSZ=200000 export GLOBALSZ=1500000 }}} Java with int rather than BigIntegers takes 0.016 s for Fib(30) and 0.163 s for Fib(35). Note that GHC Haskell seems to have received a big performance boost on this particular example (earlier versions of Haskell were on par with SICStus Prolog).
I also wanted to experiment with a Mercury version, but for the moment Mercury does not compile/install on my machine. Marc Fontaine has also written various Haskell versions of Fibonacci
Here are the various versions of Fibonacci:
Prolog Version: {{{ fib(0,1) :- !. fib(1,1) :- !. fib(N,R) :-
N1 is N-1, N2 is N1-1, fib(N1,R1), fib(N2,R2), R is R1+R2.
}}}
Python Version: {{{ def Fib(x):
if x<2:
return 1
else:
return Fib(x-1)+Fib(x-2)
}}}
Java Version with BigInteger: {{{ private static BigInteger ZERO = BigInteger.ZERO; private static BigInteger ONE = BigInteger.ONE; private static BigInteger TWO = new BigInteger("2");
public static BigInteger naiveFib(BigInteger x) {
if (x.equals(ZERO) ) return ONE;
if (x.equals(ONE) ) return BigInteger.ONE;
return naiveFib(x.subtract(ONE)).add(naiveFib(x.subtract(TWO)));
}
}}}
Haskell Version:
n == 0 = 1
Java Version with long rather than BigIntegers:
{{{
public static long fib(long xx) {
if (xx<2) return 1; else return fib(xx-1)+fib(xx-2); }
}}}
Below we test the startup times of some of the Prolog systems. Unfortunately, not all Prolog systems can easily be started as easily from the command-line as SICStus Prolog (e.g., --goal "GOAL." parameter and -l FILE parameter).
First, the following command takes 0.026 s real time (0.015 s user time) with SICStus Prolog 4.0.5 on the same system as above: {{{ time sicstus --goal "halt." }}}
For SWI Prolog 5.6.64 we get 0.015 s real time (0.008 s user time): {{{ time swipl -g "halt." }}}
For Ciao Prolog 1.13.0-8334 we get 0.271 s user time for "time ciao" and then typing halt (I found no easy way to provide goals on the command-line).
Now, take the file halt.pl with contents: {{{ main :- print(hello),nl,halt.
}}}
The following takes 0.028 seconds real time and 0.015 seconds user time. {{{ time sicstus -l halt.pl }}}
The following takes 0.204 seconds real time the first time, 0.015 seconds real time the second time: {{{ time swipl -c halt.pl }}}
The following takes 0.726 seconds real time, 0.648 seconds user time (after commenting out :- main.), i.e., 25 times slower than SICStus: {{{ time ciao -c halt.pl }}}