righ1113/judgeFiniteUnfoldr.md

## judgeFiniteUnfoldr.md

      
    Raw
  

              judgeFiniteUnfoldr.md
            
          
    judge finite unfoldr by Idris

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を返す関数の再帰部分は、

すぐ上にコンストラクタ(::)を被せないといけない。

（余再帰の条件？）
1. 依存ペアを使う

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を先頭まで持っていく算段が……

2. Stateモナドを使う

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)
3. CoなStateを作る

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

プログラムは通るが、それだけだ。何も起こらない。

4.

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

定義は出来た。
これでいきます。