(Update SICStus link) |
|||
| Line 1: | Line 1: | ||
[[Category:Developer Manual]] | [[Category:Developer Manual]] | ||
__NOTOC__ | __NOTOC__ | ||
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 [ | 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 [https://sicstus.sics.se/ 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, allows access to more than | 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, allows access to more than | ||
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, 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).
:- block less_than_equal(-,?), less_than_equal(?,-). less_than_equal(X,Y) :- X=<Y.
I believe this to be one of the "killer" features 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.
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:
SWI
Ciao
Gnu Prolog
XSB Prolog:
Yap
LPA
BinProlog
B Prolog
Other Prologs with which I have not directly experimented 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, a 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 types of data 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 since Fibonacci is 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
I have also recently tested B Prolog 7.4. It seems to perform marginally faster than SICStus (3 %), but does not support BigInts. 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:
fib :: Integer -> Integer fib n | n == 0 = 1 | n == 1 = 1 | otherwise = fib(n-1) + fib(n-2)
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. :- main.
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 and 0.015 seconds real time the second time:
time swipl -c halt.pl
The following takes 0.726 seconds real time and 0.648 seconds user time (after commenting out :- main.), i.e., 25 times slower than SICStus:
time ciao -c halt.pl