3

私は Idris と少し作業しており、確率の型を作成しました -とFloatの間の0.0s 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

LTENatは、最初の値が 2 番目の値以下の場合にのみ値が存在する型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))

もう 1 つの利点は、に変換するまでこれが任意の精度であることFloatです。

問題は、おそらく大きなLTE値を構築する必要があることです。isLTEランタイム値に使用すると、おそらくここで役立ちます!

于 2015-03-02T02:06:37.700 に答える