This modified version of the Marshall programming language accompanies
the paper the LICS 2018 paper "Computable decision-making on the reals and other spaces via partiality and nondeterminism" by Benjamin Sherman, Luke Sciarappa, Michael Carbin, and Adam Chlipala. The two example Marshall programs from the paper are found in examples/car_LICS.asd
and examples/roots_LICS.asd
. To use these libraries, run
#use "examples/car_LICS.asd";;
#use "examples/roots_LICS.asd";;
in the Marshall interpreter.
Marshall is a programming language for exact real arithmetic based on ideas from Abstract Stone Duality (ASD) and the construction of the Dedekind reals in ASD. See also Andrej Bauer's talk on Efficient computations with Dedekind reals.
The main idea of Marshall is that a real number x
is given as a Dedekind cut,
i.e., as a pair of predicates describing which numbers are smaller than x
and
which ones larger. For example, the sqrt
function is defined in Marshall as
let sqrt =
fun a : real =>
cut x
left (x < 0 \/ x * x < a)
right (x > 0 /\ x * x > a)
See example.asd
for more examples.
To compile Marshall you will need Ocaml, version 3.12 and the menhir parser generator.
Both are available through standard packaging systems on Linux distributions, and on MacOS X via opam. On Windows you might get away with Wodi -- we wish you good luck.
If you install the rlwrap
or ledit
command-line editing wrappers, Marshall will use
them automatically in the interactive mode.
Compilation should run smoothly or not at all. Type
./configure
make
The configure
command accepts standard autoconf options, see configure --help
.
The compiled executable is called marshall
and you can run it in place.
To install Marshall type
make install
This will install the Marshall exectuable in /usr/local/bin
unless you specified
a different location with configure
. You do not actually have to install Marshall
to run it.
There are examples in the example
subdirectory. It may be instructive to look at
prelude.asd
.
In etc/haskell
you can find a small Haskell implementation of real numbers that
somewhat follows the ideas of Marshall. It was implemented as part of a graduate course on
computable topology in 2009 at the Faculty of Computer Science and Informatics, University
of Ljubljana. Of particular help might be the notes etc/haskell/notes.tex
.
In theory Marshall can be compiled with the MPFR library, but this requires extra work. At the moment MPFR is not used by autoconf. Here are some obsolete instruction that may or may not work.
-
You need the prerequisites listed above.
-
You need the usual building tools, such as subversion, make, and gcc. Under Microsoft Windows you can get those by installing Cygwin.
-
You need camlidl, which is available in GODI as well.
-
You need MPFR, or through your package manager.
-
You need mlgmpidl. You should get the latest subversion version which includes some patches that we submitted. Check out mlgmpidl from subversion:
svn checkout svn://scm.gforge.inria.fr/svn/mlxxxidl/mlgmpidl
(Just in case, this repostitory includes the patch in mpfr.idl.patch
. But you
should not have to apply it if you get mlgmpidl from subversion.) Proceed with
installation of mlgmpidl.
-
TODO How to "register" it with ocamlfind?
-
To compile the bytecode version with Mpfr library, type in the
src
subdirectoryocamlbuild -use-ocamlfind marshall_mpfr.byte
To compile bytecode, native, and the documentation, type in the src
subdirectory
ocamlbuild -use-ocamlfind all.otarget