Browse Source

Construct QQ arithmetic.

idris
Thomas Kerber 1 year ago
parent
commit
ca0c684297
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
2 changed files with 71 additions and 8 deletions
  1. +51
    -7
      Yggdrasil/Distribution.idr
  2. +20
    -1
      Yggdrasil/ExecutionModel.idr

+ 51
- 7
Yggdrasil/Distribution.idr View File

@@ -6,6 +6,9 @@ import Data.QQ.SternBrocot
import Data.ZZ
import Yggdrasil.Extensible

%access public export
%default total

interface Sampler s where
sample : {n : Nat} -> s -> (Fin (S n), s)

@@ -31,14 +34,55 @@ allFin : (n : Nat) -> List (Fin n)
allFin Z = []
allFin (S n) = FZ :: map FS (allFin n)

Num QQ where
a + b = ?add_qq
a * b = ?mult_qq
fromInteger i = ?fromInt_qq
nzMultNzIsNz : {n : Nat} -> {m : Nat} -> LTE 1 n -> LTE 1 m -> LTE 1 (n * m)
nzMultNzIsNz {n=Z} _ _ impossible
nzMultNzIsNz {m=Z} _ _ impossible
nzMultNzIsNz {n=S n} {m=S m} _ _ = LTESucc LTEZero

nomDenomAdd : QPlus -> QPlus -> (ZZ, ZZ, Subset Nat (\x => GT x 0))
nomDenomAdd q1 q2 = let
(n1, d1) = extractQPlus q1;
(n2, d2) = extractQPlus q2;
a' = getWitness n1 * getWitness d2;
b' = getWitness n2 * getWitness d1 in
(Pos a', Pos b', Element (getWitness d1 * getWitness d2) (nzMultNzIsNz (getProof d1) (getProof d2)))

qplusMult : QPlus -> QPlus -> QPlus
qplusMult q1 q2 = let
(n1, d1) = extractQPlus q1;
(n2, d2) = extractQPlus q2;
n = getWitness n1 * getWitness n2;
d = getWitness d1 * getWitness d2 in
injectQPlus n d
(nzMultNzIsNz (getProof n1) (getProof n2))
(nzMultNzIsNz (getProof d1) (getProof d2))


mutual
Num QQ where
Zero + b = b
b + Zero = b
(Neg a) + (Neg b) = let (a, b, c) = nomDenomAdd a b in
(#) (negate (b + a)) (getWitness c) {dGtZ=getProof c}
(Neg a) + (Pos b) = let (a, b, c) = nomDenomAdd a b in
(#) (b - a) (getWitness c) {dGtZ=getProof c}
(Pos a) + (Pos b) = let (a, b, c) = nomDenomAdd a b in
(#) (a + b) (getWitness c) {dGtZ=getProof c}
(Pos a) + (Neg b) = let (a, b, c) = nomDenomAdd a b in
(#) (a - b) (getWitness c) {dGtZ=getProof c}
Zero * _ = Zero
_ * Zero = Zero
(Neg a) * (Neg b) = Pos (qplusMult a b)
(Neg a) * (Pos b) = Neg (qplusMult a b)
(Pos a) * (Neg b) = Neg (qplusMult a b)
(Pos a) * (Pos b) = Pos (qplusMult a b)
fromInteger i = fromInteger i # 1

Neg QQ where
negate q = ?negate_qq
a - b = ?subtract_qq
Neg QQ where
negate Zero = Zero
negate (Pos q) = (Neg q)
negate (Neg q) = (Pos q)
a - b = a + (negate b)

data Event : (a -> Bool) -> D a -> QQ -> Type where
||| If `f x` is true, it's pure distribution has probability 1.

+ 20
- 1
Yggdrasil/ExecutionModel.idr View File

@@ -1,3 +1,22 @@
module Yggdrasil.ExecutionModel

import Control.ST
--import Control.ST
import Yggdrasil.Distribution

data Action : Type -> Type -> Type where
Abort : Action s a
SecParam : Action s Nat
Sample : D a -> Action s a
-- Create : ??? (ST doesn't seem to do quite what we want...)
Compose : Action s a -> (a -> Action s b) -> Action s b

mutual
Functor (Action s) where
map f x = Compose x (pure . f)

Applicative (Action s) where
pure = Sample . pure
f <*> x = Compose f (\f' => map f' x)

Monad (Action s) where
(>>=) = Compose

Loading…
Cancel
Save