3

我正在与 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将永远是一个概率？

4

1 回答 1

3

我会从图片中删除浮点数。您几乎总是会遇到原语问题，尤其是在处理 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运行时值可能会有所帮助！

于 2015-03-02T02:06:37.700 回答