unfoldrが有限項か判定したい
/libs/contrib/Data/CoList.idr
でCoList
とunfoldr
は以下のように実装されている。
codata CoList : Type -> Type where
Nil : CoList a
(::) : a -> CoList a -> CoList a
unfoldr : (a -> Maybe (b, a)) -> a -> CoList b
unfoldr f x =
case f x of
Just (y, new_x) => y :: (unfoldr f new_x)
_ => []
unfoldr
の結果はNil
で止まる場合と無限に続く場合に分けられる。
これを前もって分かる方法はないだろうか?
現状は部分関数で以下のように書くのが精一杯。
partial
unLimited : CoList a -> Bool
unLimited [] = False
unLimited (_ :: xs) = unLimited xs
こう書いていると無理だな、と思うのだが、
計算は出来なくても、定義は出来ないか、と思ったりもする。
停止性問題にも似ているし。
CoList
を返す関数の再帰部分は、
すぐ上にコンストラクタ(::)
を被せないといけない。
(余再帰の条件?)
module Judge1
%default total
-- # 1. 依存ペアを使う
codata CoListB : Bool -> Type -> Type where
Nil : CoListB True a
(::) : a -> DPair Bool (\b=>CoListB b a)
-> CoListB b a
unfoldrB : (a -> Maybe (Nat, a)) -> a
-> (b ** CoListB b Nat)
unfoldrB f x =
case f x of
Just (y, new_x) => (b ** the (CoListB b Nat) (y :: (unfoldrB f new_x)) )
_ => (True ** [])
- まずプログラムが通らない。
CoListB
の(::)
が、依存ペアのBool値を、末項に渡せない
→それは不可能か……Nil
から逆走してBool値True
を先頭まで持っていく算段が……
module Judge2
-- > idris -p base
import Control.Monad.State
%default total
-- # 2. Stateモナドを使う
codata CoListSt : Type -> Type where
Nil : CoListSt a
(::) : a -> State Bool (CoListSt a)
-> CoListSt a
testF : Nat -> Maybe (Nat, Nat)
testF b = if b == 0 then Nothing else Just (b, pred b)
partial
unfoldrSt : (a -> Maybe (b, a)) -> a -> State Bool (CoListSt b)
unfoldrSt f x =
case f x of
Just (y, new_x) => pure $ y :: (unfoldrSt f new_x)
_ => do
put False
pure []
-
今度は全域性チェックで引っかかる。
unfoldrSt
の戻り型がState Bool (CoListSt b)
だから、
State
にも『コンストラクタを被せなくては』ルールが付く。 -
強引に実行した結果が以下。
外側の状態が更新されない……
*Judge2> runState (unfoldrSt testF 5) True
(5 :: unfoldrSt testF 4, True) : (CoListSt Nat, Bool)
*Judge2> :x runState (unfoldrSt testF 5) True
(5 :: ST (\st => Id (4 :: ST (\st1 => Id (3 :: ST (\st2 => Id (2 :: ST (\st3 => Id (1 :: ST (\st4 => Id ([], False)), st3)), st2)), st1)), st)),
True) : (CoListSt Nat, Bool)
module Judge3
%default total
-- # 3. CoなStateを作る
corecord CoState (s : Type) (a : Type) where
constructor CoST
runCoState : s -> (a, s)
tail : CoState s a
implementation Functor (CoState s) where
map f (CoST g _) = ?rhs1
implementation Applicative (CoState s) where
pure x = CoST (\s => (x, s)) (pure x)
(CoST f _) <*> (CoST a _) = ?rhs2
implementation Monad (CoState s) where
m >>= k = CoST (\s =>
let (x, s0) = runCoState m s
in runCoState (k x) s0)
(m >>= k)
get : CoState x x
get = CoST (\s => (s, s)) get
put : s -> CoState s ()
put s = CoST (const ((), s)) (put s)
testF : Nat -> Maybe (Nat, Nat)
testF b = if b == 0 then Nothing else Just (b, pred b)
unfoldrCoSt : (a -> Maybe (Nat, a)) -> a -> CoState Bool Nat
unfoldrCoSt f x =
case f x of
Just (y, new_x) =>
CoST ( \s=> (y, s) )
(unfoldrCoSt f new_x)
_ => do
put False
pure 100
- プログラムは通るが、それだけだ。何も起こらない。
module Co2
-- > idris -p contrib
import Data.CoList
%default total
limitedNStep : CoList a -> Nat -> Bool
limitedNStep [] _ = True
limitedNStep (_ :: _) Z = False
limitedNStep (_ :: xs) (S n) = limitedNStep xs n
data Limited : CoList a -> Type where
IsLimited : (n : Nat ** limitedNStep xs n = True) -> Limited xs
-- 止まるCoList
xsCo : CoList Nat
xsCo = unfoldr (\b => if b == 0 then Nothing else Just (b, pred b)) 10
-- 止まる証明
xsCoIsLimited : Limited Co2.xsCo
xsCoIsLimited = IsLimited (10 ** Refl)
-- 失敗
xsCo2 : Nat -> CoList Nat
xsCo2 = unfoldr (\b => if b == 0 then Nothing else Just (b, b))
xsCo2IsUnLimited : Limited (xsCo2 10) -> Void
xsCo2IsUnLimited (IsLimited (Z ** prf)) = absurd prf
xsCo2IsUnLimited (IsLimited ((S n) ** prf)) = ?rhs2
-- --------------------------------------
codata DecLimited : CoList a -> Bool -> Type where
YesLimited : (n : Nat ** limitedNStep xs n = True) -> DecLimited xs True
NoLimited : (x : a) -> DecLimited xs False -> DecLimited (x :: xs) False
No2Limited : (x : a) -> (DecLimited xs True -> Void) -> DecLimited (x :: xs) False
data NonEmptyCo : CoList a -> Type where
IsNonEmptyCo : NonEmptyCo (x :: xs)
Uninhabited (NonEmptyCo []) where
uninhabited IsNonEmptyCo impossible
-- 止まる証明
xsCoIsLimited2 : DecLimited Co2.xsCo True
xsCoIsLimited2 = YesLimited (10 ** Refl)
-- 止まらない証明
xsCo2IsUnLimited2 : DecLimited (xsCo2 10) False
xsCo2IsUnLimited2 = NoLimited 10 xsCo2IsUnLimited2
-- 失敗
isUnLimited : (xs : CoList Nat) -> {auto ok : NonEmptyCo xs} -> DecLimited xs False
isUnLimited [] {ok = IsNonEmptyCo} impossible
isUnLimited (x :: []) {ok = p} = ?rhs3
isUnLimited (x1 :: x2 :: xs) {ok = p} = NoLimited x1 (isUnLimited (x2 :: xs))
-- not total
-- xsCo2IsUnLimited3 : DecLimited (xsCo2 10) False
-- xsCo2IsUnLimited3 = No2Limited 10 ?rhs4
- 定義は出来た。
- これでいきます。
関係ないけど自分用メモ
-- ----- record -----
record IsGroup (A : Type)(f : A -> A -> A)(e : A)(iF : A -> A) where
-- constructor MkIsGroup
assoc : (x, y, z : A) -> (x
f
y)f
z = xf
(yf
z)identity : (x : A) -> Pair (e
f
x = x) (xf
e = x)inv : (x : A) -> Pair ((iF x)
f
x = e) (xf
(iF x) = e)myfst : Pair a b -> a
myfst = Prelude.Basics.fst
mysnd : Pair a b -> b
mysnd = Prelude.Basics.snd
postulate B : Type
postulate f1 : B -> B -> B
postulate e1 : B
postulate iF1 : B -> B
postulate f2 : B -> B -> B
postulate e2 : B
postulate iF2 : B -> B
-- 単位元は一意
unit : (e1, e2 : B) -> IsGroup B f1 e1 iF1 -> IsGroup B f1 e2 iF1 -> e1 = e2
unit e1 e2 g1 g2 =
let id1 = myfst $ identity g1 e2;
id2 = mysnd $ identity g2 e1 in trans (sym id2) id1