Preconditions and postconditions of functions in the Math library

First, this is meant to be a discussion. So please, if you have an opinion or question or anything else, please respond.

This is stemming from recent discussions on the stan-dev/math repo. There are discussions about removing error checking of functions for speed. The latest discussion is here: https://github.com/stan-dev/math/issues/1468.

I realized that we haven’t really written out some of the guiding principles for the Math library. And what may have held in the past may not hold now.

I think it helps to think about the preconditions and postconditions of all the Stan Math functions. (This is design by contract terminology used in software development.) For each of the Math functions, we’ve been operating this way:

Preconditions

  • None. Well… to be more specific:
    • Input must match the function signature. This is given to us for free by C++.
    • If using autodiff variables, they must be properly constructed and still on the autodiff stack.

Postconditions

  • If the function did not throw an exception, the result is valid and can be trusted.
  • If the function threw an exception, the autodiff stack isn’t meant to be in a good state.

And some general principles:

  • since the main client is Stan, propagate an error message as soon as we can with a sensible message so the user knows what’s going on
  • when there’s an error, we’re already in an exceptional case and it’s worth taking the time to write a reasonable message
  • be as fast as we can.

In the past, we’ve tried to track down which error checks took a long time and we couldn’t find simple ones that do in a practical use case. Once we’re using the autodiff stack and doing anything real, the error checks don’t matter so much in execution time, but they really help from a user’s point of view.


So… that’s where we’re at now. If a function doesn’t throw, you can assume it works. There are a couple edge cases to this: the standard template library doesn’t throw and returns NaN.

There’s been talk about removing some of the checks for the sake of speed. My take:

  1. I don’t know how much speed we’ll gain. But we should time it and see. If it’s significant, we should consider.
  2. I don’t think we should leave the Math library in an inconsistent state. I think once we start removing checks, we should just state that the postcondition is that it if it doesn’t throw, it’s not guaranteed to have been the correct result and that still needs to be checked. And while we’re doing that, we could change the precondition to only allow things within the domain of the function.

Anyone with thoughts on where we want to go with the Math library? And how to stage it properly so we can keep the contract to something sensible?

cc: @tadej @stevebronder @Bob_Carpenter @seantalts

2 Likes

Actually many functions also have preconditions that none of the inputs can be inf or nan. I am not sure if you meant that as valid or not, but it is kind of an edge case that should be mentioned.

I think the benchmark I posted in the linked issue shows that simple functions that contain checks on input and can throw would not significantly benefit from removing such checks. However performance of some functions that do not have checks would deteriorate if checks on inputs were added.

So if we are only talking about removing (not adding) checks performance is not an issue and we only need to discuss consistency across functions.

There was discussion here about giving users an option to turn the checks off. If/Once this gets implemented in a way that turns checks into no-ops, performance of checks is not an issue anymore. Once that happens I think we can add checks to every single functions, even ones that would become slower.

2 Likes

Yikes! By this, I believe you’re saying that the function will return as usual, but the output is undefined or invalid?

If that’s the case, we should be documenting that clearly because it isn’t consistent with the rest of the Math library and try to fix it.

Do you have a list of them? Other than the overloads for the standard template library?

Mostly I am thinking of ones that directley use std implementation. There might be others, but I do not have any list.

1 Like

Yup. Those are the ones I know about too.

Now that I’m thinking more carefully about this, I think what’s more consistent is if we actually add error checking to the std functions. Up until now, we’ve gone the other direction and matched our implementation to the standard template library. But this leads to not trapping errors early and propagating things forward.

I think we could go completely in the other direction and have the Math library have real preconditions on the input. When we originally did this, it was motivated by how C++ was generated by the compiler from the Stan language. If you haven’t dug in, the programs written in Stan are almost verbatim translated to C++ that uses the Math library. This doesn’t always need to happen this way. But what that allowed us to do is for us to have the Math library be the defensive part of the code and be very open to what it accepts while only returning values when they’re valid. It was also the responsibility of the Math library to catch errors early and let the user know that there are coding errors in their Stan program. I think this is still useful, but maybe less of a compelling reason to do it this way.

One way we can move away from this paradigm is to decouple the error checking from the computation of the function. In other words, split the function into: 1) validation and 2) computation. If we had two functions and our existing functions composed the two, then the first could validate and the second could have the preconditions of just the domain of the function being allowed.

Btw, this stuff gets really tricky if you start digging into it. Part of it is due to floating point arithmetic. Something that’s been thrown around is to not check NaN or infinity values. I think if we did that, we’d run into problems pretty quickly. For example, if we didn’t carefully check the input into something like the normal lpdf, we could end up with a 0 for the standard deviation. If mu and the number are both finite, the result is inifinity, if mu or the number are infinite (sign doesn’t matter), then the result is NaN. If mu and the number are the same and the standard deviation is 0, the result should be NaN, but could end up with a number of different values because “the same” isn’t always easy to represent in floating point numbers. And after all of that, the defined lpdf is probably not usable once it hits any of these conditions; so having an error sooner rather than later would help to debug this. (Not only does the value break down, but any use of the derivative also breaks down.) So… in this case, it was better to have checked than to not.

It might be worth splitting out the validation of input from the computation of the function. I can only think of a handful of places where we’d lose out on some performance, but I think the paradigm works. To completely switch our existing functions to have preconditions would be more work.

1 Like

My original motivation was that templated functions that use standard library functions should continue to work when templated and autodiff variables are plugged in. For example, we could write something like this:

auto y = foo(...);
if (isnan(y))
  y = ...do something...

that would work with double values but fail if foo() always throws rather than returning NaN.

I don’t know how important that is.

Whatever we do, I believe very strongly the double and var and fvar versions should throw in the same places. We can do that by writing a bunch of checks in front of functions like log() to make sure the inputs are not infinte and not nan. I have no idea how much that’d slow things down.

1 Like