psg-mit/marshall

Our modifications of the Marshall language for exact real arithmetic and examples

Dependencies

Binary dependencies: rlwrap, mpfr

brew install mpfr rlwrap

Installing

With Opam

opam install .

Manually

Opam dependencies: camlidl, menhir, num, mlgmpidl (depends on MPFR)

opam install camlidl menhir num mlgmpidl

To install Marshall type

./configure
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. The configure command accepts standard autoconf options, see configure --help.

Notes on compilation/installation

Whenever Makefile.am is edited, run

aclocal && autoconf && automake && ./configure

marshall's Issues

Smart splitting of intervals for integration

If I have

int x : [a, b], indicator (f x)

where f : real -> bool, then I should try to be smart and split up the [a,b] into close to areas where the transitions between tt and ff happen.

This should be able to be done with something along the lines of the Newton's approximation. I'm not sure how this can be made general, but it would help for integrals of the above form.

Use derivatives to speed up integration

Currently, integration approximates a function as constant on a given (hopefully small) interval.

If we can, may as well compute the derivative of the function (where we approximate the derivative as constant over the interval, passing in the interval value and getting an interval derivative out), and then use that linear interval approximation on the interval to get a finer estimate of the integral.

Bug with type polymorphism

This normal form is worrisome, with the F type variable left there. Even if perhaps that type variable doesn't matter, it's visually wrong.
The code comes from this definition:
https://github.com/psg-mit/marshall/blob/master/examples/cad.asd#L125-L128

# unit_cone;;
- : (real*real*real -> bool) -> bool = fun P : F -> bool => mkbool (forall x : [0.0, 1.] , forall x40 : [-1., 1.] , forall x24 : [-1., 1.] , 1. < x40 ^ 2 + x24 ^ 2 \/ is_true (P (x, x * x40, x * x24))) (exists x : [0.0, 1.] , exists x39 : [-1., 1.] , exists x23 : [-1., 1.] , x39 ^ 2 + x23 ^ 2 < 1. /\ is_false (P (x, x * x39, x * x23)))

Inexact representation of constants

Some constants, like 0.1, are not exactly representable as dyadic rationals. Currently, they are turned into dyadic intervals, which are hopefully very small. This ensures that answers are correct, but unfortunately, it means that we may sometimes endure nontermination. Ideally, the constant 0.1 should be represented as 1 / 10, since it does appear that integers are always represented exactly.

Use automatic differentiation instead of symbolic differentiation

Requires fusing the lower approximation code with diff.

Incorrect comparison of dyadic constants or something like that

# 0.1 - 0.1 < 1e-21;;
- : prop = False

This is obviously incorrect. I'm not sure what's going wrong.

Definitions are allowed to have free variables

This shouldn't typecheck

type Random A = integer -> integer * A;;
let runRandom (x : Random A) : A =
  (x i0)[1];;

because the A in runRandom is unbound.

let runRandom A (x : Random A) : A =
  (x i0)[1];;

Implement affine arithmetic?

Language tutorial

It would be great to have a tutorial for getting started programming in MarshallB.

Substitution in type expressions is not capture-avoiding

I just didn't implement it. Doesn't seem to be problematic for me yet, but of course it is incorrect!

0937e20#diff-4e8202e598fad8c5f8e0248b7fea312fR37

Issue with printing?

# let x = 4294967296 in x^2;;
- : real = 1.8446744074e19 +- 0.0
# let x = 4294967296 in x^2 - 18446744073709551616.;;
- : real = 0.0 +- 0.0
# 18446744073709551616. - 1.8446744074e19;;
- : real = -290448384. +- 0.0

Optimization to refinement for maximal approximations

Currently, if the lower approximation of a prop is True, then we just reduce the expression to True. Similarly, we should add the optimization such that if the lower approximation of a real is a Dyadic, then we just reduce to that dyadic.

Implicit function theorem

When the diff function in Newton.ml tries to compute the derivative with respect to a Dedekind cut that involves the variable being differentiated, it gives up.
If we want to compute the derivative of e with respect to x, and e is of the form

cut q
  left  f(q, x) < g(q, x)
  right g(q, x) < f(q, x) 

then, letting h(q, x) = g(q, x) - f(q, x), we can use the implicit function theorem to say that the derivative of e with respect to x is

- (diff h x) / (diff h q)

, where we use the interval approximation for q in the result there.

Inlining of Dedekind cuts not always sound

marshall/src/eval.ml

Lines 188 to 196 in 65f20eb

	match e1' with
	| S.Cut (x, i, p1, p2) ->
	hnf env (S.App (S.Lambda (x, S.Ty_Real, p2), e2))
	| _ ->
	list_bind (hnf env e2) (fun e2' ->
	match e2' with
	| S.Cut (x, i, p1, p2) ->
	hnf env (S.App (S.Lambda (x, S.Ty_Real, p1), e1'))
	| _ -> [S.Less (e1', e2')]

This is valid if the interval of the Dedekind cut is [-inf, inf], but if the interval is smaller, that needs to be incorporated in the inlining.

See how, e.g., sqrt pi is broken because of this.

Detect loops and halt

Sometimes, the refinement engine will take a step and not make any changes to the current expression being evaluated. In this case, it runs into an infinite loop. A better action to take would be to recognize this, and output that we ran into a loop, and the current expression which has reached the fixpoint.