It does not offer convenient ways to extract the numerator or the denominator from an existing Rational value, however. That is, there are no functions of these types:
This issue tracks whether we should add such functions or not.
What's the risk?
At first glance, it seems like it should be straightforward to implement these. Before we return the numerator or denominator, we need to ensure that they are normalized so that, e.g., numerator (ratio 6 10) == 3 and denominator (ratio 6 10) == 5. To do so, we can compute the greatest common divisor (gcd) of both Integers and divide them by the gcd. For instance, the gcd of 6 and 10 is 2, and indeed we have that 6/2 == 3 and 10/2 == 5.
This plan will work well for concrete Rational values, but what about symbolicRational values? (Recall that these can arise when :prove-ing properties about Rationals.) It is unclear to me how to implement gcd in a way such that SMT solvers can efficiently reason about it. The usual, recursive definition of gcd is:
gcd x y = gcd' (abs x) (abs y)
where
gcd' a b =
if b == 0
then a
else gcd' b (a % b)
This is recursive in the gcd's second argument, but the termination criteria is not very obvious. As such, I suspect that most SMT solvers would infinitely loop if it had to reason about any properties involving gcd.
Accept the risk?
If we can't make numerator/denominator work efficiently for symbolic Rationals, then perhaps we could still add these operations, but prominently advertise that they are not designed to work well with :prove. Would that be an unusual thing to do? I'm not aware of any other Cryptol primitives that are anti–SMT reasoning to quite the same extent, but perhaps I'm just not aware of them.
Don't risk it?
If we decide that adding numerator/denominator is a bad idea, then at the very least, we should document this choice somewhere, as the topic of deconstructing Rational values comes up quite frequently. Perhaps the documentation for Rational would be a good place for this.
Currently, Cryptol offers a way to construct a
Rational
value from a numerator and a denominator:https://github.com/GaloisInc/cryptol/blob/09853251186d4590f3b093dbdf2b324c9a7e6ca0/lib/Cryptol.cry#L780
It does not offer convenient ways to extract the numerator or the denominator from an existing
Rational
value, however. That is, there are no functions of these types:This issue tracks whether we should add such functions or not.
What's the risk?
At first glance, it seems like it should be straightforward to implement these. Before we return the numerator or denominator, we need to ensure that they are normalized so that, e.g.,
numerator (ratio 6 10) == 3
anddenominator (ratio 6 10) == 5
. To do so, we can compute the greatest common divisor (gcd) of bothInteger
s and divide them by the gcd. For instance, the gcd of6
and10
is2
, and indeed we have that6/2 == 3
and10/2 == 5
.This plan will work well for concrete
Rational
values, but what about symbolicRational
values? (Recall that these can arise when:prove
-ing properties aboutRational
s.) It is unclear to me how to implement gcd in a way such that SMT solvers can efficiently reason about it. The usual, recursive definition of gcd is:This is recursive in the gcd's second argument, but the termination criteria is not very obvious. As such, I suspect that most SMT solvers would infinitely loop if it had to reason about any properties involving gcd.
Accept the risk?
If we can't make
numerator
/denominator
work efficiently for symbolicRational
s, then perhaps we could still add these operations, but prominently advertise that they are not designed to work well with:prove
. Would that be an unusual thing to do? I'm not aware of any other Cryptol primitives that are anti–SMT reasoning to quite the same extent, but perhaps I'm just not aware of them.Don't risk it?
If we decide that adding
numerator
/denominator
is a bad idea, then at the very least, we should document this choice somewhere, as the topic of deconstructingRational
values comes up quite frequently. Perhaps the documentation forRational
would be a good place for this.