proof - 你如何证明概率在依赖类型的乘法下是封闭的？

Question

我在 Idris 上工作了一点，我写了一个概率类型 - Float 介于 0.0 和 1.0 之间:

data Probability : Type where
    MkProbability : (x : Float) -> ((x >= 0.0) && (x <= 1.0) = True) -> Probability

我希望能够将它们相乘:

multProbability : Probability -> Probability -> Probability
multProbability (MkProbability p1 proof1) (MkProbability p2 proof2) =
    MkProbability (p1 * p2) ???

我如何证明 p1 * p2 永远是一个概率？

Answer 1

我会从图片中删除 float 。您几乎总是会遇到基元问题，尤其是在处理 IEEE 754 类型的奇怪细节时。

相反，我会使用比率类型表示概率:

record Probability : Type where
  MkProbability : (numerator : Nat) ->
                  (denominator : Nat) ->
                  LTE numerator (S denominator) ->
                  Probability

LTE 是一种类型，其中值仅在第一个 Nat 小于或等于第二个 Nat 时存在。 (S denominator) 是为了确保我们没有零分母。这意味着 MkProbability 2 1 (LTESucc LTEZero) 是有效的并且表示概率 1.0，看起来很奇怪但确保有效性。

然后我们可以从类型中得到一个Float:

toFloat : Probability -> Float
toFloat (MkProbability n d _) =
  fromInteger (toIntegerNat n) / fromInteger (toIntegerNat (S d))

另一个好处是，在我们转换为 Float 之前，这是任意精度。

一个问题是您可能必须构建较大的 LTE 值。使用 isLTE 作为运行时值可能会有所帮助!